1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
|
(* *********************************************************************)
(* *)
(* 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 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
- 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 =>
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.
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 =>
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.
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 =>
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.
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 =>
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.
Nondetfunction mods (e1: expr) (e2: expr) :=
match e2 with
| Eop (Ointconst n2) Enil => modsimm e1 n2
| _ => 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.
Nondetfunction divf (e1: expr) (e2: expr) :=
match e2 with
| Eop (Ofloatconst n2) Enil => divfimm e1 n2
| _ => 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.
Nondetfunction divfs (e1: expr) (e2: expr) :=
match e2 with
| Eop (Osingleconst n2) Enil => divfsimm e1 n2
| _ => Eop Odivfs (e1 ::: e2 ::: Enil)
end.
|
