diff options
Diffstat (limited to 'powerpc/ConstpropOp.vp')
| -rw-r--r-- | powerpc/ConstpropOp.vp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index f18a72e9..2d492b66 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -65,6 +65,12 @@ 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 is_an_integer (v: aval) : bool := + match v with + | Vbot | I _ | Uns _ _ | Sgn _ _ => true + | _ => false + end. + Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := match c, args, vl with | Ccompimm Ceq n, r1 :: nil, v1 :: nil => @@ -75,6 +81,16 @@ Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list 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 + | Ccompuimm 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 if is_an_integer v1 then make_cmp_base (Ccompimm Ceq n) args vl + else make_cmp_base c args vl + | Ccompuimm 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 if is_an_integer v1 then make_cmp_base (Ccompimm Cne n) args vl + else make_cmp_base c args vl | _, _, _ => make_cmp_base c args vl end. |