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
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* Justus Fasse UGA, VERIMAG *)
(* Xavier Leroy INRIA Paris-Rocquencourt *)
(* David Monniaux CNRS, VERIMAG *)
(* Cyril Six Kalray *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Require Import Recdef Coqlib Zwf Zbits.
Require Import Errors AST Integers Floats Op.
Require Import Locations Compopts.
Require Import Mach Asm Asmblock Asmblockgen Machblockgen PostpassScheduling.
Local Open Scope error_monad_scope.
(** Functions called by the Asmexpand ocaml file, inspired and adapted from Asmblockgen.v *)
Module Asmgen_expand.
(* Load immediate *)
Definition loadimm_k (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
List.fold_right (fun np k => Asm.Pmovk sz rd (fst np) (snd np) :: k) k l.
Definition loadimm_z (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
match l with
| nil => Asm.Pmovz sz rd 0 0 :: k
| (n1, p1) :: l => Asm.Pmovz sz rd n1 p1 :: loadimm_k sz rd l k
end.
Definition loadimm_n (sz: isize) (rd: ireg) (l: list (Z * Z)) (k: code) : code :=
match l with
| nil => Asm.Pmovn sz rd 0 0 :: k
| (n1, p1) :: l => Asm.Pmovn sz rd n1 p1 :: loadimm_k sz rd (negate_decomposition l) k
end.
Definition loadimm (sz: isize) (rd: ireg) (n: Z) (k: code) : code :=
let N := match sz with W => 2%nat | X => 4%nat end in
let dz := decompose_int N n 0 in
let dn := decompose_int N (Z.lnot n) 0 in
if Nat.leb (List.length dz) (List.length dn)
then loadimm_z sz rd dz k
else loadimm_n sz rd dn k.
Definition loadimm32 (rd: ireg) (n: int) (k: code) : code :=
if is_logical_imm32 n
then Asm.Porrimm W rd XZR (Int.unsigned n) :: k
else loadimm W rd (Int.unsigned n) k.
Definition loadimm64 (rd: ireg) (n: int64) (k: code) : code :=
if is_logical_imm64 n
then Asm.Porrimm X rd XZR (Int64.unsigned n) :: k
else loadimm X rd (Int64.unsigned n) k.
(* Add immediate *)
Definition addimm_aux (insn: iregsp -> iregsp -> Z -> instruction)
(rd r1: iregsp) (n: Z) (k: code) :=
let nlo := Zzero_ext 12 n in
let nhi := n - nlo in
if Z.eqb nhi 0 then
insn rd r1 nlo :: k
else if Z.eqb nlo 0 then
insn rd r1 nhi :: k
else
insn rd r1 nhi :: insn rd rd nlo :: k.
Definition addimm64 (rd r1: iregsp) (n: int64) (k: code) : code :=
let m := Int64.neg n in
if Int64.eq n (Int64.zero_ext 24 n) then
addimm_aux (Asm.Paddimm X) rd r1 (Int64.unsigned n) k
else if Int64.eq m (Int64.zero_ext 24 m) then
addimm_aux (Asm.Psubimm X) rd r1 (Int64.unsigned m) k
else if Int64.lt n Int64.zero then
loadimm64 X16 m (Asm.Psubext rd r1 X16 (EOuxtx Int.zero) :: k)
else
loadimm64 X16 n (Asm.Paddext rd r1 X16 (EOuxtx Int.zero) :: k).
(** Register-indexed stores *)
Definition indexed_memory_access (insn: Asm.addressing -> instruction)
(sz: Z) (base: iregsp) (ofs: ptrofs) (k: code) :=
let ofs := Ptrofs.to_int64 ofs in
if offset_representable sz ofs
then insn (ADimm base ofs) :: k
else loadimm64 X16 ofs (insn (ADreg base X16) :: k).
Definition storeptr (src: ireg) (base: iregsp) (ofs: ptrofs) (k: code) :=
indexed_memory_access (Asm.Pstrx src) 8 base ofs k.
End Asmgen_expand.
(** * Translation from Asmblock to assembly language
Inspired from the KVX backend (see kvx/Asm.v and kvx/Asmgen.v) *)
Module Asmblock_TRANSF.
(* STUB *)
Definition ireg_of_preg (p : Asm.preg) : res ireg :=
match p with
| DR (IR (RR1 r)) => OK r
| _ => Error (msg "Asmgen.ireg_of_preg")
end.
Definition freg_of_preg (p : Asm.preg) : res freg :=
match p with
| DR (FR r) => OK r
| _ => Error (msg "Asmgen.freg_of_preg")
end.
Definition iregsp_of_preg (p : Asm.preg) : res iregsp :=
match p with
| DR (IR r) => OK r
| _ => Error (msg "Asmgen.iregsp_of_preg")
end.
Definition basic_to_instruction (b: basic) : res Asm.instruction :=
match b with
(* Aithmetic instructions *)
| PArith (PArithP (Padrp id ofs) rd) => do rd' <- ireg_of_preg rd;
OK (Asm.Padrp rd' id ofs)
| PArith (PArithP (Pmovz sz n pos) rd) => do rd' <- ireg_of_preg rd;
OK (Asm.Pmovz sz rd' n pos)
| PArith (PArithP (Pmovn sz n pos) rd) => do rd' <- ireg_of_preg rd;
OK (Asm.Pmovn sz rd' n pos)
| PArith (PArithP (Pfmovimms f) rd) => do rd' <- freg_of_preg rd;
OK (Asm.Pfmovimms rd' f)
| PArith (PArithP (Pfmovimmd f) rd) => do rd' <- freg_of_preg rd;
OK (Asm.Pfmovimmd rd' f)
| PArith (PArithPP (Pmovk sz n pos) rd rs) =>
if (Asm.preg_eq rd rs) then (
do rd' <- ireg_of_preg rd;
OK (Asm.Pmovk sz rd' n pos)
) else
Error (msg "Asmgen.basic_to_instruction: Pmovk uses a single register as both source and target")
| PArith (PArithPP Pmov rd rs) => do rd' <- iregsp_of_preg rd;
do rs' <- iregsp_of_preg rs;
OK (Asm.Pmov rd' rs')
| PArith (PArithPP (Paddadr id ofs) rd rs) => do rd' <- ireg_of_preg rd;
do rs' <- ireg_of_preg rs;
OK (Asm.Paddadr rd' rs' id ofs)
| PArith (PArithPP (Psbfiz sz r s) rd rs) => do rd' <- ireg_of_preg rd;
do rs' <- ireg_of_preg rs;
OK (Asm.Psbfiz sz rd' rs' r s)
| PArith (PArithPP (Psbfx sz r s) rd rs) => do rd' <- ireg_of_preg rd;
do rs' <- ireg_of_preg rs;
OK (Asm.Psbfx sz rd' rs' r s)
| PArith (PArithPP (Pubfiz sz r s) rd rs) => do rd' <- ireg_of_preg rd;
do rs' <- ireg_of_preg rs;
OK (Asm.Pubfiz sz rd' rs' r s)
| PArith (PArithPP (Pubfx sz r s) rd rs) => do rd' <- ireg_of_preg rd;
do rs' <- ireg_of_preg rs;
OK (Asm.Pubfx sz rd' rs' r s)
| PArith (PArithPP Pfmov rd rs) => do rd' <- freg_of_preg rd;
do rs' <- freg_of_preg rs;
OK (Asm.Pfmov rd' rs')
| PArith (PArithPP Pfcvtds rd rs) => do rd' <- freg_of_preg rd;
do rs' <- freg_of_preg rs;
OK (Asm.Pfcvtds rd' rs')
| PArith (PArithPP Pfcvtsd rd rs) => do rd' <- freg_of_preg rd;
do rs' <- freg_of_preg rs;
OK (Asm.Pfcvtsd rd' rs')
| PArith (PArithPP (Pfabs sz) rd rs) => do rd' <- freg_of_preg rd;
do rs' <- freg_of_preg rs;
OK (Asm.Pfabs sz rd' rs')
| PArith (PArithPP (Pfneg sz) rd rs) => do rd' <- freg_of_preg rd;
do rs' <- freg_of_preg rs;
OK (Asm.Pfneg sz rd' rs')
| PArith (PArithPP (Pscvtf fsz isz) rd rs) => do rd' <- freg_of_preg rd;
do rs' <- ireg_of_preg rs;
OK (Asm.Pscvtf fsz isz rd' rs')
| PArith (PArithPP (Pucvtf fsz isz) rd rs) => do rd' <- freg_of_preg rd;
do rs' <- ireg_of_preg rs;
OK (Asm.Pucvtf fsz isz rd' rs')
| PArith (PArithPP (Pfcvtzs isz fsz) rd rs) => do rd' <- ireg_of_preg rd;
do rs' <- freg_of_preg rs;
OK (Asm.Pfcvtzs isz fsz rd' rs')
| PArith (PArithPP (Pfcvtzu isz fsz) rd rs) => do rd' <- ireg_of_preg rd;
do rs' <- freg_of_preg rs;
OK (Asm.Pfcvtzu isz fsz rd' rs')
| PArith (PArithPP (Paddimm sz n) rd rs) => do rd' <- iregsp_of_preg rd;
do rs' <- iregsp_of_preg rs;
OK (Asm.Paddimm sz rd' rs' n)
| PArith (PArithPP (Psubimm sz n) rd rs) => do rd' <- iregsp_of_preg rd;
do rs' <- iregsp_of_preg rs;
OK (Asm.Psubimm sz rd' rs' n)
| PArith (PArithPPP (Pasrv sz) rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Pasrv sz rd' r1' r2')
| PArith (PArithPPP (Plslv sz) rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Plslv sz rd' r1' r2')
| PArith (PArithPPP (Plsrv sz) rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Plsrv sz rd' r1' r2')
| PArith (PArithPPP (Prorv sz) rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Prorv sz rd' r1' r2')
| PArith (PArithPPP Psmulh rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Psmulh rd' r1' r2')
| PArith (PArithPPP Pumulh rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Pumulh rd' r1' r2')
| PArith (PArithPPP (Psdiv sz) rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Psdiv sz rd' r1' r2')
| PArith (PArithPPP (Pudiv sz) rd r1 r2) => do rd' <- ireg_of_preg rd;
do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Pudiv sz rd' r1' r2')
| PArith (PArithPPP (Paddext x) rd r1 r2) => do rd' <- iregsp_of_preg rd;
do r1' <- iregsp_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Paddext rd' r1' r2' x)
| PArith (PArithPPP (Psubext x) rd r1 r2) => do rd' <- iregsp_of_preg rd;
do r1' <- iregsp_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Psubext rd' r1' r2' x)
| PArith (PArithPPP (Pfadd sz) rd r1 r2) => do rd' <- freg_of_preg rd;
do r1' <- freg_of_preg r1;
do r2' <- freg_of_preg r2;
OK (Asm.Pfadd sz rd' r1' r2')
| PArith (PArithPPP (Pfdiv sz) rd r1 r2) => do rd' <- freg_of_preg rd;
do r1' <- freg_of_preg r1;
do r2' <- freg_of_preg r2;
OK (Asm.Pfdiv sz rd' r1' r2')
| PArith (PArithPPP (Pfmul sz) rd r1 r2) => do rd' <- freg_of_preg rd;
do r1' <- freg_of_preg r1;
do r2' <- freg_of_preg r2;
OK (Asm.Pfmul sz rd' r1' r2')
| PArith (PArithPPP (Pfsub sz) rd r1 r2) => do rd' <- freg_of_preg rd;
do r1' <- freg_of_preg r1;
do r2' <- freg_of_preg r2;
OK (Asm.Pfsub sz rd' r1' r2')
| PArith (PArithRR0 (Pandimm sz n) rd r1) => OK (Asm.Pandimm sz rd r1 n)
| PArith (PArithRR0 (Peorimm sz n) rd r1) => OK (Asm.Peorimm sz rd r1 n)
| PArith (PArithRR0 (Porrimm sz n) rd r1) => OK (Asm.Porrimm sz rd r1 n)
| PArith (PArithRR0R (Padd sz s) rd r1 r2) => OK (Asm.Padd sz rd r1 r2 s)
| PArith (PArithRR0R (Psub sz s) rd r1 r2) => OK (Asm.Psub sz rd r1 r2 s)
| PArith (PArithRR0R (Pand sz s) rd r1 r2) => OK (Asm.Pand sz rd r1 r2 s)
| PArith (PArithRR0R (Pbic sz s) rd r1 r2) => OK (Asm.Pbic sz rd r1 r2 s)
| PArith (PArithRR0R (Peon sz s) rd r1 r2) => OK (Asm.Peon sz rd r1 r2 s)
| PArith (PArithRR0R (Peor sz s) rd r1 r2) => OK (Asm.Peor sz rd r1 r2 s)
| PArith (PArithRR0R (Porr sz s) rd r1 r2) => OK (Asm.Porr sz rd r1 r2 s)
| PArith (PArithRR0R (Porn sz s) rd r1 r2) => OK (Asm.Porn sz rd r1 r2 s)
| PArith (PArithARRRR0 (Pmadd sz) rd r1 r2 r3) => OK (Asm.Pmadd sz rd r1 r2 r3)
| PArith (PArithARRRR0 (Pmsub sz) rd r1 r2 r3) => OK (Asm.Pmsub sz rd r1 r2 r3)
| PArith (PArithComparisonPP (Pcmpext x) r1 r2) => do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Pcmpext r1' r2' x)
| PArith (PArithComparisonPP (Pcmnext x) r1 r2) => do r1' <- ireg_of_preg r1;
do r2' <- ireg_of_preg r2;
OK (Asm.Pcmnext r1' r2' x)
| PArith (PArithComparisonPP (Pfcmp sz) r1 r2) => do r1' <- freg_of_preg r1;
do r2' <- freg_of_preg r2;
OK (Asm.Pfcmp sz r1' r2')
| PArith (PArithComparisonR0R (Pcmp is s) r1 r2) => OK (Asm.Pcmp is r1 r2 s)
| PArith (PArithComparisonR0R (Pcmn is s) r1 r2) => OK (Asm.Pcmn is r1 r2 s)
| PArith (PArithComparisonR0R (Ptst is s) r1 r2) => OK (Asm.Ptst is r1 r2 s)
| PArith (PArithComparisonP (Pcmpimm sz n) r1) => do r1' <- ireg_of_preg r1;
OK (Asm.Pcmpimm sz r1' n)
| PArith (PArithComparisonP (Pcmnimm sz n) r1) => do r1' <- ireg_of_preg r1;
OK (Asm.Pcmnimm sz r1' n)
| PArith (PArithComparisonP (Ptstimm sz n) r1) => do r1' <- ireg_of_preg r1;
OK (Asm.Ptstimm sz r1' n)
| PArith (PArithComparisonP (Pfcmp0 sz) r1) => do r1' <- freg_of_preg r1;
OK (Asm.Pfcmp0 sz r1')
| PArith (Pcset rd c) => OK (Asm.Pcset rd c)
| PArith (Pfmovi fsz rd r1) => OK (Asm.Pfmovi fsz rd r1)
| PArith (Pcsel rd r1 r2 c) =>
match r1, r2 with
| IR r1', IR r2' => do rd' <- ireg_of_preg rd;
do r1'' <- ireg_of_preg r1';
do r2'' <- ireg_of_preg r2';
OK (Asm.Pcsel rd' r1'' r2'' c)
| FR r1', FR r2' => do rd' <- freg_of_preg rd;
do r1'' <- freg_of_preg r1';
do r2'' <- freg_of_preg r2';
OK (Asm.Pfsel rd' r1'' r2'' c)
| _, _ => Error (msg "Asmgen.basic_to_instruction: Pcsel is only defind on iregs and fregs.")
end
| PArith (Pfnmul fsz rd r1 r2) => OK (Asm.Pfnmul fsz rd r1 r2)
| PLoad (PLd_rd_a Pldrw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw rd' a)
| PLoad (PLd_rd_a Pldrw_a rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrw_a rd' a)
| PLoad (PLd_rd_a Pldrx rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx rd' a)
| PLoad (PLd_rd_a Pldrx_a rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrx_a rd' a)
| PLoad (PLd_rd_a (Pldrb sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrb sz rd' a)
| PLoad (PLd_rd_a (Pldrsb sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsb sz rd' a)
| PLoad (PLd_rd_a (Pldrh sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrh sz rd' a)
| PLoad (PLd_rd_a (Pldrsh sz) rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsh sz rd' a)
| PLoad (PLd_rd_a Pldrzw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrzw rd' a)
| PLoad (PLd_rd_a Pldrsw rd a) => do rd' <- ireg_of_preg rd; OK (Asm.Pldrsw rd' a)
| PLoad (PLd_rd_a Pldrs rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrs rd' a)
| PLoad (PLd_rd_a Pldrd rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrd rd' a)
| PLoad (PLd_rd_a Pldrd_a rd a) => do rd' <- freg_of_preg rd; OK (Asm.Pldrd_a rd' a)
| PLoad (Pldp Pldpw rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1;
do rd2' <- ireg_of_preg rd2;
OK (Asm.Pldpw rd1' rd2' chk1 chk2 a)
| PLoad (Pldp Pldpx rd1 rd2 chk1 chk2 a) => do rd1' <- ireg_of_preg rd1;
do rd2' <- ireg_of_preg rd2;
OK (Asm.Pldpx rd1' rd2' chk1 chk2 a)
| PLoad (Pldp Pldps rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1;
do rd2' <- freg_of_preg rd2;
OK (Asm.Pldps rd1' rd2' chk1 chk2 a)
| PLoad (Pldp Pldpd rd1 rd2 chk1 chk2 a) => do rd1' <- freg_of_preg rd1;
do rd2' <- freg_of_preg rd2;
OK (Asm.Pldpd rd1' rd2' chk1 chk2 a)
| PStore (PSt_rs_a Pstrw r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw r' a)
| PStore (PSt_rs_a Pstrw_a r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrw_a r' a)
| PStore (PSt_rs_a Pstrx r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrx r' a)
| PStore (PSt_rs_a Pstrx_a r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrx_a r' a)
| PStore (PSt_rs_a Pstrb r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrb r' a)
| PStore (PSt_rs_a Pstrh r a) => do r' <- ireg_of_preg r; OK (Asm.Pstrh r' a)
| PStore (PSt_rs_a Pstrs r a) => do r' <- freg_of_preg r; OK (Asm.Pstrs r' a)
| PStore (PSt_rs_a Pstrd r a) => do r' <- freg_of_preg r; OK (Asm.Pstrd r' a)
| PStore (PSt_rs_a Pstrd_a r a) => do r' <- freg_of_preg r; OK (Asm.Pstrd_a r' a)
| PStore (Pstp Pstpw rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1;
do rs2' <- ireg_of_preg rs2;
OK (Asm.Pstpw rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstpx rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1;
do rs2' <- ireg_of_preg rs2;
OK (Asm.Pstpx rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstps rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
do rs2' <- freg_of_preg rs2;
OK (Asm.Pstps rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstpd rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
do rs2' <- freg_of_preg rs2;
OK (Asm.Pstpd rs1' rs2' chk1 chk2 a)
| Pallocframe sz linkofs => OK (Asm.Pallocframe sz linkofs)
| Pfreeframe sz linkofs => OK (Asm.Pfreeframe sz linkofs)
| Ploadsymbol rd id => OK (Asm.Ploadsymbol rd id)
| Pcvtsw2x rd r1 => OK (Asm.Pcvtsw2x rd r1)
| Pcvtuw2x rd r1 => OK (Asm.Pcvtuw2x rd r1)
| Pcvtx2w rd => OK (Asm.Pcvtx2w rd)
| Pnop => OK (Asm.Pnop)
end.
Definition cf_instruction_to_instruction (cfi: cf_instruction) : Asm.instruction :=
match cfi with
| Pb l => Asm.Pb l
| Pbc c lbl => Asm.Pbc c lbl
| Pbl id sg => Asm.Pbl id sg
| Pbs id sg => Asm.Pbs id sg
| Pblr r sg => Asm.Pblr r sg
| Pbr r sg => Asm.Pbr r sg
| Pret r => Asm.Pret r
| Pcbnz sz r lbl => Asm.Pcbnz sz r lbl
| Pcbz sz r lbl => Asm.Pcbz sz r lbl
| Ptbnz sz r n lbl => Asm.Ptbnz sz r n lbl
| Ptbz sz r n lbl => Asm.Ptbz sz r n lbl
| Pbtbl r1 tbl => Asm.Pbtbl r1 tbl
end.
Definition control_to_instruction (c: control) :=
match c with
| PCtlFlow i => cf_instruction_to_instruction i
| Pbuiltin ef args res => Asm.Pbuiltin ef (List.map (map_builtin_arg DR) args) (map_builtin_res DR res)
end.
Fixpoint unfold_label (ll: list label) :=
match ll with
| nil => nil
| l :: ll => Plabel l :: unfold_label ll
end.
Fixpoint unfold_body (lb: list basic) : res Asm.code :=
match lb with
| nil => OK nil
| b :: lb =>
(* x_is: x's instructions *)
do b_is <- basic_to_instruction b;
do lb_is <- unfold_body lb;
OK (b_is :: lb_is)
end.
Definition unfold_exit (oc: option control) :=
match oc with
| None => nil
| Some c => control_to_instruction c :: nil
end.
Definition unfold_bblock (bb: bblock) :=
let lbl := unfold_label (header bb) in
(*
* With this dynamically checked assumption on a previous optimization we
* can show that [Asmblock.label_pos] and [Asm.label_pos] retrieve the same
* exact address. Maintaining this property allows us to use the simple
* formulation of match_states defined as equality.
* Otherwise we would have to deal with the case of a basic block header
* that has multiple labels. Asmblock.label_pos will, for all labels, point
* to the same location at the beginning of the basic block. Asm.label_pos
* on the other hand could return a position pointing into the original
* basic block.
*)
if zle (list_length_z (header bb)) 1 then
do bo_is <- unfold_body (body bb);
OK (lbl ++ bo_is ++ unfold_exit (exit bb))
else
Error (msg "Asmgen.unfold_bblock: Multiple labels were generated.").
Fixpoint unfold (bbs: Asmblock.bblocks) : res Asm.code :=
match bbs with
| nil => OK (nil)
| bb :: bbs' =>
do bb_is <- unfold_bblock bb;
do bbs'_is <- unfold bbs';
OK (bb_is ++ bbs'_is)
end.
Definition transf_function (f: Asmblock.function) : res Asm.function :=
do c <- unfold (Asmblock.fn_blocks f);
if zlt Ptrofs.max_unsigned (list_length_z c)
then Error (msg "Asmgen.trans_function: code size exceeded")
else OK {| Asm.fn_sig := Asmblock.fn_sig f; Asm.fn_code := c |}.
Definition transf_fundef (f: Asmblock.fundef) : res Asm.fundef :=
transf_partial_fundef transf_function f.
Definition transf_program (p: Asmblock.program) : res Asm.program :=
transform_partial_program transf_fundef p.
End Asmblock_TRANSF.
Definition transf_program (p: Mach.program) : res Asm.program :=
let mbp := Machblockgen.transf_program p in
do abp <- Asmblockgen.transf_program mbp;
do abp' <- (time "PostpassScheduling total oracle+verification" PostpassScheduling.transf_program) abp;
Asmblock_TRANSF.transf_program abp'.
|
