diff options
Diffstat (limited to 'arm/ConstpropOp.vp')
| -rw-r--r-- | arm/ConstpropOp.vp | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index f94606b0..bd08d597 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -160,18 +160,24 @@ Definition make_mulimm (n: int) (r1 r2: reg) := end. Definition make_divimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => if Int.ltu l (Int.repr 31) - then (Oshrximm l, r1 :: nil) - else (Odiv, r1 :: r2 :: nil) - | None => (Odiv, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => if Int.ltu l (Int.repr 31) + then (Oshrximm l, r1 :: nil) + else (Odiv, r1 :: r2 :: nil) + | None => (Odiv, r1 :: r2 :: nil) + end. Definition make_divuimm (n: int) (r1 r2: reg) := - match Int.is_power2 n with - | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil) - | None => (Odivu, r1 :: r2 :: nil) - end. + if Int.eq n Int.one then + (Omove, r1 :: nil) + else + match Int.is_power2 n with + | Some l => (Oshift (Slsr (mk_shift_amount l)), r1 :: nil) + | None => (Odivu, r1 :: r2 :: nil) + end. Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) |