diff options
| -rw-r--r-- | backend/Allocproof.v | 16 | ||||
| -rw-r--r-- | backend/CSEproof.v | 10 | ||||
| -rw-r--r-- | backend/CleanupLabelsproof.v | 15 | ||||
| -rw-r--r-- | backend/Constpropproof.v | 13 | ||||
| -rw-r--r-- | backend/Deadcodeproof.v | 28 | ||||
| -rw-r--r-- | backend/Inliningproof.v | 12 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 13 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 17 | ||||
| -rw-r--r-- | backend/Renumberproof.v | 11 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 18 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 16 | ||||
| -rw-r--r-- | backend/Tailcallproof.v | 10 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 13 | ||||
| -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/SimplExprproof.v | 19 | ||||
| -rw-r--r-- | cfrontend/SimplLocalsproof.v | 12 | ||||
| -rw-r--r-- | common/AST.v | 9 | ||||
| -rw-r--r-- | common/Events.v | 403 | ||||
| -rw-r--r-- | common/Globalenvs.v | 82 | ||||
| -rw-r--r-- | common/Smallstep.v | 28 | ||||
| -rw-r--r-- | driver/Interp.ml | 22 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 16 |
24 files changed, 562 insertions, 263 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 588a674e..2612ebf2 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1453,6 +1453,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intro. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -2016,7 +2024,7 @@ Proof. eapply star_trans. eexact A1. eapply star_left. econstructor. econstructor. unfold reglist. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. instantiate (1 := vl'); auto. instantiate (1 := ls2); auto. eapply star_right. eexact A3. @@ -2038,7 +2046,7 @@ Proof. eapply star_two. econstructor. eapply external_call_symbols_preserved' with (ge1 := ge). econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. constructor. eauto. eauto. traceEq. exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. eapply satisf_undef_reg with (r := res). @@ -2133,7 +2141,7 @@ Proof. apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved' with (ge1 := ge). econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. simpl. replace (map (Locmap.setlist (map R (loc_result (ef_sig ef))) @@ -2204,7 +2212,7 @@ Theorem transf_program_correct: Proof. set (ms := fun s s' => wt_state s /\ match_states s s'). eapply forward_simulation_plus with (match_states := ms). -- exact symbols_preserved. +- exact public_preserved. - intros. exploit initial_states_simulation; eauto. intros [st2 [A B]]. exists st2; split; auto. split; auto. apply wt_initial_state with (p := prog); auto. exact wt_prog. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index af138f83..ae8052be 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -818,6 +818,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf_partial (transf_fundef rm) prog TRANSF). +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf_partial (transf_fundef rm) prog TRANSF). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (Genv.find_var_info_transf_partial (transf_fundef rm) prog TRANSF). @@ -1104,7 +1108,7 @@ Proof. econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. * unfold transfer; rewrite H. @@ -1188,7 +1192,7 @@ Proof. econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. - (* return *) @@ -1227,7 +1231,7 @@ Theorem transf_program_correct: Proof. eapply forward_simulation_step with (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). -- eexact symbols_preserved. +- eexact public_preserved. - intros. exploit transf_initial_states; eauto. intros [s2 [A B]]. exists s2. split. auto. split. apply sound_initial; auto. auto. - intros. destruct H. eapply transf_final_states; eauto. diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v index 65ba61c9..f952f1ea 100644 --- a/backend/CleanupLabelsproof.v +++ b/backend/CleanupLabelsproof.v @@ -43,6 +43,13 @@ Proof. apply Genv.find_symbol_transf. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.public_symbol_transf. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -285,12 +292,12 @@ Proof. (* Lbuiltin *) left; econstructor; split. 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 coqlib. (* Lannot *) left; econstructor; split. 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 coqlib. (* Llabel *) case_eq (Labelset.mem lbl (labels_branched_to (fn_code f))); intros. @@ -329,7 +336,7 @@ Proof. (* external function *) left; econstructor; split. 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 coqlib. (* return *) inv H3. inv H1. left; econstructor; split. @@ -362,7 +369,7 @@ Theorem transf_program_correct: forward_simulation (Linear.semantics prog) (Linear.semantics tprog). Proof. eapply forward_simulation_opt. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b79c721e..98e6e577 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -54,6 +54,13 @@ Proof. apply Genv.find_symbol_transf. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.public_symbol_transf. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -510,7 +517,7 @@ Opaque builtin_strength_reduction. left; econstructor; econstructor; split. eapply exec_Ibuiltin. eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_succ; eauto. simpl; auto. apply set_reg_lessdef; auto. @@ -582,7 +589,7 @@ Opaque builtin_strength_reduction. simpl. left; econstructor; econstructor; split. eapply exec_function_external; 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 *) @@ -638,7 +645,7 @@ Proof. intros [ [n2 [s2' [A B]]] | [n2 [A [B C]]]]. exists n2; exists s2'; split; auto. left; apply plus_one; auto. exists n2; exists s2; split; auto. right; split; auto. subst t; apply star_refl. -- eexact symbols_preserved. +- eexact public_preserved. Qed. End PRESERVATION. diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 2fdedc63..4d09c5ba 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -381,6 +381,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intro. unfold ge, tge. + apply Genv.public_symbol_transf_partial with (transf_fundef rm). + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -792,7 +800,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. rewrite <- H4. constructor. eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -812,7 +820,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -825,7 +833,7 @@ Ltac UseTransfer := econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. + (* volatile global store *) @@ -838,7 +846,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. rewrite volatile_store_global_charact. exists b; split; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. + (* memcpy *) @@ -870,7 +878,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl. inv LD1. inv LD2. econstructor; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. + (* memcpy eliminated *) @@ -893,7 +901,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_list_match_lessdef; eauto 2 with na. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. + (* annot val *) @@ -902,7 +910,7 @@ Ltac UseTransfer := eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. simpl; constructor. eapply eventval_match_lessdef; eauto 2 with na. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. + (* all other builtins *) @@ -917,7 +925,7 @@ Ltac UseTransfer := econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved. eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 3 with na. eapply mextends_agree; eauto. @@ -969,7 +977,7 @@ Ltac UseTransfer := econstructor; split. 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. - (* return *) @@ -1009,7 +1017,7 @@ Proof. intros. apply forward_simulation_step with (match_states := fun s1 s2 => sound_state prog s1 /\ match_states s1 s2). -- exact symbols_preserved. +- exact public_preserved. - simpl; intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. exists st2; intuition. eapply sound_initial; eauto. - simpl; intros. destruct H. eapply transf_final_states; eauto. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 2564a736..9b1aec4c 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -43,6 +43,12 @@ Proof. intros. apply Genv.find_symbol_transf_partial with (transf_fundef fenv); auto. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros. apply Genv.public_symbol_transf_partial with (transf_fundef fenv); auto. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -1008,7 +1014,7 @@ Proof. left; econstructor; split. eapply plus_one. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor. eapply match_stacks_inside_set_reg. eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. @@ -1161,7 +1167,7 @@ Proof. left; econstructor; split. eapply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor. eapply match_stacks_bound with (Mem.nextblock m'0). eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. @@ -1250,7 +1256,7 @@ Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). Proof. eapply forward_simulation_star. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact step_simulation. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 3b22fc68..63fa6565 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -62,6 +62,11 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (Genv.find_symbol_transf_partial transf_fundef _ TRANSF). +Lemma public_preserved: + forall id, + Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof (Genv.public_symbol_transf_partial transf_fundef _ TRANSF). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (Genv.find_var_info_transf_partial transf_fundef _ TRANSF). @@ -640,14 +645,14 @@ Proof. left; econstructor; split. simpl. apply plus_one. eapply exec_Lbuiltin; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lannot *) left; econstructor; split. simpl. apply plus_one. eapply exec_Lannot; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lbranch *) @@ -705,7 +710,7 @@ Proof. monadInv H8. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* return *) @@ -741,7 +746,7 @@ Theorem transf_program_correct: forward_simulation (LTL.semantics prog) (Linear.semantics tprog). Proof. eapply forward_simulation_star. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact transf_step_correct. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 2aa5ab92..8acce510 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -361,6 +361,11 @@ Lemma symbols_preserved: 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: CminorSel.fundef), Genv.find_funct_ptr ge b = Some f -> @@ -687,7 +692,8 @@ Proof. (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Ibuiltin; eauto. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. reflexivity. (* Match-env *) split. eauto with rtlg. @@ -720,7 +726,8 @@ Proof. eapply star_left. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H. eauto. auto. eapply star_left. eapply exec_function_external. - eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. apply star_one. apply exec_return. reflexivity. reflexivity. reflexivity. (* Match-env *) @@ -1292,7 +1299,7 @@ Proof. left. eapply plus_right. eexact E. eapply exec_Ibuiltin. 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. constructor. eapply match_env_update_dest; eauto. @@ -1410,7 +1417,7 @@ Proof. econstructor; split. left; apply plus_one. eapply exec_function_external; 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 *) @@ -1448,7 +1455,7 @@ Theorem transf_program_correct: forward_simulation (CminorSel.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_star_wf with (order := lt_state). - eexact symbols_preserved. + eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. apply lt_state_wf. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index f18d3c2e..19c3b680 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -47,6 +47,11 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog). +Lemma public_preserved: + forall id, + Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof (@Genv.public_symbol_transf _ _ _ transf_fundef prog). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (@Genv.find_var_info_transf _ _ _ transf_fundef prog). @@ -194,7 +199,7 @@ Proof. econstructor; split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* cond *) econstructor; split. @@ -219,7 +224,7 @@ Proof. econstructor; split. eapply exec_function_external; 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 *) inv STACKS. inv H1. @@ -251,7 +256,7 @@ Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_step. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 658e6603..672853e3 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -56,6 +56,12 @@ Proof. intros. eapply Genv.find_symbol_transf_partial; eauto. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros. eapply Genv.public_symbol_transf_partial; eauto. +Qed. + Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> @@ -105,7 +111,7 @@ Proof. split. auto. split. auto. intros. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. Qed. Lemma builtin_implements_preserved: @@ -115,7 +121,7 @@ Lemma builtin_implements_preserved: Proof. unfold builtin_implements; intros. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. Qed. Lemma helpers_correct_preserved: @@ -795,7 +801,7 @@ Proof. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. 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. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* Seq *) @@ -872,14 +878,14 @@ Proof. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. - (* external call turned into a Sbuiltin *) exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. 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 *) inv MC. @@ -927,7 +933,7 @@ Proof. intros. unfold sel_program in H. destruct (get_helpers (Genv.globalenv prog)) as [hf|] eqn:E; simpl in H; try discriminate. apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). - eapply symbols_preserved; eauto. + eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. apply sel_step_correct; auto. eapply helpers_correct_preserved; eauto. apply get_helpers_correct. auto. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index c25721bc..e3e3a0d0 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -2242,6 +2242,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -2681,7 +2689,7 @@ Proof. 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 coqlib. inversion H; inversion A; subst. eapply match_stack_change_extcall; eauto. @@ -2705,7 +2713,7 @@ Proof. 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 coqlib. inv H; inv A. eapply match_stack_change_extcall; eauto. apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto. @@ -2813,7 +2821,7 @@ Proof. econstructor; split. apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply match_stacks_change_bounds with (Mem.nextblock m) (Mem.nextblock m'0). inv H0; inv A. eapply match_stack_change_extcall; eauto. apply Ple_refl. apply Ple_refl. @@ -2879,7 +2887,7 @@ Theorem transf_program_correct: Proof. set (ms := fun s s' => wt_state s /\ match_states s s'). eapply forward_simulation_plus with (match_states := ms). -- exact symbols_preserved. +- exact public_preserved. - intros. exploit transf_initial_states; eauto. intros [st2 [A B]]. exists st2; split; auto. split; auto. apply wt_initial_state with (prog := prog); auto. exact wt_prog. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index cc4ff55e..5ee7ccc1 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -241,6 +241,10 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_transf transf_fundef prog). +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof (Genv.public_symbol_transf transf_fundef prog). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (Genv.find_var_info_transf transf_fundef prog). @@ -506,7 +510,7 @@ Proof. left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'1); split. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. apply regset_set; auto. (* cond *) @@ -567,7 +571,7 @@ Proof. left. exists (Returnstate s' res' m2'); split. simpl. 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. (* returnstate *) @@ -616,7 +620,7 @@ Theorem transf_program_correct: forward_simulation (RTL.semantics prog) (RTL.semantics tprog). Proof. eapply forward_simulation_opt with (measure := measure); eauto. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact transf_step_correct. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index d02cb2e1..e6588938 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -160,6 +160,11 @@ Lemma symbols_preserved: Genv.find_symbol tge id = Genv.find_symbol ge id. Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef prog). +Lemma public_preserved: + forall id, + Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof (@Genv.public_symbol_transf _ _ _ tunnel_fundef prog). + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof (@Genv.find_var_info_transf _ _ _ tunnel_fundef prog). @@ -335,13 +340,13 @@ Proof. left; simpl; econstructor; split. eapply exec_Lbuiltin; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lannot *) left; simpl; econstructor; split. eapply exec_Lannot; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. (* Lbranch (preserved) *) @@ -373,7 +378,7 @@ Proof. left; simpl; econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. simpl. econstructor; eauto. (* return *) inv H3. inv H1. @@ -408,7 +413,7 @@ Theorem transf_program_correct: forward_simulation (LTL.semantics prog) (LTL.semantics tprog). Proof. eapply forward_simulation_opt. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact tunnel_step_correct. 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/SimplExprproof.v b/cfrontend/SimplExprproof.v index f19c7de3..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 *) @@ -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. diff --git a/common/AST.v b/common/AST.v index 75286bd6..9c29a374 100644 --- a/common/AST.v +++ b/common/AST.v @@ -657,6 +657,15 @@ Proof. Defined. Global Opaque external_function_eq. +(** Global variables referenced by an external function *) + +Definition globals_external (ef: external_function) : list ident := + match ef with + | EF_vload_global _ id _ => id :: nil + | EF_vstore_global _ id _ => id :: nil + | _ => nil + end. + (** Function definitions are the union of internal and external functions. *) Inductive fundef (F: Type): Type := diff --git a/common/Events.v b/common/Events.v index 8787a14b..175655be 100644 --- a/common/Events.v +++ b/common/Events.v @@ -276,6 +276,7 @@ Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_single: forall f, eventval_match (EVsingle f) Tsingle (Vsingle f) | ev_match_ptr: forall id b ofs, + Genv.public_symbol ge id = true -> Genv.find_symbol ge id = Some b -> eventval_match (EVptr_global id ofs) Tint (Vptr b ofs). @@ -318,45 +319,6 @@ Proof. inv H1. constructor. eapply eventval_match_lessdef; eauto. eauto. Qed. -(** Compatibility with memory injections *) - -Variable f: block -> option (block * Z). - -Definition meminj_preserves_globals : Prop := - (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0)) - /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0)) - /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> f b1 = Some(b2, delta) -> b2 = b1). - -Hypothesis glob_pres: meminj_preserves_globals. - -Lemma eventval_match_inject: - forall ev ty v1 v2, - eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2. -Proof. - intros. inv H; inv H0; try constructor; auto. - destruct glob_pres as [A [B C]]. - exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ. - rewrite Int.add_zero. econstructor; eauto. -Qed. - -Lemma eventval_match_inject_2: - forall ev ty v, - eventval_match ev ty v -> val_inject f v v. -Proof. - induction 1; auto. - destruct glob_pres as [A [B C]]. - exploit A; eauto. intro EQ. - econstructor; eauto. rewrite Int.add_zero; auto. -Qed. - -Lemma eventval_list_match_inject: - forall evl tyl vl1, eventval_list_match evl tyl vl1 -> - forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match evl tyl vl2. -Proof. - induction 1; intros. inv H; constructor. - inv H1. constructor. eapply eventval_match_inject; eauto. eauto. -Qed. - (** Determinism *) Lemma eventval_match_determ_1: @@ -388,7 +350,7 @@ Definition eventval_valid (ev: eventval) : Prop := | EVlong _ => True | EVfloat _ => True | EVsingle _ => True - | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b + | EVptr_global id ofs => Genv.public_symbol ge id = true end. Definition eventval_type (ev: eventval) : typ := @@ -407,19 +369,21 @@ Lemma eventval_match_receptive: exists v2, eventval_match ev2 ty v2. Proof. intros. inv H; destruct ev2; simpl in H2; try discriminate. - exists (Vint i0); constructor. - destruct H1 as [b EQ]. exists (Vptr b i1); constructor; auto. - exists (Vlong i0); constructor. - exists (Vfloat f1); constructor. - exists (Vsingle f1); constructor; auto. - exists (Vint i); constructor. - destruct H1 as [b' EQ]. exists (Vptr b' i0); constructor; auto. +- exists (Vint i0); constructor. +- simpl in H1; exploit Genv.public_symbol_exists; eauto. intros [b FS]. + exists (Vptr b i1); constructor; auto. +- exists (Vlong i0); constructor. +- exists (Vfloat f0); constructor. +- exists (Vsingle f0); constructor; auto. +- exists (Vint i); constructor. +- simpl in H1. exploit Genv.public_symbol_exists. eexact H1. intros [b' FS]. + exists (Vptr b' i0); constructor; auto. Qed. Lemma eventval_match_valid: forall ev ty v, eventval_match ev ty v -> eventval_valid ev. Proof. - destruct 1; simpl; auto. exists b; auto. + destruct 1; simpl; auto. Qed. Lemma eventval_match_same_type: @@ -439,6 +403,15 @@ Variables F1 V1 F2 V2: Type. Variable ge1: Genv.t F1 V1. Variable ge2: Genv.t F2 V2. +Hypothesis public_preserved: + forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id. + +Lemma eventval_valid_preserved: + forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev. +Proof. + intros. destruct ev; simpl in *; auto. rewrite <- H; auto. +Qed. + Hypothesis symbols_preserved: forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. @@ -446,7 +419,9 @@ Lemma eventval_match_preserved: forall ev ty v, eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v. Proof. - induction 1; constructor; auto. rewrite symbols_preserved; auto. + induction 1; constructor; auto. + rewrite public_preserved; auto. + rewrite symbols_preserved; auto. Qed. Lemma eventval_list_match_preserved: @@ -456,14 +431,68 @@ Proof. induction 1; constructor; auto. eapply eventval_match_preserved; eauto. Qed. -Lemma eventval_valid_preserved: - forall ev, eventval_valid ge1 ev -> eventval_valid ge2 ev. +End EVENTVAL_INV. + +(** Used for the semantics of volatile memory accesses. Move to [Globalenv] ? *) + +Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool := + match Genv.find_var_info ge b with + | None => false + | Some gv => gv.(gvar_volatile) + end. + +(** Compatibility with memory injections *) + +Section EVENTVAL_INJECT. + +Variables F1 V1 F2 V2: Type. +Variable f: block -> option (block * Z). +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. + +Definition symbols_inject : Prop := + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) +/\ (forall id b1 b2 delta, + f b1 = Some(b2, delta) -> Genv.find_symbol ge1 id = Some b1 -> + delta = 0 /\ Genv.find_symbol ge2 id = Some b2) +/\ (forall id b1, + Genv.public_symbol ge1 id = true -> Genv.find_symbol ge1 id = Some b1 -> + exists b2, f b1 = Some(b2, 0) /\ Genv.find_symbol ge2 id = Some b2) +/\ (forall b1 b2 delta, + f b1 = Some(b2, delta) -> + block_is_volatile ge2 b2 = block_is_volatile ge1 b1). + +Hypothesis symb_inj: symbols_inject. + +Lemma eventval_match_inject: + forall ev ty v1 v2, + eventval_match ge1 ev ty v1 -> val_inject f v1 v2 -> eventval_match ge2 ev ty v2. Proof. - unfold eventval_valid; destruct ev; auto. - intros [b A]. exists b; rewrite symbols_preserved; auto. + intros. inv H; inv H0; try constructor; auto. + destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ. + rewrite Int.add_zero. constructor; auto. rewrite A; auto. Qed. -End EVENTVAL_INV. +Lemma eventval_match_inject_2: + forall ev ty v1, + eventval_match ge1 ev ty v1 -> + exists v2, eventval_match ge2 ev ty v2 /\ val_inject f v1 v2. +Proof. + intros. inv H; try (econstructor; split; eauto; constructor; fail). + destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]]. + exists (Vptr b2 ofs); split. econstructor; eauto. + econstructor; eauto. rewrite Int.add_zero; auto. +Qed. + +Lemma eventval_list_match_inject: + forall evl tyl vl1, eventval_list_match ge1 evl tyl vl1 -> + forall vl2, val_list_inject f vl1 vl2 -> eventval_list_match ge2 evl tyl vl2. +Proof. + induction 1; intros. inv H; constructor. + inv H1. constructor. eapply eventval_match_inject; eauto. eauto. +Qed. + +End EVENTVAL_INJECT. (** * Matching traces. *) @@ -501,8 +530,8 @@ Variables F1 V1 F2 V2: Type. Variable ge1: Genv.t F1 V1. Variable ge2: Genv.t F2 V2. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id. +Hypothesis public_preserved: + forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id. Lemma match_traces_preserved: forall t1 t2, match_traces ge1 t1 t2 -> match_traces ge2 t1 t2. @@ -531,12 +560,6 @@ Fixpoint output_trace (t: trace) : Prop := (** * Semantics of volatile memory accesses *) -Definition block_is_volatile (F V: Type) (ge: Genv.t F V) (b: block) : bool := - match Genv.find_var_info ge b with - | None => false - | Some gv => gv.(gvar_volatile) - end. - Inductive volatile_load (F V: Type) (ge: Genv.t F V): memory_chunk -> mem -> block -> int -> trace -> val -> Prop := | volatile_load_vol: forall chunk m b ofs id ev v, @@ -600,7 +623,8 @@ Definition inject_separated (f f': meminj) (m1 m2: mem): Prop := ~Mem.valid_block m1 b1 /\ ~Mem.valid_block m2 b2. Record extcall_properties (sem: extcall_sem) - (sg: signature) : Prop := mk_extcall_properties { + (sg: signature) (free_globals: list ident) : Prop := + mk_extcall_properties { (** The return value of an external call must agree with its signature. *) ec_well_typed: @@ -612,6 +636,7 @@ Record extcall_properties (sem: extcall_sem) ec_symbols_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) vargs m1 t vres m2, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> sem F1 V1 ge1 vargs m1 t vres m2 -> sem F2 V2 ge2 vargs m1 t vres m2; @@ -653,13 +678,16 @@ Record extcall_properties (sem: extcall_sem) (** External calls must commute with memory injections, in the following sense. *) ec_mem_inject: - forall F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', - meminj_preserves_globals ge f -> - sem F V ge vargs m1 t vres m2 -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2 f m1' vargs', + symbols_inject f ge1 ge2 -> + (forall id b1, + In id free_globals -> Genv.find_symbol ge1 id = Some b1 -> + exists b2, f b1 = Some(b2, 0) /\ Genv.find_symbol ge2 id = Some b2) -> + sem F1 V1 ge1 vargs m1 t vres m2 -> Mem.inject f m1 m1' -> val_list_inject f vargs vargs' -> exists f', exists vres', exists m2', - sem F V ge vargs' m1' t vres' m2' + sem F2 V2 ge2 vargs' m1' t vres' m2' /\ val_inject f' vres vres' /\ Mem.inject f' m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 @@ -696,15 +724,16 @@ Inductive volatile_load_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): Lemma volatile_load_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m b ofs t v, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> volatile_load ge1 chunk m b ofs t v -> volatile_load ge2 chunk m b ofs t v. Proof. - intros. inv H1; constructor; auto. - rewrite H0; auto. + intros. inv H2; constructor; auto. + rewrite H1; auto. rewrite H; auto. eapply eventval_match_preserved; eauto. - rewrite H0; auto. + rewrite H1; auto. Qed. Lemma volatile_load_extends: @@ -718,35 +747,28 @@ Proof. exploit Mem.load_extends; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto. Qed. -Remark meminj_preserves_block_is_volatile: - forall F V (ge: Genv.t F V) f b1 b2 delta, - meminj_preserves_globals ge f -> - f b1 = Some (b2, delta) -> - block_is_volatile ge b2 = block_is_volatile ge b1. -Proof. - intros. destruct H as [A [B C]]. unfold block_is_volatile. - case_eq (Genv.find_var_info ge b1); intros. - exploit B; eauto. intro EQ; rewrite H0 in EQ; inv EQ. rewrite H; auto. - case_eq (Genv.find_var_info ge b2); intros. - exploit C; eauto. intro EQ. congruence. - auto. -Qed. - Lemma volatile_load_inject: - forall F V (ge: Genv.t F V) f chunk m b ofs t v b' ofs' m', - meminj_preserves_globals ge f -> - volatile_load ge chunk m b ofs t v -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) f chunk m b ofs t v b' ofs' m', + symbols_inject f ge1 ge2 -> + volatile_load ge1 chunk m b ofs t v -> val_inject f (Vptr b ofs) (Vptr b' ofs') -> Mem.inject f m m' -> - exists v', volatile_load ge chunk m' b' ofs' t v' /\ val_inject f v v'. -Proof. - intros. inv H0. - inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H8 in EQ; inv EQ. - rewrite Int.add_zero. exists (Val.load_result chunk v0); split. - constructor; auto. - apply val_load_result_inject. eapply eventval_match_inject_2; eauto. - exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros [v' [A B]]. exists v'; split; auto. - constructor; auto. rewrite <- H3. inv H1. eapply meminj_preserves_block_is_volatile; eauto. + exists v', volatile_load ge2 chunk m' b' ofs' t v' /\ val_inject f v v'. +Proof. + intros until m'; intros SI VL VI MI. generalize SI; intros (A & B & C & D). + inv VL. +- (* volatile load *) + inv VI. exploit B; eauto. intros [U V]. subst delta. + exploit eventval_match_inject_2; eauto. intros (v2 & X & Y). + rewrite Int.add_zero. exists (Val.load_result chunk v2); split. + constructor; auto. + erewrite D; eauto. + apply val_load_result_inject. auto. +- (* normal load *) + exploit Mem.loadv_inject; eauto. simpl; eauto. simpl; intros (v2 & X & Y). + exists v2; split; auto. + constructor; auto. + inv VI. erewrite D; eauto. Qed. Lemma volatile_load_receptive: @@ -763,14 +785,15 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). + (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) - inv H1. constructor. eapply volatile_load_preserved; eauto. + inv H2. constructor. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. (* max perms *) @@ -782,7 +805,7 @@ Proof. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. constructor; auto. (* mem injects *) - inv H0. inv H2. inv H7. inversion H5; subst. + inv H1. inv H3. inv H8. inversion H6; subst. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. constructor; auto. red; intros. congruence. @@ -825,14 +848,15 @@ Qed. Lemma volatile_load_global_ok: forall chunk id ofs, extcall_properties (volatile_load_global_sem chunk id ofs) - (mksignature nil (Some (type_of_chunk chunk)) cc_default). + (mksignature nil (Some (type_of_chunk chunk)) cc_default) + (id :: nil). Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H. inv H1. apply Val.load_result_type. eapply Mem.load_type; eauto. (* symbols *) - inv H1. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. + inv H2. econstructor. rewrite H; eauto. eapply volatile_load_preserved; eauto. (* valid blocks *) inv H; auto. (* max perm *) @@ -843,9 +867,10 @@ Proof. inv H. inv H1. exploit volatile_load_extends; eauto. intros [v' [A B]]. exists v'; exists m1'; intuition. econstructor; eauto. (* inject *) - inv H0. inv H2. - assert (val_inject f (Vptr b ofs) (Vptr b ofs)). - exploit (proj1 H); eauto. intros EQ. econstructor. eauto. rewrite Int.add_zero; auto. + inv H1. inv H3. + exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). + assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). + econstructor; eauto. rewrite Int.add_zero; auto. exploit volatile_load_inject; eauto. intros [v' [A B]]. exists f; exists v'; exists m1'; intuition. econstructor; eauto. red; intros; congruence. @@ -872,15 +897,16 @@ Inductive volatile_store_sem (chunk: memory_chunk) (F V: Type) (ge: Genv.t F V): Lemma volatile_store_preserved: forall F1 V1 (ge1: Genv.t F1 V1) F2 V2 (ge2: Genv.t F2 V2) chunk m1 b ofs v t m2, (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, block_is_volatile ge2 b = block_is_volatile ge1 b) -> volatile_store ge1 chunk m1 b ofs v t m2 -> volatile_store ge2 chunk m1 b ofs v t m2. Proof. - intros. inv H1; constructor; auto. - rewrite H0; auto. + intros. inv H2; constructor; auto. + rewrite H1; auto. rewrite H; auto. eapply eventval_match_preserved; eauto. - rewrite H0; auto. + rewrite H1; auto. Qed. Lemma volatile_store_readonly: @@ -922,38 +948,44 @@ Proof. Qed. Lemma volatile_store_inject: - forall F V (ge: Genv.t F V) f chunk m1 b ofs v t m2 m1' b' ofs' v', - meminj_preserves_globals ge f -> - volatile_store ge chunk m1 b ofs v t m2 -> + forall F1 V1 F2 V2 (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) f chunk m1 b ofs v t m2 m1' b' ofs' v', + symbols_inject f ge1 ge2 -> + volatile_store ge1 chunk m1 b ofs v t m2 -> val_inject f (Vptr b ofs) (Vptr b' ofs') -> val_inject f v v' -> Mem.inject f m1 m1' -> exists m2', - volatile_store ge chunk m1' b' ofs' v' t m2' + volatile_store ge2 chunk m1' b' ofs' v' t m2' /\ Mem.inject f m2 m2' /\ Mem.unchanged_on (loc_unmapped f) m1 m2 /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2'. Proof. - intros. inv H0. -- inv H1. exploit (proj1 H); eauto. intros EQ; rewrite H9 in EQ; inv EQ. - rewrite Int.add_zero. exists m1'. intuition. - constructor; auto. - eapply eventval_match_inject; eauto. apply val_load_result_inject; auto. -- assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. + intros until v'; intros SI VS AI VI MI. + generalize SI; intros (P & Q & R & S). + inv VS. +- (* volatile store *) + inv AI. exploit Q; eauto. intros [A B]. subst delta. + rewrite Int.add_zero. exists m1'; split. + constructor; auto. erewrite S; eauto. + eapply eventval_match_inject; eauto. apply val_load_result_inject. auto. + intuition auto with mem. +- (* normal store *) + inversion AI; subst. + assert (Mem.storev chunk m1 (Vptr b ofs) v = Some m2). simpl; auto. exploit Mem.storev_mapped_inject; eauto. intros [m2' [A B]]. - inv H1. exists m2'; intuition. -+ constructor; auto. rewrite <- H4. eapply meminj_preserves_block_is_volatile; eauto. + exists m2'; intuition auto. ++ constructor; auto. erewrite S; eauto. + eapply Mem.store_unchanged_on; eauto. - unfold loc_unmapped; intros. congruence. + unfold loc_unmapped; intros. inv AI; congruence. + eapply Mem.store_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. simpl in A. assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta) by (eapply Mem.address_inject; eauto with mem). rewrite EQ in *. - eelim H6; eauto. - exploit Mem.store_valid_access_3. eexact H5. intros [P Q]. + eelim H3; eauto. + exploit Mem.store_valid_access_3. eexact H0. intros [X Y]. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply P. omega. + apply X. omega. Qed. Lemma volatile_store_receptive: @@ -966,13 +998,14 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) - inv H1. constructor. eapply volatile_store_preserved; eauto. + inv H2. constructor. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H1. auto. eauto with mem. (* perms *) @@ -984,7 +1017,7 @@ Proof. exploit volatile_store_extends; eauto. intros [m2' [A [B C]]]. exists Vundef; exists m2'; intuition. constructor; auto. (* mem inject *) - inv H0. inv H2. inv H7. inv H8. inversion H5; subst. + inv H1. inv H3. inv H8. inv H9. inversion H6; subst. exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. (* trace length *) @@ -1021,13 +1054,14 @@ Qed. Lemma volatile_store_global_ok: forall chunk id ofs, extcall_properties (volatile_store_global_sem chunk id ofs) - (mksignature (type_of_chunk chunk :: nil) None cc_default). + (mksignature (type_of_chunk chunk :: nil) None cc_default) + (id :: nil). Proof. intros; constructor; intros. (* well typed *) unfold proj_sig_res; simpl. inv H; constructor. (* symbols preserved *) - inv H1. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. + inv H2. econstructor. rewrite H; eauto. eapply volatile_store_preserved; eauto. (* valid block *) inv H. inv H2. auto. eauto with mem. (* perms *) @@ -1040,13 +1074,13 @@ Proof. intros [vres' [m2' [A [B [C D]]]]]. exists vres'; exists m2'; intuition. rewrite volatile_store_global_charact. exists b; auto. (* mem inject *) - rewrite volatile_store_global_charact in H0. destruct H0 as [b [P Q]]. - exploit (proj1 H). eauto. intros EQ. - assert (val_inject f (Vptr b ofs) (Vptr b ofs)). econstructor; eauto. rewrite Int.add_zero; auto. - exploit ec_mem_inject. eapply volatile_store_ok. eauto. eexact Q. eauto. eauto. + rewrite volatile_store_global_charact in H1. destruct H1 as [b [P Q]]. + exploit H0; eauto with coqlib. intros (b2 & INJ & FS2). + assert (val_inject f (Vptr b ofs) (Vptr b2 ofs)). econstructor; eauto. rewrite Int.add_zero; auto. + exploit ec_mem_inject. eapply volatile_store_ok. eauto. intuition. eexact Q. eauto. constructor. eauto. eauto. intros [f' [vres' [m2' [A [B [C [D [E G]]]]]]]]. exists f'; exists vres'; exists m2'; intuition. - rewrite volatile_store_global_charact. exists b; auto. + rewrite volatile_store_global_charact. exists b2; auto. (* trace length *) inv H. inv H1; simpl; omega. (* receptive *) @@ -1069,7 +1103,8 @@ Inductive extcall_malloc_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint) cc_default). + (mksignature (Tint :: nil) (Some Tint) cc_default) + nil. Proof. assert (UNCHANGED: forall (P: block -> Z -> Prop) m n m' b m'', @@ -1089,7 +1124,7 @@ Proof. (* well typed *) inv H. unfold proj_sig_res; simpl. auto. (* symbols preserved *) - inv H1; econstructor; eauto. + inv H2; econstructor; eauto. (* valid block *) inv H. eauto with mem. (* perms *) @@ -1109,7 +1144,7 @@ Proof. econstructor; eauto. eapply UNCHANGED; eauto. (* mem injects *) - inv H0. inv H2. inv H6. inv H8. + inv H1. inv H3. inv H7. inv H9. exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. @@ -1121,8 +1156,8 @@ Proof. eapply UNCHANGED; eauto. eapply UNCHANGED; eauto. red; intros. destruct (eq_block b1 b). - subst b1. rewrite C in H2. inv H2. eauto with mem. - rewrite D in H2. congruence. auto. + subst b1. rewrite C in H3. inv H3. eauto with mem. + rewrite D in H3 by auto. congruence. (* trace length *) inv H; simpl; omega. (* receptive *) @@ -1144,13 +1179,14 @@ Inductive extcall_free_sem (F V: Type) (ge: Genv.t F V): Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None cc_default). + (mksignature (Tint :: nil) None cc_default) + nil. Proof. constructor; intros. (* well typed *) inv H. unfold proj_sig_res. simpl. auto. (* symbols preserved *) - inv H1; econstructor; eauto. + inv H2; econstructor; eauto. (* valid block *) inv H. eauto with mem. (* perms *) @@ -1173,13 +1209,13 @@ Proof. eapply Mem.free_range_perm. eexact H4. eauto. } tauto. (* mem inject *) - inv H0. inv H2. inv H7. inv H9. + inv H1. inv H3. inv H8. inv H10. exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable). eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. instantiate (1 := lo). omega. + apply H1. instantiate (1 := lo). omega. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. @@ -1191,9 +1227,9 @@ Proof. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. - intros. red; intros. eelim H7; eauto. + intros. red; intros. eelim H8; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. omega. + apply H1. omega. split. auto. red; intros. congruence. (* trace length *) @@ -1221,13 +1257,15 @@ Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val - Lemma extcall_memcpy_ok: forall sz al, - extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None cc_default). + extcall_properties (extcall_memcpy_sem sz al) + (mksignature (Tint :: Tint :: nil) None cc_default) + nil. Proof. intros. constructor. - (* return type *) intros. inv H. constructor. - (* change of globalenv *) - intros. inv H1. econstructor; eauto. + intros. inv H2. econstructor; eauto. - (* valid blocks *) intros. inv H. eauto with mem. - (* perms *) @@ -1253,7 +1291,7 @@ Proof. erewrite list_forall2_length; eauto. tauto. - (* injections *) - intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. + intros. inv H1. inv H3. inv H15. inv H16. inv H12. inv H13. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). @@ -1304,7 +1342,7 @@ Proof. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. congruence. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. - eelim H2; eauto. + eelim H3; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. eapply Mem.storebytes_range_perm; eauto. erewrite list_forall2_length; eauto. @@ -1340,13 +1378,15 @@ Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (g Lemma extcall_annot_ok: forall text targs, - extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None cc_default). + extcall_properties (extcall_annot_sem text targs) + (mksignature (annot_args_typ targs) None cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) inv H. simpl. auto. (* symbols *) - inv H1. econstructor; eauto. + inv H2. econstructor; eauto. eapply eventval_list_match_preserved; eauto. (* valid blocks *) inv H; auto. @@ -1360,7 +1400,7 @@ Proof. econstructor; eauto. eapply eventval_list_match_lessdef; eauto. (* mem injects *) - inv H0. + inv H1. exists f; exists Vundef; exists m1'; intuition. econstructor; eauto. eapply eventval_list_match_inject; eauto. @@ -1384,13 +1424,15 @@ Inductive extcall_annot_val_sem (text: ident) (targ: typ) (F V: Type) (ge: Genv. Lemma extcall_annot_val_ok: forall text targ, - extcall_properties (extcall_annot_val_sem text targ) (mksignature (targ :: nil) (Some targ) cc_default). + extcall_properties (extcall_annot_val_sem text targ) + (mksignature (targ :: nil) (Some targ) cc_default) + nil. Proof. intros; constructor; intros. (* well typed *) inv H. unfold proj_sig_res; simpl. eapply eventval_match_type; eauto. (* symbols *) - inv H1. econstructor; eauto. + inv H2. econstructor; eauto. eapply eventval_match_preserved; eauto. (* valid blocks *) inv H; auto. @@ -1404,7 +1446,7 @@ Proof. econstructor; eauto. eapply eventval_match_lessdef; eauto. (* mem inject *) - inv H0. inv H2. inv H7. + inv H1. inv H3. inv H8. exists f; exists v'; exists m1'; intuition. econstructor; eauto. eapply eventval_match_inject; eauto. @@ -1429,14 +1471,14 @@ Qed. Parameter external_functions_sem: ident -> signature -> extcall_sem. Axiom external_functions_properties: - forall id sg, extcall_properties (external_functions_sem id sg) sg. + forall id sg, extcall_properties (external_functions_sem id sg) sg nil. (** We treat inline assembly similarly. *) Parameter inline_assembly_sem: ident -> extcall_sem. Axiom inline_assembly_properties: - forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default). + forall id, extcall_properties (inline_assembly_sem id) (mksignature nil None cc_default) nil. (** ** Combined semantics of external calls *) @@ -1469,9 +1511,9 @@ Definition external_call (ef: external_function): extcall_sem := Theorem external_call_spec: forall ef, - extcall_properties (external_call ef) (ef_sig ef). + extcall_properties (external_call ef) (ef_sig ef) (globals_external ef). Proof. - intros. unfold external_call, ef_sig. destruct ef. + intros. unfold external_call, ef_sig, globals_external; destruct ef. apply external_functions_properties. apply external_functions_properties. apply volatile_load_ok. @@ -1492,7 +1534,7 @@ Definition external_call_valid_block ef := ec_valid_block (external_call_spec ef Definition external_call_max_perm ef := ec_max_perm (external_call_spec ef). Definition external_call_readonly ef := ec_readonly (external_call_spec ef). Definition external_call_mem_extends ef := ec_mem_extends (external_call_spec ef). -Definition external_call_mem_inject ef := ec_mem_inject (external_call_spec ef). +Definition external_call_mem_inject_gen ef := ec_mem_inject (external_call_spec ef). Definition external_call_trace_length ef := ec_trace_length (external_call_spec ef). Definition external_call_receptive ef := ec_receptive (external_call_spec ef). Definition external_call_determ ef := ec_determ (external_call_spec ef). @@ -1503,11 +1545,12 @@ Lemma external_call_symbols_preserved: forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, external_call ef ge1 vargs m1 t vres m2 -> (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> external_call ef ge2 vargs m1 t vres m2. Proof. intros. eapply external_call_symbols_preserved_gen; eauto. - intros. unfold block_is_volatile. rewrite H1. auto. + intros. unfold block_is_volatile. rewrite H2. auto. Qed. Require Import Errors. @@ -1517,6 +1560,7 @@ Lemma external_call_symbols_preserved_2: (ge1: Genv.t F1 V1) (ge2: Genv.t F2 V2) vargs m1 t vres m2, external_call ef ge1 vargs m1 t vres m2 -> (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b gv1, Genv.find_var_info ge1 b = Some gv1 -> exists gv2, Genv.find_var_info ge2 b = Some gv2 /\ transf_globvar tvar gv1 = OK gv2) -> (forall b gv2, Genv.find_var_info ge2 b = Some gv2 -> @@ -1526,9 +1570,9 @@ Proof. intros. eapply external_call_symbols_preserved_gen; eauto. intros. unfold block_is_volatile. case_eq (Genv.find_var_info ge1 b); intros. - exploit H1; eauto. intros [g2 [A B]]. rewrite A. monadInv B. destruct g; auto. + exploit H2; eauto. intros [g2 [A B]]. rewrite A. monadInv B. destruct g; auto. case_eq (Genv.find_var_info ge2 b); intros. - exploit H2; eauto. intros [g1 [A B]]. congruence. + exploit H3; eauto. intros [g1 [A B]]. congruence. auto. Qed. @@ -1545,6 +1589,40 @@ Proof. unfold Plt, Ple in *; zify; omega. Qed. +(** Special case of [external_call_mem_inject_gen] (for backward compatibility) *) + +Definition meminj_preserves_globals (F V: Type) (ge: Genv.t F V) (f: block -> option (block * Z)) : Prop := + (forall id b, Genv.find_symbol ge id = Some b -> f b = Some(b, 0)) + /\ (forall b gv, Genv.find_var_info ge b = Some gv -> f b = Some(b, 0)) + /\ (forall b1 b2 delta gv, Genv.find_var_info ge b2 = Some gv -> f b1 = Some(b2, delta) -> b2 = b1). + +Lemma external_call_mem_inject: + forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs', + meminj_preserves_globals ge f -> + external_call ef ge vargs m1 t vres m2 -> + Mem.inject f m1 m1' -> + val_list_inject f vargs vargs' -> + exists f', exists vres', exists m2', + external_call ef ge vargs' m1' t vres' m2' + /\ val_inject f' vres vres' + /\ Mem.inject f' m2 m2' + /\ Mem.unchanged_on (loc_unmapped f) m1 m2 + /\ Mem.unchanged_on (loc_out_of_reach f m1) m1' m2' + /\ inject_incr f f' + /\ inject_separated f f' m1 m1'. +Proof. + intros. destruct H as (A & B & C). eapply external_call_mem_inject_gen; eauto. + repeat split; intros. + + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + + simpl in H3. exploit A; eauto. intros EQ; rewrite EQ in H; inv H. auto. + + simpl in H3. exists b1; split; eauto. + + unfold block_is_volatile; simpl. + destruct (Genv.find_var_info ge b1) as [gv1|] eqn:V1. + * exploit B; eauto. intros EQ; rewrite EQ in H; inv H. rewrite V1; auto. + * destruct (Genv.find_var_info ge b2) as [gv2|] eqn:V2; auto. + exploit C; eauto. intros EQ; subst b2. congruence. +Qed. + (** Corollaries of [external_call_determ]. *) Lemma external_call_match_traces: @@ -1658,6 +1736,7 @@ Lemma external_call_symbols_preserved': forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2, external_call' ef ge1 vargs m1 t vres m2 -> (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) -> + (forall id, Genv.public_symbol ge2 id = Genv.public_symbol ge1 id) -> (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) -> external_call' ef ge2 vargs m1 t vres m2. Proof. diff --git a/common/Globalenvs.v b/common/Globalenvs.v index e4772e25..eb98e876 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -82,6 +82,7 @@ Variable V: Type. (**r The type of information attached to variables *) (** The type of global environments. *) Record t: Type := mkgenv { + genv_public: list ident; (**r which symbol names are public *) genv_symb: PTree.t block; (**r mapping symbol -> block *) genv_funs: PTree.t F; (**r mapping function pointer -> definition *) genv_vars: PTree.t (globvar V); (**r mapping variable pointer -> info *) @@ -112,6 +113,14 @@ Definition symbol_address (ge: t) (id: ident) (ofs: int) : val := | None => Vundef end. +(** [public_symbol ge id] says whether the name [id] is public and defined. *) + +Definition public_symbol (ge: t) (id: ident) : bool := + match find_symbol ge id with + | None => false + | Some _ => In_dec ident_eq id ge.(genv_public) + end. + (** [find_funct_ptr ge b] returns the function description associated with the given address. *) @@ -144,6 +153,7 @@ Definition find_var_info (ge: t) (b: block) : option (globvar V) := Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := @mkgenv + ge.(genv_public) (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) (match idg#2 with | Gfun f => PTree.set ge.(genv_next) f ge.(genv_funs) @@ -208,8 +218,8 @@ Proof. induction gl1; simpl; intros. auto. rewrite IHgl1; auto. Qed. -Program Definition empty_genv : t := - @mkgenv (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. +Program Definition empty_genv (pub: list ident): t := + @mkgenv pub (PTree.empty _) (PTree.empty _) (PTree.empty _) 1%positive _ _ _ _ _. Next Obligation. rewrite PTree.gempty in H. discriminate. Qed. @@ -227,7 +237,7 @@ Next Obligation. Qed. Definition globalenv (p: program F V) := - add_globals empty_genv p.(prog_defs). + add_globals (empty_genv p.(prog_public)) p.(prog_defs). (** Proof principles *) @@ -277,6 +287,14 @@ End GLOBALENV_PRINCIPLES. (** ** Properties of the operations over global environments *) +Theorem public_symbol_exists: + forall ge id, public_symbol ge id = true -> exists b, find_symbol ge id = Some b. +Proof. + unfold public_symbol; intros. destruct (find_symbol ge id) as [b|]. + exists b; auto. + discriminate. +Qed. + Theorem shift_symbol_address: forall ge id ofs n, symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). @@ -486,6 +504,21 @@ Proof. rewrite IHgl. auto. Qed. +Remark genv_public_add_globals: + forall gl ge, + genv_public (add_globals ge gl) = genv_public ge. +Proof. + induction gl; simpl; intros. + auto. + rewrite IHgl; auto. +Qed. + +Theorem globalenv_public: + forall p, genv_public (globalenv p) = prog_public p. +Proof. + unfold globalenv; intros. rewrite genv_public_add_globals. auto. +Qed. + (** * Construction of the initial memory state *) Section INITMEM. @@ -1092,7 +1125,7 @@ Lemma init_mem_genv_next: forall p m, Proof. unfold init_mem; intros. exploit alloc_globals_nextblock; eauto. rewrite Mem.nextblock_empty. intro. - generalize (genv_next_add_globals (prog_defs p) empty_genv). + generalize (genv_next_add_globals (prog_defs p) (empty_genv (prog_public p))). fold (globalenv p). simpl genv_next. intros. congruence. Qed. @@ -1606,6 +1639,17 @@ Proof. intros. destruct globalenvs_match. unfold find_symbol. auto. Qed. +Theorem public_symbol_match: + forall (s : ident), + ~In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. unfold public_symbol. rewrite find_symbol_match by auto. + destruct (find_symbol (globalenv p) s); auto. + rewrite ! globalenv_public. + destruct progmatch as (P & Q & R). rewrite R. auto. +Qed. + Hypothesis new_ids_fresh : forall s', find_symbol (globalenv p) s' <> None -> ~In s' (map fst new_globs). @@ -1804,6 +1848,14 @@ Proof. intros. eapply find_symbol_match. eexact prog_match. auto. Qed. +Theorem public_symbol_transf_augment: + forall (s: ident), + ~ In s (map fst new_globs) -> + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + intros. eapply public_symbol_match. eexact prog_match. auto. +Qed. + Theorem init_mem_transf_augment: (forall s', find_symbol (globalenv p) s' <> None -> ~ In s' (map fst new_globs)) -> @@ -1910,6 +1962,14 @@ Proof. auto. Qed. +Theorem public_symbol_transf_partial2: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + pose proof (@public_symbol_transf_augment _ _ _ _ _ _ _ _ _ _ transf_augment_OK). + auto. +Qed. + Theorem init_mem_transf_partial2: forall m, init_mem p = Some m -> init_mem p' = Some m. Proof. @@ -1968,6 +2028,13 @@ Proof. exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf_partial: + forall (s: ident), + public_symbol (globalenv p') s = public_symbol (globalenv p) s. +Proof. + exact (@public_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf_OK). +Qed. + Theorem find_var_info_transf_partial: forall (b: block), find_var_info (globalenv p') b = find_var_info (globalenv p) b. @@ -2047,6 +2114,13 @@ Proof. exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK). Qed. +Theorem public_symbol_transf: + forall (s: ident), + public_symbol (globalenv tp) s = public_symbol (globalenv p) s. +Proof. + exact (@public_symbol_transf_partial _ _ _ _ _ _ transf_OK). +Qed. + Theorem find_var_info_transf: forall (b: block), find_var_info (globalenv tp) b = find_var_info (globalenv p) b. diff --git a/common/Smallstep.v b/common/Smallstep.v index 02b18fc8..e74101b5 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -516,8 +516,8 @@ Record forward_simulation (L1 L2: semantics) : Type := exists i', exists s2', (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i)) /\ fsim_match_states i' s1' s2'; - fsim_symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id + fsim_public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id }. Implicit Arguments forward_simulation []. @@ -548,8 +548,8 @@ Section FORWARD_SIMU_DIAGRAMS. Variable L1: semantics. Variable L2: semantics. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id. +Hypothesis public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id. Variable match_states: state L1 -> state L2 -> Prop. @@ -809,7 +809,7 @@ Proof. right; split. subst t; apply star_refl. red. right. auto. exists s3; auto. (* symbols *) - intros. transitivity (Genv.find_symbol (globalenv L2) id); apply fsim_symbols_preserved; auto. + intros. transitivity (Genv.public_symbol (globalenv L2) id); apply fsim_public_preserved; auto. Qed. End COMPOSE_SIMULATIONS. @@ -927,8 +927,8 @@ Record backward_simulation (L1 L2: semantics) : Type := exists i', exists s1', (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i)) /\ bsim_match_states i' s1' s2'; - bsim_symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id + bsim_public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id }. (** An alternate form of the simulation diagram *) @@ -957,8 +957,8 @@ Section BACKWARD_SIMU_DIAGRAMS. Variable L1: semantics. Variable L2: semantics. -Hypothesis symbols_preserved: - forall id, Genv.find_symbol (globalenv L2) id = Genv.find_symbol (globalenv L1) id. +Hypothesis public_preserved: + forall id, Genv.public_symbol (globalenv L2) id = Genv.public_symbol (globalenv L1) id. Variable match_states: state L1 -> state L2 -> Prop. @@ -1201,7 +1201,7 @@ Proof. (* simulation *) exact bb_simulation. (* symbols *) - intros. transitivity (Genv.find_symbol (globalenv L2) id); apply bsim_symbols_preserved; auto. + intros. transitivity (Genv.public_symbol (globalenv L2) id); apply bsim_public_preserved; auto. Qed. End COMPOSE_BACKWARD_SIMULATIONS. @@ -1298,7 +1298,7 @@ Proof. subst. inv H1. elim H2; auto. right; intuition. eapply match_traces_preserved with (ge1 := (globalenv L2)); auto. - intros; symmetry; apply (fsim_symbols_preserved FS). + intros; symmetry; apply (fsim_public_preserved FS). Qed. Lemma f2b_determinacy_star: @@ -1492,7 +1492,7 @@ Proof. (* simulation *) exact f2b_simulation_step. (* symbols preserved *) - exact (fsim_symbols_preserved FS). + exact (fsim_public_preserved FS). Qed. End FORWARD_TO_BACKWARD. @@ -1614,7 +1614,7 @@ Proof. (* simulation *) exact ffs_simulation. (* symbols preserved *) - simpl. exact (fsim_symbols_preserved sim). + simpl. exact (fsim_public_preserved sim). Qed. End FACTOR_FORWARD_SIMULATION. @@ -1711,7 +1711,7 @@ Proof. (* simulation *) exact fbs_simulation. (* symbols *) - simpl. exact (bsim_symbols_preserved sim). + simpl. exact (bsim_public_preserved sim). Qed. End FACTOR_BACKWARD_SIMULATION. diff --git a/driver/Interp.ml b/driver/Interp.ml index 1291d70c..9bb9d237 100644 --- a/driver/Interp.ml +++ b/driver/Interp.ml @@ -380,13 +380,33 @@ let do_printf m fmt args = let (>>=) opt f = match opt with None -> None | Some arg -> f arg +(* Like eventval_of_val, but accepts static globals as well *) + +let convert_external_arg ge v t = + match v, t with + | Vint i, AST.Tint -> Some (EVint i) + | 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 -> + Genv.invert_symbol ge b >>= fun id -> Some (EVptr_global(id, ofs)) + | _, _ -> None + +let rec convert_external_args ge vl tl = + match vl, tl with + | [], [] -> Some [] + | v1::vl, t1::tl -> + convert_external_arg ge v1 t1 >>= fun e1 -> + convert_external_args ge vl tl >>= fun el -> Some (e1 :: el) + | _, _ -> None + let do_external_function id sg ge w args m = match extern_atom id, args with | "printf", Vptr(b, ofs) :: args' -> extract_string m b ofs >>= fun fmt -> print_string (do_printf m fmt args'); flush stdout; - Cexec.list_eventval_of_val ge args sg.sig_args >>= fun eargs -> + convert_external_args ge args sg.sig_args >>= fun eargs -> Some(((w, [Event_syscall(id, eargs, EVint Int.zero)]), Vint Int.zero), m) | _ -> None diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index eba710a1..57d7de4a 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -48,6 +48,14 @@ Proof. exact TRANSF. Qed. +Lemma public_preserved: + forall id, Genv.public_symbol tge id = Genv.public_symbol ge id. +Proof. + intros. unfold ge, tge. + apply Genv.public_symbol_transf_partial with transf_fundef. + exact TRANSF. +Qed. + Lemma functions_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> @@ -672,7 +680,7 @@ Opaque loadind. eapply exec_step_builtin. eauto. eauto. eapply find_instr_tail; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eauto. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). @@ -699,7 +707,7 @@ Opaque loadind. eapply exec_step_annot. eauto. eauto. eapply find_instr_tail; eauto. eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. @@ -876,7 +884,7 @@ Transparent destroyed_at_function_entry. left; econstructor; split. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved'; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor; eauto. unfold loc_external_result. apply agree_set_other; auto. apply agree_set_mregs; auto. @@ -920,7 +928,7 @@ Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. exact step_simulation. |