summaryrefslogtreecommitdiff
path: root/ia32/PrintAsm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/PrintAsm.ml')
-rw-r--r--ia32/PrintAsm.ml625
1 files changed, 625 insertions, 0 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
new file mode 100644
index 0000000..e75032c
--- /dev/null
+++ b/ia32/PrintAsm.ml
@@ -0,0 +1,625 @@
+(* *********************************************************************)
+(* *)
+(* 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 IA32 assembly code in asm syntax *)
+
+open Printf
+open Datatypes
+open Camlcoq
+open AST
+open Asm
+
+(* Recognition of target ABI and asm syntax *)
+
+type target = ELF | AOUT | MacOS
+
+let target =
+ match Configuration.system with
+ | "macosx" -> MacOS
+ | "linux" -> ELF
+ | "bsd" -> ELF
+ | "cygwin" -> AOUT
+ | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")
+
+(* 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 transl_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'
+
+(* Basic printing functions *)
+
+let coqint oc n =
+ fprintf oc "%ld" (camlint_of_coqint n)
+
+let raw_symbol oc s =
+ match target with
+ | ELF -> fprintf oc "%s" s
+ | MacOS | AOUT -> fprintf oc "_%s" s
+
+let re_variadic_stub = Str.regexp "\\(.*\\)\\$[if]*$"
+
+let symbol oc symb =
+ let s = extern_atom symb in
+ if Str.string_match re_variadic_stub s 0
+ then raw_symbol oc (Str.matched_group 1 s)
+ else raw_symbol oc s
+
+let symbol_offset oc (symb, ofs) =
+ symbol oc symb;
+ if ofs <> 0l then fprintf oc " + %ld" ofs
+
+let label oc lbl =
+ match target with
+ | ELF -> fprintf oc ".L%d" lbl
+ | MacOS | AOUT -> fprintf oc "L%d" lbl
+
+let comment = "#"
+
+let int_reg_name = function
+ | EAX -> "%eax" | EBX -> "%ebx" | ECX -> "%ecx" | EDX -> "%edx"
+ | ESI -> "%esi" | EDI -> "%edi" | EBP -> "%ebp" | ESP -> "%esp"
+
+let int8_reg_name = function
+ | EAX -> "%al" | EBX -> "%bl" | ECX -> "%cl" | EDX -> "%dl"
+ | _ -> assert false
+
+let int16_reg_name = function
+ | EAX -> "%ax" | EBX -> "%bx" | ECX -> "%cx" | EDX -> "%dx"
+ | _ -> assert false
+
+let float_reg_name = function
+ | XMM0 -> "%xmm0" | XMM1 -> "%xmm1" | XMM2 -> "%xmm2" | XMM3 -> "%xmm3"
+ | XMM4 -> "%xmm4" | XMM5 -> "%xmm5" | XMM6 -> "%xmm6" | XMM7 -> "%xmm7"
+
+let ireg oc r = output_string oc (int_reg_name r)
+let ireg8 oc r = output_string oc (int8_reg_name r)
+let ireg16 oc r = output_string oc (int16_reg_name r)
+let freg oc r = output_string oc (float_reg_name r)
+
+let addressing oc (Addrmode(base, shift, cst)) =
+ begin match cst with
+ | Coq_inl n ->
+ let n = camlint_of_coqint n in
+ fprintf oc "%ld" n
+ | Coq_inr(Coq_pair(id, ofs)) ->
+ let ofs = camlint_of_coqint ofs in
+ if ofs = 0l
+ then symbol oc id
+ else fprintf oc "(%a + %ld)" symbol id ofs
+ end;
+ begin match base, shift with
+ | None, None -> ()
+ | Some r1, None -> fprintf oc "(%a)" ireg r1
+ | None, Some(Coq_pair(r2,sc)) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc
+ | Some r1, Some(Coq_pair(r2,sc)) -> fprintf oc "(%a,%a,%a)" ireg r1 ireg r2 coqint sc
+ end
+
+let name_of_condition = function
+ | Cond_e -> "e" | Cond_ne -> "ne"
+ | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a"
+ | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g"
+ | Cond_p -> "p" | Cond_np -> "np"
+ | Cond_nep | Cond_enp -> assert false (* treated specially *)
+
+let section oc name =
+ fprintf oc " %s\n" name
+
+(* Names of sections *)
+
+let (text, data, const_data, float_literal, jumptable_literal) =
+ match target with
+ | ELF ->
+ (".text",
+ ".data",
+ ".section .rodata",
+ ".section .rodata.cst8,\"a\",@progbits",
+ ".text")
+ | MacOS ->
+ (".text",
+ ".data",
+ ".const",
+ ".const_data",
+ ".text")
+ | AOUT ->
+ (".text",
+ ".data",
+ ".section .rdata,\"dr\"",
+ ".section .rdata,\"dr\"",
+ ".text")
+
+(* SP adjustment to allocate or free a stack frame *)
+
+let stack_alignment =
+ match target with
+ | ELF | AOUT -> 8 (* minimum is 4, 8 is better for perfs *)
+ | MacOS -> 16 (* mandatory *)
+
+let int32_align n a =
+ if n >= 0l
+ then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a))
+ else Int32.logand n (Int32.of_int (-a))
+
+let sp_adjustment lo hi =
+ let lo = camlint_of_coqint lo and hi = camlint_of_coqint hi in
+ let sz = Int32.sub hi lo in
+(* Enforce stack alignment, noting that 4 bytes are already allocated
+ by the call *)
+ let sz = Int32.sub (int32_align (Int32.add sz 4l) stack_alignment) 4l in
+ assert (sz >= 0l);
+ sz
+
+(* Base-2 log of a Caml integer *)
+
+let rec log2 n =
+ assert (n > 0);
+ if n = 1 then 0 else 1 + log2 (n lsr 1)
+
+(* Emit a align directive *)
+
+let print_align oc n =
+ match target with
+ | ELF -> fprintf oc " .align %d\n" n
+ | AOUT | MacOS -> fprintf oc " .align %d\n" (log2 n)
+
+let need_masks = ref false
+
+(* Built-in functions *)
+
+(* Built-ins. They come in two flavors:
+ - inlined by the compiler: take their arguments in arbitrary
+ registers; preserve all registers except ECX, EDX, XMM6 and XMM7
+ - inlined while printing asm code; take their arguments in
+ locations dictated by the calling conventions; preserve
+ callee-save regs only. *)
+
+let print_builtin_inlined oc name args res =
+ fprintf oc "%s begin builtin %s\n" comment name;
+ begin match name, args, res with
+ (* Volatile reads *)
+ | "__builtin_volatile_read_int8unsigned", [IR addr], IR res ->
+ fprintf oc " movzbl 0(%a), %a\n" ireg addr ireg res
+ | "__builtin_volatile_read_int8signed", [IR addr], IR res ->
+ fprintf oc " movsbl 0(%a), %a\n" ireg addr ireg res
+ | "__builtin_volatile_read_int16unsigned", [IR addr], IR res ->
+ fprintf oc " movzwl 0(%a), %a\n" ireg addr ireg res
+ | "__builtin_volatile_read_int16signed", [IR addr], IR res ->
+ fprintf oc " movswl 0(%a), %a\n" ireg addr ireg res
+ | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res ->
+ fprintf oc " movl 0(%a), %a\n" ireg addr ireg res
+ | "__builtin_volatile_read_float32", [IR addr], FR res ->
+ fprintf oc " cvtss2sd 0(%a), %a\n" ireg addr freg res
+ | "__builtin_volatile_read_float64", [IR addr], FR res ->
+ fprintf oc " movsd 0(%a), %a\n" ireg addr freg res
+ (* Volatile writes *)
+ | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ ->
+ if Asmgen.low_ireg src then
+ fprintf oc " movb %a, 0(%a)\n" ireg8 src ireg addr
+ else begin
+ fprintf oc " movl %a, %%ecx\n" ireg src;
+ fprintf oc " movb %%cl, 0(%a)\n" ireg addr
+ end
+ | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ ->
+ if Asmgen.low_ireg src then
+ fprintf oc " movw %a, 0(%a)\n" ireg16 src ireg addr
+ else begin
+ fprintf oc " movl %a, %%ecx\n" ireg src;
+ fprintf oc " movw %%cx, 0(%a)\n" ireg addr
+ end
+ | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ ->
+ fprintf oc " movl %a, 0(%a)\n" ireg src ireg addr
+ | "__builtin_volatile_write_float32", [IR addr; FR src], _ ->
+ fprintf oc " cvtsd2ss %a, %%xmm7\n" freg src;
+ fprintf oc " movss %%xmm7, 0(%a)\n" ireg addr
+ | "__builtin_volatile_write_float64", [IR addr; FR src], _ ->
+ fprintf oc " movsd %a, 0(%a)\n" freg src ireg addr
+ (* Float arithmetic *)
+ | "__builtin_fabs", [FR a1], FR res ->
+ need_masks := true;
+ if a1 <> res then
+ fprintf oc " movsd %a, %a\n" freg a1 freg res;
+ fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg res
+ | "__builtin_fsqrt", [FR a1], FR res ->
+ fprintf oc " sqrtsd %a, %a\n" freg a1 freg res
+ (* Also: fmax, fmin *)
+ | _ ->
+ invalid_arg ("unrecognized builtin " ^ name)
+ end;
+ fprintf oc "%s end builtin %s\n" comment name
+
+let re_builtin_function = Str.regexp "__builtin_"
+
+let is_builtin_function s =
+ Str.string_match re_builtin_function (extern_atom s) 0
+
+let print_builtin_function oc s =
+ fprintf oc "%s begin builtin function %s\n" comment (extern_atom s);
+ (* arguments: on stack, starting at offset 0 *)
+ (* result: EAX or ST0 *)
+ begin match extern_atom s with
+ (* Block copy *)
+ | "__builtin_memcpy" ->
+ fprintf oc " movl %%esi, %%eax\n";
+ fprintf oc " movl %%edi, %%edx\n";
+ fprintf oc " movl 0(%%esp), %%edi\n";
+ fprintf oc " movl 4(%%esp), %%esi\n";
+ fprintf oc " movl 8(%%esp), %%ecx\n";
+ fprintf oc " rep movsb\n";
+ fprintf oc " movl %%eax, %%esi\n";
+ fprintf oc " movl %%edx, %%edi\n"
+ | "__builtin_memcpy_words" ->
+ fprintf oc " movl %%esi, %%eax\n";
+ fprintf oc " movl %%edi, %%edx\n";
+ fprintf oc " movl 0(%%esp), %%edi\n";
+ fprintf oc " movl 4(%%esp), %%esi\n";
+ fprintf oc " movl 8(%%esp), %%ecx\n";
+ fprintf oc " shr $2, %%ecx\n";
+ fprintf oc " rep movsl\n";
+ fprintf oc " movl %%eax, %%esi\n";
+ fprintf oc " movl %%edx, %%edi\n"
+ (* Catch-all *)
+ | s ->
+ invalid_arg ("unrecognized builtin function " ^ s)
+ end;
+ fprintf oc "%s end builtin function %s\n" comment (extern_atom s)
+
+(* Printing of instructions *)
+
+module Labelset = Set.Make(struct type t = label let compare = compare end)
+
+let float_literals : (int * int64) list ref = ref []
+let jumptables : (int * label list) list ref = ref []
+
+(* Reminder on AT&T syntax: op source, dest *)
+
+let print_instruction oc labels = function
+ (* Moves *)
+ | Pmov_rr(rd, r1) ->
+ fprintf oc " movl %a, %a\n" ireg r1 ireg rd
+ | Pmov_ri(rd, n) ->
+ let n = camlint_of_coqint n in
+ if n = 0l then
+ fprintf oc " xorl %a, %a\n" ireg rd ireg rd
+ else
+ fprintf oc " movl $%ld, %a\n" n ireg rd
+ | Pmov_rm(rd, a) ->
+ fprintf oc " movl %a, %a\n" addressing a ireg rd
+ | Pmov_mr(a, r1) ->
+ fprintf oc " movl %a, %a\n" ireg r1 addressing a
+ | Pmovd_fr(rd, r1) ->
+ fprintf oc " movd %a, %a\n" ireg r1 freg rd
+ | Pmovd_rf(rd, r1) ->
+ fprintf oc " movd %a, %a\n" freg r1 ireg rd
+ | Pmovsd_ff(rd, r1) ->
+ fprintf oc " movsd %a, %a\n" freg r1 freg rd
+ | Pmovsd_fi(rd, n) ->
+ let b = Int64.bits_of_float n in
+ if b = 0L then (* +0.0 *)
+ fprintf oc " xorpd %a, %a %s +0.0\n" freg rd freg rd comment
+ else begin
+ let lbl = new_label() in
+ fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment n;
+ float_literals := (lbl, b) :: !float_literals
+ end
+ | Pmovsd_fm(rd, a) ->
+ fprintf oc " movsd %a, %a\n" addressing a freg rd
+ | Pmovsd_mf(a, r1) ->
+ fprintf oc " movsd %a, %a\n" freg r1 addressing a
+ | Pfld_f(r1) ->
+ fprintf oc " subl $8, %%esp\n";
+ fprintf oc " movsd %a, 0(%%esp)\n" freg r1;
+ fprintf oc " fldl 0(%%esp)\n";
+ fprintf oc " addl $8, %%esp\n"
+ | Pfld_m(a) ->
+ fprintf oc " fldl %a\n" addressing a
+ | Pfstp_f(rd) ->
+ fprintf oc " subl $8, %%esp\n";
+ fprintf oc " fstpl 0(%%esp)\n";
+ fprintf oc " movsd 0(%%esp), %a\n" freg rd;
+ fprintf oc " addl $8, %%esp\n"
+ | Pfstp_m(a) ->
+ fprintf oc " fstpl %a\n" addressing a
+ (** Moves with conversion *)
+ | Pmovb_mr(a, r1) ->
+ fprintf oc " movb %a, %a\n" ireg8 r1 addressing a
+ | Pmovw_mr(a, r1) ->
+ fprintf oc " movw %a, %a\n" ireg16 r1 addressing a
+ | Pmovzb_rr(rd, r1) ->
+ fprintf oc " movzbl %a, %a\n" ireg8 r1 ireg rd
+ | Pmovzb_rm(rd, a) ->
+ fprintf oc " movzbl %a, %a\n" addressing a ireg rd
+ | Pmovsb_rr(rd, r1) ->
+ fprintf oc " movsbl %a, %a\n" ireg8 r1 ireg rd
+ | Pmovsb_rm(rd, a) ->
+ fprintf oc " movsbl %a, %a\n" addressing a ireg rd
+ | Pmovzw_rr(rd, r1) ->
+ fprintf oc " movzwl %a, %a\n" ireg16 r1 ireg rd
+ | Pmovzw_rm(rd, a) ->
+ fprintf oc " movzwl %a, %a\n" addressing a ireg rd
+ | Pmovsw_rr(rd, r1) ->
+ fprintf oc " movswl %a, %a\n" ireg16 r1 ireg rd
+ | Pmovsw_rm(rd, a) ->
+ fprintf oc " movswl %a, %a\n" addressing a ireg rd
+ | Pcvtss2sd_fm(rd, a) ->
+ fprintf oc " cvtss2sd %a, %a\n" addressing a freg rd
+ | Pcvtsd2ss_ff(rd, r1) ->
+ fprintf oc " cvtsd2ss %a, %a\n" freg r1 freg rd;
+ fprintf oc " cvtss2sd %a, %a\n" freg rd freg rd
+ | Pcvtsd2ss_mf(a, r1) ->
+ fprintf oc " cvtsd2ss %a, %%xmm7\n" freg r1;
+ fprintf oc " movss %%xmm7, %a\n" addressing a
+ | Pcvttsd2si_rf(rd, r1) ->
+ fprintf oc " cvttsd2si %a, %a\n" freg r1 ireg rd
+ | Pcvtsi2sd_fr(rd, r1) ->
+ fprintf oc " cvtsi2sd %a, %a\n" ireg r1 freg rd
+ (** Arithmetic and logical operations over integers *)
+ | Plea(rd, a) ->
+ fprintf oc " leal %a, %a\n" addressing a ireg rd
+ | Pneg(rd) ->
+ fprintf oc " negl %a\n" ireg rd
+ | Psub_rr(rd, r1) ->
+ fprintf oc " subl %a, %a\n" ireg r1 ireg rd
+ | Pimul_rr(rd, r1) ->
+ fprintf oc " imull %a, %a\n" ireg r1 ireg rd
+ | Pimul_ri(rd, n) ->
+ fprintf oc " imull $%a, %a\n" coqint n ireg rd
+ | Pdiv(r1) ->
+ fprintf oc " xorl %%edx, %%edx\n";
+ fprintf oc " divl %a\n" ireg r1
+ | Pidiv(r1) ->
+ fprintf oc " cltd\n";
+ fprintf oc " idivl %a\n" ireg r1
+ | Pand_rr(rd, r1) ->
+ fprintf oc " andl %a, %a\n" ireg r1 ireg rd
+ | Pand_ri(rd, n) ->
+ fprintf oc " andl $%a, %a\n" coqint n ireg rd
+ | Por_rr(rd, r1) ->
+ fprintf oc " orl %a, %a\n" ireg r1 ireg rd
+ | Por_ri(rd, n) ->
+ fprintf oc " orl $%a, %a\n" coqint n ireg rd
+ | Pxor_rr(rd, r1) ->
+ fprintf oc " xorl %a, %a\n" ireg r1 ireg rd
+ | Pxor_ri(rd, n) ->
+ fprintf oc " xorl $%a, %a\n" coqint n ireg rd
+ | Psal_rcl(rd) ->
+ fprintf oc " sall %%cl, %a\n" ireg rd
+ | Psal_ri(rd, n) ->
+ fprintf oc " sall $%a, %a\n" coqint n ireg rd
+ | Pshr_rcl(rd) ->
+ fprintf oc " shrl %%cl, %a\n" ireg rd
+ | Pshr_ri(rd, n) ->
+ fprintf oc " shrl $%a, %a\n" coqint n ireg rd
+ | Psar_rcl(rd) ->
+ fprintf oc " sarl %%cl, %a\n" ireg rd
+ | Psar_ri(rd, n) ->
+ fprintf oc " sarl $%a, %a\n" coqint n ireg rd
+ | Pror_ri(rd, n) ->
+ fprintf oc " rorl $%a, %a\n" coqint n ireg rd
+ | Pcmp_rr(r1, r2) ->
+ fprintf oc " cmpl %a, %a\n" ireg r2 ireg r1
+ | Pcmp_ri(r1, n) ->
+ fprintf oc " cmpl $%a, %a\n" coqint n ireg r1
+ | Ptest_rr(r1, r2) ->
+ fprintf oc " testl %a, %a\n" ireg r2 ireg r1
+ | Ptest_ri(r1, n) ->
+ fprintf oc " testl $%a, %a\n" coqint n ireg r1
+ | Pcmov(c, rd, r1) ->
+ assert (c <> Cond_nep && c <> Cond_enp);
+ fprintf oc " cmov%s %a, %a\n" (name_of_condition c) ireg r1 ireg rd
+ | Psetcc(c, rd) ->
+ begin match c with
+ | Cond_nep ->
+ fprintf oc " setne %%cl\n";
+ fprintf oc " setp %%dl\n";
+ fprintf oc " orb %%dl, %%cl\n"
+ | Cond_enp ->
+ fprintf oc " sete %%cl\n";
+ fprintf oc " setnp %%dl\n";
+ fprintf oc " andb %%dl, %%cl\n"
+ | _ ->
+ fprintf oc " set%s %%cl\n" (name_of_condition c)
+ end;
+ fprintf oc " movzbl %%cl, %a\n" ireg rd
+ (** Arithmetic operations over floats *)
+ | Paddd_ff(rd, r1) ->
+ fprintf oc " addsd %a, %a\n" freg r1 freg rd
+ | Psubd_ff(rd, r1) ->
+ fprintf oc " subsd %a, %a\n" freg r1 freg rd
+ | Pmuld_ff(rd, r1) ->
+ fprintf oc " mulsd %a, %a\n" freg r1 freg rd
+ | Pdivd_ff(rd, r1) ->
+ fprintf oc " divsd %a, %a\n" freg r1 freg rd
+ | Pnegd (rd) ->
+ need_masks := true;
+ fprintf oc " xorpd %a, %a\n" raw_symbol "__negd_mask" freg rd
+ | Pabsd (rd) ->
+ need_masks := true;
+ fprintf oc " andpd %a, %a\n" raw_symbol "__absd_mask" freg rd
+ | Pcomisd_ff(r1, r2) ->
+ fprintf oc " comisd %a, %a\n" freg r2 freg r1
+ (** Branches and calls *)
+ | Pjmp_l(l) ->
+ fprintf oc " jmp %a\n" label (transl_label l)
+ | Pjmp_s(f) ->
+ if not (is_builtin_function f) then
+ fprintf oc " jmp %a\n" symbol f
+ else begin
+ print_builtin_function oc f;
+ fprintf oc " ret\n"
+ end
+ | Pjmp_r(r) ->
+ fprintf oc " jmp *%a\n" ireg r
+ | Pjcc(c, l) ->
+ let l = transl_label l in
+ begin match c with
+ | Cond_nep ->
+ fprintf oc " jp %a\n" label l;
+ fprintf oc " jne %a\n" label l
+ | Cond_enp ->
+ let l' = new_label() in
+ fprintf oc " jp %a\n" label l';
+ fprintf oc " je %a\n" label l;
+ fprintf oc "%a:\n" label l'
+ | _ ->
+ fprintf oc " j%s %a\n" (name_of_condition c) label l
+ end
+ | Pjmptbl(r, tbl) ->
+ let l = new_label() in
+ fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r;
+ jumptables := (l, tbl) :: !jumptables
+ | Pcall_s(f) ->
+ if not (is_builtin_function f) then
+ fprintf oc " call %a\n" symbol f
+ else
+ print_builtin_function oc f
+ | Pcall_r(r) ->
+ fprintf oc " call *%a\n" ireg r
+ | Pret ->
+ fprintf oc " ret\n"
+ (** Pseudo-instructions *)
+ | Plabel(l) ->
+ if Labelset.mem l labels then
+ fprintf oc "%a:\n" label (transl_label l)
+ | Pallocframe(lo, hi, ofs_ra, ofs_link) ->
+ let sz = sp_adjustment lo hi in
+ let ofs_link = camlint_of_coqint ofs_link in
+ fprintf oc " subl $%ld, %%esp\n" sz;
+ fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l);
+ fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link
+ | Pfreeframe(lo, hi, ofs_ra, ofs_link) ->
+ let sz = sp_adjustment lo hi in
+ fprintf oc " addl $%ld, %%esp\n" sz
+ | Pbuiltin(ef, args, res) ->
+ print_builtin_inlined oc (extern_atom ef.ef_id) args res
+
+let print_literal oc (lbl, n) =
+ fprintf oc "%a: .quad 0x%Lx\n" label lbl n
+
+let print_jumptable oc (lbl, tbl) =
+ fprintf oc "%a:" label lbl;
+ List.iter
+ (fun l -> fprintf oc " .long %a\n" label (transl_label l))
+ tbl
+
+let rec labels_of_code accu = function
+ | [] ->
+ accu
+ | (Pjmp_l lbl | Pjcc(_, lbl)) :: c ->
+ labels_of_code (Labelset.add lbl accu) c
+ | Pjmptbl(_, tbl) :: c ->
+ labels_of_code (List.fold_right Labelset.add tbl accu) c
+ | _ :: c ->
+ labels_of_code accu c
+
+let print_function oc name code =
+ Hashtbl.clear current_function_labels;
+ float_literals := [];
+ jumptables := [];
+ section oc text;
+ print_align oc 16;
+ if not (C2C.atom_is_static name) then
+ fprintf oc " .globl %a\n" symbol name;
+ fprintf oc "%a:\n" symbol name;
+ List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code;
+ if target = ELF then begin
+ fprintf oc " .type %a, @function\n" symbol name;
+ fprintf oc " .size %a, . - %a\n" symbol name symbol name
+ end;
+ if !float_literals <> [] then begin
+ section oc float_literal;
+ print_align oc 8;
+ List.iter (print_literal oc) !float_literals;
+ float_literals := []
+ end;
+ if !jumptables <> [] then begin
+ section oc jumptable_literal;
+ print_align oc 4;
+ List.iter (print_jumptable oc) !jumptables;
+ jumptables := []
+ end
+
+let print_fundef oc (Coq_pair(name, defn)) =
+ match defn with
+ | Internal code -> print_function oc name code
+ | External ef -> ()
+
+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 %s %.18g\n" (Int32.bits_of_float n) comment n
+ | Init_float64 n ->
+ fprintf oc " .quad %Ld %s %.18g\n" (Int64.bits_of_float n) comment n
+ | Init_space n ->
+ let n = camlint_of_z n in
+ if n > 0l then fprintf oc " .space %ld\n" n
+ | Init_addrof(symb, ofs) ->
+ fprintf oc " .long %a\n"
+ symbol_offset (symb, camlint_of_coqint ofs)
+
+let print_init_data oc name id =
+ if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
+ && List.for_all (function Init_int8 _ -> true | _ -> false) id
+ then
+ fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id)
+ else
+ List.iter (print_init oc) id
+
+let print_var oc (Coq_pair(name, v)) =
+ match v.gvar_init with
+ | [] -> ()
+ | _ ->
+ let sec =
+ if v.gvar_readonly then const_data else data
+ and align =
+ match C2C.atom_alignof name with
+ | Some a -> a
+ | None -> 8 (* 8-alignment is a safe default *)
+ in
+ section oc sec;
+ print_align oc align;
+ if not (C2C.atom_is_static name) then
+ fprintf oc " .globl %a\n" symbol name;
+ fprintf oc "%a:\n" symbol name;
+ print_init_data oc name v.gvar_init;
+ if target = ELF then begin
+ fprintf oc " .type %a, @object\n" symbol name;
+ fprintf oc " .size %a, . - %a\n" symbol name symbol name
+ end
+
+let print_program oc p =
+ need_masks := false;
+ List.iter (print_var oc) p.prog_vars;
+ List.iter (print_fundef oc) p.prog_funct;
+ if !need_masks then begin
+ section oc float_literal;
+ print_align oc 16;
+ fprintf oc "%a: .quad 0x8000000000000000, 0\n"
+ raw_symbol "__negd_mask";
+ fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n"
+ raw_symbol "__absd_mask"
+ end
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 08:04:53 +0000