From ad8c37d0ebb36cb2e54baeacf5a4c7ff145b1a99 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 3 Nov 2014 17:40:22 +0100 Subject: Add Genv.public_symbol operation. Restrict pointer event values to public global names. Update proofs accordingly. PowerPC and ARM need updating. --- backend/Allocproof.v | 16 ++++++++++++---- backend/CSEproof.v | 10 +++++++--- backend/CleanupLabelsproof.v | 15 +++++++++++---- backend/Constpropproof.v | 13 ++++++++++--- backend/Deadcodeproof.v | 28 ++++++++++++++++++---------- backend/Inliningproof.v | 12 +++++++++--- backend/Linearizeproof.v | 13 +++++++++---- backend/RTLgenproof.v | 17 ++++++++++++----- backend/Renumberproof.v | 11 ++++++++--- backend/Selectionproof.v | 18 ++++++++++++------ backend/Stackingproof.v | 16 ++++++++++++---- backend/Tailcallproof.v | 10 +++++++--- backend/Tunnelingproof.v | 13 +++++++++---- 13 files changed, 136 insertions(+), 56 deletions(-) (limited to 'backend') 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. -- cgit