diff options
| -rw-r--r-- | arm/PrintAsm.ml | 108 | ||||
| -rw-r--r-- | backend/PrintAsm.ml | 99 | ||||
| -rw-r--r-- | backend/PrintAsm.mli (renamed from ia32/PrintAsm.mli) | 3 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 135 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 1064 | ||||
| -rw-r--r-- | ia32/TargetPrinter.ml | 976 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 849 | ||||
| -rw-r--r-- | powerpc/PrintAsm.mli | 13 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 741 |
9 files changed, 1978 insertions, 2010 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 7f511912..9558348a 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -19,6 +19,7 @@ open Sections open AST open Memdata open Asm +open PrintAsmaux (* Type for the ABI versions *) type float_abi_type = @@ -31,10 +32,6 @@ module type PRINTER_OPTIONS = val float_abi: float_abi_type val vfpv3: bool val hardware_idiv: bool - val cfi_startproc: out_channel -> unit - val cfi_endproc: out_channel -> unit - val cfi_adjust: out_channel -> int32 -> unit - val cfi_rel_offset: out_channel -> string -> int32 -> unit end (* Module containing the printing functions *) @@ -45,38 +42,14 @@ module AsmPrinter (Opt: PRINTER_OPTIONS) = let literals_in_code = ref true (* to be turned into a proper option *) -(* 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' - (* Basic printing functions *) -let print_symb oc symb = - fprintf oc "%s" (extern_atom symb) - -let print_label oc lbl = - fprintf oc ".L%d" (label_for_label lbl) - -let coqint oc n = - fprintf oc "%ld" (camlint_of_coqint n) +let print_label oc lbl = label oc (transl_label lbl) let comment = "@" -let print_symb_ofs oc (symb, ofs) = - print_symb oc symb; +let symbol_offset oc (symb, ofs) = + symbol oc symb; let ofs = camlint_of_coqint ofs in if ofs <> 0l then fprintf oc " + %ld" ofs @@ -254,7 +227,7 @@ let emit_constants oc = Hashtbl.iter (fun (id, ofs) lbl -> fprintf oc ".L%d: .word %a\n" - lbl print_symb_ofs (id, ofs)) + lbl symbol_offset (id, ofs)) symbol_labels; reset_constants () @@ -263,13 +236,13 @@ let emit_constants oc = let loadsymbol oc r id ofs = if !Clflags.option_mthumb then begin fprintf oc " movw %a, #:lower16:%a\n" - ireg r print_symb_ofs (id, ofs); + ireg r symbol_offset (id, ofs); fprintf oc " movt %a, #:upper16:%a\n" - ireg r print_symb_ofs (id, ofs); 2 + ireg r symbol_offset (id, ofs); 2 end else begin let lbl = label_symbol id ofs in fprintf oc " ldr %a, .L%d @ %a\n" - ireg r lbl print_symb_ofs (id, ofs); 1 + ireg r lbl symbol_offset (id, ofs); 1 end (* Emit instruction sequences that set or offset a register by a constant. *) @@ -336,8 +309,6 @@ let print_location oc loc = (* Handling of annotations *) -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - let print_annot_stmt oc txt targs args = if Str.string_match re_file_line txt 0 then begin print_file_line oc (Str.matched_group 1 txt) @@ -483,10 +454,6 @@ let print_builtin_vstore_global oc chunk id ofs args = (* Handling of varargs *) -let current_function_stacksize = ref 0l -let current_function_sig = - ref { sig_args = []; sig_res = None; sig_cc = cc_default } - let align n a = (n + a - 1) land (-a) let rec next_arg_location ir ofs = function @@ -761,7 +728,7 @@ let print_instruction oc = function fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1 | Pbsymb(id, sg) -> let n = fixup_arguments oc Outgoing sg in - fprintf oc " b %a\n" print_symb id; + fprintf oc " b %a\n" symbol id; n + 1 | Pbreg(r, sg) -> let n = @@ -772,7 +739,7 @@ let print_instruction oc = function n + 1 | Pblsymb(id, sg) -> let n1 = fixup_arguments oc Outgoing sg in - fprintf oc " bl %a\n" print_symb id; + fprintf oc " bl %a\n" symbol id; let n2 = fixup_result oc Incoming sg in n1 + 1 + n2 | Pblreg(r, sg) -> @@ -825,7 +792,7 @@ let print_instruction oc = function | Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) -> fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; begin match r1, r2, sa with - | IR14, IR13, SOimm n -> Opt.cfi_rel_offset oc "lr" (camlint_of_coqint n) + | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n) | _ -> () end; 1 @@ -969,11 +936,11 @@ let print_instruction oc = function fprintf oc " mov r12, sp\n"; if (!current_function_sig).sig_cc.cc_vararg then begin fprintf oc " push {r0, r1, r2, r3}\n"; - Opt.cfi_adjust oc 16l + cfi_adjust oc 16l end; let sz' = camlint_of_coqint sz in let ninstr = subimm oc "sp" "sp" sz in - Opt.cfi_adjust oc sz'; + cfi_adjust oc sz'; fprintf oc " str r12, [sp, #%a]\n" coqint ofs; current_function_stacksize := sz'; ninstr + (if (!current_function_sig).sig_cc.cc_vararg then 3 else 2) @@ -1084,18 +1051,17 @@ let print_function oc name fn = match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in fprintf oc " .balign %d\n" alignment; if not (C2C.atom_is_static name) then - fprintf oc " .global %a\n" print_symb name; + fprintf oc " .global %a\n" symbol name; if !Clflags.option_mthumb then fprintf oc " .thumb_func\n"; - fprintf oc "%a:\n" print_symb name; + fprintf oc "%a:\n" symbol name; print_location oc (C2C.atom_location name); - Opt.cfi_startproc oc; + cfi_startproc oc; ignore (fixup_arguments oc Incoming fn.fn_sig); print_instructions oc fn.fn_code; if !literals_in_code then emit_constants oc; - Opt.cfi_endproc oc; - fprintf oc " .type %a, %%function\n" print_symb name; - fprintf oc " .size %a, . - %a\n" print_symb name print_symb name; + cfi_endproc oc; + print_fun_info oc name; if not !literals_in_code && !size_constants > 0 then begin section oc lit; emit_constants oc @@ -1122,7 +1088,7 @@ let print_init oc = function if Z.gt n Z.zero then fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> - fprintf oc " .word %a\n" print_symb_ofs (symb, ofs) + fprintf oc " .word %a\n" symbol_offset (symb, ofs) let print_init_data oc name id = if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0 @@ -1151,18 +1117,17 @@ let print_var oc name v = fprintf oc " %s\n" name_sec; fprintf oc " .balign %d\n" align; if not (C2C.atom_is_static name) then - fprintf oc " .global %a\n" print_symb name; - fprintf oc "%a:\n" print_symb name; + fprintf oc " .global %a\n" symbol name; + fprintf oc "%a:\n" symbol name; print_init_data oc name v.gvar_init; - fprintf oc " .type %a, %%object\n" print_symb name; - fprintf oc " .size %a, . - %a\n" print_symb name print_symb name + print_var_info oc name end else begin let sz = match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in if C2C.atom_is_static name then - fprintf oc " .local %a\n" print_symb name; + fprintf oc " .local %a\n" symbol name; fprintf oc " .comm %a, %s, %d\n" - print_symb name + symbol name (Z.to_string sz) align end @@ -1190,31 +1155,6 @@ let print_program oc p = | "armv7r" | "armv7m" -> !Clflags.option_mthumb | _ -> false - - (* Emit .cfi directives *) - let cfi_startproc = - if Configuration.asm_supports_cfi then - (fun oc -> fprintf oc " .cfi_startproc\n") - else - (fun _ -> ()) - - let cfi_endproc = - if Configuration.asm_supports_cfi then - (fun oc ->fprintf oc " .cfi_endproc\n") - else - (fun _ -> ()) - - let cfi_adjust = - if Configuration.asm_supports_cfi then - (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta) - else - (fun _ _ -> ()) - - let cfi_rel_offset = - if Configuration.asm_supports_cfi then - (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs) - else - (fun _ _ _ -> ()) end in let module Printer = AsmPrinter(Opt) in diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml new file mode 100644 index 00000000..aa317a09 --- /dev/null +++ b/backend/PrintAsm.ml @@ -0,0 +1,99 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +open AST +open Asm +open Camlcoq +open Datatypes +open PrintAsmaux +open Printf +open Sections +open TargetPrinter + +module Target = (val (sel_target ()):TARGET) + +let print_location oc loc = + if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc) + +let print_function oc name fn = + Hashtbl.clear current_function_labels; + Target.reset_constants (); + let (text, lit, jmptbl) = Target.get_section_names name in + Target.section oc text; + let alignment = + match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in + Target.print_align oc alignment; + if not (C2C.atom_is_static name) then + fprintf oc " .globl %a\n" symbol name; + Target.print_optional_fun_info oc; + fprintf oc "%a:\n" symbol name; + print_location oc (C2C.atom_location name); + Target.cfi_startproc oc; + Target.print_instructions oc fn.fn_code; + Target.cfi_endproc oc; + if Target.print_fun_info then + print_fun_info oc name; + Target.emit_constants oc lit; + Target.print_jumptable oc jmptbl + + +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 (Target.print_init oc) id + +let print_var oc name v = + match v.gvar_init with + | [] -> () + | _ -> + let sec = + match C2C.atom_sections name with + | [s] -> s + | _ -> Section_data true + and align = + match C2C.atom_alignof name with + | Some a -> a + | None -> 8 in (* 8-alignment is a safe default *) + let name_sec = Target.name_of_section sec in + if name_sec <> "COMM" then begin + fprintf oc " %s\n" name_sec; + Target.print_align oc align; + if not (C2C.atom_is_static name) then + fprintf oc " .global %a\n" symbol name; + fprintf oc "%a:\n" symbol name; + print_init_data oc name v.gvar_init; + if Target.print_var_info then + print_var_info oc name; + end else + let sz = + match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in + Target.print_comm_symb oc sz name align + + +let print_globdef oc (name,gdef) = + match gdef with + | Gfun (Internal code) -> print_function oc name code + | Gfun (External ef) -> () + | Gvar v -> print_var oc name v + + +let print_program oc p = + PrintAnnot.reset_filenames (); + PrintAnnot.print_version_and_options oc Target.comment; + Target.print_prologue oc; + List.iter (print_globdef oc) p.prog_defs; + Target.print_epilogue oc; + PrintAnnot.close_filenames () diff --git a/ia32/PrintAsm.mli b/backend/PrintAsm.mli index aefe3a0a..eb63f1be 100644 --- a/ia32/PrintAsm.mli +++ b/backend/PrintAsm.mli @@ -3,6 +3,7 @@ (* The Compcert verified compiler *) (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) @@ -10,4 +11,6 @@ (* *) (* *********************************************************************) +open PrintAsmaux + val print_program: out_channel -> Asm.program -> unit diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml new file mode 100644 index 00000000..8812d320 --- /dev/null +++ b/backend/PrintAsmaux.ml @@ -0,0 +1,135 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +open AST +open Asm +open Camlcoq +open Datatypes +open Printf +open Sections + +(** Auxiliary functions for printing of asm *) + +module type TARGET = + sig + val print_prologue: out_channel -> unit + val print_epilogue: out_channel -> unit + val print_align: out_channel -> int -> unit + val print_comm_symb: out_channel -> Z.t -> P.t -> int -> unit + val print_var_info: bool + val print_fun_info: bool + val print_init: out_channel -> init_data -> unit + val reset_constants: unit -> unit + val get_section_names: P.t -> section_name * section_name * section_name + val print_file_line: out_channel -> string -> int -> unit + val print_optional_fun_info: out_channel -> unit + val cfi_startproc: out_channel -> unit + val print_instructions: out_channel -> code -> unit + val cfi_endproc: out_channel -> unit + val emit_constants: out_channel -> section_name -> unit + val print_jumptable: out_channel -> section_name -> unit + val section: out_channel -> section_name -> unit + val name_of_section: section_name -> string + val comment: string + end + +(* 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' + +let label oc lbl = + fprintf oc ".L%d" lbl + +(* List of literals and jumptables used in the code *) + +let float64_literals : (int * int64) list ref = ref [] +let float32_literals : (int * int32) list ref = ref [] +let jumptables : (int * label list) list ref = ref [] + +let reset_constants () = + float64_literals := []; + float32_literals := []; + jumptables := [] + +(* Variables used for the handling of varargs *) + +let current_function_stacksize = ref 0l +let current_function_sig = + ref { sig_args = []; sig_res = None; sig_cc = cc_default } + +(* Functions for printing of symbol names *) +let symbol oc symb = + fprintf oc "%s" (extern_atom symb) + +let symbol_offset oc (symb, ofs) = + symbol oc symb; + let ofs = camlint_of_coqint ofs in + if ofs <> 0l then fprintf oc " + %ld" ofs + +(* The comment deliminiter *) +let comment = "#" + +(* Functions for fun and var info *) +let print_fun_info oc name = + fprintf oc " .type %a, @function\n" symbol name; + fprintf oc " .size %a, . - %a\n" symbol name symbol name + +let print_var_info oc name = + fprintf oc " .type %a, @object\n" symbol name; + fprintf oc " .size %a, . - %a\n" symbol name symbol name + +(* Emit .cfi directives *) +let cfi_startproc = + if Configuration.asm_supports_cfi then + (fun oc -> fprintf oc " .cfi_startproc\n") + else + (fun _ -> ()) + +let cfi_endproc = + if Configuration.asm_supports_cfi then + (fun oc -> fprintf oc " .cfi_endproc\n") + else + (fun _ -> ()) + + +let cfi_adjust = + if Configuration.asm_supports_cfi then + (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta) + else + (fun _ _ -> ()) + +let cfi_rel_offset = + if Configuration.asm_supports_cfi then + (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs) + else + (fun _ _ _ -> ()) + +(* For handling of annotations *) +let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" + +(* Basic printing functions *) +let coqint oc n = + fprintf oc "%ld" (camlint_of_coqint n) diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml deleted file mode 100644 index b0ef0180..00000000 --- a/ia32/PrintAsm.ml +++ /dev/null @@ -1,1064 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 Sections -open AST -open Memdata -open Asm - -module StringSet = Set.Make(String) - -(* Basic printing functions used in definition of the systems *) - -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 high_int8_reg_name = function - | EAX -> "%ah" | EBX -> "%bh" | ECX -> "%ch" | EDX -> "%dh" - | _ -> assert false - -let int16_reg_name = function - | EAX -> "%ax" | EBX -> "%bx" | ECX -> "%cx" | EDX -> "%dx" - | ESI -> "%si" | EDI -> "%di" | EBP -> "%bp" | ESP -> "%sp" - -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 high_ireg8 oc r = output_string oc (high_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 preg oc = function - | IR r -> ireg oc r - | FR r -> freg oc r - | _ -> assert false - - -(* System dependend printer functions *) -module type SYSTEM = - sig - val raw_symbol: out_channel -> string -> unit - val symbol: out_channel -> P.t -> unit - val label: out_channel -> int -> unit - val name_of_section: section_name -> string - val stack_alignment: int - val print_align: out_channel -> int -> unit - val print_mov_ra: out_channel -> ireg -> ident -> unit - val print_fun_info: out_channel -> P.t -> unit - val print_var_info: out_channel -> P.t -> unit - val print_epilogue: out_channel -> unit - val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit - val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit - end - -(* Printer functions for cygwin *) -module Cygwin_System = - (struct - - let raw_symbol oc s = - fprintf oc "_%s" s - - let symbol oc symb = - fprintf oc "%s" (extern_atom symb) - - let label oc lbl = - fprintf oc "L%d" lbl - - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i then ".section .rdata,\"dr\"" else "COMM" - | Section_string -> ".section .rdata,\"dr\"" - | Section_literal -> ".section .rdata,\"dr\"" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\", \"%s\"\n" - s (if ex then "xr" else if wr then "d" else "dr") - - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) - - let print_align oc n = - fprintf oc " .align %d\n" n - - let print_mov_ra oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd - - let print_fun_info _ _ = () - - let print_var_info _ _ = () - - let print_epilogue _ = () - - let print_comm_decl oc name sz al = - fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al - - let print_lcomm_decl oc name sz al = - fprintf oc " .local %a\n" symbol name; - print_comm_decl oc name sz al - - end:SYSTEM) - -(* Printer functions for ELF *) -module ELF_System = - (struct - - let raw_symbol oc s = - fprintf oc "%s" s - - let symbol oc symb = - fprintf oc "%s" (extern_atom symb) - - let label oc lbl = - fprintf oc ".L%d" lbl - - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i then ".section .rodata" else "COMM" - | Section_string -> ".section .rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",@progbits" - s (if wr then "w" else "") (if ex then "x" else "") - - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) - - let print_align oc n = - fprintf oc " .align %d\n" n - - let print_mov_ra oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd - - let print_fun_info oc name = - fprintf oc " .type %a, @function\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name - - let print_var_info oc name = - fprintf oc " .type %a, @object\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name - - let print_epilogue _ = () - - let print_comm_decl oc name sz al = - fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al - - let print_lcomm_decl oc name sz al = - fprintf oc " .local %a\n" symbol name; - print_comm_decl oc name sz al - - end:SYSTEM) - -(* Printer functions for MacOS *) -module MacOS_System = - (struct - - let raw_symbol oc s = - fprintf oc "_%s" s - - let symbol oc symb = - fprintf oc "_%s" (extern_atom symb) - - let label oc lbl = - fprintf oc "L%d" lbl - - let name_of_section = function - | Section_text -> ".text" - | Section_data i | Section_small_data i -> - if i then ".data" else "COMM" - | Section_const i | Section_small_const i -> - if i then ".const" else "COMM" - | Section_string -> ".const" - | Section_literal -> ".literal8" - | Section_jumptable -> ".const" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\", %s, %s" - (if wr then "__DATA" else "__TEXT") s - (if ex then "regular, pure_instructions" else "regular") - - let stack_alignment = 16 (* mandatory *) - - (* 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) - - let print_align oc n = - fprintf oc " .align %d\n" (log2 n) - - let indirect_symbols : StringSet.t ref = ref StringSet.empty - - let print_mov_ra oc rd id = - let id = extern_atom id in - indirect_symbols := StringSet.add id !indirect_symbols; - fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd - - let print_fun_info _ _ = () - - let print_var_info _ _ = () - - let print_epilogue oc = - fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; - StringSet.iter - (fun s -> - fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; - fprintf oc " .indirect_symbol %a\n" raw_symbol s; - fprintf oc " .long 0\n") - !indirect_symbols; - indirect_symbols := StringSet.empty - - let print_comm_decl oc name sz al = - fprintf oc " .comm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) - - let print_lcomm_decl oc name sz al = - fprintf oc " .lcomm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) - - end:SYSTEM) - - -module AsmPrinter(Target: SYSTEM) = - (struct - open Target -(* 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 comment = "#" - -let symbol_offset oc (symb, ofs) = - symbol oc symb; - if ofs <> 0l then fprintf oc " + %ld" ofs - -let coqint oc n = - fprintf oc "%ld" (camlint_of_coqint n) - -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(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(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc - | Some r1, Some(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" - -let name_of_neg_condition = function - | Cond_e -> "ne" | Cond_ne -> "e" - | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" - | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" - | Cond_p -> "np" | Cond_np -> "p" - - -(* Names of sections *) - -let section oc sec = - fprintf oc " %s\n" (name_of_section sec) - -(* SP adjustment to allocate or free a stack frame *) - -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 sz = - let sz = camlint_of_coqint sz in - (* Preserve proper alignment of the stack *) - let sz = int32_align sz stack_alignment in - (* The top 4 bytes have already been allocated by the "call" instruction. *) - let sz = Int32.sub sz 4l in - 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 need_masks = ref false - -(* Emit .file / .loc debugging directives *) - -let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line - -let print_location oc loc = - if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) - -(* Emit .cfi directives *) - -let cfi_startproc oc = - if Configuration.asm_supports_cfi then fprintf oc " .cfi_startproc\n" - -let cfi_endproc oc = - if Configuration.asm_supports_cfi then fprintf oc " .cfi_endproc\n" - -let cfi_adjust oc delta = - if Configuration.asm_supports_cfi then - fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta - -(* Built-in functions *) - -(* Built-ins. They come in two flavors: - - annotation statements: take their arguments in registers or stack - locations; generate no code; - - inlined by the compiler: take their arguments in arbitrary - registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *) - -(* Handling of annotations *) - -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - -let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args - end - -let print_annot_val oc txt args res = - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_val preg oc txt args; - match args, res with - | [IR src], [IR dst] -> - if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst - | [FR src], [FR dst] -> - if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst - | _, _ -> assert false - -(* Handling of memcpy *) - -(* Unaligned memory accesses are quite fast on IA32, so use large - memory accesses regardless of alignment. *) - -let print_builtin_memcpy_small oc sz al src dst = - assert (src = EDX && dst = EAX); - let rec copy ofs sz = - if sz >= 8 && !Clflags.option_ffpu then begin - fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM7; - fprintf oc " movq %a, %d(%a)\n" freg XMM7 ofs ireg dst; - copy (ofs + 8) (sz - 8) - end else if sz >= 4 then begin - fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg ECX; - fprintf oc " movl %a, %d(%a)\n" ireg ECX ofs ireg dst; - copy (ofs + 4) (sz - 4) - end else if sz >= 2 then begin - fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 ECX; - fprintf oc " movw %a, %d(%a)\n" ireg16 ECX ofs ireg dst; - copy (ofs + 2) (sz - 2) - end else if sz >= 1 then begin - fprintf oc " movb %d(%a), %a\n" ofs ireg src ireg8 ECX; - fprintf oc " movb %a, %d(%a)\n" ireg8 ECX ofs ireg dst; - copy (ofs + 1) (sz - 1) - end in - copy 0 sz - -let print_builtin_memcpy_big oc sz al src dst = - assert (src = ESI && dst = EDI); - fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX; - fprintf oc " rep movsl\n"; - if sz mod 4 >= 2 then fprintf oc " movsw\n"; - if sz mod 2 >= 1 then fprintf oc " movsb\n" - -let print_builtin_memcpy oc sz al args = - let (dst, src) = - match args with [IR d; IR s] -> (d, s) | _ -> assert false in - fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" - comment sz al; - if sz <= 32 - then print_builtin_memcpy_small oc sz al src dst - else print_builtin_memcpy_big oc sz al src dst; - fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment - -(* Handling of volatile reads and writes *) - -let offset_addressing (Addrmode(base, ofs, cst)) delta = - Addrmode(base, ofs, - match cst with - | Coq_inl n -> Coq_inl(Integers.Int.add n delta) - | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) - -let print_builtin_vload_common oc chunk addr res = - match chunk, res with - | Mint8unsigned, [IR res] -> - fprintf oc " movzbl %a, %a\n" addressing addr ireg res - | Mint8signed, [IR res] -> - fprintf oc " movsbl %a, %a\n" addressing addr ireg res - | Mint16unsigned, [IR res] -> - fprintf oc " movzwl %a, %a\n" addressing addr ireg res - | Mint16signed, [IR res] -> - fprintf oc " movswl %a, %a\n" addressing addr ireg res - | Mint32, [IR res] -> - fprintf oc " movl %a, %a\n" addressing addr ireg res - | Mint64, [IR res1; IR res2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - if not (Asmgen.addressing_mentions addr res2) then begin - fprintf oc " movl %a, %a\n" addressing addr ireg res2; - fprintf oc " movl %a, %a\n" addressing addr' ireg res1 - end else begin - fprintf oc " movl %a, %a\n" addressing addr' ireg res1; - fprintf oc " movl %a, %a\n" addressing addr ireg res2 - end - | Mfloat32, [FR res] -> - fprintf oc " movss %a, %a\n" addressing addr freg res - | Mfloat64, [FR res] -> - fprintf oc " movsd %a, %a\n" addressing addr freg res - | _ -> - assert false - -let print_builtin_vload oc chunk args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - begin match args with - | [IR addr] -> - print_builtin_vload_common oc chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res - | _ -> - assert false - end; - fprintf oc "%s end builtin __builtin_volatile_read\n" comment - -let print_builtin_vload_global oc chunk id ofs args res = - fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; - print_builtin_vload_common oc chunk - (Addrmode(None, None, Coq_inr(id,ofs))) res; - fprintf oc "%s end builtin __builtin_volatile_read\n" comment - -let print_builtin_vstore_common oc chunk addr src tmp = - match chunk, src with - | (Mint8signed | Mint8unsigned), [IR src] -> - if Asmgen.low_ireg src then - fprintf oc " movb %a, %a\n" ireg8 src addressing addr - else begin - fprintf oc " movl %a, %a\n" ireg src ireg tmp; - fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr - end - | (Mint16signed | Mint16unsigned), [IR src] -> - fprintf oc " movw %a, %a\n" ireg16 src addressing addr - | Mint32, [IR src] -> - fprintf oc " movl %a, %a\n" ireg src addressing addr - | Mint64, [IR src1; IR src2] -> - let addr' = offset_addressing addr (coqint_of_camlint 4l) in - fprintf oc " movl %a, %a\n" ireg src2 addressing addr; - fprintf oc " movl %a, %a\n" ireg src1 addressing addr' - | Mfloat32, [FR src] -> - fprintf oc " movss %a, %a\n" freg src addressing addr - | Mfloat64, [FR src] -> - fprintf oc " movsd %a, %a\n" freg src addressing addr - | _ -> - assert false - -let print_builtin_vstore oc chunk args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - begin match args with - | IR addr :: src -> - print_builtin_vstore_common oc chunk - (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src - (if addr = EAX then ECX else EAX) - | _ -> - assert false - end; - fprintf oc "%s end builtin __builtin_volatile_write\n" comment - -let print_builtin_vstore_global oc chunk id ofs args = - fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; - print_builtin_vstore_common oc chunk - (Addrmode(None, None, Coq_inr(id,ofs))) args EAX; - fprintf oc "%s end builtin __builtin_volatile_write\n" comment - -(* Handling of varargs *) - -let current_function_stacksize = ref 0l -let current_function_sig = - ref { sig_args = []; sig_res = None; sig_cc = cc_default } - -let print_builtin_va_start oc r = - if not (!current_function_sig).sig_cc.cc_vararg then - invalid_arg "Fatal error: va_start used in non-vararg function"; - let ofs = - Int32.(add (add !current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions1.size_arguments - !current_function_sig)))) in - fprintf oc " movl %%esp, 0(%a)\n" ireg r; - fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r - -(* Handling of compiler-inlined builtins *) - -let print_builtin_inline oc name args res = - fprintf oc "%s begin builtin %s\n" comment name; - begin match name, args, res with - (* Integer arithmetic *) - | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> - if a1 <> res then - fprintf oc " movl %a, %a\n" ireg a1 ireg res; - fprintf oc " bswap %a\n" ireg res - | "__builtin_bswap16", [IR a1], [IR res] -> - if a1 <> res then - fprintf oc " movl %a, %a\n" ireg a1 ireg res; - fprintf oc " rolw $8, %a\n" ireg16 res - | "__builtin_clz", [IR a1], [IR res] -> - fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; - fprintf oc " xorl $31, %a\n" ireg res - | "__builtin_ctz", [IR a1], [IR res] -> - fprintf oc " bsfl %a, %a\n" ireg a1 ireg res - (* Float arithmetic *) - | "__builtin_fabs", [FR a1], [FR res] -> - need_masks := true; - if a1 <> res then - fprintf oc " movapd %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 - | "__builtin_fmax", [FR a1; FR a2], [FR res] -> - if res = a1 then - fprintf oc " maxsd %a, %a\n" freg a2 freg res - else if res = a2 then - fprintf oc " maxsd %a, %a\n" freg a1 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " maxsd %a, %a\n" freg a2 freg res - end - | "__builtin_fmin", [FR a1; FR a2], [FR res] -> - if res = a1 then - fprintf oc " minsd %a, %a\n" freg a2 freg res - else if res = a2 then - fprintf oc " minsd %a, %a\n" freg a1 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a1 freg res; - fprintf oc " minsd %a, %a\n" freg a2 freg res - end - | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"), - [FR a1; FR a2; FR a3], [FR res] -> - let opcode = - match name with - | "__builtin_fmadd" -> "vfmadd" - | "__builtin_fmsub" -> "vfmsub" - | "__builtin_fnmadd" -> "vfnmadd" - | "__builtin_fnmsub" -> "vfnmsub" - | _ -> assert false in - if res = a1 then - fprintf oc " %s132sd %a, %a, %a\n" opcode freg a2 freg a3 freg res - else if res = a2 then - fprintf oc " %s213sd %a, %a, %a\n" opcode freg a3 freg a1 freg res - else if res = a3 then - fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res - else begin - fprintf oc " movapd %a, %a\n" freg a3 freg res; - fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res - end - (* 64-bit integer arithmetic *) - | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); - fprintf oc " negl %a\n" ireg EAX; - fprintf oc " adcl $0, %a\n" ireg EDX; - fprintf oc " negl %a\n" ireg EDX - | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - fprintf oc " addl %a, %a\n" ireg EBX ireg EAX; - fprintf oc " adcl %a, %a\n" ireg ECX ireg EDX - | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> - assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); - fprintf oc " subl %a, %a\n" ireg EBX ireg EAX; - fprintf oc " sbbl %a, %a\n" ireg ECX ireg EDX - | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> - assert (a = EAX && b = EDX && rh = EDX && rl = EAX); - fprintf oc " mull %a\n" ireg EDX - (* Memory accesses *) - | "__builtin_read16_reversed", [IR a1], [IR res] -> - fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " rolw $8, %a\n" ireg16 res - | "__builtin_read32_reversed", [IR a1], [IR res] -> - fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; - fprintf oc " bswap %a\n" ireg res - | "__builtin_write16_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - if a2 <> tmp then - fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; - fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; - fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 - | "__builtin_write32_reversed", [IR a1; IR a2], _ -> - let tmp = if a1 = ECX then EDX else ECX in - if a2 <> tmp then - fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; - fprintf oc " bswap %a\n" ireg tmp; - fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 - (* Synchronization *) - | "__builtin_membar", [], _ -> - () - (* Vararg stuff *) - | "__builtin_va_start", [IR a], _ -> - print_builtin_va_start oc a - (* Catch-all *) - | _ -> - invalid_arg ("unrecognized builtin " ^ name) - end; - fprintf oc "%s end builtin %s\n" comment name - -(* Printing of instructions *) - -let float64_literals : (int * int64) list ref = ref [] -let float32_literals : (int * int32) list ref = ref [] -let jumptables : (int * label list) list ref = ref [] - -(* Reminder on AT&T syntax: op source, dest *) - -let print_instruction oc = function - (* Moves *) - | Pmov_rr(rd, r1) -> - fprintf oc " movl %a, %a\n" ireg r1 ireg rd - | Pmov_ri(rd, n) -> - fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd - | Pmov_ra(rd, id) -> - print_mov_ra oc rd id - | Pmov_rm(rd, a) | Pmov_rm_a(rd, a) -> - fprintf oc " movl %a, %a\n" addressing a ireg rd - | Pmov_mr(a, r1) | Pmov_mr_a(a, r1) -> - fprintf oc " movl %a, %a\n" ireg r1 addressing a - | Pmovsd_ff(rd, r1) -> - fprintf oc " movapd %a, %a\n" freg r1 freg rd - | Pmovsd_fi(rd, n) -> - let b = camlint64_of_coqint (Floats.Float.to_bits n) in - let lbl = new_label() in - fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat n); - float64_literals := (lbl, b) :: !float64_literals - | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> - fprintf oc " movsd %a, %a\n" addressing a freg rd - | Pmovsd_mf(a, r1) | Pmovsd_mf_a(a, r1) -> - fprintf oc " movsd %a, %a\n" freg r1 addressing a - | Pmovss_fi(rd, n) -> - let b = camlint_of_coqint (Floats.Float32.to_bits n) in - let lbl = new_label() in - fprintf oc " movss %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat32 n); - float32_literals := (lbl, b) :: !float32_literals - | Pmovss_fm(rd, a) -> - fprintf oc " movss %a, %a\n" addressing a freg rd - | Pmovss_mf(a, r1) -> - fprintf oc " movss %a, %a\n" freg r1 addressing a - | Pfldl_m(a) -> - fprintf oc " fldl %a\n" addressing a - | Pfstpl_m(a) -> - fprintf oc " fstpl %a\n" addressing a - | Pflds_m(a) -> - fprintf oc " flds %a\n" addressing a - | Pfstps_m(a) -> - fprintf oc " fstps %a\n" addressing a - | Pxchg_rr(r1, r2) -> - fprintf oc " xchgl %a, %a\n" ireg r1 ireg r2 - (** 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 - | Pcvtsd2ss_ff(rd, r1) -> - fprintf oc " cvtsd2ss %a, %a\n" freg r1 freg rd - | Pcvtss2sd_ff(rd, r1) -> - fprintf oc " cvtss2sd %a, %a\n" freg r1 freg rd - | 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 - | Pcvttss2si_rf(rd, r1) -> - fprintf oc " cvttss2si %a, %a\n" freg r1 ireg rd - | Pcvtsi2ss_fr(rd, r1) -> - fprintf oc " cvtsi2ss %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 - | Pimul_r(r1) -> - fprintf oc " imull %a\n" ireg r1 - | Pmul_r(r1) -> - fprintf oc " mull %a\n" ireg r1 - | 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_r(rd) -> - fprintf oc " xorl %a, %a\n" ireg rd 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 - | Pnot(rd) -> - fprintf oc " notl %a\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 - | Pshld_ri(rd, r1, n) -> - fprintf oc " shldl $%a, %a, %a\n" coqint n ireg r1 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) -> - fprintf oc " cmov%s %a, %a\n" (name_of_condition c) ireg r1 ireg rd - | Psetcc(c, rd) -> - fprintf oc " set%s %a\n" (name_of_condition c) ireg8 rd; - fprintf oc " movzbl %a, %a\n" ireg8 rd 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 - | Pxorpd_f (rd) -> - fprintf oc " xorpd %a, %a\n" freg rd freg rd - | Padds_ff(rd, r1) -> - fprintf oc " addss %a, %a\n" freg r1 freg rd - | Psubs_ff(rd, r1) -> - fprintf oc " subss %a, %a\n" freg r1 freg rd - | Pmuls_ff(rd, r1) -> - fprintf oc " mulss %a, %a\n" freg r1 freg rd - | Pdivs_ff(rd, r1) -> - fprintf oc " divss %a, %a\n" freg r1 freg rd - | Pnegs (rd) -> - need_masks := true; - fprintf oc " xorpd %a, %a\n" raw_symbol "__negs_mask" freg rd - | Pabss (rd) -> - need_masks := true; - fprintf oc " andpd %a, %a\n" raw_symbol "__abss_mask" freg rd - | Pcomiss_ff(r1, r2) -> - fprintf oc " comiss %a, %a\n" freg r2 freg r1 - | Pxorps_f (rd) -> - fprintf oc " xorpd %a, %a\n" freg rd freg rd - (** Branches and calls *) - | Pjmp_l(l) -> - fprintf oc " jmp %a\n" label (transl_label l) - | Pjmp_s(f, sg) -> - fprintf oc " jmp %a\n" symbol f - | Pjmp_r(r, sg) -> - fprintf oc " jmp *%a\n" ireg r - | Pjcc(c, l) -> - let l = transl_label l in - fprintf oc " j%s %a\n" (name_of_condition c) label l - | Pjcc2(c1, c2, l) -> - let l = transl_label l in - let l' = new_label() in - fprintf oc " j%s %a\n" (name_of_neg_condition c1) label l'; - fprintf oc " j%s %a\n" (name_of_condition c2) label l; - fprintf oc "%a:\n" label l' - | 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, sg) -> - fprintf oc " call %a\n" symbol f - | Pcall_r(r, sg) -> - fprintf oc " call *%a\n" ireg r - | Pret -> - fprintf oc " ret\n" - (** Pseudo-instructions *) - | Plabel(l) -> - fprintf oc "%a:\n" label (transl_label l) - | Pallocframe(sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - let ofs_link = camlint_of_coqint ofs_link in - fprintf oc " subl $%ld, %%esp\n" sz; - cfi_adjust oc sz; - fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); - fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link; - current_function_stacksize := sz - | Pfreeframe(sz, ofs_ra, ofs_link) -> - let sz = sp_adjustment sz in - fprintf oc " addl $%ld, %%esp\n" sz - | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_builtin(name, sg) -> - print_builtin_inline oc (extern_atom name) args res - | EF_vload chunk -> - print_builtin_vload oc chunk args res - | EF_vstore chunk -> - print_builtin_vstore oc chunk args - | EF_vload_global(chunk, id, ofs) -> - print_builtin_vload_global oc chunk id ofs args res - | EF_vstore_global(chunk, id, ofs) -> - print_builtin_vstore_global oc chunk id ofs args - | EF_memcpy(sz, al) -> - print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) - (Int32.to_int (camlint_of_coqint al)) args - | EF_annot_val(txt, targ) -> - print_annot_val oc (extern_atom txt) args res - | EF_inline_asm txt -> - fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); - fprintf oc "%s end inline assembly\n" comment - | _ -> - assert false - end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args - | _ -> - assert false - end - -let print_literal64 oc (lbl, n) = - fprintf oc "%a: .quad 0x%Lx\n" label lbl n -let print_literal32 oc (lbl, n) = - fprintf oc "%a: .long 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 print_function oc name fn = - Hashtbl.clear current_function_labels; - float64_literals := []; float32_literals := []; - jumptables := []; - current_function_sig := fn.fn_sig; - let (text, lit, jmptbl) = - match C2C.atom_sections name with - | [t;l;j] -> (t, l, j) - | _ -> (Section_text, Section_literal, Section_jumptable) in - section oc text; - let alignment = - match !Clflags.option_falignfunctions with Some n -> n | None -> 16 in - print_align oc alignment; - if not (C2C.atom_is_static name) then - fprintf oc " .globl %a\n" symbol name; - fprintf oc "%a:\n" symbol name; - print_location oc (C2C.atom_location name); - cfi_startproc oc; - List.iter (print_instruction oc) fn.fn_code; - cfi_endproc oc; - print_fun_info oc name; - if !float64_literals <> [] || !float32_literals <> [] then begin - section oc lit; - print_align oc 8; - List.iter (print_literal64 oc) !float64_literals; - float64_literals := []; - List.iter (print_literal32 oc) !float32_literals; - float32_literals := [] - end; - if !jumptables <> [] then begin - section oc jmptbl; - print_align oc 4; - List.iter (print_jumptable oc) !jumptables; - jumptables := [] - end - -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_int64 n -> - fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) - | Init_float32 n -> - fprintf oc " .long %ld %s %.18g\n" - (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_float64 n -> - fprintf oc " .quad %Ld %s %.18g\n" - (camlint64_of_coqint (Floats.Float.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string 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 name v = - match v.gvar_init with - | [] -> () - | _ -> - let sec = - match C2C.atom_sections name with - | [s] -> s - | _ -> Section_data true - and align = - match C2C.atom_alignof name with - | Some a -> a - | None -> 8 in (* 8-alignment is a safe default *) - let name_sec = - name_of_section sec in - if name_sec <> "COMM" then begin - fprintf oc " %s\n" name_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; - print_var_info oc name - end else begin - let sz = - match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in - if C2C.atom_is_static name - then Target.print_lcomm_decl oc name sz align - else Target.print_comm_decl oc name sz align - end - -let print_globdef oc (name, gdef) = - match gdef with - | Gfun(Internal code) -> print_function oc name code - | Gfun(External ef) -> () - | Gvar v -> print_var oc name v -end) - -type target = ELF | MacOS | Cygwin - -let print_program oc p = - let target = - match Configuration.system with - | "macosx" -> MacOS - | "linux" -> ELF - | "bsd" -> ELF - | "cygwin" -> Cygwin - | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") in - let module Target = (val (match target with - | MacOS -> (module MacOS_System:SYSTEM) - | ELF -> (module ELF_System:SYSTEM) - | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in - let module Printer = AsmPrinter(Target) in - PrintAnnot.print_version_and_options oc Printer.comment; - PrintAnnot.reset_filenames(); - Printer.need_masks := false; - List.iter (Printer.print_globdef oc) p.prog_defs; - if !Printer.need_masks then begin - Printer.section oc (Section_const true); - (* not Section_literal because not 8-bytes *) - Target.print_align oc 16; - fprintf oc "%a: .quad 0x8000000000000000, 0\n" - Target.raw_symbol "__negd_mask"; - fprintf oc "%a: .quad 0x7FFFFFFFFFFFFFFF, 0xFFFFFFFFFFFFFFFF\n" - Target.raw_symbol "__absd_mask"; - fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" - Target.raw_symbol "__negs_mask"; - fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" - Target.raw_symbol "__abss_mask" - end; - Target.print_epilogue oc; - PrintAnnot.close_filenames() diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml new file mode 100644 index 00000000..5bb0eec4 --- /dev/null +++ b/ia32/TargetPrinter.ml @@ -0,0 +1,976 @@ +(* *********************************************************************) +(* *) +(* 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 Sections +open AST +open Memdata +open Asm +open PrintAsmaux + +module StringSet = Set.Make(String) + +(* Basic printing functions used in definition of the systems *) + +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 high_int8_reg_name = function + | EAX -> "%ah" | EBX -> "%bh" | ECX -> "%ch" | EDX -> "%dh" + | _ -> assert false + +let int16_reg_name = function + | EAX -> "%ax" | EBX -> "%bx" | ECX -> "%cx" | EDX -> "%dx" + | ESI -> "%si" | EDI -> "%di" | EBP -> "%bp" | ESP -> "%sp" + +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 high_ireg8 oc r = output_string oc (high_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 preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + + +(* System dependend printer functions *) +module type SYSTEM = + sig + val raw_symbol: out_channel -> string -> unit + val symbol: out_channel -> P.t -> unit + val label: out_channel -> int -> unit + val name_of_section: section_name -> string + val stack_alignment: int + val print_align: out_channel -> int -> unit + val print_mov_ra: out_channel -> ireg -> ident -> unit + val print_fun_info: bool + val print_var_info: bool + val print_epilogue: out_channel -> unit + val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit + val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit + end + +(* Printer functions for cygwin *) +module Cygwin_System = + (struct + + let raw_symbol oc s = + fprintf oc "_%s" s + + let symbol = symbol + + let label oc lbl = + fprintf oc "L%d" lbl + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rdata,\"dr\"" else "COMM" + | Section_string -> ".section .rdata,\"dr\"" + | Section_literal -> ".section .rdata,\"dr\"" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\", \"%s\"\n" + s (if ex then "xr" else if wr then "d" else "dr") + + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + + let print_align oc n = + fprintf oc " .align %d\n" n + + let print_mov_ra oc rd id = + fprintf oc " movl $%a, %a\n" symbol id ireg rd + + let print_fun_info = false + + let print_var_info = false + + let print_epilogue _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + + end:SYSTEM) + +(* Printer functions for ELF *) +module ELF_System = + (struct + + let raw_symbol oc s = + fprintf oc "%s" s + + let symbol = symbol + + let label = label + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".section .rodata" else "COMM" + | Section_string -> ".section .rodata" + | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + + let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + + let print_align oc n = + fprintf oc " .align %d\n" n + + let print_mov_ra oc rd id = + fprintf oc " movl $%a, %a\n" symbol id ireg rd + + let print_fun_info = true + + let print_var_info = true + + let print_epilogue _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + + end:SYSTEM) + +(* Printer functions for MacOS *) +module MacOS_System = + (struct + + let raw_symbol oc s = + fprintf oc "_%s" s + + let symbol oc symb = + fprintf oc "_%s" (extern_atom symb) + + let label oc lbl = + fprintf oc "L%d" lbl + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + if i then ".data" else "COMM" + | Section_const i | Section_small_const i -> + if i then ".const" else "COMM" + | Section_string -> ".const" + | Section_literal -> ".literal8" + | Section_jumptable -> ".const" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\", %s, %s" + (if wr then "__DATA" else "__TEXT") s + (if ex then "regular, pure_instructions" else "regular") + + let stack_alignment = 16 (* mandatory *) + + (* 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) + + let print_align oc n = + fprintf oc " .align %d\n" (log2 n) + + let indirect_symbols : StringSet.t ref = ref StringSet.empty + + let print_mov_ra oc rd id = + let id = extern_atom id in + indirect_symbols := StringSet.add id !indirect_symbols; + fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd + + let print_fun_info = false + + let print_var_info = false + + let print_epilogue oc = + fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; + StringSet.iter + (fun s -> + fprintf oc "L%a$non_lazy_ptr:\n" raw_symbol s; + fprintf oc " .indirect_symbol %a\n" raw_symbol s; + fprintf oc " .long 0\n") + !indirect_symbols; + indirect_symbols := StringSet.empty + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + let print_lcomm_decl oc name sz al = + fprintf oc " .lcomm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + end:SYSTEM) + + +module Target(System: SYSTEM):TARGET = + (struct + open System + +(* Basic printing functions *) + + let symbol_offset oc (symb, ofs) = + symbol oc symb; + if ofs <> 0l then fprintf oc " + %ld" ofs + + + 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(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(r2,sc) -> fprintf oc "(,%a,%a)" ireg r2 coqint sc + | Some r1, Some(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" + + let name_of_neg_condition = function + | Cond_e -> "ne" | Cond_ne -> "e" + | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" + | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" + | Cond_p -> "np" | Cond_np -> "p" + + +(* Names of sections *) + + let section oc sec = + fprintf oc " %s\n" (name_of_section sec) + +(* SP adjustment to allocate or free a stack frame *) + + 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 sz = + let sz = camlint_of_coqint sz in + (* Preserve proper alignment of the stack *) + let sz = int32_align sz stack_alignment in + (* The top 4 bytes have already been allocated by the "call" instruction. *) + let sz = Int32.sub sz 4l in + 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 need_masks = ref false + +(* Emit .file / .loc debugging directives *) + + let print_file_line oc file line = + PrintAnnot.print_file_line oc comment file line + + let print_location oc loc = + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) + + +(* Built-in functions *) + +(* Built-ins. They come in two flavors: + - annotation statements: take their arguments in registers or stack + locations; generate no code; + - inlined by the compiler: take their arguments in arbitrary + registers; preserve all registers except ECX, EDX, XMM6 and XMM7. *) + +(* Handling of annotations *) + + let print_annot_stmt oc txt targs args = + if Str.string_match re_file_line txt 0 then begin + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) + end else begin + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_stmt preg "ESP" oc txt targs args + end + + let print_annot_val oc txt args res = + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_val preg oc txt args; + match args, res with + | [IR src], [IR dst] -> + if dst <> src then fprintf oc " movl %a, %a\n" ireg src ireg dst + | [FR src], [FR dst] -> + if dst <> src then fprintf oc " movapd %a, %a\n" freg src freg dst + | _, _ -> assert false + +(* Handling of memcpy *) + +(* Unaligned memory accesses are quite fast on IA32, so use large + memory accesses regardless of alignment. *) + + let print_builtin_memcpy_small oc sz al src dst = + assert (src = EDX && dst = EAX); + let rec copy ofs sz = + if sz >= 8 && !Clflags.option_ffpu then begin + fprintf oc " movq %d(%a), %a\n" ofs ireg src freg XMM7; + fprintf oc " movq %a, %d(%a)\n" freg XMM7 ofs ireg dst; + copy (ofs + 8) (sz - 8) + end else if sz >= 4 then begin + fprintf oc " movl %d(%a), %a\n" ofs ireg src ireg ECX; + fprintf oc " movl %a, %d(%a)\n" ireg ECX ofs ireg dst; + copy (ofs + 4) (sz - 4) + end else if sz >= 2 then begin + fprintf oc " movw %d(%a), %a\n" ofs ireg src ireg16 ECX; + fprintf oc " movw %a, %d(%a)\n" ireg16 ECX ofs ireg dst; + copy (ofs + 2) (sz - 2) + end else if sz >= 1 then begin + fprintf oc " movb %d(%a), %a\n" ofs ireg src ireg8 ECX; + fprintf oc " movb %a, %d(%a)\n" ireg8 ECX ofs ireg dst; + copy (ofs + 1) (sz - 1) + end in + copy 0 sz + + let print_builtin_memcpy_big oc sz al src dst = + assert (src = ESI && dst = EDI); + fprintf oc " movl $%d, %a\n" (sz / 4) ireg ECX; + fprintf oc " rep movsl\n"; + if sz mod 4 >= 2 then fprintf oc " movsw\n"; + if sz mod 2 >= 1 then fprintf oc " movsb\n" + + let print_builtin_memcpy oc sz al args = + let (dst, src) = + match args with [IR d; IR s] -> (d, s) | _ -> assert false in + fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n" + comment sz al; + if sz <= 32 + then print_builtin_memcpy_small oc sz al src dst + else print_builtin_memcpy_big oc sz al src dst; + fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment + +(* Handling of volatile reads and writes *) + + let offset_addressing (Addrmode(base, ofs, cst)) delta = + Addrmode(base, ofs, + match cst with + | Coq_inl n -> Coq_inl(Integers.Int.add n delta) + | Coq_inr(id, n) -> Coq_inr(id, Integers.Int.add n delta)) + + let print_builtin_vload_common oc chunk addr res = + match chunk, res with + | Mint8unsigned, [IR res] -> + fprintf oc " movzbl %a, %a\n" addressing addr ireg res + | Mint8signed, [IR res] -> + fprintf oc " movsbl %a, %a\n" addressing addr ireg res + | Mint16unsigned, [IR res] -> + fprintf oc " movzwl %a, %a\n" addressing addr ireg res + | Mint16signed, [IR res] -> + fprintf oc " movswl %a, %a\n" addressing addr ireg res + | Mint32, [IR res] -> + fprintf oc " movl %a, %a\n" addressing addr ireg res + | Mint64, [IR res1; IR res2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + if not (Asmgen.addressing_mentions addr res2) then begin + fprintf oc " movl %a, %a\n" addressing addr ireg res2; + fprintf oc " movl %a, %a\n" addressing addr' ireg res1 + end else begin + fprintf oc " movl %a, %a\n" addressing addr' ireg res1; + fprintf oc " movl %a, %a\n" addressing addr ireg res2 + end + | Mfloat32, [FR res] -> + fprintf oc " movss %a, %a\n" addressing addr freg res + | Mfloat64, [FR res] -> + fprintf oc " movsd %a, %a\n" addressing addr freg res + | _ -> + assert false + + let print_builtin_vload oc chunk args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + begin match args with + | [IR addr] -> + print_builtin_vload_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) res + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + + let print_builtin_vload_global oc chunk id ofs args res = + fprintf oc "%s begin builtin __builtin_volatile_read\n" comment; + print_builtin_vload_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) res; + fprintf oc "%s end builtin __builtin_volatile_read\n" comment + + let print_builtin_vstore_common oc chunk addr src tmp = + match chunk, src with + | (Mint8signed | Mint8unsigned), [IR src] -> + if Asmgen.low_ireg src then + fprintf oc " movb %a, %a\n" ireg8 src addressing addr + else begin + fprintf oc " movl %a, %a\n" ireg src ireg tmp; + fprintf oc " movb %a, %a\n" ireg8 tmp addressing addr + end + | (Mint16signed | Mint16unsigned), [IR src] -> + fprintf oc " movw %a, %a\n" ireg16 src addressing addr + | Mint32, [IR src] -> + fprintf oc " movl %a, %a\n" ireg src addressing addr + | Mint64, [IR src1; IR src2] -> + let addr' = offset_addressing addr (coqint_of_camlint 4l) in + fprintf oc " movl %a, %a\n" ireg src2 addressing addr; + fprintf oc " movl %a, %a\n" ireg src1 addressing addr' + | Mfloat32, [FR src] -> + fprintf oc " movss %a, %a\n" freg src addressing addr + | Mfloat64, [FR src] -> + fprintf oc " movsd %a, %a\n" freg src addressing addr + | _ -> + assert false + + let print_builtin_vstore oc chunk args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + begin match args with + | IR addr :: src -> + print_builtin_vstore_common oc chunk + (Addrmode(Some addr, None, Coq_inl Integers.Int.zero)) src + (if addr = EAX then ECX else EAX) + | _ -> + assert false + end; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + + let print_builtin_vstore_global oc chunk id ofs args = + fprintf oc "%s begin builtin __builtin_volatile_write\n" comment; + print_builtin_vstore_common oc chunk + (Addrmode(None, None, Coq_inr(id,ofs))) args EAX; + fprintf oc "%s end builtin __builtin_volatile_write\n" comment + +(* Handling of varargs *) + + let print_builtin_va_start oc r = + if not (!current_function_sig).sig_cc.cc_vararg then + invalid_arg "Fatal error: va_start used in non-vararg function"; + let ofs = + Int32.(add (add !current_function_stacksize 4l) + (mul 4l (Z.to_int32 (Conventions1.size_arguments + !current_function_sig)))) in + fprintf oc " movl %%esp, 0(%a)\n" ireg r; + fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r + +(* Handling of compiler-inlined builtins *) + + let print_builtin_inline oc name args res = + fprintf oc "%s begin builtin %s\n" comment name; + begin match name, args, res with + (* Integer arithmetic *) + | ("__builtin_bswap"| "__builtin_bswap32"), [IR a1], [IR res] -> + if a1 <> res then + fprintf oc " movl %a, %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res + | "__builtin_bswap16", [IR a1], [IR res] -> + if a1 <> res then + fprintf oc " movl %a, %a\n" ireg a1 ireg res; + fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_clz", [IR a1], [IR res] -> + fprintf oc " bsrl %a, %a\n" ireg a1 ireg res; + fprintf oc " xorl $31, %a\n" ireg res + | "__builtin_ctz", [IR a1], [IR res] -> + fprintf oc " bsfl %a, %a\n" ireg a1 ireg res + (* Float arithmetic *) + | "__builtin_fabs", [FR a1], [FR res] -> + need_masks := true; + if a1 <> res then + fprintf oc " movapd %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 + | "__builtin_fmax", [FR a1; FR a2], [FR res] -> + if res = a1 then + fprintf oc " maxsd %a, %a\n" freg a2 freg res + else if res = a2 then + fprintf oc " maxsd %a, %a\n" freg a1 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " maxsd %a, %a\n" freg a2 freg res + end + | "__builtin_fmin", [FR a1; FR a2], [FR res] -> + if res = a1 then + fprintf oc " minsd %a, %a\n" freg a2 freg res + else if res = a2 then + fprintf oc " minsd %a, %a\n" freg a1 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a1 freg res; + fprintf oc " minsd %a, %a\n" freg a2 freg res + end + | ("__builtin_fmadd"|"__builtin_fmsub"|"__builtin_fnmadd"|"__builtin_fnmsub"), + [FR a1; FR a2; FR a3], [FR res] -> + let opcode = + match name with + | "__builtin_fmadd" -> "vfmadd" + | "__builtin_fmsub" -> "vfmsub" + | "__builtin_fnmadd" -> "vfnmadd" + | "__builtin_fnmsub" -> "vfnmsub" + | _ -> assert false in + if res = a1 then + fprintf oc " %s132sd %a, %a, %a\n" opcode freg a2 freg a3 freg res + else if res = a2 then + fprintf oc " %s213sd %a, %a, %a\n" opcode freg a3 freg a1 freg res + else if res = a3 then + fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res + else begin + fprintf oc " movapd %a, %a\n" freg a3 freg res; + fprintf oc " %s231sd %a, %a, %a\n" opcode freg a1 freg a2 freg res + end + (* 64-bit integer arithmetic *) + | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && rh = EDX && rl = EAX); + fprintf oc " negl %a\n" ireg EAX; + fprintf oc " adcl $0, %a\n" ireg EDX; + fprintf oc " negl %a\n" ireg EDX + | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + fprintf oc " addl %a, %a\n" ireg EBX ireg EAX; + fprintf oc " adcl %a, %a\n" ireg ECX ireg EDX + | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] -> + assert (ah = EDX && al = EAX && bh = ECX && bl = EBX && rh = EDX && rl = EAX); + fprintf oc " subl %a, %a\n" ireg EBX ireg EAX; + fprintf oc " sbbl %a, %a\n" ireg ECX ireg EDX + | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] -> + assert (a = EAX && b = EDX && rh = EDX && rl = EAX); + fprintf oc " mull %a\n" ireg EDX + (* Memory accesses *) + | "__builtin_read16_reversed", [IR a1], [IR res] -> + fprintf oc " movzwl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " rolw $8, %a\n" ireg16 res + | "__builtin_read32_reversed", [IR a1], [IR res] -> + fprintf oc " movl 0(%a), %a\n" ireg a1 ireg res; + fprintf oc " bswap %a\n" ireg res + | "__builtin_write16_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; + fprintf oc " xchg %a, %a\n" ireg8 tmp high_ireg8 tmp; + fprintf oc " movw %a, 0(%a)\n" ireg16 tmp ireg a1 + | "__builtin_write32_reversed", [IR a1; IR a2], _ -> + let tmp = if a1 = ECX then EDX else ECX in + if a2 <> tmp then + fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; + fprintf oc " bswap %a\n" ireg tmp; + fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 + (* Synchronization *) + | "__builtin_membar", [], _ -> + () + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + end; + fprintf oc "%s end builtin %s\n" comment name + +(* Printing of instructions *) + +(* Reminder on AT&T syntax: op source, dest *) + + let print_instruction oc = function + (* Moves *) + | Pmov_rr(rd, r1) -> + fprintf oc " movl %a, %a\n" ireg r1 ireg rd + | Pmov_ri(rd, n) -> + fprintf oc " movl $%ld, %a\n" (camlint_of_coqint n) ireg rd + | Pmov_ra(rd, id) -> + print_mov_ra oc rd id + | Pmov_rm(rd, a) | Pmov_rm_a(rd, a) -> + fprintf oc " movl %a, %a\n" addressing a ireg rd + | Pmov_mr(a, r1) | Pmov_mr_a(a, r1) -> + fprintf oc " movl %a, %a\n" ireg r1 addressing a + | Pmovsd_ff(rd, r1) -> + fprintf oc " movapd %a, %a\n" freg r1 freg rd + | Pmovsd_fi(rd, n) -> + let b = camlint64_of_coqint (Floats.Float.to_bits n) in + let lbl = new_label() in + fprintf oc " movsd %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat n); + float64_literals := (lbl, b) :: !float64_literals + | Pmovsd_fm(rd, a) | Pmovsd_fm_a(rd, a) -> + fprintf oc " movsd %a, %a\n" addressing a freg rd + | Pmovsd_mf(a, r1) | Pmovsd_mf_a(a, r1) -> + fprintf oc " movsd %a, %a\n" freg r1 addressing a + | Pmovss_fi(rd, n) -> + let b = camlint_of_coqint (Floats.Float32.to_bits n) in + let lbl = new_label() in + fprintf oc " movss %a, %a %s %.18g\n" label lbl freg rd comment (camlfloat_of_coqfloat32 n); + float32_literals := (lbl, b) :: !float32_literals + | Pmovss_fm(rd, a) -> + fprintf oc " movss %a, %a\n" addressing a freg rd + | Pmovss_mf(a, r1) -> + fprintf oc " movss %a, %a\n" freg r1 addressing a + | Pfldl_m(a) -> + fprintf oc " fldl %a\n" addressing a + | Pfstpl_m(a) -> + fprintf oc " fstpl %a\n" addressing a + | Pflds_m(a) -> + fprintf oc " flds %a\n" addressing a + | Pfstps_m(a) -> + fprintf oc " fstps %a\n" addressing a + | Pxchg_rr(r1, r2) -> + fprintf oc " xchgl %a, %a\n" ireg r1 ireg r2 + (** 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 + | Pcvtsd2ss_ff(rd, r1) -> + fprintf oc " cvtsd2ss %a, %a\n" freg r1 freg rd + | Pcvtss2sd_ff(rd, r1) -> + fprintf oc " cvtss2sd %a, %a\n" freg r1 freg rd + | 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 + | Pcvttss2si_rf(rd, r1) -> + fprintf oc " cvttss2si %a, %a\n" freg r1 ireg rd + | Pcvtsi2ss_fr(rd, r1) -> + fprintf oc " cvtsi2ss %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 + | Pimul_r(r1) -> + fprintf oc " imull %a\n" ireg r1 + | Pmul_r(r1) -> + fprintf oc " mull %a\n" ireg r1 + | 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_r(rd) -> + fprintf oc " xorl %a, %a\n" ireg rd 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 + | Pnot(rd) -> + fprintf oc " notl %a\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 + | Pshld_ri(rd, r1, n) -> + fprintf oc " shldl $%a, %a, %a\n" coqint n ireg r1 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) -> + fprintf oc " cmov%s %a, %a\n" (name_of_condition c) ireg r1 ireg rd + | Psetcc(c, rd) -> + fprintf oc " set%s %a\n" (name_of_condition c) ireg8 rd; + fprintf oc " movzbl %a, %a\n" ireg8 rd 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 + | Pxorpd_f (rd) -> + fprintf oc " xorpd %a, %a\n" freg rd freg rd + | Padds_ff(rd, r1) -> + fprintf oc " addss %a, %a\n" freg r1 freg rd + | Psubs_ff(rd, r1) -> + fprintf oc " subss %a, %a\n" freg r1 freg rd + | Pmuls_ff(rd, r1) -> + fprintf oc " mulss %a, %a\n" freg r1 freg rd + | Pdivs_ff(rd, r1) -> + fprintf oc " divss %a, %a\n" freg r1 freg rd + | Pnegs (rd) -> + need_masks := true; + fprintf oc " xorpd %a, %a\n" raw_symbol "__negs_mask" freg rd + | Pabss (rd) -> + need_masks := true; + fprintf oc " andpd %a, %a\n" raw_symbol "__abss_mask" freg rd + | Pcomiss_ff(r1, r2) -> + fprintf oc " comiss %a, %a\n" freg r2 freg r1 + | Pxorps_f (rd) -> + fprintf oc " xorpd %a, %a\n" freg rd freg rd + (** Branches and calls *) + | Pjmp_l(l) -> + fprintf oc " jmp %a\n" label (transl_label l) + | Pjmp_s(f, sg) -> + fprintf oc " jmp %a\n" symbol f + | Pjmp_r(r, sg) -> + fprintf oc " jmp *%a\n" ireg r + | Pjcc(c, l) -> + let l = transl_label l in + fprintf oc " j%s %a\n" (name_of_condition c) label l + | Pjcc2(c1, c2, l) -> + let l = transl_label l in + let l' = new_label() in + fprintf oc " j%s %a\n" (name_of_neg_condition c1) label l'; + fprintf oc " j%s %a\n" (name_of_condition c2) label l; + fprintf oc "%a:\n" label l' + | 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, sg) -> + fprintf oc " call %a\n" symbol f + | Pcall_r(r, sg) -> + fprintf oc " call *%a\n" ireg r + | Pret -> + fprintf oc " ret\n" + (** Pseudo-instructions *) + | Plabel(l) -> + fprintf oc "%a:\n" label (transl_label l) + | Pallocframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in + let ofs_link = camlint_of_coqint ofs_link in + fprintf oc " subl $%ld, %%esp\n" sz; + cfi_adjust oc sz; + fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); + fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link; + current_function_stacksize := sz + | Pfreeframe(sz, ofs_ra, ofs_link) -> + let sz = sp_adjustment sz in + fprintf oc " addl $%ld, %%esp\n" sz + | Pbuiltin(ef, args, res) -> + begin match ef with + | EF_builtin(name, sg) -> + print_builtin_inline oc (extern_atom name) args res + | EF_vload chunk -> + print_builtin_vload oc chunk args res + | EF_vstore chunk -> + print_builtin_vstore oc chunk args + | EF_vload_global(chunk, id, ofs) -> + print_builtin_vload_global oc chunk id ofs args res + | EF_vstore_global(chunk, id, ofs) -> + print_builtin_vstore_global oc chunk id ofs args + | EF_memcpy(sz, al) -> + print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz)) + (Int32.to_int (camlint_of_coqint al)) args + | EF_annot_val(txt, targ) -> + print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment + | _ -> + assert false + end + | Pannot(ef, args) -> + begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args + | _ -> + assert false + end + + let print_literal64 oc (lbl, n) = + fprintf oc "%a: .quad 0x%Lx\n" label lbl n + let print_literal32 oc (lbl, n) = + fprintf oc "%a: .long 0x%lx\n" label lbl n + + let print_jumptable oc jmptbl = + 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 in + if !jumptables <> [] then begin + section oc jmptbl; + print_align oc 4; + List.iter (print_jumptable oc) !jumptables; + jumptables := [] + end + + 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_int64 n -> + fprintf oc " .quad %Ld\n" (camlint64_of_coqint n) + | Init_float32 n -> + fprintf oc " .long %ld %s %.18g\n" + (camlint_of_coqint (Floats.Float32.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_float64 n -> + fprintf oc " .quad %Ld %s %.18g\n" + (camlint64_of_coqint (Floats.Float.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_space n -> + if Z.gt n Z.zero then + fprintf oc " .space %s\n" (Z.to_string n) + | Init_addrof(symb, ofs) -> + fprintf oc " .long %a\n" + symbol_offset (symb, camlint_of_coqint ofs) + + let print_align = print_align + + let print_comm_symb oc sz name align = + if C2C.atom_is_static name + then System.print_lcomm_decl oc name sz align + else System.print_comm_decl oc name sz align + + let comment = comment + + let name_of_section = name_of_section + + let emit_constants oc lit = + if !float64_literals <> [] || !float32_literals <> [] then begin + section oc lit; + print_align oc 8; + List.iter (print_literal64 oc) !float64_literals; + float64_literals := []; + List.iter (print_literal32 oc) !float32_literals; + float32_literals := [] + end + + let cfi_startproc = cfi_startproc + let cfi_endproc = cfi_endproc + + let print_instructions oc code = List.iter (print_instruction oc) code + + let print_optional_fun_info _ = () + + let get_section_names name = + match C2C.atom_sections name with + | [t;l;j] -> (t, l, j) + | _ -> (Section_text, Section_literal, Section_jumptable) + + let reset_constants = reset_constants + + let print_fun_info = print_fun_info + + let print_var_info = print_var_info + + let print_prologue _ = + need_masks := false + + let print_epilogue oc = + if !need_masks then begin + section oc (Section_const true); + (* not Section_literal because not 8-bytes *) + 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"; + fprintf oc "%a: .long 0x80000000, 0, 0, 0\n" + raw_symbol "__negs_mask"; + fprintf oc "%a: .long 0x7FFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF\n" + raw_symbol "__abss_mask" + end; + System.print_epilogue oc; +end) + +let sel_target () = + let module S = (val (match Configuration.system with + | "macosx" -> (module MacOS_System:SYSTEM) + | "linux" + | "bsd" -> (module ELF_System:SYSTEM) + | "cygwin" -> (module Cygwin_System:SYSTEM) + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in + (module Target(S):TARGET) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml deleted file mode 100644 index 0c4356ec..00000000 --- a/powerpc/PrintAsm.ml +++ /dev/null @@ -1,849 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 Maps -open Camlcoq -open Sections -open AST -open Memdata -open Asm - -(* Recognition of target ABI and asm syntax *) - -module type SYSTEM = - sig - val comment: string - val constant: out_channel -> constant -> unit - val ireg: out_channel -> ireg -> unit - val freg: out_channel -> freg -> unit - val creg: out_channel -> int -> unit - val name_of_section: section_name -> string - val print_file_line: out_channel -> string -> int -> unit - val cfi_startproc: out_channel -> unit - val cfi_endproc: out_channel -> unit - val cfi_adjust: out_channel -> int32 -> unit - val cfi_rel_offset: out_channel -> string -> int32 -> unit - val print_prologue: out_channel -> unit - end - -let symbol oc symb = - fprintf oc "%s" (extern_atom symb) - -let symbol_offset oc (symb, ofs) = - symbol oc symb; - if ofs <> 0l then fprintf oc " + %ld" ofs - -let symbol_fragment oc s n op = - fprintf oc "(%a)%s" symbol_offset (s, camlint_of_coqint n) op - - -let int_reg_name = function - | GPR0 -> "0" | GPR1 -> "1" | GPR2 -> "2" | GPR3 -> "3" - | GPR4 -> "4" | GPR5 -> "5" | GPR6 -> "6" | GPR7 -> "7" - | GPR8 -> "8" | GPR9 -> "9" | GPR10 -> "10" | GPR11 -> "11" - | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15" - | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19" - | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23" - | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27" - | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31" - -let float_reg_name = function - | FPR0 -> "0" | FPR1 -> "1" | FPR2 -> "2" | FPR3 -> "3" - | FPR4 -> "4" | FPR5 -> "5" | FPR6 -> "6" | FPR7 -> "7" - | FPR8 -> "8" | FPR9 -> "9" | FPR10 -> "10" | FPR11 -> "11" - | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15" - | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19" - | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23" - | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" - | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" - -module Linux_System : SYSTEM = - struct - let comment = "#" - - let constant oc cst = - match cst with - | Cint n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Csymbol_low(s, n) -> - symbol_fragment oc s n "@l" - | Csymbol_high(s, n) -> - symbol_fragment oc s n "@ha" - | Csymbol_sda(s, n) -> - symbol_fragment oc s n "@sda21" - (* 32-bit relative addressing is supported by the Diab tools but not by - GNU binutils. In the latter case, for testing purposes, we treat - them as absolute addressings. The default base register being GPR0, - this produces correct code, albeit with absolute addresses. *) - | Csymbol_rel_low(s, n) -> - symbol_fragment oc s n "@l" - | Csymbol_rel_high(s, n) -> - symbol_fragment oc s n "@ha" - - let ireg oc r = - output_string oc (int_reg_name r) - - let freg oc r = - output_string oc (float_reg_name r) - - let creg oc r = - fprintf oc "%d" r - - let name_of_section = function - | Section_text -> ".text" - | Section_data i -> - if i then ".data" else "COMM" - | Section_small_data i -> - if i then ".section .sdata,\"aw\",@progbits" else "COMM" - | Section_const i -> - if i then ".rodata" else "COMM" - | Section_small_const i -> - if i then ".section .sdata2,\"a\",@progbits" else "COMM" - | Section_string -> ".rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",\"a%s%s\",@progbits" - s (if wr then "w" else "") (if ex then "x" else "") - - let print_file_line oc file line = - PrintAnnot.print_file_line oc comment file line - - (* Emit .cfi directives *) - let cfi_startproc = - if Configuration.asm_supports_cfi then - (fun oc -> fprintf oc " .cfi_startproc\n") - else - (fun _ -> ()) - - let cfi_endproc = - if Configuration.asm_supports_cfi then - (fun oc -> fprintf oc " .cfi_endproc\n") - else - (fun _ -> ()) - - - let cfi_adjust = - if Configuration.asm_supports_cfi then - (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta) - else - (fun _ _ -> ()) - - let cfi_rel_offset = - if Configuration.asm_supports_cfi then - (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs) - else - (fun _ _ _ -> ()) - - - let print_prologue oc = () - - end - -module Diab_System : SYSTEM = - struct - let comment = ";" - - let constant oc cst = - match cst with - | Cint n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Csymbol_low(s, n) -> - symbol_fragment oc s n "@l" - | Csymbol_high(s, n) -> - symbol_fragment oc s n "@ha" - | Csymbol_sda(s, n) -> - symbol_fragment oc s n "@sdarx" - | Csymbol_rel_low(s, n) -> - symbol_fragment oc s n "@sdax@l" - | Csymbol_rel_high(s, n) -> - symbol_fragment oc s n "@sdarx@ha" - - let ireg oc r = - output_char oc 'r'; - output_string oc (int_reg_name r) - - let freg oc r = - output_char oc 'f'; - output_string oc (float_reg_name r) - - let creg oc r = - fprintf oc "cr%d" r - - let name_of_section = function - | Section_text -> ".text" - | Section_data i -> if i then ".data" else "COMM" - | Section_small_data i -> if i then ".sdata" else ".sbss" - | Section_const _ -> ".text" - | Section_small_const _ -> ".sdata2" - | Section_string -> ".text" - | Section_literal -> ".text" - | Section_jumptable -> ".text" - | Section_user(s, wr, ex) -> - sprintf ".section \"%s\",,%c" - s - (match wr, ex with - | true, true -> 'm' (* text+data *) - | true, false -> 'd' (* data *) - | false, true -> 'c' (* text *) - | false, false -> 'r') (* const *) - - let print_file_line oc file line = - PrintAnnot.print_file_line_d1 oc comment file line - - (* Emit .cfi directives *) - let cfi_startproc oc = () - - let cfi_endproc oc = () - - let cfi_adjust oc delta = () - - let cfi_rel_offset oc reg ofs = () - - let print_prologue oc = - fprintf oc " .xopt align-fill-text=0x60000000\n"; - if !Clflags.option_g then - fprintf oc " .xopt asm-debug-on\n" - - end - -module AsmPrinter (Target : SYSTEM) = - struct - open Target - -(* 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 = - fprintf oc "%s" s - - -let label oc lbl = - fprintf oc ".L%d" lbl - -let label_low oc lbl = - fprintf oc ".L%d@l" lbl - -let label_high oc lbl = - fprintf oc ".L%d@ha" lbl - - -let num_crbit = function - | CRbit_0 -> 0 - | CRbit_1 -> 1 - | CRbit_2 -> 2 - | CRbit_3 -> 3 - | CRbit_6 -> 6 - -let crbit oc bit = - fprintf oc "%d" (num_crbit bit) - -let ireg_or_zero oc r = - if r = GPR0 then output_string oc "0" else ireg oc r - -let preg oc = function - | IR r -> ireg oc r - | FR r -> freg oc r - | _ -> assert false - -let section oc sec = - let name = name_of_section sec in - assert (name <> "COMM"); - fprintf oc " %s\n" name - -let print_location oc loc = - if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) - -(* Encoding masks for rlwinm instructions *) - -let rolm_mask n = - let mb = ref 0 (* location of last 0->1 transition *) - and me = ref 32 (* location of last 1->0 transition *) - and last = ref ((Int32.logand n 1l) <> 0l) (* last bit seen *) - and count = ref 0 (* number of transitions *) - and mask = ref 0x8000_0000l in - for mx = 0 to 31 do - if Int32.logand n !mask <> 0l then - if !last then () else (incr count; mb := mx; last := true) - else - if !last then (incr count; me := mx; last := false) else (); - mask := Int32.shift_right_logical !mask 1 - done; - if !me = 0 then me := 32; - assert (!count = 2 || (!count = 0 && !last)); - (!mb, !me-1) - -(* Handling of annotations *) - -let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" - -let print_annot_stmt oc txt targs args = - if Str.string_match re_file_line txt 0 then begin - print_file_line oc (Str.matched_group 1 txt) - (int_of_string (Str.matched_group 2 txt)) - end else begin - fprintf oc "%s annotation: " comment; - PrintAnnot.print_annot_stmt preg "R1" oc txt targs args - end - -(* Determine if the displacement of a conditional branch fits the short form *) - -let short_cond_branch tbl pc lbl_dest = - match PTree.get lbl_dest tbl with - | None -> assert false - | Some pc_dest -> - let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000 - -(* Printing of instructions *) - -let float_literals : (int * int64) list ref = ref [] -let float32_literals : (int * int32) list ref = ref [] -let jumptables : (int * label list) list ref = ref [] - -let print_instruction oc tbl pc fallthrough = function - | Padd(r1, r2, r3) -> - fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Paddc(r1, r2, r3) -> - fprintf oc " addc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Padde(r1, r2, r3) -> - fprintf oc " adde %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 constant c - | Paddic(r1, r2, c) -> - fprintf oc " addic %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c - | Paddis(r1, r2, c) -> - fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c - | Paddze(r1, r2) -> - fprintf oc " addze %a, %a\n" ireg r1 ireg r2 - | Pallocframe(sz, ofs) -> - assert false - | 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 constant c - | Pandis_(r1, r2, c) -> - fprintf oc " andis. %a, %a, %a\n" ireg r1 ireg r2 constant c - | Pb lbl -> - fprintf oc " b %a\n" label (transl_label lbl) - | Pbctr sg -> - fprintf oc " bctr\n" - | Pbctrl sg -> - fprintf oc " bctrl\n" - | Pbdnz lbl -> - fprintf oc " bdnz %a\n" label (transl_label lbl) - | Pbf(bit, lbl) -> - if !Clflags.option_faligncondbranchs > 0 then - fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; - if short_cond_branch tbl pc lbl then - fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl) - else begin - let next = new_label() in - fprintf oc " bt %a, %a\n" crbit bit label next; - fprintf oc " b %a\n" label (transl_label lbl); - fprintf oc "%a:\n" label next - end - | Pbl(s, sg) -> - fprintf oc " bl %a\n" symbol s - | Pbs(s, sg) -> - fprintf oc " b %a\n" symbol s - | Pblr -> - fprintf oc " blr\n" - | Pbt(bit, lbl) -> - if !Clflags.option_faligncondbranchs > 0 then - fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; - if short_cond_branch tbl pc lbl then - fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl) - else begin - let next = new_label() in - fprintf oc " bf %a, %a\n" crbit bit label next; - fprintf oc " b %a\n" label (transl_label lbl); - fprintf oc "%a:\n" label next - end - | Pbtbl(r, tbl) -> - let lbl = new_label() in - fprintf oc "%s begin pseudoinstr btbl(%a)\n" comment ireg r; - fprintf oc "%s jumptable [ " comment; - List.iter (fun l -> fprintf oc "%a " label (transl_label l)) tbl; - fprintf oc "]\n"; - fprintf oc " slwi %a, %a, 2\n" ireg GPR12 ireg r; - fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl; - fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; - fprintf oc " mtctr %a\n" ireg GPR12; - fprintf oc " bctr\n"; - jumptables := (lbl, tbl) :: !jumptables; - fprintf oc "%s end pseudoinstr btbl\n" comment - | Pcmplw(r1, r2) -> - fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 - | Pcmplwi(r1, c) -> - fprintf oc " cmplwi %a, %a, %a\n" creg 0 ireg r1 constant c - | Pcmpw(r1, r2) -> - fprintf oc " cmpw %a, %a, %a\n" creg 0 ireg r1 ireg r2 - | Pcmpwi(r1, c) -> - fprintf oc " cmpwi %a, %a, %a\n" creg 0 ireg r1 constant c - | Pcntlz(r1, r2) -> - fprintf oc " cntlz %a, %a\n" ireg r1 ireg r2 - | Pcreqv(c1, c2, c3) -> - fprintf oc " creqv %a, %a, %a\n" crbit c1 crbit c2 crbit c3 - | Pcror(c1, c2, c3) -> - fprintf oc " cror %a, %a, %a\n" crbit c1 crbit c2 crbit c3 - | Pcrxor(c1, c2, c3) -> - fprintf oc " crxor %a, %a, %a\n" crbit c1 crbit c2 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 - | Peieio -> - fprintf oc " eieio\n" - | 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(sz, ofs) -> - assert false - | Pfabs(r1, r2) | Pfabss(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 - | Pfadds(r1, r2, r3) -> - fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfcmpu(r1, r2) -> - fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 - | Pfcti(r1, r2) -> - assert false - | Pfctiw(r1, r2) -> - fprintf oc " fctiw %a, %a\n" freg r1 freg r2 - | Pfctiwz(r1, r2) -> - fprintf oc " fctiwz %a, %a\n" freg r1 freg r2 - | Pfdiv(r1, r2, r3) -> - fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfdivs(r1, r2, r3) -> - fprintf oc " fdivs %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfmake(rd, r1, r2) -> - assert false - | Pfmr(r1, r2) -> - fprintf oc " fmr %a, %a\n" freg r1 freg r2 - | Pfmul(r1, r2, r3) -> - fprintf oc " fmul %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfmuls(r1, r2, r3) -> - fprintf oc " fmuls %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfneg(r1, r2) | Pfnegs(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 - | Pfxdp(r1, r2) -> - assert false - | Pfsub(r1, r2, r3) -> - fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 - | Pfsubs(r1, r2, r3) -> - fprintf oc " fsubs %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 - | Pfmsub(r1, r2, r3, r4) -> - fprintf oc " fmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pfnmadd(r1, r2, r3, r4) -> - fprintf oc " fnmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pfnmsub(r1, r2, r3, r4) -> - fprintf oc " fnmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pfsqrt(r1, r2) -> - fprintf oc " fsqrt %a, %a\n" freg r1 freg r2 - | Pfrsqrte(r1, r2) -> - fprintf oc " frsqrte %a, %a\n" freg r1 freg r2 - | Pfres(r1, r2) -> - fprintf oc " fres %a, %a\n" freg r1 freg r2 - | Pfsel(r1, r2, r3, r4) -> - fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 - | Pisync -> - fprintf oc " isync\n" - | Plbz(r1, c, r2) -> - fprintf oc " lbz %a, %a(%a)\n" ireg r1 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) | Plfd_a(r1, c, r2) -> - fprintf oc " lfd %a, %a(%a)\n" freg r1 constant c ireg r2 - | Plfdx(r1, r2, r3) | Plfdx_a(r1, r2, r3) -> - fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 - | Plfs(r1, c, r2) -> - fprintf oc " lfs %a, %a(%a)\n" freg r1 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 constant c ireg r2 - | Plhax(r1, r2, r3) -> - fprintf oc " lhax %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plhbrx(r1, r2, r3) -> - fprintf oc " lhbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plhz(r1, c, r2) -> - fprintf oc " lhz %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plhzx(r1, r2, r3) -> - fprintf oc " lhzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plfi(r1, c) -> - let lbl = new_label() in - fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); - float_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float_literals; - | Plfis(r1, c) -> - let lbl = new_label() in - fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c); - float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals; - | Plwarx(r1, r2, r3) -> - fprintf oc " lwarx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plwbrx(r1, r2, r3) -> - fprintf oc " lwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) -> - fprintf oc " lwz %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plwzu(r1, c, r2) -> - fprintf oc " lwzu %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> - fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pmfcr(r1) -> - fprintf oc " mfcr %a\n" ireg r1 - | Pmfcrbit(r1, bit) -> - assert false - | 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 constant c - | Pmullw(r1, r2, r3) -> - fprintf oc " mullw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pmulhw(r1, r2, r3) -> - fprintf oc " mulhw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pmulhwu(r1, r2, r3) -> - fprintf oc " mulhwu %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 constant c - | Poris(r1, r2, c) -> - fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c - | Prlwinm(r1, r2, c1, c2) -> - let (mb, me) = rolm_mask (camlint_of_coqint c2) in - fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" - ireg r1 ireg r2 (camlint_of_coqint c1) mb me - comment (camlint_of_coqint c2) - | Prlwimi(r1, r2, c1, c2) -> - let (mb, me) = rolm_mask (camlint_of_coqint c2) in - fprintf oc " rlwimi %a, %a, %ld, %d, %d %s 0x%lx\n" - ireg r1 ireg r2 (camlint_of_coqint c1) mb me - comment (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 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) | Pstfd_a(r1, c, r2) -> - fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2 - | Pstfdu(r1, c, r2) -> - fprintf oc " stfdu %a, %a(%a)\n" freg r1 constant c ireg r2 - | Pstfdx(r1, r2, r3) | Pstfdx_a(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 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 constant c ireg r2 - | Psthx(r1, r2, r3) -> - fprintf oc " sthx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psthbrx(r1, r2, r3) -> - fprintf oc " sthbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) -> - fprintf oc " stw %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Pstwu(r1, c, r2) -> - fprintf oc " stwu %a, %a(%a)\n" ireg r1 constant c ireg r2 - | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) -> - fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstwxu(r1, r2, r3) -> - fprintf oc " stwxu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstwbrx(r1, r2, r3) -> - fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Pstwcx_(r1, r2, r3) -> - fprintf oc " stwcx. %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 - | Psubfe(r1, r2, r3) -> - fprintf oc " subfe %a, %a, %a\n" ireg r1 ireg r2 ireg r3 - | Psubfze(r1, r2) -> - fprintf oc " subfze %a, %a\n" ireg r1 ireg r2 - | Psubfic(r1, r2, c) -> - fprintf oc " subfic %a, %a, %a\n" ireg r1 ireg r2 constant c - | Psync -> - fprintf oc " sync\n" - | Ptrap -> - fprintf oc " trap\n" - | 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 constant c - | Pxoris(r1, r2, c) -> - fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c - | Plabel lbl -> - if (not fallthrough) && !Clflags.option_falignbranchtargets > 0 then - fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets; - fprintf oc "%a:\n" label (transl_label lbl) - | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_inline_asm txt -> - fprintf oc "%s begin inline assembly\n" comment; - fprintf oc " %s\n" (extern_atom txt); - fprintf oc "%s end inline assembly\n" comment - | _ -> - assert false - end - | Pannot(ef, args) -> - begin match ef with - | EF_annot(txt, targs) -> - print_annot_stmt oc (extern_atom txt) targs args - | _ -> - assert false - end - | Pcfi_adjust n -> - cfi_adjust oc (camlint_of_coqint n) - | Pcfi_rel_offset n -> - cfi_rel_offset oc "lr" (camlint_of_coqint n) - -(* Determine if an instruction falls through *) - -let instr_fall_through = function - | Pb _ -> false - | Pbctr _ -> false - | Pbs _ -> false - | Pblr -> false - | _ -> true - -(* Estimate the size of an Asm instruction encoding, in number of actual - PowerPC instructions. We can over-approximate. *) - -let instr_size = function - | Pbf(bit, lbl) -> 2 - | Pbt(bit, lbl) -> 2 - | Pbtbl(r, tbl) -> 5 - | Plfi(r1, c) -> 2 - | Plfis(r1, c) -> 2 - | Plabel lbl -> 0 - | Pbuiltin(ef, args, res) -> 0 - | Pannot(ef, args) -> 0 - | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0 - | _ -> 1 - -(* Build a table label -> estimated position in generated code. - Used to predict if relative conditional branches can use the short form. *) - -let rec label_positions tbl pc = function - | [] -> tbl - | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c - | i :: c -> label_positions tbl (pc + instr_size i) c - -(* Emit a sequence of instructions *) - -let rec print_instructions oc tbl pc fallthrough = function - | [] -> () - | i :: c -> - print_instruction oc tbl pc fallthrough i; - print_instructions oc tbl (pc + instr_size i) (instr_fall_through i) c - -(* Print the code for a function *) - -let print_literal64 oc (lbl, n) = - let nlo = Int64.to_int32 n - and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in - fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo - -let print_literal32 oc (lbl, n) = - fprintf oc "%a: .long 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 print_function oc name fn = - Hashtbl.clear current_function_labels; - float_literals := []; - float32_literals := []; - jumptables := []; - let (text, lit, jmptbl) = - match C2C.atom_sections name with - | [t;l;j] -> (t, l, j) - | _ -> (Section_text, Section_literal, Section_jumptable) in - section oc text; - let alignment = - match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in - fprintf oc " .balign %d\n" alignment; - if not (C2C.atom_is_static name) then - fprintf oc " .globl %a\n" symbol name; - fprintf oc "%a:\n" symbol name; - print_location oc (C2C.atom_location name); - cfi_startproc oc; - print_instructions oc (label_positions PTree.empty 0 fn.fn_code) - 0 true fn.fn_code; - cfi_endproc oc; - fprintf oc " .type %a, @function\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name; - if !float_literals <> [] || !float32_literals <> [] then begin - section oc lit; - fprintf oc " .balign 8\n"; - List.iter (print_literal64 oc) !float_literals; - List.iter (print_literal32 oc) !float32_literals; - float_literals := []; float32_literals := [] - end; - if !jumptables <> [] then begin - section oc jmptbl; - fprintf oc " .balign 4\n"; - List.iter (print_jumptable oc) !jumptables; - jumptables := [] - end - -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_int64 n -> - let b = camlint64_of_coqint n in - fprintf oc " .long 0x%Lx, 0x%Lx\n" - (Int64.shift_right_logical b 32) - (Int64.logand b 0xFFFFFFFFL) - | Init_float32 n -> - fprintf oc " .long 0x%lx %s %.18g\n" - (camlint_of_coqint (Floats.Float32.to_bits n)) - comment (camlfloat_of_coqfloat n) - | Init_float64 n -> - let b = camlint64_of_coqint (Floats.Float.to_bits n) in - fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" - (Int64.shift_right_logical b 32) - (Int64.logand b 0xFFFFFFFFL) - comment (camlfloat_of_coqfloat n) - | Init_space n -> - if Z.gt n Z.zero then - fprintf oc " .space %s\n" (Z.to_string 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 name v = - match v.gvar_init with - | [] -> () - | _ -> - let sec = - match C2C.atom_sections name with - | [s] -> s - | _ -> Section_data true - and align = - match C2C.atom_alignof name with - | Some a -> a - | None -> 8 in (* 8-alignment is a safe default *) - let name_sec = - name_of_section sec in - if name_sec <> "COMM" then begin - fprintf oc " %s\n" name_sec; - fprintf oc " .balign %d\n" 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; - fprintf oc " .type %a, @object\n" symbol name; - fprintf oc " .size %a, . - %a\n" symbol name symbol name - end else begin - let sz = - match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in - fprintf oc " %s %a, %s, %d\n" - (if C2C.atom_is_static name then ".lcomm" else ".comm") - symbol name - (Z.to_string sz) - align - end - -let print_globdef oc (name, gdef) = - match gdef with - | Gfun (Internal code) -> print_function oc name code - | Gfun (External ef) -> () - | Gvar v -> print_var oc name v - - end - -type target = Linux | Diab - -let print_program oc p = - let target = - (match Configuration.system with - | "linux" -> Linux - | "diab" -> Diab - | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")) in - let module Target = (val (match target with - | Linux -> (module Linux_System:SYSTEM) - | Diab -> (module Diab_System:SYSTEM)):SYSTEM) in - PrintAnnot.reset_filenames(); - PrintAnnot.print_version_and_options oc Target.comment; - let module Printer = AsmPrinter(Target) in - Target.print_prologue oc; - List.iter (Printer.print_globdef oc) p.prog_defs; - PrintAnnot.close_filenames() - - diff --git a/powerpc/PrintAsm.mli b/powerpc/PrintAsm.mli deleted file mode 100644 index aefe3a0a..00000000 --- a/powerpc/PrintAsm.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -val print_program: out_channel -> Asm.program -> unit diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml new file mode 100644 index 00000000..d7249d17 --- /dev/null +++ b/powerpc/TargetPrinter.ml @@ -0,0 +1,741 @@ +(* *********************************************************************) +(* *) +(* 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 Maps +open Camlcoq +open Sections +open AST +open Memdata +open Asm +open PrintAsmaux + +(* Recognition of target ABI and asm syntax *) + +module type SYSTEM = + sig + val constant: out_channel -> constant -> unit + val ireg: out_channel -> ireg -> unit + val freg: out_channel -> freg -> unit + val creg: out_channel -> int -> unit + val name_of_section: section_name -> string + val print_file_line: out_channel -> string -> int -> unit + val cfi_startproc: out_channel -> unit + val cfi_endproc: out_channel -> unit + val cfi_adjust: out_channel -> int32 -> unit + val cfi_rel_offset: out_channel -> string -> int32 -> unit + val print_prologue: out_channel -> unit + end + +let symbol_fragment oc s n op = + fprintf oc "(%a)%s" symbol_offset (s, n) op + + +let int_reg_name = function + | GPR0 -> "0" | GPR1 -> "1" | GPR2 -> "2" | GPR3 -> "3" + | GPR4 -> "4" | GPR5 -> "5" | GPR6 -> "6" | GPR7 -> "7" + | GPR8 -> "8" | GPR9 -> "9" | GPR10 -> "10" | GPR11 -> "11" + | GPR12 -> "12" | GPR13 -> "13" | GPR14 -> "14" | GPR15 -> "15" + | GPR16 -> "16" | GPR17 -> "17" | GPR18 -> "18" | GPR19 -> "19" + | GPR20 -> "20" | GPR21 -> "21" | GPR22 -> "22" | GPR23 -> "23" + | GPR24 -> "24" | GPR25 -> "25" | GPR26 -> "26" | GPR27 -> "27" + | GPR28 -> "28" | GPR29 -> "29" | GPR30 -> "30" | GPR31 -> "31" + +let float_reg_name = function + | FPR0 -> "0" | FPR1 -> "1" | FPR2 -> "2" | FPR3 -> "3" + | FPR4 -> "4" | FPR5 -> "5" | FPR6 -> "6" | FPR7 -> "7" + | FPR8 -> "8" | FPR9 -> "9" | FPR10 -> "10" | FPR11 -> "11" + | FPR12 -> "12" | FPR13 -> "13" | FPR14 -> "14" | FPR15 -> "15" + | FPR16 -> "16" | FPR17 -> "17" | FPR18 -> "18" | FPR19 -> "19" + | FPR20 -> "20" | FPR21 -> "21" | FPR22 -> "22" | FPR23 -> "23" + | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27" + | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31" + +module Linux_System : SYSTEM = + struct + + let constant oc cst = + match cst with + | Cint n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Csymbol_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_high(s, n) -> + symbol_fragment oc s n "@ha" + | Csymbol_sda(s, n) -> + symbol_fragment oc s n "@sda21" + (* 32-bit relative addressing is supported by the Diab tools but not by + GNU binutils. In the latter case, for testing purposes, we treat + them as absolute addressings. The default base register being GPR0, + this produces correct code, albeit with absolute addresses. *) + | Csymbol_rel_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_rel_high(s, n) -> + symbol_fragment oc s n "@ha" + + let ireg oc r = + output_string oc (int_reg_name r) + + let freg oc r = + output_string oc (float_reg_name r) + + let creg oc r = + fprintf oc "%d" r + + let name_of_section = function + | Section_text -> ".text" + | Section_data i -> + if i then ".data" else "COMM" + | Section_small_data i -> + if i then ".section .sdata,\"aw\",@progbits" else "COMM" + | Section_const i -> + if i then ".rodata" else "COMM" + | Section_small_const i -> + if i then ".section .sdata2,\"a\",@progbits" else "COMM" + | Section_string -> ".rodata" + | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + + let print_file_line oc file line = + PrintAnnot.print_file_line oc comment file line + + (* Emit .cfi directives *) + let cfi_startproc = cfi_startproc + + let cfi_endproc = cfi_endproc + + let cfi_adjust = cfi_adjust + + let cfi_rel_offset = cfi_rel_offset + + let print_prologue oc = () + + end + +module Diab_System : SYSTEM = + struct + + let constant oc cst = + match cst with + | Cint n -> + fprintf oc "%ld" (camlint_of_coqint n) + | Csymbol_low(s, n) -> + symbol_fragment oc s n "@l" + | Csymbol_high(s, n) -> + symbol_fragment oc s n "@ha" + | Csymbol_sda(s, n) -> + symbol_fragment oc s n "@sdarx" + | Csymbol_rel_low(s, n) -> + symbol_fragment oc s n "@sdax@l" + | Csymbol_rel_high(s, n) -> + symbol_fragment oc s n "@sdarx@ha" + + let ireg oc r = + output_char oc 'r'; + output_string oc (int_reg_name r) + + let freg oc r = + output_char oc 'f'; + output_string oc (float_reg_name r) + + let creg oc r = + fprintf oc "cr%d" r + + let name_of_section = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else "COMM" + | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_const _ -> ".text" + | Section_small_const _ -> ".sdata2" + | Section_string -> ".text" + | Section_literal -> ".text" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\",,%c" + s + (match wr, ex with + | true, true -> 'm' (* text+data *) + | true, false -> 'd' (* data *) + | false, true -> 'c' (* text *) + | false, false -> 'r') (* const *) + + let print_file_line oc file line = + PrintAnnot.print_file_line_d1 oc comment file line + + (* Emit .cfi directives *) + let cfi_startproc oc = () + + let cfi_endproc oc = () + + let cfi_adjust oc delta = () + + let cfi_rel_offset oc reg ofs = () + + let print_prologue oc = + fprintf oc " .xopt align-fill-text=0x60000000\n"; + if !Clflags.option_g then + fprintf oc " .xopt asm-debug-on\n" + + end + +module Target (System : SYSTEM):TARGET = + struct + include System + + (* Basic printing functions *) + + let raw_symbol oc s = + fprintf oc "%s" s + + let label_low oc lbl = + fprintf oc ".L%d@l" lbl + + let label_high oc lbl = + fprintf oc ".L%d@ha" lbl + + + let num_crbit = function + | CRbit_0 -> 0 + | CRbit_1 -> 1 + | CRbit_2 -> 2 + | CRbit_3 -> 3 + | CRbit_6 -> 6 + + let crbit oc bit = + fprintf oc "%d" (num_crbit bit) + + let ireg_or_zero oc r = + if r = GPR0 then output_string oc "0" else ireg oc r + + let preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + + let section oc sec = + let name = name_of_section sec in + assert (name <> "COMM"); + fprintf oc " %s\n" name + + let print_location oc loc = + if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc) + + (* Encoding masks for rlwinm instructions *) + + let rolm_mask n = + let mb = ref 0 (* location of last 0->1 transition *) + and me = ref 32 (* location of last 1->0 transition *) + and last = ref ((Int32.logand n 1l) <> 0l) (* last bit seen *) + and count = ref 0 (* number of transitions *) + and mask = ref 0x8000_0000l in + for mx = 0 to 31 do + if Int32.logand n !mask <> 0l then + if !last then () else (incr count; mb := mx; last := true) + else + if !last then (incr count; me := mx; last := false) else (); + mask := Int32.shift_right_logical !mask 1 + done; + if !me = 0 then me := 32; + assert (!count = 2 || (!count = 0 && !last)); + (!mb, !me-1) + + (* Handling of annotations *) + + let print_annot_stmt oc txt targs args = + if Str.string_match re_file_line txt 0 then begin + print_file_line oc (Str.matched_group 1 txt) + (int_of_string (Str.matched_group 2 txt)) + end else begin + fprintf oc "%s annotation: " comment; + PrintAnnot.print_annot_stmt preg "R1" oc txt targs args + end + + (* Determine if the displacement of a conditional branch fits the short form *) + + let short_cond_branch tbl pc lbl_dest = + match PTree.get lbl_dest tbl with + | None -> assert false + | Some pc_dest -> + let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000 + + (* Printing of instructions *) + + let print_instruction oc tbl pc fallthrough = function + | Padd(r1, r2, r3) -> + fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Paddc(r1, r2, r3) -> + fprintf oc " addc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Padde(r1, r2, r3) -> + fprintf oc " adde %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 constant c + | Paddic(r1, r2, c) -> + fprintf oc " addic %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c + | Paddis(r1, r2, c) -> + fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c + | Paddze(r1, r2) -> + fprintf oc " addze %a, %a\n" ireg r1 ireg r2 + | Pallocframe(sz, ofs) -> + assert false + | 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 constant c + | Pandis_(r1, r2, c) -> + fprintf oc " andis. %a, %a, %a\n" ireg r1 ireg r2 constant c + | Pb lbl -> + fprintf oc " b %a\n" label (transl_label lbl) + | Pbctr sg -> + fprintf oc " bctr\n" + | Pbctrl sg -> + fprintf oc " bctrl\n" + | Pbdnz lbl -> + fprintf oc " bdnz %a\n" label (transl_label lbl) + | Pbf(bit, lbl) -> + if !Clflags.option_faligncondbranchs > 0 then + fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; + if short_cond_branch tbl pc lbl then + fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl) + else begin + let next = new_label() in + fprintf oc " bt %a, %a\n" crbit bit label next; + fprintf oc " b %a\n" label (transl_label lbl); + fprintf oc "%a:\n" label next + end + | Pbl(s, sg) -> + fprintf oc " bl %a\n" symbol s + | Pbs(s, sg) -> + fprintf oc " b %a\n" symbol s + | Pblr -> + fprintf oc " blr\n" + | Pbt(bit, lbl) -> + if !Clflags.option_faligncondbranchs > 0 then + fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs; + if short_cond_branch tbl pc lbl then + fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl) + else begin + let next = new_label() in + fprintf oc " bf %a, %a\n" crbit bit label next; + fprintf oc " b %a\n" label (transl_label lbl); + fprintf oc "%a:\n" label next + end + | Pbtbl(r, tbl) -> + let lbl = new_label() in + fprintf oc "%s begin pseudoinstr btbl(%a)\n" comment ireg r; + fprintf oc "%s jumptable [ " comment; + List.iter (fun l -> fprintf oc "%a " label (transl_label l)) tbl; + fprintf oc "]\n"; + fprintf oc " slwi %a, %a, 2\n" ireg GPR12 ireg r; + fprintf oc " addis %a, %a, %a\n" ireg GPR12 ireg GPR12 label_high lbl; + fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; + fprintf oc " mtctr %a\n" ireg GPR12; + fprintf oc " bctr\n"; + jumptables := (lbl, tbl) :: !jumptables; + fprintf oc "%s end pseudoinstr btbl\n" comment + | Pcmplw(r1, r2) -> + fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 + | Pcmplwi(r1, c) -> + fprintf oc " cmplwi %a, %a, %a\n" creg 0 ireg r1 constant c + | Pcmpw(r1, r2) -> + fprintf oc " cmpw %a, %a, %a\n" creg 0 ireg r1 ireg r2 + | Pcmpwi(r1, c) -> + fprintf oc " cmpwi %a, %a, %a\n" creg 0 ireg r1 constant c + | Pcntlz(r1, r2) -> + fprintf oc " cntlz %a, %a\n" ireg r1 ireg r2 + | Pcreqv(c1, c2, c3) -> + fprintf oc " creqv %a, %a, %a\n" crbit c1 crbit c2 crbit c3 + | Pcror(c1, c2, c3) -> + fprintf oc " cror %a, %a, %a\n" crbit c1 crbit c2 crbit c3 + | Pcrxor(c1, c2, c3) -> + fprintf oc " crxor %a, %a, %a\n" crbit c1 crbit c2 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 + | Peieio -> + fprintf oc " eieio\n" + | 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(sz, ofs) -> + assert false + | Pfabs(r1, r2) | Pfabss(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 + | Pfadds(r1, r2, r3) -> + fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfcmpu(r1, r2) -> + fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 + | Pfcti(r1, r2) -> + assert false + | Pfctiw(r1, r2) -> + fprintf oc " fctiw %a, %a\n" freg r1 freg r2 + | Pfctiwz(r1, r2) -> + fprintf oc " fctiwz %a, %a\n" freg r1 freg r2 + | Pfdiv(r1, r2, r3) -> + fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfdivs(r1, r2, r3) -> + fprintf oc " fdivs %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfmake(rd, r1, r2) -> + assert false + | Pfmr(r1, r2) -> + fprintf oc " fmr %a, %a\n" freg r1 freg r2 + | Pfmul(r1, r2, r3) -> + fprintf oc " fmul %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfmuls(r1, r2, r3) -> + fprintf oc " fmuls %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfneg(r1, r2) | Pfnegs(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 + | Pfxdp(r1, r2) -> + assert false + | Pfsub(r1, r2, r3) -> + fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 + | Pfsubs(r1, r2, r3) -> + fprintf oc " fsubs %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 + | Pfmsub(r1, r2, r3, r4) -> + fprintf oc " fmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfnmadd(r1, r2, r3, r4) -> + fprintf oc " fnmadd %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfnmsub(r1, r2, r3, r4) -> + fprintf oc " fnmsub %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pfsqrt(r1, r2) -> + fprintf oc " fsqrt %a, %a\n" freg r1 freg r2 + | Pfrsqrte(r1, r2) -> + fprintf oc " frsqrte %a, %a\n" freg r1 freg r2 + | Pfres(r1, r2) -> + fprintf oc " fres %a, %a\n" freg r1 freg r2 + | Pfsel(r1, r2, r3, r4) -> + fprintf oc " fsel %a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4 + | Pisync -> + fprintf oc " isync\n" + | Plbz(r1, c, r2) -> + fprintf oc " lbz %a, %a(%a)\n" ireg r1 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) | Plfd_a(r1, c, r2) -> + fprintf oc " lfd %a, %a(%a)\n" freg r1 constant c ireg r2 + | Plfdx(r1, r2, r3) | Plfdx_a(r1, r2, r3) -> + fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 + | Plfs(r1, c, r2) -> + fprintf oc " lfs %a, %a(%a)\n" freg r1 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 constant c ireg r2 + | Plhax(r1, r2, r3) -> + fprintf oc " lhax %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plhbrx(r1, r2, r3) -> + fprintf oc " lhbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plhz(r1, c, r2) -> + fprintf oc " lhz %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plhzx(r1, r2, r3) -> + fprintf oc " lhzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plfi(r1, c) -> + let lbl = new_label() in + fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; + fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); + float64_literals := (lbl, camlint64_of_coqint (Floats.Float.to_bits c)) :: !float64_literals; + | Plfis(r1, c) -> + let lbl = new_label() in + fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; + fprintf oc " lfs %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat32 c); + float32_literals := (lbl, camlint_of_coqint (Floats.Float32.to_bits c)) :: !float32_literals; + | Plwarx(r1, r2, r3) -> + fprintf oc " lwarx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plwbrx(r1, r2, r3) -> + fprintf oc " lwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Plwz(r1, c, r2) | Plwz_a(r1, c, r2) -> + fprintf oc " lwz %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plwzu(r1, c, r2) -> + fprintf oc " lwzu %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) -> + fprintf oc " lwzx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmfcr(r1) -> + fprintf oc " mfcr %a\n" ireg r1 + | Pmfcrbit(r1, bit) -> + assert false + | 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 constant c + | Pmullw(r1, r2, r3) -> + fprintf oc " mullw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhw(r1, r2, r3) -> + fprintf oc " mulhw %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pmulhwu(r1, r2, r3) -> + fprintf oc " mulhwu %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 constant c + | Poris(r1, r2, c) -> + fprintf oc " oris %a, %a, %a\n" ireg r1 ireg r2 constant c + | Prlwinm(r1, r2, c1, c2) -> + let (mb, me) = rolm_mask (camlint_of_coqint c2) in + fprintf oc " rlwinm %a, %a, %ld, %d, %d %s 0x%lx\n" + ireg r1 ireg r2 (camlint_of_coqint c1) mb me + comment (camlint_of_coqint c2) + | Prlwimi(r1, r2, c1, c2) -> + let (mb, me) = rolm_mask (camlint_of_coqint c2) in + fprintf oc " rlwimi %a, %a, %ld, %d, %d %s 0x%lx\n" + ireg r1 ireg r2 (camlint_of_coqint c1) mb me + comment (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 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) | Pstfd_a(r1, c, r2) -> + fprintf oc " stfd %a, %a(%a)\n" freg r1 constant c ireg r2 + | Pstfdu(r1, c, r2) -> + fprintf oc " stfdu %a, %a(%a)\n" freg r1 constant c ireg r2 + | Pstfdx(r1, r2, r3) | Pstfdx_a(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 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 constant c ireg r2 + | Psthx(r1, r2, r3) -> + fprintf oc " sthx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psthbrx(r1, r2, r3) -> + fprintf oc " sthbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstw(r1, c, r2) | Pstw_a(r1, c, r2) -> + fprintf oc " stw %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Pstwu(r1, c, r2) -> + fprintf oc " stwu %a, %a(%a)\n" ireg r1 constant c ireg r2 + | Pstwx(r1, r2, r3) | Pstwx_a(r1, r2, r3) -> + fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstwxu(r1, r2, r3) -> + fprintf oc " stwxu %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstwbrx(r1, r2, r3) -> + fprintf oc " stwbrx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Pstwcx_(r1, r2, r3) -> + fprintf oc " stwcx. %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 + | Psubfe(r1, r2, r3) -> + fprintf oc " subfe %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psubfze(r1, r2) -> + fprintf oc " subfze %a, %a\n" ireg r1 ireg r2 + | Psubfic(r1, r2, c) -> + fprintf oc " subfic %a, %a, %a\n" ireg r1 ireg r2 constant c + | Psync -> + fprintf oc " sync\n" + | Ptrap -> + fprintf oc " trap\n" + | 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 constant c + | Pxoris(r1, r2, c) -> + fprintf oc " xoris %a, %a, %a\n" ireg r1 ireg r2 constant c + | Plabel lbl -> + if (not fallthrough) && !Clflags.option_falignbranchtargets > 0 then + fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets; + fprintf oc "%a:\n" label (transl_label lbl) + | Pbuiltin(ef, args, res) -> + begin match ef with + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment + | _ -> + assert false + end + | Pannot(ef, args) -> + begin match ef with + | EF_annot(txt, targs) -> + print_annot_stmt oc (extern_atom txt) targs args + | _ -> + assert false + end + | Pcfi_adjust n -> + cfi_adjust oc (camlint_of_coqint n) + | Pcfi_rel_offset n -> + cfi_rel_offset oc "lr" (camlint_of_coqint n) + + (* Determine if an instruction falls through *) + + let instr_fall_through = function + | Pb _ -> false + | Pbctr _ -> false + | Pbs _ -> false + | Pblr -> false + | _ -> true + + (* Estimate the size of an Asm instruction encoding, in number of actual + PowerPC instructions. We can over-approximate. *) + + let instr_size = function + | Pbf(bit, lbl) -> 2 + | Pbt(bit, lbl) -> 2 + | Pbtbl(r, tbl) -> 5 + | Plfi(r1, c) -> 2 + | Plfis(r1, c) -> 2 + | Plabel lbl -> 0 + | Pbuiltin(ef, args, res) -> 0 + | Pannot(ef, args) -> 0 + | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0 + | _ -> 1 + + (* Build a table label -> estimated position in generated code. + Used to predict if relative conditional branches can use the short form. *) + + let rec label_positions tbl pc = function + | [] -> tbl + | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c + | i :: c -> label_positions tbl (pc + instr_size i) c + + (* Emit a sequence of instructions *) + + let print_instructions oc code = + let rec aux oc tbl pc fallthrough = function + | [] -> () + | i :: c -> + print_instruction oc tbl pc fallthrough i; + aux oc tbl (pc + instr_size i) (instr_fall_through i) c in + aux oc (label_positions PTree.empty 0 code) 0 true code + + (* Print the code for a function *) + + let print_literal64 oc (lbl, n) = + let nlo = Int64.to_int32 n + and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in + fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo + + let print_literal32 oc (lbl, n) = + fprintf oc "%a: .long 0x%lx\n" label lbl n + + 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_int64 n -> + let b = camlint64_of_coqint n in + fprintf oc " .long 0x%Lx, 0x%Lx\n" + (Int64.shift_right_logical b 32) + (Int64.logand b 0xFFFFFFFFL) + | Init_float32 n -> + fprintf oc " .long 0x%lx %s %.18g\n" + (camlint_of_coqint (Floats.Float32.to_bits n)) + comment (camlfloat_of_coqfloat n) + | Init_float64 n -> + let b = camlint64_of_coqint (Floats.Float.to_bits n) in + fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" + (Int64.shift_right_logical b 32) + (Int64.logand b 0xFFFFFFFFL) + comment (camlfloat_of_coqfloat n) + | Init_space n -> + if Z.gt n Z.zero then + fprintf oc " .space %s\n" (Z.to_string n) + | Init_addrof(symb, ofs) -> + fprintf oc " .long %a\n" + symbol_offset (symb, ofs) + + let comment = comment + + let print_fun_info = true + + let emit_constants oc lit = + if !float64_literals <> [] || !float32_literals <> [] then begin + section oc lit; + fprintf oc " .balign 8\n"; + List.iter (print_literal64 oc) !float64_literals; + List.iter (print_literal32 oc) !float32_literals; + float64_literals := []; float32_literals := [] + end + + let print_optional_fun_info _ = () + + let get_section_names name = + match C2C.atom_sections name with + | [t;l;j] -> (t, l, j) + | _ -> (Section_text, Section_literal, Section_jumptable) + + let reset_constants = reset_constants + + let print_var_info = true + + let print_comm_symb oc sz name align = + fprintf oc " %s %a, %s, %d\n" + (if C2C.atom_is_static name then ".lcomm" else ".comm") + symbol name + (Z.to_string sz) + align + + let print_align oc align = + fprintf oc " .balign %d\n" align + + let print_epilogue _ = () + + let print_jumptable oc jmptbl = + 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 in + if !jumptables <> [] then begin + section oc jmptbl; + fprintf oc " .balign 4\n"; + List.iter (print_jumptable oc) !jumptables; + jumptables := [] + end + + end + +let sel_target () = + let module S = (val + (match Configuration.system with + | "linux" -> (module Linux_System:SYSTEM) + | "diab" -> (module Diab_System:SYSTEM) + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")):SYSTEM) in + (module Target(S):TARGET) |