1 (* *********************************************************************)
3 (* The Compcert verified compiler *)
5 (* Xavier Leroy, INRIA Paris-Rocquencourt *)
7 (* Copyright Institut National de Recherche en Informatique et en *)
8 (* Automatique. All rights reserved. This file is distributed *)
9 (* under the terms of the GNU General Public License as published by *)
10 (* the Free Software Foundation, either version 2 of the License, or *)
11 (* (at your option) any later version. This file is also distributed *)
12 (* under the terms of the INRIA Non-Commercial License Agreement. *)
14 (* *********************************************************************)
16 (* Operations on C types and abstract syntax *)
24 (* Set and Map structures over identifiers *)
28 let compare id1 id2 = Pervasives.compare id1.stamp id2.stamp
31 module IdentSet = Set.Make(Ident)
32 module IdentMap = Map.Make(Ident)
34 (* Operations on attributes *)
36 (* Lists of attributes are kept sorted in increasing order *)
38 let rec add_attributes (al1: attributes) (al2: attributes) =
42 | a1 :: al1', a2 :: al2' ->
43 if a1 < a2 then a1 :: add_attributes al1' al2
44 else if a1 > a2 then a2 :: add_attributes al1 al2'
45 else a1 :: add_attributes al1' al2'
47 let rec remove_attributes (al1: attributes) (al2: attributes) =
48 (* viewed as sets: al1 \ al2 *)
52 | a1 :: al1', a2 :: al2' ->
53 if a1 < a2 then a1 :: remove_attributes al1' al2
54 else if a1 > a2 then remove_attributes al1 al2'
55 else remove_attributes al1' al2'
57 let rec incl_attributes (al1: attributes) (al2: attributes) =
61 | a1 :: al1', a2 :: al2' ->
63 else if a1 > a2 then incl_attributes al1 al2'
64 else incl_attributes al1' al2'
66 (* Adding top-level attributes to a type. Doesn't need to unroll defns. *)
67 (* Array types cannot carry attributes, so add them to the element type. *)
69 let rec add_attributes_type attr t =
71 | TVoid a -> TVoid (add_attributes attr a)
72 | TInt(ik, a) -> TInt(ik, add_attributes attr a)
73 | TFloat(fk, a) -> TFloat(fk, add_attributes attr a)
74 | TPtr(ty, a) -> TPtr(ty, add_attributes attr a)
75 | TArray(ty, sz, a) -> TArray(add_attributes_type attr ty, sz, a)
76 | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, add_attributes attr
78 | TNamed(s, a) -> TNamed(s, add_attributes attr a)
79 | TStruct(s, a) -> TStruct(s, add_attributes attr a)
80 | TUnion(s, a) -> TUnion(s, add_attributes attr a)
82 (* Unrolling of typedef *)
84 let rec unroll env t =
86 | TNamed(name, attr) ->
87 let ty = Env.find_typedef env name in
88 unroll env (add_attributes_type attr ty)
91 (* Extracting the attributes of a type *)
93 let rec attributes_of_type env t =
99 | TArray(ty, sz, a) -> a (* correct? *)
100 | TFun(ty, params, vararg, a) -> a
101 | TNamed(s, a) -> attributes_of_type env (unroll env t)
105 (* Changing the attributes of a type (at top-level) *)
106 (* Same hack as above for array types. *)
108 let rec change_attributes_type env (f: attributes -> attributes) t =
110 | TVoid a -> TVoid (f a)
111 | TInt(ik, a) -> TInt(ik, f a)
112 | TFloat(fk, a) -> TFloat(fk, f a)
113 | TPtr(ty, a) -> TPtr(ty, f a)
114 | TArray(ty, sz, a) ->
115 TArray(change_attributes_type env f ty, sz, a)
116 | TFun(ty, params, vararg, a) -> TFun(ty, params, vararg, f a)
118 let t1 = unroll env t in
119 let t2 = change_attributes_type env f t1 in
120 if t2 = t1 then t else t2 (* avoid useless expansion *)
121 | TStruct(s, a) -> TStruct(s, f a)
122 | TUnion(s, a) -> TUnion(s, f a)
124 let remove_attributes_type env attr t =
125 change_attributes_type env (fun a -> remove_attributes a attr) t
127 let erase_attributes_type env t =
128 change_attributes_type env (fun a -> []) t
130 (* Type compatibility *)
134 let combine_types ?(noattrs = false) env t1 t2 =
136 let comp_attr a1 a2 =
138 else if noattrs then add_attributes a1 a2
140 and comp_base x1 x2 =
141 if x1 = x2 then x2 else raise Incompat
142 and comp_array_size sz1 sz2 =
146 | Some n1, Some n2 -> if n1 = n2 then Some n2 else raise Incompat
147 and comp_conv (id, ty) =
148 match unroll env ty with
149 | TInt(kind, attr) ->
150 begin match kind with
151 | IBool | IChar | ISChar | IUChar | IShort | IUShort -> raise Incompat
154 | TFloat(kind, attr) ->
155 begin match kind with
156 | FFloat -> raise Incompat
163 | TVoid a1, TVoid a2 ->
164 TVoid(comp_attr a1 a2)
165 | TInt(ik1, a1), TInt(ik2, a2) ->
166 TInt(comp_base ik1 ik2, comp_attr a1 a2)
167 | TFloat(fk1, a1), TFloat(fk2, a2) ->
168 TFloat(comp_base fk1 fk2, comp_attr a1 a2)
169 | TPtr(ty1, a1), TPtr(ty2, a2) ->
170 TPtr(comp ty1 ty2, comp_attr a1 a2)
171 | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
172 TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
173 | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
174 let (params, vararg) =
175 match params1, params2 with
176 | None, None -> None, false
177 | None, Some l2 -> List.iter comp_conv l2; (params2, vararg2)
178 | Some l1, None -> List.iter comp_conv l1; (params1, vararg1)
179 | Some l1, Some l2 ->
180 if List.length l1 <> List.length l2 then raise Incompat;
181 (Some(List.map2 (fun (id1, ty1) (id2, ty2) -> (id2, comp ty1 ty2))
183 comp_base vararg1 vararg2)
185 TFun(comp ty1 ty2, params, vararg, comp_attr a1 a2)
186 | TNamed _, _ -> comp (unroll env t1) t2
187 | _, TNamed _ -> comp t1 (unroll env t2)
188 | TStruct(s1, a1), TStruct(s2, a2) ->
189 TStruct(comp_base s1 s2, comp_attr a1 a2)
190 | TUnion(s1, a1), TUnion(s2, a2) ->
191 TUnion(comp_base s1 s2, comp_attr a1 a2)
195 in try Some(comp t1 t2) with Incompat -> None
197 let compatible_types ?noattrs env t1 t2 =
198 match combine_types ?noattrs env t1 t2 with Some _ -> true | None -> false
200 (* Naive placement algorithm for bit fields, might not match that
203 let pack_bitfields ml =
204 let rec pack nbits = function
208 match m.fld_bitfield with
209 | None -> (nbits, ml)
212 (nbits, ms) (* bit width 0 means end of pack *)
213 else if nbits + n > 8 * !config.sizeof_int then
214 (nbits, ml) (* doesn't fit in current word *)
216 pack (nbits + n) ms (* add to current word *)
218 let (nbits, ml') = pack 0 ml in
220 if nbits <= 8 then 1 else
221 if nbits <= 16 then 2 else
222 if nbits <= 32 then 4 else
223 if nbits <= 64 then 8 else assert false in
226 (* Natural alignment, in bytes *)
228 let alignof_ikind = function
229 | IBool | IChar | ISChar | IUChar -> 1
230 | IInt | IUInt -> !config.alignof_int
231 | IShort | IUShort -> !config.alignof_short
232 | ILong | IULong -> !config.alignof_long
233 | ILongLong | IULongLong -> !config.alignof_longlong
235 let alignof_fkind = function
236 | FFloat -> !config.alignof_float
237 | FDouble -> !config.alignof_double
238 | FLongDouble -> !config.alignof_longdouble
240 (* Return natural alignment of given type, or None if the type is incomplete *)
242 let rec alignof env t =
244 | TVoid _ -> !config.alignof_void
245 | TInt(ik, _) -> Some(alignof_ikind ik)
246 | TFloat(fk, _) -> Some(alignof_fkind fk)
247 | TPtr(_, _) -> Some(!config.alignof_ptr)
248 | TArray(ty, _, _) -> alignof env ty
249 | TFun(_, _, _, _) -> !config.alignof_fun
250 | TNamed(_, _) -> alignof env (unroll env t)
251 | TStruct(name, _) ->
252 let ci = Env.find_struct env name in ci.ci_alignof
254 let ci = Env.find_union env name in ci.ci_alignof
256 (* Compute the natural alignment of a struct or union. *)
258 let alignof_struct_union env members =
259 let rec align_rec al = function
262 if m.fld_bitfield = None then begin
263 match alignof env m.fld_typ with
265 | Some a -> align_rec (max a al) rem
267 let (sz, ml') = pack_bitfields ml in
268 align_rec (max sz al) ml'
270 in align_rec 1 members
272 let align x boundary =
273 (* boundary must be a power of 2 *)
274 (x + boundary - 1) land (lnot (boundary - 1))
276 (* Size of, in bytes *)
278 let sizeof_ikind = function
279 | IBool | IChar | ISChar | IUChar -> 1
280 | IInt | IUInt -> !config.sizeof_int
281 | IShort | IUShort -> !config.sizeof_short
282 | ILong | IULong -> !config.sizeof_long
283 | ILongLong | IULongLong -> !config.sizeof_longlong
285 let sizeof_fkind = function
286 | FFloat -> !config.sizeof_float
287 | FDouble -> !config.sizeof_double
288 | FLongDouble -> !config.sizeof_longdouble
290 (* Overflow-avoiding multiplication of an int64 and an int, with
291 result in type int. *)
293 let cautious_mul (a: int64) (b: int) =
294 if b = 0 || a <= Int64.of_int (max_int / b)
295 then Some(Int64.to_int a * b)
298 (* Return size of type, in bytes, or [None] if the type is incomplete *)
300 let rec sizeof env t =
302 | TVoid _ -> !config.sizeof_void
303 | TInt(ik, _) -> Some(sizeof_ikind ik)
304 | TFloat(fk, _) -> Some(sizeof_fkind fk)
305 | TPtr(_, _) -> Some(!config.sizeof_ptr)
306 | TArray(ty, None, _) -> None
307 | TArray(ty, Some n, _) as t' ->
308 begin match sizeof env ty with
311 match cautious_mul n s with
313 | None -> error "sizeof(%a) overflows" Cprint.typ t'; Some 1
315 | TFun(_, _, _, _) -> !config.sizeof_fun
316 | TNamed(_, _) -> sizeof env (unroll env t)
317 | TStruct(name, _) ->
318 let ci = Env.find_struct env name in ci.ci_sizeof
320 let ci = Env.find_union env name in ci.ci_sizeof
322 (* Compute the size of a union.
323 It is the size is the max of the sizes of fields, rounded up to the
324 natural alignment. *)
326 let sizeof_union env members =
327 let rec sizeof_rec sz = function
329 begin match alignof_struct_union env members with
330 | None -> None (* should not happen? *)
331 | Some al -> Some (align sz al)
334 begin match sizeof env m.fld_typ with
336 | Some s -> sizeof_rec (max sz s) rem
338 in sizeof_rec 0 members
340 (* Compute the size of a struct.
341 We lay out fields consecutively, inserting padding to preserve
342 their natural alignment. *)
344 let sizeof_struct env members =
345 let rec sizeof_rec ofs = function
346 | [] | [ { fld_typ = TArray(_, None, _) } ] ->
347 (* C99: ty[] allowed as last field *)
348 begin match alignof_struct_union env members with
349 | None -> None (* should not happen? *)
350 | Some al -> Some (align ofs al)
353 if m.fld_bitfield = None then begin
354 match alignof env m.fld_typ, sizeof env m.fld_typ with
355 | Some a, Some s -> sizeof_rec (align ofs a + s) rem
358 let (sz, ml') = pack_bitfields ml in
359 sizeof_rec (align ofs sz + sz) ml'
361 in sizeof_rec 0 members
363 (* Determine whether a type is incomplete *)
365 let incomplete_type env t =
366 match sizeof env t with None -> true | Some _ -> false
368 (* Computing composite_info records *)
370 let composite_info_decl env su =
371 { ci_kind = su; ci_members = []; ci_alignof = None; ci_sizeof = None }
373 let composite_info_def env su m =
374 { ci_kind = su; ci_members = m;
375 ci_alignof = alignof_struct_union env m;
378 | Struct -> sizeof_struct env m
379 | Union -> sizeof_union env m }
381 (* Type of a function definition *)
384 TFun(fd.fd_ret, Some fd.fd_params, fd.fd_vararg, [])
386 (* Signedness of integer kinds *)
388 let is_signed_ikind = function
390 | IChar -> !config.char_signed
400 | IULongLong -> false
402 (* Conversion to unsigned ikind *)
404 let unsigned_ikind_of = function
406 | IChar | ISChar | IUChar -> IUChar
407 | IInt | IUInt -> IUInt
408 | IShort | IUShort -> IUShort
409 | ILong | IULong -> IULong
410 | ILongLong | IULongLong -> IULongLong
412 (* Some classification functions over types *)
414 let is_void_type env t =
415 match unroll env t with
419 let is_integer_type env t =
420 match unroll env t with
424 let is_arith_type env t =
425 match unroll env t with
427 | TFloat(_, _) -> true
430 let is_pointer_type env t =
431 match unroll env t with
435 let is_scalar_type env t =
436 match unroll env t with
438 | TFloat(_, _) -> true
440 | TArray _ -> true (* assume implicit decay *)
441 | TFun _ -> true (* assume implicit decay *)
444 let is_composite_type env t =
445 match unroll env t with
446 | TStruct _ | TUnion _ -> true
449 let is_function_type env t =
450 match unroll env t with
454 (* Ranking of integer kinds *)
456 let integer_rank = function
458 | IChar | ISChar | IUChar -> 2
459 | IShort | IUShort -> 3
461 | ILong | IULong -> 5
462 | ILongLong | IULongLong -> 6
464 (* Ranking of float kinds *)
466 let float_rank = function
471 (* Array and function types "decay" to pointer types in many cases *)
473 let pointer_decay env t =
474 match unroll env t with
475 | TArray(ty, _, _) -> TPtr(ty, [])
476 | TFun _ as ty -> TPtr(ty, [])
479 (* The usual unary conversions (H&S 6.3.3) *)
481 let unary_conversion env t =
482 match unroll env t with
483 (* Promotion of small integer types *)
484 | TInt(kind, attr) ->
485 begin match kind with
486 | IBool | IChar | ISChar | IUChar | IShort | IUShort ->
488 | IInt | IUInt | ILong | IULong | ILongLong | IULongLong ->
491 (* Arrays and functions decay automatically to pointers *)
492 | TArray(ty, _, _) -> TPtr(ty, [])
493 | TFun _ as ty -> TPtr(ty, [])
494 (* Other types are not changed *)
497 (* The usual binary conversions (H&S 6.3.4).
498 Applies only to arithmetic types.
499 Return the type to which both sides are to be converted. *)
501 let binary_conversion env t1 t2 =
502 let t1 = unary_conversion env t1 in
503 let t2 = unary_conversion env t2 in
504 match unroll env t1, unroll env t2 with
505 | TFloat(FLongDouble, _), (TInt _ | TFloat _) -> t1
506 | (TInt _ | TFloat _), TFloat(FLongDouble, _) -> t2
507 | TFloat(FDouble, _), (TInt _ | TFloat _) -> t1
508 | (TInt _ | TFloat _), TFloat(FDouble, _) -> t2
509 | TFloat(FFloat, _), (TInt _ | TFloat _) -> t1
510 | (TInt _), TFloat(FFloat, _) -> t2
511 | TInt(k1, _), TInt(k2, _) ->
512 if k1 = k2 then t1 else begin
513 match is_signed_ikind k1, is_signed_ikind k2 with
514 | true, true | false, false ->
515 (* take the bigger of the two types *)
516 if integer_rank k1 >= integer_rank k2 then t1 else t2
518 (* if rank (unsigned type) >= rank (signed type),
519 take the unsigned type *)
520 if integer_rank k1 >= integer_rank k2 then t1
521 (* if rank (unsigned type) < rank (signed type)
522 and all values of the unsigned type can be represented
523 in the signed type, take the signed type *)
524 else if sizeof_ikind k2 > sizeof_ikind k1 then t2
525 (* if rank (unsigned type) < rank (signed type)
526 and some values of the unsigned type cannot be represented
528 take the unsigned type corresponding to the signed type *)
529 else TInt(unsigned_ikind_of k2, [])
531 if integer_rank k2 >= integer_rank k1 then t2
532 else if sizeof_ikind k1 > sizeof_ikind k2 then t1
533 else TInt(unsigned_ikind_of k1, [])
535 | _, _ -> assert false
537 (* Conversion on function arguments (with protoypes) *)
539 let argument_conversion env t =
540 (* Arrays and functions degrade automatically to pointers *)
541 (* Other types are not changed *)
542 match unroll env t with
543 | TArray(ty, _, _) -> TPtr(ty, [])
544 | TFun _ as ty -> TPtr(ty, [])
545 | _ -> t (* preserve typedefs *)
547 (* Conversion on function arguments (old-style unprototyped, or vararg *)
550 let default_argument_conversion env t =
551 match unary_conversion env t with
552 | TFloat(FFloat, attr) -> TFloat(FDouble, attr)
555 (** Is the type Tptr(ty, a) appropriate for pointer arithmetic? *)
557 let pointer_arithmetic_ok env ty =
558 match unroll env ty with
559 | TVoid _ | TFun _ -> false
560 | _ -> not (incomplete_type env ty)
564 let find_matching_unsigned_ikind sz =
565 if sz = !config.sizeof_int then IUInt
566 else if sz = !config.sizeof_long then IULong
567 else if sz = !config.sizeof_longlong then IULongLong
570 let find_matching_signed_ikind sz =
571 if sz = !config.sizeof_int then IInt
572 else if sz = !config.sizeof_long then ILong
573 else if sz = !config.sizeof_longlong then ILongLong
576 let wchar_ikind = find_matching_unsigned_ikind !config.sizeof_wchar
577 let size_t_ikind = find_matching_unsigned_ikind !config.sizeof_size_t
578 let ptr_t_ikind = find_matching_unsigned_ikind !config.sizeof_ptr
579 let ptrdiff_t_ikind = find_matching_signed_ikind !config.sizeof_ptrdiff_t
580 let enum_ikind = IInt
582 (** The type of a constant *)
584 let type_of_constant = function
585 | CInt(_, ik, _) -> TInt(ik, [])
586 | CFloat(_, fk, _) -> TFloat(fk, [])
587 | CStr _ -> TPtr(TInt(IChar, []), []) (* XXX or array? const? *)
588 | CWStr _ -> TPtr(TInt(wchar_ikind, []), []) (* XXX or array? const? *)
589 | CEnum(_, _) -> TInt(IInt, [])
591 (* Check that a C expression is a lvalue *)
593 let rec is_lvalue env e =
594 (* Type must not be array or function *)
595 match unroll env e.etyp with
596 | TFun _ | TArray _ -> false
600 | EUnop((Oderef | Oarrow _), _) -> true
601 | EUnop(Odot _, e') -> is_lvalue env e'
602 | EBinop(Oindex, _, _, _) -> true
605 (* Check that a C expression is the literal "0", which can be used
610 | EConst(CInt(0L, _, _)) -> true
613 (* Check that an assignment is allowed *)
615 let valid_assignment env from tto =
616 match pointer_decay env from.etyp, pointer_decay env tto with
617 | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
618 | TInt _, TPtr _ -> is_literal_0 from
619 | TPtr(ty, _), TPtr(ty', _) ->
620 incl_attributes (attributes_of_type env ty) (attributes_of_type env ty')
621 && (is_void_type env ty || is_void_type env ty'
622 || compatible_types env
623 (erase_attributes_type env ty)
624 (erase_attributes_type env ty'))
625 | TStruct(s, _), TStruct(s', _) -> s = s'
626 | TUnion(s, _), TUnion(s', _) -> s = s'
629 (* Check that a cast is allowed *)
631 let valid_cast env tfrom tto =
632 compatible_types ~noattrs:true env tfrom tto ||
633 begin match unroll env tfrom, unroll env tto with
635 (* from any int-or-pointer (with array and functions decaying to pointers)
636 to any int-or-pointer *)
637 | (TInt _ | TPtr _ | TArray _ | TFun _), (TInt _ | TPtr _) -> true
638 (* between int and float types *)
639 | (TInt _ | TFloat _), (TInt _ | TFloat _) -> true
643 (* Construct an integer constant *)
646 { edesc = EConst(CInt(v, ik, "")); etyp = TInt(ik, []) }
648 (* Construct a float constant *)
650 let floatconst v fk =
651 { edesc = EConst(CFloat(v, fk, "")); etyp = TFloat(fk, []) }
653 (* Construct the literal "0" with void * type *)
656 { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
658 (* Construct a sequence *)
661 match s1.sdesc, s2.sdesc with
664 | _, Sblock sl -> { sdesc = Sblock(s1 :: sl); sloc = loc }
665 | _, _ -> { sdesc = Sseq(s1, s2); sloc = loc }
667 (* Construct an assignment statement *)
669 let sassign loc lv rv =
670 { sdesc = Sdo {edesc = EBinop(Oassign, lv, rv, lv.etyp); etyp = lv.etyp};
675 let no_loc = ("", -1)
677 (* Dummy skip statement *)
679 let sskip = { sdesc = Sskip; sloc = no_loc }
681 (* Print a location *)
683 let printloc oc (filename, lineno) =
684 if filename <> "" then Printf.fprintf oc "%s:%d: " filename lineno
686 (* Format a location *)
688 let formatloc pp (filename, lineno) =
689 if filename <> "" then Format.fprintf pp "%s:%d: " filename lineno