More faithful semantics for volatile reads and writes.

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

19 files changed, 90 insertions, 25 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index b845323..c5d6adc 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -418,6 +418,14 @@ Proof.
   exact TRANSF.
 Qed.
 
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof.
+  intro. unfold ge, tge.
+  apply Genv.find_var_info_transf_partial with transf_fundef.
+  exact TRANSF.
+Qed.
+
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
@@ -717,7 +725,8 @@ Proof.
   injection H7; intro EQ; inv EQ.
   econstructor; split.
   eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   eapply match_states_return; eauto.
 
   (* return *)
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index ce577ac..445c1af 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -735,6 +735,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 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).
+
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
@@ -935,7 +939,8 @@ Proof.
   (* external function *)
   simpl. econstructor; split.
   eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
 
   (* return *)
diff --git a/backend/Cminor.v b/backend/Cminor.v
index cc4afa5..bdfb379 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 (Genv.find_symbol ge) vargs m t vres m' ->
+      external_call ef 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 (Genv.find_symbol ge) args m t res m' ->
+      external_call ef 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 65dd4de..1e87419 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 (Genv.find_symbol ge) vargs m t vres m' ->
+      external_call ef 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 b5c3b1e..16f839f 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -146,6 +146,13 @@ Proof.
   apply Genv.find_symbol_transf.
 Qed.
 
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof.
+  intros; unfold ge, tge, tprog, transf_program. 
+  apply Genv.find_var_info_transf.
+Qed.
+
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
@@ -415,7 +422,8 @@ Proof.
   (* external function *)
   simpl. econstructor; split.
   eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
 
   (* return *)
diff --git a/backend/LTL.v b/backend/LTL.v
index 4aa8afc..a44f3fa 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 (Genv.find_symbol ge) args m t res m' ->
+      external_call ef 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 64017c3..806a7aa 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 (Genv.find_symbol ge) args m t res m' ->
+      external_call ef 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 7d21651..71310a9 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 (Genv.find_symbol ge) args m t res m' ->
+      external_call ef 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 fcb1acf..5f0a2a4 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -63,6 +63,10 @@ Lemma symbols_preserved:
   Genv.find_symbol tge id = Genv.find_symbol ge id.
 Proof (Genv.find_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).
+
 Lemma sig_preserved:
   forall f tf,
   transf_fundef f = OK tf ->
@@ -684,7 +688,8 @@ Proof.
   (* external function *)
   monadInv H6. econstructor; split.
   apply plus_one. eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
 
   (* return *)
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index bbc7e7d..060c6c2 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 (Genv.find_symbol ge) args m t res m' ->
+      external_call ef 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 b823297..481b561 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 symb fr sp base mm ms mm' ms' ef vargs vres t vargs' vres',
+  forall (ge: genv) 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 symb vargs mm t vres mm' ->
+  external_call ef ge vargs mm t vres mm' ->
   Mem.extends mm' ms' ->
-  external_call ef symb vargs' ms t vres' ms' ->
+  external_call ef ge 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 (Genv.find_symbol ge) vargs mm t vres mm' ->
+  external_call ef ge vargs mm t vres mm' ->
   Mem.extends mm' ms' ->
-  external_call ef (Genv.find_symbol ge) vargs' ms t vres' ms' ->
+  external_call ef 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 90d08f1..5b63fa8 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 (Genv.find_symbol ge) args m t res m' ->
+      external_call ef 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/RTL.v b/backend/RTL.v
index c8220e5..a17c74e 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 (Genv.find_symbol ge) args m t res m' ->
+      external_call ef 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 92f4cc9..a96dfbf 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -388,6 +388,11 @@ Proof.
   intro. inversion H. reflexivity.
 Qed.
 
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof
+  (Genv.find_var_info_transf_partial transl_fundef _ TRANSL).
+
 (** Correctness of the code generated by [add_move]. *)
 
 Lemma tr_move_correct:
@@ -1320,7 +1325,8 @@ Proof.
   monadInv TF. 
   econstructor; split.
   left; apply plus_one. eapply exec_function_external; eauto. 
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
 
   (* return *)
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 1fa000c..155f7b1 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -813,6 +813,10 @@ Lemma symbols_preserved:
   Genv.find_symbol tge id = Genv.find_symbol ge id.
 Proof (@Genv.find_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).
+
 Lemma sig_preserved:
   forall f, funsig (transf_fundef f) = LTLin.funsig f.
 Proof.
@@ -1310,7 +1314,8 @@ 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.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   econstructor; eauto.
   simpl. rewrite Locmap.gss. auto.
   intros. rewrite Locmap.gso. auto. 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 0d1a1ee..e03085a 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -319,6 +319,13 @@ Proof.
   intros. destruct f; reflexivity.
 Qed.
 
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof.
+  intros; unfold ge, tge, tprog, sel_program. 
+  apply Genv.find_var_info_transf.
+Qed.
+
 (** Semantic preservation for expressions. *)
 
 Lemma sel_expr_correct:
@@ -471,7 +478,8 @@ Proof.
   constructor; auto.
   (* external call *)
   econstructor; split.
-  econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. 
+  econstructor. eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   constructor; auto.
 Qed.
 
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index fbe4b68..4406187 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1139,6 +1139,14 @@ Proof.
   exact TRANSF. 
 Qed.
 
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof.
+  intros. unfold ge, tge. 
+  apply Genv.find_var_info_transf_partial with transf_fundef.
+  exact TRANSF. 
+Qed.
+
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
@@ -1574,7 +1582,8 @@ 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.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_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 0535cbf..2eed6e8 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -240,6 +240,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 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).
+
 Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
@@ -557,7 +561,8 @@ 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.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   constructor; auto. 
 
 (* returnstate *)
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 3f0a27d..774ce85 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -160,6 +160,10 @@ Lemma symbols_preserved:
   Genv.find_symbol tge id = Genv.find_symbol ge id.
 Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef p).
 
+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 p).
+
 Lemma sig_preserved:
   forall f, funsig (tunnel_fundef f) = funsig f.
 Proof.
@@ -335,7 +339,8 @@ Proof.
   (* external function *)
   simpl. left; econstructor; split.
   eapply exec_function_external; eauto.
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
   simpl. econstructor; eauto. 
   (* return *)
   inv H3. inv H1.