diff options
Diffstat (limited to 'powerpc/PrintDiab.ml')
-rw-r--r-- | powerpc/PrintDiab.ml | 150 |
1 files changed, 150 insertions, 0 deletions
diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml new file mode 100644 index 00000000..61a4eff9 --- /dev/null +++ b/powerpc/PrintDiab.ml @@ -0,0 +1,150 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* The Diab specific printing functions *) + +open Printf +open Datatypes +open DwarfTypes +open DwarfUtil +open DwarfPrinter +open Camlcoq +open Sections +open Asm +open PrintUtil + +module Diab_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 filenum : (string, int) Hashtbl.t = Hashtbl.create 7 + + let print_file_line oc file line = + PrintAnnot.print_file_line_d2 oc comment file line; + if !Clflags.option_g && file <> "" && not (Hashtbl.mem filenum file) then + Hashtbl.add filenum file (new_label ()) + + (* Emit .cfi directives *) + let cfi_startproc oc = () + + let cfi_endproc oc = () + + let cfi_adjust oc delta = () + + let cfi_rel_offset oc reg ofs = () + + let debug_line_start = ref (-1) + + let compilation_unit_start_addr = ref (-1) + + let compilation_unit_end_addr = ref (-1) + + (* Mapping from debug addresses to labels *) + let addr_label_map: (int,int) Hashtbl.t = Hashtbl.create 7 + + let set_compilation_unit_addrs cu_start cu_end = + compilation_unit_start_addr := cu_start; + compilation_unit_end_addr := cu_end + + let debug_info_start = ref (-1) + + let print_addr_label oc addr = + let lbl = try + Hashtbl.find addr_label_map addr + with Not_found -> + let lbl = new_label () in + Hashtbl.add addr_label_map addr lbl; + lbl in + fprintf oc "%a:\n" label lbl + + let register_addr_label = Hashtbl.add addr_label_map + + let print_prologue oc = + fprintf oc " .xopt align-fill-text=0x60000000\n"; + if !Clflags.option_g then + begin + fprintf oc " .text\n"; + fprintf oc " .section .debug_line,,n\n"; + let label_debug_line = new_label () in + debug_line_start := label_debug_line; + fprintf oc "%a:\n" label label_debug_line; + fprintf oc " .text\n"; + print_addr_label oc !compilation_unit_start_addr; + let label_debug_info = new_label () in + debug_info_start := label_debug_info; + fprintf oc " .0byte %a\n" label label_debug_info; + fprintf oc " .d2_line_start .debug_line\n"; + fprintf oc " .text\n"; + fprintf oc " .align 2\n" + end + + let print_epilogue oc = + if !Clflags.option_g then + begin + (* Everthink available for printing of the compilation unit *) + fprintf oc " .text\n"; + (* End Address of the compilation unit *) + print_addr_label oc !compilation_unit_end_addr; + (* Print the filenum which is used for the location expressions *) + Hashtbl.iter (fun name lbl -> + fprintf oc "%a: .d2filenum \"%s\"\n" label lbl name) filenum; + (* The end of the debug line info *) + fprintf oc " .d2_line_end\n"; + end + + + + end:SYSTEM) |