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 /powerpc/SelectLongproof.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 'powerpc/SelectLongproof.v')
| -rw-r--r-- | powerpc/SelectLongproof.v | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v index 3e5e82d3..a214d131 100644 --- a/powerpc/SelectLongproof.v +++ b/powerpc/SelectLongproof.v @@ -240,18 +240,12 @@ Theorem eval_shllimm: forall n, unary_constructor_sound (fun e => shllimm e n) ( Proof. intros; unfold shllimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shllimm; auto. red; intros. - assert (ROLM: forall n1 v, - Int.ltu n1 Int64.iwordsize' = true -> - Val.shll v (Vint n1) = Val.rolml v n1 (Int64.shl Int64.mone (Int64.repr (Int.unsigned n1)))). - { intros. destruct v; auto. simpl. rewrite H0. rewrite <- Int64.shl_rolm. unfold Int64.shl. - rewrite Int64.int_unsigned_repr. constructor. unfold Int64.ltu. rewrite Int64.int_unsigned_repr. - apply H0. } predSpec Int.eq Int.eq_spec n Int.zero. exists x; split; auto. subst n; destruct x; simpl; auto. destruct (Int.ltu Int.zero Int64.iwordsize'); auto. change (Int64.shl' i Int.zero) with (Int64.shl i Int64.zero). rewrite Int64.shl_zero; auto. destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. -- rewrite ROLM by apply LT. apply eval_rolml. auto. +- rewrite Val.shll_rolml by apply LT. apply eval_rolml. auto. - TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. constructor. Qed. @@ -260,18 +254,10 @@ Theorem eval_shrluimm: forall n, unary_constructor_sound (fun e => shrluimm e n) Proof. unfold shrluimm; destruct Archi.splitlong. apply SplitLongproof.eval_shrluimm. auto. red; intros. - assert (ROLM: forall n1 v, - Int.ltu n1 Int64.iwordsize' = true -> - Val.shrlu v (Vint n1) = Val.rolml v (Int.sub Int64.iwordsize' n1) (Int64.shru Int64.mone (Int64.repr (Int.unsigned n1)))). - { intros. destruct v; auto. simpl. rewrite H0. - rewrite Int64.int_sub_ltu by apply H0. 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. - } predSpec Int.eq Int.eq_spec n Int.zero. exists x. split. apply H. destruct x; simpl; auto. rewrite H0. rewrite Int64.shru'_zero. constructor. destruct (Int.ltu n Int64.iwordsize') eqn:LT; simpl. -- rewrite ROLM by apply LT. apply eval_rolml. auto. +- rewrite Val.shrlu_rolml by apply LT. apply eval_rolml. auto. - TrivialExists. constructor; eauto. constructor. EvalOp. simpl; eauto. constructor. constructor. Qed. |