Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



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

1 files changed, 68 insertions, 8 deletions

diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 22a1e79d..44e7c418 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -504,6 +504,32 @@ Proof.
   right; eauto with rtlg.
 Qed.
 
+Lemma alloc_regs_2addr_valid:
+  forall al rd s1 s2 map rl i,
+  map_valid map s1 ->
+  reg_valid rd s1 ->
+  alloc_regs_2addr map al rd s1 = OK rl s2 i ->
+  regs_valid rl s2.
+Proof.
+  unfold alloc_regs_2addr; intros. 
+  destruct al; monadInv H1.
+  apply regs_valid_nil.
+  apply regs_valid_cons. eauto with rtlg. eauto with rtlg. 
+Qed.
+Hint Resolve alloc_regs_2addr_valid: rtlg.
+
+Lemma alloc_regs_2addr_fresh_or_in_map:
+  forall map al rd s rl s' i,
+  map_valid map s ->
+  alloc_regs_2addr map al rd s = OK rl s' i ->
+  forall r, In r rl -> r = rd \/ reg_in_map map r \/ reg_fresh r s.
+Proof.
+  unfold alloc_regs_2addr; intros. 
+  destruct al; monadInv H0.
+  elim H1.
+  simpl in H1; destruct H1. auto. right. eapply alloc_regs_fresh_or_in_map; eauto.
+Qed.
+
 (** A register is an adequate target for holding the value of an
   expression if
 - either the register is associated with a Cminor let-bound variable
@@ -606,7 +632,24 @@ Proof.
   apply regs_valid_cons; eauto with rtlg.
 Qed.
 
-Hint Resolve new_reg_target_ok alloc_reg_target_ok alloc_regs_target_ok: rtlg.  
+Lemma alloc_regs_2addr_target_ok:
+  forall map al rd pr s1 rl s2 i,
+  map_valid map s1 ->
+  regs_valid pr s1 ->
+  reg_valid rd s1 -> 
+  ~(reg_in_map map rd) -> ~In rd pr ->
+  alloc_regs_2addr map al rd s1 = OK rl s2 i ->
+  target_regs_ok map pr al rl.
+Proof.
+  unfold alloc_regs_2addr; intros. destruct al; monadInv H4. 
+  constructor.
+  constructor. constructor; auto. 
+  eapply alloc_regs_target_ok; eauto.
+  apply regs_valid_cons; auto. 
+Qed.
+
+Hint Resolve new_reg_target_ok alloc_reg_target_ok 
+             alloc_regs_target_ok alloc_regs_2addr_target_ok: rtlg.  
 
 (** The following predicate is a variant of [target_reg_ok] used
   to characterize registers that are adequate for holding the return
@@ -804,9 +847,14 @@ Inductive tr_stmt (c: code) (map: mapping):
   | tr_Sskip: forall ns nexits ngoto nret rret,
      tr_stmt c map Sskip ns ns nexits ngoto nret rret
   | tr_Sassign: forall id a ns nd nexits ngoto nret rret r,
-     map.(map_vars)!id = Some r ->
+     map.(map_vars)!id = Some r -> expr_is_2addr_op a = false ->
      tr_expr c map nil a ns nd r (Some id) ->
      tr_stmt c map (Sassign id a) ns nd nexits ngoto nret rret
+  | tr_Sassign_2: forall id a ns n1 nd nexits ngoto nret rret rd r,
+     map.(map_vars)!id = Some r ->
+     tr_expr c map nil a ns n1 rd None ->
+     tr_move c n1 rd nd r ->
+     tr_stmt c map (Sassign id a) ns nd nexits ngoto nret rret
   | tr_Sstore: forall chunk addr al b ns nd nexits ngoto nret rret rd n1 rl n2,
      tr_exprlist c map nil al ns n1 rl ->
      tr_expr c map rl b n1 n2 rd None ->
@@ -970,7 +1018,9 @@ Proof.
   inv OK. left; split; congruence. right; eauto with rtlg.
   eapply add_move_charact; eauto.
   (* Eop *)
-  inv OK.
+  inv OK. destruct (two_address_op o). 
+  econstructor; eauto with rtlg.
+  eapply transl_exprlist_charact; eauto with rtlg.
   econstructor; eauto with rtlg.
   eapply transl_exprlist_charact; eauto with rtlg.
   (* Eload *)
@@ -1047,21 +1097,25 @@ Lemma transl_expr_assign_charact:
   forall id a map rd nd s ns s' INCR
      (TR: transl_expr map a rd nd s = OK ns s' INCR)
      (WF: map_valid map s)
-     (OK: reg_map_ok map rd (Some id)),
+     (OK: reg_map_ok map rd (Some id))
+     (NOT2ADDR: expr_is_2addr_op a = false),
    tr_expr s'.(st_code) map nil a ns nd rd (Some id).
 Proof.
+Opaque two_address_op.
   induction a; intros; monadInv TR; saturateTrans.
   (* Evar *)
   generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1.
   econstructor; eauto.
   eapply add_move_charact; eauto.
   (* Eop *)
-  econstructor; eauto with rtlg.
+  simpl in NOT2ADDR. rewrite NOT2ADDR in EQ. 
+  econstructor; eauto with rtlg. 
   eapply transl_exprlist_charact; eauto with rtlg.
   (* Eload *)
   econstructor; eauto with rtlg.
   eapply transl_exprlist_charact; eauto with rtlg. 
   (* Econdition *)
+  simpl in NOT2ADDR. destruct (orb_false_elim _ _ NOT2ADDR).
   econstructor; eauto with rtlg.
   eapply transl_condexpr_charact; eauto with rtlg.
   apply tr_expr_incr with s1; auto. 
@@ -1069,6 +1123,7 @@ Proof.
   apply tr_expr_incr with s0; auto. 
   eapply IHa2; eauto 2 with rtlg.
   (* Elet *)
+  simpl in NOT2ADDR.
   econstructor. eapply new_reg_not_in_map; eauto with rtlg.  
   eapply transl_expr_charact; eauto 3 with rtlg.
   apply tr_expr_incr with s1; auto.
@@ -1112,8 +1167,9 @@ Proof.
   intros s1 s2 EXT.
   generalize tr_expr_incr tr_condition_incr tr_exprlist_incr; intros I1 I2 I3.
   pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
-  induction 1; econstructor; eauto.
-  eapply tr_switch_incr; eauto.
+  induction 1; try (econstructor; eauto; fail).
+  eapply tr_Sassign_2; eauto. eapply tr_move_incr; eauto.
+  econstructor; eauto. eapply tr_switch_incr; eauto.
 Qed.
 
 Lemma transl_exit_charact:
@@ -1181,7 +1237,11 @@ Proof.
   constructor.
   (* Sassign *)
   revert EQ. unfold find_var. case_eq (map_vars map)!i; intros; monadInv EQ.
-  econstructor. eauto. 
+  remember (expr_is_2addr_op e) as is2a. destruct is2a.
+  monadInv EQ0. eapply tr_Sassign_2; eauto. 
+  eapply transl_expr_charact; eauto with rtlg.
+  apply tr_move_incr with s1; auto. eapply add_move_charact; eauto. 
+  eapply tr_Sassign; eauto.
   eapply transl_expr_assign_charact; eauto with rtlg.
   constructor. auto.
   (* Sstore *)