diff options
Diffstat (limited to 'powerpc/ConstpropOp.vp')
-rw-r--r-- | powerpc/ConstpropOp.vp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index d0322c1..b755b5e 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -245,6 +245,11 @@ Definition make_xorimm (n: int) (r: reg) := then (Omove, r :: nil) else (Oxorimm n, r :: nil). +Definition make_mulfimm (n: float) (r r1 r2: reg) := + if Float.eq_dec n (Float.floatofint (Int.repr 2)) + then (Oaddf, r :: r :: nil) + else (Omulf, r1 :: r2 :: nil). + Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list approx) := match op, args, vl with @@ -267,6 +272,8 @@ Nondetfunction op_strength_reduction | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 | Ocmp c, args, vl => let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') + | Omulf, r1 :: r2 :: nil, v1 :: F n2 :: nil => make_mulfimm n2 r1 r1 r2 + | Omulf, r1 :: r2 :: nil, F n1 :: v2 :: nil => make_mulfimm n1 r2 r1 r2 | _, _, _ => (op, args) end. |