# Module SelectDiv

Instruction selection for division and modulus

Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel SelectOp SplitLong SelectLong.

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, (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) =>
let p := p - 32 in
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) =>
let p := p - 32 in
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 divls_mul_params (d: Z) : option (Z * Z) :=
match find_div_mul_params
Int64.wordsize
(Int64.half_modulus - Int64.half_modulus mod d - 1)
d 64 with
| None => None
| Some(p, m) =>
let p := p - 64 in
if zlt 0 d
&& zlt (two_p (64 + p)) (m * d)
&& zle (m * d) (two_p (64 + p) + two_p (p + 1))
&& zle 0 m && zlt m Int64.modulus
&& zle 0 p && zlt p 64
then Some(p, m) else None
end.

Definition divlu_mul_params (d: Z) : option (Z * Z) :=
match find_div_mul_params
Int64.wordsize
(Int64.modulus - Int64.modulus mod d - 1)
d 64 with
| None => None
| Some(p, m) =>
let p := p - 64 in
if zlt 0 d
&& zle (two_p (64 + p)) (m * d)
&& zle (m * d) (two_p (64 + p) + two_p p)
&& zle 0 m && zlt m Int64.modulus
&& zle 0 p && zlt p 64
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
(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.

64-bit integer divisions

Section SELECT.

Context {hf: helper_functions}.

Definition modl_from_divl (equo: expr) (n: int64) :=
subl (Eletvar O) (mullimm n equo).

Definition divlu_mull (p: Z) (m: Z) :=
shrluimm (mullhu (Eletvar O) (Int64.repr m)) (Int.repr p).

Definition divlu (e1 e2: expr) :=
match is_longconst e2, is_longconst e1 with
| Some n2, Some n1 => longconst (Int64.divu n1 n2)
| Some n2, _ =>
match Int64.is_power2' n2 with
| Some l => shrluimm e1 l
| None => if optim_for_size tt then
divlu_base e1 e2
else
match divlu_mul_params (Int64.unsigned n2) with
| None => divlu_base e1 e2
| Some(p, m) => Elet e1 (divlu_mull p m)
end
end
| _, _ => divlu_base e1 e2
end.

Definition modlu (e1 e2: expr) :=
match is_longconst e2, is_longconst e1 with
| Some n2, Some n1 => longconst (Int64.modu n1 n2)
| Some n2, _ =>
match Int64.is_power2 n2 with
| Some l => andl e1 (longconst (Int64.sub n2 Int64.one))
| None => if optim_for_size tt then
modlu_base e1 e2
else
match divlu_mul_params (Int64.unsigned n2) with
| None => modlu_base e1 e2
| Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2)
end
end
| _, _ => modlu_base e1 e2
end.

Definition divls_mull (p: Z) (m: Z) :=
let e2 :=
mullhs (Eletvar O) (Int64.repr m) in
let e3 :=
if zlt m Int64.half_modulus then e2 else addl e2 (Eletvar O) in
(shrluimm (Eletvar O) (Int.repr (Int64.zwordsize - 1))).

Definition divls (e1 e2: expr) :=
match is_longconst e2, is_longconst e1 with
| Some n2, Some n1 => longconst (Int64.divs n1 n2)
| Some n2, _ =>
match Int64.is_power2' n2 with
| Some l => if Int.ltu l (Int.repr 63)
then shrxlimm e1 l
else divls_base e1 e2
| None => if optim_for_size tt then
divls_base e1 e2
else
match divls_mul_params (Int64.signed n2) with
| None => divls_base e1 e2
| Some(p, m) => Elet e1 (divls_mull p m)
end
end
| _, _ => divls_base e1 e2
end.

Definition modls (e1 e2: expr) :=
match is_longconst e2, is_longconst e1 with
| Some n2, Some n1 => longconst (Int64.mods n1 n2)
| Some n2, _ =>
match Int64.is_power2' n2 with
| Some l => if Int.ltu l (Int.repr 63)
then Elet e1 (modl_from_divl (shrxlimm (Eletvar O) l) n2)
else modls_base e1 e2
| None => if optim_for_size tt then
modls_base e1 e2
else
match divls_mul_params (Int64.signed n2) with
| None => modls_base e1 e2
| Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2)
end
end
| _, _ => modls_base e1 e2
end.

End SELECT.

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.