diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:22:27 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-03 10:22:27 +0000 |
commit | 891377ce1962cdb31357d6580d6546ec22df2b4f (patch) | |
tree | 4ff7c38749cc7a4c1af411c5aa3eb7225c4ae6a1 /cfrontend/C2Clight.ml | |
parent | 018edf2d81bf94197892cf1df221f7eeac1f96f6 (diff) | |
download | compcert-891377ce1962cdb31357d6580d6546ec22df2b4f.tar.gz compcert-891377ce1962cdb31357d6580d6546ec22df2b4f.zip |
Switching to the new C parser/elaborator/simplifier
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/C2Clight.ml')
-rw-r--r-- | cfrontend/C2Clight.ml | 741 |
1 files changed, 741 insertions, 0 deletions
diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml new file mode 100644 index 00000000..fcb0c7c1 --- /dev/null +++ b/cfrontend/C2Clight.ml @@ -0,0 +1,741 @@ +open Printf + +open Cparser +open Cparser.C +open Cparser.Env + +open Camlcoq +open AST +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) +let define_variable_hook = ref (fun (id: ident) (d: C.decl) -> ()) +let define_function_hook = ref (fun (id: ident) (d: C.decl) -> ()) +let define_stringlit_hook = ref (fun (id: ident) -> ()) + +(** ** 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 + + +(** ** 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)); + !define_stringlit_hook 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(Datatypes.Coq_pair(id, !init), typeStringLiteral s) + +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(intern_string stub_name, 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) -> + 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) + +(** Expressions *) + +let ezero = Expr(Econst_int(coqint_of_camlint 0l), Tint(I32, Signed)) + +let rec convertExpr env e = + let ty = convertTyp env e.etyp in + match e.edesc with + | C.EConst(C.CInt(i, _, _)) -> + Expr(Econst_int(convertInt i), ty) + | C.EConst(C.CFloat(f, _, _)) -> + Expr(Econst_float f, ty) + | C.EConst(C.CStr s) -> + Expr(Evar(name_for_string_literal env s), typeStringLiteral s) + | C.EConst(C.CWStr s) -> + unsupported "wide string literal"; ezero + | C.EConst(C.CEnum(id, i)) -> + Expr(Econst_int(convertInt i), ty) + + | C.ESizeof ty1 -> + Expr(Esizeof(convertTyp env ty1), ty) + | C.EVar id -> + Expr(Evar(intern_string id.name), ty) + + | C.EUnop(C.Oderef, e1) -> + Expr(Ederef(convertExpr env e1), ty) + | C.EUnop(C.Oaddrof, e1) -> + Expr(Eaddrof(convertExpr env e1), ty) + | C.EUnop(C.Odot id, e1) -> + Expr(Efield(convertExpr 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 + Expr(Efield(Expr(Ederef(convertExpr env e1), ty1), + intern_string id), ty) + | C.EUnop(C.Oplus, e1) -> + convertExpr env e1 + | C.EUnop(C.Ominus, e1) -> + Expr(Eunop(Oneg, convertExpr env e1), ty) + | C.EUnop(C.Olognot, e1) -> + Expr(Eunop(Onotbool, convertExpr env e1), ty) + | C.EUnop(C.Onot, e1) -> + Expr(Eunop(Onotint, convertExpr env e1), ty) + | C.EUnop(_, _) -> + unsupported "pre/post increment/decrement operator"; ezero + + | C.EBinop(C.Oindex, e1, e2, _) -> + Expr(Ederef(Expr(Ebinop(Oadd, convertExpr env e1, convertExpr env e2), + Tpointer ty)), ty) + | C.EBinop(C.Ologand, e1, e2, _) -> + Expr(Eandbool(convertExpr env e1, convertExpr env e2), ty) + | C.EBinop(C.Ologor, e1, e2, _) -> + Expr(Eorbool(convertExpr env e1, convertExpr env e2), ty) + | C.EBinop(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 + | C.Ocomma -> unsupported "sequence operator"; Oadd + | _ -> unsupported "assignment operator"; Oadd in + Expr(Ebinop(op', convertExpr env e1, convertExpr env e2), ty) + | C.EConditional(e1, e2, e3) -> + Expr(Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3), ty) + | C.ECast(ty1, e1) -> + Expr(Ecast(convertTyp env ty1, convertExpr env e1), ty) + | C.ECall _ -> + unsupported "function call within expression"; ezero + +(* Function calls *) + +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 + +let convertFuncall env lhs fn args = + let lhs' = + match lhs with None -> None | Some e -> Some(convertExpr env e) in + match projFunType env fn.etyp with + | None -> + error "wrong type for function part of a call"; Sskip + | Some(res, false) -> + (* Non-variadic function *) + Scall(lhs', convertExpr env fn, List.map (convertExpr env) args) + | 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"; + "" 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 + Scall(lhs', + Expr(Evar(intern_string stub_fun_name), stub_fun_typ), + List.map (convertExpr env) args) + +(* Toplevel expression, argument of an Sdo *) + +let convertTopExpr env e = + match e.edesc with + | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) -> + convertFuncall env (Some lhs) fn args + | C.EBinop(C.Oassign, lhs, rhs, _) -> + Sassign(convertExpr env lhs, convertExpr env rhs) + | C.ECall(fn, args) -> + convertFuncall env None fn args + | _ -> + unsupported "illegal toplevel expression"; Sskip + +(* 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 -> + convertTopExpr 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); + !define_function_hook id' decl; + Datatypes.Coq_pair(id', + Internal {fn_return = ret; fn_params = params; + fn_vars = vars; fn_body = body'}) + +(** External function declaration *) + +let convertFundecl env (sto, id, ty, optinit) = + match convertTyp env ty with + | Tfunction(args, res) -> + let id' = intern_string id.name in + Datatypes.Coq_pair(id', External(id', args, res)) + | _ -> + assert false + +(** 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 -> + 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 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); + !define_variable_hook id' decl; + Datatypes.Coq_pair(Datatypes.Coq_pair(id', init'), 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 + {ci_kind = su; ci_incomplete = true; ci_members = []} + | C.Gcompositedef(su, id, fld) -> + Env.add_composite env id + {ci_kind = su; ci_incomplete = false; ci_members = 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; + 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 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(ty, _, _) -> + let a' = Cutil.attributes_of_type env ty in + List.mem C.AConst a' && not (List.mem C.AVolatile a') + | _ -> + false + +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 |