Module SelectDiv


Instruction selection for division and modulus

Require Import Coqlib.
Require Import Compopts.
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

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 =>
      if optim_for_size tt then
        divu_base e1 (Eop (Ointconst n2) Enil)
      else
        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.

Original definition: 
Nondetfunction divu (e1: expr) (e2: expr) := 
  match e2 with
  | Eop (Ointconst n2) Enil => divuimm e1 n2
  | _ => divu_base e1 e2
  end.

Inductive divu_cases: forall (e2: expr), Type :=
  | divu_case1: forall n2, divu_cases (Eop (Ointconst n2) Enil)
  | divu_default: forall (e2: expr), divu_cases e2.

Definition divu_match (e2: expr) :=
  match e2 as zz1 return divu_cases zz1 with
  | Eop (Ointconst n2) Enil => divu_case1 n2
  | e2 => divu_default e2
  end.

Definition divu (e1: expr) (e2: expr) :=
  match divu_match e2 with
  | divu_case1 n2 =>
      divuimm e1 n2
  | divu_default e2 =>
      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 =>
      if optim_for_size tt then
        modu_base e1 (Eop (Ointconst n2) Enil)
      else
        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.

Original definition: 
Nondetfunction modu (e1: expr) (e2: expr) := 
  match e2 with
  | Eop (Ointconst n2) Enil => moduimm e1 n2
  | _ => modu_base e1 e2
  end.

Inductive modu_cases: forall (e2: expr), Type :=
  | modu_case1: forall n2, modu_cases (Eop (Ointconst n2) Enil)
  | modu_default: forall (e2: expr), modu_cases e2.

Definition modu_match (e2: expr) :=
  match e2 as zz1 return modu_cases zz1 with
  | Eop (Ointconst n2) Enil => modu_case1 n2
  | e2 => modu_default e2
  end.

Definition modu (e1: expr) (e2: expr) :=
  match modu_match e2 with
  | modu_case1 n2 =>
      moduimm e1 n2
  | modu_default e2 =>
      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 =>
      if optim_for_size tt then
        divs_base e1 (Eop (Ointconst n2) Enil)
      else
        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.

Original definition: 
Nondetfunction divs (e1: expr) (e2: expr) := 
  match e2 with
  | Eop (Ointconst n2) Enil => divsimm e1 n2
  | _ => divs_base e1 e2
  end.

Inductive divs_cases: forall (e2: expr), Type :=
  | divs_case1: forall n2, divs_cases (Eop (Ointconst n2) Enil)
  | divs_default: forall (e2: expr), divs_cases e2.

Definition divs_match (e2: expr) :=
  match e2 as zz1 return divs_cases zz1 with
  | Eop (Ointconst n2) Enil => divs_case1 n2
  | e2 => divs_default e2
  end.

Definition divs (e1: expr) (e2: expr) :=
  match divs_match e2 with
  | divs_case1 n2 =>
      divsimm e1 n2
  | divs_default e2 =>
      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 =>
      if optim_for_size tt then
        mods_base e1 (Eop (Ointconst n2) Enil)
      else
        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.

Original definition: 
Nondetfunction mods (e1: expr) (e2: expr) := 
  match e2 with
  | Eop (Ointconst n2) Enil => modsimm e1 n2
  | _ => mods_base e1 e2
  end.

Inductive mods_cases: forall (e2: expr), Type :=
  | mods_case1: forall n2, mods_cases (Eop (Ointconst n2) Enil)
  | mods_default: forall (e2: expr), mods_cases e2.

Definition mods_match (e2: expr) :=
  match e2 as zz1 return mods_cases zz1 with
  | Eop (Ointconst n2) Enil => mods_case1 n2
  | e2 => mods_default e2
  end.

Definition mods (e1: expr) (e2: expr) :=
  match mods_match e2 with
  | mods_case1 n2 =>
      modsimm e1 n2
  | mods_default e2 =>
      mods_base e1 e2
  end.


Floating-point division by a constant can also be turned into a FP multiplication by the inverse constant, but only for powers of 2.

Definition divfimm (e: expr) (n: float) :=
  match Float.exact_inverse n with
  | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil)
  | None => Eop Odivf (e ::: Eop (Ofloatconst n) Enil ::: Enil)
  end.

Original definition: 
Nondetfunction divf (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Ofloatconst n2) Enil => divfimm e1 n2
  | _ => Eop Odivf (e1 ::: e2 ::: Enil)
  end.

Inductive divf_cases: forall (e2: expr), Type :=
  | divf_case1: forall n2, divf_cases (Eop (Ofloatconst n2) Enil)
  | divf_default: forall (e2: expr), divf_cases e2.

Definition divf_match (e2: expr) :=
  match e2 as zz1 return divf_cases zz1 with
  | Eop (Ofloatconst n2) Enil => divf_case1 n2
  | e2 => divf_default e2
  end.

Definition divf (e1: expr) (e2: expr) :=
  match divf_match e2 with
  | divf_case1 n2 =>
      divfimm e1 n2
  | divf_default e2 =>
      Eop Odivf (e1 ::: e2 ::: Enil)
  end.


Definition divfsimm (e: expr) (n: float32) :=
  match Float32.exact_inverse n with
  | Some n' => Eop Omulfs (e ::: Eop (Osingleconst n') Enil ::: Enil)
  | None => Eop Odivfs (e ::: Eop (Osingleconst n) Enil ::: Enil)
  end.

Original definition: 
Nondetfunction divfs (e1: expr) (e2: expr) :=
  match e2 with
  | Eop (Osingleconst n2) Enil => divfsimm e1 n2
  | _ => Eop Odivfs (e1 ::: e2 ::: Enil)
  end.

Inductive divfs_cases: forall (e2: expr), Type :=
  | divfs_case1: forall n2, divfs_cases (Eop (Osingleconst n2) Enil)
  | divfs_default: forall (e2: expr), divfs_cases e2.

Definition divfs_match (e2: expr) :=
  match e2 as zz1 return divfs_cases zz1 with
  | Eop (Osingleconst n2) Enil => divfs_case1 n2
  | e2 => divfs_default e2
  end.

Definition divfs (e1: expr) (e2: expr) :=
  match divfs_match e2 with
  | divfs_case1 n2 =>
      divfsimm e1 n2
  | divfs_default e2 =>
      Eop Odivfs (e1 ::: e2 ::: Enil)
  end.



Generated by coq2html