From 2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 12 Jul 2017 14:05:06 +0200 Subject: Constprop strength reduction (#17) PowerPC port: add strength reduction for 64-bit operations * Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748) * Moved shru_rolml proof to Values. --- common/Values.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'common/Values.v') diff --git a/common/Values.v b/common/Values.v index d086c69f..802d827b 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1259,6 +1259,16 @@ Proof. rewrite H. decEq. apply Int.shl_rolm. exact H. Qed. +Theorem shll_rolml: + forall x n, + Int.ltu n Int64.iwordsize' = true -> + shll x (Vint n) = rolml x n (Int64.shl Int64.mone (Int64.repr (Int.unsigned n))). +Proof. + intros. destruct x; auto. simpl. rewrite H. rewrite <- Int64.shl_rolm. unfold Int64.shl. + rewrite Int64.int_unsigned_repr. constructor. unfold Int64.ltu. rewrite Int64.int_unsigned_repr. + apply H. +Qed. + Theorem shru_rolm: forall x n, Int.ltu n Int.iwordsize = true -> @@ -1268,6 +1278,17 @@ Proof. rewrite H. decEq. apply Int.shru_rolm. exact H. Qed. +Theorem shrlu_rolml: + forall x n, + Int.ltu n Int64.iwordsize' = true -> + shrlu x (Vint n) = rolml x (Int.sub Int64.iwordsize' n) (Int64.shru Int64.mone (Int64.repr (Int.unsigned n))). +Proof. + intros. destruct x; auto. simpl. rewrite H. + rewrite Int64.int_sub_ltu by apply H. rewrite Int64.repr_unsigned. rewrite <- Int64.shru_rolm. unfold Int64.shru'. unfold Int64.shru. + rewrite Int64.unsigned_repr. reflexivity. apply Int64.int_unsigned_range. + unfold Int64.ltu. rewrite Int64.int_unsigned_repr. auto. +Qed. + Theorem shrx_carry: forall x y z, shrx x y = Some z -> -- cgit