diff options
Diffstat (limited to 'arm/ConstpropOp.vp')
| -rw-r--r-- | arm/ConstpropOp.vp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index caf0da6..47d2086 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -287,6 +287,11 @@ Definition make_xorimm (n: int) (r: reg) := else if Int.eq n Int.mone then (Onot, 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 @@ -317,6 +322,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. |