diff options
Diffstat (limited to 'arm/ConstpropOp.vp')
| -rw-r--r-- | arm/ConstpropOp.vp | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index bd08d597..d62240ef 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -105,16 +105,28 @@ Nondetfunction cond_strength_reduction 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'). +Definition make_cmp_imm_eq (c: condition) (args: list reg) (vl: list aval) + (n: int) (r1: reg) (v1: aval) := + if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) + else make_cmp_base c args vl. + +Definition make_cmp_imm_ne (c: condition) (args: list reg) (vl: list aval) + (n: int) (r1: reg) (v1: aval) := + if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) + else make_cmp_base c args vl. + 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 Ptop 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) - else make_cmp_base c args vl + make_cmp_imm_eq c args vl n r1 v1 | Ccompimm Cne n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) - else make_cmp_base c args vl + make_cmp_imm_ne c args vl n r1 v1 + | Ccompuimm Ceq n, r1 :: nil, v1 :: nil => + make_cmp_imm_eq c args vl n r1 v1 + | Ccompuimm Cne n, r1 :: nil, v1 :: nil => + make_cmp_imm_ne c args vl n r1 v1 | _, _, _ => make_cmp_base c args vl end. |