(* *********************************************************************) (* *) (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU Lesser General Public License as *) (* published by the Free Software Foundation, either version 2.1 of *) (* the License, or (at your option) any later version. *) (* This file is also distributed under the terms of the *) (* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) open C open Camlcoq open! Floats open Values open Ctypes open Csyntax (** ** Extracting information about global variables from their atom *) (** Record useful information about global variables and functions, and associate it with the corresponding atoms. *) type inline_status = | No_specifier (* No inline specifier and no noinline attribute *) | Noinline (* The atom is declared with the noinline attribute *) | Inline (* The atom is declared inline *) type atom_info = { a_storage: C.storage; (* storage class *) a_size: int64 option; (* size in bytes *) a_alignment: int option; (* alignment *) a_sections: Sections.section_name list; (* in which section to put it *) (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *) a_access: Sections.access_mode; (* access mode, e.g. small data area *) a_inline: inline_status; (* function declared inline? *) a_loc: location (* source location *) } let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 let atom_is_static a = try (Hashtbl.find decl_atom a).a_storage = C.Storage_static with Not_found -> false let atom_is_extern a = try (Hashtbl.find decl_atom a).a_storage = C.Storage_extern with Not_found -> false let atom_alignof a = try (Hashtbl.find decl_atom a).a_alignment with Not_found -> None let atom_is_aligned a sz = match atom_alignof a with | None -> false | Some align -> align mod (Z.to_int sz) = 0 let atom_sections a = try (Hashtbl.find decl_atom a).a_sections with Not_found -> [] let atom_is_small_data a ofs = try let info = Hashtbl.find decl_atom a in info.a_access = Sections.Access_near && (match info.a_size with | None -> false | Some sz -> let ofs = camlint64_of_ptrofs ofs in 0L <= ofs && ofs < sz) with Not_found -> false let atom_is_rel_data a ofs = try (Hashtbl.find decl_atom a).a_access = Sections.Access_far with Not_found -> false let atom_inline a = try (Hashtbl.find decl_atom a).a_inline with Not_found -> No_specifier (** Iso C99 defines inline definitions of functions as functions with inline specifier and without extern. These functions do not provide an external definition. In the case of non static functions this means that no code should be generated for these functions. *) let atom_is_iso_inline_definition a = try let i = Hashtbl.find decl_atom a in match i.a_storage with | C.Storage_default -> i.a_inline = Inline | _ -> false with Not_found -> false let atom_location a = try (Hashtbl.find decl_atom a).a_loc with Not_found -> Cutil.no_loc (** The current environment of composite definitions *) let comp_env : composite_env ref = ref Maps.PTree.empty (** Hooks -- overridden in machine-dependent CPragmas module *) let process_pragma_hook = ref (fun (_: string) -> false) (** ** Error handling *) let currentLocation = ref Cutil.no_loc let updateLoc l = currentLocation := l let currentFunction = ref "" let updateFunction f = currentFunction := f let error fmt = Diagnostics.error !currentLocation fmt let fatal_error fmt = Diagnostics.fatal_error !currentLocation fmt let unsupported msg = Diagnostics.error !currentLocation "unsupported feature: %s" msg let warning t msg = Diagnostics.warning !currentLocation t msg let string_of_errmsg msg = let string_of_err = function | Errors.MSG s -> camlstring_of_coqstring s | Errors.CTX i -> extern_atom i | Errors.POS i -> Z.to_string (Z.Zpos i) in String.concat "" (List.map string_of_err msg) (** ** The builtin environment *) let ais_annot_functions = if Configuration.elf_target then [(* Ais Annotations, only available for ELF targets *) "__builtin_ais_annot", (TVoid [], [TPtr(TInt(IChar, [AConst]), [])], true);] else [] let builtins_generic = { builtin_typedefs = []; builtin_functions = ais_annot_functions @ [ (* Integer arithmetic *) "__builtin_bswap64", (TInt(IULongLong, []), [TInt(IULongLong, [])], false); "__builtin_bswap", (TInt(IUInt, []), [TInt(IUInt, [])], false); "__builtin_bswap32", (TInt(IUInt, []), [TInt(IUInt, [])], false); "__builtin_bswap16", (TInt(IUShort, []), [TInt(IUShort, [])], false); "__builtin_clz", (TInt(IInt, []), [TInt(IUInt, [])], false); "__builtin_clzl", (TInt(IInt, []), [TInt(IULong, [])], false); "__builtin_clzll", (TInt(IInt, []), [TInt(IULongLong, [])], false); "__builtin_ctz", (TInt(IInt, []), [TInt(IUInt, [])], false); "__builtin_ctzl", (TInt(IInt, []), [TInt(IULong, [])], false); "__builtin_ctzll", (TInt(IInt, []), [TInt(IULongLong, [])], false); (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); "__builtin_fabsf", (TFloat(FFloat, []), [TFloat(FFloat, [])], false); (* Float arithmetic *) "__builtin_fsqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); "__builtin_sqrt", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [AConst], []); TInt(IULong, []); TInt(IULong, [])], false); (* Selection *) "__builtin_sel", (TVoid [], [TInt(C.IBool, [])], true); (* Annotations *) "__builtin_annot", (TVoid [], [TPtr(TInt(IChar, [AConst]), [])], true); "__builtin_annot_intval", (TInt(IInt, []), [TPtr(TInt(IChar, [AConst]), []); TInt(IInt, [])], false); (* Software memory barrier *) "__builtin_membar", (TVoid [], [], false); (* Variable arguments *) (* va_start(ap,n) (preprocessing) --> __builtin_va_start(ap, arg) (elaboration) --> __builtin_va_start(ap) *) "__builtin_va_start", (TVoid [], [TPtr(TVoid [], [])], false); (* va_arg(ap, ty) (preprocessing) --> __builtin_va_arg(ap, ty) (parsing) --> __builtin_va_arg(ap, sizeof(ty)) *) "__builtin_va_arg", (TVoid [], [TPtr(TVoid [], []); TInt(IUInt, [])], false); "__builtin_va_copy", (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false); "__builtin_va_end", (TVoid [], [TPtr(TVoid [], [])], false); (* Optimization hints *) "__builtin_unreachable", (TVoid [], [], false); "__builtin_expect", (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false) ] } (* Add processor-dependent builtins *) let builtins = { builtin_typedefs = builtins_generic.builtin_typedefs @ CBuiltins.builtins.builtin_typedefs; builtin_functions = builtins_generic.builtin_functions @ CBuiltins.builtins.builtin_functions } (** ** The known attributes *) let attributes = [ (* type-related -- currently none *) (* struct-related *) ("packed", Cutil.Attr_struct); (* function-related *) ("noreturn", Cutil.Attr_function); ("noinline",Cutil.Attr_function); (* name-related *) ("aligned", Cutil.Attr_name); (* object-related *) ("section", Cutil.Attr_object); ("unused", Cutil.Attr_object) ] (** ** Handling of inlined memcpy functions *) let constant_size_t a = match Initializers.constval_cast !comp_env a Ctyping.size_t with | Errors.OK(Vint n) -> Some(Integers.Int.unsigned n) | Errors.OK(Vlong n) -> Some(Integers.Int64.unsigned n) | _ -> None let make_builtin_memcpy args = match args with | Econs(dst, Econs(src, Econs(sz, Econs(al, Enil)))) -> let sz1 = match constant_size_t sz with | Some n -> n | None -> error "size argument of '__builtin_memcpy_aligned' must be a constant"; Z.zero in let al1 = match constant_size_t al with | Some n -> n | None -> error "alignment argument of '__builtin_memcpy_aligned' must be a constant"; Z.one in if not (Z.is_power2 al1) then error "alignment argument of '__builtin_memcpy_aligned' must be a power of 2"; if not (Z.eq (Z.modulo sz1 al1) Z.zero) then error "alignment argument of '__builtin_memcpy_aligned' must be a divisor of the size"; (* Issue #28: must decay array types to pointer types *) Ebuiltin( AST.EF_memcpy(sz1, al1), Tcons(typeconv(typeof dst), Tcons(typeconv(typeof src), Tnil)), Econs(dst, Econs(src, Enil)), Tvoid) | _ -> assert false (** ** Translation of [va_arg] for variadic functions. *) let va_list_ptr e = if not CBuiltins.va_list_scalar then e else match e with | Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr)) | _ -> error "bad use of a va_list object"; e let make_builtin_va_arg_by_val helper ty ty_ret arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, AST.cc_default) in Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), Econs(va_list_ptr arg, Enil), ty_ret), ty) let make_builtin_va_arg_by_ref helper ty arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tcons(Ctyping.size_t, Tnil)), Tpointer(Tvoid, noattr), AST.cc_default) in let ty_ptr = Tpointer(ty, noattr) in let call = Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), Econs(va_list_ptr arg, Econs(Esizeof(ty, Ctyping.size_t), Enil)), Tpointer(Tvoid, noattr)) in Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) let make_builtin_va_arg env ty e = match ty with | Ctypes.Tint _ -> make_builtin_va_arg_by_val "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e | Tpointer _ when Archi.ptr64 = false -> make_builtin_va_arg_by_val "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e | Tpointer _ when Archi.ptr64 = true -> make_builtin_va_arg_by_val "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e | Tlong _ -> make_builtin_va_arg_by_val "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e | Tfloat _ -> make_builtin_va_arg_by_val "__compcert_va_float64" ty (Tfloat(F64, noattr)) e | Tstruct _ | Tunion _ -> make_builtin_va_arg_by_ref "__compcert_va_composite" ty e | _ -> unsupported "va_arg at this type"; Eval(Vint(coqint_of_camlint 0l), type_int32s) (** ** Translation functions *) (** Constants *) let convertInt32 (n: int64) = coqint_of_camlint(Int64.to_int32 n) let convertInt64 (n: int64) = coqint_of_camlint64 n let convertIntZ (n: int64) = Z.of_sint64 n (** Attributes *) let rec log2 n = if n = 1 then 0 else 1 + log2 (n lsr 1) let convertAttr a = { attr_volatile = List.mem AVolatile a; attr_alignas = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } let convertCallconv _tres targs va attr = let vararg = match targs with | None -> None | Some tl -> if va then Some (Z.of_uint (List.length tl)) else None in let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in { AST.cc_vararg = vararg; AST.cc_unproto = (targs = None); AST.cc_structret = (sr <> []) } (** Types *) let convertIkind k a : coq_type = match k with | C.IBool -> Tint (Ctypes.IBool, Unsigned, a) | C.IChar -> Tint (I8, (if Machine.((!config).char_signed) then Signed else Unsigned), a) | C.ISChar -> Tint (I8, Signed, a) | C.IUChar -> Tint (I8, Unsigned, a) | C.IInt -> Tint (I32, Signed, a) | C.IUInt -> Tint (I32, Unsigned, a) | C.IShort -> Tint (I16, Signed, a) | C.IUShort -> Tint (I16, Unsigned, a) | C.ILong -> if Machine.((!config).sizeof_long) = 8 then Tlong (Signed, a) else Tint (I32, Signed, a) | C.IULong -> if Machine.((!config).sizeof_long) = 8 then Tlong (Unsigned, a) else Tint (I32, Unsigned, a) | C.ILongLong -> Tlong (Signed, a) | C.IULongLong -> Tlong (Unsigned, a) let convertFkind k a : coq_type = match k with | C.FFloat -> Tfloat (F32, a) | C.FDouble -> Tfloat (F64, a) | C.FLongDouble -> if not !Clflags.option_flongdouble then unsupported "'long double' type"; Tfloat (F64, a) let checkResultType env ty = if (not !Clflags.option_fstruct_passing) && Cutil.is_composite_type env ty then unsupported "function returning a struct or union \ (consider adding option [-fstruct-passing])" let checkArgumentType env ty = if (not !Clflags.option_fstruct_passing) && Cutil.is_composite_type env ty then unsupported "function parameter of struct or union type \ (consider adding option [-fstruct-passing])" let checkFunctionType env tres targs = checkResultType env tres; begin match targs with | None -> () | Some l -> List.iter (fun (id, ty) -> checkArgumentType env ty) l end let rec convertTyp env ?bitwidth t = match t with | C.TVoid a -> Tvoid | C.TInt(ik, a) -> convertIkind ik (convertAttr a) | C.TFloat(fk, a) -> convertFkind fk (convertAttr a) | C.TPtr(ty, a) -> Tpointer(convertTyp env ty, convertAttr a) | C.TArray(ty, None, a) -> (* Cparser verified that the type ty[] occurs only in contexts that are safe for Clight, so just treat as ty[0]. *) (* warning "array type of unspecified size"; *) Tarray(convertTyp env ty, Z.zero, convertAttr a) | C.TArray(ty, Some sz, a) -> Tarray(convertTyp env ty, convertIntZ sz, convertAttr a) | C.TFun(tres, targs, va, a) -> checkFunctionType env tres targs; Tfunction(begin match targs with | None -> Tnil | Some tl -> convertParams env tl end, convertTyp env tres, convertCallconv tres targs va a) | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> Ctypes.Tstruct(intern_string id.name, convertAttr a) | C.TUnion(id, a) -> Tunion(intern_string id.name, convertAttr a) | C.TEnum(id, a) -> let ik = match bitwidth with | None -> Cutil.enum_ikind | Some w -> let info = Env.find_enum env id in let representable sg = List.for_all (fun (_, v, _) -> Cutil.int_representable v w sg) info.Env.ei_members in if representable false then Cutil.unsigned_ikind_of Cutil.enum_ikind else if representable true then Cutil.signed_ikind_of Cutil.enum_ikind else Cutil.enum_ikind in convertIkind ik (convertAttr a) and convertParams env = function | [] -> Tnil | (id, ty) :: rem -> Tcons(convertTyp env ty, convertParams env rem) (* Convert types for the arguments to a function call. The types for fixed arguments are taken from the function prototype. The types for other arguments (variable-argument function or unprototyped K&R functions) are taken from the types of the function arguments, after default argument conversion. *) let rec convertTypArgs env tl el = match tl, el with | _, [] -> Tnil | [], e1 :: el -> Tcons(convertTyp env (Cutil.default_argument_conversion env e1.etyp), convertTypArgs env [] el) | (id, t1) :: tl, e1 :: el -> Tcons(convertTyp env t1, convertTypArgs env tl el) (* Convert types for the arguments to inline asm statements and to the special built-in functions __builtin_annot, __builtin_ais_annot_ and __builtin_debug. The types are taken from the types of the arguments, after performing the usual unary conversions. Hence char becomes int but float remains float and is not promoted to double. The goal is to preserve the representation of the arguments and avoid inserting compiled code to convert the arguments. *) let rec convertTypAnnotArgs env = function | [] -> Tnil | e1 :: el -> Tcons(convertTyp env (Cutil.unary_conversion env e1.etyp), convertTypAnnotArgs env el) let convertField env sid f = let id = intern_string f.fld_name and ty = convertTyp env ?bitwidth: f.fld_bitfield f.fld_typ in Debug.set_member_atom ~str_id:sid f.fld_name ~fld_id:id; match f.fld_bitfield with | None -> Member_plain(id, ty) | Some w -> match ty with | Tint(sz, sg, attr) -> Member_bitfield(id, sz, sg, attr, Z.of_uint w, f.fld_name = "") | _ -> fatal_error "bitfield must have type int" let convertCompositedef env su id attr members = if Cutil.find_custom_attributes ["packed";"__packed__"] attr <> [] then unsupported "packed struct (consider adding option [-fpacked-structs])"; let intern_name = intern_string id.name in let (t, su') = match su with | C.Struct -> TStruct (id, attr), Ctypes.Struct | C.Union -> TUnion (id, attr), Ctypes.Union in Debug.set_composite_size id intern_name su (Cutil.sizeof env t); let ms = List.map (convertField env intern_name) members in Composite(intern_name, su', ms, convertAttr attr) let rec projFunType env ty = match Cutil.unroll env ty with | TFun(res, args, vararg, attr) -> Some(res, args, vararg) | TPtr(ty', attr) -> projFunType env ty' | _ -> None let string_of_type ty = let b = Buffer.create 20 in let fb = Format.formatter_of_buffer b in Cprint.typ fb ty; Format.pp_print_flush fb (); Buffer.contents b let is_int64 env ty = match Cutil.unroll env ty with | C.TInt(k, _) -> Cutil.sizeof_ikind k = 8 | C.TEnum(_, _) -> false | _ -> assert false (** String literals *) let stringNum = ref 0 (* number of next global for string literals *) let stringTable : (string, AST.ident) Hashtbl.t = Hashtbl.create 47 let wstringTable : (int64 list * ikind, AST.ident) Hashtbl.t = Hashtbl.create 47 let is_C_string s = not (String.contains s '\000') let name_for_string_literal s = try Hashtbl.find stringTable s with Not_found -> incr stringNum; let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in let mergeable = if is_C_string s then 1 else 0 in Hashtbl.add decl_atom id { a_storage = C.Storage_static; a_alignment = Some 1; a_size = Some (Int64.of_int (String.length s + 1)); a_sections = [Sections.for_stringlit mergeable]; a_access = Sections.Access_default; a_inline = No_specifier; a_loc = Cutil.no_loc }; Hashtbl.add stringTable s id; id let typeStringLiteral s = let sg = if Machine.((!config).char_signed) then Signed else Unsigned in Tarray(Tint(I8, sg, noattr), Z.of_uint (String.length s + 1), noattr) let global_for_string s id = let init = ref [] in let add_char c = init := AST.Init_int8(Z.of_uint(Char.code c)) :: !init in add_char '\000'; for i = String.length s - 1 downto 0 do add_char s.[i] done; AST.(id, Gvar { gvar_info = typeStringLiteral s; gvar_init = !init; gvar_readonly = true; gvar_volatile = false}) let is_C_wide_string s = not (List.mem 0L s) let name_for_wide_string_literal s ik = try Hashtbl.find wstringTable (s, ik) with Not_found -> incr stringNum; let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in let wchar_size = Cutil.sizeof_ikind ik in let mergeable = if is_C_wide_string s then wchar_size else 0 in Hashtbl.add decl_atom id { a_storage = C.Storage_static; a_alignment = Some wchar_size; a_size = Some (Int64.(mul (of_int (List.length s + 1)) (of_int wchar_size))); a_sections = [Sections.for_stringlit mergeable]; a_access = Sections.Access_default; a_inline = No_specifier; a_loc = Cutil.no_loc }; Hashtbl.add wstringTable (s, ik) id; id let typeWideStringLiteral s ik = Tarray(convertIkind ik noattr, Z.of_uint (List.length s + 1), noattr) let global_for_wide_string (s, ik) id = let init = ref [] in let init_of_char = match Cutil.sizeof_ikind ik with | 2 -> (fun z -> AST.Init_int16 z) | 4 -> (fun z -> AST.Init_int32 z) | _ -> assert false in let add_char c = init := init_of_char(Z.of_uint64 c) :: !init in List.iter add_char s; add_char 0L; AST.(id, Gvar { gvar_info = typeWideStringLiteral s ik; gvar_init = List.rev !init; gvar_readonly = true; gvar_volatile = false}) let globals_for_strings globs = let globs1 = Hashtbl.fold (fun s id l -> global_for_wide_string s id :: l) wstringTable globs in let globs2 = Hashtbl.fold (fun s id l -> global_for_string s id :: l) stringTable globs1 in globs2 (** Floating point constants *) let z_of_str hex str fst = let res = ref Z.Z0 in let base = if hex then 16 else 10 in for i = fst to String.length str - 1 do let d = int_of_char str.[i] in let d = if hex && d >= int_of_char 'a' && d <= int_of_char 'f' then d - int_of_char 'a' + 10 else if hex && d >= int_of_char 'A' && d <= int_of_char 'F' then d - int_of_char 'A' + 10 else d - int_of_char '0' in assert (d >= 0 && d < base); res := Z.add (Z.mul (Z.of_uint base) !res) (Z.of_uint d) done; !res let checkFloatOverflow f typ = match f with | Binary.B754_finite _ -> () | Binary.B754_zero _ -> warning Diagnostics.Literal_range "magnitude of floating-point constant too small for type '%s'" typ | Binary.B754_infinity _ -> warning Diagnostics.Literal_range "magnitude of floating-point constant too large for type '%s'" typ | Binary.B754_nan _ -> warning Diagnostics.Literal_range "floating-point converts converts to 'NaN'" let convertFloat f kind = let mant = z_of_str f.C.hex (f.C.intPart ^ f.C.fracPart) 0 in match mant with | Z.Z0 -> begin match kind with | FFloat -> Ctyping.econst_single (Float.to_single Float.zero) | FDouble | FLongDouble -> Ctyping.econst_float Float.zero end | Z.Zpos mant -> let sgExp = match f.C.exp.[0] with '+' | '-' -> true | _ -> false in let exp = z_of_str false f.C.exp (if sgExp then 1 else 0) in let exp = if f.C.exp.[0] = '-' then Z.neg exp else exp in let shift_exp = (if f.C.hex then 4 else 1) * String.length f.C.fracPart in let exp = Z.sub exp (Z.of_uint shift_exp) in let base = P.of_int (if f.C.hex then 2 else 10) in begin match kind with | FFloat -> let f = Float32.from_parsed base mant exp in checkFloatOverflow f "float"; Ctyping.econst_single f | FDouble | FLongDouble -> let f = Float.from_parsed base mant exp in checkFloatOverflow f "double"; Ctyping.econst_float f end | Z.Zneg _ -> assert false (** Expressions *) let check_volatile_bitfield env e = if Cutil.is_bitfield env e && List.mem AVolatile (Cutil.attributes_of_type env e.etyp) then warning Diagnostics.Unnamed "access to a volatile bit field, the 'volatile' qualifier is ignored" let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) let ewrap = function | Errors.OK e -> e | Errors.Error msg -> error "retyping error: %s" (string_of_errmsg msg); ezero let rec convertExpr env e = match e.edesc with | C.EConst (C.CStr _ | C.CWStr _) | C.EVar _ | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) | C.EBinop(C.Oindex, _, _, _) -> let l = convertLvalue env e in check_volatile_bitfield env e; ewrap (Ctyping.evalof l) | C.EConst(C.CInt(i, k, _)) -> let sg = if Cutil.is_signed_ikind k then Signed else Unsigned in if Cutil.sizeof_ikind k = 8 then Ctyping.econst_long (convertInt64 i) sg else Ctyping.econst_int (convertInt32 i) sg | C.EConst(C.CFloat(f, k)) -> if k = C.FLongDouble && not !Clflags.option_flongdouble then unsupported "'long double' floating-point constant"; convertFloat f k | C.EConst(C.CEnum(id, i)) -> Ctyping.econst_int (convertInt32 i) Signed | C.ESizeof ty1 -> Ctyping.esizeof (convertTyp env ty1) | C.EAlignof ty1 -> Ctyping.ealignof (convertTyp env ty1) | C.EUnop(C.Ominus, e1) -> ewrap (Ctyping.eunop Cop.Oneg (convertExpr env e1)) | C.EUnop(C.Oplus, e1) -> convertExpr env e1 | C.EUnop(C.Olognot, e1) -> ewrap (Ctyping.eunop Cop.Onotbool (convertExpr env e1)) | C.EUnop(C.Onot, e1) -> ewrap (Ctyping.eunop Cop.Onotint (convertExpr env e1)) | C.EUnop(C.Oaddrof, e1) -> ewrap (Ctyping.eaddrof (convertLvalue env e1)) | C.EUnop(C.Opreincr, e1) -> ewrap (Ctyping.epreincr (convertLvalue env e1)) | C.EUnop(C.Opredecr, e1) -> ewrap (Ctyping.epredecr (convertLvalue env e1)) | C.EUnop(C.Opostincr, e1) -> ewrap (Ctyping.epostincr (convertLvalue env e1)) | C.EUnop(C.Opostdecr, e1) -> ewrap (Ctyping.epostdecr (convertLvalue env e1)) | C.EBinop((C.Oadd|C.Osub|C.Omul|C.Odiv|C.Omod|C.Oand|C.Oor|C.Oxor| C.Oshl|C.Oshr|C.Oeq|C.One|C.Olt|C.Ogt|C.Ole|C.Oge) as op, e1, e2, tyres) -> let op' = match op with | C.Oadd -> Cop.Oadd | C.Osub -> Cop.Osub | C.Omul -> Cop.Omul | C.Odiv -> Cop.Odiv | C.Omod -> Cop.Omod | C.Oand -> Cop.Oand | C.Oor -> Cop.Oor | C.Oxor -> Cop.Oxor | C.Oshl -> Cop.Oshl | C.Oshr -> Cop.Oshr | C.Oeq -> Cop.Oeq | C.One -> Cop.One | C.Olt -> Cop.Olt | C.Ogt -> Cop.Ogt | C.Ole -> Cop.Ole | C.Oge -> Cop.Oge | _ -> assert false in ewrap (Ctyping.ebinop op' (convertExpr env e1) (convertExpr env e2)) | C.EBinop(C.Oassign, e1, e2, _) -> let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in if Cutil.is_composite_type env e1.etyp && List.mem AVolatile (Cutil.attributes_of_type env e1.etyp) then warning Diagnostics.Unnamed "assignment to an lvalue of volatile composite type, the 'volatile' qualifier is ignored"; if Cutil.is_composite_type env e2.etyp && List.mem AVolatile (Cutil.attributes_of_type env e2.etyp) then warning Diagnostics.Unnamed "assignment of a value of volatile composite type, the 'volatile' qualifier is ignored"; check_volatile_bitfield env e1; ewrap (Ctyping.eassign e1' e2') | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign| C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign| C.Oshl_assign|C.Oshr_assign) as op, e1, e2, tyres) -> let op' = match op with | C.Oadd_assign -> Cop.Oadd | C.Osub_assign -> Cop.Osub | C.Omul_assign -> Cop.Omul | C.Odiv_assign -> Cop.Odiv | C.Omod_assign -> Cop.Omod | C.Oand_assign -> Cop.Oand | C.Oor_assign -> Cop.Oor | C.Oxor_assign -> Cop.Oxor | C.Oshl_assign -> Cop.Oshl | C.Oshr_assign -> Cop.Oshr | _ -> assert false in let e1' = convertLvalue env e1 in let e2' = convertExpr env e2 in check_volatile_bitfield env e1; ewrap (Ctyping.eassignop op' e1' e2') | C.EBinop(C.Ocomma, e1, e2, _) -> ewrap (Ctyping.ecomma (convertExpr env e1) (convertExpr env e2)) | C.EBinop(C.Ologand, e1, e2, _) -> ewrap (Ctyping.eseqand (convertExpr env e1) (convertExpr env e2)) | C.EBinop(C.Ologor, e1, e2, _) -> ewrap (Ctyping.eseqor (convertExpr env e1) (convertExpr env e2)) | C.EConditional(e1, e2, e3) -> ewrap (Ctyping.econdition (convertExpr env e1) (convertExpr env e2) (convertExpr env e3)) | C.ECast(ty1, e1) -> ewrap (Ctyping.ecast (convertTyp env ty1) (convertExpr env e1)) | C.ECompound(ty1, ie) -> unsupported "compound literals"; ezero | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 -> error "too few arguments to function call, expected at least 2, have 0"; ezero | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) -> let (kind, args1) = match args with | {edesc = C.EConst(CInt(n,_,_))} :: args1 when n <> 0L-> (n, args1) | _::args -> error "argument 1 of '__builtin_debug' must be a non-zero constant"; (1L, args) | [] -> assert false (* catched earlier *) in let (text, args2) = match args1 with | {edesc = C.EConst(CStr(txt))} :: args2 -> (txt, args2) | {edesc = C.EVar id} :: args2 -> (id.name, args2) | _::args2 -> error "argument 2 of '__builtin_debug' must be either a string literal or a variable"; ("", args2) | [] -> assert false (* catched earlier *) in let targs2 = convertTypAnnotArgs env args2 in Ebuiltin( AST.EF_debug(P.of_int64 kind, intern_string text, typlist_of_typelist targs2), targs2, convertExprList env args2, convertTyp env e.etyp) | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypAnnotArgs env args1 in Ebuiltin( AST.EF_annot(P.of_int 1,coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "argument 1 of '__builtin_annot' must be a string literal"; ezero end | C.ECall({edesc = C.EVar {name = "__builtin_annot_intval"}}, args) -> begin match args with | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in Ebuiltin(AST.EF_annot_val(P.of_int 1,coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> error "argument 1 of '__builtin_annot_intval' must be a string literal"; ezero end | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target -> begin match args with | {edesc = C.EConst(CStr txt)} :: args1 -> let file,line = !currentLocation in let fun_name = !currentFunction in let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in let targs1 = convertTypAnnotArgs env args1 in AisAnnot.validate_ais_annot env !currentLocation txt args1; Ebuiltin( AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ txt), typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "argument 1 of '__builtin_ais_annot' must be a string literal"; ezero end | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) -> make_builtin_memcpy (convertExprList env args) | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) -> ewrap (Ctyping.eunop Cop.Oabsfloat (convertExpr env arg)) | C.ECall({edesc = C.EVar {name = "__builtin_va_start"}} as fn, [arg]) -> Ecall(convertExpr env fn, Econs(va_list_ptr(convertExpr env arg), Enil), convertTyp env e.etyp) | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; arg2]) -> make_builtin_va_arg env (convertTyp env e.etyp) (convertExpr env arg1) | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, _) -> Ecast (ezero, Tvoid) | C.ECall({edesc = C.EVar {name = "__builtin_va_copy"}}, [arg1; arg2]) -> let dst = convertExpr env arg1 in let src = convertExpr env arg2 in Ebuiltin( AST.EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4), Tcons(Tpointer(Tvoid, noattr), Tcons(Tpointer(Tvoid, noattr), Tnil)), Econs(va_list_ptr dst, Econs(va_list_ptr src, Enil)), Tvoid) | C.ECall({edesc = C.EVar {name = "__builtin_sel"}}, [arg1; arg2; arg3]) -> ewrap (Ctyping.eselection (convertExpr env arg1) (convertExpr env arg2) (convertExpr env arg3)) | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, [arg1; arg2]) -> convertExpr env arg1 | C.ECall({edesc = C.EVar {name = "printf"}}, args) when !Clflags.option_interp -> let targs = convertTypArgs env [] args and tres = convertTyp env e.etyp in let sg = signature_of_type targs tres { AST.cc_vararg = Some (coqint_of_camlint 1l); cc_unproto = false; cc_structret = false} in Ebuiltin( AST.EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) | C.ECall(fn, args) -> begin match projFunType env fn.etyp with | None -> error "wrong type for function part of a call" | Some(tres, targs, va) -> if targs = None && not !Clflags.option_funprototyped then unsupported "call to unprototyped function (consider adding option [-funprototyped])"; if va && not !Clflags.option_fvararg_calls then unsupported "call to variable-argument function (consider adding option [-fvararg-calls])" end; checkResultType env e.etyp; List.iter (fun arg -> checkArgumentType env arg.etyp) args; ewrap (Ctyping.ecall (convertExpr env fn) (convertExprList env args)) and convertLvalue env e = match e.edesc with | C.EVar id -> Evar(intern_string id.name, convertTyp env e.etyp) | C.EUnop(C.Oderef, e1) -> ewrap (Ctyping.ederef (convertExpr env e1)) | C.EUnop(C.Odot id, e1) -> ewrap (Ctyping.efield !comp_env (convertExpr env e1) (intern_string id)) | C.EUnop(C.Oarrow id, e1) -> let e1' = convertExpr env e1 in let e2' = ewrap (Ctyping.ederef e1') in let e3' = ewrap (Ctyping.evalof e2') in ewrap (Ctyping.efield !comp_env e3' (intern_string id)) | C.EBinop(C.Oindex, e1, e2, _) -> let e1' = convertExpr env e1 and e2' = convertExpr env e2 in let e3' = ewrap (Ctyping.ebinop Cop.Oadd e1' e2') in ewrap (Ctyping.ederef e3') | C.EConst(C.CStr s) -> let ty = typeStringLiteral s in Evar(name_for_string_literal s, ty) | C.EConst(C.CWStr(s, ik)) -> let ty = typeWideStringLiteral s ik in Evar(name_for_wide_string_literal s ik, ty) | _ -> error "illegal lvalue"; ezero and convertExprList env el = match el with | [] -> Enil | e1 :: el' -> Econs(convertExpr env e1, convertExprList env el') (* Extended assembly *) let convertAsm loc env txt outputs inputs clobber = let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = List.map (fun s -> coqstring_uppercase_ascii_of_camlstring s) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) let e = let tinputs = convertTypAnnotArgs env inputs' in let toutput = convertTyp env ty_res in Ebuiltin( AST.EF_inline_asm(coqstring_of_camlstring txt', signature_of_type tinputs toutput AST.cc_default, clobber'), tinputs, convertExprList env inputs', toutput) in (* Add an assignment to the output, if any *) match output' with | None -> e | Some lhs -> Eassign (convertLvalue env lhs, e, typeof e) (** Annotations for line numbers *) (** Statements *) let swrap = function | Errors.OK s -> s | Errors.Error msg -> error "retyping error: %s" (string_of_errmsg msg); Csyntax.Sskip let rec convertStmt env s = updateLoc s.sloc; match s.sdesc with | C.Sskip -> Csyntax.Sskip | C.Sdo e -> swrap (Ctyping.sdo (convertExpr env e)) | C.Sseq(s1, s2) -> let s1' = convertStmt env s1 in let s2' = convertStmt env s2 in Ssequence(s1', s2') | C.Sif(e, s1, s2) -> let te = convertExpr env e in swrap (Ctyping.sifthenelse te (convertStmt env s1) (convertStmt env s2)) | C.Swhile(e, s1) -> let te = convertExpr env e in swrap (Ctyping.swhile te (convertStmt env s1)) | C.Sdowhile(s1, e) -> let te = convertExpr env e in swrap (Ctyping.sdowhile te (convertStmt env s1)) | C.Sfor(s1, e, s2, s3) -> let te = convertExpr env e in swrap (Ctyping.sfor (convertStmt env s1) te (convertStmt env s2) (convertStmt env s3)) | C.Sbreak -> Csyntax.Sbreak | C.Scontinue -> Csyntax.Scontinue | C.Sswitch(e, s1) -> let te = convertExpr env e in swrap (Ctyping.sswitch te (convertSwitch env (is_int64 env e.etyp) s1)) | C.Slabeled(C.Slabel lbl, s1) -> Csyntax.Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> unsupported "'case' statement not in 'switch' statement"; Csyntax.Sskip | C.Slabeled(C.Sdefault, _) -> unsupported "'default' statement not in 'switch' statement"; Csyntax.Sskip | C.Sgoto lbl -> Csyntax.Sgoto(intern_string lbl) | C.Sreturn None -> Csyntax.Sreturn None | C.Sreturn(Some e) -> Csyntax.Sreturn(Some(convertExpr env e)) | C.Sblock _ -> unsupported "nested blocks"; Csyntax.Sskip | C.Sdecl _ -> unsupported "inner declarations"; Csyntax.Sskip | C.Sasm(attrs, txt, outputs, inputs, clobber) -> if not !Clflags.option_finline_asm then unsupported "inline 'asm' statement (consider adding option [-finline-asm])"; Csyntax.Sdo (convertAsm s.sloc env txt outputs inputs clobber) and convertSwitch env is_64 = function | {sdesc = C.Sskip} -> LSnil | {sdesc = C.Slabeled(lbl, s)} -> convertSwitchCase env is_64 lbl s LSnil | {sdesc = C.Sseq ({sdesc = C.Slabeled(lbl, s)}, rem)} -> convertSwitchCase env is_64 lbl s (convertSwitch env is_64 rem) | _ -> assert false and convertSwitchCase env is_64 lbl s k = let lbl' = match lbl with | C.Sdefault -> None | C.Scase(e, v) -> Some (if is_64 then Z.of_uint64 v else Z.of_uint32 (Int64.to_int32 v)) | _ -> assert false in LScons(lbl', convertStmt env s, k) (** Function definitions *) let convertFundef loc env fd = checkFunctionType env fd.fd_ret (Some fd.fd_params); updateFunction fd.fd_name.name; if fd.fd_vararg && not !Clflags.option_fvararg_calls then unsupported "variable-argument function (consider adding option [-fvararg-calls])"; let ret = convertTyp env fd.fd_ret in let params = List.map (fun (id, ty) -> let id' = intern_string id.name in Debug.atom_parameter fd.fd_name id id'; (id', convertTyp env ty)) fd.fd_params in let vars = List.map (fun (sto, id, ty, init) -> if sto = Storage_extern || sto = Storage_static then unsupported "'static' or 'extern' local variable"; if init <> None then unsupported "initialized local variable"; let id' = intern_string id.name in Debug.atom_local_variable id id'; (id', convertTyp env ty)) fd.fd_locals in let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in let noinline = Cutil.find_custom_attributes ["noinline";"__noinline__"] fd.fd_attrib <> [] in let inline = if noinline || fd.fd_vararg then (* PR#15 *) Noinline else if fd.fd_inline then Inline else No_specifier in Debug.atom_global fd.fd_name id'; Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; a_size = None; a_sections = Sections.for_function env loc id' fd.fd_attrib; a_access = Sections.Access_default; a_inline = inline; a_loc = loc }; (id', AST.Gfun(Ctypes.Internal {fn_return = ret; fn_callconv = convertCallconv fd.fd_ret (Some fd.fd_params) fd.fd_vararg fd.fd_attrib; fn_params = params; fn_vars = vars; fn_body = body'})) (** External function declaration *) let re_builtin = Str.regexp "__builtin_" let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = match convertTyp env ty with | Tfunction(args, res, cconv) -> (args, res, cconv) | _ -> assert false in let id' = intern_string id.name in let id'' = coqstring_of_camlstring id.name in let sg = signature_of_type args res cconv in let ef = if id.name = "malloc" then AST.EF_malloc else if id.name = "free" then AST.EF_free else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.builtin_functions then AST.EF_builtin(id'', sg) else AST.EF_external(id'', sg) in (id', AST.Gfun(Ctypes.External(ef, args, res, cconv))) (** Initializers *) let rec convertInit env init = match init with | C.Init_single e -> Initializers.Init_single (convertExpr env e) | C.Init_array il -> Initializers.Init_array (convertInitList env (List.rev il) Initializers.Init_nil) | C.Init_struct(_, flds) -> Initializers.Init_struct (convertInitList env (List.rev_map snd flds) Initializers.Init_nil) | C.Init_union(_, fld, i) -> Initializers.Init_union (intern_string fld.fld_name, convertInit env i) and convertInitList env il accu = match il with | [] -> accu | i :: il' -> convertInitList env il' (Initializers.Init_cons(convertInit env i, accu)) let convertInitializer env ty i = match Initializers.transl_init !comp_env (convertTyp env ty) (convertInit env i) with | Errors.OK init -> init | Errors.Error msg -> error "initializer element is not a compile-time constant (%s)" (string_of_errmsg msg); [] (** Global variable *) let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in Debug.atom_global id id'; let ty' = convertTyp env ty in let sz = Ctypes.sizeof !comp_env ty' in let al = Ctypes.alignof !comp_env ty' in let attr = Cutil.attributes_of_type env ty in let init' = match optinit with | None -> if sto = C.Storage_extern then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in let initialized = if optinit = None then Sections.Uninit else if List.exists (function AST.Init_addrof _ -> true | _ -> false) init' then Sections.Init_reloc else Sections.Init in let (section, access) = Sections.for_variable env loc id' ty initialized in if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then error "'%s' is too big (%s bytes)" id.name (Z.to_string sz); if sto <> C.Storage_extern && Cutil.incomplete_type env ty then error "'%s' has incomplete type" id.name; Hashtbl.add decl_atom id' { a_storage = sto; a_alignment = Some (Z.to_int al); a_size = Some (Z.to_int64 sz); a_sections = [section]; a_access = access; a_inline = No_specifier; a_loc = loc }; let volatile = List.mem C.AVolatile attr in let readonly = List.mem C.AConst attr && not volatile in (id', AST.Gvar { AST.gvar_info = ty'; gvar_init = init'; gvar_readonly = readonly; gvar_volatile = volatile}) (** Convert a list of global declarations. Result is a list of CompCert C global declarations (functions + variables). *) let rec convertGlobdecls env res gl = match gl with | [] -> List.rev res | g :: gl' -> updateLoc g.gloc; match g.gdesc with | C.Gdecl((sto, id, ty, optinit) as d) -> (* Functions become external declarations. Other types become variable declarations. *) begin match Cutil.unroll env ty with | TFun(tres, targs, va, a) -> if targs = None then warning Diagnostics.Unnamed "'%s' is declared without a function prototype" id.name; convertGlobdecls env (convertFundecl env d :: res) gl' | _ -> convertGlobdecls env (convertGlobvar g.gloc env d :: res) gl' end | C.Gfundef fd -> convertGlobdecls env (convertFundef g.gloc env fd :: res) gl' | C.Gcompositedecl _ | C.Gcompositedef _ | C.Gtypedef _ | C.Genumdef _ -> (* Composites are treated in a separate pass, typedefs are unrolled, and enum tags are folded. So we just skip their declarations. *) convertGlobdecls env res gl' | C.Gpragma s -> if not (!process_pragma_hook s) then warning Diagnostics.Unknown_pragmas "unknown pragma ignored"; convertGlobdecls env res gl' (** Convert struct and union declarations. Result is a list of CompCert C composite declarations. *) let rec convertCompositedefs env res gl = match gl with | [] -> List.rev res | g :: gl' -> updateLoc g.gloc; match g.gdesc with | C.Gcompositedef(su, id, a, m) -> convertCompositedefs env (convertCompositedef env su id a m :: res) gl' | _ -> convertCompositedefs env res gl' (** Add declarations for the helper functions (for varargs and for int64 arithmetic) *) let helper_functions () = [ "__compcert_va_int32", Tint(I32, Unsigned, noattr), [Tpointer(Tvoid, noattr)]; "__compcert_va_int64", Tlong(Unsigned, noattr), [Tpointer(Tvoid, noattr)]; "__compcert_va_float64", Tfloat(F64, noattr), [Tpointer(Tvoid, noattr)]; "__compcert_va_composite", Tpointer(Tvoid, noattr), [Tpointer(Tvoid, noattr); convertIkind (Cutil.size_t_ikind()) noattr]; "__compcert_i64_dtos", Tlong(Signed, noattr), [Tfloat(F64, noattr)]; "__compcert_i64_dtou", Tlong(Unsigned, noattr), [Tfloat(F64, noattr)]; "__compcert_i64_stod", Tfloat(F64, noattr), [Tlong(Signed, noattr)]; "__compcert_i64_utod", Tfloat(F64, noattr), [Tlong(Unsigned, noattr)]; "__compcert_i64_stof", Tfloat(F32, noattr), [Tlong(Signed, noattr)]; "__compcert_i64_utof", Tfloat(F32, noattr), [Tlong(Unsigned, noattr)]; "__compcert_i64_sdiv", Tlong(Signed, noattr), [Tlong(Signed, noattr); Tlong(Signed, noattr)]; "__compcert_i64_udiv", Tlong(Unsigned, noattr), [Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)]; "__compcert_i64_smod", Tlong(Signed, noattr), [Tlong(Signed, noattr); Tlong(Signed, noattr)]; "__compcert_i64_umod", Tlong(Unsigned, noattr), [Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)]; "__compcert_i64_shl", Tlong(Signed, noattr), [Tlong(Signed, noattr); Tint(I32, Signed, noattr)]; "__compcert_i64_shr", Tlong(Unsigned, noattr), [Tlong(Unsigned, noattr); Tint(I32, Signed, noattr)]; "__compcert_i64_sar", Tlong(Signed, noattr), [Tlong(Signed, noattr); Tint(I32, Signed, noattr)]; "__compcert_i64_smulh", Tlong(Signed, noattr), [Tlong(Signed, noattr); Tlong(Signed, noattr)]; "__compcert_i64_umulh", Tlong(Unsigned, noattr), [Tlong(Unsigned, noattr); Tlong(Unsigned, noattr)] ] let helper_function_declaration (name, tyres, tyargs) = let tyargs = List.fold_right (fun t tl -> Tcons(t, tl)) tyargs Tnil in let ef = AST.EF_runtime(coqstring_of_camlstring name, signature_of_type tyargs tyres AST.cc_default) in (intern_string name, AST.Gfun (Ctypes.External(ef, tyargs, tyres, AST.cc_default))) let add_helper_functions globs = List.map helper_function_declaration (helper_functions()) @ globs (** Build environment of typedefs, structs, unions and enums *) let rec translEnv env = function | [] -> env | g :: gl -> let env' = match g.gdesc with | C.Gcompositedecl(su, id, attr) -> Env.add_composite env id (Cutil.composite_info_decl su attr) | C.Gcompositedef(su, id, attr, fld) -> Env.add_composite env id (Cutil.composite_info_def env su attr fld) | C.Gtypedef(id, ty) -> Env.add_typedef env id ty | C.Genumdef(id, attr, members) -> Env.add_enum env id {Env.ei_members = members; ei_attr = attr} | _ -> env in translEnv env' gl (** Eliminate multiple declarations of globals. *) module IdentSet = Set.Make(struct type t = C.ident let compare = compare end) let cleanupGlobals p = (* First pass: determine what is defined *) let strong = ref IdentSet.empty (* def functions or variables with inits *) and weak = ref IdentSet.empty (* variables without inits *) and extern = ref IdentSet.empty in (* extern decls *) let classify_def g = updateLoc g.gloc; match g.gdesc with | C.Gfundef fd -> if IdentSet.mem fd.fd_name !strong then error "multiple definitions of %s" fd.fd_name.name; strong := IdentSet.add fd.fd_name !strong | C.Gdecl(Storage_extern, id, ty, init) -> extern := IdentSet.add id !extern | C.Gdecl(sto, id, ty, Some i) -> if IdentSet.mem id !strong then error "multiple definitions of %s" id.name; strong := IdentSet.add id !strong | C.Gdecl(sto, id, ty, None) -> weak := IdentSet.add id !weak | _ -> () in List.iter classify_def p; (* Second pass: keep "best" definition for each identifier *) let rec clean defs accu = function | [] -> accu | g :: gl -> updateLoc g.gloc; match g.gdesc with | C.Gdecl(sto, id, ty, init) -> let better_def_exists = if sto = Storage_extern then IdentSet.mem id !strong || IdentSet.mem id !weak else if init = None then IdentSet.mem id !strong else false in if IdentSet.mem id defs || better_def_exists then clean defs accu gl else clean (IdentSet.add id defs) (g :: accu) gl | C.Gfundef fd -> clean (IdentSet.add fd.fd_name defs) (g :: accu) gl | _ -> clean defs (g :: accu) gl in clean IdentSet.empty [] (List.rev p) (** Extract the list of public (non-static) names *) let public_globals gl = List.fold_left (fun accu (id, g) -> if atom_is_static id then accu else id :: accu) [] gl (** Complete the debug information of struct/unions *) (* [debug_set_struct_mem_ofs sid ((id,byte_ofs), bits)] sets the byte and bit offset information of the member [id] of the struct [sid] *) let debug_set_struct_mem_ofs sid ((id, byte_ofs), bits) = let byte_ofs = Z.to_int byte_ofs in match bits with | Full -> Debug.set_member_offset ~str_id:sid ~fld_id:id byte_ofs | Bits (sz, sg, bit_pos, width) -> let bit_pos = Z.to_int bit_pos in let sz = Z.to_int (bitalignof_intsize sz) in let bit_pos = if not !Machine.config.Machine.bitfields_msb_first then sz - bit_pos - (Z.to_int width) else bit_pos in let size = sz / 8 in Debug.set_bitfield_offset ~str_id:sid ~fld_id:id ~bit_ofs:bit_pos ~byte_ofs:byte_ofs ~size:size (* [debug_set_struct_ofs env types] sets the missing offset information of all structs in the list of composites in [types] if we compile with debug information. *) let debug_set_struct_ofs env typs = if !Clflags.option_g then List.iter (function | Composite (sid, Ctypes.Struct, ms, a) -> let layout = Ctypes.layout_struct env ms in begin match layout with | Errors.OK layout -> List.iter (debug_set_struct_mem_ofs sid) layout | Errors.Error _ -> () end | _ -> ()) typs (** Convert a [C.program] into a [Csyntax.program] *) let convertProgram p = Diagnostics.reset(); stringNum := 0; Hashtbl.clear decl_atom; Hashtbl.clear stringTable; Hashtbl.clear wstringTable; let p = cleanupGlobals (Env.initial_declarations() @ p) in try let env = translEnv Env.empty p in let typs = convertCompositedefs env [] p in match build_composite_env typs with | Errors.Error msg -> fatal_error "incorrect struct or union definition: %s" (string_of_errmsg msg) | Errors.OK ce -> comp_env := ce; let gl1 = convertGlobdecls env [] p in let gl2 = globals_for_strings gl1 in let gl3 = add_helper_functions gl2 in comp_env := Maps.PTree.empty; let p' = { prog_defs = gl3; prog_public = public_globals gl3; prog_main = intern_string !Clflags.main_function_name; prog_types = typs; prog_comp_env = ce } in debug_set_struct_ofs ce typs; Diagnostics.check_errors (); p' with Env.Error msg -> fatal_error "%s" (Env.error_message msg)