From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: 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 --- powerpc/SelectOpproof.v | 48 +++++++++++++++++++++++++++++++++--------------- 1 file changed, 33 insertions(+), 15 deletions(-) (limited to 'powerpc/SelectOpproof.v') 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. -- cgit