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.

7 files changed, 128 insertions, 6 deletions

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
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 079ba2be..a4f5c29c 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -24,7 +24,7 @@ Require Import Events.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
-Require Import ValueDomain.
+Require Import ValueDomain ValueAOp ValueAnalysis.
 Require Import ConstpropOp.
 
 Local Transparent Archi.ptr64.
@@ -234,6 +234,28 @@ Proof.
 - apply make_cmp_base_correct; auto.
 Qed.
 
+Lemma make_select_correct:
+  forall c ty r1 r2 args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_select c ty r1 r2 args vl in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v
+         /\ Val.lessdef (Val.select (eval_condition c rs##args m) rs#r1 rs#r2 ty) v.
+Proof.
+  unfold make_select; intros.
+  destruct (resolve_branch (eval_static_condition c vl)) as [b|] eqn:RB.
+- exists (if b then rs#r1 else rs#r2); split.
++ simpl. destruct b; auto.
++ destruct (eval_condition c rs##args m) as [b'|] eqn:EC; simpl; auto.
+  assert (b = b').
+  { eapply resolve_branch_sound; eauto. 
+    rewrite <- EC. apply eval_static_condition_sound with bc. 
+    subst vl. exact (aregs_sound _ _ _ args MATCH). }
+  subst b'. apply Val.lessdef_normalize.
+- generalize (cond_strength_reduction_correct c args vl H).
+  destruct (cond_strength_reduction c args vl) as [cond' args']; intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -616,6 +638,8 @@ Proof.
   InvApproxRegs; SimplVM. inv H0. apply make_shruimm_correct; auto.
 (* cmp *)
   inv H0. apply make_cmp_correct; auto.
+(* select *)
+  inv H0. apply make_select_correct; congruence.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2).
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index 2d492b66..cf1dc6e8 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -16,7 +16,7 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats.
 Require Import Op Registers.
-Require Import ValueDomain.
+Require Import ValueDomain ValueAOp.
 
 (** * Converting known values to constants *)
 
@@ -95,6 +95,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)
@@ -303,6 +312,7 @@ Nondetfunction op_strength_reduction
   | Oshrl, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrlimm n2 r1 r2
   | Oshrlu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_shrluimm 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
diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v
index fe061e5b..38daefe4 100644
--- a/powerpc/ConstpropOpproof.v
+++ b/powerpc/ConstpropOpproof.v
@@ -14,7 +14,7 @@
 
 Require Import Coqlib Compopts.
 Require Import Integers Floats Values Memory Globalenvs Events.
-Require Import Op Registers RTL ValueDomain.
+Require Import Op Registers RTL ValueDomain ValueAOp ValueAnalysis.
 Require Import ConstpropOp.
 
 Local Transparent Archi.ptr64.
@@ -211,6 +211,28 @@ Proof.
 - apply make_cmp_base_correct; auto.
 Qed.
 
+Lemma make_select_correct:
+  forall c ty r1 r2 args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_select c ty r1 r2 args vl in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v
+         /\ Val.lessdef (Val.select (eval_condition c rs##args m) rs#r1 rs#r2 ty) v.
+Proof.
+  unfold make_select; intros.
+  destruct (resolve_branch (eval_static_condition c vl)) as [b|] eqn:RB.
+- exists (if b then rs#r1 else rs#r2); split.
++ simpl. destruct b; auto.
++ destruct (eval_condition c rs##args m) as [b'|] eqn:EC; simpl; auto.
+  assert (b = b').
+  { eapply resolve_branch_sound; eauto. 
+    rewrite <- EC. apply eval_static_condition_sound with bc. 
+    subst vl. exact (aregs_sound _ _ _ args MATCH). }
+  subst b'. apply Val.lessdef_normalize.
+- generalize (cond_strength_reduction_correct c args vl H).
+  destruct (cond_strength_reduction c args vl) as [cond' args']; intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -715,6 +737,8 @@ Proof.
   InvApproxRegs; SimplVM; inv H0. apply make_shrluimm_correct; auto.
 (* cmp *)
   inv H0. apply make_cmp_correct; auto.
+(* select *)
+  inv H0. apply make_select_correct; congruence.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) rs#r2).
diff --git a/test/regression/ifconv.c b/test/regression/ifconv.c
index dcbf43e5..e12a394c 100644
--- a/test/regression/ifconv.c
+++ b/test/regression/ifconv.c
@@ -83,6 +83,26 @@ float sdoz(float x, float y)
   return x >= y ? x - y : 0.0f;
 }
 
+/* Examples where constant propagation should take place */
+
+int constprop1(int x)
+{
+  int n = 0;
+  return n ? x : 42;
+}
+
+int constprop2(int x)
+{
+  int n = 1;
+  return n ? x : 42;
+}
+
+int constprop3(int x, int y)
+{
+  int n = 0;
+  return x < n ? y - 1 : y + 1;
+}
+
 /* Test harness */
 
 #define TESTI(call) printf(#call " = %d\n", call)
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index f59b9dba..ada8d54a 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -16,7 +16,7 @@
 Require Import Coqlib Compopts.
 Require Import AST Integers Floats.
 Require Import Op Registers.
-Require Import ValueDomain.
+Require Import ValueDomain ValueAOp.
 
 (** * Converting known values to constants *)
 
@@ -98,6 +98,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.
+
 (** For addressing modes, we need to distinguish
 - reductions that produce pointers (i.e. that produce [Aglobal], [Ainstack], [Abased] and [Abasedscaled] addressing modes), which are valid only if the pointer size is right;
 - other reductions (producing [Aindexed] or [Aindexed2] modes), which are valid independently of the pointer size.
@@ -416,6 +425,7 @@ Nondetfunction op_strength_reduction
       let (addr', args') := addr_strength_reduction_64 addr args vl in
       (Oleal addr', args')
   | 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
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 3bb0f3cd..6d2df9c1 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -14,7 +14,7 @@
 
 Require Import Coqlib Compopts.
 Require Import Integers Floats Values Memory Globalenvs Events.
-Require Import Op Registers RTL ValueDomain.
+Require Import Op Registers RTL ValueDomain ValueAOp ValueAnalysis.
 Require Import ConstpropOp.
 
 Section STRENGTH_REDUCTION.
@@ -371,6 +371,28 @@ Proof.
 - apply make_cmp_base_correct; auto.
 Qed.
 
+Lemma make_select_correct:
+  forall c ty r1 r2 args vl,
+  vl = map (fun r => AE.get r ae) args ->
+  let (op', args') := make_select c ty r1 r2 args vl in
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' e##args' m = Some v
+         /\ Val.lessdef (Val.select (eval_condition c e##args m) e#r1 e#r2 ty) v.
+Proof.
+  unfold make_select; intros.
+  destruct (resolve_branch (eval_static_condition c vl)) as [b|] eqn:RB.
+- exists (if b then e#r1 else e#r2); split.
++ simpl. destruct b; auto.
++ destruct (eval_condition c e##args m) as [b'|] eqn:EC; simpl; auto.
+  assert (b = b').
+  { eapply resolve_branch_sound; eauto. 
+    rewrite <- EC. apply eval_static_condition_sound with bc. 
+    subst vl. exact (aregs_sound _ _ _ args MATCH). }
+  subst b'. apply Val.lessdef_normalize.
+- generalize (cond_strength_reduction_correct c args vl H).
+  destruct (cond_strength_reduction c args vl) as [cond' args']; intros EQ.
+  econstructor; split. simpl; eauto. rewrite EQ; auto.
+Qed.
+
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
@@ -905,6 +927,8 @@ Proof.
   auto.
 (* cond *)
   inv H0. apply make_cmp_correct; auto.
+(* select *)
+  inv H0. apply make_select_correct; congruence.
 (* mulf *)
   InvApproxRegs; SimplVM; inv H0. rewrite <- H2. apply make_mulfimm_correct; auto.
   InvApproxRegs; SimplVM; inv H0. fold (Val.mulf (Vfloat n1) e#r2).