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

6 files changed, 40 insertions, 32 deletions

diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 4ed4bc8..e60de3d 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -599,10 +599,10 @@ Definition build_compilenv
     (globenv, 0).
 
 Definition assign_global_variable
-     (ce: compilenv) (info: ident * list init_data * var_kind) : compilenv :=
+     (ce: compilenv) (info: ident * globvar var_kind) : compilenv :=
   match info with
-  | (id, _, Vscalar chunk) => PMap.set id (Var_global_scalar chunk) ce
-  | (id, _, Varray _) => PMap.set id Var_global_array ce
+  | (id, mkglobvar (Vscalar chunk) _ _ _ ) => PMap.set id (Var_global_scalar chunk) ce
+  | (id, mkglobvar (Varray _) _ _ _) => PMap.set id Var_global_array ce
   end.
 
 Definition build_global_compilenv (p: Csharpminor.program) : compilenv :=
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9f572ed..bb7d95a 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -94,9 +94,9 @@ Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop :=
 Lemma global_compilenv_charact:
   global_compilenv_match gce gvare.
 Proof.
-  set (mkgve := fun gv (vars: list (ident * list init_data * var_kind)) =>
+  set (mkgve := fun gv (vars: list (ident * globvar var_kind)) =>
          List.fold_left
-          (fun gve x => match x with (id, init, k) => PTree.set id k gve end)
+          (fun gve x => match x with (id, v) => PTree.set id v.(gvar_info) gve end)
           vars gv).
   assert (forall vars gv ce,
             global_compilenv_match ce gv ->
@@ -105,7 +105,7 @@ Proof.
   induction vars; simpl; intros.
   auto.
   apply IHvars. intro id1. unfold assign_global_variable.
-  destruct a as [[id2 init2] lv2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec.
+  destruct a as [id2 lv2]. destruct lv2. destruct gvar_info; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec.
   case (peq id1 id2); intro. auto. apply H. 
   case (peq id1 id2); intro. auto. apply H.
 
@@ -799,7 +799,8 @@ Inductive match_globalenvs (f: meminj) (bound: Z): Prop :=
       (POS: bound > 0)
       (DOMAIN: forall b, b < bound -> f b = Some(b, 0))
       (IMAGE: forall b1 b2 delta, f b1 = Some(b2, delta) -> b2 < bound -> b1 = b2)
-      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound).
+      (SYMBOLS: forall id b, Genv.find_symbol ge id = Some b -> b < bound)
+      (INFOS: forall b gv, Genv.find_var_info ge b = Some gv -> b < bound).
 
 (** Matching of call stacks imply:
 - matching of environments for each of the frames
@@ -1250,22 +1251,23 @@ Qed.
 
 Remark external_call_nextblock_incr:
   forall ef vargs m1 t vres m2,
-  external_call ef (Genv.find_symbol ge) vargs m1 t vres m2 ->
+  external_call ef ge vargs m1 t vres m2 ->
   Mem.nextblock m1 <= Mem.nextblock m2.
 Proof.
   intros. 
-  generalize (external_call_valid_block _ _ _ _ _ _ _ (Mem.nextblock m1 - 1) H).
+  generalize (@external_call_valid_block _ _ _ _ _ _ _ _ _ (Mem.nextblock m1 - 1) H).
   unfold Mem.valid_block. omega. 
 Qed.
 
 Remark inj_preserves_globals:
   forall f hi,
   match_globalenvs f hi ->
-  meminj_preserves_globals (Genv.find_symbol ge) f.
+  meminj_preserves_globals ge f.
 Proof.
-  intros. inv H. split; intros.
-  apply DOMAIN. eapply SYMBOLS. eauto.
-  symmetry. eapply IMAGE; eauto. 
+  intros. inv H.
+  split. intros. apply DOMAIN. eapply SYMBOLS. eauto.
+  split. intros. apply DOMAIN. eapply INFOS. eauto. 
+  intros. symmetry. eapply IMAGE; eauto. 
 Qed.
 
 (** * Soundness of chunk and type inference. *)
@@ -3176,7 +3178,10 @@ Proof.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor.
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved_2; eauto.
+  exact symbols_preserved.
+  eexact (Genv.find_var_info_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
+  eexact (Genv.find_var_info_rev_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
   econstructor; eauto.
   apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
@@ -3216,6 +3221,7 @@ Proof.
   intros. unfold Mem.flat_inj in H0. 
   destruct (zlt b1 (Mem.nextblock m)); congruence.
   intros. eapply Genv.find_symbol_not_fresh; eauto.
+  intros. eapply Genv.find_var_info_not_fresh; eauto. 
 Qed.
 
 Lemma transl_initial_states:
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index 4e4c379..4288409 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -901,7 +901,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f f.(fn_body) k e m2)
 
   | step_external_function: forall id targs tres vargs k m vres t m',
-      external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' ->
+      external_call (external_function id targs tres) ge vargs m t vres m' ->
       step (Callstate (External id targs tres) vargs k m)
          t (Returnstate vres k m')
 
@@ -1106,7 +1106,7 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop :=
       Mem.free_list m3 (blocks_of_env e) = Some m4 ->
       eval_funcall m (Internal f) vargs t m4 vres
   | eval_funcall_external: forall m id targs tres vargs t vres m',
-      external_call (external_function id targs tres) (Genv.find_symbol ge) vargs m t vres m' ->
+      external_call (external_function id targs tres) ge vargs m t vres m' ->
       eval_funcall m (External id targs tres) vargs t m' vres.
 
 Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 4c61918..558ae1c 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -516,7 +516,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State f f.(fn_body) k e m2)
 
   | 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')        
 
@@ -554,7 +554,7 @@ Inductive final_state: state -> int -> Prop :=
 
 Definition global_var_env (p: program): gvarenv :=
   List.fold_left
-    (fun gve x => match x with (id, init, k) => PTree.set id k gve end)
+    (fun gve x => match x with (id, v) => PTree.set id (gvar_info v) gve end)
     p.(prog_vars) (PTree.empty var_kind).
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index 99450de..fb1edbe 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -279,9 +279,9 @@ Qed.
 
 Definition globvarenv 
     (gv: gvarenv)
-    (vars: list (ident * list init_data * var_kind)) :=
+    (vars: list (ident * globvar var_kind)) :=
   List.fold_left
-    (fun gve x => match x with (id, init, k) => PTree.set id k gve end)
+    (fun gve x => match x with (id, v) => PTree.set id (gvar_info v) gve end)
     vars gv.
 
 Definition type_not_by_value (ty: type) : Prop :=
@@ -324,21 +324,20 @@ Qed.
 Lemma add_global_var_match_globalenv:
   forall vars tenv gv tvars,
   match_globalenv tenv gv ->
-  map_partial AST.prefix_var_name transl_globvar vars = OK tvars ->
+  map_partial AST.prefix_name (transf_globvar transl_globvar) vars = OK tvars ->
   match_globalenv (add_global_vars tenv vars) (globvarenv gv tvars).
 Proof.
   induction vars; simpl.
   intros. inversion H0. assumption.
-  destruct a as [[id init] ty]. intros until tvars; intro.
-  caseEq (transl_globvar ty); simpl; try congruence. intros vk VK. 
-  caseEq (map_partial AST.prefix_var_name transl_globvar vars); simpl; try congruence. intros tvars' EQ1 EQ2.
+  destruct a as [id v]. intros until tvars; intro.
+  caseEq (transf_globvar transl_globvar v); simpl; try congruence. intros vk VK. 
+  caseEq (map_partial AST.prefix_name (transf_globvar transl_globvar) vars); simpl; try congruence. intros tvars' EQ1 EQ2.
   inversion EQ2; clear EQ2. simpl. 
   apply IHvars; auto.
-  red. intros until chunk. repeat rewrite PTree.gsspec. 
+  red. intros until chunk. unfold add_global_var. repeat rewrite PTree.gsspec. simpl. 
   destruct (peq id0 id); intros.
-  inversion H0; clear H0; subst id0 ty0. 
-  generalize (var_kind_by_value _ _ H2). 
-  unfold transl_globvar in VK. congruence.
+  inv H0. monadInv VK. unfold transl_globvar in EQ.  
+  generalize (var_kind_by_value _ _ H2). simpl. congruence.
   red in H. eauto. 
 Qed.
 
@@ -1561,7 +1560,10 @@ Proof.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
   apply plus_one. constructor. eauto. 
-  eapply external_call_symbols_preserved; eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved_2; eauto.
+  exact symbols_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.
 
 (* returnstate 0 *)
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 2bb9a9d..b147fbd 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -159,11 +159,11 @@ Inductive wt_fundef: typenv -> fundef -> Prop :=
       wt_fundef env (External id args res).
 
 Definition add_global_var
-     (env: typenv) (id_ty_init: ident * list init_data * type) : typenv :=
-  match id_ty_init with (id, init, ty) => PTree.set id ty env end.
+     (env: typenv) (id_v: ident * globvar type) : typenv :=
+  PTree.set (fst id_v) (gvar_info (snd id_v)) env.
 
 Definition add_global_vars
-     (env: typenv) (vars: list(ident * list init_data * type)) : typenv :=
+     (env: typenv) (vars: list(ident * globvar type)) : typenv :=
   List.fold_left add_global_var vars env.
 
 Definition add_global_fun