From 41b7ecb127b93b1aecc29a298ec21dc94603e6fa Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 29 Jul 2013 12:10:11 +0000 Subject: 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 --- lib/Integers.v | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) (limited to 'lib') 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. -- cgit v1.2.3