Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


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

1 files changed, 22 insertions, 14 deletions

diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 18deca6..1569ad6 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -26,13 +26,6 @@ Require Import SelectOp.
 
 Open Local Scope cminorsel_scope.
 
-Section CMCONSTR.
-
-Variable ge: genv.
-Variable sp: val.
-Variable e: env.
-Variable m: mem.
-
 (** * Useful lemmas and tactics *)
 
 (** The following are trivial lemmas and custom tactics that help
@@ -78,9 +71,15 @@ Ltac TrivialExists :=
   | [ |- exists v, _ /\ Val.lessdef ?a v ] => exists a; split; [EvalOp | auto]
   end.
 
-
 (** * Correctness of the smart constructors *)
 
+Section CMCONSTR.
+
+Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
 (** We now show that the code generated by "smart constructor" functions
   such as [SelectOp.notint] behaves as expected.  Continuing the
   [notint] example, we show that if the expression [e]
@@ -410,6 +409,12 @@ Proof.
   discriminate.
 Qed.
 
+Remark int_add_sub_eq:
+  forall x y z, Int.add x y = z -> Int.sub z x = y.
+Proof.
+  intros. subst z. rewrite Int.sub_add_l. rewrite Int.sub_idem. apply Int.add_zero_l.
+Qed.
+
 Lemma eval_or: binary_constructor_sound or Val.or.
 Proof.
   red; intros until y; unfold or; case (or_match a b); intros.
@@ -417,26 +422,29 @@ Proof.
   InvEval. rewrite Val.or_commut. apply eval_orimm; auto. 
   InvEval. apply eval_orimm; auto.
 (* shlimm - shruimm *)
-  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
-  destruct (andb_prop _ _ Heqb0). 
-  generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ.
+  predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
+  destruct (same_expr_pure t1 t2) eqn:?.
   InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
   exists (Val.ror v0 (Vint n2)); split. EvalOp.
   destruct v0; simpl; auto. 
   destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
   destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
   simpl. rewrite <- Int.or_ror; auto.
+  InvEval. exists (Val.or x y); split. EvalOp. 
+  simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto. auto.
   TrivialExists. 
 (* shruimm - shlimm *) 
-  destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?.
-  destruct (andb_prop _ _ Heqb0). 
-  generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ.
+  predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
+  destruct (same_expr_pure t1 t2) eqn:?.
   InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. 
   exists (Val.ror v1 (Vint n2)); split. EvalOp.
   destruct v1; simpl; auto. 
   destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
   destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
   simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
+  InvEval. exists (Val.or y x); split. EvalOp. 
+  simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto.
+  rewrite Val.or_commut; auto.
   TrivialExists. 
 (* default *)
   TrivialExists.