summaryrefslogtreecommitdiff
path: root/caml/PrintPPC.ml
blob: f4f2940221fcbcd3d731eaed019422dc459a5c50 (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
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
(* *********************************************************************)
(*                                                                     *)
(*              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.     *)
(*                                                                     *)
(* *********************************************************************)

(* Printing PPC assembly code in asm syntax *)

open Printf
open Datatypes
open CList
open Camlcoq
open AST
open PPC

(* On-the-fly label renaming *)

let next_label = ref 100

let new_label() =
  let lbl = !next_label in incr next_label; lbl

let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)

let label_for_label lbl =
  try
    Hashtbl.find current_function_labels lbl
  with Not_found ->
    let lbl' = new_label() in
    Hashtbl.add current_function_labels lbl lbl';
    lbl'

(* Record identifiers of external functions *)

module IdentSet = Set.Make(struct type t = ident let compare = compare end)

let extfuns = ref IdentSet.empty

let record_extfun (Coq_pair(name, defn)) =
  match defn with
  | Internal _ -> ()
  | External _ -> extfuns := IdentSet.add name !extfuns

(* Basic printing functions *)

let print_symb oc symb =
  if IdentSet.mem symb !extfuns
  then fprintf oc "L%s$stub" (extern_atom symb)
  else fprintf oc "_%s" (extern_atom symb)

let print_label oc lbl =
  fprintf oc "L%d" (label_for_label lbl)

let print_symb_ofs oc (symb, ofs) =
  print_symb oc symb;
  if ofs <> 0l then fprintf oc " + %ld" ofs

let print_constant oc = function
  | Cint n ->
      fprintf oc "%ld" (camlint_of_coqint n)
  | Csymbol_low(s, n) ->
      fprintf oc "lo16(%a)" print_symb_ofs (s, camlint_of_coqint n)
  | Csymbol_high(s, n) ->
      fprintf oc "ha16(%a)" print_symb_ofs (s, camlint_of_coqint n)

let num_crbit = function
  | CRbit_0 -> 0
  | CRbit_1 -> 1
  | CRbit_2 -> 2
  | CRbit_3 -> 3

let print_crbit oc bit =
  fprintf oc "%d" (num_crbit bit)

let print_coqint oc n =
  fprintf oc "%ld" (camlint_of_coqint n)

let int_reg_name = function
  | GPR0 -> "r0"  | GPR1 -> "r1"  | GPR2 -> "r2"  | GPR3 -> "r3"
  | GPR4 -> "r4"  | GPR5 -> "r5"  | GPR6 -> "r6"  | GPR7 -> "r7"
  | GPR8 -> "r8"  | GPR9 -> "r9"  | GPR10 -> "r10" | GPR11 -> "r11"
  | GPR12 -> "r12" | GPR13 -> "r13" | GPR14 -> "r14" | GPR15 -> "r15"
  | GPR16 -> "r16" | GPR17 -> "r17" | GPR18 -> "r18" | GPR19 -> "r19"
  | GPR20 -> "r20" | GPR21 -> "r21" | GPR22 -> "r22" | GPR23 -> "r23"
  | GPR24 -> "r24" | GPR25 -> "r25" | GPR26 -> "r26" | GPR27 -> "r27"
  | GPR28 -> "r28" | GPR29 -> "r29" | GPR30 -> "r30" | GPR31 -> "r31"

let float_reg_name = function
  | FPR0 -> "f0"  | FPR1 -> "f1"  | FPR2 -> "f2"  | FPR3 -> "f3"
  | FPR4 -> "f4"  | FPR5 -> "f5"  | FPR6 -> "f6"  | FPR7 -> "f7"
  | FPR8 -> "f8"  | FPR9 -> "f9"  | FPR10 -> "f10" | FPR11 -> "f11"
  | FPR12 -> "f12" | FPR13 -> "f13" | FPR14 -> "f14" | FPR15 -> "f15"
  | FPR16 -> "f16" | FPR17 -> "f17" | FPR18 -> "f18" | FPR19 -> "f19"
  | FPR20 -> "f20" | FPR21 -> "f21" | FPR22 -> "f22" | FPR23 -> "f23"
  | FPR24 -> "f24" | FPR25 -> "f25" | FPR26 -> "f26" | FPR27 -> "f27"
  | FPR28 -> "f28" | FPR29 -> "f29" | FPR30 -> "f30" | FPR31 -> "f31"

let ireg oc r = output_string oc (int_reg_name r)
let ireg_or_zero oc r = if r = GPR0 then output_string oc "0" else ireg oc r
let freg oc r = output_string oc (float_reg_name r)

(* Printing of instructions *)

module Labelset = Set.Make(struct type t = label let compare = compare end)

let print_instruction oc labels = function
  | Padd(r1, r2, r3) ->
      fprintf oc "	add	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Paddi(r1, r2, c) ->
      fprintf oc "	addi	%a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c
  | Paddis(r1, r2, c) ->
      fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 print_constant c
  | Paddze(r1, r2) ->
      fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
  | Pallocblock ->
      fprintf oc "	bl	_compcert_alloc\n"
  | Pallocframe(lo, hi, ofs) ->
      let lo = camlint_of_coqint lo
      and hi = camlint_of_coqint hi
      and ofs = camlint_of_coqint ofs in
      let sz = Int32.sub hi lo in
      (* Keep stack 16-aligned *)
      let sz16 = Int32.logand (Int32.add sz 15l) 0xFFFF_FFF0l in
      assert (ofs = 0l);
      fprintf oc "	stwu	r1, %ld(r1)\n" (Int32.neg sz16)
  | Pand_(r1, r2, r3) ->
      fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pandc(r1, r2, r3) ->
      fprintf oc "	andc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pandi_(r1, r2, c) ->
      fprintf oc "	andi.	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Pandis_(r1, r2, c) ->
      fprintf oc "	andis.	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Pb lbl ->
      fprintf oc "	b	%a\n" print_label lbl
  | Pbctr ->
      fprintf oc "	bctr\n"
  | Pbctrl ->
      fprintf oc "	bctrl\n"
  | Pbf(bit, lbl) ->
      fprintf oc "	bf	%a, %a\n" print_crbit bit print_label lbl
  | Pbl s ->
      fprintf oc "	bl	%a\n" print_symb s
  | Pbs s ->
      fprintf oc "	b	%a\n" print_symb s
  | Pblr ->
      fprintf oc "	blr\n"
  | Pbt(bit, lbl) ->
      fprintf oc "	bt	%a, %a\n" print_crbit bit print_label lbl
  | Pcmplw(r1, r2) ->
      fprintf oc "	cmplw	cr0, %a, %a\n" ireg r1 ireg r2
  | Pcmplwi(r1, c) ->
      fprintf oc "	cmplwi	cr0, %a, %a\n" ireg r1 print_constant c
  | Pcmpw(r1, r2) ->
      fprintf oc "	cmpw	cr0, %a, %a\n" ireg r1 ireg r2
  | Pcmpwi(r1, c) ->
      fprintf oc "	cmpwi	cr0, %a, %a\n" ireg r1 print_constant c
  | Pcror(c1, c2, c3) ->
      fprintf oc "	cror	%a, %a, %a\n" print_crbit c1 print_crbit c2 print_crbit c3
  | Pdivw(r1, r2, r3) ->
      fprintf oc "	divw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pdivwu(r1, r2, r3) ->
      fprintf oc "	divwu	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Peqv(r1, r2, r3) ->
      fprintf oc "	eqv	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pextsb(r1, r2) ->
      fprintf oc "	extsb	%a, %a\n" ireg r1 ireg r2
  | Pextsh(r1, r2) ->
      fprintf oc "	extsh	%a, %a\n" ireg r1 ireg r2
  | Pfreeframe ofs ->
      fprintf oc "	lwz	r1, %ld(r1)\n" (camlint_of_coqint ofs)
  | Pfabs(r1, r2) ->
      fprintf oc "	fabs	%a, %a\n" freg r1 freg r2
  | Pfadd(r1, r2, r3) ->
      fprintf oc "	fadd	%a, %a, %a\n" freg r1 freg r2 freg r3
  | Pfcmpu(r1, r2) ->
      fprintf oc "	fcmpu	cr0, %a, %a\n" freg r1 freg r2
  | Pfcti(r1, r2) ->
      fprintf oc "	fctiwz	f13, %a\n" freg r2;
      fprintf oc "	stfd	f13, -8(r1)\n";
      fprintf oc "	lwz	%a, -4(r1)\n" ireg r1
  | Pfctiu(r1, r2) ->
      let lbl1 = new_label() in
      let lbl2 = new_label() in
      let lbl3 = new_label() in
      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl1;
      fprintf oc "	lfd	f13, lo16(L%d)(r12)\n" lbl1;
      fprintf oc "	fcmpu	cr7, %a, f13\n" freg r2;
      fprintf oc "	cror	30, 29, 30\n";
      fprintf oc "	beq	cr7, L%d\n" lbl2;
      fprintf oc "	fctiwz	f13, %a\n" freg r2;
      fprintf oc "	stfdu	f13, -8(r1)\n";
      fprintf oc "	lwz	%a, 4(r1)\n" ireg r1;
      fprintf oc "	b	L%d\n" lbl3;
      fprintf oc "L%d:	fsub	f13, %a, f13\n" lbl2 freg r2;
      fprintf oc "	fctiwz	f13, f13\n";
      fprintf oc "	stfdu	f13, -8(r1)\n";
      fprintf oc "	lwz	%a, 4(r1)\n" ireg r1;
      fprintf oc "	addis	%a, %a, 0x8000\n" ireg r1 ireg r1;
      fprintf oc "L%d:	addi	r1, r1, 8\n" lbl3;
      fprintf oc "	.const_data\n";
      fprintf oc "L%d:	.long	0x41e00000, 0x00000000\n" lbl1;
      fprintf oc "	.text\n"
  | Pfdiv(r1, r2, r3) ->
      fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
  | Pfmadd(r1, r2, r3, r4) ->
      fprintf oc "	fmadd	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
  | Pfmr(r1, r2) ->
      fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
  | Pfmsub(r1, r2, r3, r4) ->
      fprintf oc "	fmsub	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
  | Pfmul(r1, r2, r3) ->
      fprintf oc "	fmul	%a, %a, %a\n" freg r1 freg r2 freg r3
  | Pfneg(r1, r2) ->
      fprintf oc "	fneg	%a, %a\n" freg r1 freg r2
  | Pfrsp(r1, r2) ->
      fprintf oc "	frsp	%a, %a\n" freg r1 freg r2
  | Pfsub(r1, r2, r3) ->
      fprintf oc "	fsub	%a, %a, %a\n" freg r1 freg r2 freg r3
  | Pictf(r1, r2) ->
      let lbl = new_label() in
      fprintf oc "	addis	r12, 0, 0x4330\n";
      fprintf oc "	stw	r12, -8(r1)\n";
      fprintf oc "	addis	r12, %a, 0x8000\n" ireg r2;
      fprintf oc "	stw	r12, -4(r1)\n";
      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl;
      fprintf oc "	lfd	f13, lo16(L%d)(r12)\n" lbl;
      fprintf oc "	lfd	%a, -8(r1)\n" freg r1;
      fprintf oc "	fsub	%a, %a, f13\n" freg r1 freg r1;
      fprintf oc "	.const_data\n";
      fprintf oc "L%d:	.long	0x43300000, 0x80000000\n" lbl;
      fprintf oc "	.text\n"
  | Piuctf(r1, r2) ->
      let lbl = new_label() in
      fprintf oc "	addis	r12, 0, 0x4330\n";
      fprintf oc "	stw	r12, -8(r1)\n";
      fprintf oc "	stw	%a, -4(r1)\n" ireg r2;
      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl;
      fprintf oc "	lfd	f13, lo16(L%d)(r12)\n" lbl;
      fprintf oc "	lfd	%a, -8(r1)\n" freg r1;
      fprintf oc "	fsub	%a, %a, f13\n" freg r1 freg r1;
      fprintf oc "	.const_data\n";
      fprintf oc "L%d:	.long	0x43300000, 0x00000000\n" lbl;
      fprintf oc "	.text\n"
  | Plbz(r1, c, r2) ->
      fprintf oc "	lbz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
  | Plbzx(r1, r2, r3) ->
      fprintf oc "	lbzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Plfd(r1, c, r2) ->
      fprintf oc "	lfd	%a, %a(%a)\n" freg r1 print_constant c ireg r2
  | Plfdx(r1, r2, r3) ->
      fprintf oc "	lfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
  | Plfi(r1, c) ->
      let lbl = new_label() in
      fprintf oc "	addis	r12, 0, ha16(L%d)\n" lbl;
      fprintf oc "	lfd	%a, lo16(L%d)(r12)\n" freg r1 lbl;
      fprintf oc "	.const_data\n";
      let n = Int64.bits_of_float c in
      let nlo = Int64.to_int32 n
      and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
      fprintf oc "L%d:	.long	0x%lx, 0x%lx   ; %f\n" lbl nhi nlo c;
      fprintf oc "	.text\n"
  | Plfs(r1, c, r2) ->
      fprintf oc "	lfs	%a, %a(%a)\n" freg r1 print_constant c ireg r2
  | Plfsx(r1, r2, r3) ->
      fprintf oc "	lfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
  | Plha(r1, c, r2) ->
      fprintf oc "	lha	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
  | Plhax(r1, r2, r3) ->
      fprintf oc "	lhax	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Plhz(r1, c, r2) ->
      fprintf oc "	lhz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
  | Plhzx(r1, r2, r3) ->
      fprintf oc "	lhzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Plwz(r1, c, r2) ->
      fprintf oc "	lwz	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
  | Plwzx(r1, r2, r3) ->
      fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pmfcrbit(r1, bit) ->
      fprintf oc "	mfcr	r2\n";
      fprintf oc "	rlwinm	%a, r2, %d, 1\n" ireg r1 (1 + num_crbit bit)
  | Pmflr(r1) ->
      fprintf oc "	mflr	%a\n" ireg r1
  | Pmr(r1, r2) ->
      fprintf oc "	mr	%a, %a\n" ireg r1 ireg r2
  | Pmtctr(r1) ->
      fprintf oc "	mtctr	%a\n" ireg r1
  | Pmtlr(r1) ->
      fprintf oc "	mtlr	%a\n" ireg r1
  | Pmulli(r1, r2, c) ->
      fprintf oc "	mulli	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Pmullw(r1, r2, r3) ->
      fprintf oc "	mullw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pnand(r1, r2, r3) ->
      fprintf oc "	nand	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pnor(r1, r2, r3) ->
      fprintf oc "	nor	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Por(r1, r2, r3) ->
      fprintf oc "	or	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Porc(r1, r2, r3) ->
      fprintf oc "	orc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pori(r1, r2, c) ->
      fprintf oc "	ori	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Poris(r1, r2, c) ->
      fprintf oc "	oris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Prlwinm(r1, r2, c1, c2) ->
      fprintf oc "	rlwinm	%a, %a, %ld, 0x%lx\n"
                ireg r1 ireg r2 (camlint_of_coqint c1) (camlint_of_coqint c2)
  | Pslw(r1, r2, r3) ->
      fprintf oc "	slw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Psraw(r1, r2, r3) ->
      fprintf oc "	sraw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Psrawi(r1, r2, c) ->
      fprintf oc "	srawi	%a, %a, %ld\n" ireg r1 ireg r2 (camlint_of_coqint c)
  | Psrw(r1, r2, r3) ->
      fprintf oc "	srw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pstb(r1, c, r2) ->
      fprintf oc "	stb	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
  | Pstbx(r1, r2, r3) ->
      fprintf oc "	stbx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pstfd(r1, c, r2) ->
      fprintf oc "	stfd	%a, %a(%a)\n" freg r1 print_constant c ireg r2
  | Pstfdx(r1, r2, r3) ->
      fprintf oc "	stfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
  | Pstfs(r1, c, r2) ->
      fprintf oc "	stfs	%a, %a(%a)\n" freg r1 print_constant c ireg r2
  | Pstfsx(r1, r2, r3) ->
      fprintf oc "	stfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
  | Psth(r1, c, r2) ->
      fprintf oc "	sth	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
  | Psthx(r1, r2, r3) ->
      fprintf oc "	sthx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pstw(r1, c, r2) ->
      fprintf oc "	stw	%a, %a(%a)\n" ireg r1 print_constant c ireg r2
  | Pstwx(r1, r2, r3) ->
      fprintf oc "	stwx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Psubfc(r1, r2, r3) ->
      fprintf oc "	subfc	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Psubfic(r1, r2, c) ->
      fprintf oc "	subfic	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Pxor(r1, r2, r3) ->
      fprintf oc "	xor	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
  | Pxori(r1, r2, c) ->
      fprintf oc "	xori	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Pxoris(r1, r2, c) ->
      fprintf oc "	xoris	%a, %a, %a\n" ireg r1 ireg r2 print_constant c
  | Plabel lbl ->
      if Labelset.mem lbl labels then fprintf oc "%a:\n" print_label lbl

let rec labels_of_code = function
  | Coq_nil -> Labelset.empty
  | Coq_cons((Pb lbl | Pbf(_, lbl) | Pbt(_, lbl)), c) ->
      Labelset.add lbl (labels_of_code c)
  | Coq_cons(_, c) -> labels_of_code c

let print_function oc name code =
  Hashtbl.clear current_function_labels;
  fprintf oc "	.text\n";
  fprintf oc "	.align 2\n";
  fprintf oc "	.globl %a\n" print_symb name;
  fprintf oc "%a:\n" print_symb name;
  coqlist_iter (print_instruction oc (labels_of_code code)) code

(* Generation of stub code for variadic functions, e.g. printf.
   Calling conventions for variadic functions are:
     - always reserve 8 stack words (offsets 24 to 52) so that the
       variadic function can save there the integer registers parameters
       r3 ... r10
     - treat float arguments as pairs of integers, i.e. if we
       must pass them in registers, use a pair of integer registers
       for this purpose.
   The code we generate is:
     - allocate large enough stack frame
     - save return address
     - copy our arguments (registers and stack) to the stack frame,
       starting at offset 24
     - load relevant integer parameter registers r3...r10 from the
       stack frame, limited by the actual number of arguments
     - call the variadic thing
     - deallocate stack frame and return
*)

let variadic_stub oc stub_name fun_name ty_args =
  (* Compute total size of arguments *)
  let arg_size =
    CList.fold_left
     (fun sz ty -> match ty with Tint -> sz + 4 | Tfloat -> sz + 8)
     ty_args 0 in
  (* Stack size is linkage area + argument size, with a minimum of 56 bytes *)
  let frame_size = max 56 (24 + arg_size) in
  fprintf oc "	mflr	r0\n";
  fprintf oc "	stwu	r1, %d(r1)\n" (-frame_size);
  fprintf oc "	stw	r0, %d(r1)\n" (frame_size + 4);
  (* Copy our parameters to our stack frame.
     As an optimization, don't copy parameters that are already in
     integer registers, since these stay in place. *)
  let rec copy gpr fpr src_ofs dst_ofs = function
    | Coq_nil -> ()
    | Coq_cons(Tint, rem) ->
        if gpr > 10 then begin
          fprintf oc "	lwz	r0, %d(r1)\n" src_ofs;
          fprintf oc "	stw	r0, %d(r1)\n" dst_ofs
        end;
        copy (gpr + 1) fpr (src_ofs + 4) (dst_ofs + 4) rem
    | Coq_cons(Tfloat, rem) ->
        if fpr <= 10 then begin
          fprintf oc "	stfd	f%d, %d(r1)\n" fpr dst_ofs
        end else begin
          fprintf oc "	lfd	f0, %d(r1)\n" src_ofs;
          fprintf oc "	stfd	f0, %d(r1)\n" dst_ofs
        end;
        copy (gpr + 2) (fpr + 1) (src_ofs + 8) (dst_ofs + 8) rem
  in copy 3 1 (frame_size + 24) 24 ty_args;
  (* Load the first parameters into integer registers.
     As an optimization, don't load parameters that are already
     in the correct integer registers. *)
  let rec load gpr ofs = function
    | Coq_nil -> ()
    | Coq_cons(Tint, rem) ->
        load (gpr + 1) (ofs + 4) rem
    | Coq_cons(Tfloat, rem) ->
        if gpr <= 10 then
          fprintf oc "	lwz	r%d, %d(r1)\n" gpr ofs;
        if gpr + 1 <= 10 then
          fprintf oc "	lwz	r%d, %d(r1)\n" (gpr + 1) (ofs + 4);
        load (gpr + 2) (ofs + 8) rem
  in load 3 24 ty_args;
  (* Call the function *)
  fprintf oc "	addis	r11, 0, ha16(L%s$ptr)\n" stub_name;
  fprintf oc "	lwz	r11, lo16(L%s$ptr)(r11)\n" stub_name;
  fprintf oc "	mtctr	r11\n";
  fprintf oc "	bctrl\n";
  (* Free our frame and return *)
  fprintf oc "	lwz	r0, %d(r1)\n" (frame_size + 4);
  fprintf oc "	mtlr	r0\n";
  fprintf oc "	addi	r1, r1, %d\n" frame_size;
  fprintf oc "	blr\n";
  (* The function pointer *)
  fprintf oc "	.non_lazy_symbol_pointer\n";
  fprintf oc "L%s$ptr:\n" stub_name;
  fprintf oc "	.indirect_symbol _%s\n" fun_name;
  fprintf oc "	.long	0\n"

(* Stubs for fixed-type functions are much simpler *)

let non_variadic_stub oc name =
  fprintf oc "	addis	r11, 0, ha16(L%s$ptr)\n" name;
  fprintf oc "	lwz	r11, lo16(L%s$ptr)(r11)\n" name;
  fprintf oc "	mtctr	r11\n";
  fprintf oc "	bctr\n";
  fprintf oc "	.non_lazy_symbol_pointer\n";
  fprintf oc "L%s$ptr:\n" name;
  fprintf oc "	.indirect_symbol _%s\n" name;
  fprintf oc "	.long	0\n"

let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$"

let print_external_function oc name ef =
  let name = extern_atom name in
  fprintf oc "	.text\n";
  fprintf oc "	.align 2\n";
  fprintf oc "L%s$stub:\n" name;
  if Str.string_match re_variadic_stub name 0
  then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args
  else non_variadic_stub oc name

let print_fundef oc (Coq_pair(name, defn)) =
  match defn with
  | Internal code -> print_function oc name code
  | External ef -> print_external_function oc name ef

let init_data_queue = ref []

let print_init oc = function
  | Init_int8 n ->
      fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
  | Init_int16 n ->
      fprintf oc "	.short	%ld\n" (camlint_of_coqint n)
  | Init_int32 n ->
      fprintf oc "	.long	%ld\n" (camlint_of_coqint n)
  | Init_float32 n ->
      fprintf oc "	.long	%ld ; %g \n" (Int32.bits_of_float n) n
  | Init_float64 n ->
      (* .quad not working on all versions of the MacOSX assembler *)
      let b = Int64.bits_of_float n in
      fprintf oc "	.long	%Ld, %Ld ; %g \n"
                 (Int64.shift_right_logical b 32)
                 (Int64.logand b 0xFFFFFFFFL)
                 n
  | Init_space n ->
      let n = camlint_of_z n in
      if n > 0l then fprintf oc "	.space	%ld\n" n
  | Init_pointer id ->
      let lbl = new_label() in
      fprintf oc "	.long	L%d\n" lbl;
      init_data_queue := (lbl, id) :: !init_data_queue

let print_init_data oc id =
  init_data_queue := [];
  coqlist_iter (print_init oc) id;
  let rec print_remainder () =
    match !init_data_queue with
    | [] -> ()
    | (lbl, id) :: rem ->
        init_data_queue := rem;
        fprintf oc "L%d:\n" lbl;
        coqlist_iter (print_init oc) id;
        print_remainder()
  in print_remainder()

let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
  match init_data with
  | Coq_nil -> ()
  | _  ->
      fprintf oc "	.data\n";
      fprintf oc "	.align	3\n";
      fprintf oc "	.globl	%a\n" print_symb name;
      fprintf oc "%a:\n" print_symb name;
      print_init_data oc init_data

let print_program oc p =
  extfuns := IdentSet.empty;
  coqlist_iter record_extfun p.prog_funct;
  coqlist_iter (print_var oc) p.prog_vars;
  coqlist_iter (print_fundef oc) p.prog_funct