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.

1 files changed, 25 insertions, 1 deletions

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).