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.

1 files changed, 16 insertions, 10 deletions

diff --git a/riscV/ConstpropOp.vp b/riscV/ConstpropOp.vp
index 37241816..76a1e8f8 100644
--- a/riscV/ConstpropOp.vp
+++ b/riscV/ConstpropOp.vp
@@ -128,18 +128,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