diff options
Diffstat (limited to 'arm/ConstpropOp.vp')
| -rw-r--r-- | arm/ConstpropOp.vp | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index bf08610..2b658a4 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -74,6 +74,23 @@ Nondetfunction cond_strength_reduction (cond, args) end. +Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := + let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args'). + +Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := + match c, args, vl with + | Ccompimm Ceq n, r1 :: nil, v1 :: nil => + if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + else make_cmp_base c args vl + | Ccompimm Cne n, r1 :: nil, v1 :: nil => + if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + else make_cmp_base c args vl + | _, _, _ => + make_cmp_base c args vl + end. + Definition make_addimm (n: int) (r: reg) := if Int.eq n Int.zero then (Omove, r :: nil) @@ -191,8 +208,7 @@ Nondetfunction op_strength_reduction | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 r2 | Oshru, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shruimm n2 r1 r2 | Osingleoffloat, r1 :: nil, v1 :: nil => make_singleoffloat r1 v1 - | Ocmp c, args, vl => - let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') + | Ocmp c, args, vl => make_cmp c args vl | 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) |