From 76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Sep 2013 16:24:30 +0000 Subject: Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms are necessary, only two parameters (default_pl and choose_binop_pl). SelectDiv: optimize FP division by a power of 2. ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/ConstpropOp.vp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'ia32/ConstpropOp.vp') diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp index a29b4508..8c3a7fa1 100644 --- a/ia32/ConstpropOp.vp +++ b/ia32/ConstpropOp.vp @@ -291,20 +291,25 @@ Definition make_moduimm n (r1 r2: reg) := | None => (Omodu, r1 :: r2 :: nil) end. -(** We must be careful to preserve 2-address constraints over the - RTL code, which means that commutative operations cannot - be specialized if their first argument is a constant. *) +Definition make_mulfimm (n: float) (r r1 r2: reg) := + if Float.eq_dec n (Float.floatofint (Int.repr 2)) + then (Oaddf, r :: r :: nil) + else (Omulf, r1 :: r2 :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list approx) := match op, args, vl with | Osub, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_addimm (Int.neg n2) r1 + | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2 | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2 | Omodu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_moduimm n2 r1 r2 + | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 | Oand, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_andimm n2 r1 + | Oor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_orimm n1 r2 | Oor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_orimm n2 r1 + | Oxor, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_xorimm n1 r2 | Oxor, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_xorimm n2 r1 | Oshl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shlimm n2 r1 | Oshr, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrimm n2 r1 @@ -315,6 +320,8 @@ Nondetfunction op_strength_reduction | Ocmp c, args, vl => let (c', args') := cond_strength_reduction c args vl in (Ocmp c', args') + | 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 | _, _, _ => (op, args) end. -- cgit