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. --- powerpc/SelectLongproof.v | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) (limited to 'powerpc/SelectLongproof.v') 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. -- cgit