(* *********************************************************************) (* *) (* 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 match (Hashtbl.find decl_atom a).a_storage with | C.Storage_static | C.Storage_thread_local_static -> true | _ -> false with Not_found -> false let atom_is_extern a = try match (Hashtbl.find decl_atom a).a_storage with | C.Storage_extern| C.Storage_thread_local_extern -> true | _ -> false with Not_found -> false let atom_is_thread_local a = try match (Hashtbl.find decl_atom a).a_storage with | C.Storage_thread_local_extern| C.Storage_thread_local_static | C.Storage_thread_local -> true | _ -> false 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 @ [ "__builtin_expect", (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false); (* 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); (* Helper functions for int64 arithmetic *) "__compcert_i64_dtos", (TInt(ILongLong, []), [TFloat(FDouble, [])], false); "__compcert_i64_dtou", (TInt(IULongLong, []), [TFloat(FDouble, [])], false); "__compcert_i64_stod", (TFloat(FDouble, []), [TInt(ILongLong, [])], false); "__compcert_i64_utod", (TFloat(FDouble, []), [TInt(IULongLong, [])], false); "__compcert_i64_stof", (TFloat(FFloat, []), [TInt(ILongLong, [])], false); "__compcert_i64_utof", (TFloat(FFloat, []), [TInt(IULongLong, [])], false); "__compcert_i64_sdiv", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(ILongLong, [])], false); "__compcert_i64_udiv", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], false); "__compcert_i64_smod", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(ILongLong, [])], false); "__compcert_i64_umod", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], false); "__compcert_i64_shl", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(IInt, [])], false); "__compcert_i64_shr", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IInt, [])], false); "__compcert_i64_sar", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(IInt, [])], false); "__compcert_i64_smulh", (TInt(ILongLong, []), [TInt(ILongLong, []); TInt(ILongLong, [])], false); "__compcert_i64_umulh", (TInt(IULongLong, []), [TInt(IULongLong, []); TInt(IULongLong, [])], false); "__compcert_i32_sdiv", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); "__compcert_i32_udiv", (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); "__compcert_i32_smod", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); "__compcert_i32_umod", (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); "__compcert_f32_div", (TFloat(FFloat,[]), [TFloat(FFloat,[]); TFloat(FFloat,[])], false); "__compcert_f64_div", (TFloat(FDouble,[]), [TFloat(FDouble,[]); TFloat(FDouble,[])], 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) ] (** ** Functions used to handle 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, AST.ident) Hashtbl.t = Hashtbl.create 47 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 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()]; 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; (id, AST.Gvar { AST.gvar_info = typeStringLiteral s; AST.gvar_init = !init; AST.gvar_readonly = true; AST.gvar_volatile = false}) let name_for_wide_string_literal s = try Hashtbl.find wstringTable s with Not_found -> incr stringNum; let name = Printf.sprintf "__stringlit_%d" !stringNum in let id = intern_string name in let wchar_size = Machine.((!config).sizeof_wchar) 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()]; a_access = Sections.Access_default; a_inline = No_specifier; a_loc = Cutil.no_loc }; Hashtbl.add wstringTable s id; id let typeWideStringLiteral s = let sz = match Machine.((!config).sizeof_wchar) with | 2 -> I16 | 4 -> I32 | _ -> assert false in let sg = if Machine.((!config).wchar_signed) then Signed else Unsigned in Tarray(Tint(sz, sg, noattr), Z.of_uint (List.length s + 1), noattr) let global_for_wide_string s id = let init = ref [] in let init_of_char = match Machine.((!config).sizeof_wchar) 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; 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 (** ** 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 f = let id = intern_string f.fld_name and ty = convertTyp env ?bitwidth: f.fld_bitfield f.fld_typ in 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 t = match su with | C.Struct -> let layout = Cutil.struct_layout env attr members in List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout; TStruct (id,attr) | C.Union -> TUnion (id,attr) in Debug.set_composite_size id su (Cutil.sizeof env t); Composite(intern_string id.name, begin match su with C.Struct -> Ctypes.Struct | C.Union -> Ctypes.Union end, List.map (convertField env) members, 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 (** 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_expect"}}, args) -> (match args with | [e1; e2] -> ewrap (Ctyping.ebinop Cop.Oexpect (convertExpr env e1) (convertExpr env e2)) | _ -> error "__builtin_expect wants two arguments"; 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) -> let ty = typeWideStringLiteral s in Evar(name_for_wide_string_literal s, 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) (* Separate the cases of a switch statement body *) type switchlabel = | Case of C.exp | Default type switchbody = | Label of switchlabel | Stmt of C.stmt let rec flattenSwitch = function | {sdesc = C.Sseq(s1, s2)} -> flattenSwitch s1 @ flattenSwitch s2 | {sdesc = C.Slabeled(C.Scase(e, _), s1)} -> Label(Case e) :: flattenSwitch s1 | {sdesc = C.Slabeled(C.Sdefault, s1)} -> Label Default :: flattenSwitch s1 | {sdesc = C.Slabeled(C.Slabel lbl, s1); sloc = loc} -> Stmt {sdesc = C.Slabeled(C.Slabel lbl, Cutil.sskip); sloc = loc} :: flattenSwitch s1 | s -> [Stmt s] let rec groupSwitch = function | [] -> (Cutil.sskip, []) | Label case :: rem -> let (fst, cases) = groupSwitch rem in (Cutil.sskip, (case, fst) :: cases) | Stmt s :: rem -> let (fst, cases) = groupSwitch rem in (Cutil.sseq s.sloc s fst, cases) (* Test whether the statement contains case and give an *) let rec contains_case s = match s.sdesc with | C.Sskip | C.Sdo _ | C.Sbreak | C.Scontinue | C.Sswitch _ (* Stop at a switch *) | C.Sgoto _ | C.Sreturn _ | C.Sdecl _ | C.Sasm _ -> () | C.Sseq (s1,s2) | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 | C.Swhile (_,s1) | C.Sdowhile (s1,_) -> contains_case s1 | C.Sfor (s1,e,s2,s3) -> contains_case s1; contains_case s2; contains_case s3 | C.Slabeled(C.Scase _, _) -> unsupported "'case' statement not in 'switch' statement" | C.Slabeled(_,s) -> contains_case s | C.Sblock b -> List.iter contains_case b (** 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 (init, cases) = groupSwitch (flattenSwitch s1) in let rec init_debug s = match s.sdesc with | Sseq (a,b) -> init_debug a && init_debug b | C.Sskip -> true | _ -> Cutil.is_debug_stmt s in if init.sdesc <> C.Sskip && not (init_debug init) then begin warning Diagnostics.Unnamed "ignored code at beginning of 'switch'"; contains_case init end; let te = convertExpr env e in swrap (Ctyping.sswitch te (convertSwitch env (is_int64 env e.etyp) cases)) | 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 | [] -> LSnil | (lbl, s) :: rem -> updateLoc s.sloc; let lbl' = match lbl with | Default -> None | Case e -> match Ceval.integer_expr env e with | None -> unsupported "expression is not an integer constant expression"; None | Some v -> Some (if is_64 then Z.of_uint64 v else Z.of_uint32 (Int64.to_int32 v)) in LScons(lbl', convertStmt env s, convertSwitch env is_64 rem) (** 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_thread_local_extern || sto = Storage_static || sto = Storage_thread_local_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_" (* BEGIN CHECK *) let re_runtime64 = Str.regexp "__compcert_i64" let re_runtime32 = Str.regexp "__compcert_i32" let re_runtimef32 = Str.regexp "__compcert_f32" let re_runtimef64 = Str.regexp "__compcert_f64" (* END CHECK *) 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 (* BEGIN CHECK *) if Str.string_match re_runtime64 id.name 0 || Str.string_match re_runtime32 id.name 0 || Str.string_match re_runtimef64 id.name 0 || Str.string_match re_runtimef32 id.name 0 then AST.EF_runtime(id'', sg) else (* END CHECK *) 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 || sto = C.Storage_thread_local_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 (match sto with | Storage_thread_local | Storage_thread_local_extern | Storage_thread_local_static -> true | _ -> false) 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 && sto <> C.Storage_thread_local_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|Storage_thread_local_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 || sto = Storage_thread_local_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 (** 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 Diagnostics.check_errors (); p' with Env.Error msg -> fatal_error "%s" (Env.error_message msg)