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, 33 insertions, 15 deletions

diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 7be88580..f7513140 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -27,13 +27,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
@@ -81,6 +74,13 @@ Ltac TrivialExists :=
 
 (** * 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]
@@ -163,7 +163,7 @@ Proof.
   rewrite Int.add_commut. auto.
   unfold symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
   rewrite Val.add_assoc. rewrite Int.add_commut. auto.
-  subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
+  subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
 Qed. 
 
 Theorem eval_add: binary_constructor_sound add Val.add.
@@ -327,7 +327,15 @@ Qed.
 Theorem eval_andimm:
   forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
 Proof.
-  intros; red; intros until x. unfold andimm. case (andimm_match a); intros.
+  intros; red; intros until x. unfold andimm. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. subst. exists (Vint Int.zero); split. EvalOp. 
+  destruct x; simpl; auto. rewrite Int.and_zero; auto.
+  predSpec Int.eq Int.eq_spec n Int.mone.
+  intros. subst. exists x; split. auto.
+  destruct x; simpl; auto. rewrite Int.and_mone; auto.
+  clear H H0.
+  case (andimm_match a); intros.
   InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
   set (n' := Int.and n n2). 
   destruct (Int.eq (Int.shru (Int.shl n' amount) amount) n' &&
@@ -376,8 +384,12 @@ Qed.
 Theorem eval_orimm:
   forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Vint n)).
 Proof.
-  intros; red; intros until x.
-  unfold orimm. destruct (orimm_match a); intros; InvEval.
+  intros; red; intros until x. unfold orimm.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.or_zero; auto.
+  predSpec Int.eq Int.eq_spec n Int.mone.
+  intros. subst. exists (Vint Int.mone); split. EvalOp. destruct x; simpl; auto. rewrite Int.or_mone; auto.
+  clear H H0. destruct (orimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.or_commut; auto.
   subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. 
   TrivialExists.
@@ -433,8 +445,10 @@ Qed.
 Theorem eval_xorimm:
   forall n, unary_constructor_sound (xorimm n) (fun x => Val.xor x (Vint n)).
 Proof.
-  intros; red; intros until x.
-  unfold xorimm. destruct (xorimm_match a); intros; InvEval.
+  intros; red; intros until x. unfold xorimm.
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.xor_zero; auto.
+  clear H. destruct (xorimm_match a); intros; InvEval.
   TrivialExists. simpl. rewrite Int.xor_commut; auto.
   subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. 
   TrivialExists.
@@ -445,9 +459,9 @@ Proof.
   red; intros until y; unfold xor; case (xor_match a b); intros; InvEval.
   rewrite Val.xor_commut. apply eval_xorimm; auto.
   apply eval_xorimm; auto.
-  subst x. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. 
+  subst. rewrite Val.xor_commut. rewrite Val.not_xor. rewrite <- Val.xor_assoc. 
   rewrite <- Val.not_xor. rewrite Val.xor_commut. TrivialExists.
-  subst y. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. TrivialExists.
+  subst. rewrite Val.not_xor. rewrite <- Val.xor_assoc. rewrite <- Val.not_xor. TrivialExists.
   TrivialExists.
 Qed.
 
@@ -843,7 +857,11 @@ Proof.
   exists (@nil val). split. eauto with evalexpr. simpl. auto.
   exists (v0 :: nil). split. eauto with evalexpr. simpl. congruence.
   exists (v1 :: nil). split. eauto with evalexpr. simpl. congruence.
+  destruct (can_use_Aindexed2 chunk). 
   exists (v1 :: v0 :: nil). split. eauto with evalexpr. simpl. congruence.
+  exists (Vptr b ofs :: nil). split.
+  constructor. EvalOp. simpl; congruence. constructor. 
+  simpl. rewrite Int.add_zero. auto.
   exists (v :: nil). split. eauto with evalexpr. subst v. simpl. 
   rewrite Int.add_zero. auto.
 Qed.