# Module SelectDiv

Instruction selection for division and modulus

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

Local Open Scope cminorsel_scope.

Section SELECT.
Context {hf: helper_functions}.

Definition is_intconst (e: expr) : option int :=
match e with
| Eop (Ointconst n) _ => Some n
| _ => None
end.

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 (mulhu (Eletvar O) (Eop (Ointconst (Int.repr m)) 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) || negb Archi.has_mulhu 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.

Definition divu (e1: expr) (e2: expr) :=
match is_intconst e2, is_intconst e1 with
| Some n2, Some n1 =>
if Int.eq n2 Int.zero
then divu_base e1 e2
else Eop (Ointconst (Int.divu n1 n2)) Enil
| Some n2, _ => 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 =>
if optim_for_size tt || negb Archi.has_mulhu 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.

Definition modu (e1: expr) (e2: expr) :=
match is_intconst e2, is_intconst e1 with
| Some n2, Some n1 =>
if Int.eq n2 Int.zero
then modu_base e1 e2
else Eop (Ointconst (Int.modu n1 n2)) Enil
| Some n2, _ => moduimm e1 n2
| _, _ => modu_base e1 e2
end.

Definition divs_mul (p: Z) (m: Z) :=
let e2 :=
mulhs (Eletvar O) (Eop (Ointconst (Int.repr m)) 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 || negb Archi.has_mulhs 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.

Definition divs (e1: expr) (e2: expr) :=
match is_intconst e2, is_intconst e1 with
| Some n2, Some n1 =>
if Int.eq n2 Int.zero
then divs_base e1 e2
else Eop (Ointconst (Int.divs n1 n2)) Enil
| Some n2, _ => 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 =>
if optim_for_size tt || negb Archi.has_mulhs 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.

Definition mods (e1: expr) (e2: expr) :=
match is_intconst e2, is_intconst e1 with
| Some n2, Some n1 =>
if Int.eq n2 Int.zero
then mods_base e1 e2
else Eop (Ointconst (Int.mods n1 n2)) Enil
| Some n2, _ => modsimm e1 n2
| _, _ => mods_base e1 e2
end.

64-bit integer divisions

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 || negb Archi.has_mullhu 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 || negb Archi.has_mullhu 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 || negb Archi.has_mullhs 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 || negb Archi.has_mullhs 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.

Definition divu_exact_imm (e1 : expr) (n2 : int) : expr :=
let (py, oy) := Zmax_two_power (Int.unsigned n2) in
mulimm (Int.repr (multiplicative_inverse Int.modulus oy))
(shruimm e1 (Int.repr py)).

Original definition:
```Nondetfunction divu_exact (e1 : expr) (e2 : expr) :=
match e1, e2 with
| e, Eop (Ointconst n2) Enil => divu_exact_imm e n2
| _, _ => divu e1 e2
end.```

Inductive divu_exact_cases: forall (e1 : expr) (e2 : expr), Type :=
| divu_exact_case1: forall e n2, divu_exact_cases (e) (Eop (Ointconst n2) Enil)
| divu_exact_default: forall (e1 : expr) (e2 : expr), divu_exact_cases e1 e2.

Definition divu_exact_match (e1 : expr) (e2 : expr) :=
match e1 as zz1, e2 as zz2 return divu_exact_cases zz1 zz2 with
| e, Eop (Ointconst n2) Enil => divu_exact_case1 e n2
| e1, e2 => divu_exact_default e1 e2
end.

Definition divu_exact (e1 : expr) (e2 : expr) :=
match divu_exact_match e1 e2 with
| divu_exact_case1 e n2 =>
divu_exact_imm e n2
| divu_exact_default e1 e2 =>
divu e1 e2
end.

Definition divs_exact_imm (e1 : expr) (n2 : int) : expr :=
let (py, oy) := Zmax_two_power (Int.signed n2) in
mulimm (Int.repr (multiplicative_inverse Int.modulus oy))
(shrimm e1 (Int.repr py)).

Original definition:
```Nondetfunction divs_exact (e1 : expr) (e2 : expr) :=
match e1, e2 with
| e, Eop (Ointconst n2) Enil => divs_exact_imm e n2
| _, _ => divs e1 e2
end.```

Inductive divs_exact_cases: forall (e1 : expr) (e2 : expr), Type :=
| divs_exact_case1: forall e n2, divs_exact_cases (e) (Eop (Ointconst n2) Enil)
| divs_exact_default: forall (e1 : expr) (e2 : expr), divs_exact_cases e1 e2.

Definition divs_exact_match (e1 : expr) (e2 : expr) :=
match e1 as zz1, e2 as zz2 return divs_exact_cases zz1 zz2 with
| e, Eop (Ointconst n2) Enil => divs_exact_case1 e n2
| e1, e2 => divs_exact_default e1 e2
end.

Definition divs_exact (e1 : expr) (e2 : expr) :=
match divs_exact_match e1 e2 with
| divs_exact_case1 e n2 =>
divs_exact_imm e n2
| divs_exact_default e1 e2 =>
divs e1 e2
end.

Definition divlu_exact_imm (e1 : expr) (n2 : int64) : expr :=
let (py, oy) := Zmax_two_power (Int64.unsigned n2) in
mullimm (Int64.repr (multiplicative_inverse Int64.modulus oy))
(shrluimm e1 (Int.repr py)).

Definition divlu_exact (e1 : expr) (e2 : expr) :=
match is_longconst e2 with
| Some n2 => divlu_exact_imm e1 n2
| None => divlu e1 e2
end.

Definition divls_exact_imm (e1 : expr) (n2 : int64) : expr :=
let (py, oy) := Zmax_two_power (Int64.signed n2) in
mullimm (Int64.repr (multiplicative_inverse Int64.modulus oy))
(shrlimm e1 (Int.repr py)).

Definition divls_exact (e1 : expr) (e2 : expr) :=
match is_longconst e2 with
| Some n2 => divls_exact_imm e1 n2
| None => divls 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 => divf_base e (Eop (Ofloatconst n) Enil)
end.

Original definition:
```Nondetfunction divf (e1: expr) (e2: expr) :=
match e2 with
| Eop (Ofloatconst n2) Enil => divfimm e1 n2
| _ => divf_base e1 e2
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 =>
divf_base e1 e2
end.

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

Original definition:
```Nondetfunction divfs (e1: expr) (e2: expr) :=
match e2 with
| Eop (Osingleconst n2) Enil => divfsimm e1 n2
| _ => divfs_base e1 e2
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 =>
divfs_base e1 e2
end.

End SELECT.