diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/ConstpropOp.vp | 15 | ||||
-rw-r--r-- | powerpc/ConstpropOpproof.v | 4 |
2 files changed, 13 insertions, 6 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 0ed92e90..f18a72e9 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -124,12 +124,15 @@ Definition make_mulimm (n: int) (r1 r2: reg) := end. Definition make_divimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. Definition make_divuimm (n: int) (r1 r2: reg) := match Int.is_power2 n with diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index e9d091ca..7fddd053 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -267,6 +267,10 @@ Lemma make_divimm_correct: exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. + predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H. + destruct (rs#r1) eqn:?; + try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto); + inv H; auto. destruct (Int.is_power2 n) eqn:?. destruct (Int.ltu i (Int.repr 31)) eqn:?. exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence. |