Merge of branches/full-expr-4:

- Csyntax, Csem: source C language has side-effects within expressions,
  performs implicit casts, and has nondeterministic reduction semantics
  for expressions
- Cstrategy: deterministic red. sem. for the above
- Clight: the previous source C language, with pure expressions.
  Added: temporary variables + implicit casts.
- New pass SimplExpr to pull side-effects out of expressions
  (previously done in untrusted Caml code in cparser/)
- Csharpminor: added temporary variables to match Clight.
- Cminorgen: adapted, removed cast optimization (moved to back-end)
- CastOptim: RTL-level optimization of casts
- cparser: transformations Bitfields, StructByValue and StructAssign
  now work on non-simplified expressions
- Added pretty-printers for several intermediate languages,
  and matching -dxxx command-line flags.



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

1 files changed, 13 insertions, 61 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index a1bd6618..12a8e2be 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -200,18 +200,12 @@ Qed.
 (** A variant of [match_env_update_var] where a variable is optionally
   assigned to, depending on the [dst] parameter. *)
 
-Definition assign_dest (dst: option ident) (v: val) (e: Cminor.env) : Cminor.env :=
-  match dst with
-  | None => e
-  | Some id => PTree.set id v e
-  end.
-
 Lemma match_env_update_dest:
   forall map e le rs dst r v,
   map_wf map ->
   reg_map_ok map r dst ->
   match_env map e le rs ->
-  match_env map (assign_dest dst v e) le (rs#r <- v).
+  match_env map (set_optvar dst v e) le (rs#r <- v).
 Proof.
   intros. inv H0; simpl. 
   eapply match_env_update_temp; eauto. 
@@ -410,43 +404,6 @@ Proof.
   split. apply Regmap.gss. intros; apply Regmap.gso; auto.
 Qed.
 
-(** Correctness of the code generated by [store_var] and [store_optvar]. *)
-
-Lemma tr_store_var_correct:
-  forall rs cs f map r id ns nd e sp m,
-  tr_store_var f.(fn_code) map r id ns nd ->
-  map_wf map ->
-  match_env map e nil rs ->
-  exists rs',
-     star step tge (State cs f sp ns rs m)
-                E0 (State cs f sp nd rs' m)
-  /\ match_env map (PTree.set id rs#r e) nil rs'.
-Proof.
-  intros. destruct H as [rv [A B]].
-  exploit tr_move_correct; eauto. intros [rs' [EX [RES OTHER]]].
-  exists rs'; split. eexact EX.
-  apply match_env_invariant with (rs#rv <- (rs#r)).
-  apply match_env_update_var; auto.
-  intros. rewrite Regmap.gsspec. destruct (peq r0 rv).
-  subst r0; auto.
-  auto.
-Qed.
-
-Lemma tr_store_optvar_correct:
-  forall rs cs f map r optid ns nd e sp m,
-  tr_store_optvar f.(fn_code) map r optid ns nd ->
-  map_wf map ->
-  match_env map e nil rs ->
-  exists rs',
-     star step tge (State cs f sp ns rs m)
-                E0 (State cs f sp nd rs' m)
-  /\ match_env map (set_optvar optid rs#r e) nil rs'.
-Proof.
-  intros. destruct optid; simpl in *.
-  eapply tr_store_var_correct; eauto.
-  exists rs; split. subst nd. apply star_refl. auto.  
-Qed.
-
 (** Correctness of the translation of [switch] statements *)
 
 Lemma transl_switch_correct:
@@ -558,7 +515,7 @@ Definition transl_expr_prop
     (ME: match_env map e le rs),
   exists rs',
      star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m)
-  /\ match_env map (assign_dest dst v e) le rs'
+  /\ match_env map (set_optvar dst v e) le rs'
   /\ rs'#rd = v
   /\ (forall r, In r pr -> rs'#r = rs#r).
 
@@ -1042,13 +999,12 @@ Inductive tr_cont: RTL.code -> mapping ->
 with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop :=
   | match_stacks_stop:
       match_stacks Kstop nil
-  | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret n',
+  | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret,
       map_wf map ->
       tr_fun tf map f ngoto nret rret ->
       match_env map e nil rs ->
-      tr_store_optvar tf.(fn_code) map r optid n n' ->
-      ~reg_in_map map r ->
-      tr_cont tf.(fn_code) map k n' nexits ngoto nret rret cs ->
+      reg_map_ok map r optid ->
+      tr_cont tf.(fn_code) map k n nexits ngoto nret rret cs ->
       match_stacks (Kcall optid f sp e k) (Stackframe r tf sp n rs :: cs).
 
 Inductive match_states: CminorSel.state -> RTL.state -> Prop :=
@@ -1218,16 +1174,14 @@ Proof.
   inv TS. 
   exploit transl_exprlist_correct; eauto.
   intros [rs' [E [F [G J]]]].
-  exploit tr_store_optvar_correct. eauto. eauto.
-  apply match_env_update_temp. eexact F. eauto. 
-  intros [rs'' [A B]].
   econstructor; split.
-  left. eapply star_plus_trans. eexact E. eapply plus_left.
+  left. eapply plus_right. eexact E.
   eapply exec_Ibuiltin. eauto. rewrite G. 
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
-  eexact A. reflexivity. traceEq. 
-  econstructor; eauto. constructor. rewrite Regmap.gss in B. auto. 
+  traceEq. 
+  econstructor; eauto. constructor.
+  eapply match_env_update_dest; eauto.
 
   (* seq *)
   inv TS. 
@@ -1347,12 +1301,10 @@ Proof.
 
   (* return *)
   inv MS.
-  set (rs' := (rs#r <- v)).
-  assert (match_env map e nil rs'). unfold rs'; eauto with rtlg. 
-  exploit tr_store_optvar_correct. eauto. eauto. eexact H. intros [rs'' [A B]].
-  econstructor; split.
-  left; eapply plus_left. constructor. eexact A. traceEq.
-  econstructor; eauto. constructor. unfold rs' in B. rewrite Regmap.gss in B. auto.
+  econstructor; split. 
+  left; apply plus_one; constructor. 
+  econstructor; eauto. constructor. 
+  eapply match_env_update_dest; eauto.
 Qed.
 
 Lemma transl_initial_states: