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 --- backend/SelectDiv.vp | 156 +++++++++++++ backend/SelectDivproof.v | 547 ++++++++++++++++++++++++++++++++++++++++++++++ backend/SelectLongproof.v | 2 +- backend/Selection.v | 1 + backend/Selectionproof.v | 2 + 5 files changed, 707 insertions(+), 1 deletion(-) create mode 100644 backend/SelectDiv.vp create mode 100644 backend/SelectDivproof.v (limited to 'backend') diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp new file mode 100644 index 0000000..e60a97d --- /dev/null +++ b/backend/SelectDiv.vp @@ -0,0 +1,156 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for integer division and modulus *) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. + +Open Local Scope cminorsel_scope. + +(** We try to turn divisions by a constant into a multiplication by + a pseudo-inverse of the divisor. The approach is described in +- Torbjörn Granlund, Peter L. Montgomery: "Division by Invariant + Integers using Multiplication". PLDI 1994. +- Henry S. Warren, Jr: "Hacker's Delight". Addison-Wesley. Chapter 10. +*) + +Fixpoint find_div_mul_params (fuel: nat) (nc: Z) (d: Z) (p: Z) : option (Z * Z) := + match fuel with + | O => None + | S fuel' => + let twp := two_p p in + if zlt (nc * (d - twp mod d)) twp + then Some(p - 32, (twp + d - twp mod d) / d) + else find_div_mul_params fuel' nc d (p + 1) + end. + +Definition divs_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int.wordsize + (Int.half_modulus - Int.half_modulus mod d - 1) + d 32 with + | None => None + | Some(p, m) => + if zlt 0 d + && zlt (two_p (32 + p)) (m * d) + && zle (m * d) (two_p (32 + p) + two_p (p + 1)) + && zle 0 m && zlt m Int.modulus + && zle 0 p && zlt p 32 + then Some(p, m) else None + end. + +Definition divu_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int.wordsize + (Int.modulus - Int.modulus mod d - 1) + d 32 with + | None => None + | Some(p, m) => + if zlt 0 d + && zle (two_p (32 + p)) (m * d) + && zle (m * d) (two_p (32 + p) + two_p p) + && zle 0 m && zlt m Int.modulus + && zle 0 p && zlt p 32 + then Some(p, m) else None + end. + +Definition divu_mul (p: Z) (m: Z) := + shruimm (Eop Omulhu (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil)) + (Int.repr p). + +Definition divuimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => shruimm e1 l + | None => + match divu_mul_params (Int.unsigned n2) with + | None => divu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divu_mul p m) + end + end. + +Nondetfunction divu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divuimm e1 n2 + | _ => divu_base e1 e2 + end. + +Definition mod_from_div (equo: expr) (n: int) := + Eop Osub (Eletvar O ::: mulimm n equo ::: Enil). + +Definition moduimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => andimm (Int.sub n2 Int.one) e1 + | None => + match divu_mul_params (Int.unsigned n2) with + | None => modu_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2) + end + end. + +Nondetfunction modu (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => moduimm e1 n2 + | _ => modu_base e1 e2 + end. + +Definition divs_mul (p: Z) (m: Z) := + let e2 := + Eop Omulhs (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil) in + let e3 := + if zlt m Int.half_modulus then e2 else add e2 (Eletvar O) in + add (shrimm e3 (Int.repr p)) + (shruimm (Eletvar O) (Int.repr (Int.zwordsize - 1))). + +Definition divsimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => + if Int.ltu l (Int.repr 31) + then shrximm e1 l + else divs_base e1 (Eop (Ointconst n2) Enil) + | None => + match divs_mul_params (Int.signed n2) with + | None => divs_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (divs_mul p m) + end + end. + +Nondetfunction divs (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => divsimm e1 n2 + | _ => divs_base e1 e2 + end. + +Definition modsimm (e1: expr) (n2: int) := + match Int.is_power2 n2 with + | Some l => + if Int.ltu l (Int.repr 31) + then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2) + else mods_base e1 (Eop (Ointconst n2) Enil) + | None => + match divs_mul_params (Int.signed n2) with + | None => mods_base e1 (Eop (Ointconst n2) Enil) + | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2) + end + end. + +Nondetfunction mods (e1: expr) (e2: expr) := + match e2 with + | Eop (Ointconst n2) Enil => modsimm e1 n2 + | _ => mods_base e1 e2 + end. + diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v new file mode 100644 index 0000000..4d8f96a --- /dev/null +++ b/backend/SelectDivproof.v @@ -0,0 +1,547 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness of instruction selection for integer division *) + +Require Import Coqlib. +Require Import Zquot. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Cminor. +Require Import Op. +Require Import CminorSel. +Require Import SelectOp. +Require Import SelectOpproof. +Require Import SelectDiv. + +Open Local Scope cminorsel_scope. + +(** * Main approximation theorems *) + +Section Z_DIV_MUL. + +Variable N: Z. (**r number of relevant bits *) +Hypothesis N_pos: N >= 0. +Variable d: Z. (**r divisor *) +Hypothesis d_pos: d > 0. + +(** This is theorem 4.2 from Granlund and Montgomery, PLDI 1994. *) + +Lemma Zdiv_mul_pos: + forall m l, + l >= 0 -> + two_p (N+l) <= m * d <= two_p (N+l) + two_p l -> + forall n, + 0 <= n < two_p N -> + Zdiv n d = Zdiv (m * n) (two_p (N + l)). +Proof. + intros m l l_pos [LO HI] n RANGE. + exploit (Z_div_mod_eq n d). auto. + set (q := n / d). + set (r := n mod d). + intro EUCL. + assert (0 <= r <= d - 1). + unfold r. generalize (Z_mod_lt n d d_pos). omega. + assert (0 <= m). + apply Zmult_le_0_reg_r with d. auto. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + set (k := m * d - two_p (N + l)). + assert (0 <= k <= two_p l). + unfold k; omega. + assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). + unfold k. rewrite EUCL. ring. + assert (0 <= k * n). + apply Zmult_le_0_compat; omega. + assert (k * n <= two_p (N + l) - two_p l). + apply Zle_trans with (two_p l * n). + apply Zmult_le_compat_r. omega. omega. + replace (N + l) with (l + N) by omega. + rewrite two_p_is_exp. + replace (two_p l * two_p N - two_p l) + with (two_p l * (two_p N - 1)) + by ring. + apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. + omega. omega. + assert (0 <= two_p (N + l) * r). + apply Zmult_le_0_compat. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + omega. + assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). + replace (two_p (N + l) * d - two_p (N + l)) + with (two_p (N + l) * (d - 1)) by ring. + apply Zmult_le_compat_l. + omega. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + assert (0 <= m * n - two_p (N + l) * q). + apply Zmult_le_reg_r with d. auto. + replace (0 * d) with 0 by ring. rewrite H2. omega. + assert (m * n - two_p (N + l) * q < two_p (N + l)). + apply Zmult_lt_reg_r with d. omega. + rewrite H2. + apply Zle_lt_trans with (two_p (N + l) * d - two_p l). + omega. + exploit (two_p_gt_ZERO l). omega. omega. + symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q). + ring. omega. +Qed. + +Lemma Zdiv_unique_2: + forall x y q, y > 0 -> 0 < y * q - x <= y -> Zdiv x y = q - 1. +Proof. + intros. apply Zdiv_unique with (x - (q - 1) * y). ring. + replace ((q - 1) * y) with (y * q - y) by ring. omega. +Qed. + +Lemma Zdiv_mul_opp: + forall m l, + l >= 0 -> + two_p (N+l) < m * d <= two_p (N+l) + two_p l -> + forall n, + 0 < n <= two_p N -> + Zdiv n d = - Zdiv (m * (-n)) (two_p (N + l)) - 1. +Proof. + intros m l l_pos [LO HI] n RANGE. + replace (m * (-n)) with (- (m * n)) by ring. + exploit (Z_div_mod_eq n d). auto. + set (q := n / d). + set (r := n mod d). + intro EUCL. + assert (0 <= r <= d - 1). + unfold r. generalize (Z_mod_lt n d d_pos). omega. + assert (0 <= m). + apply Zmult_le_0_reg_r with d. auto. + exploit (two_p_gt_ZERO (N + l)). omega. omega. + cut (Zdiv (- (m * n)) (two_p (N + l)) = -q - 1). + omega. + apply Zdiv_unique_2. + apply two_p_gt_ZERO. omega. + replace (two_p (N + l) * - q - - (m * n)) + with (m * n - two_p (N + l) * q) + by ring. + set (k := m * d - two_p (N + l)). + assert (0 < k <= two_p l). + unfold k; omega. + assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r). + unfold k. rewrite EUCL. ring. + split. + apply Zmult_lt_reg_r with d. omega. + replace (0 * d) with 0 by omega. + rewrite H2. + assert (0 < k * n). apply Zmult_lt_0_compat; omega. + assert (0 <= two_p (N + l) * r). + apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)); omega. omega. + omega. + apply Zmult_le_reg_r with d. omega. + rewrite H2. + assert (k * n <= two_p (N + l)). + rewrite Zplus_comm. rewrite two_p_is_exp; try omega. + apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega. + apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega. + assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)). + replace (two_p (N + l) * d - two_p (N + l)) + with (two_p (N + l) * (d - 1)) + by ring. + apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO (N + l)). omega. omega. + omega. +Qed. + +(** This is theorem 5.1 from Granlund and Montgomery, PLDI 1994. *) + +Lemma Zquot_mul: + forall m l, + l >= 0 -> + two_p (N+l) < m * d <= two_p (N+l) + two_p l -> + forall n, + - two_p N <= n < two_p N -> + Z.quot n d = Zdiv (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0). +Proof. + intros. destruct (zlt n 0). + exploit (Zdiv_mul_opp m l H H0 (-n)). omega. + replace (- - n) with n by ring. + replace (Z.quot n d) with (- Z.quot (-n) d). + rewrite Zquot_Zdiv_pos by omega. omega. + rewrite Z.quot_opp_l by omega. ring. + rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega. + apply Zdiv_mul_pos; omega. +Qed. + +End Z_DIV_MUL. + +(** * Correctness of the division parameters *) + +Lemma divs_mul_params_sound: + forall d m p, + divs_mul_params d = Some(p, m) -> + 0 <= m < Int.modulus /\ 0 <= p < 32 /\ + forall n, + Int.min_signed <= n <= Int.max_signed -> + Z.quot n d = Zdiv (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0). +Proof with (try discriminate). + unfold divs_mul_params; intros d m' p' EQ. + destruct (find_div_mul_params Int.wordsize + (Int.half_modulus - Int.half_modulus mod d - 1) d 32) + as [[p m] | ]... + destruct (zlt 0 d)... + destruct (zlt (two_p (32 + p)) (m * d))... + destruct (zle (m * d) (two_p (32 + p) + two_p (p + 1)))... + destruct (zle 0 m)... + destruct (zlt m Int.modulus)... + destruct (zle 0 p)... + destruct (zlt p 32)... + simpl in EQ. inv EQ. + split. auto. split. auto. intros. + replace (32 + p') with (31 + (p' + 1)) by omega. + apply Zquot_mul; try omega. + replace (31 + (p' + 1)) with (32 + p') by omega. omega. + change (Int.min_signed <= n < Int.half_modulus). + unfold Int.max_signed in H. omega. +Qed. + +Lemma divu_mul_params_sound: + forall d m p, + divu_mul_params d = Some(p, m) -> + 0 <= m < Int.modulus /\ 0 <= p < 32 /\ + forall n, + 0 <= n < Int.modulus -> + Zdiv n d = Zdiv (m * n) (two_p (32 + p)). +Proof with (try discriminate). + unfold divu_mul_params; intros d m' p' EQ. + destruct (find_div_mul_params Int.wordsize + (Int.modulus - Int.modulus mod d - 1) d 32) + as [[p m] | ]... + destruct (zlt 0 d)... + destruct (zle (two_p (32 + p)) (m * d))... + destruct (zle (m * d) (two_p (32 + p) + two_p p))... + destruct (zle 0 m)... + destruct (zlt m Int.modulus)... + destruct (zle 0 p)... + destruct (zlt p 32)... + simpl in EQ. inv EQ. + split. auto. split. auto. intros. + apply Zdiv_mul_pos; try omega. assumption. +Qed. + +Lemma divs_mul_shift_gen: + forall x y m p, + divs_mul_params (Int.signed y) = Some(p, m) -> + 0 <= m < Int.modulus /\ 0 <= p < 32 /\ + Int.divs x y = Int.add (Int.shr (Int.repr ((Int.signed x * m) / Int.modulus)) (Int.repr p)) + (Int.shru x (Int.repr 31)). +Proof. + intros. set (n := Int.signed x). set (d := Int.signed y) in *. + exploit divs_mul_params_sound; eauto. intros (A & B & C). + split. auto. split. auto. + unfold Int.divs. fold n; fold d. rewrite C by (apply Int.signed_range). + rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv. + rewrite Int.shru_lt_zero. unfold Int.add. apply Int.eqm_samerepr. apply Int.eqm_add. + rewrite Int.shr_div_two_p. apply Int.eqm_unsigned_repr_r. apply Int.eqm_refl2. + rewrite Int.unsigned_repr. f_equal. + rewrite Int.signed_repr. rewrite Int.modulus_power. f_equal. ring. + cut (Int.min_signed <= n * m / Int.modulus < Int.half_modulus). + unfold Int.max_signed; omega. + apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos. + apply Int.modulus_pos. + split. apply Zle_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega. + apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto. + apply Zle_lt_trans with (Int.half_modulus * m). + apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto. + apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto. + assert (32 < Int.max_unsigned) by (compute; auto). omega. + unfold Int.lt; fold n. rewrite Int.signed_zero. destruct (zlt n 0); apply Int.eqm_unsigned_repr. + apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. omega. +Qed. + +Theorem divs_mul_shift_1: + forall x y m p, + divs_mul_params (Int.signed y) = Some(p, m) -> + m < Int.half_modulus -> + 0 <= p < 32 /\ + Int.divs x y = Int.add (Int.shr (Int.mulhs x (Int.repr m)) (Int.repr p)) + (Int.shru x (Int.repr 31)). +Proof. + intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). + intros (A & B & C). split. auto. rewrite C. + unfold Int.mulhs. rewrite Int.signed_repr. auto. + generalize Int.min_signed_neg; unfold Int.max_signed; omega. +Qed. + +Theorem divs_mul_shift_2: + forall x y m p, + divs_mul_params (Int.signed y) = Some(p, m) -> + m >= Int.half_modulus -> + 0 <= p < 32 /\ + Int.divs x y = Int.add (Int.shr (Int.add (Int.mulhs x (Int.repr m)) x) (Int.repr p)) + (Int.shru x (Int.repr 31)). +Proof. + intros. exploit divs_mul_shift_gen; eauto. instantiate (1 := x). + intros (A & B & C). split. auto. rewrite C. f_equal. f_equal. + rewrite Int.add_signed. unfold Int.mulhs. set (n := Int.signed x). + transitivity (Int.repr (n * (m - Int.modulus) / Int.modulus + n)). + f_equal. + replace (n * (m - Int.modulus)) with (n * m + (-n) * Int.modulus) by ring. + rewrite Z_div_plus. ring. apply Int.modulus_pos. + apply Int.eqm_samerepr. apply Int.eqm_add; auto with ints. + apply Int.eqm_sym. eapply Int.eqm_trans. apply Int.eqm_signed_unsigned. + apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl2. f_equal. f_equal. + rewrite Int.signed_repr_eq. rewrite Zmod_small by assumption. + apply zlt_false. omega. +Qed. + +Theorem divu_mul_shift: + forall x y m p, + divu_mul_params (Int.unsigned y) = Some(p, m) -> + 0 <= p < 32 /\ + Int.divu x y = Int.shru (Int.mulhu x (Int.repr m)) (Int.repr p). +Proof. + intros. exploit divu_mul_params_sound; eauto. intros (A & B & C). + split. auto. + rewrite Int.shru_div_two_p. rewrite Int.unsigned_repr. + unfold Int.divu, Int.mulhu. f_equal. rewrite C by apply Int.unsigned_range. + rewrite two_p_is_exp by omega. rewrite <- Zdiv_Zdiv by (apply two_p_gt_ZERO; omega). + f_equal. rewrite (Int.unsigned_repr m). + rewrite Int.unsigned_repr. f_equal. ring. + cut (0 <= Int.unsigned x * m / Int.modulus < Int.modulus). + unfold Int.max_unsigned; omega. + apply Zdiv_interval_1. omega. compute; auto. compute; auto. + split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega. + apply Zle_lt_trans with (Int.modulus * m). + apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega. + apply Zmult_lt_compat_l. compute; auto. omega. + unfold Int.max_unsigned; omega. + assert (32 < Int.max_unsigned) by (compute; auto). omega. +Qed. + +(** * Correctness of the smart constructors for division and modulus *) + +Section CMCONSTRS. + +Variable ge: genv. +Variable sp: val. +Variable e: env. +Variable m: mem. + +Lemma eval_divu_mul: + forall le x y p M, + divu_mul_params (Int.unsigned y) = Some(p, M) -> + nth_error le O = Some (Vint x) -> + eval_expr ge sp e m le (divu_mul p M) (Vint (Int.divu x y)). +Proof. + intros. unfold divu_mul. exploit (divu_mul_shift x); eauto. intros [A B]. + assert (eval_expr ge sp e m le + (Eop Omulhu (Eletvar 0 ::: Eop (Ointconst (Int.repr M)) Enil ::: Enil)) + (Vint (Int.mulhu x (Int.repr M)))). + { EvalOp. econstructor. econstructor; eauto. econstructor. EvalOp. simpl; reflexivity. constructor. + auto. } + exploit eval_shruimm. eexact H1. instantiate (1 := Int.repr p). + intros [v [P Q]]. simpl in Q. + replace (Int.ltu (Int.repr p) Int.iwordsize) with true in Q. + inv Q. rewrite B. auto. + unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true; auto. tauto. + assert (32 < Int.max_unsigned) by (compute; auto). omega. +Qed. + +Theorem eval_divuimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.divu x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (divuimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold divuimm; intros. generalize H0; intros DIV. + destruct x; simpl in DIV; try discriminate. + destruct (Int.eq n2 Int.zero) eqn:Z2; inv DIV. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- erewrite Int.divu_pow2 by eauto. + replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). + apply eval_shruimm; auto. + simpl. erewrite Int.is_power2_range; eauto. +- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + + exists (Vint (Int.divu i n2)); split; auto. + econstructor; eauto. eapply eval_divu_mul; eauto. + + eapply eval_divu_base; eauto. EvalOp. +Qed. + +Theorem eval_divu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divu x y = Some z -> + exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v. +Proof. + unfold divu; intros until b. destruct (divu_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_divuimm; eauto. +- eapply eval_divu_base; eauto. +Qed. + +Lemma eval_mod_from_div: + forall le a n x y, + eval_expr ge sp e m le a (Vint y) -> + nth_error le O = Some (Vint x) -> + eval_expr ge sp e m le (mod_from_div a n) (Vint (Int.sub x (Int.mul y n))). +Proof. + unfold mod_from_div; intros. + exploit eval_mulimm; eauto. instantiate (1 := n). intros [v [A B]]. + simpl in B. inv B. EvalOp. +Qed. + +Theorem eval_moduimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.modu x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (moduimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold moduimm; intros. generalize H0; intros MOD. + destruct x; simpl in MOD; try discriminate. + destruct (Int.eq n2 Int.zero) eqn:Z2; inv MOD. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- erewrite Int.modu_and by eauto. + change (Vint (Int.and i (Int.sub n2 Int.one))) + with (Val.and (Vint i) (Vint (Int.sub n2 Int.one))). + apply eval_andimm. auto. +- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + + econstructor; split. + econstructor; eauto. eapply eval_mod_from_div. + eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. + rewrite Int.modu_divu. auto. + red; intros; subst n2; discriminate. + + eapply eval_modu_base; eauto. EvalOp. +Qed. + +Theorem eval_modu: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.modu x y = Some z -> + exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v. +Proof. + unfold modu; intros until b. destruct (modu_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_moduimm; eauto. +- eapply eval_modu_base; eauto. +Qed. + +Lemma eval_divs_mul: + forall le x y p M, + divs_mul_params (Int.signed y) = Some(p, M) -> + nth_error le O = Some (Vint x) -> + eval_expr ge sp e m le (divs_mul p M) (Vint (Int.divs x y)). +Proof. + intros. unfold divs_mul. + assert (V: eval_expr ge sp e m le (Eletvar O) (Vint x)). + { constructor; auto. } + assert (X: eval_expr ge sp e m le + (Eop Omulhs (Eletvar 0 ::: Eop (Ointconst (Int.repr M)) Enil ::: Enil)) + (Vint (Int.mulhs x (Int.repr M)))). + { EvalOp. econstructor. eauto. econstructor. EvalOp. simpl; reflexivity. constructor. + auto. } + exploit eval_shruimm. eexact V. instantiate (1 := Int.repr (Int.zwordsize - 1)). + intros [v1 [Y LD]]. simpl in LD. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. + simpl in LD. inv LD. + assert (RANGE: 0 <= p < 32 -> Int.ltu (Int.repr p) Int.iwordsize = true). + { intros. unfold Int.ltu. rewrite Int.unsigned_repr. rewrite zlt_true by tauto. auto. + assert (32 < Int.max_unsigned) by (compute; auto). omega. } + destruct (zlt M Int.half_modulus). +- exploit (divs_mul_shift_1 x); eauto. intros [A B]. + exploit eval_shrimm. eexact X. instantiate (1 := Int.repr p). intros [v1 [Z LD]]. + simpl in LD. rewrite RANGE in LD by auto. inv LD. + exploit eval_add. eexact Z. eexact Y. intros [v1 [W LD]]. + simpl in LD. inv LD. + rewrite B. exact W. +- exploit (divs_mul_shift_2 x); eauto. intros [A B]. + exploit eval_add. eexact X. eexact V. intros [v1 [Z LD]]. + simpl in LD. inv LD. + exploit eval_shrimm. eexact Z. instantiate (1 := Int.repr p). intros [v1 [U LD]]. + simpl in LD. rewrite RANGE in LD by auto. inv LD. + exploit eval_add. eexact U. eexact Y. intros [v1 [W LD]]. + simpl in LD. inv LD. + rewrite B. exact W. +Qed. + +Theorem eval_divsimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.divs x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (divsimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold divsimm; intros. generalize H0; intros DIV. + destruct x; simpl in DIV; try discriminate. + destruct (Int.eq n2 Int.zero + || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto. + + eapply eval_divs_base; eauto. EvalOp. +- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + exists (Vint (Int.divs i n2)); split; auto. + econstructor; eauto. eapply eval_divs_mul; eauto. + + eapply eval_divs_base; eauto. EvalOp. +Qed. + +Theorem eval_divs: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divs x y = Some z -> + exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v. +Proof. + unfold divs; intros until b. destruct (divs_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_divsimm; eauto. +- eapply eval_divs_base; eauto. +Qed. + +Theorem eval_modsimm: + forall le e1 x n2 z, + eval_expr ge sp e m le e1 x -> + Val.mods x (Vint n2) = Some z -> + exists v, eval_expr ge sp e m le (modsimm e1 n2) v /\ Val.lessdef z v. +Proof. + unfold modsimm; intros. + exploit Val.mods_divs; eauto. intros [y [A B]]. + generalize A; intros DIV. + destruct x; simpl in DIV; try discriminate. + destruct (Int.eq n2 Int.zero + || Int.eq i (Int.repr Int.min_signed) && Int.eq n2 Int.mone) eqn:Z2; inv DIV. + destruct (Int.is_power2 n2) as [l | ] eqn:P2. +- destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + + exploit (eval_shrximm ge sp e m (Vint i :: le) (Eletvar O)). + constructor. simpl; eauto. eapply Val.divs_pow2; eauto. + intros [v1 [X LD]]. inv LD. + econstructor; split. econstructor. eauto. + apply eval_mod_from_div. eexact X. simpl; eauto. + simpl. auto. + + eapply eval_mods_base; eauto. EvalOp. +- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + + econstructor; split. + econstructor. eauto. apply eval_mod_from_div with (x := i); auto. + eapply eval_divs_mul with (x := i); eauto. + simpl. auto. + + eapply eval_mods_base; eauto. EvalOp. +Qed. + +Theorem eval_mods: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.mods x y = Some z -> + exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v. +Proof. + unfold mods; intros until b. destruct (mods_match b); intros. +- inv H0. inv H5. simpl in H7. inv H7. eapply eval_modsimm; eauto. +- eapply eval_mods_base; eauto. +Qed. + +End CMCONSTRS. diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v index 3978828..26f33da 100644 --- a/backend/SelectLongproof.v +++ b/backend/SelectLongproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness of instruction selection for 64-bit integer operations *) +(** Correctness of instruction selection for integer division *) Require Import Coqlib. Require Import AST. diff --git a/backend/Selection.v b/backend/Selection.v index b35c891..f62a888 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -31,6 +31,7 @@ Require Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import SelectDiv. Require Import SelectLong. Open Local Scope cminorsel_scope. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index e94f85d..c292b49 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -26,9 +26,11 @@ Require Import Cminor. Require Import Op. Require Import CminorSel. Require Import SelectOp. +Require Import SelectDiv. Require Import SelectLong. Require Import Selection. Require Import SelectOpproof. +Require Import SelectDivproof. Require Import SelectLongproof. Open Local Scope cminorsel_scope. -- cgit v1.2.3