summaryrefslogtreecommitdiff
path: root/powerpc/ConstpropOpproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/ConstpropOpproof.v')
-rw-r--r--powerpc/ConstpropOpproof.v32
1 files changed, 32 insertions, 0 deletions
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index 9d833bf..b7fad69 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -364,6 +364,33 @@ Proof.
econstructor; split; eauto. auto.
Qed.
+Lemma make_mulfimm_correct:
+ forall n r1 r2,
+ rs#r2 = Vfloat n ->
+ let (op, args) := make_mulfimm n r1 r1 r2 in
+ exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+Proof.
+ intros; unfold make_mulfimm.
+ destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros.
+ simpl. econstructor; split. eauto. rewrite H; subst n.
+ destruct (rs#r1); simpl; auto. rewrite Float.mul2_add; auto.
+ simpl. econstructor; split; eauto.
+Qed.
+
+Lemma make_mulfimm_correct_2:
+ forall n r1 r2,
+ rs#r1 = Vfloat n ->
+ let (op, args) := make_mulfimm n r2 r1 r2 in
+ exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+Proof.
+ intros; unfold make_mulfimm.
+ destruct (Float.eq_dec n (Float.floatofint (Int.repr 2))); intros.
+ simpl. econstructor; split. eauto. rewrite H; subst n.
+ destruct (rs#r2); simpl; auto. rewrite Float.mul2_add; auto.
+ rewrite Float.mul_commut; auto.
+ simpl. econstructor; split; eauto.
+Qed.
+
Lemma op_strength_reduction_correct:
forall op args vl v,
vl = approx_regs app args ->
@@ -407,6 +434,11 @@ Proof.
generalize (cond_strength_reduction_correct c args0 vl0).
destruct (cond_strength_reduction c args0 vl0) as [c' args']; intros.
rewrite <- H1 in H0; auto. econstructor; split; eauto.
+(* mulf *)
+ inv H0. assert (rs#r2 = Vfloat n2). InvApproxRegs; SimplVMA; auto.
+ apply make_mulfimm_correct; auto.
+ inv H0. assert (rs#r1 = Vfloat n1). InvApproxRegs; SimplVMA; auto.
+ apply make_mulfimm_correct_2; auto.
(* default *)
exists v; auto.
Qed.