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/ConstpropOpproof.v | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) (limited to 'arm/ConstpropOpproof.v') 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). -- cgit