Add Genv.public_symbol operation.

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

5 files changed, 51 insertions, 22 deletions

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.