diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 131 | ||||
| -rw-r--r-- | cfrontend/PrintClight.ml | 13 | ||||
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 18 |
3 files changed, 77 insertions, 85 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 0d24691f..f2fbf255 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -14,17 +14,10 @@ (* *********************************************************************) open C -open Env -open Builtins open Camlcoq -open AST -open Values -open !Ctypes -open !Cop -open !Csyntax -open !Initializers -open Floats +open Ctypes +open Csyntax (** ** Extracting information about global variables from their atom *) @@ -131,8 +124,8 @@ let string_of_errmsg msg = (** ** The builtin environment *) let builtins_generic = { - typedefs = []; - functions = [ + Builtins.typedefs = []; + Builtins.functions = [ (* Floating-point absolute value *) "__builtin_fabs", (TFloat(FDouble, []), [TFloat(FDouble, [])], false); @@ -264,8 +257,8 @@ let builtins_generic = { (* Add processor-dependent builtins *) let builtins = - { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; - functions = builtins_generic.functions @ CBuiltins.builtins.functions } + Builtins.({ typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; + functions = builtins_generic.Builtins.functions @ CBuiltins.builtins.functions }) (** ** The known attributes *) @@ -314,8 +307,8 @@ let global_for_string s id = 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, Gvar {gvar_info = typeStringLiteral s; gvar_init = !init; - gvar_readonly = true; gvar_volatile = false}) + (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 @@ -355,7 +348,7 @@ let global_for_wide_string s id = init := init_of_char(Z.of_uint64 c) :: !init in List.iter add_char s; add_char 0L; - (id, Gvar {gvar_info = typeWideStringLiteral s; gvar_init = List.rev !init; + AST.(id, Gvar { gvar_info = typeWideStringLiteral s; gvar_init = List.rev !init; gvar_readonly = true; gvar_volatile = false}) let globals_for_strings globs = @@ -373,8 +366,8 @@ let globals_for_strings globs = 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) + | Errors.OK(Values.Vint n) -> Some(Integers.Int.unsigned n) + | Errors.OK(Values.Vlong n) -> Some(Integers.Int64.unsigned n) | _ -> None let make_builtin_memcpy args = @@ -393,7 +386,7 @@ let make_builtin_memcpy args = 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(EF_memcpy(sz1, al1), + Ebuiltin( AST.EF_memcpy(sz1, al1), Tcons(typeconv(typeof dst), Tcons(typeconv(typeof src), Tnil)), Econs(dst, Econs(src, Enil)), Tvoid) @@ -410,7 +403,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 + 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), @@ -420,7 +413,7 @@ 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), Tcons(Ctyping.size_t, Tnil)), - Tpointer(Tvoid, noattr), cc_default) in + Tpointer(Tvoid, noattr), AST.cc_default) in let ty_ptr = Tpointer(ty, noattr) in let call = @@ -451,7 +444,7 @@ let make_builtin_va_arg env ty e = "__compcert_va_composite" ty e | _ -> unsupported "va_arg at this type"; - Eval(Vint(coqint_of_camlint 0l), type_int32s) + Eval(Values.Vint(coqint_of_camlint 0l), type_int32s) (** ** Translation functions *) @@ -472,13 +465,13 @@ let convertAttr a = let convertCallconv va unproto attr = let sr = Cutil.find_custom_attributes ["structreturn"; "__structreturn"] attr in - { cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } + { AST.cc_vararg = va; cc_unproto = unproto; cc_structret = sr <> [] } (** Types *) let convertIkind k a : coq_type = match k with - | C.IBool -> Tint (IBool, Unsigned, a) + | 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) @@ -544,7 +537,7 @@ let rec convertTyp env t = | C.TNamed _ -> convertTyp env (Cutil.unroll env t) | C.TStruct(id, a) -> - Tstruct(intern_string id.name, convertAttr a) + Ctypes.Tstruct(intern_string id.name, convertAttr a) | C.TUnion(id, a) -> Tunion(intern_string id.name, convertAttr a) | C.TEnum(id, a) -> @@ -577,7 +570,7 @@ let convertCompositedef env su id attr members = | 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 -> Struct | C.Union -> Union end, + begin match su with C.Struct -> Ctypes.Struct | C.Union -> Ctypes.Union end, List.map (convertField env) members, convertAttr attr) @@ -637,9 +630,9 @@ let convertFloat f kind = | Z.Z0 -> begin match kind with | FFloat -> - Ctyping.econst_single (Float.to_single Float.zero) + Ctyping.econst_single (Floats.Float.to_single Floats.Float.zero) | FDouble | FLongDouble -> - Ctyping.econst_float Float.zero + Ctyping.econst_float Floats.Float.zero end | Z.Zpos mant -> @@ -654,11 +647,11 @@ let convertFloat f kind = begin match kind with | FFloat -> - let f = Float32.from_parsed base mant exp in + let f = Floats.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 + let f = Floats.Float.from_parsed base mant exp in checkFloatOverflow f "double"; Ctyping.econst_float f end @@ -667,7 +660,7 @@ let convertFloat f kind = (** Expressions *) -let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s) +let ezero = Eval(Values.Vint(coqint_of_camlint 0l), type_int32s) let ewrap = function | Errors.OK e -> e @@ -705,13 +698,13 @@ let rec convertExpr env e = Ctyping.ealignof (convertTyp env ty1) | C.EUnop(C.Ominus, e1) -> - ewrap (Ctyping.eunop Oneg (convertExpr env 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 Onotbool (convertExpr env e1)) + ewrap (Ctyping.eunop Cop.Onotbool (convertExpr env e1)) | C.EUnop(C.Onot, e1) -> - ewrap (Ctyping.eunop Onotint (convertExpr env 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) -> @@ -805,7 +798,7 @@ let rec convertExpr env e = | [] -> assert false (* catched earlier *) in let targs2 = convertTypArgs env [] args2 in Ebuiltin( - EF_debug(P.of_int64 kind, intern_string text, + AST.EF_debug(P.of_int64 kind, intern_string text, typlist_of_typelist targs2), targs2, convertExprList env args2, convertTyp env e.etyp) @@ -814,7 +807,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), + AST.EF_annot(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"; @@ -826,7 +819,7 @@ let rec convertExpr env e = | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), + Ebuiltin(AST.EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> @@ -838,7 +831,7 @@ let rec convertExpr env e = make_builtin_memcpy (convertExprList env args) | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) -> - ewrap (Ctyping.eunop Oabsfloat (convertExpr env 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, @@ -854,7 +847,7 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_va_copy"}}, [arg1; arg2]) -> let dst = convertExpr env arg1 in let src = convertExpr env arg2 in - Ebuiltin(EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4), + 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)), @@ -866,8 +859,8 @@ let rec convertExpr env e = and tres = convertTyp env e.etyp in let sg = signature_of_type targs tres - {cc_vararg = true; cc_unproto = false; cc_structret = false} in - Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), + { AST.cc_vararg = true; 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) -> @@ -898,7 +891,7 @@ and convertLvalue env e = 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 Oadd e1' e2') in + let e3' = ewrap (Ctyping.ebinop Cop.Oadd e1' e2') in ewrap (Ctyping.ederef e3') | _ -> error "illegal lvalue"; ezero @@ -921,8 +914,8 @@ let convertAsm loc env txt outputs inputs clobber = let e = let tinputs = convertTypArgs env [] inputs' in let toutput = convertTyp env ty_res in - Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', - signature_of_type tinputs toutput cc_default, + Ebuiltin( AST.EF_inline_asm(coqstring_of_camlstring txt', + signature_of_type tinputs toutput AST.cc_default, clobber'), tinputs, convertExprList env inputs', @@ -1022,9 +1015,9 @@ let rec convertStmt env s = (convertStmt env s1) te (convertStmt env s2) (convertStmt env s3)) | C.Sbreak -> - Sbreak + Csyntax.Sbreak | C.Scontinue -> - Scontinue + Csyntax.Scontinue | C.Sswitch(e, s1) -> let (init, cases) = groupSwitch (flattenSwitch s1) in let rec init_debug s = @@ -1041,25 +1034,25 @@ let rec convertStmt env s = swrap (Ctyping.sswitch te (convertSwitch env (is_int64 env e.etyp) cases)) | C.Slabeled(C.Slabel lbl, s1) -> - Slabel(intern_string lbl, convertStmt env s1) + Csyntax.Slabel(intern_string lbl, convertStmt env s1) | C.Slabeled(C.Scase _, _) -> - unsupported "'case' statement not in 'switch' statement"; Sskip + unsupported "'case' statement not in 'switch' statement"; Csyntax.Sskip | C.Slabeled(C.Sdefault, _) -> - unsupported "'default' statement not in 'switch' statement"; Sskip + unsupported "'default' statement not in 'switch' statement"; Csyntax.Sskip | C.Sgoto lbl -> - Sgoto(intern_string lbl) + Csyntax.Sgoto(intern_string lbl) | C.Sreturn None -> - Sreturn None + Csyntax.Sreturn None | C.Sreturn(Some e) -> - Sreturn(Some(convertExpr env e)) + Csyntax.Sreturn(Some(convertExpr env e)) | C.Sblock _ -> - unsupported "nested blocks"; Sskip + unsupported "nested blocks"; Csyntax.Sskip | C.Sdecl _ -> - unsupported "inner declarations"; Sskip + 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])"; - Sdo (convertAsm s.sloc env txt outputs inputs clobber) + Csyntax.Sdo (convertAsm s.sloc env txt outputs inputs clobber) and convertSwitch env is_64 = function | [] -> @@ -1116,7 +1109,7 @@ let convertFundef loc env fd = a_access = Sections.Access_default; a_inline = fd.fd_inline && not fd.fd_vararg; (* PR#15 *) a_loc = loc }; - (id', Gfun(Ctypes.Internal + (id', AST.Gfun(Ctypes.Internal {fn_return = ret; fn_callconv = convertCallconv fd.fd_vararg false fd.fd_attrib; fn_params = params; @@ -1137,14 +1130,14 @@ let convertFundecl env (sto, id, ty, optinit) = 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_runtime id.name 0 then EF_runtime(id'', sg) else + if id.name = "malloc" then AST.EF_malloc else + if id.name = "free" then AST.EF_free else + if Str.string_match re_runtime id.name 0 then AST.EF_runtime(id'', sg) 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 - (id', Gfun(Ctypes.External(ef, args, res, cconv))) + && List.mem_assoc id.name builtins.Builtins.functions + then AST.EF_builtin(id'', sg) + else AST.EF_external(id'', sg) in + (id', AST.Gfun(Ctypes.External(ef, args, res, cconv))) (** Initializers *) @@ -1153,16 +1146,16 @@ let rec convertInit env init = | C.Init_single e -> Initializers.Init_single (convertExpr env e) | C.Init_array il -> - Initializers.Init_array (convertInitList env (List.rev il) Init_nil) + 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) Init_nil) + 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' (Init_cons(convertInit env i, accu)) + | i :: il' -> convertInitList env il' (Initializers.Init_cons(convertInit env i, accu)) let convertInitializer env ty i = match Initializers.transl_init @@ -1185,7 +1178,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = let init' = match optinit with | None -> - if sto = C.Storage_extern then [] else [Init_space sz] + if sto = C.Storage_extern then [] else [AST.Init_space sz] | Some i -> convertInitializer env ty i in let (section, access) = @@ -1204,7 +1197,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) = a_loc = loc }; let volatile = List.mem C.AVolatile attr in let readonly = List.mem C.AConst attr && not volatile in - (id', Gvar {gvar_info = ty'; gvar_init = init'; + (id', AST.Gvar { AST.gvar_info = ty'; gvar_init = init'; gvar_readonly = readonly; gvar_volatile = volatile}) (** Convert a list of global declarations. @@ -1269,7 +1262,7 @@ let rec translEnv env = function | C.Gtypedef(id, ty) -> Env.add_typedef env id ty | C.Genumdef(id, attr, members) -> - Env.add_enum env id {ei_members = members; ei_attr = attr} + Env.add_enum env id {Env.ei_members = members; ei_attr = attr} | _ -> env in translEnv env' gl diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 7fa35f16..ecfaf0df 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -17,16 +17,15 @@ open Format open Camlcoq -open AST open PrintAST -open !Ctypes +open Ctypes open Cop open PrintCsyntax -open !Clight +open Clight (* Naming temporaries *) -let temp_name (id: ident) = "$" ^ Z.to_string (Z.Zpos id) +let temp_name (id: AST.ident) = "$" ^ Z.to_string (Z.Zpos id) (* Declarator (identifier + type) -- reuse from PrintCsyntax *) @@ -254,7 +253,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | Ctypes.External((EF_external _ | EF_runtime _), args, res, cconv) -> + | Ctypes.External((AST.EF_external _ | AST.EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | Ctypes.External(_, _, _, _) -> @@ -264,8 +263,8 @@ let print_fundef p id fd = let print_globdef p (id, gd) = match gd with - | Gfun f -> print_fundef p id f - | Gvar v -> print_globvar p id v (* from PrintCsyntax *) + | AST.Gfun f -> print_fundef p id f + | AST.Gvar v -> print_globvar p id v (* from PrintCsyntax *) let print_program p prog = fprintf p "@[<v 0>"; diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index e3e259f7..6366906a 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -19,9 +19,9 @@ open Format open Camlcoq open Values open AST -open !Ctypes +open Ctypes open Cop -open !Csyntax +open Csyntax let name_unop = function | Onotbool -> "!" @@ -87,11 +87,11 @@ let rec name_cdecl id ty = match ty with | Tvoid -> "void" ^ name_optid id - | Tint(sz, sg, a) -> + | Ctypes.Tint(sz, sg, a) -> name_inttype sz sg ^ attributes a ^ name_optid id - | Tfloat(sz, a) -> + | Ctypes.Tfloat(sz, a) -> name_floattype sz ^ attributes a ^ name_optid id - | Tlong(sg, a) -> + | Ctypes.Tlong(sg, a) -> name_longtype sg ^ attributes a ^ name_optid id | Tpointer(t, a) -> let id' = @@ -182,7 +182,7 @@ let print_typed_value p v ty = fprintf p "%.15F" (camlfloat_of_coqfloat f) | Vsingle f, _ -> fprintf p "%.15Ff" (camlfloat_of_coqfloat32 f) - | Vlong n, Tlong(Unsigned, _) -> + | Vlong n, Ctypes.Tlong(Unsigned, _) -> fprintf p "%LuLLU" (camlint64_of_coqint n) | Vlong n, _ -> fprintf p "%LdLL" (camlint64_of_coqint n) @@ -498,7 +498,7 @@ let print_globvar p id v = fprintf p "@[<hov 2>%s = " (name_cdecl name2 v.gvar_info); begin match v.gvar_info, v.gvar_init with - | (Tint _ | Tlong _ | Tfloat _ | Tpointer _ | Tfunction _), + | (Ctypes.Tint _ | Ctypes.Tlong _ | Ctypes.Tfloat _ | Tpointer _ | Tfunction _), [i1] -> print_init p i1 | _, il -> @@ -543,8 +543,8 @@ let print_program p prog = fprintf p "@[<v 0>"; List.iter (declare_composite p) prog.prog_types; List.iter (define_composite p) prog.prog_types; - List.iter (print_globdecl p) prog.prog_defs; - List.iter (print_globdef p) prog.prog_defs; + List.iter (print_globdecl p) prog.Ctypes.prog_defs; + List.iter (print_globdef p) prog.Ctypes.prog_defs; fprintf p "@]@." let destination : string option ref = ref None |