Add Genv.public_symbol operation.

Restrict pointer event values to public global names.
Update proofs accordingly.  PowerPC and ARM need updating.

13 files changed, 136 insertions, 56 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.