diff options
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 922 |
1 files changed, 922 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml new file mode 100644 index 00000000..f62099a4 --- /dev/null +++ b/cfrontend/C2C.ml @@ -0,0 +1,922 @@ +open Printf + +open Cparser +open Cparser.C +open Cparser.Env +open Cparser.Builtins + +open Camlcoq +open AST +open Values +open Csyntax + +(** Record the declarations of global variables and associate them + with the corresponding atom. *) + +let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103 + +(** Hooks -- overriden in machine-dependent CPragmas module *) + +let process_pragma_hook = ref (fun (s: string) -> false) + +(** ** Error handling *) + +let currentLocation = ref Cutil.no_loc + +let updateLoc l = currentLocation := l + +let numErrors = ref 0 + +let error msg = + incr numErrors; + eprintf "%aError: %s\n" Cutil.printloc !currentLocation msg + +let unsupported msg = + incr numErrors; + eprintf "%aUnsupported feature: %s\n" Cutil.printloc !currentLocation msg + +let warning msg = + eprintf "%aWarning: %s\n" Cutil.printloc !currentLocation msg + + +(** ** The builtin environment *) + +let builtins_generic = { + typedefs = [ + (* keeps GCC-specific headers happy, harmless for others *) + "__builtin_va_list", C.TPtr(C.TVoid [], []) + ]; + functions = [ + (* Floating-point absolute value *) + "__builtin_fabs", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + (* The volatile read/volatile write functions *) + "__builtin_volatile_read_int8unsigned", + (TInt(IUChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int8signed", + (TInt(ISChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16unsigned", + (TInt(IUShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16signed", + (TInt(IShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int32", + (TInt(IInt, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float32", + (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float64", + (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_pointer", + (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_write_int8unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); + "__builtin_volatile_write_int8signed", + (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); + "__builtin_volatile_write_int16unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); + "__builtin_volatile_write_int16signed", + (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); + "__builtin_volatile_write_int32", + (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); + "__builtin_volatile_write_float32", + (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); + "__builtin_volatile_write_float64", + (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); + "__builtin_volatile_write_pointer", + (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false); + (* Block copy *) + "__builtin_memcpy", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false); + "__builtin_memcpy_words", + (TVoid [], + [TPtr(TVoid [], []); + TPtr(TVoid [AConst], []); + TInt(Cutil.size_t_ikind, [])], + false) + ] +} + +(* Add processor-dependent builtins *) + +let builtins = + { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; + functions = builtins_generic.functions @ CBuiltins.builtins.functions } + +(** ** Functions used to handle string literals *) + +let stringNum = ref 0 (* number of next global for string literals *) +let stringTable = Hashtbl.create 47 + +let name_for_string_literal env 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 + (env, (C.Storage_static, + Env.fresh_ident name, + C.TPtr(C.TInt(C.IChar,[C.AConst]),[]), + None)); + Sections.define_stringlit id; + Hashtbl.add stringTable s id; + id + +let typeStringLiteral s = + Tarray(Tint(I8, Unsigned), z_of_camlint(Int32.of_int(String.length s + 1))) + +let global_for_string s id = + let init = ref [] in + let add_char c = + init := + AST.Init_int8(coqint_of_camlint(Int32.of_int(Char.code c))) + :: !init in + add_char '\000'; + for i = String.length s - 1 downto 0 do add_char s.[i] done; + Datatypes.Coq_pair(id, + {gvar_info = typeStringLiteral s; gvar_init = !init; + gvar_readonly = true; gvar_volatile = false}) + +let globals_for_strings globs = + Hashtbl.fold + (fun s id l -> global_for_string s id :: l) + stringTable globs + +(** ** Handling of stubs for variadic functions *) + +let stub_function_table = Hashtbl.create 47 + +let register_stub_function name tres targs = + let rec letters_of_type = function + | Tnil -> [] + | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl + | Tcons(_, tl) -> "i" :: letters_of_type tl in + let stub_name = + name ^ "$" ^ String.concat "" (letters_of_type targs) in + try + (stub_name, Hashtbl.find stub_function_table stub_name) + with Not_found -> + let rec types_of_types = function + | Tnil -> Tnil + | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl) + | Tcons(_, tl) -> Tcons(Tpointer Tvoid, types_of_types tl) in + let stub_type = Tfunction (types_of_types targs, tres) in + Hashtbl.add stub_function_table stub_name stub_type; + (stub_name, stub_type) + +let declare_stub_function stub_name stub_type = + match stub_type with + | Tfunction(targs, tres) -> + Datatypes.Coq_pair(intern_string stub_name, + External({ ef_id = intern_string stub_name; + ef_sig = signature_of_type targs tres; + ef_inline = false }, + targs, tres)) + | _ -> assert false + +let declare_stub_functions k = + Hashtbl.fold (fun n i k -> declare_stub_function n i :: k) + stub_function_table k + +(** ** Translation functions *) + +(** Constants *) + +let convertInt n = coqint_of_camlint(Int64.to_int32 n) + +(** Types *) + +let convertIkind = function + | C.IBool -> unsupported "'_Bool' type"; (Unsigned, I8) + | C.IChar -> (Unsigned, I8) + | C.ISChar -> (Signed, I8) + | C.IUChar -> (Unsigned, I8) + | C.IInt -> (Signed, I32) + | C.IUInt -> (Unsigned, I32) + | C.IShort -> (Signed, I16) + | C.IUShort -> (Unsigned, I16) + | C.ILong -> (Signed, I32) + | C.IULong -> (Unsigned, I32) + | C.ILongLong -> + if not !Clflags.option_flonglong then unsupported "'long long' type"; + (Signed, I32) + | C.IULongLong -> + if not !Clflags.option_flonglong then unsupported "'unsigned long long' type"; + (Unsigned, I32) + +let convertFkind = function + | C.FFloat -> F32 + | C.FDouble -> F64 + | C.FLongDouble -> + if not !Clflags.option_flonglong then unsupported "'long double' type"; + F64 + +let convertTyp env t = + + let rec convertTyp seen t = + match Cutil.unroll env t with + | C.TVoid a -> Tvoid + | C.TInt(ik, a) -> + let (sg, sz) = convertIkind ik in Tint(sz, sg) + | C.TFloat(fk, a) -> + Tfloat(convertFkind fk) + | C.TPtr(C.TStruct(id, _), _) when List.mem id seen -> + Tcomp_ptr(intern_string ("struct " ^ id.name)) + | C.TPtr(C.TUnion(id, _), _) when List.mem id seen -> + Tcomp_ptr(intern_string ("union " ^ id.name)) + | C.TPtr(ty, a) -> + Tpointer(convertTyp seen ty) + | 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 seen ty, coqint_of_camlint 0l) + | C.TArray(ty, Some sz, a) -> + Tarray(convertTyp seen ty, convertInt sz) + | C.TFun(tres, targs, va, a) -> + if va then unsupported "variadic function type"; + if Cutil.is_composite_type env tres then + unsupported "return type is a struct or union"; + Tfunction(begin match targs with + | None -> warning "un-prototyped function type"; Tnil + | Some tl -> convertParams seen tl + end, + convertTyp seen tres) + | C.TNamed _ -> + assert false + | C.TStruct(id, a) -> + let flds = + try + convertFields (id :: seen) (Env.find_struct env id) + with Env.Error e -> + error (Env.error_message e); Fnil in + Tstruct(intern_string("struct " ^ id.name), flds) + | C.TUnion(id, a) -> + let flds = + try + convertFields (id :: seen) (Env.find_union env id) + with Env.Error e -> + error (Env.error_message e); Fnil in + Tunion(intern_string("union " ^ id.name), flds) + + and convertParams seen = function + | [] -> Tnil + | (id, ty) :: rem -> + if Cutil.is_composite_type env ty then + unsupported "function parameter of struct or union type"; + Tcons(convertTyp seen ty, convertParams seen rem) + + and convertFields seen ci = + convertFieldList seen ci.Env.ci_members + + and convertFieldList seen = function + | [] -> Fnil + | f :: fl -> + if f.fld_bitfield <> None then + unsupported "bit field in struct or union"; + Fcons(intern_string f.fld_name, convertTyp seen f.fld_typ, + convertFieldList seen fl) + + in convertTyp [] t + +let rec convertTypList env = function + | [] -> Tnil + | t1 :: tl -> Tcons(convertTyp env t1, convertTypList env tl) + +let rec projFunType env ty = + match Cutil.unroll env ty with + | TFun(res, args, vararg, attr) -> Some(res, vararg) + | TPtr(ty', attr) -> projFunType env ty' + | _ -> None + +(* Handling of volatile *) + +let is_volatile_access env e = + List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp) + && Cutil.is_lvalue env e + +let volatile_fun_suffix_type ty = + match ty with + | Tint(I8, Unsigned) -> ("int8unsigned", ty) + | Tint(I8, Signed) -> ("int8signed", ty) + | Tint(I16, Unsigned) -> ("int16unsigned", ty) + | Tint(I16, Signed) -> ("int16signed", ty) + | Tint(I32, _) -> ("int32", Tint(I32, Signed)) + | Tfloat F32 -> ("float32", ty) + | Tfloat F64 -> ("float64", ty) + | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ -> + ("pointer", Tpointer Tvoid) + | _ -> + unsupported "operation on volatile struct or union"; ("", Tvoid) + +let volatile_read_fun ty = + let (suffix, ty') = volatile_fun_suffix_type ty in + let funty = Tfunction(Tcons(Tpointer Tvoid, Tnil), ty') in + Evalof(Evar(intern_string ("__builtin_volatile_read_" ^ suffix), funty), funty) + +let volatile_write_fun ty = + let (suffix, ty') = volatile_fun_suffix_type ty in + let funty = Tfunction(Tcons(Tpointer Tvoid, Tcons(ty', Tnil)), Tvoid) in + Evalof(Evar(intern_string ("__builtin_volatile_write_" ^ suffix), funty), funty) + +(** Expressions *) + +let ezero = Eval(Vint(coqint_of_camlint 0l), Tint(I32, Signed)) + +let rec convertExpr env e = + let ty = convertTyp env e.etyp in + match e.edesc with + | C.EVar _ + | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _) + | C.EBinop(C.Oindex, _, _, _) -> + let l = convertLvalue env e in + if is_volatile_access env e then + Ecall(volatile_read_fun (typeof l), + Econs(Eaddrof(l, Tpointer(typeof l)), Enil), + ty) + else + Evalof(l, ty) + + | C.EConst(C.CInt(i, _, _)) -> + Eval(Vint(convertInt i), ty) + | C.EConst(C.CFloat(f, _, _)) -> + Eval(Vfloat(f), ty) + | C.EConst(C.CStr s) -> + let ty = typeStringLiteral s in + Evalof(Evar(name_for_string_literal env s, ty), ty) + | C.EConst(C.CWStr s) -> + unsupported "wide string literal"; ezero + | C.EConst(C.CEnum(id, i)) -> + Eval(Vint(convertInt i), ty) + | C.ESizeof ty1 -> + Esizeof(convertTyp env ty1, ty) + + | C.EUnop(C.Ominus, e1) -> + Eunop(Oneg, convertExpr env e1, ty) + | C.EUnop(C.Oplus, e1) -> + convertExpr env e1 + | C.EUnop(C.Olognot, e1) -> + Eunop(Onotbool, convertExpr env e1, ty) + | C.EUnop(C.Onot, e1) -> + Eunop(Onotint, convertExpr env e1, ty) + | C.EUnop(C.Oaddrof, e1) -> + Eaddrof(convertLvalue env e1, ty) + | C.EUnop(C.Opreincr, e1) -> + coq_Epreincr Incr (convertLvalue env e1) ty + | C.EUnop(C.Opredecr, e1) -> + coq_Epreincr Decr (convertLvalue env e1) ty + | C.EUnop(C.Opostincr, e1) -> + Epostincr(Incr, convertLvalue env e1, ty) + | C.EUnop(C.Opostdecr, e1) -> + Epostincr(Decr, convertLvalue env e1, ty) + + | 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, _) -> + let op' = + match op with + | C.Oadd -> Oadd + | C.Osub -> Osub + | C.Omul -> Omul + | C.Odiv -> Odiv + | C.Omod -> Omod + | C.Oand -> Oand + | C.Oor -> Oor + | C.Oxor -> Oxor + | C.Oshl -> Oshl + | C.Oshr -> Oshr + | C.Oeq -> Oeq + | C.One -> One + | C.Olt -> Olt + | C.Ogt -> Ogt + | C.Ole -> Ole + | C.Oge -> Oge + | _ -> assert false in + Ebinop(op', convertExpr env e1, convertExpr env e2, ty) + | 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 then + unsupported "assignment between structs or between unions"; + if is_volatile_access env e1 then + Ecall(volatile_write_fun (typeof e1'), + Econs(Eaddrof(e1', Tpointer(typeof e1')), Econs(e2', Enil)), + Tvoid) (* typing issue here *) + else + Eassign(e1', e2', ty) + | 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 tyres = convertTyp env tyres in + let op' = + match op with + | C.Oadd_assign -> Oadd + | C.Osub_assign -> Osub + | C.Omul_assign -> Omul + | C.Odiv_assign -> Odiv + | C.Omod_assign -> Omod + | C.Oand_assign -> Oand + | C.Oor_assign -> Oor + | C.Oxor_assign -> Oxor + | C.Oshl_assign -> Oshl + | C.Oshr_assign -> Oshr + | _ -> assert false in + let e1' = convertLvalue env e1 in + let e2' = convertExpr env e2 in + if is_volatile_access env e1 then + (error "assign-op to volatile not supported"; ezero) + else + Eassignop(op', e1', e2', tyres, ty) + | C.EBinop(C.Ocomma, e1, e2, _) -> + Ecomma(convertExpr env e1, convertExpr env e2, ty) + | C.EBinop(C.Ologand, e1, e2, _) -> + coq_Eseqand (convertExpr env e1) (convertExpr env e2) ty + | C.EBinop(C.Ologor, e1, e2, _) -> + coq_Eseqor (convertExpr env e1) (convertExpr env e2) ty + + | C.EConditional(e1, e2, e3) -> + Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3, ty) + | C.ECast(ty1, e1) -> + Ecast(convertExpr env e1, convertTyp env ty1) + | C.ECall(fn, args) -> + match projFunType env fn.etyp with + | None -> + error "wrong type for function part of a call"; ezero + | Some(res, false) -> + (* Non-variadic function *) + Ecall(convertExpr env fn, convertExprList env args, ty) + | Some(res, true) -> + (* Variadic function: generate a call to a stub function with + the appropriate number and types of arguments. Works only if + the function expression e is a global variable. *) + let fun_name = + match fn with + | {edesc = C.EVar id} when !Clflags.option_fvararg_calls -> + (*warning "emulating call to variadic function"; *) + id.name + | _ -> + unsupported "call to variadic function"; + "<error>" in + let targs = convertTypList env (List.map (fun e -> e.etyp) args) in + let tres = convertTyp env res in + let (stub_fun_name, stub_fun_typ) = + register_stub_function fun_name tres targs in + Ecall(Evalof(Evar(intern_string stub_fun_name, stub_fun_typ), + stub_fun_typ), + convertExprList env args, ty) + +and convertLvalue env e = + let ty = convertTyp env e.etyp in + match e.edesc with + | C.EVar id -> + Evar(intern_string id.name, ty) + | C.EUnop(C.Oderef, e1) -> + Ederef(convertExpr env e1, ty) + | C.EUnop(C.Odot id, e1) -> + Efield(convertLvalue env e1, intern_string id, ty) + | C.EUnop(C.Oarrow id, e1) -> + let e1' = convertExpr env e1 in + let ty1 = + match typeof e1' with + | Tpointer t -> t + | _ -> error ("wrong type for ->" ^ id ^ " access"); Tvoid in + Efield(Ederef(e1', ty1), intern_string id, ty) + | C.EBinop(C.Oindex, e1, e2, _) -> + coq_Eindex (convertExpr env e1) (convertExpr env e2) ty + | _ -> + error "illegal l-value"; ezero + +and convertExprList env el = + match el with + | [] -> Enil + | e1 :: el' -> Econs(convertExpr env e1, convertExprList env el') + +(* 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 + | 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) + +(* Statement *) + +let rec convertStmt env s = + updateLoc s.sloc; + match s.sdesc with + | C.Sskip -> + Sskip + | C.Sdo e -> + Sdo(convertExpr env e) + | C.Sseq(s1, s2) -> + Ssequence(convertStmt env s1, convertStmt env s2) + | C.Sif(e, s1, s2) -> + Sifthenelse(convertExpr env e, convertStmt env s1, convertStmt env s2) + | C.Swhile(e, s1) -> + Swhile(convertExpr env e, convertStmt env s1) + | C.Sdowhile(s1, e) -> + Sdowhile(convertExpr env e, convertStmt env s1) + | C.Sfor(s1, e, s2, s3) -> + Sfor(convertStmt env s1, convertExpr env e, convertStmt env s2, + convertStmt env s3) + | C.Sbreak -> + Sbreak + | C.Scontinue -> + Scontinue + | C.Sswitch(e, s1) -> + let (init, cases) = groupSwitch (flattenSwitch s1) in + if cases = [] then + unsupported "ill-formed 'switch' statement"; + if init.sdesc <> C.Sskip then + warning "ignored code at beginning of 'switch'"; + Sswitch(convertExpr env e, convertSwitch env cases) + | C.Slabeled(C.Slabel lbl, s1) -> + Slabel(intern_string lbl, convertStmt env s1) + | C.Slabeled(C.Scase _, _) -> + unsupported "'case' outside of 'switch'"; Sskip + | C.Slabeled(C.Sdefault, _) -> + unsupported "'default' outside of 'switch'"; Sskip + | C.Sgoto lbl -> + Sgoto(intern_string lbl) + | C.Sreturn None -> + Sreturn None + | C.Sreturn(Some e) -> + Sreturn(Some(convertExpr env e)) + | C.Sblock _ -> + unsupported "nested blocks"; Sskip + | C.Sdecl _ -> + unsupported "inner declarations"; Sskip + +and convertSwitch env = function + | [] -> + LSdefault Sskip + | [Default, s] -> + LSdefault (convertStmt env s) + | (Default, s) :: _ -> + updateLoc s.sloc; + unsupported "'default' case must occur last"; + LSdefault Sskip + | (Case e, s) :: rem -> + updateLoc s.sloc; + let v = + match Ceval.integer_expr env e with + | None -> unsupported "'case' label is not a compile-time integer"; 0L + | Some v -> v in + LScase(convertInt v, + convertStmt env s, + convertSwitch env rem) + +(** Function definitions *) + +let convertFundef env fd = + if Cutil.is_composite_type env fd.fd_ret then + unsupported "function returning a struct or union"; + let ret = + convertTyp env fd.fd_ret in + let params = + List.map + (fun (id, ty) -> + if Cutil.is_composite_type env ty then + unsupported "function parameter of struct or union type"; + Datatypes.Coq_pair(intern_string id.name, 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"; + Datatypes.Coq_pair(intern_string id.name, 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 decl = + (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in + Hashtbl.add decl_atom id' (env, decl); + Sections.define_function id'; + Datatypes.Coq_pair(id', + Internal {fn_return = ret; fn_params = params; + fn_vars = vars; fn_body = body'}) + +(** External function declaration *) + +let noninlined_builtin_functions = [ + "__builtin_memcpy"; + "__builtin_memcpy_words" +] + +let convertFundecl env (sto, id, ty, optinit) = + let (args, res) = + match convertTyp env ty with + | Tfunction(args, res) -> (args, res) + | _ -> assert false in + let id' = intern_string id.name in + let ef = + { ef_id = id'; + ef_sig = signature_of_type args res; + ef_inline = List.mem_assoc id.name builtins.functions + && not (List.mem id.name noninlined_builtin_functions) } in + Datatypes.Coq_pair(id', External(ef, args, res)) + +(** Initializers *) + +let init_data_of_string s = + let id = ref [] in + let enter_char c = + let n = coqint_of_camlint(Int32.of_int(Char.code c)) in + id := Init_int8 n :: !id in + enter_char '\000'; + for i = String.length s - 1 downto 0 do enter_char s.[i] done; + !id + +let convertInit env ty init = + + let k = ref [] + and pos = ref 0 in + let emit size datum = + k := datum :: !k; + pos := !pos + size in + let emit_space size = + emit size (Init_space (z_of_camlint (Int32.of_int size))) in + let align size = + let n = !pos land (size - 1) in + if n > 0 then emit_space (size - n) in + let check_align size = + assert (!pos land (size - 1) = 0) in + + let rec reduceInitExpr = function + | { edesc = C.EVar id; etyp = ty } -> + begin match Cutil.unroll env ty with + | C.TArray _ | C.TFun _ -> Some id + | _ -> None + end + | {edesc = C.EUnop(C.Oaddrof, {edesc = C.EVar id})} -> Some id + | {edesc = C.ECast(ty, e)} -> reduceInitExpr e + | _ -> None in + + let rec cvtInit ty = function + | Init_single e -> + begin match reduceInitExpr e with + | Some id -> + check_align 4; + emit 4 (Init_addrof(intern_string id.name, coqint_of_camlint 0l)) + | None -> + match Ceval.constant_expr env ty e with + | Some(C.CInt(v, ik, _)) -> + begin match convertIkind ik with + | (_, I8) -> + emit 1 (Init_int8(convertInt v)) + | (_, I16) -> + check_align 2; + emit 2 (Init_int16(convertInt v)) + | (_, I32) -> + check_align 4; + emit 4 (Init_int32(convertInt v)) + end + | Some(C.CFloat(v, fk, _)) -> + begin match convertFkind fk with + | F32 -> + check_align 4; + emit 4 (Init_float32 v) + | F64 -> + check_align 8; + emit 8 (Init_float64 v) + end + | Some(C.CStr s) -> + check_align 4; + let id = name_for_string_literal env s in + emit 4 (Init_addrof(id, coqint_of_camlint 0l)) + | Some(C.CWStr _) -> + unsupported "wide character strings" + | Some(C.CEnum _) -> + error "enum tag after constant folding" + | None -> + Format.printf "%a@." Cprint.exp (0, e); + error "initializer is not a compile-time constant" + end + | Init_array il -> + let ty_elt = + match Cutil.unroll env ty with + | C.TArray(t, _, _) -> t + | _ -> error "array type expected in initializer"; C.TVoid [] in + List.iter (cvtInit ty_elt) il + | Init_struct(_, flds) -> + cvtPadToSizeof ty (fun () -> List.iter cvtFieldInit flds) + | Init_union(_, fld, i) -> + cvtPadToSizeof ty (fun () -> cvtFieldInit (fld,i)) + + and cvtFieldInit (fld, i) = + let ty' = convertTyp env fld.fld_typ in + let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in + align al; + cvtInit fld.fld_typ i + + and cvtPadToSizeof ty fn = + let ty' = convertTyp env ty in + let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in + let pos0 = !pos in + fn(); + let pos1 = !pos in + assert (pos1 <= pos0 + sz); + if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1) + + in cvtInit ty init; List.rev !k + +(** Global variable *) + +let rec type_is_readonly env t = + let a = Cutil.attributes_of_type env t in + if List.mem C.AVolatile a then false else + if List.mem C.AConst a then true else + match Cutil.unroll env t with + | C.TArray(t', _, _) -> type_is_readonly env t' + | _ -> false + +let rec type_is_volatile env t = + let a = Cutil.attributes_of_type env t in + if List.mem C.AConst a then true else + match Cutil.unroll env t with + | C.TArray(t', _, _) -> type_is_volatile env t' + | _ -> false + +let convertGlobvar env (sto, id, ty, optinit as decl) = + let id' = intern_string id.name in + let ty' = convertTyp env ty in + let init' = + match optinit with + | None -> + if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')] + | Some i -> + convertInit env ty i in + Hashtbl.add decl_atom id' (env, decl); + Sections.define_variable id' + (match Cutil.sizeof env ty with Some sz -> sz | None -> max_int) + (type_is_readonly env ty); + Datatypes.Coq_pair(id', + {gvar_info = ty'; gvar_init = init'; + gvar_readonly = type_is_readonly env ty; + gvar_volatile = type_is_volatile env ty}) + +(** Convert a list of global declarations. + Result is a pair [(funs, vars)] where [funs] are + the function definitions (internal and external) + and [vars] the variable declarations. *) + +let rec convertGlobdecls env funs vars gl = + match gl with + | [] -> (List.rev funs, List.rev vars) + | g :: gl' -> + updateLoc g.gloc; + match g.gdesc with + | C.Gdecl((sto, id, ty, optinit) as d) -> + (* Prototyped functions become external declarations. + Variadic functions are skipped. + Other types become variable declarations. *) + begin match Cutil.unroll env ty with + | TFun(_, Some _, false, _) -> + convertGlobdecls env (convertFundecl env d :: funs) vars gl' + | TFun(_, None, false, _) -> + error "function declaration without prototype"; + convertGlobdecls env funs vars gl' + | TFun(_, _, true, _) -> + convertGlobdecls env funs vars gl' + | _ -> + convertGlobdecls env funs (convertGlobvar env d :: vars) gl' + end + | C.Gfundef fd -> + convertGlobdecls env (convertFundef env fd :: funs) vars gl' + | C.Gcompositedecl _ | C.Gcompositedef _ + | C.Gtypedef _ | C.Genumdef _ -> + (* typedefs are unrolled, structs are expanded inline, and + enum tags are folded. So we just skip their declarations. *) + convertGlobdecls env funs vars gl' + | C.Gpragma s -> + if not (!process_pragma_hook s) then + warning ("'#pragma " ^ s ^ "' directive ignored"); + convertGlobdecls env funs vars gl' + +(** Build environment of typedefs and structs *) + +let rec translEnv env = function + | [] -> env + | g :: gl -> + let env' = + match g.gdesc with + | C.Gcompositedecl(su, id) -> + Env.add_composite env id (Cutil.composite_info_decl env su) + | C.Gcompositedef(su, id, fld) -> + Env.add_composite env id (Cutil.composite_info_def env su fld) + | C.Gtypedef(id, ty) -> + Env.add_typedef env id ty + | _ -> + env in + translEnv env' gl + +(** Eliminate forward declarations of globals that are defined later. *) + +module IdentSet = Set.Make(struct type t = C.ident let compare = compare end) + +let cleanupGlobals p = + + let rec clean defs accu = function + | [] -> accu + | g :: gl -> + updateLoc g.gloc; + match g.gdesc with + | C.Gdecl(sto, id, ty, None) -> + if IdentSet.mem id defs + then clean defs accu gl + else clean (IdentSet.add id defs) (g :: accu) gl + | C.Gdecl(_, id, ty, _) -> + if IdentSet.mem id defs then + error ("multiple definitions of " ^ id.name); + clean (IdentSet.add id defs) (g :: accu) gl + | C.Gfundef fd -> + if IdentSet.mem fd.fd_name defs then + error ("multiple definitions of " ^ fd.fd_name.name); + clean (IdentSet.add fd.fd_name defs) (g :: accu) gl + | _ -> + clean defs (g :: accu) gl + + in clean IdentSet.empty [] (List.rev p) + +(** Convert a [C.program] into a [Csyntax.program] *) + +let convertProgram p = + numErrors := 0; + stringNum := 0; + Hashtbl.clear decl_atom; + Hashtbl.clear stringTable; + Hashtbl.clear stub_function_table; + let p = Builtins.declarations() @ p in + try + let (funs1, vars1) = + convertGlobdecls (translEnv Env.empty p) [] [] (cleanupGlobals p) in + let funs2 = declare_stub_functions funs1 in + let vars2 = globals_for_strings vars1 in + if !numErrors > 0 + then None + else Some { AST.prog_funct = funs2; + AST.prog_vars = vars2; + AST.prog_main = intern_string "main" } + with Env.Error msg -> + error (Env.error_message msg); None + +(** ** Extracting information about global variables from their atom *) + +let atom_is_static a = + try + let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in + sto = C.Storage_static + with Not_found -> + false + +let atom_is_readonly a = + try + let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in + type_is_readonly env ty + with Not_found -> + false + +let atom_sizeof a = + try + let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in + Cutil.sizeof env ty + with Not_found -> + None + +let atom_alignof a = + try + let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in + Cutil.alignof env ty + with Not_found -> + None + |