From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/ConstpropOp.vp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'ia32/ConstpropOp.vp') diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index b27f405..8c7f01f 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -174,10 +174,15 @@ Definition make_moduimm n (r1 r2: reg) := end. 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_cast8unsigned (r: reg) (a: aval) := @@ -186,10 +191,6 @@ Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). Definition make_cast16unsigned (r: reg) (a: aval) := if vincl a (Uns 16) then (Omove, r :: nil) else (Ocast16unsigned, 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) := @@ -217,9 +218,10 @@ Nondetfunction op_strength_reduction | Olea addr, args, vl => let (addr', args') := addr_strength_reduction addr args vl in (Olea addr', args') - | 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. -- cgit v1.2.3