diff options
-rw-r--r-- | lib/Integers.v | 46 | ||||
-rw-r--r-- | powerpc/SelectOp.vp | 19 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 28 |
3 files changed, 77 insertions, 16 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 8dc5b6f5..6630de33 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -653,6 +653,14 @@ Proof. auto. unfold max_signed in H. omegaContradiction. Qed. +Theorem signed_positive: + forall x, signed x >= 0 <-> unsigned x <= max_signed. +Proof. + intros. unfold signed, max_signed. + generalize (unsigned_range x) half_modulus_modulus half_modulus_pos; intros. + destruct (zlt (unsigned x) half_modulus); omega. +Qed. + (** ** Properties of zero, one, minus one *) Theorem unsigned_zero: unsigned zero = 0. @@ -2660,6 +2668,44 @@ Proof. generalize min_signed_neg. unfold max_signed. omega. Qed. +(** Connections between [shr] and [shru]. *) + +Lemma shr_shru_positive: + forall x y, + signed x >= 0 -> + shr x y = shru x y. +Proof. + intros. + rewrite shr_div_two_p. rewrite shru_div_two_p. + rewrite signed_eq_unsigned. auto. apply signed_positive. auto. +Qed. + +Lemma and_positive: + forall x y, signed y >= 0 -> signed (and x y) >= 0. +Proof. + intros. + assert (unsigned y < half_modulus). rewrite signed_positive in H. unfold max_signed in H; omega. + generalize (sign_bit_of_Z y). rewrite zlt_true; auto. intros A. + generalize (sign_bit_of_Z (and x y)). + unfold and at 1. unfold bitwise_binop at 1. + set (fx := bits_of_Z wordsize (unsigned x)). + set (fy := bits_of_Z wordsize (unsigned y)). + rewrite unsigned_repr; auto with ints. + rewrite bits_of_Z_of_bits. unfold fy. rewrite A. rewrite andb_false_r. + destruct (zlt (unsigned (and x y)) half_modulus); intros. + rewrite signed_positive. unfold max_signed; omega. + congruence. + generalize wordsize_pos; omega. +Qed. + +Theorem shr_and_is_shru_and: + forall x y z, + lt y zero = false -> shr (and x y) z = shru (and x y) z. +Proof. + intros. apply shr_shru_positive. apply and_positive. + unfold lt in H. rewrite signed_zero in H. destruct (zlt (signed y) 0). congruence. auto. +Qed. + (** ** Properties of integer zero extension and sign extension. *) Section EXTENSIONS. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index a1457dfa..d9139585 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -179,12 +179,6 @@ Definition shlimm (e1: expr) (n2: int) := else Eop Oshl (e1:::Eop (Ointconst n2) Enil:::Enil). -Definition shrimm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero then - e1 - else - Eop (Oshrimm n2) (e1:::Enil). - Definition shruimm (e1: expr) (n2: int) := if Int.eq n2 Int.zero then e1 @@ -193,6 +187,19 @@ Definition shruimm (e1: expr) (n2: int) := else Eop Oshru (e1:::Eop (Ointconst n2) Enil:::Enil). +Nondetfunction shrimm (e1: expr) (n2: int) := + if Int.eq n2 Int.zero then + e1 + else + match e1 with + | Eop (Oandimm mask1) (t1:::Enil) => + if Int.lt mask1 Int.zero + then Eop (Oshrimm n2) (e1:::Enil) + else shruimm e1 n2 + | _ => + Eop (Oshrimm n2) (e1:::Enil) + end. + (** ** Integer multiply *) Definition mulimm_base (n1: int) (e2: expr) := diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index fa6b5608..7d3ae831 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -286,16 +286,6 @@ Proof. TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto. Qed. -Theorem eval_shrimm: - forall n, unary_constructor_sound (fun a => shrimm a n) - (fun x => Val.shr x (Vint n)). -Proof. - red; intros. unfold shrimm. - predSpec Int.eq Int.eq_spec n Int.zero. - subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto. - TrivialExists. -Qed. - Theorem eval_shruimm: forall n, unary_constructor_sound (fun a => shruimm a n) (fun x => Val.shru x (Vint n)). @@ -308,6 +298,24 @@ Proof. TrivialExists. econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto. Qed. +Theorem eval_shrimm: + forall n, unary_constructor_sound (fun a => shrimm a n) + (fun x => Val.shr x (Vint n)). +Proof. + red; intros until x. unfold shrimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto. + case (shrimm_match a); intros. + destruct (Int.lt mask1 Int.zero) as []_eqn. + TrivialExists. + replace (Val.shr x (Vint n)) with (Val.shru x (Vint n)). + apply eval_shruimm; auto. + destruct x; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto. + decEq. symmetry. InvEval. destruct v1; simpl in H0; inv H0. + apply Int.shr_and_is_shru_and; auto. + TrivialExists. +Qed. + Lemma eval_mulimm_base: forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)). Proof. |