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 +++++++++++- arm/ConstpropOpproof.v | 26 +++++++++++++++++++++++++- powerpc/ConstpropOp.vp | 12 +++++++++++- powerpc/ConstpropOpproof.v | 26 +++++++++++++++++++++++++- test/regression/ifconv.c | 20 ++++++++++++++++++++ x86/ConstpropOp.vp | 12 +++++++++++- x86/ConstpropOpproof.v | 26 +++++++++++++++++++++++++- 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). -- cgit