summaryrefslogtreecommitdiff
path: root/ia32/Asmgen.v
blob: f53ec81030cbb69780d16a17762007a6370d0c7d (plain)
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
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Translation from Mach to IA32 Asm. *)

Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Mach.
Require Import Asm.

Open Local Scope string_scope.
Open Local Scope error_monad_scope.

(** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler:
- Argument and result registers are of the correct type.
- For two-address instructions, the result and the first argument
  are in the same register.  (True by construction in [RTLgen], and preserved by [Reload].)
- The first argument register is never [ECX] (a.k.a. [IT2]) nor [XMM7]
  (a.k.a [FT2]).
- The top of the floating-point stack ([ST0], a.k.a. [FP0]) can only
  appear in [mov] instructions, but never in arithmetic instructions.

All these properties are true by construction, but it is painful to track them statically.  Instead, we recheck them during code generation and fail if they do not hold.
*)

(** Extracting integer or float registers. *)

Definition ireg_of (r: mreg) : res ireg :=
  match preg_of r with IR mr => OK mr | _ => Error(msg "Asmgen.ireg_of") end.

Definition freg_of (r: mreg) : res freg :=
  match preg_of r with FR mr => OK mr | _ => Error(msg "Asmgen.freg_of") end.

(** Smart constructors for various operations. *)

Definition mk_mov (rd rs: preg) (k: code) : res code :=
  match rd, rs with
  | IR rd, IR rs => OK (Pmov_rr rd rs :: k)
  | FR rd, FR rs => OK (Pmovsd_ff rd rs :: k)
  | ST0, FR rs => OK (Pfld_f rs :: k)
  | FR rd, ST0 => OK (Pfstp_f rd :: k)
  | _, _ => Error(msg "Asmgen.mk_mov")
  end.

Definition mk_shift (shift_instr: ireg -> instruction)
                    (r1 r2: ireg) (k: code) : res code :=
  if ireg_eq r2 ECX then
    OK (shift_instr r1 :: k)
  else
    do x <- assertion (negb (ireg_eq r1 ECX));
    OK (Pmov_rr ECX r2 :: shift_instr r1 :: k).

Definition mk_div (div_instr: ireg -> instruction)
                  (r1 r2: ireg) (k: code) : res code :=
  if ireg_eq r1 EAX then
    if ireg_eq r2 EDX then
      OK (Pmov_rr ECX EDX :: div_instr ECX :: k)
    else
      OK (div_instr r2 :: k)
  else
    do x <- assertion (negb (ireg_eq r1 ECX));
    if ireg_eq r2 EAX then
      OK (Pmov_rr ECX EAX :: Pmov_rr EAX r1 ::
          div_instr ECX ::
          Pmov_rr r1 EAX :: Pmov_rr EAX ECX :: k)
    else
      OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 ::
          div_instr ECX ::
          Pmov_rr r2 ECX :: Pmov_rr r1 EAX :: Pmovd_rf EAX XMM7 :: k).

Definition mk_mod (div_instr: ireg -> instruction)
                  (r1 r2: ireg) (k: code) : res code :=
  if ireg_eq r1 EAX then
    if ireg_eq r2 EDX then
      OK (Pmov_rr ECX EDX :: div_instr ECX :: Pmov_rr EAX EDX :: k)
    else
      OK (div_instr r2 :: Pmov_rr EAX EDX :: k)
  else
    do x <- assertion (negb (ireg_eq r1 ECX));
    if ireg_eq r2 EDX then
      OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX EDX :: Pmov_rr EAX r1 ::
          div_instr ECX ::
          Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k)
    else
      OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 ::
          div_instr ECX ::
          Pmov_rr r2 ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k).

Definition mk_shrximm (r: ireg) (n: int) (k: code) : res code :=
  do x <- assertion (negb (ireg_eq r ECX));
  let p := Int.sub (Int.shl Int.one n) Int.one in
  OK (Ptest_rr r r ::
      Plea ECX (Addrmode (Some r) None (inl _ p)) ::
      Pcmov Cond_l r ECX ::
      Psar_ri r n :: k).

Definition low_ireg (r: ireg) : bool :=
  match r with
  | EAX | EBX | ECX | EDX => true
  | ESI | EDI | EBP | ESP => false
  end.

Definition mk_intconv (mk: ireg -> ireg -> instruction) (rd rs: ireg) (k: code) :=
  if low_ireg rs then
    OK (mk rd rs :: k)
  else
    OK (Pmov_rr EDX rs :: mk rd EDX :: k).

Definition addressing_mentions (addr: addrmode) (r: ireg) : bool :=
  match addr with Addrmode base displ const =>
      match base with Some r' => ireg_eq r r' | None => false end
   || match displ with Some(r', sc) => ireg_eq r r' | None => false end
  end.

Definition mk_smallstore (sto: addrmode -> ireg ->instruction) 
                         (addr: addrmode) (rs: ireg) (k: code) :=
  if low_ireg rs then
    OK (sto addr rs :: k)
  else if addressing_mentions addr ECX then
    OK (Plea ECX addr :: Pmov_rr EDX rs ::
        sto (Addrmode (Some ECX) None (inl _ Int.zero)) EDX :: k)
  else
    OK (Pmov_rr ECX rs :: sto addr ECX :: k).

(** Accessing slots in the stack frame.  *)

Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
  match ty with
  | Tint =>
      do r <- ireg_of dst;
      OK (Pmov_rm r (Addrmode (Some base) None (inl _ ofs)) :: k)
  | Tfloat =>
      match preg_of dst with
      | FR r => OK (Pmovsd_fm r (Addrmode (Some base) None (inl _ ofs)) :: k)
      | ST0  => OK (Pfld_m (Addrmode (Some base) None (inl _ ofs)) :: k)
      | _ => Error (msg "Asmgen.loadind")
      end
  end.

Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
  match ty with
  | Tint =>
      do r <- ireg_of src;
      OK (Pmov_mr (Addrmode (Some base) None (inl _ ofs)) r :: k)
  | Tfloat =>
      match preg_of src with
      | FR r => OK (Pmovsd_mf (Addrmode (Some base) None (inl _ ofs)) r :: k)
      | ST0  => OK (Pfstp_m (Addrmode (Some base) None (inl _ ofs)) :: k)
      | _ => Error (msg "Asmgen.loadind")
      end
  end.

(** Translation of addressing modes *)

Definition transl_addressing (a: addressing) (args: list mreg): res addrmode :=
  match a, args with
  | Aindexed n, a1 :: nil =>
      do r1 <- ireg_of a1; OK(Addrmode (Some r1) None (inl _ n))
  | Aindexed2 n, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK(Addrmode (Some r1) (Some(r2, Int.one)) (inl _ n))
  | Ascaled sc n, a1 :: nil =>
      do r1 <- ireg_of a1; OK(Addrmode None (Some(r1, sc)) (inl _ n))
  | Aindexed2scaled sc n, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
      OK(Addrmode (Some r1) (Some(r2, sc)) (inl _ n))
  | Aglobal id ofs, nil =>
      OK(Addrmode None None (inr _ (id, ofs)))
  | Abased id ofs, a1 :: nil =>
      do r1 <- ireg_of a1; OK(Addrmode (Some r1) None (inr _ (id, ofs)))
  | Abasedscaled sc id ofs, a1 :: nil =>
      do r1 <- ireg_of a1; OK(Addrmode None (Some(r1, sc)) (inr _ (id, ofs)))
  | Ainstack n, nil =>
      OK(Addrmode (Some ESP) None (inl _ n))
  | _, _ =>
      Error(msg "Asmgen.transl_addressing")
  end.

(** Floating-point comparison.  We swap the operands in some cases
   to simplify the handling of the unordered case. *)

Definition floatcomp (cmp: comparison) (r1 r2: freg) : instruction :=
  match cmp with
  | Clt | Cle => Pcomisd_ff r2 r1
  | Ceq | Cne | Cgt | Cge => Pcomisd_ff r1 r2
  end.

(** Translation of a condition.  Prepends to [k] the instructions
  that evaluate the condition and leave its boolean result in bits
  of the condition register. *)

Definition transl_cond
              (cond: condition) (args: list mreg) (k: code) : res code :=
  match cond, args with
  | Ccomp c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k)
  | Ccompu c, a1 :: a2 :: nil =>
      do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pcmp_rr r1 r2 :: k)
  | Ccompimm c n, a1 :: nil =>
      do r1 <- ireg_of a1; OK (Pcmp_ri r1 n :: k)
  | Ccompuimm c n, a1 :: nil =>
      do r1 <- ireg_of a1;
      OK (if Int.eq_dec n Int.zero then Ptest_rr r1 r1 :: k else Pcmp_ri r1 n :: k)
  | Ccompf cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k)
  | Cnotcompf cmp, a1 :: a2 :: nil =>
      do r1 <- freg_of a1; do r2 <- freg_of a2; OK (floatcomp cmp r1 r2 :: k)
  | Cmaskzero n, a1 :: nil =>
      do r1 <- ireg_of a1; OK (Ptest_ri r1 n :: k)
  | Cmasknotzero n, a1 :: nil =>
      do r1 <- ireg_of a1; OK (Ptest_ri r1 n :: k)
  | _, _ =>
     Error(msg "Asmgen.transl_cond")
  end.

(** What processor condition to test for a given Mach condition. *)

Definition testcond_for_signed_comparison (cmp: comparison) :=
  match cmp with
  | Ceq => Cond_e
  | Cne => Cond_ne
  | Clt => Cond_l
  | Cle => Cond_le
  | Cgt => Cond_g
  | Cge => Cond_ge
  end.

Definition testcond_for_unsigned_comparison (cmp: comparison) :=
  match cmp with
  | Ceq => Cond_e
  | Cne => Cond_ne
  | Clt => Cond_b
  | Cle => Cond_be
  | Cgt => Cond_a
  | Cge => Cond_ae
  end.

Definition testcond_for_condition (cond: condition) : testcond :=
  match cond with
  | Ccomp c => testcond_for_signed_comparison c
  | Ccompu c => testcond_for_unsigned_comparison c
  | Ccompimm c n => testcond_for_signed_comparison c
  | Ccompuimm c n => testcond_for_unsigned_comparison c
  | Ccompf c =>
      match c with
      | Ceq => Cond_enp
      | Cne => Cond_nep
      | Clt => Cond_a
      | Cle => Cond_ae
      | Cgt => Cond_a
      | Cge => Cond_ae
      end
  | Cnotcompf c =>
      match c with
      | Ceq => Cond_nep
      | Cne => Cond_enp
      | Clt => Cond_be
      | Cle => Cond_b
      | Cgt => Cond_be
      | Cge => Cond_b
      end
  | Cmaskzero n => Cond_e
  | Cmasknotzero n => Cond_ne
  end.

(** Translation of the arithmetic operation [r <- op(args)].
  The corresponding instructions are prepended to [k]. *)

Definition transl_op
             (op: operation) (args: list mreg) (res: mreg) (k: code) : Errors.res code :=
  match op, args with
  | Omove, a1 :: nil =>
      mk_mov (preg_of res) (preg_of a1) k
  | Ointconst n, nil =>
      do r <- ireg_of res; OK (Pmov_ri r n :: k)
  | Ofloatconst f, nil =>
      do r <- freg_of res; OK (Pmovsd_fi r f :: k)
  | Ocast8signed, a1 :: nil =>
      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k
  | Ocast8unsigned, a1 :: nil =>
      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovzb_rr r r1 k
  | Ocast16signed, a1 :: nil =>
      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsw_rr r r1 k
  | Ocast16unsigned, a1 :: nil =>
      do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovzw_rr r r1 k
  | Oneg, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Pneg r :: k)
  | Osub, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Psub_rr r r2 :: k)
  | Omul, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pimul_rr r r2 :: k)
  | Omulimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Pimul_ri r n :: k)
  | Odiv, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; mk_div Pidiv r r2 k
  | Odivu, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; mk_div Pdiv r r2 k
  | Omod, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; mk_mod Pidiv r r2 k
  | Omodu, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; mk_mod Pdiv r r2 k
  | Oand, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pand_rr r r2 :: k)
  | Oandimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Pand_ri r n :: k)
  | Oor, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Por_rr r r2 :: k)
  | Oorimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Por_ri r n :: k)
  | Oxor, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; OK (Pxor_rr r r2 :: k)
  | Oxorimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Pxor_ri r n :: k)
  | Oshl, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Psal_rcl r r2 k
  | Oshlimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Psal_ri r n :: k)
  | Oshr, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Psar_rcl r r2 k
  | Oshrimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Psar_ri r n :: k)
  | Oshru, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; do r2 <- ireg_of a2; mk_shift Pshr_rcl r r2 k
  | Oshruimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Pshr_ri r n :: k)
  | Oshrximm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; mk_shrximm r n k
  | Ororimm n, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- ireg_of res; OK (Pror_ri r n :: k)
  | Olea addr, _ =>
      do am <- transl_addressing addr args; do r <- ireg_of res;
      OK (Plea r am :: k)
  | Onegf, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- freg_of res; OK (Pnegd r :: k)
  | Oabsf, a1 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- freg_of res; OK (Pabsd r :: k)
  | Oaddf, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- freg_of res; do r2 <- freg_of a2; OK (Paddd_ff r r2 :: k)
  | Osubf, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- freg_of res; do r2 <- freg_of a2; OK (Psubd_ff r r2 :: k)
  | Omulf, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- freg_of res; do r2 <- freg_of a2; OK (Pmuld_ff r r2 :: k)
  | Odivf, a1 :: a2 :: nil =>
      do x <- assertion (mreg_eq a1 res);
      do r <- freg_of res; do r2 <- freg_of a2; OK (Pdivd_ff r r2 :: k)
  | Osingleoffloat, a1 :: nil =>
      do r <- freg_of res; do r1 <- freg_of a1; OK (Pcvtsd2ss_ff r r1 :: k)
  | Ointoffloat, a1 :: nil =>
      do r <- ireg_of res; do r1 <- freg_of a1; OK (Pcvttsd2si_rf r r1 :: k)
  | Ofloatofint, a1 :: nil =>
      do r <- freg_of res; do r1 <- ireg_of a1; OK (Pcvtsi2sd_fr r r1 :: k)
  | Ocmp c, args =>
      do r <- ireg_of res;
      transl_cond c args (Psetcc (testcond_for_condition c) r :: k)
  | _, _ =>
      Error(msg "Asmgen.transl_op")
  end.

(** Translation of memory loads and stores *)

Definition transl_load (chunk: memory_chunk)
                       (addr: addressing) (args: list mreg) (dest: mreg)
                       (k: code) : res code :=
  do am <- transl_addressing addr args;
  match chunk with
  | Mint8unsigned =>
      do r <- ireg_of dest; OK(Pmovzb_rm r am :: k)
  | Mint8signed =>
      do r <- ireg_of dest; OK(Pmovsb_rm r am :: k)
  | Mint16unsigned =>
      do r <- ireg_of dest; OK(Pmovzw_rm r am :: k)
  | Mint16signed =>
      do r <- ireg_of dest; OK(Pmovsw_rm r am :: k)
  | Mint32 =>
      do r <- ireg_of dest; OK(Pmov_rm r am :: k)
  | Mfloat32 =>
      do r <- freg_of dest; OK(Pcvtss2sd_fm r am :: k)
  | Mfloat64 =>
      do r <- freg_of dest; OK(Pmovsd_fm r am :: k)
  end.

Definition transl_store (chunk: memory_chunk)
                        (addr: addressing) (args: list mreg) (src: mreg)
                        (k: code) : res code :=
  do am <- transl_addressing addr args;
  match chunk with
  | Mint8unsigned | Mint8signed =>
      do r <- ireg_of src; mk_smallstore Pmovb_mr am r k
  | Mint16unsigned | Mint16signed =>
      do r <- ireg_of src; OK(Pmovw_mr am r :: k)
  | Mint32 =>
      do r <- ireg_of src; OK(Pmov_mr am r :: k)
  | Mfloat32 =>
      do r <- freg_of src; OK(Pcvtsd2ss_mf am r :: k)
  | Mfloat64 =>
      do r <- freg_of src; OK(Pmovsd_mf am r :: k)
  end.

(** Translation of a Mach instruction. *)

Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
  match i with
  | Mgetstack ofs ty dst =>
      loadind ESP ofs ty dst k
  | Msetstack src ofs ty =>
      storeind src ESP ofs ty k
  | Mgetparam ofs ty dst =>
      do k1 <- loadind EDX ofs ty dst k;
      loadind ESP f.(fn_link_ofs) Tint IT1 k1
  | Mop op args res =>
      transl_op op args res k
  | Mload chunk addr args dst =>
      transl_load chunk addr args dst k
  | Mstore chunk addr args src =>
      transl_store chunk addr args src k
  | Mcall sig (inl reg) =>
      do r <- ireg_of reg; OK (Pcall_r r :: k)
  | Mcall sig (inr symb) =>
      OK (Pcall_s symb :: k)
  | Mtailcall sig (inl reg) =>
      do r <- ireg_of reg; 
      OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) 
                     f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
          Pjmp_r r :: k)
  | Mtailcall sig (inr symb) =>
      OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) 
                     f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
          Pjmp_s symb :: k)
  | Mlabel lbl =>
      OK(Plabel lbl :: k)
  | Mgoto lbl =>
      OK(Pjmp_l lbl :: k)
  | Mcond cond args lbl =>
      transl_cond cond args (Pjcc (testcond_for_condition cond) lbl :: k)
  | Mjumptable arg tbl =>
      do r <- ireg_of arg; OK (Pjmptbl r tbl :: k)
  | Mreturn =>
      OK (Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) 
                     f.(fn_retaddr_ofs) f.(fn_link_ofs) :: 
          Pret :: k)
  | Mbuiltin ef args res =>
      OK (Pbuiltin ef (List.map preg_of args) (preg_of res) :: k)
  end.

Fixpoint transl_code (f: Mach.function) (il: list Mach.instruction) :=
  match il with
  | nil => OK nil
  | i1 :: il' => do k <- transl_code f il'; transl_instr f i1 k
  end.

(** Translation of a whole function.  Note that we must check
  that the generated code contains less than [2^32] instructions,
  otherwise the offset part of the [PC] code pointer could wrap
  around, leading to incorrect executions. *)

Definition transf_function (f: Mach.function) : res Asm.code :=
  do c <- transl_code f f.(fn_code);
  if zlt (list_length_z c) Int.max_unsigned 
  then OK (Pallocframe (- f.(fn_framesize)) f.(fn_stacksize)
                       f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)
  else Error (msg "code size exceeded").

Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
  transf_partial_fundef transf_function f.

Definition transf_program (p: Mach.program) : res Asm.program :=
  transform_partial_program transf_fundef p.