Optimize integer divisions by positive constants, turning them into

multiply-high and shifts.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 28 insertions, 0 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 23f2294..cbbf28c 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -286,6 +286,11 @@ Definition rolm (x a m: int): int := and (rol x a) m.
 Definition shrx (x y: int): int :=
   divs x (shl one y).
 
+(** High half of full multiply. *)
+
+Definition mulhu (x y: int): int := repr ((unsigned x * unsigned y) / modulus).
+Definition mulhs (x y: int): int := repr ((signed x * signed y) / modulus).
+
 (** Condition flags *)
 
 Definition negative (x: int): int :=
@@ -4275,6 +4280,19 @@ Qed.
 
 Definition mul' (x y: Int.int) : int := repr (Int.unsigned x * Int.unsigned y).
 
+Lemma mul'_mulhu:
+  forall x y, mul' x y = ofwords (Int.mulhu x y) (Int.mul x y).
+Proof.
+  intros. 
+  rewrite ofwords_add. unfold mul', Int.mulhu, Int.mul. 
+  set (p := Int.unsigned x * Int.unsigned y).
+  set (ph := p / Int.modulus). set (pl := p mod Int.modulus). 
+  transitivity (repr (ph * Int.modulus + pl)).
+- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos. 
+- apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. auto with ints.
+  rewrite Int.unsigned_repr_eq. apply eqm_refl.
+Qed.
+
 Lemma decompose_mul:
   forall xh xl yh yl,
   mul (ofwords xh xl) (ofwords yh yl) =
@@ -4310,6 +4328,16 @@ Proof.
   f_equal. ring. 
 Qed.
 
+Lemma decompose_mul_2:
+  forall xh xl yh yl,
+  mul (ofwords xh xl) (ofwords yh yl) =
+  ofwords (Int.add (Int.add (Int.mulhu xl yl) (Int.mul xl yh)) (Int.mul xh yl))
+          (Int.mul xl yl).
+Proof.
+  intros. rewrite decompose_mul. rewrite mul'_mulhu. 
+  rewrite hi_ofwords, lo_ofwords. auto.
+Qed.
+
 Lemma decompose_ltu:
   forall xh xl yh yl,
   ltu (ofwords xh xl) (ofwords yh yl) = if Int.eq xh yh then Int.ltu xl yl else Int.ltu xh yh.