From 93ef5fbd926aead27cbfa386e88daf323d749f81 Mon Sep 17 00:00:00 2001 From: Gergö Barany Date: Fri, 15 Sep 2017 11:05:51 +0200 Subject: Strength reduction patterns for ARM mla instruction. --- arm/ConstpropOp.vp | 29 ++++++++++++++++++++ arm/ConstpropOpproof.v | 73 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 102 insertions(+) (limited to 'arm') diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index cb7a73eb..f94606b0 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -206,6 +206,30 @@ Definition make_cast8signed (r: reg) (a: aval) := Definition make_cast16signed (r: reg) (a: aval) := if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). +Definition make_mla_mulimm (n1: int) (r1 r2 r3: reg) := + if Int.eq n1 Int.zero then + (Omove, r3 :: nil) + else if Int.eq n1 Int.one then + (Oadd, r2 :: r3 :: nil) + else + (Omla, r1 :: r2 :: r3 :: nil). + +Definition make_mla_addimm (n3: int) (r1 r2 r3: reg) := + if Int.eq n3 Int.zero then + (Omul, r1 :: r2 :: nil) + else + (Omla, r1 :: r2 :: r3 :: nil). + +Definition make_mla_bothimm (n1 n3: int) (r1 r2 r3: reg) := + if Int.eq n1 Int.zero then + (Ointconst n3, nil) + else if Int.eq n1 Int.one then + make_addimm n3 r2 + else if Int.eq n3 Int.zero then + make_mulimm n1 r2 r1 + else + (Omla, r1 :: r2 :: r3 :: nil). + Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := match op, args, vl with @@ -220,6 +244,11 @@ Nondetfunction op_strength_reduction | Orsubshift s, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Orsubimm (eval_static_shift s n2), r1 :: nil) | Omul, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_mulimm n1 r2 r1 | Omul, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_mulimm n2 r1 r2 + | Omla, r1 :: r2 :: r3 :: nil, I n1 :: v2 :: I n3 :: nil => make_mla_bothimm n1 n3 r1 r2 r3 + | Omla, r1 :: r2 :: r3 :: nil, v1 :: I n2 :: I n3 :: nil => make_mla_bothimm n2 n3 r2 r1 r3 + | Omla, r1 :: r2 :: r3 :: nil, I n1 :: v2 :: v3 :: nil => make_mla_mulimm n1 r1 r2 r3 + | Omla, r1 :: r2 :: r3 :: nil, v1 :: I n2 :: v3 :: nil => make_mla_mulimm n2 r2 r1 r3 + | Omla, r1 :: r2 :: r3 :: nil, v1 :: v2 :: I n3 :: nil => make_mla_addimm n3 r1 r2 r3 | Odiv, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divimm n2 r1 r2 | Odivu, r1 :: r2 :: nil, v1 :: I n2 :: nil => make_divuimm n2 r1 r2 | Oand, r1 :: r2 :: nil, I n1 :: v2 :: nil => make_andimm n1 r2 v2 diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index c9f97aa8..93ef2475 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -285,6 +285,69 @@ Proof. econstructor; split; eauto. simpl. congruence. Qed. +Lemma make_mla_mulimm_correct: + forall n1 r1 r2 r3, + rs#r1 = Vint n1 -> + let (op, args) := make_mla_mulimm n1 r1 r2 r3 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add (Val.mul (Vint n1) rs#r2) rs#r3) v. +Proof. + intros; unfold make_mla_mulimm. + predSpec Int.eq Int.eq_spec n1 Int.zero; intros. subst. + exists (rs#r3); split; auto. destruct (rs#r2); simpl; auto. + destruct (rs#r3); simpl; auto. + rewrite Int.mul_commut, Int.mul_zero, Int.add_zero_l; auto. + rewrite Int.mul_commut, Int.mul_zero, Ptrofs.add_zero; auto. + predSpec Int.eq Int.eq_spec n1 Int.one; intros. subst. + exists (Val.add rs#r2 rs#r3); split; auto. destruct (rs#r2); simpl; auto. + destruct (rs#r3); simpl; auto. + rewrite Int.mul_commut, Int.mul_one; auto. + rewrite Int.mul_commut, Int.mul_one; auto. + eexists. simpl; split; eauto. + fold (Val.mul (Vint n1) (rs#r2)). rewrite H; auto. +Qed. + +Lemma make_mla_addimm_correct: + forall n3 r1 r2 r3, + rs#r3 = Vint n3 -> + let (op, args) := make_mla_addimm n3 r1 r2 r3 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add (Val.mul rs#r1 rs#r2) (Vint n3)) v. +Proof. + intros; unfold make_mla_addimm. + predSpec Int.eq Int.eq_spec n3 Int.zero; intros. subst. + exists (Val.mul rs#r1 rs#r2); split; auto. + destruct (rs#r1), (rs#r2); simpl; auto. + rewrite Int.add_zero; auto. + eexists. simpl; split; eauto. rewrite H; auto. +Qed. + +Lemma make_mla_bothimm_correct: + forall n1 n3 r1 r2 r3, + rs#r1 = Vint n1 -> + rs#r3 = Vint n3 -> + let (op, args) := make_mla_bothimm n1 n3 r1 r2 r3 in + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add (Val.mul (Vint n1) rs#r2) (Vint n3)) v. +Proof. + intros; unfold make_mla_bothimm. + predSpec Int.eq Int.eq_spec n1 Int.zero; intros. subst. + exists (Vint n3); split; auto. + destruct (rs#r2); simpl; auto. + rewrite Int.mul_commut, Int.mul_zero, Int.add_zero_l; auto. + predSpec Int.eq Int.eq_spec n1 Int.one; intros. subst. + generalize (make_addimm_correct n3 r2); intro ADDIMM. + destruct (make_addimm n3 r2) as [op args]. destruct ADDIMM as [v [OP LESSDEF]]. + exists v; split; auto. + destruct (rs#r2); simpl; auto. + simpl in LESSDEF. rewrite Int.mul_commut, Int.mul_one; auto. + predSpec Int.eq Int.eq_spec n3 Int.zero; intros. subst. + generalize (make_mulimm_correct n1 r2 r1 H); eauto; intro MULIMM. + destruct (make_mulimm n1 r2 r1) as [op args]. destruct MULIMM as [v [OP LESSDEF]]. + exists v; split; auto. + destruct (rs#r2); simpl; auto. + simpl in LESSDEF. rewrite Int.add_zero, Int.mul_commut; auto. + eexists. simpl; split; eauto. + fold (Val.mul (Vint n1) (rs#r2)). rewrite H, H0; auto. +Qed. + Lemma make_divimm_correct: forall n r1 r2 v, Val.divs rs#r1 rs#r2 = Some v -> @@ -480,6 +543,16 @@ Proof. InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2). rewrite Val.mul_commut. apply make_mulimm_correct; auto. InvApproxRegs; SimplVM. inv H0. apply make_mulimm_correct; auto. +(* mla *) + InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2). + apply make_mla_bothimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. + rewrite Val.mul_commut. apply make_mla_bothimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. fold (Val.mul (Vint n1) rs#r2). + apply make_mla_mulimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. + rewrite Val.mul_commut. apply make_mla_mulimm_correct; auto. + InvApproxRegs; SimplVM. inv H0. apply make_mla_addimm_correct; auto. (* divs *) assert (rs#r2 = Vint n2). clear H0. InvApproxRegs; SimplVM; auto. apply make_divimm_correct; auto. -- cgit