Merge pull request #202 from gergo-/mla-folding

Strength reduction patterns for ARM mla instruction.

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

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.