From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/PrintAsm.ml | 625 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 625 insertions(+) create mode 100644 ia32/PrintAsm.ml (limited to 'ia32/PrintAsm.ml') diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml new file mode 100644 index 00000000..e75032c5 --- /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 -- cgit