- Extended traces so that pointers within globals are supported as event values.

- Revised handling of volatile reads: the execution environment
  dictates the value read, via the trace of events.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

20 files changed, 29 insertions, 16 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3f526aa4..b845323f 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -717,6 +717,7 @@ Proof.
   injection H7; intro EQ; inv EQ.
   econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   eapply match_states_return; eauto.
 
   (* return *)
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index fcc867af..ce577aca 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -935,6 +935,7 @@ Proof.
   (* external function *)
   simpl. econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
 
   (* return *)
diff --git a/backend/Cminor.v b/backend/Cminor.v
index f2f03c5d..cc4afa50 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -496,7 +496,7 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
   | step_external_function: forall ef vargs k m t vres m',
-      external_call ef vargs m t vres m' ->
+      external_call ef (Genv.find_symbol ge) vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
          t (Returnstate vres k m')        
 
@@ -595,7 +595,7 @@ Inductive eval_funcall:
       eval_funcall m (Internal f) vargs t m3 vres
   | eval_funcall_external:
       forall ef m args t res m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       eval_funcall m (External ef) args t m' res
 
 (** Execution of a statement: [exec_stmt ge f sp e m s t e' m' out]
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 231af8fb..65dd4dec 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -354,7 +354,7 @@ Inductive step: state -> trace -> state -> Prop :=
       step (Callstate (Internal f) vargs k m)
         E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m')
   | step_external_function: forall ef vargs k m t vres m',
-      external_call ef vargs m t vres m' ->
+      external_call ef (Genv.find_symbol ge) vargs m t vres m' ->
       step (Callstate (External ef) vargs k m)
          t (Returnstate vres k m')        
 
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 6671960c..b5c3b1e3 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -415,6 +415,7 @@ Proof.
   (* external function *)
   simpl. econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   constructor; auto.
 
   (* return *)
diff --git a/backend/LTL.v b/backend/LTL.v
index 2a1172ab..4aa8afc5 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -228,7 +228,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m')
   | exec_function_external:
       forall s ef t args res m m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       step (Callstate s (External ef) args m)
          t (Returnstate s res m')
   | exec_return:
diff --git a/backend/LTLin.v b/backend/LTLin.v
index c3b432ba..64017c30 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -225,7 +225,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m')
   | exec_function_external:
       forall s ef args t res m m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       step (Callstate s (External ef) args m)
          t (Returnstate s res m')
   | exec_return:
diff --git a/backend/Linear.v b/backend/Linear.v
index be07b827..7d21651d 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -314,7 +314,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f (Vptr stk Int.zero) f.(fn_code) (call_regs rs) m')
   | exec_function_external:
       forall s ef args res rs1 rs2 m t m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) ->
       rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 ->
       step (Callstate s (External ef) rs1 m)
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 5d670650..fcb1acfb 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -684,6 +684,7 @@ Proof.
   (* external function *)
   monadInv H6. econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
 
   (* return *)
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index ceaf9a68..bbc7e7d8 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -303,7 +303,7 @@ Inductive step: state -> trace -> state -> Prop :=
                   f.(fn_code) rs empty_frame m')
   | exec_function_external:
       forall s ef args res rs1 rs2 m t m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args ->
       rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       step (Callstate s (External ef) rs1 m)
diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v
index b766ed0d..b8232971 100644
--- a/backend/Machabstr2concr.v
+++ b/backend/Machabstr2concr.v
@@ -407,12 +407,12 @@ Qed.
 (** [frame_match] is preserved by external calls. *)
 
 Lemma frame_match_external_call:
-  forall fr sp base mm ms mm' ms' ef vargs vres t vargs' vres',
+  forall symb fr sp base mm ms mm' ms' ef vargs vres t vargs' vres',
   frame_match fr sp base mm ms ->
   Mem.extends mm ms ->
-  external_call ef vargs mm t vres mm' ->
+  external_call ef symb vargs mm t vres mm' ->
   Mem.extends mm' ms' ->
-  external_call ef vargs' ms t vres' ms' ->
+  external_call ef symb vargs' ms t vres' ms' ->
   mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
   frame_match fr sp base mm' ms'.
 Proof.
@@ -420,7 +420,7 @@ Proof.
   eapply external_call_valid_block; eauto.
   eapply external_call_valid_block; eauto.
   auto.
-  rewrite (external_call_bounds _ _ _ _ _ _ _ H1); auto.
+  rewrite (external_call_bounds _ _ _ _ _ _ _ _ H1); auto.
   red; intros. apply A; auto. red. omega.
   intros. exploit fm_contents_match0; eauto. intros [v [C D]].
   exists v; split; auto.
@@ -814,9 +814,9 @@ Lemma match_stacks_external_call:
   match_stacks s ts mm ms ->
   forall ef vargs t vres mm' ms' vargs' vres',
   Mem.extends mm ms ->
-  external_call ef vargs mm t vres mm' ->
+  external_call ef (Genv.find_symbol ge) vargs mm t vres mm' ->
   Mem.extends mm' ms' ->
-  external_call ef vargs' ms t vres' ms' ->
+  external_call ef (Genv.find_symbol ge) vargs' ms t vres' ms' ->
   mem_unchanged_on (loc_out_of_bounds mm) ms ms' ->
   match_stacks s ts mm' ms'.
 Proof.
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index a6be4bc2..90d08f1f 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -233,7 +233,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_function_external:
       forall s fb rs m t rs' ef args res m',
       Genv.find_funct_ptr ge fb = Some (External ef) ->
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       extcall_arguments rs m (parent_sp s) ef.(ef_sig) args ->
       rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) ->
       step (Callstate s fb rs m)
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index c2e797ae..b0673ca8 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -285,7 +285,7 @@ Proof.
   apply wt_empty_frame.
 
   econstructor; eauto. apply wt_setreg; auto.
-  generalize (external_call_well_typed _ _ _ _ _ _ H).  
+  generalize (external_call_well_typed _ _ _ _ _ _ _ H).  
   unfold proj_sig_res, Conventions.loc_result.
   destruct (sig_res (ef_sig ef)).
   destruct t0; simpl; auto.
diff --git a/backend/RTL.v b/backend/RTL.v
index c5d4d7d0..c8220e5d 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -282,7 +282,7 @@ Inductive step: state -> trace -> state -> Prop :=
                   m')
   | exec_function_external:
       forall s ef args res t m m',
-      external_call ef args m t res m' ->
+      external_call ef (Genv.find_symbol ge) args m t res m' ->
       step (Callstate s (External ef) args m)
          t (Returnstate s res m')
   | exec_return:
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index a15095bd..92f4cc91 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1320,6 +1320,7 @@ Proof.
   monadInv TF. 
   econstructor; split.
   left; apply plus_one. eapply exec_function_external; eauto. 
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   constructor; auto.
 
   (* return *)
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index bf728fae..1fa000c9 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -1310,6 +1310,7 @@ Proof.
   intros [res' [tm' [A [B [C D]]]]]. 
   left; econstructor; split.
   apply plus_one. eapply exec_function_external; eauto. 
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
   simpl. rewrite Locmap.gss. auto.
   intros. rewrite Locmap.gso. auto. 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 1da7884e..0d1a1ee7 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -469,6 +469,10 @@ Proof.
   econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut.
   rewrite H. simpl. reflexivity. 
   constructor; auto.
+  (* external call *)
+  econstructor; split.
+  econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. 
+  constructor; auto.
 Qed.
 
 Lemma sel_initial_states:
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index f44eac2e..fbe4b68f 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1574,6 +1574,7 @@ Proof.
   exploit transl_external_arguments; eauto. intro EXTARGS.
   econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   econstructor; eauto.
   intros. unfold Regmap.set. case (RegEq.eq r (loc_result (ef_sig ef))); intro.
   rewrite e. rewrite Locmap.gss; auto. rewrite Locmap.gso; auto.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 0ca4c028..0535cbfb 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -557,6 +557,7 @@ Proof.
   intros [res' [m2' [A [B [C D]]]]].
   left. exists (Returnstate s' res' m2'); split.
   simpl. econstructor; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   constructor; auto. 
 
 (* returnstate *)
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 4cbcbd4f..3f0a27d0 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -335,6 +335,7 @@ Proof.
   (* external function *)
   simpl. left; econstructor; split.
   eapply exec_function_external; eauto.
+  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
   simpl. econstructor; eauto. 
   (* return *)
   inv H3. inv H1.