diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-07-12 14:05:06 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-07-12 14:05:06 +0200 |
| commit | 2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e (patch) | |
| tree | 8f7f5d59c692ee8f548a0695d14eb89cccf951c5 /common/Values.v | |
| parent | 0d783f1aa5e4f94b713588fb272ecca6a1bc23ca (diff) | |
| download | compcert-kvx-2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e.tar.gz compcert-kvx-2ee3bc6fecc3607b368fbf2a034bdfd8ccdf2d3e.zip | |
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.
Diffstat (limited to 'common/Values.v')
| -rw-r--r-- | common/Values.v | 21 |
1 files changed, 21 insertions, 0 deletions
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 -> |