diff options
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 89 |
1 files changed, 45 insertions, 44 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd281374..a2db0915 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -141,8 +141,8 @@ let builtins_generic = { (* Block copy *) "__builtin_memcpy_aligned", (TVoid [], - [TPtr(TVoid [], []); - TPtr(TVoid [AConst], []); + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); TInt(IUInt, []); TInt(IUInt, [])], false); @@ -357,12 +357,12 @@ let make_builtin_memcpy args = let sz1 = match Initializers.constval !comp_env sz with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be + | _ -> error "ill-formed __builtin_memcpy_aligned (3rd argument must be a constant)"; Integers.Int.zero in let al1 = match Initializers.constval !comp_env al with | Errors.OK(Vint n) -> n - | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be + | _ -> error "ill-formed __builtin_memcpy_aligned (4th argument must be a constant)"; Integers.Int.one in (* to check: sz1 > 0, al1 divides sz1, al1 = 1|2|4|8 *) (* Issue #28: must decay array types to pointer types *) @@ -384,7 +384,7 @@ let va_list_ptr e = let make_builtin_va_arg_by_val helper ty ty_ret arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in - Ecast + Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), Econs(va_list_ptr arg, Enil), ty_ret), @@ -392,13 +392,13 @@ let make_builtin_va_arg_by_val helper ty ty_ret arg = let make_builtin_va_arg_by_ref helper ty arg = let ty_fun = - Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), Tpointer(Tvoid, noattr), 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(va_list_ptr arg, Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)), Tpointer(Tvoid, noattr)) in Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) @@ -406,13 +406,13 @@ let make_builtin_va_arg_by_ref helper ty arg = let make_builtin_va_arg env ty e = match ty with | Tint _ | Tpointer _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e | Tlong _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e | Tfloat _ -> - make_builtin_va_arg_by_val + make_builtin_va_arg_by_val "__compcert_va_float64" ty (Tfloat(F64, noattr)) e | Tstruct _ | Tunion _ -> make_builtin_va_arg_by_ref @@ -433,7 +433,7 @@ 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 = + attr_alignas = let n = Cutil.alignas_attribute a in if n > 0 then Some (N.of_int (log2 n)) else None } @@ -463,7 +463,7 @@ let convertFkind = function | C.FFloat -> F32 | C.FDouble -> F64 | C.FLongDouble -> - if not !Clflags.option_flongdouble then unsupported "'long double' type"; + if not !Clflags.option_flongdouble then unsupported "'long double' type"; F64 let rec convertTyp env t = @@ -524,11 +524,11 @@ let convertField env f = (intern_string f.fld_name, convertTyp env f.fld_typ) let convertCompositedef env su id attr members = - let t = match su with - | C.Struct -> + let t = match su with + | C.Struct -> let layout = Cutil.struct_layout env members in List.iter (fun (a,b) -> Debug.set_member_offset id a b) layout; - TStruct (id,attr) + TStruct (id,attr) | C.Union -> TUnion (id,attr) in Debug.set_composite_size id su (Cutil.sizeof env t); Composite(intern_string id.name, @@ -763,31 +763,31 @@ let rec convertExpr env e = 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 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(intern_string txt, typlist_of_typelist targs1), + EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot (first argument must be string literal)"; ezero - end - + 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(EF_annot_val(intern_string txt, typ_of_type targ), - Tcons(targ, Tnil), convertExprList env [arg], + Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), + Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> error "ill-formed __builtin_annot_intval (first argument must be string literal)"; ezero - end + end | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) -> make_builtin_memcpy (convertExprList env args) @@ -822,9 +822,9 @@ let rec convertExpr env e = let sg = signature_of_type targs tres {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(intern_string "printf", sg), + Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), targs, convertExprList env args, tres) - + | C.ECall(fn, args) -> if not (supported_return_type env e.etyp) then unsupported ("function returning a result of type " ^ string_of_type e.etyp ^ " (consider adding option -fstruct-return)"); @@ -867,17 +867,17 @@ and convertExprList env el = (* Extended assembly *) let convertAsm loc env txt outputs inputs clobber = - let (txt', output', inputs') = + let (txt', output', inputs') = ExtendedAsm.transf_asm loc env txt outputs inputs clobber in let clobber' = List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in let ty_res = match output' with None -> TVoid [] | Some e -> e.etyp in (* Build the Ebuiltin expression *) - let e = + let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(intern_string txt', + Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', signature_of_type tinputs toutput cc_default, clobber'), tinputs, @@ -894,7 +894,7 @@ type switchlabel = | Case of C.exp | Default -type switchbody = +type switchbody = | Label of switchlabel | Stmt of C.stmt @@ -922,16 +922,16 @@ let rec groupSwitch = function (Cutil.sseq s.sloc s fst, cases) (* Test whether the statement contains case and give an *) -let rec contains_case s = +let rec contains_case s = match s.sdesc with - | C.Sskip - | C.Sdo _ + | C.Sskip + | C.Sdo _ | C.Sbreak - | C.Scontinue + | C.Scontinue | C.Sswitch _ (* Stop at a switch *) - | C.Sgoto _ - | C.Sreturn _ - | C.Sdecl _ + | C.Sgoto _ + | C.Sreturn _ + | C.Sdecl _ | C.Sasm _ -> () | C.Sseq (s1,s2) | C.Sif(_,s1,s2) -> contains_case s1; contains_case s2 @@ -1021,7 +1021,7 @@ and convertSwitch env is_64 = function match lbl with | Default -> None - | Case e -> + | Case e -> match Ceval.integer_expr env e with | None -> unsupported "'case' label is not a compile-time integer"; None @@ -1060,7 +1060,7 @@ let convertFundef loc env fd = fd.fd_locals in let body' = convertStmt env fd.fd_body in let id' = intern_string fd.fd_name.name in - Debug.atom_function fd.fd_name id'; + Debug.atom_global fd.fd_name id'; Hashtbl.add decl_atom id' { a_storage = fd.fd_storage; a_alignment = None; @@ -1085,14 +1085,15 @@ let convertFundecl env (sto, id, ty, optinit) = | 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 EF_malloc else if id.name = "free" then EF_free else if Str.string_match re_builtin id.name 0 && List.mem_assoc id.name builtins.functions - then EF_builtin(id', sg) - else EF_external(id', sg) in + then EF_builtin(id'', sg) + else EF_external(id'', sg) in (id', Gfun(External(ef, args, res, cconv))) (** Initializers *) @@ -1126,8 +1127,8 @@ let convertInitializer env ty i = let convertGlobvar loc env (sto, id, ty, optinit) = let id' = intern_string id.name in - Debug.atom_global_variable id id'; - let ty' = convertTyp env ty 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 @@ -1189,7 +1190,7 @@ let rec convertGlobdecls env res gl = warning ("'#pragma " ^ s ^ "' directive ignored"); convertGlobdecls env res gl' -(** Convert struct and union declarations. +(** Convert struct and union declarations. Result is a list of CompCert C composite declarations. *) let rec convertCompositedefs env res gl = @@ -1228,7 +1229,7 @@ let rec translEnv env = function 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 *) @@ -1251,7 +1252,7 @@ let cleanupGlobals p = | _ -> () in List.iter classify_def p; - (* Second pass: keep "best" definition for each identifier *) + (* Second pass: keep "best" definition for each identifier *) let rec clean defs accu = function | [] -> accu | g :: gl -> |