From 37cebaabf65fe3961b9932c6582d15b3b676cefe Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 17 Jun 2019 09:43:34 +0200 Subject: Perform constant propagation and strength reduction on conditional moves A conditional move whose condition is statically known becomes a regular move. Otherwise, the condition can sometimes be simplified by strength reduction. --- arm/ConstpropOp.vp | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) (limited to 'arm/ConstpropOp.vp') diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index d62240ef..8555d3aa 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -20,7 +20,7 @@ Require Import Integers. Require Import Floats. Require Import Op. Require Import Registers. -Require Import ValueDomain. +Require Import ValueDomain ValueAOp. (** * Converting known values to constants *) @@ -131,6 +131,15 @@ Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := make_cmp_base c args vl end. +Definition make_select (c: condition) (ty: typ) + (r1 r2: reg) (args: list reg) (vl: list aval) := + match resolve_branch (eval_static_condition c vl) with + | Some b => (Omove, (if b then r1 else r2) :: nil) + | None => + let (c', args') := cond_strength_reduction c args vl in + (Osel c' ty, r1 :: r2 :: args') + end. + Definition make_addimm (n: int) (r: reg) := if Int.eq n Int.zero then (Omove, r :: nil) @@ -284,6 +293,7 @@ Nondetfunction op_strength_reduction | 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 | Ocmp c, args, vl => make_cmp c args vl + | Osel c ty, r1 :: r2 :: args, v1 :: v2 :: vl => make_select c ty r1 r2 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 -- cgit