diff options
| -rw-r--r-- | backend/CMparser.mly | 2 | ||||
| -rw-r--r-- | backend/Unusedglob.ml | 1 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 123 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 2 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 2 | ||||
| -rw-r--r-- | common/AST.v | 28 | ||||
| -rw-r--r-- | driver/Interp.ml | 3 |
7 files changed, 98 insertions, 63 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index ad92a12e..10cf8bf4 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -400,10 +400,12 @@ let mkmatch expr cases = prog: EQUAL STRINGLIT global_declarations EOF { { prog_defs = List.rev $3; + prog_public = List.map fst $3; (* FIXME *) prog_main = intern_string $2; } } | global_declarations EOF { { prog_defs = List.rev $1; + prog_public = List.map fst $1; (* FIXME *) prog_main = intern_string "main" } } ; diff --git a/backend/Unusedglob.ml b/backend/Unusedglob.ml index 1a88ee96..3834f8e6 100644 --- a/backend/Unusedglob.ml +++ b/backend/Unusedglob.ml @@ -81,6 +81,7 @@ let rec filter used = function let filter_prog used p = { prog_defs = filter used p.prog_defs; + prog_public = p.prog_public; prog_main = p.prog_main } (* Entry point *) diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 73d9edbd..4d5d6c07 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -28,6 +28,8 @@ open Csyntax open Initializers open Floats +(** ** Extracting information about global variables from their atom *) + (** Record useful information about global variables and functions, and associate it with the corresponding atoms. *) @@ -43,6 +45,61 @@ type atom_info = let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103 +let atom_is_static a = + try + let i = Hashtbl.find decl_atom a in + (* inline functions can remain in generated code, but should not + be global, unless explicitly marked "extern" *) + match i.a_storage with + | C.Storage_default -> i.a_inline + | C.Storage_extern -> false + | C.Storage_static -> true + | C.Storage_register -> false (* should not happen *) + with Not_found -> + false + +let atom_is_extern a = + try + (Hashtbl.find decl_atom a).a_storage = C.Storage_extern + with Not_found -> + false + +let atom_alignof a = + try + (Hashtbl.find decl_atom a).a_alignment + with Not_found -> + None + +let atom_sections a = + try + (Hashtbl.find decl_atom a).a_sections + with Not_found -> + [] + +let atom_is_small_data a ofs = + try + (Hashtbl.find decl_atom a).a_access = Sections.Access_near + 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_is_inline a = + try + (Hashtbl.find decl_atom a).a_inline + with Not_found -> + false + +let atom_location a = + try + (Hashtbl.find decl_atom a).a_loc + with Not_found -> + Cutil.no_loc + (** Hooks -- overriden in machine-dependent CPragmas module *) let process_pragma_hook = ref (fun (s: string) -> false) @@ -1059,6 +1116,13 @@ let cleanupGlobals p = 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 = @@ -1072,66 +1136,11 @@ let convertProgram p = let gl1 = convertGlobdecls (translEnv Env.empty p) [] (cleanupGlobals p) in let gl2 = globals_for_strings gl1 in let p' = { AST.prog_defs = gl2; - AST.prog_main = intern_string "main" } in + AST.prog_public = public_globals gl2; + AST.prog_main = intern_string "main" } in if !numErrors > 0 then None else Some p' 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 i = Hashtbl.find decl_atom a in - (* inline functions can remain in generated code, but should not - be global, unless explicitly marked "extern" *) - match i.a_storage with - | C.Storage_default -> i.a_inline - | C.Storage_extern -> false - | C.Storage_static -> true - | C.Storage_register -> false (* should not happen *) - with Not_found -> - false - -let atom_is_extern a = - try - (Hashtbl.find decl_atom a).a_storage = C.Storage_extern - with Not_found -> - false - -let atom_alignof a = - try - (Hashtbl.find decl_atom a).a_alignment - with Not_found -> - None - -let atom_sections a = - try - (Hashtbl.find decl_atom a).a_sections - with Not_found -> - [] - -let atom_is_small_data a ofs = - try - (Hashtbl.find decl_atom a).a_access = Sections.Access_near - 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_is_inline a = - try - (Hashtbl.find decl_atom a).a_inline - with Not_found -> - false - -let atom_location a = - try - (Hashtbl.find decl_atom a).a_loc - with Not_found -> - Cutil.no_loc diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index df33d727..089797f2 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -541,4 +541,4 @@ Fixpoint transl_globdefs Definition transl_program (p: Csyntax.program) : res program := do gl' <- transl_globdefs p.(prog_defs) (initial_generator tt); - OK (mkprogram gl' p.(prog_main)). + OK (mkprogram gl' p.(prog_public) p.(prog_main)). diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index 3802b957..f19c7de3 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -2198,7 +2198,7 @@ Proof. econstructor. exploit Genv.init_mem_match; eauto. simpl. fold tge. rewrite symbols_preserved. - destruct MP as [A B]. rewrite B; eexact H1. + destruct MP as (A & B & C). rewrite B; eexact H1. eexact FIND. rewrite <- H3. apply type_of_fundef_preserved. auto. constructor. auto. constructor. diff --git a/common/AST.v b/common/AST.v index 1c46389e..75286bd6 100644 --- a/common/AST.v +++ b/common/AST.v @@ -201,6 +201,8 @@ Record globvar (V: Type) : Type := mkglobvar { (** Whole programs consist of: - a collection of global definitions (name and description); +- a set of public names (the names that are visible outside + this compilation unit); - the name of the ``main'' function that serves as entry point in the program. A global definition is either a global function or a global variable. @@ -218,6 +220,7 @@ Implicit Arguments Gvar [F V]. Record program (F V: Type) : Type := mkprogram { prog_defs: list (ident * globdef F V); + prog_public: list ident; prog_main: ident }. @@ -244,6 +247,7 @@ Definition transform_program_globdef (idg: ident * globdef A V) : ident * globde Definition transform_program (p: program A V) : program B V := mkprogram (List.map transform_program_globdef p.(prog_defs)) + p.(prog_public) p.(prog_main). Lemma transform_program_function: @@ -295,7 +299,8 @@ Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * gl end. Definition transform_partial_program2 (p: program A V) : res (program B W) := - do gl' <- transf_globdefs p.(prog_defs); OK(mkprogram gl' p.(prog_main)). + do gl' <- transf_globdefs p.(prog_defs); + OK (mkprogram gl' p.(prog_public) p.(prog_main)). Lemma transform_partial_program2_function: forall p tp i tf, @@ -363,6 +368,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_program2_public: + forall p tp, + transform_partial_program2 p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + intros. monadInv H. reflexivity. +Qed. + (** Additionally, we can also "augment" the program with new global definitions and a different "main" function. *) @@ -373,7 +386,7 @@ Variable new_main: ident. Definition transform_partial_augment_program (p: program A V) : res (program B W) := do gl' <- transf_globdefs p.(prog_defs); - OK(mkprogram (gl' ++ new_globs) new_main). + OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main). Lemma transform_partial_augment_program_main: forall p tp, @@ -416,6 +429,14 @@ Proof. apply transform_partial_program2_main. Qed. +Lemma transform_partial_program_public: + forall p tp, + transform_partial_program p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + apply transform_partial_program2_public. +Qed. + Lemma transform_partial_program_function: forall p tp i tf, transform_partial_program p = OK tp -> @@ -480,7 +501,8 @@ Definition match_program (new_globs : list (ident * globdef B W)) (p1: program A V) (p2: program B W) : Prop := (exists tglob, list_forall2 match_globdef p1.(prog_defs) tglob /\ p2.(prog_defs) = tglob ++ new_globs) /\ - p2.(prog_main) = new_main. + p2.(prog_main) = new_main /\ + p2.(prog_public) = p1.(prog_public). End MATCH_PROGRAM. diff --git a/driver/Interp.ml b/driver/Interp.ml index e277ebe0..1291d70c 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -612,7 +612,8 @@ let change_main_function p old_main old_main_ty = fn_params = []; fn_vars = []; fn_body = body } in let new_main_id = intern_string "___main" in { prog_main = new_main_id; - prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs } + prog_defs = (new_main_id, Gfun(Internal new_main_fn)) :: p.prog_defs; + prog_public = p.prog_public } let rec find_main_function name = function | [] -> None |