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
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(* FIXME: expected branching information not propagated *)
(** Instruction selection for 64-bit integer operations *)
Require String.
Require Import Coqlib.
Require Import AST Integers Floats.
Require Import Op CminorSel.
Require Import OpHelpers.
Require Import SelectOp.
Local Open Scope cminorsel_scope.
Local Open Scope string_scope.
Section SELECT.
Context {hf: helper_functions}.
Definition makelong (h l: expr): expr :=
Eop Omakelong (h ::: l ::: Enil).
Nondetfunction splitlong (e: expr) (f: expr -> expr -> expr) :=
match e with
| Eop Omakelong (h ::: l ::: Enil) => f h l
| _ => Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
end.
Nondetfunction splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) :=
match e1, e2 with
| Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) =>
f h1 l1 h2 l2
| Eop Omakelong (h1 ::: l1 ::: Enil), t2 =>
Elet t2 (f (lift h1) (lift l1)
(Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
| t1, Eop Omakelong (h2 ::: l2 ::: Enil) =>
Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))
(lift h2) (lift l2))
| _, _ =>
Elet e1 (Elet (lift e2)
(f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil))
(Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))))
end.
Nondetfunction lowlong (e: expr) :=
match e with
| Eop Omakelong (e1 ::: e2 ::: Enil) => e2
| _ => Eop Olowlong (e ::: Enil)
end.
Nondetfunction highlong (e: expr) :=
match e with
| Eop Omakelong (e1 ::: e2 ::: Enil) => e1
| _ => Eop Ohighlong (e ::: Enil)
end.
Definition longconst (n: int64) : expr :=
makelong (Eop (Ointconst (Int64.hiword n)) Enil)
(Eop (Ointconst (Int64.loword n)) Enil).
Nondetfunction is_longconst (e: expr) :=
match e with
| Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
Some(Int64.ofwords h l)
| _ =>
None
end.
Definition is_longconst_zero (e: expr) :=
match is_longconst e with
| Some n => Int64.eq n Int64.zero
| None => false
end.
Definition intoflong (e: expr) := lowlong e.
Nondetfunction longofint (e: expr) :=
match e with
| Eop (Ointconst n) Enil => longconst (Int64.repr (Int.signed n))
| _ => Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O))
end.
Definition longofintu (e: expr) :=
makelong (Eop (Ointconst Int.zero) Enil) e.
Definition negl (e: expr) :=
match is_longconst e with
| Some n => longconst (Int64.neg n)
| None => Ebuiltin (EF_builtin "__builtin_negl" sig_l_l) (e ::: Enil)
end.
Definition notl (e: expr) :=
splitlong e (fun h l => makelong (notint h) (notint l)).
Definition longoffloat (arg: expr) :=
Eexternal i64_dtos sig_f_l (arg ::: Enil).
Definition longuoffloat (arg: expr) :=
Eexternal i64_dtou sig_f_l (arg ::: Enil).
Definition floatoflong (arg: expr) :=
Eexternal i64_stod sig_l_f (arg ::: Enil).
Definition floatoflongu (arg: expr) :=
Eexternal i64_utod sig_l_f (arg ::: Enil).
Definition longofsingle (arg: expr) :=
longoffloat (floatofsingle arg).
Definition longuofsingle (arg: expr) :=
longuoffloat (floatofsingle arg).
Definition singleoflong (arg: expr) :=
Eexternal i64_stof sig_l_s (arg ::: Enil).
Definition singleoflongu (arg: expr) :=
Eexternal i64_utof sig_l_s (arg ::: Enil).
Definition andl (e1 e2: expr) :=
splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)).
Definition orl (e1 e2: expr) :=
splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (or h1 h2) (or l1 l2)).
Definition xorl (e1 e2: expr) :=
splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (xor h1 h2) (xor l1 l2)).
Definition shllimm (e1: expr) (n: int) :=
if Int.eq n Int.zero then e1 else
if Int.ltu n Int.iwordsize then
splitlong e1 (fun h l =>
makelong (or (shlimm h n) (shruimm l (Int.sub Int.iwordsize n)))
(shlimm l n))
else if Int.ltu n Int64.iwordsize' then
makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize))
(Eop (Ointconst Int.zero) Enil)
else
Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
Definition shrluimm (e1: expr) (n: int) :=
if Int.eq n Int.zero then e1 else
if Int.ltu n Int.iwordsize then
splitlong e1 (fun h l =>
makelong (shruimm h n)
(or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n))))
else if Int.ltu n Int64.iwordsize' then
makelong (Eop (Ointconst Int.zero) Enil)
(shruimm (highlong e1) (Int.sub n Int.iwordsize))
else
Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
Definition shrlimm (e1: expr) (n: int) :=
if Int.eq n Int.zero then e1 else
if Int.ltu n Int.iwordsize then
splitlong e1 (fun h l =>
makelong (shrimm h n)
(or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n))))
else if Int.ltu n Int64.iwordsize' then
Elet (highlong e1)
(makelong (shrimm (Eletvar 0) (Int.repr 31))
(shrimm (Eletvar 0) (Int.sub n Int.iwordsize)))
else
Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
Definition is_intconst (e: expr) :=
match e with
| Eop (Ointconst n) Enil => Some n
| _ => None
end.
Definition shll (e1 e2: expr) :=
match is_intconst e2 with
| Some n => shllimm e1 n
| None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil)
end.
Definition shrlu (e1 e2: expr) :=
match is_intconst e2 with
| Some n => shrluimm e1 n
| None => Eexternal i64_shr sig_li_l (e1 ::: e2 ::: Enil)
end.
Definition shrl (e1 e2: expr) :=
match is_intconst e2 with
| Some n => shrlimm e1 n
| None => Eexternal i64_sar sig_li_l (e1 ::: e2 ::: Enil)
end.
Definition addl (e1 e2: expr) :=
let default := Ebuiltin (EF_builtin "__builtin_addl" sig_ll_l) (e1 ::: e2 ::: Enil) in
match is_longconst e1, is_longconst e2 with
| Some n1, Some n2 => longconst (Int64.add n1 n2)
| Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default
| _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default
| _, _ => default
end.
Definition subl (e1 e2: expr) :=
let default := Ebuiltin (EF_builtin "__builtin_subl" sig_ll_l) (e1 ::: e2 ::: Enil) in
match is_longconst e1, is_longconst e2 with
| Some n1, Some n2 => longconst (Int64.sub n1 n2)
| Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default
| _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default
| _, _ => default
end.
Definition mull_base (e1 e2: expr) :=
splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
Elet (Ebuiltin (EF_builtin "__builtin_mull" sig_ii_l) (l1 ::: l2 ::: Enil))
(makelong
(add (add (Eop Ohighlong (Eletvar O ::: Enil))
(mul (lift l1) (lift h2)))
(mul (lift h1) (lift l2)))
(Eop Olowlong (Eletvar O ::: Enil)))).
Definition mullimm (n: int64) (e: expr) :=
if Int64.eq n Int64.zero then longconst Int64.zero else
if Int64.eq n Int64.one then e else
match Int64.is_power2' n with
| Some l => shllimm e l
| None => mull_base e (longconst n)
end.
Definition mull (e1 e2: expr) :=
match is_longconst e1, is_longconst e2 with
| Some n1, Some n2 => longconst (Int64.mul n1 n2)
| Some n1, _ => mullimm n1 e2
| _, Some n2 => mullimm n2 e1
| _, _ => mull_base e1 e2
end.
Definition mullhu (e1: expr) (n2: int64) :=
Eexternal i64_umulh sig_ll_l (e1 ::: longconst n2 ::: Enil).
Definition mullhs (e1: expr) (n2: int64) :=
Eexternal i64_smulh sig_ll_l (e1 ::: longconst n2 ::: Enil).
Definition shrxlimm (e: expr) (n: int) :=
if Int.eq n Int.zero then e else
Elet e (shrlimm (addl (Eletvar O)
(shrluimm (shrlimm (Eletvar O) (Int.repr 63))
(Int.sub (Int.repr 64) n)))
n).
Definition divlu_base (e1 e2: expr) := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil).
Definition modlu_base (e1 e2: expr) := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil).
Definition divls_base (e1 e2: expr) := Eexternal i64_sdiv sig_ll_l (e1 ::: e2 ::: Enil).
Definition modls_base (e1 e2: expr) := Eexternal i64_smod sig_ll_l (e1 ::: e2 ::: Enil).
Definition cmpl_eq_zero (e: expr) :=
splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)).
Definition cmpl_ne_zero (e: expr) :=
splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)).
Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) :=
splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil))
(Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
(Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))).
Definition cmplu (c: comparison) (e1 e2: expr) :=
match c with
| Ceq =>
cmpl_eq_zero (xorl e1 e2)
| Cne =>
cmpl_ne_zero (xorl e1 e2)
| Clt =>
cmplu_gen Clt Clt e1 e2
| Cle =>
cmplu_gen Clt Cle e1 e2
| Cgt =>
cmplu_gen Cgt Cgt e1 e2
| Cge =>
cmplu_gen Cgt Cge e1 e2
end.
Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) :=
splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
Econdition (CEcond (Ccomp Ceq) None (h1:::h2:::Enil))
(Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
(Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))).
Definition cmpl (c: comparison) (e1 e2: expr) :=
match c with
| Ceq =>
cmpl_eq_zero (xorl e1 e2)
(*
(if is_longconst_zero e2 then e1
else if is_longconst_zero e1 then e2
else xorl e1 e2) *)
| Cne =>
cmpl_ne_zero (xorl e1 e2)
(* (if is_longconst_zero e2 then e1
else if is_longconst_zero e1 then e2
else xorl e1 e2) *)
| Clt =>
if is_longconst_zero e2
then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil)
else cmpl_gen Clt Clt e1 e2
| Cle =>
cmpl_gen Clt Cle e1 e2
| Cgt =>
cmpl_gen Cgt Cgt e1 e2
| Cge =>
if is_longconst_zero e2
then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil)
else cmpl_gen Cgt Cge e1 e2
end.
End SELECT.
|
