From 90b76a0842b7f080893dd70a7c0c6bc878f4056b Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Tue, 5 Dec 2017 14:48:18 +0100
Subject: Optimization for division by one during constant propagation (#39)

Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase.  This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
---
 x86/ConstpropOp.vp     | 26 ++++++++++++++++----------
 x86/ConstpropOpproof.v |  8 ++++++++
 2 files changed, 24 insertions(+), 10 deletions(-)

(limited to 'x86')

diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index f0000a85..be0cc09a 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -248,18 +248,24 @@ Definition make_xorimm (n: int) (r: reg) :=
   else (Oxorimm n, r :: nil).
 
 Definition make_divimm n (r1 r2: reg) :=
-  match Int.is_power2 n with
-  | Some l => if Int.ltu l (Int.repr 31)
-              then (Oshrximm l, r1 :: nil)
-              else (Odiv, r1 :: r2 :: nil)
-  | None   => (Odiv, r1 :: r2 :: nil)
-  end.
+  if Int.eq n Int.one then
+    (Omove, r1 :: nil)
+  else
+    match Int.is_power2 n with
+    | Some l => if Int.ltu l (Int.repr 31)
+                then (Oshrximm l, r1 :: nil)
+                else (Odiv, r1 :: r2 :: nil)
+    | None   => (Odiv, r1 :: r2 :: nil)
+    end.
 
 Definition make_divuimm n (r1 r2: reg) :=
-  match Int.is_power2 n with
-  | Some l => (Oshruimm l, r1 :: nil)
-  | None   => (Odivu, r1 :: r2 :: nil)
-  end.
+  if Int.eq n Int.one then
+    (Omove, r1 :: nil)
+  else
+    match Int.is_power2 n with
+    | Some l => (Oshruimm l, r1 :: nil)
+    | None   => (Odivu, r1 :: r2 :: nil)
+    end.
 
 Definition make_moduimm n (r1 r2: reg) :=
   match Int.is_power2 n with
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index ce20738c..e82c2963 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -421,6 +421,10 @@ Lemma make_divimm_correct:
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
+  predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H.
+  destruct (e#r1) eqn:?;
+    try (rewrite Val.divs_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto);
+    inv H; auto.
   destruct (Int.is_power2 n) eqn:?.
   destruct (Int.ltu i (Int.repr 31)) eqn:?.
   exists v; split; auto. simpl. eapply Val.divs_pow2; eauto. congruence.
@@ -436,6 +440,10 @@ Lemma make_divuimm_correct:
   exists w, eval_operation ge (Vptr sp Ptrofs.zero) op e##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
+  predSpec Int.eq Int.eq_spec n Int.one; intros. subst. rewrite H0 in H.
+  destruct (e#r1) eqn:?;
+    try (rewrite Val.divu_one in H; exists (Vint i); split; simpl; try rewrite Heqv0; auto);
+    inv H; auto.
   destruct (Int.is_power2 n) eqn:?.
   econstructor; split. simpl; eauto.
   rewrite H0 in H. erewrite Val.divu_pow2 by eauto. auto.
-- 
cgit