diff options
Diffstat (limited to 'cfrontend')
| -rw-r--r-- | cfrontend/C2C.ml | 123 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 22 | ||||
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 10 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof.v | 10 | ||||
| -rw-r--r-- | cfrontend/SimplExpr.v | 2 | ||||
| -rw-r--r-- | cfrontend/SimplExprproof.v | 21 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 12 |
7 files changed, 119 insertions, 81 deletions
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/Cexec.v b/cfrontend/Cexec.v index c33068d9..80748df1 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -106,7 +106,10 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval := | Vfloat f, AST.Tfloat => Some (EVfloat f) | Vsingle f, AST.Tsingle => Some (EVsingle f) | Vlong n, AST.Tlong => Some (EVlong n) - | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs) + | Vptr b ofs, AST.Tint => + do id <- Genv.invert_symbol ge b; + check (Genv.public_symbol ge id); + Some (EVptr_global id ofs) | _, _ => None end. @@ -126,7 +129,10 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val := | EVfloat f, AST.Tfloat => Some (Vfloat f) | EVsingle f, AST.Tsingle => Some (Vsingle f) | EVlong n, AST.Tlong => Some (Vlong n) - | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs) + | EVptr_global id ofs, AST.Tint => + check (Genv.public_symbol ge id); + do b <- Genv.find_symbol ge id; + Some (Vptr b ofs) | _, _ => None end. @@ -134,15 +140,16 @@ Lemma eventval_of_val_sound: forall v t ev, eventval_of_val v t = Some ev -> eventval_match ge ev t v. Proof. intros. destruct v; destruct t; simpl in H; inv H; try constructor. - destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. - constructor. apply Genv.invert_find_symbol; auto. + destruct (Genv.invert_symbol ge b) as [id|] eqn:?; try discriminate. + destruct (Genv.public_symbol ge id) eqn:?; inv H1. + constructor. auto. apply Genv.invert_find_symbol; auto. Qed. Lemma eventval_of_val_complete: forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev. Proof. induction 1; simpl; auto. - rewrite (Genv.find_invert_symbol _ _ H). auto. + rewrite (Genv.find_invert_symbol _ _ H0). rewrite H. auto. Qed. Lemma list_eventval_of_val_sound: @@ -166,14 +173,15 @@ Lemma val_of_eventval_sound: forall ev t v, val_of_eventval ev t = Some v -> eventval_match ge ev t v. Proof. intros. destruct ev; destruct t; simpl in H; inv H; try constructor. + destruct (Genv.public_symbol ge i) eqn:?; try discriminate. destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1. - constructor. auto. + constructor; auto. Qed. Lemma val_of_eventval_complete: forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v. Proof. - induction 1; simpl; auto. rewrite H; auto. + induction 1; simpl; auto. rewrite H, H0; auto. Qed. (** Volatile memory accesses. *) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 7cb604ec..17c59b97 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -46,6 +46,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf_partial transl_fundef _ TRANSL). +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf_partial transl_fundef _ TRANSL). + Lemma function_ptr_translated: forall (b: block) (f: Csharpminor.fundef), Genv.find_funct_ptr ge b = Some f -> @@ -2026,7 +2030,7 @@ Proof. left; econstructor; split. apply plus_one. econstructor. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. eexact varinfo_preserved. + exact symbols_preserved. exact public_preserved. eexact varinfo_preserved. assert (MCS': match_callstack f' m' tm' (Frame cenv tfn e le te sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm')). @@ -2181,7 +2185,7 @@ Opaque PTree.set. left; econstructor; split. apply plus_one. econstructor. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. eexact varinfo_preserved. + exact symbols_preserved. exact public_preserved. eexact varinfo_preserved. econstructor; eauto. apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). eapply match_callstack_external_call; eauto. @@ -2246,7 +2250,7 @@ Theorem transl_program_correct: forward_simulation (Csharpminor.semantics prog) (Cminor.semantics tprog). Proof. eapply forward_simulation_star; eauto. - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step_correct. diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v index fdf5b06d..9cb112b0 100644 --- a/cfrontend/Cshmgenproof.v +++ b/cfrontend/Cshmgenproof.v @@ -743,6 +743,10 @@ Lemma symbols_preserved: forall s, Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL). +Lemma public_preserved: + forall s, Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL). + Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> @@ -1285,7 +1289,7 @@ Proof. apply plus_one. econstructor. eapply transl_arglist_correct; eauto. eapply external_call_symbols_preserved_2; eauto. - exact symbols_preserved. + exact symbols_preserved. exact public_preserved. eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). eapply match_states_skip; eauto. @@ -1466,7 +1470,7 @@ Proof. econstructor; split. apply plus_one. constructor. eauto. eapply external_call_symbols_preserved_2; eauto. - exact symbols_preserved. + exact symbols_preserved. exact public_preserved. eexact (Genv.find_var_info_transf_partial2 transl_fundef transl_globvar _ TRANSL). eexact (Genv.find_var_info_rev_transf_partial2 transl_fundef transl_globvar _ TRANSL). econstructor; eauto. @@ -1506,7 +1510,7 @@ Theorem transl_program_correct: forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog). Proof. eapply forward_simulation_plus. - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. eexact transl_step. 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..250f2b26 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -49,6 +49,13 @@ Proof. simpl. tauto. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros. eapply Genv.public_symbol_match. eapply transl_program_spec; eauto. + simpl. tauto. +Qed. + Lemma function_ptr_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> @@ -155,7 +162,7 @@ Proof. rewrite H1. split; auto. eapply deref_loc_value; eauto. (* By_value, volatile *) rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto. - exact symbols_preserved. exact block_is_volatile_preserved. + exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. (* By reference *) rewrite H0. destruct (type_is_volatile ty); split; auto; eapply deref_loc_reference; eauto. (* By copy *) @@ -175,7 +182,7 @@ Proof. rewrite H1. split; auto. eapply assign_loc_value; eauto. (* By_value, volatile *) rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto. - exact symbols_preserved. exact block_is_volatile_preserved. + exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. (* By copy *) rewrite H0. destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto. Qed. @@ -1861,7 +1868,7 @@ Proof. left. eapply plus_left. constructor. apply star_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. traceEq. econstructor; eauto. change sl2 with (nil ++ sl2). apply S. constructor. simpl; auto. auto. @@ -1872,7 +1879,7 @@ Proof. left. eapply plus_left. constructor. apply star_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. traceEq. econstructor; eauto. change sl2 with (nil ++ sl2). apply S. @@ -2161,7 +2168,7 @@ Proof. econstructor; split. left; apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. (* return *) @@ -2198,7 +2205,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. @@ -2215,7 +2222,7 @@ Theorem transl_program_correct: forward_simulation (Cstrategy.semantics prog) (Clight.semantics1 tprog). Proof. eapply forward_simulation_star_wf with (order := ltof _ measure). - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. apply well_founded_ltof. diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 67a7e626..15d0af06 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -48,6 +48,12 @@ Proof. exact (Genv.find_symbol_transf_partial _ _ TRANSF). Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + exact (Genv.public_symbol_transf_partial _ _ TRANSF). +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -2031,7 +2037,7 @@ Proof. intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto with compat. eapply match_envs_set_opttemp; eauto. eapply match_envs_extcall; eauto. @@ -2187,7 +2193,7 @@ Proof. intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]]. econstructor; split. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm). eapply match_cont_extcall; eauto. xomega. xomega. @@ -2242,7 +2248,7 @@ Theorem transf_program_correct: forward_simulation (semantics1 prog) (semantics2 tprog). Proof. eapply forward_simulation_plus. - eexact symbols_preserved. + eexact public_preserved. eexact initial_states_simulation. eexact final_states_simulation. eexact step_simulation. |