diff options
Diffstat (limited to 'arm/ConstpropOp.vp')
| -rw-r--r-- | arm/ConstpropOp.vp | 30 |
1 files changed, 24 insertions, 6 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 2b658a4e..4f4bf5aa 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -70,6 +70,22 @@ Nondetfunction cond_strength_reduction if Float.eq_dec n2 Float.zero then (Cnotcompfzero c, r1 :: nil) else (cond, args) + | Ccompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil => + if Float32.eq_dec n1 Float32.zero + then (Ccompfszero (swap_comparison c), r2 :: nil) + else (cond, args) + | Ccompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil => + if Float32.eq_dec n2 Float32.zero + then (Ccompfszero c, r1 :: nil) + else (cond, args) + | Cnotcompfs c, r1 :: r2 :: nil, FS n1 :: v2 :: nil => + if Float32.eq_dec n1 Float32.zero + then (Cnotcompfszero (swap_comparison c), r2 :: nil) + else (cond, args) + | Cnotcompfs c, r1 :: r2 :: nil, v1 :: FS n2 :: nil => + if Float32.eq_dec n2 Float32.zero + then (Cnotcompfszero c, r1 :: nil) + else (cond, args) | _, _, _ => (cond, args) end. @@ -164,18 +180,19 @@ Definition make_xorimm (n: int) (r: reg) := else (Oxorimm n, r :: nil). Definition make_mulfimm (n: float) (r r1 r2: reg) := - if Float.eq_dec n (Float.floatofint (Int.repr 2)) + if Float.eq_dec n (Float.of_int (Int.repr 2)) then (Oaddf, r :: r :: nil) else (Omulf, r1 :: r2 :: nil). +Definition make_mulfsimm (n: float32) (r r1 r2: reg) := + if Float32.eq_dec n (Float32.of_int (Int.repr 2)) + then (Oaddfs, r :: r :: nil) + else (Omulfs, r1 :: r2 :: nil). + Definition make_cast8signed (r: reg) (a: aval) := if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). -Definition make_singleoffloat (r: reg) (a: aval) := - if vincl a Fsingle && generate_float_constants tt - then (Omove, r :: nil) - else (Osingleoffloat, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := @@ -207,10 +224,11 @@ Nondetfunction op_strength_reduction | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 r2 | 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 => 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 + | Omulfs, r1 :: r2 :: nil, v1 :: FS n2 :: nil => make_mulfsimm n2 r1 r1 r2 + | Omulfs, r1 :: r2 :: nil, FS n1 :: v2 :: nil => make_mulfsimm n1 r2 r1 r2 | _, _, _ => (op, args) end. |