diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | Makefile.extr | 2 | ||||
| -rw-r--r-- | backend/PrintAnnot.ml | 8 | ||||
| -rw-r--r-- | debug/DwarfAbbrvPrinter.ml | 314 | ||||
| -rw-r--r-- | debug/DwarfTypes.ml | 248 | ||||
| -rw-r--r-- | debug/DwarfUtil.ml | 88 | ||||
| -rw-r--r-- | driver/Driver.ml | 2 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 319 | ||||
| -rw-r--r-- | powerpc/PrintDiab.ml | 231 | ||||
| -rw-r--r-- | powerpc/PrintLinux.ml | 109 | ||||
| -rw-r--r-- | powerpc/PrintUtil.ml | 180 |
11 files changed, 1186 insertions, 317 deletions
@@ -15,7 +15,7 @@ include Makefile.config -DIRS=lib common $(ARCH) backend cfrontend driver \ +DIRS=lib common $(ARCH) backend cfrontend driver debug\ flocq/Core flocq/Prop flocq/Calc flocq/Appli exportclight \ cparser cparser/validator diff --git a/Makefile.extr b/Makefile.extr index 2afd6e31..f5f7e7b4 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -21,7 +21,7 @@ include Makefile.config DIRS=extraction \ lib common $(ARCH) backend cfrontend cparser driver \ - exportclight + exportclight debug # Directories containing Caml code that must be preprocessed by Camlp4 diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 54174b9f..26f96370 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -66,10 +66,10 @@ let print_file_line oc pref file line = | Some fb -> Printlines.copy oc pref fb line line end -(* Add file and line debug location, using DWARF1 directives in the style +(* Add file and line debug location, using DWARF2 directives in the style of Diab C 5 *) -let print_file_line_d1 oc pref file line = +let print_file_line_d2 oc pref file line = if !Clflags.option_g && file <> "" then begin let (_, filebuf) = try @@ -77,10 +77,10 @@ let print_file_line_d1 oc pref file line = with Not_found -> enter_filename file in if file <> !last_file then begin - fprintf oc " .d1file %S\n" file; + fprintf oc " .d2file %S\n" file; last_file := file end; - fprintf oc " .d1line %d\n" line; + fprintf oc " .d2line %d\n" line; match filebuf with | None -> () | Some fb -> Printlines.copy oc pref fb line line diff --git a/debug/DwarfAbbrvPrinter.ml b/debug/DwarfAbbrvPrinter.ml new file mode 100644 index 00000000..214484b6 --- /dev/null +++ b/debug/DwarfAbbrvPrinter.ml @@ -0,0 +1,314 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + + +open DwarfTypes +open DwarfUtil + +module type DWARF_ABBRV_DEFS = + sig + (* Functions used for the printing of the dwarf abbreviations *) + val string_of_byte: bool -> string + val string_of_abbrv_entry: int -> string + val abbrv_section_start: out_channel -> unit + val abbrv_section_end: out_channel -> unit + val abbrv_prologue: out_channel -> int -> unit + val abbrv_epilogue: out_channel -> unit + val get_abbrv_start_addr: unit -> int + (* The form constants of the types *) + val sibling_type_abbr: int + val decl_file_type_abbr: int + val decl_line_type_abbr: int + val type_abbr: int + val name_type_abbr: int + val encoding_type_abbr: int + val byte_size_type_abbr: int + val high_pc_type_abbr: int + val low_pc_type_abbr: int + val stmt_list_type_abbr: int + val declaration_type_abbr: int + val external_type_abbr: int + val prototyped_type_abbr: int + val bit_offset_type_abbr: int + val comp_dir_type_abbr: int + val language_type_abbr: int + val producer_type_abbr: int + val value_type_abbr: int + val artificial_type_abbr: int + val variable_parameter_type_abbr: int + val bit_size_type_abbr: int + val location_const_type_abbr: int + val location_block_type_abbr: int + val data_location_block_type_abbr: int + val data_location_ref_type_abbr: int + val bound_const_type_abbr: int + val bound_ref_type_abbr: int + end + +module DwarfAbbrvPrinter(Defs:DWARF_ABBRV_DEFS) : + sig + val print_debug_abbrv: out_channel -> dw_entry -> unit + val get_abbrv: dw_entry -> bool -> int + val get_abbrv_start_addr: unit -> int + end = + (struct + + let curr_abbrv = ref 0 + + let next_abbrv = + let abbrv = !curr_abbrv in + incr curr_abbrv;abbrv + + let abbrvs: (string * int) list ref = ref [] + + let abbrv_mapping: (string,int) Hashtbl.t = Hashtbl.create 7 + + let add_byte buf value = + Buffer.add_string buf (Defs.string_of_byte value) + + let add_abbr_uleb v buf = + Buffer.add_string buf (Defs.string_of_abbrv_entry v) + + let add_abbr_entry (v1,v2) buf = + add_abbr_uleb v1 buf; + add_abbr_uleb v2 buf + + let add_sibling = add_abbr_entry (0x1,Defs.sibling_type_abbr) + + let add_decl_file = add_abbr_entry (0x3a,Defs.decl_file_type_abbr) + + let add_decl_line = add_abbr_entry (0x3b,Defs.decl_line_type_abbr) + + let add_type = add_abbr_entry (0x49,Defs.type_abbr) + + let add_name = add_abbr_entry (0x3,Defs.name_type_abbr) + + let add_encoding = add_abbr_entry (0x3e,Defs.encoding_type_abbr) + + let add_byte_size = add_abbr_entry (0xb,Defs.byte_size_type_abbr) + + let add_high_pc = add_abbr_entry (0x12,Defs.high_pc_type_abbr) + + let add_low_pc = add_abbr_entry (0x11,Defs.low_pc_type_abbr) + + let add_stmt_list = add_abbr_entry (0x10,Defs.stmt_list_type_abbr) + + let add_declaration = add_abbr_entry (0x3c,Defs.declaration_type_abbr) + + let add_external = add_abbr_entry (0x3f,Defs.external_type_abbr) + + let add_prototyped = add_abbr_entry (0x27,Defs.prototyped_type_abbr) + + let add_bit_offset = add_abbr_entry (0xd,Defs.bit_offset_type_abbr) + + let add_comp_dir = add_abbr_entry (0x1b,Defs.comp_dir_type_abbr) + + let add_language = add_abbr_entry (0x13,Defs.language_type_abbr) + + let add_producer = add_abbr_entry (0x25,Defs.producer_type_abbr) + + let add_value = add_abbr_entry (0x1c,Defs.value_type_abbr) + + let add_artificial = add_abbr_entry (0x34,Defs.artificial_type_abbr) + + let add_variable_parameter = add_abbr_entry (0x4b,Defs.variable_parameter_type_abbr) + + let add_bit_size = add_abbr_entry (0xc,Defs.bit_size_type_abbr) + + let add_location loc buf = + match loc with + | None -> () + | Some (LocConst _) -> add_abbr_entry (0x2,Defs.location_const_type_abbr) buf + | Some (LocBlock _) -> add_abbr_entry (0x2,Defs.location_block_type_abbr) buf + + let add_data_location loc buf = + match loc with + | None -> () + | Some (DataLocBlock __) -> add_abbr_entry (0x38,Defs.data_location_block_type_abbr) buf + | Some (DataLocRef _) -> add_abbr_entry (0x38,Defs.data_location_ref_type_abbr) buf + + let add_bound_value bound = + match bound with + | BoundConst _ -> add_abbr_entry (0x2f,Defs.bound_const_type_abbr) + | BoundRef _ -> add_abbr_entry (0x2f,Defs.bound_ref_type_abbr) + + let abbrv_string_of_entity entity has_sibling = + let buf = Buffer.create 12 in + let add_attr_some v f = + match v with + | None -> () + | Some _ -> f buf in + let prologue id = + let has_child = match entity.children with + | [] -> false + | _ -> true in + add_abbr_uleb id buf; + add_byte buf has_child; + if has_sibling then add_sibling buf; + in + (match entity.tag with + | DW_TAG_array_type e -> + prologue 0x1; + add_attr_some e.array_type_decl_file add_decl_file; + add_attr_some e.array_type_decl_line add_decl_line; + add_type buf + | DW_TAG_base_type _ -> + prologue 0x24; + add_encoding buf; + add_byte_size buf; + add_name buf + | DW_TAG_compile_unit e -> + prologue 0x11; + add_comp_dir buf; + add_high_pc buf; + add_low_pc buf; + add_language buf; + add_name buf; + add_producer buf; + add_attr_some e.compile_unit_stmt_list add_stmt_list + | DW_TAG_const_type _ -> + prologue 0x26; + add_type buf + | DW_TAG_enumeration_type e -> + prologue 0x4; + add_attr_some e.enumeration_decl_file add_decl_file; + add_attr_some e.enumeration_decl_line add_decl_line; + add_byte_size buf; + add_name buf; + add_attr_some e.enumeration_declaration add_declaration + | DW_TAG_enumerator e -> + prologue 0x28; + add_attr_some e.enumerator_decl_file add_decl_file; + add_attr_some e.enumerator_decl_line add_decl_line; + add_value buf; + add_name buf + | DW_TAG_formal_parameter e -> + prologue 0x34; + add_attr_some e.formal_parameter_decl_file add_decl_file; + add_attr_some e.formal_parameter_decl_line add_decl_line; + add_attr_some e.formal_parameter_artificial add_artificial; + add_location e.formal_parameter_location buf; + add_name buf; + add_location e.formal_parameter_segment buf; + add_type buf; + add_attr_some e.formal_parameter_variable_parameter add_variable_parameter + | DW_TAG_label _ -> + prologue 0xa; + add_low_pc buf; + add_name buf; + | DW_TAG_lexical_block _ -> + prologue 0xb; + add_high_pc buf; + add_low_pc buf + | DW_TAG_member e -> + prologue 0xd; + add_attr_some e.member_decl_file add_decl_file; + add_attr_some e.member_decl_line add_decl_line; + add_attr_some e.member_byte_size add_byte_size; + add_attr_some e.member_bit_offset add_bit_offset; + add_attr_some e.member_bit_size add_bit_size; + add_data_location e.member_data_member_location buf; + add_attr_some e.member_declaration add_declaration; + add_name buf; + add_type buf + | DW_TAG_pointer_type _ -> + prologue 0xf; + add_type buf + | DW_TAG_structure_type e -> + prologue 0x13; + add_attr_some e.structure_decl_file add_decl_file; + add_attr_some e.structure_decl_line add_decl_line; + add_byte_size buf; + add_attr_some e.structure_declaration add_declaration; + add_name buf + | DW_TAG_subprogram e -> + prologue 0x2e; + add_attr_some e.subprogram_decl_file add_decl_file; + add_attr_some e.subprogram_decl_line add_decl_line; + add_attr_some e.subprogram_external add_external; + add_high_pc buf; + add_low_pc buf; + add_name buf; + add_prototyped buf; + add_type buf + | DW_TAG_subrange_type e -> + prologue 0x21; + add_attr_some e.subrange_type add_type; + add_bound_value e.subrange_upper_bound buf + | DW_TAG_subroutine_type _ -> + prologue 0x15; + add_prototyped buf + | DW_TAG_typedef e -> + prologue 0x16; + add_attr_some e.typedef_decl_file add_decl_file; + add_attr_some e.typedef_decl_line add_decl_line; + add_name buf; + add_type buf + | DW_TAG_union_type e -> + prologue 0x17; + add_attr_some e.union_decl_file add_decl_file; + add_attr_some e.union_decl_line add_decl_line; + add_byte_size buf; + add_name buf + | DW_TAG_unspecified_parameter e -> + prologue 0x18; + add_attr_some e.unspecified_parameter_decl_file add_decl_file; + add_attr_some e.unspecified_parameter_decl_line add_decl_line; + add_attr_some e.unspecified_parameter_artificial add_artificial + | DW_TAG_variable e -> + prologue 0x34; + add_attr_some e.variable_decl_file add_decl_file; + add_attr_some e.variable_decl_line add_decl_line; + add_attr_some e.variable_declaration add_declaration; + add_attr_some e.variable_external add_external; + add_location e.variable_location buf; + add_name buf; + add_location e.variable_segment buf; + add_type buf + | DW_TAG_volatile_type _ -> + prologue 0x35; + add_type buf); + Buffer.contents buf + + let get_abbrv entity has_sibling = + let abbrv_string = abbrv_string_of_entity entity has_sibling in + (try + Hashtbl.find abbrv_mapping abbrv_string + with Not_found -> + let id = next_abbrv in + abbrvs:=(abbrv_string,id)::!abbrvs; + Hashtbl.add abbrv_mapping abbrv_string id; + id) + + let compute_abbrv entry = + entry_iter_sib (fun sib entry -> + let has_sib = match sib with + | None -> false + | Some _ -> true in + ignore (get_abbrv entry has_sib)) entry + + let print_abbrv oc = + let abbrvs = List.sort (fun (_,a) (_,b) -> Pervasives.compare a b) !abbrvs in + Defs.abbrv_section_start oc; + List.iter (fun (s,id) -> + Defs.abbrv_prologue oc id; + output_string oc s; + Defs.abbrv_epilogue oc) abbrvs; + Defs.abbrv_section_end oc + + let print_debug_abbrv oc entry = + compute_abbrv entry; + print_abbrv oc + + let get_abbrv_start_addr = Defs.get_abbrv_start_addr + + end) diff --git a/debug/DwarfTypes.ml b/debug/DwarfTypes.ml new file mode 100644 index 00000000..5a832bdf --- /dev/null +++ b/debug/DwarfTypes.ml @@ -0,0 +1,248 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Types used for writing dwarf debug information *) + +(* Basic types for the value of attributes *) + +type constant = int + +type flag = bool + +type reference = int + +type encoding = + | DW_ATE_address + | DW_ATE_boolean + | DW_ATE_complex_float + | DW_ATE_float + | DW_ATE_signed + | DW_ATE_signed_char + | DW_ATE_unsigned + | DW_ATE_unsigned_char + +type address = int + +type language = + | DW_LANG_C + | DW_LANG_C89 + +type block = string + +type location_value = + | LocConst of constant + | LocBlock of block + +type data_location_value = + | DataLocBlock of block + | DataLocRef of reference + +type bound_value = + | BoundConst of constant + | BoundRef of reference + +(* Types representing the attribute information per tag value *) + +type dw_tag_array_type = + { + array_type_decl_file: string option; + array_type_decl_line: constant option; + array_type: reference; + } + +type dw_tag_base_type = + { + base_type_byte_size: constant; + base_type_encoding: encoding; + base_type_name: string; + } + +type dw_tag_compile_unit = + { + compile_unit_comp_dir: string; + compile_unit_high_pc: address; + compile_unit_low_pc: address; + compile_unit_language: language; + compile_unit_name: string; + compile_unit_producer: string; + compile_unit_stmt_list: constant option; + } + +type dw_tag_const_type = + { + const_type: reference; + } + +type dw_tag_enumeration_type = + { + enumeration_decl_file: string option; + enumeration_decl_line: constant option; + enumeration_byte_size: constant; + enumeration_declaration: flag option; + enumeration_name: string; + } + +type dw_tag_enumerator = + { + enumerator_decl_file: string option; + enumerator_decl_line: constant option; + enumerator_value: constant; + enumerator_name: string; + } + +type dw_tag_formal_parameter = + { + formal_parameter_decl_file: string option; + formal_parameter_decl_line: constant option; + formal_parameter_artificial: flag option; + formal_parameter_location: location_value option; + formal_parameter_name: string; + formal_parameter_segment: location_value option; + formal_parameter_type: reference; + formal_parameter_variable_parameter: flag option; + } + +type dw_tag_label = + { + label_low_pc: address; + label_name: string; + } + +type dw_tag_lexical_block = + { + lexical_block__high_pc: address; + lexical_block_low_pc: address; + } + +type dw_tag_member = + { + member_decl_file: string option; + member_decl_line: constant option; + member_byte_size: constant option; + member_bit_offset: constant option; + member_bit_size: constant option; + member_data_member_location: data_location_value option; + member_declaration: flag option; + member_name: string; + member_type: reference; + } + +type dw_tag_pointer_type = + { + pointer_type: reference; + } + +type dw_tag_structure_type = + { + structure_decl_file: string option; + structure_decl_line: constant option; + structure_byte_size: constant; + structure_declaration: flag option; + structure_name: string; + } + +type dw_tag_subprogram = + { + subprogram_decl_file: string option; + subprogram_decl_line: constant option; + subprogram_external: flag option; + subprogram_frame_base: location_value option; + subprogram_high_pc: address; + subprogram_low_pc: address; + subprogram_name: string; + subprogram_prototyped: flag; + subprogram_type: reference; + } + +type dw_tag_subrange_type = + { + subrange_type: reference option; + subrange_upper_bound: bound_value; + } + +type dw_tag_subroutine_type = + { + subroutine_prototyped: flag; + } + +type dw_tag_typedef = + { + typedef_decl_file: string option; + typedef_decl_line: constant option; + typedef_name: string; + typedef_type: reference; + } + +type dw_tag_union_type = + { + union_decl_file: string option; + union_decl_line: constant option; + union_byte_size: constant; + union_name: string; + } + +type dw_tag_unspecified_parameter = + { + unspecified_parameter_decl_file: string option; + unspecified_parameter_decl_line: constant option; + unspecified_parameter_artificial: flag option; + } + +type dw_tag_variable = + { + variable_decl_file: string option; + variable_decl_line: constant option; + variable_declaration: flag option; + variable_external: flag option; + variable_location: location_value option; + variable_name: string; + variable_segment: location_value option; + variable_type: reference; + } + +type dw_tag_volatile_type = + { + volatile_type: reference; + } + +type dw_tag = + | DW_TAG_array_type of dw_tag_array_type + | DW_TAG_base_type of dw_tag_base_type + | DW_TAG_compile_unit of dw_tag_compile_unit + | DW_TAG_const_type of dw_tag_const_type + | DW_TAG_enumeration_type of dw_tag_enumeration_type + | DW_TAG_enumerator of dw_tag_enumerator + | DW_TAG_formal_parameter of dw_tag_formal_parameter + | DW_TAG_label of dw_tag_label + | DW_TAG_lexical_block of dw_tag_lexical_block + | DW_TAG_member of dw_tag_member + | DW_TAG_pointer_type of dw_tag_pointer_type + | DW_TAG_structure_type of dw_tag_structure_type + | DW_TAG_subprogram of dw_tag_subprogram + | DW_TAG_subrange_type of dw_tag_subrange_type + | DW_TAG_subroutine_type of dw_tag_subroutine_type + | DW_TAG_typedef of dw_tag_typedef + | DW_TAG_union_type of dw_tag_union_type + | DW_TAG_unspecified_parameter of dw_tag_unspecified_parameter + | DW_TAG_variable of dw_tag_variable + | DW_TAG_volatile_type of dw_tag_volatile_type + +(* The type of the entries. *) + +type dw_entry = + { + tag: dw_tag; + children: dw_entry list; + id: reference; + } + + diff --git a/debug/DwarfUtil.ml b/debug/DwarfUtil.ml new file mode 100644 index 00000000..79516e65 --- /dev/null +++ b/debug/DwarfUtil.ml @@ -0,0 +1,88 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +(* Utility functions for the dwarf debuging type *) + +open DwarfTypes + +let id = ref 0 + +let next_id () = + let nid = !id in + incr id; nid + +let reset_id () = + id := 0 + +(* Hashtable to from type name to entry id *) +let type_table: (string, int) Hashtbl.t = Hashtbl.create 7 + +(* Clear the type map *) +let reset_type_table () = + Hashtbl.clear type_table + +(* Generate a new entry from a given tag *) +let new_entry tag = + let id = next_id () in + { + tag = tag; + children = []; + id = id; + } + +(* Add an entry as child to another entry *) +let add_children entry child = + {entry with children = child::entry.children;} + + +let list_iter_with_next f list = + let rec aux = (function + | [] -> () + | [a] -> f None a + | a::b::rest -> f (Some b.id) a; aux (b::rest)) in + aux list + +(* Iter over the tree and pass the sibling id *) +let entry_iter_sib f entry = + let rec aux sib entry = + f sib entry; + list_iter_with_next aux entry.children in + aux None entry + + +(* Fold over the tree in prefix order *) +let rec entry_fold f acc entry = + let acc = f acc entry.tag in + List.fold_left (entry_fold f) acc entry.children + +(* Attribute form encoding *) +let dw_form_addr = 0x01 +let dw_form_block2 = 0x03 +let dw_form_block4 = 0x04 +let dw_form_data2 = 0x05 +let dw_form_data4 = 0x06 +let dw_form_data8 = 0x07 +let dw_form_string = 0x08 +let dw_form_block = 0x09 +let dw_form_block1 = 0x0a +let dw_form_data1 = 0x0b +let dw_form_flag = 0x0c +let dw_form_sdata = 0x0d +let dw_form_strp = 0x0e +let dw_form_udata = 0x0f +let dw_form_ref_addr = 0x10 +let dw_form_ref1 = 0x11 +let dw_form_ref2 = 0x12 +let dw_form_ref4 = 0x13 +let dw_form_ref8 = 0x14 +let dw_ref_udata = 0x15 +let dw_ref_indirect = 0x16 diff --git a/driver/Driver.ml b/driver/Driver.ml index b6224c32..16a13375 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -485,7 +485,7 @@ let cmdline_actions = Exact "-fall", Self (fun _ -> set_all language_support_options); Exact "-fnone", Self (fun _ -> unset_all language_support_options); (* Debugging options *) - Exact "-g", Self (fun s -> option_g := true; push_linker_arg s); + Exact "-g", Self (fun s -> option_g := true); (* Code generation options -- more below *) Exact "-O0", Self (fun _ -> unset_all optimization_options); Exact "-O", Self (fun _ -> set_all optimization_options); diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index f058cde5..97b57c0e 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -20,256 +20,16 @@ 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 +open PrintUtil +open PrintLinux +open PrintDiab 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' + include Target (* 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 @@ -286,29 +46,8 @@ let section oc sec = 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) @@ -318,14 +57,6 @@ let print_annot_stmt oc txt targs args = 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 [] @@ -657,37 +388,6 @@ let print_instruction oc tbl pc fallthrough = function | 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 *) @@ -847,11 +547,10 @@ let print_program oc p = 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; + Printer.set_compilation_unit_addrs 1 2; (* TODO This is dummy code *) + PrintAnnot.reset_filenames(); + PrintAnnot.print_version_and_options oc Printer.comment; + Printer.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; - PrintAnnot.close_filenames() - - + Printer.print_epilogue oc diff --git a/powerpc/PrintDiab.ml b/powerpc/PrintDiab.ml new file mode 100644 index 00000000..e431a8c7 --- /dev/null +++ b/powerpc/PrintDiab.ml @@ -0,0 +1,231 @@ +(* *********************************************************************) +(* *) +(* 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 DwarfAbbrvPrinter +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 + + module AbbrvPrinter = DwarfAbbrvPrinter(struct + let string_of_byte value = + Printf.sprintf " .byte %s\n" (if value then "0x1" else "0x2") + + let string_of_abbrv_entry v = + Printf.sprintf " .uleb128 %d\n" v + + let abbrv_start_addr = ref (-1) + + let get_abbrv_start_addr () = !abbrv_start_addr + + let sibling_type_abbr = dw_form_ref4 + let decl_file_type_abbr = dw_form_data4 + let decl_line_type_abbr = dw_form_udata + let type_abbr = dw_form_ref_addr + let name_type_abbr = dw_form_string + let encoding_type_abbr = dw_form_data1 + let byte_size_type_abbr = dw_form_data1 + let high_pc_type_abbr = dw_form_addr + let low_pc_type_abbr = dw_form_addr + let stmt_list_type_abbr = dw_form_data4 + let declaration_type_abbr = dw_form_flag + let external_type_abbr = dw_form_flag + let prototyped_type_abbr = dw_form_flag + let bit_offset_type_abbr = dw_form_data1 + let comp_dir_type_abbr = dw_form_string + let language_type_abbr = dw_form_udata + let producer_type_abbr = dw_form_string + let value_type_abbr = dw_form_sdata + let artificial_type_abbr = dw_form_flag + let variable_parameter_type_abbr = dw_form_flag + let bit_size_type_abbr = dw_form_data1 + let location_const_type_abbr = dw_form_data4 + let location_block_type_abbr = dw_form_block + let data_location_block_type_abbr = dw_form_block + let data_location_ref_type_abbr = dw_form_ref4 + let bound_const_type_abbr = dw_form_udata + let bound_ref_type_abbr=dw_form_ref4 + + + let abbrv_section_start oc = + fprintf oc " .section .debug_abbrev,,n\n"; + let lbl = new_label () in + abbrv_start_addr := lbl; + fprintf oc "%a:\n" label lbl + + let abbrv_section_end oc = + fprintf oc " .section .debug_abbrev,,n\n"; + fprintf oc " .sleb128 0\n" + + let abbrv_prologue oc id = + fprintf oc " .section .debug_abbrev,,n\n"; + fprintf oc " .uleb128 %d\n" id + + let abbrv_epilogue oc = + fprintf oc " .uleb128 0\n"; + fprintf oc " .uleb128 0\n" + + end) + + let rec print_entry oc entry has_sibling = + () + + let print_debug_info oc entry = + AbbrvPrinter.print_debug_abbrv oc entry; + let abbrv_start = AbbrvPrinter.get_abbrv_start_addr () in + let debug_start = new_label () in + let print_info () = + fprintf oc" .section .debug_info,,n\n" in + print_info (); + fprintf oc "%a\n" label debug_start; + let debug_length_start = new_label () in (* Address used for length calculation *) + let debug_end = new_label () in + fprintf oc " .4byte %a-%a\n" label debug_end label debug_length_start; + fprintf oc "%a\n" label debug_length_start; + fprintf oc " .2byte 0x2\n"; (* Dwarf version *) + fprintf oc " .4byte %a\n" label abbrv_start; (* Offset into the abbreviation *) + fprintf oc " .byte %X\n" !Machine.config.Machine.sizeof_ptr; (* Sizeof pointer type *) + print_entry oc entry false; + fprintf oc "%a\n" label debug_end; (* End of the debug section *) + fprintf oc " .sleb128 0\n" + + + end:SYSTEM) diff --git a/powerpc/PrintLinux.ml b/powerpc/PrintLinux.ml new file mode 100644 index 00000000..7ed98d2e --- /dev/null +++ b/powerpc/PrintLinux.ml @@ -0,0 +1,109 @@ +(* *********************************************************************) +(* *) +(* 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 Linux specific printing functions *) + +open Printf +open Datatypes +open Camlcoq +open Sections +open Asm +open PrintUtil + +module Linux_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 = () + + let print_epilogue oc = () + + let set_compilation_unit_addrs _ _ = () + + let print_addr_label _ _ = () + + end:SYSTEM) diff --git a/powerpc/PrintUtil.ml b/powerpc/PrintUtil.ml new file mode 100644 index 00000000..e007b273 --- /dev/null +++ b/powerpc/PrintUtil.ml @@ -0,0 +1,180 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(* Common functions for the AsmPrinter *) + +open Printf +open Maps +open Camlcoq +open Sections +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 + val print_epilogue: out_channel -> unit + val print_addr_label: out_channel -> int -> unit + val set_compilation_unit_addrs: int -> int -> 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" + +(* 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) + + +(* 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]*\\)$" + +(* 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 + +(* 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 |