diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/dwarf.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/dwarf.ml | 4619 |
1 files changed, 4619 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/dwarf.ml b/lib/ocaml_rts/linksem/dwarf.ml new file mode 100644 index 00000000..9e5a31aa --- /dev/null +++ b/lib/ocaml_rts/linksem/dwarf.ml @@ -0,0 +1,4619 @@ +(*Generated by Lem from dwarf.lem.*) +open Lem_basic_classes +open Lem_bool +open Lem_function +open Lem_maybe +open Lem_num +open Lem_string + +open Lem_list (* TODO: check why this is not imported in ELF *) + +open Byte_sequence +open Error +open Hex_printing +open Missing_pervasives +open Show + +open Default_printing + +open Endianness +open String_table + +open Elf_dynamic +open Elf_file +open Elf_header +open Elf_program_header_table +open Elf_relocation +open Elf_section_header_table +open Elf_symbol_table +open Elf_types_native_uint + + +(** ***************** experimental DWARF reading *********** *) + +(* + +This defines a representation of some of the DWARF debug information, +with parsing functions to extract it from the byte sequences of the +relevant ELF sections, and pretty-printing function to dump it in a +human-readable form, similar to that of readelf. The main functions +for this are: + + val extract_dwarf : elf64_file -> maybe dwarf + val pp_dwarf : dwarf -> string + +It also defines evaluation of DWARF expressions and analysis functions +to convert the variable location information to a form suitable for +looking up variable names from machine addresses that arise during +execution, including the call frame address calculation. The main +types and functions for this are: + + type analysed_location_data + val analyse_locations : dwarf -> analysed_location_data + + type evaluated_frame_info + val evaluate_frame_info : dwarf -> evaluated_frame_info + + type dwarf_static + val extract_dwarf_static : elf64_file -> maybe dwarf_static + +The last collects all the above - information that can be computed statically. + +Then to do lookup from addresses to source-code names, we have: + + type analysed_location_data_at_pc + val analysed_locations_at_pc : evaluation_context -> dwarf_static -> natural -> analysed_location_data_at_pc + val names_of_address : dwarf -> analysed_location_data_at_pc -> natural -> list string + +The definitions are deliberately simple-minded, to be quick to write, +easy to see the correspondence to the DWARF text specification, and +potentially support generation of theorem-prover definitions in +future. They are in a pure functional style, making the information +dependencies explicit. They are not written for performance, though +they may be efficient enough for small examples as-is. They are +written in Lem, and compiled from that to executable OCaml. + +The development follows the DWARF 4 pdf specification at http://www.dwarfstd.org/ +though tweaked in places where our examples use earlier versions. It doesn't +systematically cover all the DWARF versions. +It doesn't cover the GNU extensions +(at https://fedorahosted.org/elfutils/wiki/DwarfExtensions). +The representation, parsing, and pretty printing are mostly complete for the +data in these DWARF ELF sections: + +.debug_abbrev +.debug_info +.debug_types +.debug_loc +.debug_str +.debug_ranges +.debug_frame (without augmentations) +.debug_line + +The following DWARF ELF sections are not covered: + +.debug_aranges +.debug_macinfo +.debug_pubnames +.debug_pubtypes + +The evaluation of DWARF expressions covers only some of the operations +- probably enough for common cases. + +The analysis of DWARF location data should be enough to look up names +from the addresses of variables and formal parameters. It does not +currently handle the DWARF type data, so will not be useful for accesses +strictly within the extent of a variable or parameter. + +The 'dwarf' type gives a lightly parsed representation of some of the +dwarf information, with the byte sequences of the above .debug_* +sections parsed into a structured representation. That makes the list +and tree structures explicit, and converts the various numeric types +into just natural, integer, and byte sequences. The lem natural and +integer could be replaced by unsigned and signed 64-bit types; that'd +probably be better for execution but not for theorem-prover use. + +*) + +(* some spec ambiguities (more in comments in-line below): *) +(* can a location list be referenced from multiple compilation units, with different base addresses? *) + + +(** debug *) + +(* workaround debug.lem linking *) +(*val print_endline : string -> unit*) + +let my_debug s:unit= () (*print_endline s*) +let my_debug2 s:unit= () (*print_endline s*) +let my_debug3 s:unit= () (*print_endline s*) +let my_debug4 s:unit= () (*print_endline s*) +let my_debug5 s:unit= (print_endline s) + + +(** ************************************************************ *) +(** ** dwarf representation types **************************** *) +(** ************************************************************ *) + + +type dwarf_attribute_classes = + | DWA_7_5_3 + | DWA_address + | DWA_block + | DWA_constant + | DWA_dash + | DWA_exprloc + | DWA_flag + | DWA_lineptr + | DWA_loclistptr + | DWA_macptr + | DWA_rangelistptr + | DWA_reference + | DWA_string + +(* operations and expression evalution *) + +type operation_argument_type = + | OAT_addr + | OAT_dwarf_format_t + | OAT_uint8 + | OAT_uint16 + | OAT_uint32 + | OAT_uint64 + | OAT_sint8 + | OAT_sint16 + | OAT_sint32 + | OAT_sint64 + | OAT_ULEB128 + | OAT_SLEB128 + | OAT_block + +type operation_argument_value = + | OAV_natural of Nat_big_num.num + | OAV_integer of Nat_big_num.num + | OAV_block of Nat_big_num.num * char list + +type operation_stack = Nat_big_num.num list + +type arithmetic_context = + { + ac_bitwidth: Nat_big_num.num; + ac_half: Nat_big_num.num; (* 2 ^ (ac_bitwidth -1) *) + ac_all: Nat_big_num.num; (* 2 ^ ac_bitwidth *) + ac_max: Nat_big_num.num; (* (2 ^ ac_bitwidth) -1 *) (* also the representation of -1 *) +} + +type operation_semantics = + | OpSem_lit + | OpSem_deref + | OpSem_stack of (arithmetic_context -> operation_stack -> operation_argument_value list -> operation_stack option) + | OpSem_not_supported + | OpSem_binary of (arithmetic_context -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num option) + | OpSem_unary of (arithmetic_context -> Nat_big_num.num -> Nat_big_num.num option) + | OpSem_opcode_lit of Nat_big_num.num + | OpSem_reg + | OpSem_breg + | OpSem_bregx + | OpSem_fbreg + | OpSem_deref_size + | OpSem_nop + | OpSem_piece + | OpSem_bit_piece + | OpSem_implicit_value + | OpSem_stack_value + | OpSem_call_frame_cfa + +type operation = + { + op_code: Nat_big_num.num; + op_string: string; + op_argument_values: operation_argument_value list; + op_semantics: operation_semantics; + } + + +(* the result of a location expression evaluation is a single_location (or failure) *) + +type simple_location = + | SL_memory_address of Nat_big_num.num + | SL_register of Nat_big_num.num + | SL_implicit of char list (* used for implicit and stack values *) + | SL_empty + +type composite_location_piece = + | CLP_piece of Nat_big_num.num * simple_location + | CLP_bit_piece of Nat_big_num.num * Nat_big_num.num * simple_location + +type single_location = + | SL_simple of simple_location + | SL_composite of composite_location_piece list + +(* location expression evaluation is a stack machine operating over the following state *) + +type state = + { + s_stack: operation_stack; + s_value: simple_location; + s_location_pieces: composite_location_piece list; + } + +(* location expression evaluation can involve register and memory reads, via the following interface *) + +type 'a register_read_result = + | RRR_result of Nat_big_num.num + | RRR_not_currently_available + | RRR_bad_register_number + +type 'a memory_read_result = + | MRR_result of Nat_big_num.num + | MRR_not_currently_available + | MRR_bad_address + +type evaluation_context = + { + read_register: Nat_big_num.num -> Nat_big_num.num register_read_result; + read_memory: Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num memory_read_result; + } + + +(* dwarf sections *) + +type dwarf_format = + | Dwarf32 + | Dwarf64 + +(* .debug_abbrev section *) + +type abbreviation_declaration = + { + ad_abbreviation_code: Nat_big_num.num; + ad_tag: Nat_big_num.num; + ad_has_children: bool; + ad_attribute_specifications: (Nat_big_num.num * Nat_big_num.num) list; + } + +type abbreviations_table = abbreviation_declaration list + +(* .debug_info section *) + +type attribute_value = + | AV_addr of Nat_big_num.num + | AV_block of Nat_big_num.num * char list + | AV_constantN of Nat_big_num.num * char list + | AV_constant_SLEB128 of Nat_big_num.num + | AV_constant_ULEB128 of Nat_big_num.num + | AV_exprloc of Nat_big_num.num * char list + | AV_flag of bool + | AV_ref of Nat_big_num.num + | AV_ref_addr of Nat_big_num.num (* dwarf_format dependent *) + | AV_ref_sig8 of Nat_big_num.num + | AV_sec_offset of Nat_big_num.num + | AV_string of char list (* not including terminating null *) + | AV_strp of Nat_big_num.num (* dwarf_format dependent *) + +type die = + { + die_offset: Nat_big_num.num; + die_abbreviation_code: Nat_big_num.num; + die_abbreviation_declaration: abbreviation_declaration; + die_attribute_values: (Nat_big_num.num (*pos*) * attribute_value) list; + die_children: die list; + } + +type compilation_unit_header = + { + cuh_offset: Nat_big_num.num; + cuh_dwarf_format: dwarf_format; + cuh_unit_length: Nat_big_num.num; + cuh_version: Nat_big_num.num; + cuh_debug_abbrev_offset: Nat_big_num.num; + cuh_address_size: Nat_big_num.num; + } + +type compilation_unit = + { + cu_header: compilation_unit_header; + cu_abbreviations_table: abbreviations_table; + cu_die: die; + } + +type compilation_units = compilation_unit list + +(* .debug_type section *) + +type type_unit_header = + { + tuh_cuh: compilation_unit_header; + tuh_type_signature: Nat_big_num.num; + tuh_type_offset: Nat_big_num.num; + } + +type type_unit = + { + tu_header: type_unit_header; + tu_abbreviations_table: abbreviations_table; + tu_die: die; + } + +type type_units = type_unit list + +(* .debug_loc section *) + +type single_location_description = char list + +type location_list_entry = + { + lle_beginning_address_offset: Nat_big_num.num; + lle_ending_address_offset: Nat_big_num.num; + lle_single_location_description: single_location_description; + } + +type base_address_selection_entry = + { + base_address: Nat_big_num.num; + } + +type location_list_item = + | LLI_lle of location_list_entry + | LLI_base of base_address_selection_entry + +type location_list = Nat_big_num.num (*offset*) * location_list_item list + +type location_list_list = location_list list + +(* .debug_ranges section *) + +type range_list_entry = + { + rle_beginning_address_offset: Nat_big_num.num; + rle_ending_address_offset: Nat_big_num.num; + } + +type range_list_item = + | RLI_rle of range_list_entry + | RLI_base of base_address_selection_entry + +type range_list = Nat_big_num.num (*offset*) * range_list_item list + +type range_list_list = range_list list + +(* .debug_frame section: call frame instructions *) + +type cfa_address = Nat_big_num.num +type cfa_block = char list +type cfa_delta = Nat_big_num.num +type cfa_offset = Nat_big_num.num +type cfa_register = Nat_big_num.num +type cfa_sfoffset = Nat_big_num.num + +type call_frame_argument_type = + | CFAT_address + | CFAT_delta1 + | CFAT_delta2 + | CFAT_delta4 + | CFAT_delta_ULEB128 + | CFAT_offset (*ULEB128*) + | CFAT_sfoffset (*SLEB128*) + | CFAT_register (*ULEB128*) + | CFAT_block + +type call_frame_argument_value = + | CFAV_address of cfa_address + | CFAV_block of cfa_block + | CFAV_delta of cfa_delta + | CFAV_offset of cfa_offset + | CFAV_register of cfa_register + | CFAV_sfoffset of cfa_sfoffset + +type call_frame_instruction = + | DW_CFA_advance_loc of cfa_delta + | DW_CFA_offset of cfa_register * cfa_offset + | DW_CFA_restore of cfa_register + | DW_CFA_nop + | DW_CFA_set_loc of cfa_address + | DW_CFA_advance_loc1 of cfa_delta + | DW_CFA_advance_loc2 of cfa_delta + | DW_CFA_advance_loc4 of cfa_delta + | DW_CFA_offset_extended of cfa_register * cfa_offset + | DW_CFA_restore_extended of cfa_register + | DW_CFA_undefined of cfa_register + | DW_CFA_same_value of cfa_register + | DW_CFA_register of cfa_register * cfa_register + | DW_CFA_remember_state + | DW_CFA_restore_state + | DW_CFA_def_cfa of cfa_register * cfa_offset + | DW_CFA_def_cfa_register of cfa_register + | DW_CFA_def_cfa_offset of cfa_offset + | DW_CFA_def_cfa_expression of cfa_block + | DW_CFA_expression of cfa_register * cfa_block + | DW_CFA_offset_extended_sf of cfa_register * cfa_sfoffset + | DW_CFA_def_cfa_sf of cfa_register * cfa_sfoffset + | DW_CFA_def_cfa_offset_sf of cfa_sfoffset + | DW_CFA_val_offset of cfa_register * cfa_offset + | DW_CFA_val_offset_sf of cfa_register * cfa_sfoffset + | DW_CFA_val_expression of cfa_register * cfa_block + | DW_CFA_unknown of char + +(* .debug_frame section: top-level *) + +type cie = + { + cie_offset: Nat_big_num.num; + cie_length: Nat_big_num.num; + cie_id: Nat_big_num.num; + cie_version: Nat_big_num.num; + cie_augmentation: char list; (* not including terminating null *) + cie_address_size: Nat_big_num.num option; + cie_segment_size: Nat_big_num.num option; + cie_code_alignment_factor: Nat_big_num.num; + cie_data_alignment_factor: Nat_big_num.num; + cie_return_address_register: cfa_register; + cie_initial_instructions_bytes: char list; + cie_initial_instructions: call_frame_instruction list; + } + +type fde = + { + fde_offset: Nat_big_num.num; + fde_length: Nat_big_num.num; + fde_cie_pointer: Nat_big_num.num; + fde_initial_location_segment_selector: Nat_big_num.num option; + fde_initial_location_address: Nat_big_num.num; + fde_address_range: Nat_big_num.num; + fde_instructions_bytes: char list; + fde_instructions: call_frame_instruction list; + } + +type frame_info_element = + | FIE_cie of cie + | FIE_fde of fde + +type frame_info = frame_info_element list + + +(* evaluated cfa data *) + +type cfa_rule = + | CR_undefined + | CR_register of cfa_register * Nat_big_num.num + | CR_expression of single_location_description + +type register_rule = + | RR_undefined (*A register that has this rule has no recoverable value in the previous frame. + (By convention, it is not preserved by a callee.)*) + | RR_same_value (*This register has not been modified from the previous frame. (By convention, + it is preserved by the callee, but the callee has not modified it.)*) + | RR_offset of Nat_big_num.num (* The previous value of this register is saved at the address CFA+N where CFA + is the current CFA value and N is a signed offset.*) + | RR_val_offset of Nat_big_num.num (* The previous value of this register is the value CFA+N where CFA is the + current CFA value and N is a signed offset.*) + | RR_register of Nat_big_num.num (* The previous value of this register is stored in another register numbered R.*) + | RR_expression of single_location_description (* The previous value of this register is located at the address produced by + executing the DWARF expression E.*) + | RR_val_expression of single_location_description (* The previous value of this register is the value produced by executing the +DWARF expression E.*) + | RR_architectural (*The rule is defined externally to this specification by the augmenter*) + +type register_rule_map = (cfa_register * register_rule) list + +type cfa_table_row = + { + ctr_loc: Nat_big_num.num; + ctr_cfa: cfa_rule; + ctr_regs: register_rule_map; + } + +type cfa_state = + { + cs_current_row: cfa_table_row; + cs_previous_rows: cfa_table_row list; + cs_initial_instructions_row: cfa_table_row; + cs_row_stack: cfa_table_row list; + } + + +type evaluated_frame_info = (fde * cfa_table_row list) + list + + +(* line number *) + +type line_number_argument_type = + | LNAT_address + | LNAT_ULEB128 + | LNAT_SLEB128 + | LNAT_uint16 + | LNAT_string + +type line_number_argument_value = + | LNAV_address of Nat_big_num.num + | LNAV_ULEB128 of Nat_big_num.num + | LNAV_SLEB128 of Nat_big_num.num + | LNAV_uint16 of Nat_big_num.num + | LNAV_string of char list (* not including terminating null *) + +type line_number_operation = + (* standard *) + | DW_LNS_copy + | DW_LNS_advance_pc of Nat_big_num.num + | DW_LNS_advance_line of Nat_big_num.num + | DW_LNS_set_file of Nat_big_num.num + | DW_LNS_set_column of Nat_big_num.num + | DW_LNS_negate_stmt + | DW_LNS_set_basic_block + | DW_LNS_const_add_pc + | DW_LNS_fixed_advance_pc of Nat_big_num.num + | DW_LNS_set_prologue_end + | DW_LNS_set_epilogue_begin + | DW_LNS_set_isa of Nat_big_num.num + (* extended *) + | DW_LNE_end_sequence + | DW_LNE_set_address of Nat_big_num.num + | DW_LNE_define_file of ( char list) * Nat_big_num.num * Nat_big_num.num * Nat_big_num.num + | DW_LNE_set_discriminator of Nat_big_num.num + (* special *) + | DW_LN_special of Nat_big_num.num (* the adjusted opcode *) + +type line_number_file_entry = + { + lnfe_path: char list; + lnfe_directory_index: Nat_big_num.num; + lnfe_last_modification: Nat_big_num.num; + lnfe_length: Nat_big_num.num; + } + +type line_number_header = + { + lnh_offset: Nat_big_num.num; + lnh_dwarf_format: dwarf_format; + lnh_unit_length: Nat_big_num.num; + lnh_version: Nat_big_num.num; + lnh_header_length: Nat_big_num.num; + lnh_minimum_instruction_length: Nat_big_num.num; + lnh_maximum_operations_per_instruction: Nat_big_num.num; + lnh_default_is_stmt: bool; + lnh_line_base: Nat_big_num.num; + lnh_line_range: Nat_big_num.num; + lnh_opcode_base: Nat_big_num.num; + lnh_standard_opcode_lengths: Nat_big_num.num list; + lnh_include_directories: ( char list) list; + lnh_file_names: line_number_file_entry list; + } + +type line_number_program = + { + lnp_header: line_number_header; + lnp_operations: line_number_operation list; + } + +(* line number evaluation *) + +type line_number_registers = + { + lnr_address: Nat_big_num.num; + lnr_op_index: Nat_big_num.num; + lnr_file: Nat_big_num.num; + lnr_line: Nat_big_num.num; + lnr_column: Nat_big_num.num; + lnr_is_stmt: bool; + lnr_basic_block: bool; + lnr_end_sequence: bool; + lnr_prologue_end: bool; + lnr_epilogue_begin: bool; + lnr_isa: Nat_big_num.num; + lnr_discriminator: Nat_big_num.num; + } + + + + +(* top-level collection of dwarf data *) + +type dwarf = + { + d_endianness: Endianness.endianness; (* from the ELF *) + d_str: char list; + d_compilation_units: compilation_units; + d_type_units: type_units; + d_loc: location_list_list; + d_ranges: range_list_list; + d_frame_info: frame_info; + d_line_info: line_number_program list; + } + +(* analysed location data *) + +type analysed_location_data = ((compilation_unit * ( die list) * die) * ( (Nat_big_num.num * Nat_big_num.num * single_location_description)list)option) list + +type analysed_location_data_at_pc = ((compilation_unit * ( die list) * die) * (Nat_big_num.num * Nat_big_num.num * single_location_description * single_location error)) list + +(* evaluated line data *) + +type evaluated_line_info = (line_number_header * line_number_registers list) list + +type dwarf_static = + { + ds_dwarf: dwarf; + ds_analysed_location_data: analysed_location_data; + ds_evaluated_frame_info: evaluated_frame_info; + ds_evaluated_line_info: evaluated_line_info; + } + +type dwarf_dynamic_at_pc = analysed_location_data_at_pc + +(** context for parsing and pp functions *) + +type p_context = + { + endianness: Endianness.endianness; + } + + + +(** ************************************************************ *) +(** ** missing pervasives ************************************ *) +(** ************************************************************ *) + +(** hex parsing *) + +(* this should be in lem, either built-in or in pervasives *) + +(*val natural_of_char : char -> natural*) +let natural_of_char c:Nat_big_num.num= + (let naturalOrd c'= (Nat_big_num.of_int (Char.code c')) in + let n = (naturalOrd c) in + if Nat_big_num.greater_equal n (naturalOrd '0') && Nat_big_num.less_equal n (naturalOrd '9') then Nat_big_num.sub_nat n (naturalOrd '0') + else if Nat_big_num.greater_equal n (naturalOrd 'A') && Nat_big_num.less_equal n (naturalOrd 'F') then Nat_big_num.add (Nat_big_num.sub_nat n (naturalOrd 'A'))(Nat_big_num.of_int 10) + else if Nat_big_num.greater_equal n (naturalOrd 'a') && Nat_big_num.less_equal n (naturalOrd 'f') then Nat_big_num.add (Nat_big_num.sub_nat n (naturalOrd 'a'))(Nat_big_num.of_int 10) + else failwith ("natural_of_char argument #'" ^ (Xstring.implode [c] ^ "' not in 0-9,A-F,a-f"))) + +(*val natural_of_hex' : list char -> natural*) +let rec natural_of_hex' cs:Nat_big_num.num= + ((match cs with + | c :: cs' -> Nat_big_num.add (natural_of_char c) (Nat_big_num.mul(Nat_big_num.of_int 16) (natural_of_hex' cs')) + | [] ->Nat_big_num.of_int 0 + )) + +(*val natural_of_hex : string -> natural*) +let natural_of_hex s:Nat_big_num.num= + (let cs = (Xstring.explode s) in + (match cs with + | '0'::'x'::cs' -> + (match cs' with + | c :: _ -> natural_of_hex' (List.rev cs') + | [] -> failwith ("natural_of_hex argument \"" ^ (s ^ "\" has no digits")) + ) + | _ -> failwith ("natural_of_hex argument \"" ^ (s ^ "\" does not begin 0x")) + )) + + +(* natural version of List.index *) +(*val index_natural : forall 'a. list 'a -> natural -> maybe 'a*) +let rec index_natural l n:'a option= ((match l with + | [] -> None + | x :: xs -> if Nat_big_num.equal n(Nat_big_num.of_int 0) then Some x else index_natural xs (Nat_big_num.sub_nat n(Nat_big_num.of_int 1)) +)) + +let partialNaturalFromInteger (i:Nat_big_num.num) : Nat_big_num.num= + (if Nat_big_num.less i(Nat_big_num.of_int 0) then failwith "partialNaturalFromInteger" else Nat_big_num.abs i) + +(*val natural_nat_shift_left : natural -> nat -> natural*) + +(*val natural_nat_shift_right : natural -> nat -> natural*) + + + +(** ************************************************************ *) +(** ** dwarf encodings *************************************** *) +(** ************************************************************ *) + +(* these encoding tables are pasted from the DWARF 4 specification *) + +(* tag encoding *) +let tag_encodings:(string*Nat_big_num.num)list= ([ + ("DW_TAG_array_type" , natural_of_hex "0x01" ); + ("DW_TAG_class_type" , natural_of_hex "0x02" ); + ("DW_TAG_entry_point" , natural_of_hex "0x03" ); + ("DW_TAG_enumeration_type" , natural_of_hex "0x04" ); + ("DW_TAG_formal_parameter" , natural_of_hex "0x05" ); + ("DW_TAG_imported_declaration" , natural_of_hex "0x08" ); + ("DW_TAG_label" , natural_of_hex "0x0a" ); + ("DW_TAG_lexical_block" , natural_of_hex "0x0b" ); + ("DW_TAG_member" , natural_of_hex "0x0d" ); + ("DW_TAG_pointer_type" , natural_of_hex "0x0f" ); + ("DW_TAG_reference_type" , natural_of_hex "0x10" ); + ("DW_TAG_compile_unit" , natural_of_hex "0x11" ); + ("DW_TAG_string_type" , natural_of_hex "0x12" ); + ("DW_TAG_structure_type" , natural_of_hex "0x13" ); + ("DW_TAG_subroutine_type" , natural_of_hex "0x15" ); + ("DW_TAG_typedef" , natural_of_hex "0x16" ); + ("DW_TAG_union_type" , natural_of_hex "0x17" ); + ("DW_TAG_unspecified_parameters" , natural_of_hex "0x18" ); + ("DW_TAG_variant" , natural_of_hex "0x19" ); + ("DW_TAG_common_block" , natural_of_hex "0x1a" ); + ("DW_TAG_common_inclusion" , natural_of_hex "0x1b" ); + ("DW_TAG_inheritance" , natural_of_hex "0x1c" ); + ("DW_TAG_inlined_subroutine" , natural_of_hex "0x1d" ); + ("DW_TAG_module" , natural_of_hex "0x1e" ); + ("DW_TAG_ptr_to_member_type" , natural_of_hex "0x1f" ); + ("DW_TAG_set_type" , natural_of_hex "0x20" ); + ("DW_TAG_subrange_type" , natural_of_hex "0x21" ); + ("DW_TAG_with_stmt" , natural_of_hex "0x22" ); + ("DW_TAG_access_declaration" , natural_of_hex "0x23" ); + ("DW_TAG_base_type" , natural_of_hex "0x24" ); + ("DW_TAG_catch_block" , natural_of_hex "0x25" ); + ("DW_TAG_const_type" , natural_of_hex "0x26" ); + ("DW_TAG_constant" , natural_of_hex "0x27" ); + ("DW_TAG_enumerator" , natural_of_hex "0x28" ); + ("DW_TAG_file_type" , natural_of_hex "0x29" ); + ("DW_TAG_friend" , natural_of_hex "0x2a" ); + ("DW_TAG_namelist" , natural_of_hex "0x2b" ); + ("DW_TAG_namelist_item" , natural_of_hex "0x2c" ); + ("DW_TAG_packed_type" , natural_of_hex "0x2d" ); + ("DW_TAG_subprogram" , natural_of_hex "0x2e" ); + ("DW_TAG_template_type_parameter" , natural_of_hex "0x2f" ); + ("DW_TAG_template_value_parameter" , natural_of_hex "0x30" ); + ("DW_TAG_thrown_type" , natural_of_hex "0x31" ); + ("DW_TAG_try_block" , natural_of_hex "0x32" ); + ("DW_TAG_variant_part" , natural_of_hex "0x33" ); + ("DW_TAG_variable" , natural_of_hex "0x34" ); + ("DW_TAG_volatile_type" , natural_of_hex "0x35" ); + ("DW_TAG_dwarf_procedure" , natural_of_hex "0x36" ); + ("DW_TAG_restrict_type" , natural_of_hex "0x37" ); + ("DW_TAG_interface_type" , natural_of_hex "0x38" ); + ("DW_TAG_namespace" , natural_of_hex "0x39" ); + ("DW_TAG_imported_module" , natural_of_hex "0x3a" ); + ("DW_TAG_unspecified_type" , natural_of_hex "0x3b" ); + ("DW_TAG_partial_unit" , natural_of_hex "0x3c" ); + ("DW_TAG_imported_unit" , natural_of_hex "0x3d" ); + ("DW_TAG_condition" , natural_of_hex "0x3f" ); + ("DW_TAG_shared_type" , natural_of_hex "0x40" ); + ("DW_TAG_type_unit" , natural_of_hex "0x41" ); + ("DW_TAG_rvalue_reference_type" , natural_of_hex "0x42" ); + ("DW_TAG_template_alias" , natural_of_hex "0x43" ); + ("DW_TAG_lo_user" , natural_of_hex "0x4080"); + ("DW_TAG_hi_user" , natural_of_hex "0xffff") +]) + + +(* child determination encoding *) + +let vDW_CHILDREN_no:Nat_big_num.num= (natural_of_hex "0x00") +let vDW_CHILDREN_yes:Nat_big_num.num= (natural_of_hex "0x01") + + +(* attribute encoding *) + +let attribute_encodings:(string*Nat_big_num.num*(dwarf_attribute_classes)list)list= ([ + ("DW_AT_sibling" , natural_of_hex "0x01", [DWA_reference]) ; + ("DW_AT_location" , natural_of_hex "0x02", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_name" , natural_of_hex "0x03", [DWA_string]) ; + ("DW_AT_ordering" , natural_of_hex "0x09", [DWA_constant]) ; + ("DW_AT_byte_size" , natural_of_hex "0x0b", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_bit_offset" , natural_of_hex "0x0c", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_bit_size" , natural_of_hex "0x0d", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_stmt_list" , natural_of_hex "0x10", [DWA_lineptr]) ; + ("DW_AT_low_pc" , natural_of_hex "0x11", [DWA_address]) ; + ("DW_AT_high_pc" , natural_of_hex "0x12", [DWA_address; DWA_constant]) ; + ("DW_AT_language" , natural_of_hex "0x13", [DWA_constant]) ; + ("DW_AT_discr" , natural_of_hex "0x15", [DWA_reference]) ; + ("DW_AT_discr_value" , natural_of_hex "0x16", [DWA_constant]) ; + ("DW_AT_visibility" , natural_of_hex "0x17", [DWA_constant]) ; + ("DW_AT_import" , natural_of_hex "0x18", [DWA_reference]) ; + ("DW_AT_string_length" , natural_of_hex "0x19", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_common_reference" , natural_of_hex "0x1a", [DWA_reference]) ; + ("DW_AT_comp_dir" , natural_of_hex "0x1b", [DWA_string]) ; + ("DW_AT_const_value" , natural_of_hex "0x1c", [DWA_block; DWA_constant; DWA_string]) ; + ("DW_AT_containing_type" , natural_of_hex "0x1d", [DWA_reference]) ; + ("DW_AT_default_value" , natural_of_hex "0x1e", [DWA_reference]) ; + ("DW_AT_inline" , natural_of_hex "0x20", [DWA_constant]) ; + ("DW_AT_is_optional" , natural_of_hex "0x21", [DWA_flag]) ; + ("DW_AT_lower_bound" , natural_of_hex "0x22", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_producer" , natural_of_hex "0x25", [DWA_string]) ; + ("DW_AT_prototyped" , natural_of_hex "0x27", [DWA_flag]) ; + ("DW_AT_return_addr" , natural_of_hex "0x2a", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_start_scope" , natural_of_hex "0x2c", [DWA_constant; DWA_rangelistptr]) ; + ("DW_AT_bit_stride" , natural_of_hex "0x2e", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_upper_bound" , natural_of_hex "0x2f", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_abstract_origin" , natural_of_hex "0x31", [DWA_reference]) ; + ("DW_AT_accessibility" , natural_of_hex "0x32", [DWA_constant]) ; + ("DW_AT_address_class" , natural_of_hex "0x33", [DWA_constant]) ; + ("DW_AT_artificial" , natural_of_hex "0x34", [DWA_flag]) ; + ("DW_AT_base_types" , natural_of_hex "0x35", [DWA_reference]) ; + ("DW_AT_calling_convention" , natural_of_hex "0x36", [DWA_constant]) ; + ("DW_AT_count" , natural_of_hex "0x37", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_data_member_location" , natural_of_hex "0x38", [DWA_constant; DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_decl_column" , natural_of_hex "0x39", [DWA_constant]) ; + ("DW_AT_decl_file" , natural_of_hex "0x3a", [DWA_constant]) ; + ("DW_AT_decl_line" , natural_of_hex "0x3b", [DWA_constant]) ; + ("DW_AT_declaration" , natural_of_hex "0x3c", [DWA_flag]) ; + ("DW_AT_discr_list" , natural_of_hex "0x3d", [DWA_block]) ; + ("DW_AT_encoding" , natural_of_hex "0x3e", [DWA_constant]) ; + ("DW_AT_external" , natural_of_hex "0x3f", [DWA_flag]) ; + ("DW_AT_frame_base" , natural_of_hex "0x40", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_friend" , natural_of_hex "0x41", [DWA_reference]) ; + ("DW_AT_identifier_case" , natural_of_hex "0x42", [DWA_constant]) ; + ("DW_AT_macro_info" , natural_of_hex "0x43", [DWA_macptr]) ; + ("DW_AT_namelist_item" , natural_of_hex "0x44", [DWA_reference]) ; + ("DW_AT_priority" , natural_of_hex "0x45", [DWA_reference]) ; + ("DW_AT_segment" , natural_of_hex "0x46", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_specification" , natural_of_hex "0x47", [DWA_reference]) ; + ("DW_AT_static_link" , natural_of_hex "0x48", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_type" , natural_of_hex "0x49", [DWA_reference]) ; + ("DW_AT_use_location" , natural_of_hex "0x4a", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_variable_parameter" , natural_of_hex "0x4b", [DWA_flag]) ; + ("DW_AT_virtuality" , natural_of_hex "0x4c", [DWA_constant]) ; + ("DW_AT_vtable_elem_location" , natural_of_hex "0x4d", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_allocated" , natural_of_hex "0x4e", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_associated" , natural_of_hex "0x4f", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_data_location" , natural_of_hex "0x50", [DWA_exprloc]) ; + ("DW_AT_byte_stride" , natural_of_hex "0x51", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_entry_pc" , natural_of_hex "0x52", [DWA_address]) ; + ("DW_AT_use_UTF8" , natural_of_hex "0x53", [DWA_flag]) ; + ("DW_AT_extension" , natural_of_hex "0x54", [DWA_reference]) ; + ("DW_AT_ranges" , natural_of_hex "0x55", [DWA_rangelistptr]) ; + ("DW_AT_trampoline" , natural_of_hex "0x56", [DWA_address; DWA_flag; DWA_reference; DWA_string]); + ("DW_AT_call_column" , natural_of_hex "0x57", [DWA_constant]) ; + ("DW_AT_call_file" , natural_of_hex "0x58", [DWA_constant]) ; + ("DW_AT_call_line" , natural_of_hex "0x59", [DWA_constant]) ; + ("DW_AT_description" , natural_of_hex "0x5a", [DWA_string]) ; + ("DW_AT_binary_scale" , natural_of_hex "0x5b", [DWA_constant]) ; + ("DW_AT_decimal_scale" , natural_of_hex "0x5c", [DWA_constant]) ; + ("DW_AT_small" , natural_of_hex "0x5d", [DWA_reference]) ; + ("DW_AT_decimal_sign" , natural_of_hex "0x5e", [DWA_constant]) ; + ("DW_AT_digit_count" , natural_of_hex "0x5f", [DWA_constant]) ; + ("DW_AT_picture_string" , natural_of_hex "0x60", [DWA_string]) ; + ("DW_AT_mutable" , natural_of_hex "0x61", [DWA_flag]) ; + ("DW_AT_threads_scaled" , natural_of_hex "0x62", [DWA_flag]) ; + ("DW_AT_explicit" , natural_of_hex "0x63", [DWA_flag]) ; + ("DW_AT_object_pointer" , natural_of_hex "0x64", [DWA_reference]) ; + ("DW_AT_endianity" , natural_of_hex "0x65", [DWA_constant]) ; + ("DW_AT_elemental" , natural_of_hex "0x66", [DWA_flag]) ; + ("DW_AT_pure" , natural_of_hex "0x67", [DWA_flag]) ; + ("DW_AT_recursive" , natural_of_hex "0x68", [DWA_flag]) ; + ("DW_AT_signature" , natural_of_hex "0x69", [DWA_reference]) ; + ("DW_AT_main_subprogram" , natural_of_hex "0x6a", [DWA_flag]) ; + ("DW_AT_data_bit_offset" , natural_of_hex "0x6b", [DWA_constant]) ; + ("DW_AT_const_expr" , natural_of_hex "0x6c", [DWA_flag]) ; + ("DW_AT_enum_class" , natural_of_hex "0x6d", [DWA_flag]) ; + ("DW_AT_linkage_name" , natural_of_hex "0x6e", [DWA_string]) ; + ("DW_AT_lo_user" , natural_of_hex "0x2000", [DWA_dash]) ; + ("DW_AT_hi_user" , natural_of_hex "0x3fff", [DWA_dash]) +]) + + +(* attribute form encoding *) + +let attribute_form_encodings:(string*Nat_big_num.num*(dwarf_attribute_classes)list)list= ([ + ("DW_FORM_addr" , natural_of_hex "0x01", [DWA_address]) ; + ("DW_FORM_block2" , natural_of_hex "0x03", [DWA_block]) ; + ("DW_FORM_block4" , natural_of_hex "0x04", [DWA_block]) ; + ("DW_FORM_data2" , natural_of_hex "0x05", [DWA_constant]) ; + ("DW_FORM_data4" , natural_of_hex "0x06", [DWA_constant]) ; + ("DW_FORM_data8" , natural_of_hex "0x07", [DWA_constant]) ; + ("DW_FORM_string" , natural_of_hex "0x08", [DWA_string]) ; + ("DW_FORM_block" , natural_of_hex "0x09", [DWA_block]) ; + ("DW_FORM_block1" , natural_of_hex "0x0a", [DWA_block]) ; + ("DW_FORM_data1" , natural_of_hex "0x0b", [DWA_constant]) ; + ("DW_FORM_flag" , natural_of_hex "0x0c", [DWA_flag]) ; + ("DW_FORM_sdata" , natural_of_hex "0x0d", [DWA_constant]) ; + ("DW_FORM_strp" , natural_of_hex "0x0e", [DWA_string]) ; + ("DW_FORM_udata" , natural_of_hex "0x0f", [DWA_constant]) ; + ("DW_FORM_ref_addr" , natural_of_hex "0x10", [DWA_reference]); + ("DW_FORM_ref1" , natural_of_hex "0x11", [DWA_reference]); + ("DW_FORM_ref2" , natural_of_hex "0x12", [DWA_reference]); + ("DW_FORM_ref4" , natural_of_hex "0x13", [DWA_reference]); + ("DW_FORM_ref8" , natural_of_hex "0x14", [DWA_reference]); + ("DW_FORM_ref_udata" , natural_of_hex "0x15", [DWA_reference]); + ("DW_FORM_indirect" , natural_of_hex "0x16", [DWA_7_5_3]) ; + ("DW_FORM_sec_offset" , natural_of_hex "0x17", [DWA_lineptr; DWA_loclistptr; DWA_macptr; DWA_rangelistptr]) ; + ("DW_FORM_exprloc" , natural_of_hex "0x18", [DWA_exprloc]) ; + ("DW_FORM_flag_present", natural_of_hex "0x19", [DWA_flag]) ; + ("DW_FORM_ref_sig8" , natural_of_hex "0x20", [DWA_reference]) +]) + + +(* operation encoding *) + +let operation_encodings:(string*Nat_big_num.num*(operation_argument_type)list*operation_semantics)list= ([ +("DW_OP_addr", natural_of_hex "0x03", [OAT_addr] , OpSem_lit); (*1*) (*constant address (size target specific)*) +("DW_OP_deref", natural_of_hex "0x06", [] , OpSem_deref); (*0*) +("DW_OP_const1u", natural_of_hex "0x08", [OAT_uint8] , OpSem_lit); (*1*) (* 1-byte constant *) +("DW_OP_const1s", natural_of_hex "0x09", [OAT_sint8] , OpSem_lit); (*1*) (* 1-byte constant *) +("DW_OP_const2u", natural_of_hex "0x0a", [OAT_uint16] , OpSem_lit); (*1*) (* 2-byte constant *) +("DW_OP_const2s", natural_of_hex "0x0b", [OAT_sint16] , OpSem_lit); (*1*) (* 2-byte constant *) +("DW_OP_const4u", natural_of_hex "0x0c", [OAT_uint32] , OpSem_lit); (*1*) (* 4-byte constant *) +("DW_OP_const4s", natural_of_hex "0x0d", [OAT_sint32] , OpSem_lit); (*1*) (* 4-byte constant *) +("DW_OP_const8u", natural_of_hex "0x0e", [OAT_uint64] , OpSem_lit); (*1*) (* 8-byte constant *) +("DW_OP_const8s", natural_of_hex "0x0f", [OAT_sint64] , OpSem_lit); (*1*) (* 8-byte constant *) +("DW_OP_constu", natural_of_hex "0x10", [OAT_ULEB128] , OpSem_lit); (*1*) (* ULEB128 constant *) +("DW_OP_consts", natural_of_hex "0x11", [OAT_SLEB128] , OpSem_lit); (*1*) (* SLEB128 constant *) +("DW_OP_dup", natural_of_hex "0x12", [] , OpSem_stack (fun ac vs args -> (match vs with v::vs -> Some (v::(v::vs)) | _ -> None ))); (*0*) +("DW_OP_drop", natural_of_hex "0x13", [] , OpSem_stack (fun ac vs args -> (match vs with v::vs -> Some vs | _ -> None ))); (*0*) +("DW_OP_over", natural_of_hex "0x14", [] , OpSem_stack (fun ac vs args -> (match vs with v::v'::vs -> Some (v'::(v::(v'::vs))) | _ -> None ))); (*0*) +("DW_OP_pick", natural_of_hex "0x15", [OAT_uint8] , OpSem_stack (fun ac vs args -> (match args with [OAV_natural n] -> (match index_natural vs n with Some v -> Some (v::vs) | None -> None ) | _ -> None ))); (*1*) (* 1-byte stack index *) +("DW_OP_swap", natural_of_hex "0x16", [] , OpSem_stack (fun ac vs args -> (match vs with v::v'::vs -> Some (v'::(v::vs)) | _ -> None ))); (*0*) +("DW_OP_rot", natural_of_hex "0x17", [] , OpSem_stack (fun ac vs args -> (match vs with v::v'::v''::vs -> Some (v'::(v''::(v::vs))) | _ -> None ))); (*0*) +("DW_OP_xderef", natural_of_hex "0x18", [] , OpSem_not_supported); (*0*) +("DW_OP_abs", natural_of_hex "0x19", [] , OpSem_unary (fun ac v -> if Nat_big_num.less v ac.ac_half then Some v else if Nat_big_num.equal v ac.ac_max then None else Some (Nat_big_num.sub_nat ac.ac_all v))); (*0*) +("DW_OP_and", natural_of_hex "0x1a", [] , OpSem_binary (fun ac v1 v2 -> Some (Nat_big_num.bitwise_and v1 v2))); (*0*) +("DW_OP_div", natural_of_hex "0x1b", [] , OpSem_not_supported) (*TODO*); (*0*) +("DW_OP_minus", natural_of_hex "0x1c", [] , OpSem_binary (fun ac v1 v2 -> Some (partialNaturalFromInteger ( Nat_big_num.modulus( Nat_big_num.sub( v1) ( v2)) ( ac.ac_all))))); (*0*) +("DW_OP_mod", natural_of_hex "0x1d", [] , OpSem_binary (fun ac v1 v2 -> Some ( Nat_big_num.modulus v1 v2))); (*0*) +("DW_OP_mul", natural_of_hex "0x1e", [] , OpSem_binary (fun ac v1 v2 -> Some (partialNaturalFromInteger ( Nat_big_num.modulus( Nat_big_num.mul( v1) ( v2)) ( ac.ac_all))))); (*0*) +("DW_OP_neg", natural_of_hex "0x1f", [] , OpSem_unary (fun ac v -> if Nat_big_num.less v ac.ac_half then Some ( Nat_big_num.sub_nat ac.ac_max v) else if Nat_big_num.equal v ac.ac_half then None else Some ( Nat_big_num.sub_nat ac.ac_all v))); (*0*) +("DW_OP_not", natural_of_hex "0x20", [] , OpSem_unary (fun ac v -> Some (Nat_big_num.bitwise_xor v ac.ac_max))); (*0*) +("DW_OP_or", natural_of_hex "0x21", [] , OpSem_binary (fun ac v1 v2 -> Some (Nat_big_num.bitwise_or v1 v2))); (*0*) +("DW_OP_plus", natural_of_hex "0x22", [] , OpSem_binary (fun ac v1 v2 -> Some ( Nat_big_num.modulus( Nat_big_num.add v1 v2) ac.ac_all))); (*0*) +("DW_OP_plus_uconst", natural_of_hex "0x23", [OAT_ULEB128] , OpSem_stack (fun ac vs args -> (match args with [OAV_natural n] -> (match vs with v::vs' -> let v' = (Nat_big_num.modulus (Nat_big_num.add v n) ac.ac_all) in Some (v'::vs) | [] -> None ) | _ -> None ))); (*1*) (* ULEB128 addend *) +("DW_OP_shl", natural_of_hex "0x24", [] , OpSem_binary (fun ac v1 v2 -> if Nat_big_num.greater_equal v2 ac.ac_bitwidth then Some(Nat_big_num.of_int 0) else Some (Nat_big_num.shift_left v1 (Nat_big_num.to_int v2)))); (*0*) +("DW_OP_shr", natural_of_hex "0x25", [] , OpSem_binary (fun ac v1 v2 -> if Nat_big_num.greater_equal v2 ac.ac_bitwidth then Some(Nat_big_num.of_int 0) else Some (Nat_big_num.shift_right v1 (Nat_big_num.to_int v2)))); (*0*) +("DW_OP_shra", natural_of_hex "0x26", [] , OpSem_binary (fun ac v1 v2 -> if Nat_big_num.less v1 ac.ac_half then (if Nat_big_num.greater_equal v2 ac.ac_bitwidth then Some(Nat_big_num.of_int 0) else Some (Nat_big_num.shift_right v1 (Nat_big_num.to_int v2))) else (if Nat_big_num.greater_equal v2 ac.ac_bitwidth then Some ac.ac_max else Some ( Nat_big_num.sub_nat ac.ac_max (Nat_big_num.shift_right ( Nat_big_num.sub_nat ac.ac_max v1) (Nat_big_num.to_int v2)))))); (*0*) +("DW_OP_xor", natural_of_hex "0x27", [] , OpSem_binary (fun ac v1 v2 -> Some (Nat_big_num.bitwise_xor v1 v2))); (*0*) +("DW_OP_skip", natural_of_hex "0x2f", [OAT_sint16] , OpSem_not_supported); (*1*) (* signed 2-byte constant *) +("DW_OP_bra", natural_of_hex "0x28", [OAT_sint16] , OpSem_not_supported); (*1*) (* signed 2-byte constant *) +("DW_OP_eq", natural_of_hex "0x29", [] , OpSem_not_supported); (*0*) +("DW_OP_ge", natural_of_hex "0x2a", [] , OpSem_not_supported); (*0*) +("DW_OP_gt", natural_of_hex "0x2b", [] , OpSem_not_supported); (*0*) +("DW_OP_le", natural_of_hex "0x2c", [] , OpSem_not_supported); (*0*) +("DW_OP_lt", natural_of_hex "0x2d", [] , OpSem_not_supported); (*0*) +("DW_OP_ne", natural_of_hex "0x2e", [] , OpSem_not_supported); (*0*) +("DW_OP_lit0", natural_of_hex "0x30", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) (* literals 0..31 =(DW_OP_lit0 + literal) *) +("DW_OP_lit1", natural_of_hex "0x31", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit2", natural_of_hex "0x32", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit3", natural_of_hex "0x33", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit4", natural_of_hex "0x34", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit5", natural_of_hex "0x35", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit6", natural_of_hex "0x36", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit7", natural_of_hex "0x37", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit8", natural_of_hex "0x38", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit9", natural_of_hex "0x39", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit10", natural_of_hex "0x3a", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit11", natural_of_hex "0x3b", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit12", natural_of_hex "0x3c", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit13", natural_of_hex "0x3d", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit14", natural_of_hex "0x3e", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit15", natural_of_hex "0x3f", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit16", natural_of_hex "0x40", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit17", natural_of_hex "0x41", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit18", natural_of_hex "0x42", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit19", natural_of_hex "0x43", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit20", natural_of_hex "0x44", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit21", natural_of_hex "0x45", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit22", natural_of_hex "0x46", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit23", natural_of_hex "0x47", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit24", natural_of_hex "0x48", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit25", natural_of_hex "0x49", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit26", natural_of_hex "0x4a", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit27", natural_of_hex "0x4b", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit28", natural_of_hex "0x4c", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit29", natural_of_hex "0x4d", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit30", natural_of_hex "0x4e", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_lit31", natural_of_hex "0x4f", [] , OpSem_opcode_lit (natural_of_hex "0x30")); (*0*) +("DW_OP_reg0", natural_of_hex "0x50", [] , OpSem_reg); (*1*) (* reg 0..31 = (DW_OP_reg0 + regnum) *) +("DW_OP_reg1", natural_of_hex "0x51", [] , OpSem_reg); (*1*) +("DW_OP_reg2", natural_of_hex "0x52", [] , OpSem_reg); (*1*) +("DW_OP_reg3", natural_of_hex "0x53", [] , OpSem_reg); (*1*) +("DW_OP_reg4", natural_of_hex "0x54", [] , OpSem_reg); (*1*) +("DW_OP_reg5", natural_of_hex "0x55", [] , OpSem_reg); (*1*) +("DW_OP_reg6", natural_of_hex "0x56", [] , OpSem_reg); (*1*) +("DW_OP_reg7", natural_of_hex "0x57", [] , OpSem_reg); (*1*) +("DW_OP_reg8", natural_of_hex "0x58", [] , OpSem_reg); (*1*) +("DW_OP_reg9", natural_of_hex "0x59", [] , OpSem_reg); (*1*) +("DW_OP_reg10", natural_of_hex "0x5a", [] , OpSem_reg); (*1*) +("DW_OP_reg11", natural_of_hex "0x5b", [] , OpSem_reg); (*1*) +("DW_OP_reg12", natural_of_hex "0x5c", [] , OpSem_reg); (*1*) +("DW_OP_reg13", natural_of_hex "0x5d", [] , OpSem_reg); (*1*) +("DW_OP_reg14", natural_of_hex "0x5e", [] , OpSem_reg); (*1*) +("DW_OP_reg15", natural_of_hex "0x5f", [] , OpSem_reg); (*1*) +("DW_OP_reg16", natural_of_hex "0x60", [] , OpSem_reg); (*1*) +("DW_OP_reg17", natural_of_hex "0x61", [] , OpSem_reg); (*1*) +("DW_OP_reg18", natural_of_hex "0x62", [] , OpSem_reg); (*1*) +("DW_OP_reg19", natural_of_hex "0x63", [] , OpSem_reg); (*1*) +("DW_OP_reg20", natural_of_hex "0x64", [] , OpSem_reg); (*1*) +("DW_OP_reg21", natural_of_hex "0x65", [] , OpSem_reg); (*1*) +("DW_OP_reg22", natural_of_hex "0x66", [] , OpSem_reg); (*1*) +("DW_OP_reg23", natural_of_hex "0x67", [] , OpSem_reg); (*1*) +("DW_OP_reg24", natural_of_hex "0x68", [] , OpSem_reg); (*1*) +("DW_OP_reg25", natural_of_hex "0x69", [] , OpSem_reg); (*1*) +("DW_OP_reg26", natural_of_hex "0x6a", [] , OpSem_reg); (*1*) +("DW_OP_reg27", natural_of_hex "0x6b", [] , OpSem_reg); (*1*) +("DW_OP_reg28", natural_of_hex "0x6c", [] , OpSem_reg); (*1*) +("DW_OP_reg29", natural_of_hex "0x6d", [] , OpSem_reg); (*1*) +("DW_OP_reg30", natural_of_hex "0x6e", [] , OpSem_reg); (*1*) +("DW_OP_reg31", natural_of_hex "0x6f", [] , OpSem_reg); (*1*) +("DW_OP_breg0", natural_of_hex "0x70", [OAT_SLEB128] , OpSem_breg); (*1*) (* base register 0..31 = (DW_OP_breg0 + regnum) *) +("DW_OP_breg1", natural_of_hex "0x71", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg2", natural_of_hex "0x72", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg3", natural_of_hex "0x73", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg4", natural_of_hex "0x74", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg5", natural_of_hex "0x75", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg6", natural_of_hex "0x76", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg7", natural_of_hex "0x77", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg8", natural_of_hex "0x78", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg9", natural_of_hex "0x79", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg10", natural_of_hex "0x7a", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg11", natural_of_hex "0x7b", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg12", natural_of_hex "0x7c", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg13", natural_of_hex "0x7d", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg14", natural_of_hex "0x7e", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg15", natural_of_hex "0x7f", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg16", natural_of_hex "0x80", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg17", natural_of_hex "0x81", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg18", natural_of_hex "0x82", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg19", natural_of_hex "0x83", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg20", natural_of_hex "0x84", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg21", natural_of_hex "0x85", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg22", natural_of_hex "0x86", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg23", natural_of_hex "0x87", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg24", natural_of_hex "0x88", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg25", natural_of_hex "0x89", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg26", natural_of_hex "0x8a", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg27", natural_of_hex "0x8b", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg28", natural_of_hex "0x8c", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg29", natural_of_hex "0x8d", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg30", natural_of_hex "0x8e", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg31", natural_of_hex "0x8f", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_regx", natural_of_hex "0x90", [OAT_ULEB128] , OpSem_lit); (*1*) (* ULEB128 register *) +("DW_OP_fbreg", natural_of_hex "0x91", [OAT_SLEB128] , OpSem_fbreg); (*1*) (* SLEB128 offset *) +("DW_OP_bregx", natural_of_hex "0x92", [OAT_ULEB128; OAT_SLEB128] , OpSem_bregx); (*2*) (* ULEB128 register followed by SLEB128 offset *) +("DW_OP_piece", natural_of_hex "0x93", [OAT_ULEB128] , OpSem_piece); (*1*) (* ULEB128 size of piece addressed *) +("DW_OP_deref_size", natural_of_hex "0x94", [OAT_uint8] , OpSem_deref_size); (*1*) (* 1-byte size of data retrieved *) +("DW_OP_xderef_size", natural_of_hex "0x95", [OAT_uint8] , OpSem_not_supported); (*1*) (* 1-byte size of data retrieved *) +("DW_OP_nop", natural_of_hex "0x96", [] , OpSem_nop); (*0*) +("DW_OP_push_object_address", natural_of_hex "0x97", [] , OpSem_not_supported); (*0*) +("DW_OP_call2", natural_of_hex "0x98", [OAT_uint16] , OpSem_not_supported); (*1*) (* 2-byte offset of DIE *) +("DW_OP_call4", natural_of_hex "0x99", [OAT_uint32] , OpSem_not_supported); (*1*) (* 4-byte offset of DIE *) +("DW_OP_call_ref", natural_of_hex "0x9a", [OAT_dwarf_format_t] , OpSem_not_supported); (*1*) (* 4- or 8-byte offset of DIE *) +("DW_OP_form_tls_address", natural_of_hex "0x9b", [] , OpSem_not_supported); (*0*) +("DW_OP_call_frame_cfa", natural_of_hex "0x9c", [] , OpSem_call_frame_cfa); (*0*) +("DW_OP_bit_piece", natural_of_hex "0x9d", [OAT_ULEB128; OAT_ULEB128] , OpSem_bit_piece); (*2*) (* ULEB128 size followed by ULEB128 offset *) +("DW_OP_implicit_value", natural_of_hex "0x9e", [OAT_block] , OpSem_implicit_value); (*2*) (* ULEB128 size followed by block of that size *) +("DW_OP_stack_value", natural_of_hex "0x9f", [] , OpSem_stack_value); (*0*) +(* these aren't real operations +("DW_OP_lo_user", natural_of_hex "0xe0", [] , ); +("DW_OP_hi_user", natural_of_hex "0xff", [] , ); +*) + +(* GCC also produces these for our example: +https://fedorahosted.org/elfutils/wiki/DwarfExtensions +http://dwarfstd.org/ShowIssue.php?issue=100909.1 *) +("DW_GNU_OP_entry_value", natural_of_hex "0xf3", [OAT_block], OpSem_not_supported); (*2*) (* ULEB128 size followed by DWARF expression block of that size*) +("DW_OP_GNU_implicit_pointer", natural_of_hex "0xf2", [OAT_dwarf_format_t;OAT_SLEB128], OpSem_not_supported) + +]) + + +let vDW_OP_reg0:Nat_big_num.num= (natural_of_hex "0x50") +let vDW_OP_breg0:Nat_big_num.num= (natural_of_hex "0x70") + + +(* call frame instruction encoding *) + +let call_frame_instruction_encoding : (string * Nat_big_num.num * Nat_big_num.num * call_frame_argument_type list * (( call_frame_argument_value list) -> call_frame_instruction option)) list= ([ +(* high-order 2 bits low-order 6 bits uniformly parsed arguments *) + +(* instructions using low-order 6 bits for first argument *) +(* +("DW_CFA_advance_loc", 1, 0,(*delta *) []); +("DW_CFA_offset", 2, 0,(*register*) [CFAT_offset]); +("DW_CFA_restore", 3, 0,(*register*) []); +*) +(* instructions using low-order 6 bits as part of opcode *) +("DW_CFA_nop",Nat_big_num.of_int 0, natural_of_hex "0x00", [], +( (* *)fun avs -> (match avs with [] -> Some (DW_CFA_nop) | _ -> None ))); +("DW_CFA_set_loc",Nat_big_num.of_int 0, natural_of_hex "0x01", [CFAT_address], +( (* address *)fun avs -> (match avs with [CFAV_address a] -> Some (DW_CFA_set_loc a) | _ -> None ))); +("DW_CFA_advance_loc1",Nat_big_num.of_int 0, natural_of_hex "0x02", [CFAT_delta1], +( (* 1-byte delta *)fun avs -> (match avs with [CFAV_delta d] -> Some (DW_CFA_advance_loc1 d) | _ -> None ))); +("DW_CFA_advance_loc2",Nat_big_num.of_int 0, natural_of_hex "0x03", [CFAT_delta2], +( (* 2-byte delta *)fun avs -> (match avs with [CFAV_delta d] -> Some (DW_CFA_advance_loc2 d) | _ -> None ))); +("DW_CFA_advance_loc4",Nat_big_num.of_int 0, natural_of_hex "0x04", [CFAT_delta4], +( (* 4-byte delta *)fun avs -> (match avs with [CFAV_delta d] -> Some (DW_CFA_advance_loc4 d) | _ -> None ))); +("DW_CFA_offset_extended",Nat_big_num.of_int 0, natural_of_hex "0x05", [CFAT_register; CFAT_offset], +( (* ULEB128 register ULEB128 offset *)fun avs -> (match avs with [CFAV_register r; CFAV_offset n] -> Some (DW_CFA_offset_extended( r, n)) | _ -> None ))); +("DW_CFA_restore_extended",Nat_big_num.of_int 0, natural_of_hex "0x06", [CFAT_register], +( (* ULEB128 register *)fun avs -> (match avs with [CFAV_register r] -> Some (DW_CFA_restore_extended r) | _ -> None ))); +("DW_CFA_undefined",Nat_big_num.of_int 0, natural_of_hex "0x07", [CFAT_register], +( (* ULEB128 register *)fun avs -> (match avs with [CFAV_register r] -> Some (DW_CFA_undefined r) | _ -> None ))); +("DW_CFA_same_value",Nat_big_num.of_int 0, natural_of_hex "0x08", [CFAT_register], +( (* ULEB128 register *)fun avs -> (match avs with [CFAV_register r] -> Some (DW_CFA_same_value r) | _ -> None ))); +("DW_CFA_register",Nat_big_num.of_int 0, natural_of_hex "0x09", [CFAT_register; CFAT_register], +( (* ULEB128 register ULEB128 register *)fun avs -> (match avs with [CFAV_register r1; CFAV_register r2] -> Some (DW_CFA_register( r1, r2)) | _ -> None ))); +("DW_CFA_remember_state",Nat_big_num.of_int 0, natural_of_hex "0x0a", [], +( (* *)fun avs -> (match avs with [] -> Some (DW_CFA_remember_state) | _ -> None ))); +("DW_CFA_restore_state",Nat_big_num.of_int 0, natural_of_hex "0x0b", [], +( (* *)fun avs -> (match avs with [] -> Some (DW_CFA_restore_state) | _ -> None ))); +("DW_CFA_def_cfa",Nat_big_num.of_int 0, natural_of_hex "0x0c", [CFAT_register; CFAT_offset], +( (* ULEB128 register ULEB128 offset *)fun avs -> (match avs with [CFAV_register r; CFAV_offset n] -> Some (DW_CFA_def_cfa( r, n)) | _ -> None ))); +("DW_CFA_def_cfa_register",Nat_big_num.of_int 0, natural_of_hex "0x0d", [CFAT_register], +( (* ULEB128 register *)fun avs -> (match avs with [CFAV_register r] -> Some (DW_CFA_def_cfa_register r) | _ -> None ))); +("DW_CFA_def_cfa_offset",Nat_big_num.of_int 0, natural_of_hex "0x0e", [CFAT_offset], +( (* ULEB128 offset *)fun avs -> (match avs with [CFAV_offset n] -> Some (DW_CFA_def_cfa_offset n) | _ -> None ))); +("DW_CFA_def_cfa_expression",Nat_big_num.of_int 0, natural_of_hex "0x0f", [CFAT_block], +( (* BLOCK *)fun avs -> (match avs with [CFAV_block b] -> Some (DW_CFA_def_cfa_expression b) | _ -> None ))); +("DW_CFA_expression",Nat_big_num.of_int 0, natural_of_hex "0x10", [CFAT_register; CFAT_block], +( (* ULEB128 register BLOCK *)fun avs -> (match avs with [CFAV_register r; CFAV_block b] -> Some (DW_CFA_expression( r, b)) | _ -> None ))); +("DW_CFA_offset_extended_sf",Nat_big_num.of_int 0, natural_of_hex "0x11", [CFAT_register; CFAT_sfoffset], +( (* ULEB128 register SLEB128 offset *)fun avs -> (match avs with [CFAV_register r; CFAV_sfoffset i] -> Some (DW_CFA_offset_extended_sf( r, i)) | _ -> None ))); +("DW_CFA_def_cfa_sf",Nat_big_num.of_int 0, natural_of_hex "0x12", [CFAT_register; CFAT_sfoffset], +( (* ULEB128 register SLEB128 offset *)fun avs -> (match avs with [CFAV_register r; CFAV_sfoffset i] -> Some (DW_CFA_def_cfa_sf( r, i)) | _ -> None ))); +("DW_CFA_def_cfa_offset_sf",Nat_big_num.of_int 0, natural_of_hex "0x13", [CFAT_sfoffset], +( (* SLEB128 offset *)fun avs -> (match avs with [CFAV_sfoffset i] -> Some (DW_CFA_def_cfa_offset_sf i) | _ -> None ))); +("DW_CFA_val_offset",Nat_big_num.of_int 0, natural_of_hex "0x14", [CFAT_register; CFAT_offset], +( (* ULEB128 ULEB128 *)fun avs -> (match avs with [CFAV_register r; CFAV_offset n] -> Some (DW_CFA_val_offset( r, n)) | _ -> None ))); +("DW_CFA_val_offset_sf",Nat_big_num.of_int 0, natural_of_hex "0x15", [CFAT_register; CFAT_sfoffset], +( (* ULEB128 SLEB128 *)fun avs -> (match avs with [CFAV_register r; CFAV_sfoffset i] -> Some (DW_CFA_val_offset_sf( r, i)) | _ -> None ))); +("DW_CFA_val_expression",Nat_big_num.of_int 0, natural_of_hex "0x16", [CFAT_register; CFAT_block], +( (* ULEB128 BLOCK *)fun avs -> (match avs with [CFAV_register r; CFAV_block b] -> Some (DW_CFA_val_expression( r, b)) | _ -> None ))) +]) + +(* +("DW_CFA_lo_user", 0, natural_of_hex "0x1c", []); (* *) +("DW_CFA_hi_user", 0, natural_of_hex "0x3f", []); (* *) +*) + + +(* line number encodings *) + +let line_number_standard_encodings:(string*Nat_big_num.num*(line_number_argument_type)list*((line_number_argument_value)list ->(line_number_operation)option))list= ([ + ("DW_LNS_copy" , natural_of_hex "0x01", [ ], + (fun lnvs -> (match lnvs with [] -> Some DW_LNS_copy | _ -> None ))); + ("DW_LNS_advance_pc" , natural_of_hex "0x02", [LNAT_ULEB128 ], + (fun lnvs -> (match lnvs with [LNAV_ULEB128 n] -> Some (DW_LNS_advance_pc n) | _ -> None ))); + ("DW_LNS_advance_line" , natural_of_hex "0x03", [LNAT_SLEB128 ], + (fun lnvs -> (match lnvs with [LNAV_SLEB128 i] -> Some (DW_LNS_advance_line i) | _ -> None ))); + ("DW_LNS_set_file" , natural_of_hex "0x04", [LNAT_ULEB128 ], + (fun lnvs -> (match lnvs with [LNAV_ULEB128 n] -> Some (DW_LNS_set_file n) | _ -> None ))); + ("DW_LNS_set_column" , natural_of_hex "0x05", [LNAT_ULEB128 ], + (fun lnvs -> (match lnvs with [LNAV_ULEB128 n] -> Some (DW_LNS_set_column n) | _ -> None ))); + ("DW_LNS_negate_stmt" , natural_of_hex "0x06", [ ], + (fun lnvs -> (match lnvs with [] -> Some (DW_LNS_negate_stmt) | _ -> None ))); + ("DW_LNS_set_basic_block" , natural_of_hex "0x07", [ ], + (fun lnvs -> (match lnvs with [] -> Some (DW_LNS_set_basic_block) | _ -> None ))); + ("DW_LNS_const_add_pc" , natural_of_hex "0x08", [ ], + (fun lnvs -> (match lnvs with [] -> Some (DW_LNS_const_add_pc) | _ -> None ))); + ("DW_LNS_fixed_advance_pc" , natural_of_hex "0x09", [LNAT_uint16 ], + (fun lnvs -> (match lnvs with [LNAV_uint16 n] -> Some (DW_LNS_fixed_advance_pc n) | _ -> None ))); + ("DW_LNS_set_prologue_end" , natural_of_hex "0x0a", [ ], +(fun lnvs -> (match lnvs with [] -> Some (DW_LNS_set_prologue_end) | _ -> None ))); + ("DW_LNS_set_epilogue_begin" , natural_of_hex "0x0b", [ ], +(fun lnvs -> (match lnvs with [] -> Some (DW_LNS_set_epilogue_begin) | _ -> None ))); + ("DW_LNS_set_isa" , natural_of_hex "0x0c", [LNAT_ULEB128 ], + (fun lnvs -> (match lnvs with [LNAV_ULEB128 n] -> Some (DW_LNS_set_isa n) | _ -> None ))) +]) + +let line_number_extended_encodings:(string*Nat_big_num.num*(line_number_argument_type)list*((line_number_argument_value)list ->(line_number_operation)option))list= ([ + ("DW_LNE_end_sequence" , natural_of_hex "0x01", [], + (fun lnvs -> (match lnvs with [] -> Some (DW_LNE_end_sequence) | _ -> None ))); + ("DW_LNE_set_address" , natural_of_hex "0x02", [LNAT_address], + (fun lnvs -> (match lnvs with [LNAV_address n] -> Some (DW_LNE_set_address n) | _ -> None ))); + ("DW_LNE_define_file" , natural_of_hex "0x03", [LNAT_string; LNAT_ULEB128; LNAT_ULEB128; LNAT_ULEB128], + (fun lnvs -> (match lnvs with [LNAV_string s; LNAV_ULEB128 n1; LNAV_ULEB128 n2; LNAV_ULEB128 n3] -> Some (DW_LNE_define_file( s, n1, n2, n3)) | _ -> None ))); + ("DW_LNE_set_discriminator" , natural_of_hex "0x04", [LNAT_ULEB128], + (fun lnvs -> (match lnvs with [LNAV_ULEB128 n] -> Some (DW_LNE_set_discriminator n) | _ -> None ))) (* new in Dwarf 4*) +]) + + +(* +(DW_LNE_lo_user , natural_of_hex "0x80", "DW_LNE_lo_user"); +(DW_LNE_hi_user , natural_of_hex "0xff", "DW_LNE_hi_user"); +*) + + + +(* booleans encoded as a single byte containing the value 0 for âfalse,â and a non-zero value for âtrue.â *) + + +(** ************************************************************ *) +(** ** more missing pervasives and bits *********************** *) +(** ************************************************************ *) + + +(* quick hacky workaround: this is in String.lem, in src_lem_library, but the linker doesn't find it *) +(*val myconcat : string -> list string -> string*) +let rec myconcat sep ss:string= + ((match ss with + | [] -> "" + | s :: ss' -> + (match ss' with + | [] -> s + | _ -> s ^ (sep ^ myconcat sep ss') + ) + )) + +(*val myhead : forall 'a. list 'a -> 'a*) +let myhead l:'a= ((match l with | x::xs -> x | [] -> failwith "myhead of empty list" )) + + +(*val myfindNonPure : forall 'a. ('a -> bool) -> list 'a -> 'a*) +let myfindNonPure p0 l:'a= ((match (Lem_list.list_find_opt p0 l) with + | Some e -> e + | None -> failwith "myfindNonPure" +)) + +(*val myfindmaybe : forall 'a 'b. ('a -> maybe 'b) -> list 'a -> maybe 'b*) +let rec myfindmaybe f xs:'b option= + ((match xs with + | [] -> None + | x::xs' -> (match f x with Some y -> Some y | None -> myfindmaybe f xs' ) + )) + +(*val myfind : forall 'a. ('a -> bool) -> list 'a -> maybe 'a*) +let rec myfind f xs:'a option= + ((match xs with + | [] -> None + | x::xs' -> (match f x with true -> Some x | false -> myfind f xs' ) + )) + +(*val myfiltermaybe : forall 'a 'b. ('a -> maybe 'b) -> list 'a -> list 'b*) +let rec myfiltermaybe f xs:'b list= + ((match xs with + | [] -> [] + | x::xs' -> (match f x with Some y -> y::myfiltermaybe f xs'| None -> myfiltermaybe f xs' ) + )) + + + +(*val bytes_of_natural: endianness -> natural (*size*) -> natural (*value*) -> list byte*) +let bytes_of_natural en size2 n:(char)list= + (if Nat_big_num.equal size2(Nat_big_num.of_int 8) then + bytes_of_elf64_xword en (Uint64.of_string (Nat_big_num.to_string n)) + else if Nat_big_num.equal size2(Nat_big_num.of_int 4) then + bytes_of_elf32_word en (Uint32.of_string (Nat_big_num.to_string n)) + else + failwith "bytes_of_natural given size that is not 4 or 8") + +(* TODO: generalise *) +(*val natural_of_bytes: endianness -> list byte -> natural*) +let natural_of_bytes en bs:Nat_big_num.num= + ((match bs with + | b0::b1::b2::b3::b4::b5::b6::b7::[] -> + let v = (if en=Little then + Nat_big_num.add (Nat_big_num.add (Nat_big_num.add (Nat_big_num.add + (natural_of_byte b0)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b3))) (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))( Nat_big_num.add (Nat_big_num.add (Nat_big_num.add(natural_of_byte b4)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b5)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b6)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b7)))) + else + Nat_big_num.add (Nat_big_num.add (Nat_big_num.add (Nat_big_num.add +(natural_of_byte b7)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b6)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b5)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b4))) (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))( Nat_big_num.add (Nat_big_num.add (Nat_big_num.add(natural_of_byte b3)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b0))))) + in + v + | b0::b1::b2::b3::[] -> + let v = (if en=Little then Nat_big_num.add (Nat_big_num.add (Nat_big_num.add + (natural_of_byte b0)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b3)) + else Nat_big_num.add (Nat_big_num.add (Nat_big_num.add +(natural_of_byte b3)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b0))) + + in + v + | b0::b1::[] -> + let v = (if en=Little then Nat_big_num.add + (natural_of_byte b0)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b1)) + else Nat_big_num.add +(natural_of_byte b1)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b0))) + + in + v + | b0::[] -> + natural_of_byte b0 + | _ -> failwith "natural_of_bytes given not-8/4/2/1 bytes" + )) + + +(*val bigunionListMap : forall 'a 'b. SetType 'b => ('a -> set 'b) -> list 'a -> set 'b*) +let rec bigunionListMap dict_Basic_classes_SetType_b f xs:'b Pset.set= + ((match xs with + | [] ->(Pset.from_list + dict_Basic_classes_SetType_b.setElemCompare_method []) + | x::xs' -> Pset.(union) (f x) (bigunionListMap + dict_Basic_classes_SetType_b f xs') + )) + +let rec mytake' (n:Nat_big_num.num) acc xs:('a list*'a list)option= + ( + if(Nat_big_num.equal n (Nat_big_num.of_int 0)) then + (Some (List.rev acc, xs)) else + ((match xs with + [] -> None + | x::xs' -> mytake' (Nat_big_num.sub_nat n (Nat_big_num.of_int 1)) + (x :: acc) xs' + ))) + +(*val mytake : forall 'a. natural -> (list 'a) -> maybe (list 'a * list 'a)*) +let mytake n xs:('a list*'a list)option= (mytake' n [] xs) + +(*val mynth : forall 'a. natural -> (list 'a) -> maybe 'a*) +let rec mynth (n:Nat_big_num.num) xs:'a option= + ( (*Assert_extra.failwith "mynth"*) + if(Nat_big_num.equal n (Nat_big_num.of_int 0)) then + ((match xs with x::xs' -> Some x | [] -> None )) else + ((match xs with + x::xs' -> mynth (Nat_big_num.sub_nat n (Nat_big_num.of_int 1)) xs' + ))) + + +(** basic pretty printing *) + +let pphex n:string= ("0x" ^ unsafe_hex_string_of_natural( 0) n) + +let ppbytes dict_Show_Show_a xs:string= (string_of_list + instance_Show_Show_string_dict (Lem_list.map (fun x -> + dict_Show_Show_a.show_method x) xs)) + +let rec ppbytes2 dict_Show_Show_a n xs:string= ((match xs with | [] -> "" | x::xs' -> "<"^(pphex n^("> "^( + dict_Show_Show_a.show_method x^("\n"^ppbytes2 dict_Show_Show_a (Nat_big_num.add n(Nat_big_num.of_int 1)) xs')))) )) + +(* workaround: from String *) +(*val mytoString : list char -> string*) + +let string_of_bytes bs:string= (Xstring.implode (Lem_list.map (fun x-> x) bs)) + + +let just_one s xs:'a= + ((match xs with + | [] -> failwith ("no " ^ s) + | x1::x2::_ -> failwith ("more than one " ^ s) + | [x] -> x + )) + + + + +let max_address (as': Nat_big_num.num) : Nat_big_num.num= + ( + if(Nat_big_num.equal as' (Nat_big_num.of_int 4)) then + (natural_of_hex "0xffffffff") else + ( + if(Nat_big_num.equal as' (Nat_big_num.of_int 8)) then + (natural_of_hex "0xffffffffffffffff") else + (failwith "max_address size not 4 or 8"))) + + +(** lookup of encodings *) + +(*val lookup_Ab_b : forall 'a 'b. Eq 'a => 'a -> list ('a * 'b) -> maybe 'b*) +let rec lookup_Ab_b dict_Basic_classes_Eq_a x0 xys:'b option= + ((match xys with + | [] -> None + | (x,y)::xys' -> if + dict_Basic_classes_Eq_a.isEqual_method x x0 then Some y else lookup_Ab_b + dict_Basic_classes_Eq_a x0 xys' + )) + +(*val lookup_aB_a : forall 'a 'b. Eq 'b => 'b -> list ('a * 'b) -> maybe 'a*) +let rec lookup_aB_a dict_Basic_classes_Eq_b y0 xys:'a option= + ((match xys with + | [] -> None + | (x,y)::xys' -> if + dict_Basic_classes_Eq_b.isEqual_method y y0 then Some x else lookup_aB_a + dict_Basic_classes_Eq_b y0 xys' + )) + + +(*val lookup_aBc_a : forall 'a 'b 'c. Eq 'b => 'b -> list ('a * 'b * 'c) -> maybe 'a*) +let rec lookup_aBc_a dict_Basic_classes_Eq_b y0 xyzs:'a option= + ((match xyzs with + | [] -> None + | (x,y,_)::xyzs' -> if + dict_Basic_classes_Eq_b.isEqual_method y y0 then Some x else lookup_aBc_a + dict_Basic_classes_Eq_b y0 xyzs' + )) + +(*val lookup_aBc_ac : forall 'a 'b 'c. Eq 'b => 'b -> list ('a * 'b * 'c) -> maybe ('a*'c)*) +let rec lookup_aBc_ac dict_Basic_classes_Eq_b y0 xyzs:('a*'c)option= + ((match xyzs with + | [] -> None + | (x,y,z)::xyzs' -> if + dict_Basic_classes_Eq_b.isEqual_method y y0 then Some (x,z) else lookup_aBc_ac + dict_Basic_classes_Eq_b y0 xyzs' + )) + +(*val lookup_Abc_b : forall 'a 'b 'c. Eq 'a => 'a -> list ('a * 'b * 'c) -> maybe 'b*) +let rec lookup_Abc_b dict_Basic_classes_Eq_a x0 xyzs:'b option= + ((match xyzs with + | [] -> None + | (x,y,_)::xyzs' -> if + dict_Basic_classes_Eq_a.isEqual_method x x0 then Some y else lookup_Abc_b + dict_Basic_classes_Eq_a x0 xyzs' + )) + + + +(*val lookup_aBcd_a : forall 'a 'b 'c 'd. Eq 'b => 'b -> list ('a * 'b * 'c * 'd) -> maybe 'a*) +let rec lookup_aBcd_a dict_Basic_classes_Eq_b y0 xyzws:'a option= + ((match xyzws with + | [] -> None + | (x,y,_,_)::xyzws' -> if + dict_Basic_classes_Eq_b.isEqual_method y y0 then Some x else lookup_aBcd_a + dict_Basic_classes_Eq_b y0 xyzws' + )) + +(*val lookup_aBcd_acd : forall 'a 'b 'c 'd. Eq 'b => 'b -> list ('a * 'b * 'c * 'd) -> maybe ('a * 'c * 'd)*) +let rec lookup_aBcd_acd dict_Basic_classes_Eq_b y0 xyzws:('a*'c*'d)option= + ((match xyzws with + | [] -> None + | (x,y,z,w)::xyzws' -> if + dict_Basic_classes_Eq_b.isEqual_method y y0 then Some (x,z,w) else lookup_aBcd_acd + dict_Basic_classes_Eq_b y0 xyzws' + )) + +(*val lookup_abCde_de : forall 'a 'b 'c 'd 'e. Eq 'c => 'c -> list ('a * 'b * 'c * 'd * 'e) -> maybe ('d * 'e)*) +let rec lookup_abCde_de dict_Basic_classes_Eq_c z0 xyzwus:('d*'e)option= + ((match xyzwus with + | [] -> None + | (x,y,z,w,u)::xyzwus' -> if + dict_Basic_classes_Eq_c.isEqual_method z z0 then Some (w,u) else lookup_abCde_de + dict_Basic_classes_Eq_c z0 xyzwus' + )) + + +let pp_maybe ppf n:string= ((match ppf n with Some s -> s | None -> "encoding not found: " ^ pphex n )) + +let pp_tag_encoding n:string= (pp_maybe (fun n -> lookup_aB_a + instance_Basic_classes_Eq_Num_natural_dict n tag_encodings) n) +let pp_attribute_encoding n:string= (pp_maybe (fun n -> lookup_aBc_a + instance_Basic_classes_Eq_Num_natural_dict n attribute_encodings) n) +let pp_attribute_form_encoding n:string= (pp_maybe (fun n -> lookup_aBc_a + instance_Basic_classes_Eq_Num_natural_dict n attribute_form_encodings) n) +let pp_operation_encoding n:string= (pp_maybe (fun n -> lookup_aBcd_a + instance_Basic_classes_Eq_Num_natural_dict n operation_encodings) n) + +let tag_encode (s: string) : Nat_big_num.num= + ((match lookup_Ab_b + instance_Basic_classes_Eq_string_dict s tag_encodings with + | Some n -> n + | None -> failwith "attribute_encode" + )) + + +let attribute_encode (s: string) : Nat_big_num.num= + ((match lookup_Abc_b + instance_Basic_classes_Eq_string_dict s attribute_encodings with + | Some n -> n + | None -> failwith "attribute_encode" + )) + +let attribute_form_encode (s: string) : Nat_big_num.num= + ((match lookup_Abc_b + instance_Basic_classes_Eq_string_dict s attribute_form_encodings with + | Some n -> n + | None -> failwith "attribute_form_encode" + )) + + + +(** ************************************************************ *) +(** ** parser combinators and primitives ********************* *) +(** ************************************************************ *) + +(* parsing combinators *) + +type parse_context = { pc_bytes: char list; pc_offset: Nat_big_num.num } + +type 'a parse_result = + | PR_success of 'a * parse_context + | PR_fail of string * parse_context + +type 'a parser = parse_context -> 'a parse_result + +let pp_parse_context pc:string= ("pc_offset = " ^ pphex pc.pc_offset) + +let pp_parse_fail s pc:string= + ("Parse fail\n" ^ (s ^ (" at " ^ (pp_parse_context pc ^ "\n")))) + +let pp_parse_result ppa pr:string= + ((match pr with + | PR_success( x, pc) -> "Parse success\n" ^ (ppa x ^ ("\n" ^ (pp_parse_context pc ^ "\n"))) + | PR_fail( s, pc) -> pp_parse_fail s pc + )) + +(* [(>>=)] should be the monadic binding function for [parse_result]. *) +(* but there's a type clash if we use >>=, and lem seems to output bad ocaml for >>>=. So we just use a non-infix version for now *) + +(*val pr_bind : forall 'a 'b. parse_result 'a -> ('a -> parser 'b) -> parse_result 'b*) +let pr_bind x f:'b parse_result= + ((match x with + | PR_success( v, pc) -> f v pc + | PR_fail( err, pc) -> PR_fail( err, pc) + )) + +(*val pr_return : forall 'a. 'a -> (parser 'a)*) +let pr_return x pc:'a parse_result= (PR_success( x, pc)) + +(*val pr_map : forall 'a 'b. ('a -> 'b) -> parse_result 'a -> parse_result 'b*) +let pr_map f x:'b parse_result= + ((match x with + | PR_success( v, pc) -> PR_success( (f v), pc) + | PR_fail( err, pc) -> PR_fail( err, pc) + )) + +(*val pr_map2 : forall 'a 'b. ('a -> 'b) -> (parser 'a) -> (parser 'b)*) +let pr_map2 f p:parse_context ->'b parse_result= (fun pc -> pr_map f (p pc)) + +(*val pr_post_map1 : forall 'a 'b. (parse_result 'a) -> ('a -> 'b) -> (parse_result 'b)*) +let pr_post_map1 x f:'b parse_result= (pr_map f x) + +(* +val pr_post_map : forall 'a 'b 'c. ('c -> parse_result 'a) -> ('a -> 'b) -> ('c -> parse_result 'b) +let pr_post_map g f = fun x -> pr_map f (g x) +*) +(*val pr_post_map : forall 'a 'b. (parser 'a) -> ('a -> 'b) -> (parser 'b)*) +let pr_post_map p f:parse_context ->'b parse_result= (fun (pc: parse_context) -> pr_map f (p pc)) + + +(*val pr_with_pos : forall 'a. (parser 'a) -> (parser (natural * 'a))*) +let pr_with_pos p:parse_context ->(Nat_big_num.num*'a)parse_result= (fun pc -> pr_map (fun x -> (pc.pc_offset,x)) (p pc)) + + +(*val parse_pair : forall 'a 'b. (parser 'a) -> (parser 'b) -> (parser ('a * 'b))*) +let parse_pair p1 p2:parse_context ->('a*'b)parse_result= + (fun pc -> + let _ = (my_debug "pair ") in + pr_bind (p1 pc) (fun x pc' -> (match p2 pc' with + | PR_success( y, pc'') -> PR_success( (x,y), pc'') + | PR_fail( s, pc'') -> PR_fail( s, pc'') + ))) + +(*val parse_triple : forall 'a 'b 'c. (parser 'a) -> (parser 'b) -> (parser 'c) -> parser ('a * ('b * 'c))*) +let parse_triple p1 p2 p3:parse_context ->('a*('b*'c))parse_result= + (parse_pair p1 (parse_pair p2 p3)) + +(*val parse_quadruple : forall 'a 'b 'c 'd. (parser 'a) -> (parser 'b) -> (parser 'c) -> (parser 'd) -> parser ('a * ('b * ('c * 'd)))*) +let parse_quadruple p1 p2 p3 p4:parse_context ->('a*('b*('c*'d)))parse_result= + (parse_pair p1 (parse_pair p2 (parse_pair p3 p4))) + +(*val parse_pentuple : forall 'a 'b 'c 'd 'e. (parser 'a) -> (parser 'b) -> (parser 'c) -> (parser 'd) -> (parser 'e) -> parser ('a * ('b * ('c * ('d * 'e))))*) +let parse_pentuple p1 p2 p3 p4 p5:parse_context ->('a*('b*('c*('d*'e))))parse_result= + (parse_pair p1 (parse_pair p2 (parse_pair p3 (parse_pair p4 p5)))) + +(*val parse_sextuple : forall 'a 'b 'c 'd 'e 'f. (parser 'a) -> (parser 'b) -> (parser 'c) -> (parser 'd) -> (parser 'e) -> (parser 'f) -> parser ('a * ('b * ('c * ('d * ('e * 'f)))))*) +let parse_sextuple p1 p2 p3 p4 p5 p6:parse_context ->('a*('b*('c*('d*('e*'f)))))parse_result= + (parse_pair p1 (parse_pair p2 (parse_pair p3 (parse_pair p4 (parse_pair p5 p6))))) + +(*val parse_dependent_pair : forall 'a 'b. (parser 'a) -> ('a -> parser 'b) -> (parser ('a * 'b))*) +let parse_dependent_pair p1 p2:parse_context ->('a*'b)parse_result= + (fun pc -> + pr_bind (p1 pc) (fun x pc' -> (match p2 x pc' with + | PR_success( y, pc'') -> PR_success( (x,y), pc'') + | PR_fail( s, pc'') -> PR_fail( s, pc'') + ))) + +(*val parse_dependent : forall 'a 'b. (parser 'a) -> ('a -> parser 'b) -> (parser 'b)*) +let parse_dependent p1 p2:parse_context ->'b parse_result= + (fun pc -> + pr_bind (p1 pc) (fun x pc' -> p2 x pc')) + + + +(*val parse_list' : forall 'a. (parser (maybe 'a)) -> (list 'a -> parser (list 'a))*) +let rec parse_list' p1:'a list ->parse_context ->('a list)parse_result= + (fun acc pc -> let _ = (my_debug "list' ") in pr_bind (p1 pc) (fun mx pc' -> + (match mx with + | None -> PR_success( acc, pc') + | Some x -> parse_list' p1 (x :: acc) pc' + ))) + +(*val parse_list : forall 'a. (parser (maybe 'a)) -> (parser (list 'a))*) +let parse_list p1:parse_context ->('a list)parse_result= + (pr_post_map + (parse_list' p1 []) + (List.rev)) + +(*val parse_parser_list : forall 'a. (list (parser 'a)) -> (parser (list 'a))*) +let rec parse_parser_list ps:parse_context ->('a list)parse_result= + ((match ps with + | [] -> pr_return [] + | p::ps' -> + (fun pc -> pr_bind (p pc) (fun x pc' -> + (match parse_parser_list ps' pc' with + | PR_success( xs, pc'') -> PR_success( (x::xs), pc'') + | PR_fail( s, pc'') -> PR_fail( s, pc'') + ))) + )) + +(*val parse_maybe : forall 'a. parser 'a -> parser (maybe 'a)*) +let parse_maybe p:parse_context ->('a option)parse_result= + (fun pc -> + (match pc.pc_bytes with + | [] -> pr_return None pc + | _ -> + (match p pc with + | PR_success( v, pc'') -> PR_success( (Some v), pc'') + | PR_fail( s, pc'') -> PR_fail( s, pc'') + ) + )) + +(*val parse_demaybe : forall 'a. string ->parser (maybe 'a) -> parser 'a*) +let parse_demaybe s p:parse_context ->'a parse_result= + (fun pc -> + (match p pc with + | PR_success( (Some v), pc'') -> PR_success( v, pc'') + | PR_success( (None), pc'') -> PR_fail( s, pc'') + | PR_fail( s, pc'') -> PR_fail( s, pc'') + + )) + + +(*val parse_restrict_length : forall 'a. natural -> parser 'a -> parser 'a*) +let parse_restrict_length n p:parse_context ->'a parse_result= + (fun pc -> + (match mytake n pc.pc_bytes with + | None -> failwith "parse_restrict_length not given enough bytes" + | Some (xs,ys) -> + let pc' = ({ pc_bytes = xs; pc_offset = (pc.pc_offset) }) in + p pc' + )) + + +(* parsing of basic types *) + + +let parse_n_bytes (n:Nat_big_num.num) : ( char list) parser= + (fun (pc:parse_context) -> + (match mytake n pc.pc_bytes with + | None -> PR_fail( ("parse_n_bytes n=" ^ pphex n), pc) + | Some (xs,bs) -> PR_success( xs, ({pc_bytes=bs; pc_offset= (Nat_big_num.add pc.pc_offset (Nat_big_num.of_int (List.length xs))) } )) + )) + +let rec mytakestring' acc xs:((char)list*(char)list)option= + ((match xs with + | [] -> None + | x::xs' -> if Nat_big_num.equal (natural_of_byte x)(Nat_big_num.of_int 0) then Some (List.rev acc, xs') else mytakestring' (x::acc) xs' + )) + +let parse_string : ( char list) parser= + (fun (pc:parse_context) -> + (match mytakestring' [] pc.pc_bytes with + | None -> PR_fail( "parse_string", pc) + | Some (xs,bs) -> PR_success( xs, ({pc_bytes=bs; pc_offset = (Nat_big_num.add (Nat_big_num.add pc.pc_offset (Nat_big_num.of_int (List.length xs))) (Nat_big_num.of_int( 1))) } )) + )) + +(* parse a null-terminated string; return Nothing if it is empty, Just s otherwise *) +let parse_non_empty_string : ( ( char list)option) parser= + (fun (pc:parse_context) -> + (match mytakestring' [] pc.pc_bytes with + | None -> PR_fail( "parse_string", pc) + | Some (xs,bs) -> + (*let _ = my_debug5 ("**" ^string_of_bytes xs ^ "**\n") in *) + let pc' = ({pc_bytes=bs; pc_offset = (Nat_big_num.add (Nat_big_num.add pc.pc_offset (Nat_big_num.of_int (List.length xs))) (Nat_big_num.of_int( 1))) } ) in + if (listEqualBy (=) xs []) then PR_success( (None), pc') + else PR_success( (Some xs), pc') + )) + + +let parse_uint8 : Nat_big_num.num parser= + (fun (pc:parse_context) -> + let _ = (my_debug "uint8 ") in + (match pc.pc_bytes with + | b0::bytes' -> + let v = (natural_of_byte b0) in + PR_success( v, ({ pc_bytes = bytes'; pc_offset = (Nat_big_num.add pc.pc_offset(Nat_big_num.of_int 1)) })) + | _ -> PR_fail( "parse_uint32 not given enough bytes", pc) + )) + +let parse_uint16 c : Nat_big_num.num parser= + (fun (pc:parse_context) -> + let _ = (my_debug "uint16 ") in + (match pc.pc_bytes with + | b0::b1::bytes' -> + let v = (if c.endianness=Little then Nat_big_num.add + (natural_of_byte b0)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b1)) + else Nat_big_num.add + (natural_of_byte b1)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b0))) in + PR_success( v, ({ pc_bytes = bytes'; pc_offset = (Nat_big_num.add pc.pc_offset(Nat_big_num.of_int 2)) })) + | _ -> PR_fail( "parse_uint32 not given enough bytes", pc) + )) + +let parse_uint32 c : Nat_big_num.num parser= + (fun (pc:parse_context) -> + let _ = (my_debug "uint32 ") in + (match pc.pc_bytes with + | b0::b1::b2::b3::bytes' -> + let v = (if c.endianness=Little then Nat_big_num.add (Nat_big_num.add (Nat_big_num.add + (natural_of_byte b0)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b3)) + else Nat_big_num.add (Nat_big_num.add (Nat_big_num.add + (natural_of_byte b3)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b0))) in + PR_success( v, ({ pc_bytes = bytes'; pc_offset = (Nat_big_num.add pc.pc_offset(Nat_big_num.of_int 4)) })) + | _ -> PR_fail( "parse_uint32 not given enough bytes", pc) + )) + +let parse_uint64 c : Nat_big_num.num parser= + (fun (pc:parse_context) -> + let _ = (my_debug "uint64 ") in + (match pc.pc_bytes with + | b0::b1::b2::b3::b4::b5::b6::b7::bytes' -> + let v = (if c.endianness=Little then + Nat_big_num.add (Nat_big_num.add (Nat_big_num.add (Nat_big_num.add + (natural_of_byte b0)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b3))) (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))( Nat_big_num.add (Nat_big_num.add (Nat_big_num.add(natural_of_byte b4)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b5)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b6)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b7)))) + else + Nat_big_num.add (Nat_big_num.add (Nat_big_num.add (Nat_big_num.add +(natural_of_byte b7)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b6)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b5)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b4))) (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))( Nat_big_num.add (Nat_big_num.add (Nat_big_num.add(natural_of_byte b3)(Nat_big_num.mul(Nat_big_num.of_int 256)(natural_of_byte b2)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(natural_of_byte b1)))(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(natural_of_byte b0))))) + in + PR_success( v, ({ pc_bytes = bytes'; pc_offset = (Nat_big_num.add pc.pc_offset(Nat_big_num.of_int 8)) })) + | _ -> PR_fail( "parse_uint64 not given enough bytes", pc) + )) + +let integerFromTwosComplementNatural (n:Nat_big_num.num) (half: Nat_big_num.num) (all:Nat_big_num.num) : Nat_big_num.num= + (if Nat_big_num.less n half then n else Nat_big_num.sub ( n) all) + +let partialTwosComplementNaturalFromInteger (i:Nat_big_num.num) (half: Nat_big_num.num) (all:Nat_big_num.num) : Nat_big_num.num= + (if Nat_big_num.greater_equal i(Nat_big_num.of_int 0) && Nat_big_num.less i ( half) then partialNaturalFromInteger i + else if Nat_big_num.greater_equal i (Nat_big_num.sub(Nat_big_num.of_int 0)( half)) && Nat_big_num.less i(Nat_big_num.of_int 0) then partialNaturalFromInteger ( Nat_big_num.add all i) + else failwith "partialTwosComplementNaturalFromInteger") + + +let parse_sint8 : Nat_big_num.num parser= + (pr_post_map (parse_uint8) (fun n -> integerFromTwosComplementNatural n(Nat_big_num.of_int 128)(Nat_big_num.of_int 256))) + +let parse_sint16 c : Nat_big_num.num parser= + (pr_post_map (parse_uint16 c) (fun n -> integerFromTwosComplementNatural n (Nat_big_num.mul(Nat_big_num.of_int 128)(Nat_big_num.of_int 256)) (Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256)))) + +let parse_sint32 c : Nat_big_num.num parser= + (pr_post_map (parse_uint32 c) (fun n -> integerFromTwosComplementNatural n (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 128)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256)) (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256)))) + +let parse_sint64 c : Nat_big_num.num parser= + (pr_post_map (parse_uint64 c) (fun n -> integerFromTwosComplementNatural n (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 128)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256)) (Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.mul(Nat_big_num.of_int 256)(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256))(Nat_big_num.of_int 256)))) + +let rec parse_ULEB128' (acc: Nat_big_num.num) (shift_factor: Nat_big_num.num) : Nat_big_num.num parser= + (fun (pc:parse_context) -> + let _ = (my_debug "ULEB128' ") in + (match pc.pc_bytes with + | b::bytes' -> + let n = (natural_of_byte b) in + let acc' = (Nat_big_num.add (Nat_big_num.mul (Nat_big_num.bitwise_and n(Nat_big_num.of_int 127)) shift_factor) acc) in + let finished = ( Nat_big_num.equal(Nat_big_num.bitwise_and n(Nat_big_num.of_int 128))(Nat_big_num.of_int 0)) in + let pc' = ({ pc_bytes = bytes'; pc_offset = (Nat_big_num.add pc.pc_offset(Nat_big_num.of_int 1)) }) in + if finished then + PR_success( acc', pc') + else + parse_ULEB128' acc' ( Nat_big_num.mul shift_factor(Nat_big_num.of_int 128)) pc' + | _ -> + PR_fail( "parse_ULEB128' not given enough bytes", pc) + )) + +let parse_ULEB128 : Nat_big_num.num parser= + (fun (pc:parse_context) -> + parse_ULEB128'(Nat_big_num.of_int 0)(Nat_big_num.of_int 1) pc) + +let rec parse_SLEB128' (acc: Nat_big_num.num) (shift_factor: Nat_big_num.num) : (bool * Nat_big_num.num * Nat_big_num.num) parser= + (fun (pc:parse_context) -> + let _ = (my_debug "SLEB128' ") in + (match pc.pc_bytes with + | b::bytes' -> + let n = (natural_of_byte b) in + let acc' = (Nat_big_num.add acc (Nat_big_num.mul (Nat_big_num.bitwise_and n(Nat_big_num.of_int 127)) shift_factor)) in + let shift_factor' = (Nat_big_num.mul shift_factor(Nat_big_num.of_int 128)) in + let finished = ( Nat_big_num.equal(Nat_big_num.bitwise_and n(Nat_big_num.of_int 128))(Nat_big_num.of_int 0)) in + let positive = ( Nat_big_num.equal(Nat_big_num.bitwise_and n(Nat_big_num.of_int 64))(Nat_big_num.of_int 0)) in + let pc' = ({ pc_bytes = bytes'; pc_offset = (Nat_big_num.add pc.pc_offset(Nat_big_num.of_int 1)) }) in + if finished then + PR_success( (positive, shift_factor', acc'), pc') + else + parse_SLEB128' acc' shift_factor' pc' + | _ -> + PR_fail( "parse_SLEB128' not given enough bytes", pc) + )) + +let parse_SLEB128 : Nat_big_num.num parser= + (pr_post_map (parse_SLEB128'(Nat_big_num.of_int 0)(Nat_big_num.of_int 1)) (fun (positive, shift_factor, acc) -> + if positive then acc else Nat_big_num.sub ( acc) ( shift_factor))) + +let parse_nonzero_ULEB128_pair : ( (Nat_big_num.num*Nat_big_num.num)option) parser= + (let _ = (my_debug "nonzero_ULEB128_pair ") in + pr_post_map + (parse_pair parse_ULEB128 parse_ULEB128) + (fun (n1,n2) -> if Nat_big_num.equal n1(Nat_big_num.of_int 0) &&Nat_big_num.equal n2(Nat_big_num.of_int 0) then None else Some (n1,n2))) + +let parse_zero_terminated_ULEB128_pair_list : ( (Nat_big_num.num*Nat_big_num.num)list) parser= + (let _ = (my_debug "zero_terminated_ULEB128_pair_list ") in + parse_list parse_nonzero_ULEB128_pair) + +let parse_uintDwarfN c (df: dwarf_format) : Nat_big_num.num parser= + ((match df with + | Dwarf32 -> (parse_uint32 c) + | Dwarf64 -> (parse_uint64 c) + )) + +let parse_uint_address_size c (as': Nat_big_num.num) : Nat_big_num.num parser= + ( + if(Nat_big_num.equal as' (Nat_big_num.of_int 4)) then (parse_uint32 c) else + ( + if(Nat_big_num.equal as' (Nat_big_num.of_int 8)) then (parse_uint64 c) + else + (failwith ("cuh_address_size not 4 or 8: " ^ Nat_big_num.to_string as')))) + +let parse_uint_segment_selector_size c (ss: Nat_big_num.num) : ( Nat_big_num.num option) parser= + ( + if(Nat_big_num.equal ss (Nat_big_num.of_int 0)) then (pr_return None) else + ( + if(Nat_big_num.equal ss (Nat_big_num.of_int 1)) then + (pr_post_map (parse_uint8) (fun n -> Some n)) else + ( + if(Nat_big_num.equal ss (Nat_big_num.of_int 2)) then + (pr_post_map (parse_uint16 c) (fun n -> Some n)) else + ( + if(Nat_big_num.equal ss (Nat_big_num.of_int 4)) then + (pr_post_map (parse_uint32 c) (fun n -> Some n)) else + ( + if(Nat_big_num.equal ss (Nat_big_num.of_int 8)) then + (pr_post_map (parse_uint64 c) (fun n -> Some n)) else + (failwith "cuh_address_size not 4 or 8")))))) + + + +(** ************************************************************ *) +(** ** parsing and pretty printing of .debug_* sections ****** *) +(** ************************************************************ *) + + +(** abbreviations table: pp and parsing *) + +let pp_abbreviation_declaration (x:abbreviation_declaration):string= + (" " + ^ (Nat_big_num.to_string x.ad_abbreviation_code ^ (" " + ^ (pp_tag_encoding x.ad_tag ^ (" " + ^ ((if x.ad_has_children then "[has children]" else "[no children]") + ^ ("\n" +(* ^ " "^show (List.length x.ad_attribute_specifications) ^ " attributes\n"*) + ^ myconcat "" + (Lem_list.map + (fun (n1,n2) -> + " " ^ (pp_attribute_encoding n1 ^ (" " ^ (pp_attribute_form_encoding n2 ^ "\n")))) + x.ad_attribute_specifications)))))))) + +let pp_abbreviations_table (x:abbreviations_table):string= + (myconcat "" (Lem_list.map (pp_abbreviation_declaration) x)) + +let parse_abbreviation_declaration c : ( abbreviation_declaration option) parser= + (fun (pc: parse_context) -> + pr_bind (parse_ULEB128 pc) (fun n1 pc' -> + if Nat_big_num.equal n1(Nat_big_num.of_int 0) then + PR_success( None, pc') + else + pr_bind (parse_ULEB128 pc') (fun n2 pc'' -> + pr_bind (parse_uint8 pc'') (fun c pc''' -> + pr_post_map1 + (parse_zero_terminated_ULEB128_pair_list pc''') + (fun l -> + Some ( let ad = + ({ + ad_abbreviation_code = n1; + ad_tag = n2; + ad_has_children = (not (Nat_big_num.equal c(Nat_big_num.of_int 0))); + ad_attribute_specifications = l; + }) in let _ = (my_debug2 (pp_abbreviation_declaration ad)) in ad) + ))))) + +let parse_abbreviations_table c:parse_context ->((abbreviation_declaration)list)parse_result= + (parse_list (parse_abbreviation_declaration c)) + + +(** debug_str entry *) + +(*val mydrop : forall 'a. natural -> list 'a -> maybe (list 'a)*) +let rec mydrop n xs:('a list)option= + (if Nat_big_num.equal n(Nat_big_num.of_int 0) then Some xs + else + (match xs with + | x::xs' -> mydrop (Nat_big_num.sub_nat n(Nat_big_num.of_int 1)) xs' + | [] -> None + )) + +let rec null_terminated_list (acc: char list) (xs: char list) : char list= + ((match xs with + | [] -> List.rev acc (* TODO: flag failure? *) + | x::xs' -> if Nat_big_num.equal (natural_of_byte x)(Nat_big_num.of_int 0) then List.rev acc else null_terminated_list (x::acc) xs' + )) + +let pp_debug_str_entry (str: char list) (n: Nat_big_num.num):string= + ((match mydrop n str with + | None -> "strp beyond .debug_str extent" + | Some xs -> string_of_bytes (null_terminated_list [] xs) + )) + +(** operations: pp and parsing *) + +let pp_operation_argument_value (oav:operation_argument_value) : string= + ((match oav with + | OAV_natural n -> pphex n + | OAV_integer n -> Nat_big_num.to_string n + | OAV_block( n, bs) -> pphex n ^ (" " ^ ppbytes + instance_Show_Show_Missing_pervasives_byte_dict bs) + )) + +let pp_operation_semantics (os: operation_semantics) : string= + ((match os with + | OpSem_lit -> "OpSem_lit" + | OpSem_deref -> "OpSem_deref" + | OpSem_stack _ -> "OpSem_stack ..." + | OpSem_not_supported -> "OpSem_not_supported" + | OpSem_binary _ -> "OpSem_binary ..." + | OpSem_unary _ -> "OpSem_unary ..." + | OpSem_opcode_lit _ -> "OpSem_opcode_lit ..." + | OpSem_reg -> "OpSem_reg" + | OpSem_breg -> "OpSem_breg" + | OpSem_bregx -> "OpSem_bregx" + | OpSem_fbreg -> "OpSem_fbreg" + | OpSem_deref_size -> "OpSem_deref_size" + | OpSem_nop -> "OpSem_nop" + | OpSem_piece -> "OpSem_piece" + | OpSem_bit_piece -> "OpSem_bitpiece" + | OpSem_implicit_value -> "OpSem_implicit_value" + | OpSem_stack_value -> "OpSem_stack_value" + | OpSem_call_frame_cfa -> "OpSem_call_frame_cfa" + )) + +let pp_operation (op: operation) : string= + (op.op_string ^ (" " ^ (myconcat " " (Lem_list.map pp_operation_argument_value op.op_argument_values) ^ (" (" ^ (pp_operation_semantics op.op_semantics ^ ")"))))) + +let pp_operations (ops: operation list) : string= + (myconcat "; " (Lem_list.map pp_operation ops)) + +(*val parser_of_operation_argument_type : p_context -> compilation_unit_header -> operation_argument_type -> (parser operation_argument_value)*) +let parser_of_operation_argument_type c cuh oat:parse_context ->(operation_argument_value)parse_result= + ((match oat with + | OAT_addr -> + pr_map2 (fun n -> OAV_natural n) (parse_uint_address_size c cuh.cuh_address_size) + | OAT_dwarf_format_t -> + pr_map2 (fun n -> OAV_natural n) (parse_uintDwarfN c cuh.cuh_dwarf_format) + | OAT_uint8 -> pr_map2 (fun n -> OAV_natural n) (parse_uint8) + | OAT_uint16 -> pr_map2 (fun n -> OAV_natural n) (parse_uint16 c) + | OAT_uint32 -> pr_map2 (fun n -> OAV_natural n) (parse_uint32 c) + | OAT_uint64 -> pr_map2 (fun n -> OAV_natural n) (parse_uint64 c) + | OAT_sint8 -> pr_map2 (fun n -> OAV_integer n) (parse_sint8) + | OAT_sint16 -> pr_map2 (fun n -> OAV_integer n) (parse_sint16 c) + | OAT_sint32 -> pr_map2 (fun n -> OAV_integer n) (parse_sint32 c) + | OAT_sint64 -> pr_map2 (fun n -> OAV_integer n) (parse_sint64 c) + | OAT_ULEB128 -> pr_map2 (fun n -> OAV_natural n) parse_ULEB128 + | OAT_SLEB128 -> pr_map2 (fun n -> OAV_integer n) parse_SLEB128 + | OAT_block -> + (fun pc -> pr_bind (parse_ULEB128 pc) (fun n pc' -> + pr_map (fun bs -> OAV_block( n, bs)) (parse_n_bytes n pc'))) + )) + +(*val parse_operation : p_context -> compilation_unit_header -> parser (maybe operation)*) +let parse_operation c cuh pc:((operation)option)parse_result= + ((match parse_uint8 pc with + | PR_fail( s, pc') -> PR_success( None, pc) + | PR_success( code, pc') -> + (match lookup_aBcd_acd + instance_Basic_classes_Eq_Num_natural_dict code operation_encodings with + | None -> PR_fail( ("encoding not found: " ^ pphex code), pc) + | Some (s,oats,opsem) -> + let ps = (Lem_list.map (parser_of_operation_argument_type c cuh) oats) in + (pr_post_map + (parse_parser_list ps) + (fun oavs -> Some { op_code = code; op_string = s; op_argument_values = oavs; op_semantics = opsem }) + ) + pc' + ) + )) + +(*val parse_operations : p_context -> compilation_unit_header -> parser (list operation)*) +let parse_operations c cuh:parse_context ->((operation)list)parse_result= + (parse_list (parse_operation c cuh)) + +(*val parse_and_pp_operations : p_context -> compilation_unit_header -> list byte -> string*) +let parse_and_pp_operations c cuh bs:string= + (let pc = ({pc_bytes = bs; pc_offset =(Nat_big_num.of_int 0) }) in + (match parse_operations c cuh pc with + | PR_fail( s, pc') -> "parse_operations fail: " ^ pp_parse_fail s pc' + | PR_success( ops, pc') -> + pp_operations ops + ^ (if not ((listEqualBy (=) pc'.pc_bytes [])) then " Warning: extra non-parsed bytes" else "") + )) + + +(** attribute values: pp and parsing *) + +(*val pp_attribute_value : p_context -> compilation_unit_header -> list byte -> natural (*attribute tag*) -> attribute_value -> string*) +let pp_attribute_value c cuh str at av:string= + ((match av with + | AV_addr x -> "AV_addr " ^ pphex x + | AV_block( n, bs) -> "AV_block " ^ (Nat_big_num.to_string n ^ (" " ^ (ppbytes + instance_Show_Show_Missing_pervasives_byte_dict bs + ^ (if Nat_big_num.equal at (attribute_encode "DW_AT_location") then " " ^ parse_and_pp_operations c cuh bs else "")))) + | AV_constantN( n, bs) -> "AV_constantN " ^ (Nat_big_num.to_string n ^ (" " ^ ppbytes + instance_Show_Show_Missing_pervasives_byte_dict bs)) + | AV_constant_SLEB128 i -> "AV_constant_SLEB128 " ^ Nat_big_num.to_string i + | AV_constant_ULEB128 n -> "AV_constant_ULEB128 " ^ Nat_big_num.to_string n + | AV_exprloc( n, bs) -> "AV_exprloc " ^ (Nat_big_num.to_string n ^ (" " ^ (ppbytes + instance_Show_Show_Missing_pervasives_byte_dict bs + ^ (" " ^ parse_and_pp_operations c cuh bs)))) + | AV_flag b -> "AV_flag " ^ string_of_bool b + | AV_ref n -> "AV_ref " ^ pphex n + | AV_ref_addr n -> "AV_ref_addr " ^ pphex n + | AV_ref_sig8 n -> "AV_ref_sig8 " ^ pphex n + | AV_sec_offset n -> "AV_sec_offset " ^ pphex n + | AV_string bs -> string_of_bytes bs + | AV_strp n -> "AV_sec_offset " ^ (pphex n ^ (" " + ^ pp_debug_str_entry str n)) + )) + + +(*val parser_of_attribute_form_non_indirect : p_context -> compilation_unit_header -> natural -> parser attribute_value*) +let parser_of_attribute_form_non_indirect c cuh n:parse_context ->(attribute_value)parse_result= +( +(* address*)if Nat_big_num.equal n (attribute_form_encode "DW_FORM_addr") then + pr_map2 (fun n -> AV_addr n) (parse_uint_address_size c cuh.cuh_address_size) +(* block *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_block1") then + (fun pc -> pr_bind (parse_uint8 pc) (fun n pc' -> + pr_map (fun bs -> AV_block( n, bs)) (parse_n_bytes n pc'))) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_block2") then + (fun pc -> pr_bind (parse_uint16 c pc) (fun n pc' -> + pr_map (fun bs -> AV_block( n, bs)) (parse_n_bytes n pc'))) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_block4") then + (fun pc -> pr_bind (parse_uint32 c pc) (fun n pc' -> + pr_map (fun bs -> AV_block( n, bs)) (parse_n_bytes n pc'))) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_block") then + (fun pc -> pr_bind (parse_ULEB128 pc) (fun n pc' -> + pr_map (fun bs -> AV_block( n, bs)) (parse_n_bytes n pc'))) +(* constant *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_data1") then + pr_map2 (fun bs -> AV_block((Nat_big_num.of_int 1), bs)) (parse_n_bytes(Nat_big_num.of_int 1)) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_data2") then + pr_map2 (fun bs -> AV_block((Nat_big_num.of_int 2), bs)) (parse_n_bytes(Nat_big_num.of_int 2)) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_data4") then + pr_map2 (fun bs -> AV_block((Nat_big_num.of_int 4), bs)) (parse_n_bytes(Nat_big_num.of_int 4)) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_data8") then + pr_map2 (fun bs -> AV_block((Nat_big_num.of_int 8), bs)) (parse_n_bytes(Nat_big_num.of_int 8)) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_sdata") then + pr_map2 (fun i -> AV_constant_SLEB128 i) parse_SLEB128 + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_udata") then + pr_map2 (fun n -> AV_constant_ULEB128 n) parse_ULEB128 +(* exprloc *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_exprloc") then + (fun pc -> pr_bind (parse_ULEB128 pc) (fun n pc' -> + pr_map (fun bs -> AV_exprloc( n, bs)) (parse_n_bytes n pc'))) +(* flag *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_flag") then + pr_map2 (fun n -> AV_flag (not (Nat_big_num.equal n(Nat_big_num.of_int 0)))) (parse_uint8) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_flag_present") then + pr_map2 (fun () -> AV_flag true) (pr_return ()) +(* lineptr, loclistptr, macptr, rangelistptr *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_sec_offset") then + pr_map2 (fun n -> AV_sec_offset n) (parse_uintDwarfN c cuh.cuh_dwarf_format) +(* reference - first type *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_ref1") then + pr_map2 (fun n -> AV_ref n) (parse_uint8) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_ref2") then + pr_map2 (fun n -> AV_ref n) (parse_uint16 c) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_ref4") then + pr_map2 (fun n -> AV_ref n) (parse_uint32 c) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_ref8") then + pr_map2 (fun n -> AV_ref n) (parse_uint64 c) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_ref_udata") then + pr_map2 (fun n -> AV_ref n) parse_ULEB128 +(* reference - second type *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_ref_addr") then + pr_map2 (fun n -> AV_ref_addr n) (parse_uintDwarfN c cuh.cuh_dwarf_format) +(* reference - third type *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_ref_sig8") then + pr_map2 (fun n -> AV_ref_sig8 n) (parse_uint64 c) +(* string *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_string") then + pr_map2 (fun bs -> AV_string bs) parse_string + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_strp") then + pr_map2 (fun n -> AV_strp n) (parse_uintDwarfN c cuh.cuh_dwarf_format) +(* indirect (cycle detection) *) + else if Nat_big_num.equal n (attribute_form_encode "DW_FORM_indirect") then + failwith "DW_FORM_INDIRECT cycle" +(* unknown *) + else + failwith "parser_of_attribute_form_non_indirect: unknown attribute form") + + +let parser_of_attribute_form c cuh n:parse_context ->(attribute_value)parse_result= + (if Nat_big_num.equal n (attribute_form_encode "DW_FORM_indirect") then + (fun pc -> pr_bind (parse_ULEB128 pc) (fun n -> + parser_of_attribute_form_non_indirect c cuh n) ) + else + parser_of_attribute_form_non_indirect c cuh n) + +(** attribute find *) + +let find_name str ats : string option= + (myfindmaybe + (fun (((at: Nat_big_num.num), (af: Nat_big_num.num)), ((pos: Nat_big_num.num),(av:attribute_value))) -> + if Nat_big_num.equal (attribute_encode "DW_AT_name") at then + let name1 = + ((match av with + | AV_string bs -> string_of_bytes bs + | AV_strp n -> pp_debug_str_entry str n + | _ -> "av_name AV not understood" + )) in + Some name1 + else + None) + ats) + +let find_name_of_die str die1 : string option= + (let ats = (Lem_list.list_combine + die1.die_abbreviation_declaration.ad_attribute_specifications + die1.die_attribute_values) in + find_name str ats) + +let find_attribute_value (an: string) (die1:die) : attribute_value option= + (let at = (attribute_encode an) in + let ats = (Lem_list.list_combine + die1.die_abbreviation_declaration.ad_attribute_specifications + die1.die_attribute_values) in + myfindmaybe + (fun (((at': Nat_big_num.num), (af: Nat_big_num.num)), ((pos: Nat_big_num.num),(av:attribute_value))) -> + if Nat_big_num.equal at' at then Some av else None) + ats) + +(** compilation unit header: pp and parsing *) + +let pp_dwarf_format df:string= ((match df with Dwarf32 -> "(32-bit)" | Dwarf64 -> "(64-bit)" )) + +let pp_unit_header (s:string) (x:compilation_unit_header) : string= + (" " ^ (s ^ (" Unit @ offset " ^ (pphex x.cuh_offset ^ (":\n" + ^ (" Length: " ^ (pphex x.cuh_unit_length ^ (" " ^ (pp_dwarf_format x.cuh_dwarf_format ^ ("\n" + ^ (" Version: " ^ (Nat_big_num.to_string x.cuh_version ^ ("\n" + ^ (" Abbrev Offset: " ^ (pphex x.cuh_debug_abbrev_offset ^ ("\n" + ^ (" Pointer Size: " ^ (Nat_big_num.to_string x.cuh_address_size ^ "\n")))))))))))))))))) + +let pp_compilation_unit_header (x:compilation_unit_header) : string= + (pp_unit_header "Compilation" x) + +let parse_unit_length c : (dwarf_format * Nat_big_num.num) parser= + (fun (pc: parse_context) -> + pr_bind (parse_uint32 c pc) (fun x pc' -> + if Nat_big_num.less x (natural_of_hex "0xfffffff0") then PR_success( (Dwarf32,x), pc') + else if not (Nat_big_num.equal x (natural_of_hex "0xffffffff")) then PR_fail( "bad unit_length", pc) + else + pr_bind (parse_uint64 c pc') (fun x' pc'' -> + PR_success( (Dwarf64, x'), pc')))) + + +let parse_compilation_unit_header c : compilation_unit_header parser= + (pr_post_map + (pr_with_pos + (parse_dependent_pair + (parse_unit_length c) + (fun (df,ul) -> + parse_triple + (parse_uint16 c) (* version *) + (parse_uintDwarfN c df) (* debug abbrev offset *) + (parse_uint8) (* address_size *)))) + (fun (offset,((df,ul), (v, (dao, as')))) -> + { + cuh_offset = offset; + cuh_dwarf_format = df; + cuh_unit_length = ul; + cuh_version = v; + cuh_debug_abbrev_offset = dao; + cuh_address_size = as'; + })) + + +(** type unit header: pp and parsing *) + +(* the test binaries don't have a .debug_types section, so this isn't tested *) + +let pp_type_unit_header (x:type_unit_header) : string= + (pp_unit_header "Type" x.tuh_cuh + ^ (" Type Signature: " ^ (pphex x.tuh_type_signature ^ ("\n" + ^ (" Type Offset: " ^ (pphex x.tuh_type_offset ^ "\n")))))) + + +let parse_type_unit_header c : type_unit_header parser= + (pr_post_map + (parse_dependent_pair + (parse_compilation_unit_header c) + (fun cuh -> + parse_pair + (parse_uint64 c) (* type signature *) + (parse_uintDwarfN c cuh.cuh_dwarf_format) (* type offset *) )) + (fun (cuh, (ts, to')) -> + { + tuh_cuh = cuh; + tuh_type_signature = ts; + tuh_type_offset = to'; + })) + + +(** debugging information entries: pp and parsing *) + +(* example pp from readelf + <2><51>: Abbrev Number: 3 (DW_TAG_variable) + <52> DW_AT_name : x + <54> DW_AT_decl_file : 1 + <55> DW_AT_decl_line : 2 + <56> DW_AT_type : <0x6a> + <5a> DW_AT_location : 2 byte block: 91 6c (DW_OP_fbreg: -20) +*) + +let pp_pos pos:string= ("<" ^ (pphex pos ^">")) + +let indent_level (level: Nat_big_num.num):string= (Xstring.implode (replicate0 ( Nat_big_num.mul(Nat_big_num.of_int 3) level) ' ')) + +let pp_die_attribute c (cuh:compilation_unit_header) (str : char list) (level: Nat_big_num.num) (((at: Nat_big_num.num), (af: Nat_big_num.num)), ((pos: Nat_big_num.num),(av:attribute_value))) : string= + (indent_level ( Nat_big_num.add level(Nat_big_num.of_int 1)) ^ (pp_pos pos ^ (" " + ^ (pp_attribute_encoding at ^ (" : " + ^ ("(" ^ (pp_attribute_form_encoding af ^ (") " + ^ (pp_attribute_value c cuh str at av + ^ "\n"))))))))) + +(*val pp_die : p_context -> compilation_unit_header -> list byte -> natural -> bool -> die -> string*) +let rec pp_die c cuh str level (pp_children:bool) die1:string= + (indent_level level ^ ("<" ^ (Nat_big_num.to_string level ^ (">" + ^ (pp_pos die1.die_offset + ^ (": Abbrev Number: " ^ (Nat_big_num.to_string die1.die_abbreviation_code + ^ (" (" ^ (pp_tag_encoding die1.die_abbreviation_declaration.ad_tag ^(")\n" + ^ +(let ats = (Lem_list.list_combine + die1.die_abbreviation_declaration.ad_attribute_specifications + die1.die_attribute_values) in + (myconcat "" (Lem_list.map (pp_die_attribute c cuh str level) ats)) + ^ +(if pp_children then myconcat "" (Lem_list.map (pp_die c cuh str ( Nat_big_num.add level(Nat_big_num.of_int 1)) pp_children) die1.die_children) else "")))))))))))) + +(*val pp_die_abbrev : p_context -> compilation_unit_header -> list byte -> natural -> bool -> (list die) -> die -> string*) +let rec pp_die_abbrev c cuh str level (pp_children:bool) parents die1:string= + (indent_level level + ^ (pp_tag_encoding die1.die_abbreviation_declaration.ad_tag + ^ (" (" ^ (pp_pos die1.die_offset ^ (") " +(* ^ ": Abbrev Number: " ^ show die.die_abbreviation_code *) + ^ +(let ats = (Lem_list.list_combine + die1.die_abbreviation_declaration.ad_attribute_specifications + die1.die_attribute_values) in + ((match find_name str ats with Some s -> s | None -> "-" )) + ^ (" : " ^ (myconcat " : " (Lem_list.map (fun die' -> pp_tag_encoding die'.die_abbreviation_declaration.ad_tag) parents) + ^ ("\n" + ^ + +( (*(myconcat "" (List.map (pp_die_abbrev_attribute c cuh str) ats))*)if pp_children then myconcat "" (Lem_list.map (pp_die_abbrev c cuh str ( Nat_big_num.add level(Nat_big_num.of_int 1)) pp_children (die1::parents)) die1.die_children) else "")))))))))) + + + +(*val parse_die : p_context -> list byte -> compilation_unit_header -> (natural->abbreviation_declaration) -> parser (maybe die)*) +let rec parse_die c str cuh find_abbreviation_declaration:parse_context ->((die)option)parse_result= + (fun (pc: parse_context) -> + let _ = (my_debug3 ("parse_die called at " ^ (pp_parse_context pc ^ "\n"))) in + pr_bind (parse_ULEB128 pc) (fun abbreviation_code pc' -> + if Nat_big_num.equal abbreviation_code(Nat_big_num.of_int 0) then PR_success( None, pc') + else + let _ = (my_debug3 ("parse_die abbreviation code "^(pphex abbreviation_code ^"\n"))) in + let ad = (find_abbreviation_declaration abbreviation_code) in + let attribute_value_parsers = (Lem_list.map (fun (at,af) -> pr_with_pos (parser_of_attribute_form c cuh af)) ad.ad_attribute_specifications) in + pr_bind (parse_parser_list attribute_value_parsers pc') (fun avs pc'' -> + +(* + let die_header = + <| + die_offset = pc.pc_offset; + die_abbreviation_code = abbreviation_code; + die_abbreviation_declaration = ad; + die_attribute_values = avs; + die_children = []; + |> in let _ = my_debug3 ("die_header " ^ pp_die cuh str 999 die_header) in + *) + pr_bind + (if ad.ad_has_children then parse_list (parse_die c str cuh find_abbreviation_declaration) pc'' else pr_return [] pc'') + (fun dies pc''' -> + PR_success( (Some ( let die1 = + ({ + die_offset = (pc.pc_offset); + die_abbreviation_code = abbreviation_code; + die_abbreviation_declaration = ad; + die_attribute_values = avs; + die_children = dies; + }) in (* let _ = my_debug3 ("die entire " ^ pp_die cuh str 999 die) in *)die1)), pc'''))))) + +let has_attribute (an: string) (die1: die) : bool= + (Lem_list.elem instance_Basic_classes_Eq_Num_natural_dict + (attribute_encode an) + (Lem_list.map fst die1.die_abbreviation_declaration.ad_attribute_specifications)) + + +(** compilation units: pp and parsing *) + +let pp_compilation_unit c (debug_str_section_body: char list) cu:string= + + ("*** compilation unit header ***\n" + ^ (pp_compilation_unit_header cu.cu_header + ^ ("\n*** compilation unit abbreviation table ***\n" + ^ (pp_abbreviations_table cu.cu_abbreviations_table + ^ ("\n*** compilation unit die tree ***\n" + ^ (pp_die c cu.cu_header debug_str_section_body(Nat_big_num.of_int 0) true cu.cu_die + ^ "\n")))))) + +let pp_compilation_units c debug_string_section_body (compilation_units1: compilation_unit list) : string= + (myconcat "" (Lem_list.map (pp_compilation_unit c debug_string_section_body) compilation_units1)) + + +let pp_compilation_unit_abbrev c (debug_str_section_body: char list) cu:string= + (pp_compilation_unit_header cu.cu_header +(* ^ pp_abbreviations_table cu.cu_abbreviations_table*) + ^ pp_die_abbrev c cu.cu_header debug_str_section_body(Nat_big_num.of_int 0) true [] cu.cu_die) + +let pp_compilation_units_abbrev c debug_string_section_body (compilation_units1: compilation_unit list) : string= + (myconcat "" (Lem_list.map (pp_compilation_unit_abbrev c debug_string_section_body) compilation_units1)) + + +let parse_compilation_unit c (debug_str_section_body: char list) (debug_abbrev_section_body: char list) : ( compilation_unit option) parser= + (fun (pc:parse_context) -> + + if (listEqualBy (=) pc.pc_bytes []) then PR_success( None, pc) else + + let (cuh, pc') = + + ((match parse_compilation_unit_header c pc with + | PR_fail( s, pc') -> failwith ("parse_cuh_header fail: " ^ pp_parse_fail s pc') + | PR_success( cuh, pc') -> (cuh,pc') + )) in + + let _ = (my_debug4 (pp_compilation_unit_header cuh)) in + + let pc_abbrev = ({pc_bytes = ((match mydrop cuh.cuh_debug_abbrev_offset debug_abbrev_section_body with Some bs -> bs | None -> failwith "mydrop of debug_abbrev" )); pc_offset = (cuh.cuh_debug_abbrev_offset) }) in + + let abbreviations_table1 = + ((match parse_abbreviations_table c pc_abbrev with + | PR_fail( s, pc_abbrev') -> failwith ("parse_abbrevations_table fail: " ^ pp_parse_fail s pc_abbrev') + | PR_success( at, pc_abbrev') -> at + )) in + + let _ = (my_debug4 (pp_abbreviations_table abbreviations_table1)) in + + let find_abbreviation_declaration (ac:Nat_big_num.num) : abbreviation_declaration= + (let _ = (my_debug4 ("find_abbreviation_declaration "^pphex ac)) in + myfindNonPure (fun ad -> Nat_big_num.equal ad.ad_abbreviation_code ac) abbreviations_table1) in + + let _ = (my_debug3 (pp_abbreviations_table abbreviations_table1)) in + + (match parse_die c debug_str_section_body cuh find_abbreviation_declaration pc' with + | PR_fail( s, pc'') -> failwith ("parse_die fail: " ^ pp_parse_fail s pc'') + | PR_success( (None), pc'') -> failwith ("parse_die returned Nothing: " ^ pp_parse_context pc'') + | PR_success( (Some die1), pc'') -> + let cu = + ({ + cu_header = cuh; + cu_abbreviations_table = abbreviations_table1; + cu_die = die1; + }) in + PR_success( (Some cu), pc'') + )) + +let parse_compilation_units c (debug_str_section_body: char list) (debug_abbrev_section_body: char list): ( compilation_unit list) parser= + + (parse_list (parse_compilation_unit c debug_str_section_body debug_abbrev_section_body)) + + +(** type units: pp and parsing *) + +let pp_type_unit c (debug_str_section_body: char list) tu:string= + (pp_type_unit_header tu.tu_header + ^ (pp_abbreviations_table tu.tu_abbreviations_table + ^ pp_die c tu.tu_header.tuh_cuh debug_str_section_body(Nat_big_num.of_int 0) true tu.tu_die)) + +let pp_type_units c debug_string_section_body (type_units1: type_unit list) : string= + (myconcat "" (Lem_list.map (pp_type_unit c debug_string_section_body) type_units1)) + + +let parse_type_unit c (debug_str_section_body: char list) (debug_abbrev_section_body: char list) : ( type_unit option) parser= + (fun (pc:parse_context) -> + + if (listEqualBy (=) pc.pc_bytes []) then PR_success( None, pc) else + + let (tuh, pc') = + ((match parse_type_unit_header c pc with + | PR_fail( s, pc') -> failwith ("parse_tuh_header fail: " ^ pp_parse_fail s pc') + | PR_success( tuh, pc') -> (tuh,pc') + )) in + + let _ = (my_debug4 (pp_type_unit_header tuh)) in + + let pc_abbrev = (let n = (tuh.tuh_cuh.cuh_debug_abbrev_offset) in {pc_bytes = ((match mydrop n debug_abbrev_section_body with Some bs -> bs | None -> failwith "mydrop of debug_abbrev" )); pc_offset = n }) in + + let abbreviations_table1 = + ((match parse_abbreviations_table c pc_abbrev with + | PR_fail( s, pc_abbrev') -> failwith ("parse_abbrevations_table fail: " ^ pp_parse_fail s pc_abbrev') + | PR_success( at, pc_abbrev') -> at + )) in + + let _ = (my_debug4 (pp_abbreviations_table abbreviations_table1)) in + + let find_abbreviation_declaration (ac:Nat_big_num.num) : abbreviation_declaration= + (let _ = (my_debug4 ("find_abbreviation_declaration "^pphex ac)) in + myfindNonPure (fun ad -> Nat_big_num.equal ad.ad_abbreviation_code ac) abbreviations_table1) in + + let _ = (my_debug3 (pp_abbreviations_table abbreviations_table1)) in + + (match parse_die c debug_str_section_body tuh.tuh_cuh find_abbreviation_declaration pc' with + | PR_fail( s, pc'') -> failwith ("parse_die fail: " ^ pp_parse_fail s pc'') + | PR_success( (None), pc'') -> failwith ("parse_die returned Nothing: " ^ pp_parse_context pc'') + | PR_success( (Some die1), pc'') -> + let tu = + ({ + tu_header = tuh; + tu_abbreviations_table = abbreviations_table1; + tu_die = die1; + }) in + PR_success( (Some tu), pc'') + )) + +let parse_type_units c (debug_str_section_body: char list) (debug_abbrev_section_body: char list): ( type_unit list) parser= + + (parse_list (parse_type_unit c debug_str_section_body debug_abbrev_section_body)) + +(** location lists, pp and parsing *) + +(* readelf example +Contents of the .debug_loc section: + + Offset Begin End Expression + 00000000 0000000000400168 0000000000400174 (DW_OP_reg0 (r0)) + 00000000 0000000000400174 0000000000400184 (DW_OP_GNU_entry_value: (DW_OP_reg0 (r0)); DW_OP_stack_value) + 00000000 <End of list> + 00000039 000000000040017c 0000000000400180 (DW_OP_lit1; DW_OP_stack_value) +*) + +let pp_location_list_entry c (cuh:compilation_unit_header) (offset:Nat_big_num.num) (x:location_list_entry) : string= + (" " ^ (pphex offset + ^ (" " ^ (pphex x.lle_beginning_address_offset + ^ (" " ^ (pphex x.lle_ending_address_offset + ^ (" (" ^ (parse_and_pp_operations c cuh x.lle_single_location_description ^(")" + ^ "\n"))))))))) + +let pp_base_address_selection_entry c (cuh:compilation_unit_header) (offset:Nat_big_num.num) (x:base_address_selection_entry) : string= + (" " ^ (pphex offset + ^ (" " ^ (pphex x.base_address + ^ "\n")))) + +let pp_location_list_item c (cuh: compilation_unit_header) (offset: Nat_big_num.num) (x:location_list_item):string= + ((match x with + | LLI_lle lle -> pp_location_list_entry c cuh offset lle + | LLI_base base -> pp_base_address_selection_entry c cuh offset base + )) + +let pp_location_list c (cuh: compilation_unit_header) ((offset:Nat_big_num.num), (llis: location_list_item list)):string= + (myconcat "" (Lem_list.map (pp_location_list_item c cuh offset) llis)) +(* ^ " " ^ pphex offset ^ " <End of list>\n"*) + +let pp_loc c (cuh: compilation_unit_header) (lls: location_list list):string= + (" Offset Begin End Expression\n" + ^ myconcat "" (Lem_list.map (pp_location_list c cuh) lls)) + +(* Note that this is just pp'ing the raw location list data - Sectoin +3.1.1 says: The applicable base address of a location list entry is +determined by the closest preceding base address selection entry in +the same location list. If there is no such selection entry, then the +applicable base address defaults to the base address of the +compilation unit. That is handled by the interpret_location_list below *) + + + +let parse_location_list_item c (cuh: compilation_unit_header) : ( location_list_item option) parser= + (fun (pc:parse_context) -> + pr_bind + (parse_pair + (parse_uint_address_size c cuh.cuh_address_size) + (parse_uint_address_size c cuh.cuh_address_size) + pc) + (fun ((a1: Nat_big_num.num),(a2:Nat_big_num.num)) pc' -> + let _ = (my_debug4 ("offset="^(pphex pc.pc_offset ^ (" begin=" ^ (pphex a1 ^ (" end=" ^ pphex a2)))))) in + if Nat_big_num.equal a1(Nat_big_num.of_int 0) &&Nat_big_num.equal a2(Nat_big_num.of_int 0) then + PR_success( None, pc') + else if Nat_big_num.equal a1 (max_address cuh.cuh_address_size) then + let x = (LLI_base { (*base_offset=pc.pc_offset;*) base_address=a1 }) in + PR_success( (Some x (*(pc.pc_offset, x)*)), pc') + else + pr_bind (parse_uint16 c pc') (fun n pc'' -> + pr_post_map1 + (parse_n_bytes n pc'') + (fun bs -> + let x = + (LLI_lle { + (*lle_offset = pc.pc_offset;*) + lle_beginning_address_offset = a1; + lle_ending_address_offset = a2; + lle_single_location_description = bs; + }) in + Some x (*(pc.pc_offset, x)*)) + ) + )) + +let parse_location_list c cuh : ( location_list option) parser= + (fun (pc: parse_context) -> + if (listEqualBy (=) pc.pc_bytes []) then + PR_success( None, pc) + else + pr_post_map1 + (parse_list (parse_location_list_item c cuh) pc) + (fun llis -> (Some (pc.pc_offset, llis)))) + +let parse_location_list_list c cuh : location_list_list parser= + (parse_list (parse_location_list c cuh)) + +let find_location_list dloc n : location_list= + (myfindNonPure (fun (n',_)->Nat_big_num.equal n' n) dloc) + (* fails if location list not found *) + +(* interpretation of a location list applies the base_address and LLI_base offsets to give a list indexed by concrete address ranges *) + +let rec interpret_location_list (base_address1: Nat_big_num.num) (llis: location_list_item list) : (Nat_big_num.num * Nat_big_num.num * single_location_description) list= + ((match llis with + | [] -> [] + | LLI_base base::llis' -> interpret_location_list base.base_address llis' + | LLI_lle lle :: llis' -> (Nat_big_num.add base_address1 lle.lle_beginning_address_offset,Nat_big_num.add base_address1 lle.lle_ending_address_offset, lle.lle_single_location_description) :: interpret_location_list base_address1 llis' + )) + + +(** range lists, pp and parsing *) + +(* readelf example +Contents of the .debug_aranges section: + + Length: 44 + Version: 2 + Offset into .debug_info: 0x0 + Pointer Size: 8 + Segment Size: 0 + + Address Length + 00000000100000e8 0000000000000090 + 0000000000000000 0000000000000000 + Length: 44 + Version: 2 + Offset into .debug_info: 0x1de + Pointer Size: 8 + Segment Size: 0 +*) + +let pp_range_list_entry c (cuh:compilation_unit_header) (offset:Nat_big_num.num) (x:range_list_entry) : string= + (" " ^ (pphex offset + ^ (" " ^ (pphex x.rle_beginning_address_offset + ^ (" " ^ (pphex x.rle_ending_address_offset + ^ "\n")))))) + +let pp_range_list_item c (cuh: compilation_unit_header) (offset: Nat_big_num.num) (x:range_list_item):string= + ((match x with + | RLI_rle rle -> pp_range_list_entry c cuh offset rle + | RLI_base base -> pp_base_address_selection_entry c cuh offset base + )) + +let pp_range_list c (cuh: compilation_unit_header) ((offset:Nat_big_num.num), (rlis: range_list_item list)):string= + (myconcat "" (Lem_list.map (pp_range_list_item c cuh offset) rlis)) +(* ^ " " ^ pphex offset ^ " <End of list>\n"*) + +let pp_ranges c (cuh: compilation_unit_header) (rls: range_list list):string= + (" Offset Begin End Expression\n" + ^ myconcat "" (Lem_list.map (pp_range_list c cuh) rls)) + +(* Note that this is just pp'ing the raw range list data - see also +the interpret_range_list below *) + + +let parse_range_list_item c (cuh: compilation_unit_header) : ( range_list_item option) parser= + (fun (pc:parse_context) -> + pr_bind + (parse_pair + (parse_uint_address_size c cuh.cuh_address_size) + (parse_uint_address_size c cuh.cuh_address_size) + pc) + (fun ((a1: Nat_big_num.num),(a2:Nat_big_num.num)) pc' -> + let _ = (my_debug4 ("offset="^(pphex pc.pc_offset ^ (" begin=" ^ (pphex a1 ^ (" end=" ^ pphex a2)))))) in + if Nat_big_num.equal a1(Nat_big_num.of_int 0) &&Nat_big_num.equal a2(Nat_big_num.of_int 0) then + PR_success( None, pc') + else if Nat_big_num.equal a1 (max_address cuh.cuh_address_size) then + let x = (RLI_base { base_address=a1 }) in + PR_success( (Some x), pc') + else + let x = + (RLI_rle { + rle_beginning_address_offset = a1; + rle_ending_address_offset = a2; + }) in + PR_success( (Some x (*(pc.pc_offset, x)*)), pc') + )) + +let parse_range_list c cuh : ( range_list option) parser= + (fun (pc: parse_context) -> + if (listEqualBy (=) pc.pc_bytes []) then + PR_success( None, pc) + else + pr_post_map1 + (parse_list (parse_range_list_item c cuh) pc) + (fun rlis -> (Some (pc.pc_offset, rlis)))) + +let parse_range_list_list c cuh : range_list_list parser= + (parse_list (parse_range_list c cuh)) + +let find_range_list dranges n : range_list= + (myfindNonPure (fun (n',_)->Nat_big_num.equal n' n) dranges) + (* fails if range list not found *) + +(* interpretation of a range list applies the base_address and RLI_base offsets to give a list of concrete address ranges *) + +let rec interpret_range_list (base_address1: Nat_big_num.num) (rlis: range_list_item list) : (Nat_big_num.num * Nat_big_num.num) list= + ((match rlis with + | [] -> [] + | RLI_base base::rlis' -> interpret_range_list base.base_address rlis' + | RLI_rle rle :: rlis' -> (Nat_big_num.add base_address1 rle.rle_beginning_address_offset,Nat_big_num.add base_address1 rle.rle_ending_address_offset) :: interpret_range_list base_address1 rlis' + )) + +(** frame information, pp and parsing *) + +(* readelf example + +Contents of the .debug_frame section: + +00000000 0000000c ffffffff CIE + Version: 1 + Augmentation: "" + Code alignment factor: 4 + Data alignment factor: -8 + Return address column: 65 + + DW_CFA_def_cfa: r1 ofs 0 + +00000010 00000024 00000000 FDE cie=00000000 pc=100000b0..10000120 + DW_CFA_advance_loc: 8 to 100000b8 + DW_CFA_def_cfa_offset: 80 + DW_CFA_offset: r31 at cfa-8 + DW_CFA_advance_loc: 4 to 100000bc + DW_CFA_def_cfa_register: r31 + DW_CFA_advance_loc: 80 to 1000010c + DW_CFA_def_cfa: r1 ofs 0 + DW_CFA_nop + DW_CFA_nop + DW_CFA_nop + DW_CFA_nop + +00000038 00000024 00000000 FDE cie=00000000 pc=10000120..100001a4 + DW_CFA_advance_loc: 16 to 10000130 + DW_CFA_def_cfa_offset: 144 + DW_CFA_offset_extended_sf: r65 at cfa+16 + DW_CFA_offset: r31 at cfa-8 + DW_CFA_advance_loc: 4 to 10000134 + DW_CFA_def_cfa_register: r31 + DW_CFA_advance_loc: 84 to 10000188 + DW_CFA_def_cfa: r1 ofs 0 +*) + + + +let pp_cfa_address a:string= (pphex a) +let pp_cfa_block dict_Show_Show_a b:string= (ppbytes + dict_Show_Show_a b) +let pp_cfa_delta d:string= (pphex d) +(*let pp_cfa_offset n = pphex n +let pp_cfa_register r = show r*) +let pp_cfa_sfoffset dict_Show_Show_a i:string= ( + dict_Show_Show_a.show_method i) + +let pp_cfa_register dict_Show_Show_a r:string= ("r"^ + dict_Show_Show_a.show_method r) (*TODO: arch-specific register names *) + +let pp_cfa_offset (i:Nat_big_num.num):string= (if Nat_big_num.equal i(Nat_big_num.of_int 0) then "" else if Nat_big_num.less i(Nat_big_num.of_int 0) then Nat_big_num.to_string i else "+" ^ Nat_big_num.to_string i) + +let pp_cfa_rule (cr:cfa_rule) : string= + ((match cr with + | CR_undefined -> "u" + | CR_register( r, i) -> pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ pp_cfa_offset i + | CR_expression bs -> "exp" + )) + +let pp_register_rule (rr:register_rule) : string= +( (*TODO make this more readelf-like *)(match rr with + | RR_undefined -> "u" + | RR_same_value -> "s" + | RR_offset i -> "c" ^ pp_cfa_offset i + | RR_val_offset i -> "val(c" ^ (pp_cfa_offset i ^ ")") + | RR_register r -> pp_cfa_register + instance_Show_Show_Num_natural_dict r + | RR_expression bs -> "exp" + | RR_val_expression bs -> "val(exp)" + | RR_architectural -> "" + )) + + + +let pp_call_frame_instruction i:string= + ((match i with + | DW_CFA_advance_loc d -> "DW_CFA_advance_loc" ^ (" " ^ pp_cfa_delta d) + | DW_CFA_offset( r, n) -> "DW_CFA_offset" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_offset ( n)))) + | DW_CFA_restore r -> "DW_CFA_restore" ^ (" " ^ pp_cfa_register + instance_Show_Show_Num_natural_dict r) + | DW_CFA_nop -> "DW_CFA_nop" + | DW_CFA_set_loc a -> "DW_CFA_set_loc" ^ (" " ^ pp_cfa_address a) + | DW_CFA_advance_loc1 d -> "DW_CFA_advance_loc1" ^ (" " ^ pp_cfa_delta d) + | DW_CFA_advance_loc2 d -> "DW_CFA_advance_loc2" ^ (" " ^ pp_cfa_delta d) + | DW_CFA_advance_loc4 d -> "DW_CFA_advance_loc4" ^ (" " ^ pp_cfa_delta d) + | DW_CFA_offset_extended( r, n) -> "DW_CFA_offset_extended" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_offset ( n)))) + | DW_CFA_restore_extended r -> "DW_CFA_restore_extended" ^ (" " ^ pp_cfa_register + instance_Show_Show_Num_natural_dict r) + | DW_CFA_undefined r -> "DW_CFA_undefined" ^ (" " ^ pp_cfa_register + instance_Show_Show_Num_natural_dict r) + | DW_CFA_same_value r -> "DW_CFA_same_value" ^ (" " ^ pp_cfa_register + instance_Show_Show_Num_natural_dict r) + | DW_CFA_register( r1, r2) -> "DW_CFA_register" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r1 ^ (" " ^ pp_cfa_register + instance_Show_Show_Num_natural_dict r2))) + | DW_CFA_remember_state -> "DW_CFA_remember_state" + | DW_CFA_restore_state -> "DW_CFA_restore_state" + | DW_CFA_def_cfa( r, n) -> "DW_CFA_def_cfa" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_offset ( n)))) + | DW_CFA_def_cfa_register r -> "DW_CFA_def_cfa_register" ^ (" " ^ pp_cfa_register + instance_Show_Show_Num_natural_dict r) + | DW_CFA_def_cfa_offset n -> "DW_CFA_def_cfa_offset" ^ (" " ^ pp_cfa_offset ( n)) + | DW_CFA_def_cfa_expression b -> "DW_CFA_def_cfa_expression" ^ (" " ^ pp_cfa_block + instance_Show_Show_Missing_pervasives_byte_dict b) + | DW_CFA_expression( r, b) -> "DW_CFA_expression" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_block + instance_Show_Show_Missing_pervasives_byte_dict b))) + | DW_CFA_offset_extended_sf( r, i) -> "DW_CFA_offset_extended_sf" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_sfoffset + instance_Show_Show_Num_integer_dict i))) + | DW_CFA_def_cfa_sf( r, i) -> "DW_CFA_def_cfa_sf" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_sfoffset + instance_Show_Show_Num_integer_dict i))) + | DW_CFA_def_cfa_offset_sf i -> "DW_CFA_def_cfa_offset_sf" ^ (" " ^ pp_cfa_sfoffset + instance_Show_Show_Num_integer_dict i) + | DW_CFA_val_offset( r, n) -> "DW_CFA_val_offset" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_offset ( n)))) + | DW_CFA_val_offset_sf( r, i) -> "DW_CFA_val_offset_sf" ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_sfoffset + instance_Show_Show_Num_integer_dict i)) + | DW_CFA_val_expression( r, b) -> "DW_CFA_val_expression" ^ (" " ^ (pp_cfa_register + instance_Show_Show_Num_natural_dict r ^ (" " ^ pp_cfa_block + instance_Show_Show_Missing_pervasives_byte_dict b))) + | DW_CFA_unknown bt -> "DW_CFA_unknown" ^ (" " ^ hex_string_of_byte bt) + )) + +let pp_call_frame_instructions is:string= (myconcat "" (Lem_list.map (fun i -> " " ^ (pp_call_frame_instruction i ^ "\n")) is)) + + +let parser_of_call_frame_argument_type c cuh (cfat: call_frame_argument_type) : call_frame_argument_value parser= + ((match cfat with + | CFAT_address -> pr_map2 (fun n -> CFAV_address n) (parse_uint_address_size c cuh.cuh_address_size) + | CFAT_delta1 -> pr_map2 (fun n -> CFAV_delta n) (parse_uint8) + | CFAT_delta2 -> pr_map2 (fun n -> CFAV_delta n) (parse_uint16 c) + | CFAT_delta4 -> pr_map2 (fun n -> CFAV_delta n) (parse_uint32 c) + | CFAT_delta_ULEB128 -> pr_map2 (fun n -> CFAV_delta n) (parse_ULEB128) + | CFAT_offset -> pr_map2 (fun n -> CFAV_offset n) (parse_ULEB128) + | CFAT_sfoffset -> pr_map2 (fun n -> CFAV_sfoffset n) (parse_SLEB128) + | CFAT_register -> pr_map2 (fun n -> CFAV_register n) (parse_ULEB128) + | CFAT_block -> + (fun pc -> pr_bind (parse_ULEB128 pc) (fun n pc' -> + pr_map (fun bs -> CFAV_block bs) (parse_n_bytes n pc'))) + )) + +let parse_call_frame_instruction c cuh : ( call_frame_instruction option) parser= + (fun pc -> + (match pc.pc_bytes with + | [] -> PR_success( None, pc) + | b::bs' -> + let pc' = ({ pc_bytes = bs'; pc_offset = (Nat_big_num.add pc.pc_offset(Nat_big_num.of_int 1)) }) in + let ch = (Uint32.of_int (Char.code b)) in + let high_bits = (Uint32.logand ch (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 192)))) in + let low_bits = (Nat_big_num.of_string (Uint32.to_string (Uint32.logand ch (Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 63)))))) in + if high_bits = Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 0)) then + (match lookup_abCde_de + instance_Basic_classes_Eq_Num_natural_dict low_bits call_frame_instruction_encoding with + | Some ((args: call_frame_argument_type list), result) -> + let ps = (Lem_list.map (parser_of_call_frame_argument_type c cuh) args) in + let p = + (pr_post_map + (parse_parser_list ps) + result) in + (match p pc' with + | PR_success( (Some cfi), pc'') -> PR_success( (Some cfi), pc'') + | PR_success( (None), pc'') -> failwith "bad call frame instruction argument 1" + | PR_fail( s, pc'') -> failwith "bad call frame instruction argument 2" + ) + | None -> + (*Assert_extra.failwith ("can't parse " ^ show b ^ " as call frame instruction")*) + PR_success( (Some (DW_CFA_unknown b)), pc') + ) + else + if high_bits = Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 64)) then + PR_success( (Some (DW_CFA_advance_loc low_bits)), pc') + else if high_bits = Uint32.of_string (Nat_big_num.to_string (Nat_big_num.of_int 192)) then + PR_success( (Some (DW_CFA_restore low_bits)), pc') + else + let p = (parser_of_call_frame_argument_type c cuh CFAT_offset) in + (match p pc' with + | PR_success( (CFAV_offset n), pc'') -> PR_success( (Some (DW_CFA_offset( low_bits, n))), pc'') + | PR_success( _, pc'') -> failwith "bad call frame instruction argument 3" + | PR_fail( s, pc'') -> failwith "bad call frame instruction argument 4" + ) + )) + +let parse_call_frame_instructions c cuh : ( call_frame_instruction list) parser= + (parse_list (parse_call_frame_instruction c cuh)) + +(*val parse_and_pp_call_frame_instructions : p_context -> compilation_unit_header -> list byte -> string*) +let parse_and_pp_call_frame_instructions c cuh bs:string= + (let pc = ({pc_bytes = bs; pc_offset =(Nat_big_num.of_int 0) }) in + (match parse_call_frame_instructions c cuh pc with + | PR_fail( s, pc') -> "parse_call_frame_instructions fail: " ^ pp_parse_fail s pc' + | PR_success( is, pc') -> + pp_call_frame_instructions is + ^ (if not ((listEqualBy (=) pc'.pc_bytes [])) then " Warning: extra non-parsed bytes" else "") + )) + + + +let pp_call_frame_instructions' c cuh bs:string= +( + (* ppbytes bs ^ "\n" *)parse_and_pp_call_frame_instructions c cuh bs) + + + +let pp_cie c cuh cie1:string= + (pphex cie1.cie_offset + ^ (" " ^ (pphex cie1.cie_length + ^ (" " ^ (pphex cie1.cie_id + ^ (" CIE\n" + ^ (" Version: " ^ (Nat_big_num.to_string cie1.cie_version ^ ("\n" + ^ (" Augmentation: \""^ (string_of_string (Xstring.implode (Lem_list.map (fun x-> x) cie1.cie_augmentation)) ^ ("\"\n" + ^ (" Code alignment factor: " ^ (Nat_big_num.to_string cie1.cie_code_alignment_factor ^ ("\n" + ^ (" Data alignment factor: " ^ (Nat_big_num.to_string cie1.cie_data_alignment_factor ^ ("\n" + ^ (" Return address column: " ^ (Nat_big_num.to_string cie1.cie_return_address_register ^ ("\n" + ^ ("\n" + ^ (ppbytes instance_Show_Show_Missing_pervasives_byte_dict cie1.cie_initial_instructions_bytes ^ ("\n" + ^ pp_call_frame_instructions cie1.cie_initial_instructions)))))))))))))))))))))))) + +(* cie_address_size: natural; (* not shown by readelf - must match compilation unit *)*) +(* cie_segment_size: natural; (* not shown by readelf *)*) +(* readelf says "Return address column", but the DWARF spec says "Return address register" *) + + +let pp_fde c cuh fde1:string= + (pphex fde1.fde_offset + ^ (" " ^ (pphex fde1.fde_length + ^ (" " ^ (pphex fde1.fde_cie_pointer (* not what this field of readelf output is *) + ^ (" FDE" + ^ (" cie=" ^ (pphex fde1.fde_cie_pointer (* duplicated?? *) + ^ (" pc=" ^ ((match fde1.fde_initial_location_segment_selector with None -> "" | Some segment_selector -> "("^(pphex segment_selector^")") ) ^ (pphex fde1.fde_initial_location_address ^ (".." ^ (pphex ( Nat_big_num.add fde1.fde_initial_location_address fde1.fde_address_range) ^ ("\n" + ^ (ppbytes instance_Show_Show_Missing_pervasives_byte_dict fde1.fde_instructions_bytes ^ ("\n" + ^ pp_call_frame_instructions fde1.fde_instructions)))))))))))))))) + +let pp_frame_info_element c cuh fie:string= + ((match fie with + | FIE_cie cie1 -> pp_cie c cuh cie1 + | FIE_fde fde1 -> pp_fde c cuh fde1 + )) + +let pp_frame_info c cuh fi:string= + ("Contents of the .debug_frame section:\n\n" + ^ (myconcat "\n" (Lem_list.map (pp_frame_info_element c cuh) fi) + ^ "\n")) + + + +let rec find_cie fi cie_id1:cie= + ((match fi with + | [] -> failwith "find_cie: cie_id not found" + | FIE_fde _ :: fi' -> find_cie fi' cie_id1 + | FIE_cie cie1 :: fi' -> if Nat_big_num.equal cie_id1 cie1.cie_offset then cie1 else find_cie fi' cie_id1 + )) + +let parse_initial_location c cuh mss mas' : (( Nat_big_num.num option) * Nat_big_num.num) parser= +( (*(segment selector and target address)*) + (* assume segment selector size is zero unless given explicitly. Probably we need to do something architecture-specific for earlier dwarf versions?*)parse_pair + (parse_uint_segment_selector_size c ((match mss with Some n -> n | None ->Nat_big_num.of_int 0 ))) + (parse_uint_address_size c ((match mas' with Some n -> n | None -> cuh.cuh_address_size )))) + + +let parse_call_frame_instruction_bytes offset' ul:parse_context ->((char)list)parse_result= + (fun (pc: parse_context) -> + parse_n_bytes ( Nat_big_num.sub_nat ul ( Nat_big_num.sub_nat pc.pc_offset offset')) pc) + +let parse_frame_info_element c cuh (fi: frame_info_element list) : frame_info_element parser= + (parse_dependent + (pr_with_pos + (parse_dependent_pair + (parse_unit_length c) + (fun (df,ul) -> + pr_with_pos + (parse_uintDwarfN c df) (* CIE_id (cie) or CIE_pointer (fde) *) + ))) + (fun (offset,((df,ul),(offset',cie_id1))) -> + if ( Nat_big_num.equal cie_id1 + (match df with + | Dwarf32 -> natural_of_hex "0xffffffff" + | Dwarf64 -> natural_of_hex "0xffffffffffffffff" + )) + then + (* parse cie *) + pr_post_map + (parse_pair + (parse_dependent_pair + parse_uint8 (* version *) + (fun v -> + parse_triple + parse_string (* augmentation *) + (if Nat_big_num.equal v(Nat_big_num.of_int 4) ||Nat_big_num.equal v(Nat_big_num.of_int 46) then pr_post_map parse_uint8 (fun i->Some i) else pr_return None) (* address_size *) + (if Nat_big_num.equal v(Nat_big_num.of_int 4) ||Nat_big_num.equal v(Nat_big_num.of_int 46) then pr_post_map parse_uint8 (fun i->Some i) else pr_return None))) (* segment_size *) + (parse_quadruple + parse_ULEB128 (* code_alignment_factor *) + parse_SLEB128 (* data_alignment_factor *) + parse_ULEB128 (* return address register *) + (parse_call_frame_instruction_bytes offset' ul))) + (fun ( (v,(aug,(mas',mss))), (caf,(daf,(rar,bs))) ) -> + let pc = ({pc_bytes = bs; pc_offset =(Nat_big_num.of_int 0) }) in + (match parse_call_frame_instructions c cuh pc with + | PR_success( is, _) -> + FIE_cie + ( + { + cie_offset = offset; + cie_length = ul; + cie_id = cie_id1; + cie_version = v; + cie_augmentation = aug; + cie_address_size = mas'; + cie_segment_size = mss; + cie_code_alignment_factor = caf; + cie_data_alignment_factor = daf; + cie_return_address_register = rar; + cie_initial_instructions_bytes = bs; + cie_initial_instructions = is; + }) + | PR_fail( s, _) -> failwith s + ) + ) + + else + (* parse fde *) + let cie1 = (find_cie fi cie_id1) in + let _ = (my_debug4 (pp_cie c cuh cie1)) in + pr_post_map + (parse_triple + (parse_initial_location c cuh cie1.cie_segment_size cie1.cie_address_size) (*(segment selector and target address)*) + (parse_uint_address_size c ((match cie1.cie_address_size with Some n -> n | None -> cuh.cuh_address_size ))) (* address_range (target address) *) + (parse_call_frame_instruction_bytes offset' ul) + ) + (fun ( (ss,adr), (ar, bs)) -> + let pc = ({pc_bytes = bs; pc_offset =(Nat_big_num.of_int 0) }) in + (match parse_call_frame_instructions c cuh pc with + | PR_success( is, _) -> + FIE_fde + ( + { + fde_offset = offset; + fde_length = ul; + fde_cie_pointer = cie_id1; + fde_initial_location_segment_selector = ss; + fde_initial_location_address = adr; + fde_address_range = ar; + fde_instructions_bytes = bs; + fde_instructions = is; + } ) + | PR_fail( s, _) -> failwith s + ) + ) + )) + +(* you can't even parse an fde without accessing the cie it refers to +(to determine the segment selector size). Gratuitous complexity or what? +Hence the following, which should be made more tail-recursive. *) + +(*val parse_dependent_list' : forall 'a. (list 'a -> parser 'a) -> list 'a -> parser (list 'a)*) +let rec parse_dependent_list' p1 acc:parse_context ->('a list)parse_result= + (fun pc -> + if (listEqualBy (=) pc.pc_bytes []) then + PR_success( (List.rev acc), pc) + else + pr_bind + (p1 acc pc) + (fun x pc' -> + parse_dependent_list' p1 (x::acc) pc')) + +(*val parse_dependent_list : forall 'a. (list 'a -> parser 'a) -> parser (list 'a)*) +let parse_dependent_list p1:parse_context ->('a list)parse_result= (parse_dependent_list' p1 []) + + +let parse_frame_info c cuh : frame_info parser= + +(parse_dependent_list (parse_frame_info_element c cuh)) + + +(** line numbers .debug_line, pp and parsing *) + +let pp_line_number_file_entry lnfe:string= + ("lnfe_path = " ^ (string_of_bytes lnfe.lnfe_path ^ ("\n" +^ ("lnfe_directory_index " ^ (Nat_big_num.to_string lnfe.lnfe_directory_index ^ ("\n" +^ ("lnfe_last_modification = " ^ (Nat_big_num.to_string lnfe.lnfe_last_modification ^ ("\n" +^ ("lnfe_length = " ^ (Nat_big_num.to_string lnfe.lnfe_length ^ "\n"))))))))))) + + +let pp_line_number_header lnh:string= + ("offset = " ^ (pphex lnh.lnh_offset ^ ("\n" +^ ("dwarf_format = " ^ (pp_dwarf_format lnh.lnh_dwarf_format ^ ("\n" +^ ("unit_length = " ^ (Nat_big_num.to_string lnh.lnh_unit_length ^ ("\n" +^ ("version = " ^ (Nat_big_num.to_string lnh.lnh_version ^ ("\n" +^ ("header_length = " ^ (Nat_big_num.to_string lnh.lnh_header_length ^ ("\n" +^ ("minimum_instruction_length = " ^ (Nat_big_num.to_string lnh.lnh_minimum_instruction_length ^ ("\n" +^ ("maximum_operations_per_instruction = " ^ (Nat_big_num.to_string lnh.lnh_maximum_operations_per_instruction ^ ("\n" +^ ("default_is_stmt = " ^ (string_of_bool lnh.lnh_default_is_stmt ^ ("\n" +^ ("line_base = " ^ (Nat_big_num.to_string lnh.lnh_line_base ^ ("\n" +^ ("line_range = " ^ (Nat_big_num.to_string lnh.lnh_line_range ^ ("\n" +^ ("opcode_base = " ^ (Nat_big_num.to_string lnh.lnh_opcode_base ^ ("\n" +^ ("standard_opcode_lengths = " ^ (string_of_list + instance_Show_Show_Num_natural_dict lnh.lnh_standard_opcode_lengths ^ ("\n" +^ ("include_directories = " ^ (myconcat ", " (Lem_list.map string_of_bytes lnh.lnh_include_directories) ^ ("\n" +^ ("file_names = \n\n" ^ (myconcat "\n" (Lem_list.map pp_line_number_file_entry lnh.lnh_file_names) ^ "\n"))))))))))))))))))))))))))))))))))))))))) + +let pp_line_number_operation lno:string= + ((match lno with + | DW_LNS_copy -> "DW_LNS_copy" + | DW_LNS_advance_pc n -> "DW_LNS_advance_pc" ^ (" " ^ Nat_big_num.to_string n) + | DW_LNS_advance_line i -> "DW_LNS_advance_line" ^ (" " ^ Nat_big_num.to_string i) + | DW_LNS_set_file n -> "DW_LNS_set_file" ^ (" " ^ Nat_big_num.to_string n) + | DW_LNS_set_column n -> "DW_LNS_set_column" ^ (" " ^ Nat_big_num.to_string n) + | DW_LNS_negate_stmt -> "DW_LNS_negate_stmt" + | DW_LNS_set_basic_block -> "DW_LNS_set_basic_block" + | DW_LNS_const_add_pc -> "DW_LNS_const_add_pc" + | DW_LNS_fixed_advance_pc n -> "DW_LNS_fixed_advance_pc" ^ (" " ^ Nat_big_num.to_string n) + | DW_LNS_set_prologue_end -> "DW_LNS_set_prologue_end" + | DW_LNS_set_epilogue_begin -> "DW_LNS_set_epilogue_begin" + | DW_LNS_set_isa n -> "DW_LNS_set_isa" ^ (" " ^ Nat_big_num.to_string n) + | DW_LNE_end_sequence -> "DW_LNE_end_sequence" + | DW_LNE_set_address n -> "DW_LNE_set_address" ^ (" " ^ pphex n) + | DW_LNE_define_file( s, n1, n2, n3) -> "DW_LNE_define_file" ^ (" " ^ (string_of_list + instance_Show_Show_Missing_pervasives_byte_dict s ^ (" " ^ (Nat_big_num.to_string n1 ^ (" " ^ (Nat_big_num.to_string n2 ^ (" " ^ Nat_big_num.to_string n3))))))) + | DW_LNE_set_discriminator n -> "DW_LNE_set_discriminator" ^ (" " ^ Nat_big_num.to_string n) + | DW_LN_special n -> "DW_LN_special" ^ (" " ^ Nat_big_num.to_string n) + )) + +let pp_line_number_program lnp:string= + (pp_line_number_header lnp.lnp_header + ^ ("[" ^ (myconcat ", " (Lem_list.map pp_line_number_operation lnp.lnp_operations) ^ "]\n"))) + + + +let parse_line_number_file_entry : ( line_number_file_entry option) parser= + +(parse_dependent + (parse_non_empty_string) + (fun ms -> + (match ms with + | None -> + pr_return None + | Some s -> + pr_post_map + (parse_triple + parse_ULEB128 + parse_ULEB128 + parse_ULEB128 + ) + (fun (n1,(n2,n3)) -> + (Some + { + lnfe_path = s; + lnfe_directory_index = n1; + lnfe_last_modification = n2; + lnfe_length = n3; + } ) + ) + ) + )) + +let parse_line_number_header c : line_number_header parser= + (parse_dependent + ((pr_with_pos + (parse_unit_length c) )) + (fun (pos,(df,ul)) -> + parse_dependent + (parse_pair + (parse_triple + (parse_uint16 c) (* version *) + (parse_uintDwarfN c df) (* header_length *) + (parse_uint8) (* minimum_instruction_length *) + (* (parse_uint8) (* maximum_operations_per_instruction *) NOT IN DWARF 2*) + ) + (parse_quadruple + (parse_uint8) (* default_is_stmt *) + (parse_sint8) (* line_base *) + (parse_uint8) (* line_range *) + (parse_uint8) (* opcode_base *) + )) + (fun ((v,(hl,(minil(*,maxopi*)))),(dis,(lb,(lr,ob)))) -> + pr_post_map + (parse_triple + (pr_post_map (parse_n_bytes (Nat_big_num.sub_nat ob(Nat_big_num.of_int 1))) (Lem_list.map natural_of_byte)) (* standard_opcode_lengths *) + ((*pr_return [[]]*) parse_list parse_non_empty_string) (* include_directories *) + (parse_list parse_line_number_file_entry) (* file names *) + ) + (fun (sols, (ids, fns)) -> + { + lnh_offset = pos; + lnh_dwarf_format = df; + lnh_unit_length = ul; + lnh_version = v; + lnh_header_length = hl; + lnh_minimum_instruction_length = minil; + lnh_maximum_operations_per_instruction =(Nat_big_num.of_int 1) (*maxopi*); + lnh_default_is_stmt = (not (Nat_big_num.equal dis(Nat_big_num.of_int 0))); + lnh_line_base = lb; + lnh_line_range = lr; + lnh_opcode_base = ob; + lnh_standard_opcode_lengths = sols; + lnh_include_directories = ids; + lnh_file_names = fns; + } + ) + ) + ) + ) + +let parser_of_line_number_argument_type c (cuh: compilation_unit_header) (lnat: line_number_argument_type) : line_number_argument_value parser= + ((match lnat with + | LNAT_address -> pr_map2 (fun n -> LNAV_address n) (parse_uint_address_size c cuh.cuh_address_size) + | LNAT_ULEB128 -> pr_map2 (fun n -> LNAV_ULEB128 n) (parse_ULEB128) + | LNAT_SLEB128 -> pr_map2 (fun i -> LNAV_SLEB128 i) (parse_SLEB128) + | LNAT_uint16 -> pr_map2 (fun n -> LNAV_uint16 n) (parse_uint16 c) + | LNAT_string -> pr_map2 (fun s -> LNAV_string s) (parse_string) + )) + +let parse_line_number_operation c (cuh: compilation_unit_header) (lnh: line_number_header) : line_number_operation parser= + (parse_dependent + parse_uint8 + (fun opcode -> + if Nat_big_num.equal opcode(Nat_big_num.of_int 0) then + (* parse extended opcode *) + parse_dependent + (parse_pair + parse_ULEB128 + parse_uint8) + (fun (size2,opcode') -> + (match lookup_aBcd_acd + instance_Basic_classes_Eq_Num_natural_dict opcode' line_number_extended_encodings with + | Some (_, arg_types, result) -> + let ps = (Lem_list.map (parser_of_line_number_argument_type c cuh) arg_types) in + parse_demaybe ("parse_line_number_operation fail") + (pr_post_map + (parse_parser_list ps) + result ) + | None -> + failwith ("parse_line_number_operation extended opcode not found: " ^ Nat_big_num.to_string opcode') + )) + (* it's not clear what the ULEB128 size field is for, as the extended opcides all seem to have well-defined sizes. perhaps there can be extra padding that needs to be absorbed? *) + else if Nat_big_num.greater_equal opcode lnh.lnh_opcode_base then + (* parse special opcode *) + let adjusted_opcode = (Nat_big_num.sub_nat opcode lnh.lnh_opcode_base) in + pr_return (DW_LN_special adjusted_opcode) + else + (* parse standard opcode *) + (match lookup_aBcd_acd + instance_Basic_classes_Eq_Num_natural_dict opcode line_number_standard_encodings with + | Some (_, arg_types, result) -> + let ps = (Lem_list.map (parser_of_line_number_argument_type c cuh) arg_types) in + parse_demaybe ("parse_line_number_operation fail") + (pr_post_map + (parse_parser_list ps) + result) + | None -> + failwith ("parse_line_number_operation standard opcode not found: " ^ Nat_big_num.to_string opcode) + (* the standard_opcode_lengths machinery is intended to allow vendor specific extension instructions to be parsed and ignored, but here we couldn't usefully process such instructions in any case, so we just fail *) + ))) + + +let parse_line_number_operations c (cuh:compilation_unit_header) (lnh:line_number_header) : ( line_number_operation list) parser= + (parse_list (parse_maybe (parse_line_number_operation c cuh lnh))) + + + (* assume operations start immediately after the header - not completely clear in DWARF whether the header_length is just an optimisation or whether it's intended to allow the operations to start later *) + (* line number operations have no no-op and no termination operation, so we have to cut down the available bytes to the right length *) + +let parse_line_number_program c (cuh:compilation_unit_header) : line_number_program parser= + (parse_dependent + (parse_line_number_header c) + (fun lnh -> + let byte_count_of_operations = (Nat_big_num.sub_nat + lnh.lnh_unit_length ( Nat_big_num.add (Nat_big_num.add lnh.lnh_header_length(Nat_big_num.of_int 2)) ((match lnh.lnh_dwarf_format with Dwarf32 ->Nat_big_num.of_int 4 | Dwarf64 ->Nat_big_num.of_int 8 )))) in + pr_post_map + (parse_restrict_length + byte_count_of_operations + (parse_line_number_operations c cuh lnh) + ) + (fun ops -> + { + lnp_header = lnh; + lnp_operations = ops; + }) + )) + +let parse_line_number_info c (d_line: char list) (cu: compilation_unit) : line_number_program= + (let f n= + (let d_line' = ((match mydrop n d_line with Some xs -> xs | None -> failwith "parse_line_number_info drop" )) in + let pc = ({ pc_bytes = d_line'; pc_offset = n}) in + (match parse_line_number_program c cu.cu_header pc with + | PR_success( lnp, pc') -> + (*let _ = print_endline (pp_line_number_program lnp) in*) + lnp + | PR_fail( s, pc') -> failwith ("parse_line_number_header failed: " ^ s) + )) in + (match find_attribute_value "DW_AT_stmt_list" cu.cu_die with + | Some (AV_sec_offset n) -> f n + | Some (AV_block( n, bs)) -> f (natural_of_bytes c.endianness bs) + (* a 32-bit MIPS example used a 4-byte AV_block not AV_sec_offset *) + | Some _ -> failwith "compilation unit DW_AT_stmt_list attribute was not an AV_sec_offset" + | _ -> failwith "compilation unit did not have a DW_AT_stmt_list attribute" + )) + + +let parse_line_number_infos c debug_line_section_body compilation_units1:(line_number_program)list= + + (Lem_list.map (parse_line_number_info c debug_line_section_body) compilation_units1) + +let pp_line_info li:string= + +(myconcat "\n" (Lem_list.map (pp_line_number_program) li)) + + +(** all dwarf info: pp and parsing *) + +let pp_dwarf d:string= + (let c : p_context = ({ endianness = (d.d_endianness) }) in + + "\n************** .debug_info section - abbreviated *****************\n" + ^ (pp_compilation_units_abbrev c d.d_str d.d_compilation_units + ^ ("\n************** .debug_info section - full ************************\n" + ^ (pp_compilation_units c d.d_str d.d_compilation_units + ^ ("\n************** .debug_loc section: location lists ****************\n" + ^ (let (cuh_default : compilation_unit_header) = (let cu = (myhead d.d_compilation_units) in cu.cu_header) in + pp_loc c cuh_default d.d_loc + ^ ("\n************** .debug_ranges section: range lists ****************\n" + ^ (pp_ranges c cuh_default d.d_ranges + ^ ("\n************** .debug_frame section: frame info ****************\n" + ^ (pp_frame_info c cuh_default d.d_frame_info + ^ ("\n************** .debug_line section: line number info ****************\n" + ^ pp_line_info d.d_line_info))))))))))) + + +let parse_dwarf c + (debug_info_section_body: char list) + (debug_abbrev_section_body: char list) + (debug_str_section_body: char list) + (debug_loc_section_body: char list) + (debug_ranges_section_body: char list) + (debug_frame_section_body: char list) + (debug_line_section_body: char list) + : dwarf= + + (let pc_info = ({pc_bytes = debug_info_section_body; pc_offset =(Nat_big_num.of_int 0) }) in + + let compilation_units1 = + ((match parse_compilation_units c debug_str_section_body debug_abbrev_section_body pc_info with + | PR_fail( s, pc_info') -> failwith ("parse_compilation_units: " ^ pp_parse_fail s pc_info') + | PR_success( cus, pc_info') -> cus + )) in + + (*let _ = my_debug5 (pp_compilation_units c debug_str_section_body compilation_units) in*) + + +(* the DWARF4 spec doesn't seem to specify the address size used in the .debug_loc section, so we (hackishly) take it from the first compilation unit *) + let (cuh_default : compilation_unit_header) = (let cu = (myhead compilation_units1) in cu.cu_header) in + + let pc_loc = ({pc_bytes = debug_loc_section_body; pc_offset =(Nat_big_num.of_int 0) }) in + + let loc = + ((match parse_location_list_list c cuh_default pc_loc with + | PR_fail( s, pc_info') -> failwith ("parse_location_list: " ^ pp_parse_fail s pc_info') + | PR_success( loc, pc_loc') -> loc + )) in + + let pc_ranges = ({pc_bytes = debug_ranges_section_body; pc_offset =(Nat_big_num.of_int 0) }) in + + let ranges = + ((match parse_range_list_list c cuh_default pc_ranges with + | PR_fail( s, pc_info') -> failwith ("parse_range_list: " ^ pp_parse_fail s pc_info') + | PR_success( r, pc_loc') -> r + )) in + + let pc_frame = ({pc_bytes = debug_frame_section_body; pc_offset =(Nat_big_num.of_int 0) }) in + + let fi = + (let _ = (my_debug5 ("debug_frame_section_body:\n" ^ ppbytes2 + instance_Show_Show_Missing_pervasives_byte_dict(Nat_big_num.of_int 0) debug_frame_section_body)) in + + (match parse_frame_info c cuh_default pc_frame with + | PR_fail( s, pc_info') -> failwith ("parse_frame_info: " ^ pp_parse_fail s pc_info') + | PR_success( fi, pc_loc') -> fi + )) in + + let li = (parse_line_number_infos c debug_line_section_body compilation_units1) in + + { + d_endianness = (c.endianness); + d_str = debug_str_section_body; + d_compilation_units = compilation_units1; + d_type_units = ([]); + d_loc = loc; + d_ranges = ranges; + d_frame_info = fi; + d_line_info = li; + }) + +(*val extract_dwarf : elf_file -> maybe dwarf*) +let extract_dwarf f:(dwarf)option= + + (let (en: Endianness.endianness) = + ((match f with + | ELF_File_32 f32 -> Elf_header.get_elf32_header_endianness f32.Elf_file.elf32_file_header + | ELF_File_64 f64 -> Elf_header.get_elf64_header_endianness f64.Elf_file.elf64_file_header + )) in + let (c: p_context) = ({ endianness = en }) in + let extract_section_body section_name (strict: bool)= + ((match f with + | ELF_File_32 f32 -> + let sections = + (List.filter + (fun x -> + x.Elf_interpreted_section.elf32_section_name_as_string = section_name + ) f32.elf32_file_interpreted_sections) in + (match sections with + | [section] -> + let section_body = ((match section.Elf_interpreted_section.elf32_section_body with Sequence bs -> bs )) in + let _ = (my_debug4 (section_name ^ (": \n" ^ (Elf_interpreted_section.string_of_elf32_interpreted_section section ^ ("\n" + ^ (" body = " ^ (ppbytes2 + instance_Show_Show_Missing_pervasives_byte_dict(Nat_big_num.of_int 0) section_body ^ "\n"))))))) in + section_body + | [] -> + if strict then + failwith ("" ^ (section_name ^ " section not present")) + else + [] + | _ -> failwith ("multiple " ^ (section_name ^ " sections present")) + ) + + + | ELF_File_64 f64 -> + let sections = + (List.filter + (fun x -> + x.Elf_interpreted_section.elf64_section_name_as_string = section_name + ) f64.elf64_file_interpreted_sections) in + (match sections with + | [section] -> + let section_body = ((match section.Elf_interpreted_section.elf64_section_body with Sequence bs -> bs )) in + section_body + | [] -> + if strict then + failwith ("" ^ (section_name ^ " section not present")) + else + [] + | _ -> failwith ("multiple " ^ (section_name ^ " sections present")) + ) + )) in + + let debug_info_section_body = (extract_section_body ".debug_info" true) in + let debug_abbrev_section_body = (extract_section_body ".debug_abbrev" false) in + let debug_str_section_body = (extract_section_body ".debug_str" false) in + let debug_loc_section_body = (extract_section_body ".debug_loc" false) in + let debug_ranges_section_body = (extract_section_body ".debug_ranges" false) in + let debug_frame_section_body = (extract_section_body ".debug_frame" false) in + let debug_line_section_body = (extract_section_body ".debug_line" false) in + + let d = (parse_dwarf c debug_info_section_body debug_abbrev_section_body debug_str_section_body debug_loc_section_body debug_ranges_section_body debug_frame_section_body debug_line_section_body) in + + Some d) + + +(** ************************************************************ *) +(** ****** location evaluation ******************************** *) +(** ************************************************************ *) + + +(** pp of locations *) + +(*val pp_simple_location : simple_location -> string*) +let pp_simple_location sl:string= + ((match sl with + | SL_memory_address n -> pphex n + | SL_register n -> "reg" ^ Nat_big_num.to_string n + | SL_implicit bs -> "value: " ^ ppbytes + instance_Show_Show_Missing_pervasives_byte_dict bs + | SL_empty -> "<empty>" + )) + +(*val pp_composite_location_piece : composite_location_piece -> string*) +let pp_composite_location_piece clp:string= + ((match clp with + | CLP_piece( n, sl) -> "piece (" ^ (Nat_big_num.to_string n ^ (") " ^ pp_simple_location sl)) + | CLP_bit_piece( n1, n2, sl) -> "bit_piece (" ^ (Nat_big_num.to_string n1 ^ ("," ^ (Nat_big_num.to_string n2 ^ (") " ^ pp_simple_location sl)))) + )) + +(*val pp_single_location: single_location -> string*) +let pp_single_location sl:string= + ((match sl with + | SL_simple sl -> pp_simple_location sl + | SL_composite clps -> "composite: " ^ myconcat ", " (Lem_list.map pp_composite_location_piece clps) + )) + + +(** evaluation of location expressions *) + +(* cf dwarflist, btw: https://fedorahosted.org/elfutils/wiki/DwarfLint?format=txt *) + +(* + +location description ::= +| single location description +| location list + +single location description ::= +| simple location description +| composite location description + +simple location description ::= +| memory location description : non-empty dwarf expr, value is address of all or part of object in memory +| register location description : single DW_OP_regN or DW_OP_regx, naming a register in which all the object is +| implicit location description : single DW_OP_implicit_value or a non-empty dwarf expr ending in DW_OP_stack_value, giving the value of all/part of object +| empty location description : an empty dwarf expr, indicating a part or all of an object that is not represented + +composite location description : a list of simple location descriptions, each followed by a DW_OP_piece or DW_OP_bitpiece + +(the simple location description can be a register location description: https://www.mail-archive.com/dwarf-discuss@lists.dwarfstd.org/msg00271.html) +(contradicting "A register location description must stand alone as the entire description of an object or a piece of an object.") + +location list entry : a list of address ranges (possibly overlapping), each with a single location description + +Dwarf expressions can include data-dependent control flow choices +(though we don't see that in the examples?), so we can't statically +determine which kind of single location description or simple location +description we have. We can distinguish: + +- empty -> simple.empty +- DW_OP_regN/DW_OP_regx -> simple.register +- DW_OP_implicit_value -> simple.implicit +- any of those followed by DW_OP_piece or DW_OP_bitpiece, perhaps followed by more composite parts -> composite part :: composite + +otherwise run to the end, or a DW_OP_stack_value at the end, or to +anything (except a DO_OP_regN/DW_OP_regx) followed by a +DW_OP_piece/DW_OP_bitpiece. Pfeh. + + +actually used in our examples (ignoring GNU extentions): + +DW_OP_addr literal +DW_OP_lit1 literal +DW_OP_const4u literal + +DW_OP_breg3 (r3) read register value and add offset + +DW_OP_and bitwise and +DW_OP_plus addition (mod whatever) + +DW_OP_deref_size +DW_OP_fbreg evaluate location description from DW_AT_frame_base attribute of the current function (which is DW_OP_call_frame_cfa in our examples) and add offset + +DW_OP_implicit_value the argument block is the actual value (not location) of the entity in question +DW_OP_stack_value use the value at top of stack as the actual value (not location) of the entity in question + +DW_OP_reg0 (r0)) read register value + +DW_OP_call_frame_cfa go off to 6.4 and pull info out of .debug_frame (possibly involving other location expressions) + +*) + + + +let initial_state:state= + ({ + s_stack = ([]); + s_value = SL_empty; + s_location_pieces = ([]); +}) + +(* the main location expression evaluation function *) + +(* location expression evaluation is basically a recursive function +down a list of operations, maintaining an operation_stack (a list of +naturals representing machine-address-size words), the current +simple_location, and a list of any composite_location_piece's +accumulated so far *) + + + +let arithmetic_context_of_cuh cuh:arithmetic_context= + ( + if(Nat_big_num.equal cuh.cuh_address_size (Nat_big_num.of_int 8)) then + ({ ac_bitwidth =(Nat_big_num.of_int 64); + ac_half = (Nat_big_num.pow_int (Nat_big_num.of_int 2) ( 32)); + ac_all = (Nat_big_num.pow_int (Nat_big_num.of_int 2) ( 64)); + ac_max = (Nat_big_num.sub_nat + (Nat_big_num.pow_int (Nat_big_num.of_int 2) ( 64)) + (Nat_big_num.of_int 1)); }) else + ( + if(Nat_big_num.equal cuh.cuh_address_size (Nat_big_num.of_int 4)) then + ({ ac_bitwidth =(Nat_big_num.of_int 32); + ac_half = (Nat_big_num.pow_int (Nat_big_num.of_int 2) ( 16)); + ac_all = (Nat_big_num.pow_int (Nat_big_num.of_int 2) ( 32)); + ac_max = (Nat_big_num.sub_nat + (Nat_big_num.pow_int (Nat_big_num.of_int 2) ( 32)) + (Nat_big_num.of_int 1)); }) else + (failwith "arithmetic_context_of_cuh given non-4/8 size"))) + +let find_cfa_table_row_for_pc (evaluated_frame_info1: evaluated_frame_info) (pc: Nat_big_num.num) : cfa_table_row= + ((match + myfind + (fun (fde1,rows) -> Nat_big_num.greater_equal pc fde1.fde_initial_location_address && Nat_big_num.less pc (Nat_big_num.add fde1.fde_initial_location_address fde1.fde_address_range)) + evaluated_frame_info1 + with + | Some (fde1,rows) -> + (match myfind (fun row -> Nat_big_num.greater_equal pc row.ctr_loc) rows with + | Some row -> row + | None -> failwith "evaluate_cfa: no matchine row" + ) + | None -> failwith "evaluate_cfa: no fde encloding pc" + )) + + +let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evaluated_frame_info1: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: attribute_value option) (pc: Nat_big_num.num) (s: state) (ops: operation list) : single_location error= + + (let push_memory_address v vs'= (Success { s with s_stack = (v :: vs'); s_value = (SL_memory_address v) }) in + + let push_memory_address_maybe (mv: Nat_big_num.num option) vs' (err:string) op= + ((match mv with + | Some v -> push_memory_address v vs' + | None -> Fail (err ^ pp_operation op) + )) in + + let bregxi r i= + ((match ev.read_register r with + | RRR_result v -> push_memory_address (partialNaturalFromInteger ( Nat_big_num.modulus(Nat_big_num.add( v)i) ( ac.ac_all))) s.s_stack + | RRR_not_currently_available -> Fail "RRR_not_currently_available" + | RRR_bad_register_number -> Fail ("RRR_bad_register_number " ^ Nat_big_num.to_string r) + )) in + + let deref_size n= + ((match s.s_stack with + | v::vs' -> + (match ev.read_memory v n with + | MRR_result v' -> push_memory_address v' vs' + | MRR_not_currently_available -> Fail "MRR_not_currently_available" + | MRR_bad_address -> Fail "MRR_bad_address" + ) + | _ -> Fail "OpSem unary not given an element on stack" + )) in + + (match ops with + | [] -> + if (listEqualBy (=) s.s_location_pieces []) then + Success (SL_simple s.s_value) + else if s.s_value = SL_empty then + Success (SL_composite s.s_location_pieces) + else + (* unclear what's supposed to happen in this case *) + Fail "unfinished part of composite expression" + + | op::ops' -> + let es' = + ((match (op.op_semantics, op.op_argument_values) with + | (OpSem_nop, []) -> + Success s + | (OpSem_lit, [OAV_natural n]) -> + push_memory_address n s.s_stack + | (OpSem_lit, [OAV_integer i]) -> + push_memory_address (partialTwosComplementNaturalFromInteger i ac.ac_half ( ac.ac_all)) s.s_stack + | (OpSem_stack f, []) -> + (match f ac s.s_stack op.op_argument_values with + | Some stack' -> + let value' : simple_location = ((match stack' with [] -> SL_empty | v'::_ -> SL_memory_address v' )) in + Success { s with s_stack = stack'; s_value = value' } + | None -> Fail "OpSem_stack failed" + ) + | (OpSem_not_supported, []) -> + Fail ("OpSem_not_supported: " ^ pp_operation op) + | (OpSem_binary f, []) -> + (match s.s_stack with + | v1::v2::vs' -> push_memory_address_maybe (f ac v1 v2) vs' "OpSem_binary error: " op + | _ -> Fail "OpSem binary not given two elements on stack" + ) + | (OpSem_unary f, []) -> + (match s.s_stack with + | v1::vs' -> push_memory_address_maybe (f ac v1) vs' "OpSem_unary error: " op + | _ -> Fail "OpSem unary not given an element on stack" + ) + | (OpSem_opcode_lit base, []) -> + if Nat_big_num.greater_equal op.op_code base && Nat_big_num.less op.op_code (Nat_big_num.add base(Nat_big_num.of_int 32)) then + push_memory_address ( Nat_big_num.sub_nat op.op_code base) s.s_stack + else + Fail "OpSem_opcode_lit opcode not within [base,base+32)" + | (OpSem_reg, []) -> + (* TODO: unclear whether this should push the register id or not *) + let r = (Nat_big_num.sub_nat op.op_code vDW_OP_reg0) in + Success { s with s_stack = (r :: s.s_stack); s_value = (SL_register r) } + | (OpSem_breg, [OAV_integer i]) -> + let r = (Nat_big_num.sub_nat op.op_code vDW_OP_breg0) in + bregxi r i + | (OpSem_bregx, [OAV_natural r; OAV_integer i]) -> + bregxi r i + | (OpSem_deref, []) -> + deref_size cuh.cuh_address_size + | (OpSem_deref_size, [OAV_natural n]) -> + deref_size n + | (OpSem_fbreg, [OAV_integer i]) -> + (match mfbloc with + | Some fbloc -> + (*let _ = my_debug5 ("OpSem_fbreg (" ^ show i ^ ")\n") in*) + (match evaluate_location_description c dloc evaluated_frame_info1 cuh ac ev (*mfbloc*)None pc fbloc with + (* what to do if the recursive call also uses fbreg? for now assume that's not allowed *) + | Success l -> + (match l with + | SL_simple (SL_memory_address a) -> + (*let _ = my_debug5 ("OpSem_fbreg: a = "^ pphex a ^ "\n") in*) + let vi = (Nat_big_num.modulus ( Nat_big_num.add( a) i) ( ac.ac_all)) in + (*let _ = my_debug5 ("OpSem_fbreg: v = "^ show vi ^ "\n") in*) + let v = (partialNaturalFromInteger vi) (*ac.ac_half (integerFromNatural ac.ac_all)*) in + push_memory_address v s.s_stack + | _ -> + Fail "OpSem_fbreg got a non-SL_simple (SL_memory_address _) result" + (* "The DW_OP_fbreg operation provides a signed LEB128 + offset from the address specified by the location + description in the DW_AT_frame_base attribute of the + current function. " + - so what to do if the location description returns a non-memory-address location? *) + ) + | Fail e -> + Fail ("OpSem_fbreg failure: " ^ e) + ) + | None -> + Fail "OpSem_fbreg: no frame base location description given" + ) + + | (OpSem_piece, [OAV_natural size_bytes]) -> + let piece = (CLP_piece( size_bytes, s.s_value)) in + (* we allow a piece (or bit_piece) to be any simple_location, including implicit and stack values. Unclear if this is intended, esp. the latter *) + let stack' = ([]) in + let value' = SL_empty in + Success { s_stack = stack'; s_value = value'; s_location_pieces = (List.rev_append (List.rev s.s_location_pieces) [piece]) } + | (OpSem_bit_piece, [OAV_natural size_bits; OAV_natural offset_bits]) -> + let piece = (CLP_bit_piece( size_bits, offset_bits, s.s_value)) in + let stack' = ([]) in + let value' = SL_empty in + Success { s_stack = stack'; s_value = value'; s_location_pieces = (List.rev_append (List.rev s.s_location_pieces) [piece]) } + | (OpSem_implicit_value, [OAV_block( size2, bs)]) -> + let stack' = ([]) in + let value' = (SL_implicit bs) in + Success { s with s_stack = stack'; s_value = value' } + | (OpSem_stack_value, []) -> + (* "The DW_OP_stack_value operation terminates the expression." - does + this refer to just the subexpression, ie allowing a stack value to be + a piece of a composite location, or necessarily the whole expression? + Why does DW_OP_stack_value have this clause while DW_OP_implicit_value + does not? *) + (* why doesn't DW_OP_stack_value have a size argument? *) + (match s.s_stack with + | v::vs' -> + let stack' = ([]) in + let value' = (SL_implicit (bytes_of_natural c.endianness cuh.cuh_address_size v)) in + Success { s with s_stack = stack'; s_value = value' } + + | _ -> Fail "OpSem_stack_value not given an element on stack" + ) + | (OpSem_call_frame_cfa, []) -> + let row = (find_cfa_table_row_for_pc evaluated_frame_info1 pc) in + (match row.ctr_cfa with + | CR_undefined -> + failwith "evaluate_cfa of CR_undefined" + | CR_register( r, i) -> + bregxi r i (* same behaviour as an OpSem_bregx *) + | CR_expression bs -> + failwith "CR_expression" + (*TODO: fix result type - not this evaluate_location_description_bytes c dloc evaluated_frame_info cuh ac ev mfbloc pc bs*) + (* TODO: restrict allowed OpSem_* in that recursive call *) + ) + | (_, _) -> + Fail ("bad OpSem invocation: op=" ^ (pp_operation op ^ (" arguments=" ^ myconcat "" (Lem_list.map pp_operation_argument_value op.op_argument_values)))) + )) + in + (match es' with + | Success s' -> + evaluate_operation_list c dloc evaluated_frame_info1 cuh ac ev mfbloc pc s' ops' + | Fail e -> + Fail e + ) + )) + +and evaluate_location_description_bytes (c:p_context) (dloc: location_list_list) (evaluated_frame_info1: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: attribute_value option) (pc: Nat_big_num.num) (bs: char list) : single_location error= + (let parse_context1 = ({pc_bytes = bs; pc_offset =(Nat_big_num.of_int 0) }) in + (match parse_operations c cuh parse_context1 with + | PR_fail( s, pc') -> Fail ("evaluate_location_description_bytes: parse_operations fail: " ^ pp_parse_fail s pc') + | PR_success( ops, pc') -> + if not ((listEqualBy (=) pc'.pc_bytes [])) then + Fail "evaluate_location_description_bytes: extra non-parsed bytes" + else + evaluate_operation_list c dloc evaluated_frame_info1 cuh ac ev mfbloc pc initial_state ops + )) + +and evaluate_location_description (c:p_context) (dloc: location_list_list) (evaluated_frame_info1: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: attribute_value option) (pc: Nat_big_num.num) (loc:attribute_value) : single_location error= + ((match loc with + | AV_exprloc( n, bs) -> + evaluate_location_description_bytes c dloc evaluated_frame_info1 cuh ac ev mfbloc pc bs + | AV_block( n, bs) -> + evaluate_location_description_bytes c dloc evaluated_frame_info1 cuh ac ev mfbloc pc bs + | AV_sec_offset n -> + let location_list1 = (find_location_list dloc n) in + let (offset,(llis: location_list_item list)) = location_list1 in + let f (lli:location_list_item) : single_location_description option= + ((match lli with + | LLI_lle lle -> + if Nat_big_num.greater_equal pc lle.lle_beginning_address_offset && Nat_big_num.less pc lle.lle_ending_address_offset then Some lle.lle_single_location_description else None + | LLI_base _ -> + None (* TODO: either refactor to do offset during parsing or update base offsets here. Should refactor to use "interpreted". *) + )) in + (match myfindmaybe f llis with + | Some bs -> + evaluate_location_description_bytes c dloc evaluated_frame_info1 cuh ac ev mfbloc pc bs + | None -> + Fail "evaluate_location_description didn't find pc in location list ranges" + ) + | _ -> Fail "evaluate_location_description av_location not understood" + )) + + + + + +(** ************************************************************ *) +(** **** evaluation of frame information ********************** *) +(** ************************************************************ *) + +(** register maps *) + +(*val rrp_update : register_rule_map -> cfa_register -> register_rule -> register_rule_map*) +let rrp_update rrp r rr:(Nat_big_num.num*register_rule)list= ((r,rr)::rrp) + +(*val rrp_lookup : cfa_register -> register_rule_map -> register_rule*) +let rrp_lookup r rrp:register_rule= + ((match (lookupBy Nat_big_num.equal r rrp) with + | Some rr -> rr + | None -> RR_undefined + )) + +(*val rrp_empty : register_rule_map*) +let rrp_empty:(cfa_register*register_rule)list= ([]) + + + +(** pp of evaluated cfa information from .debug_frame *) +(* readelf --debug-dump=frames-interp test/a.out + +Contents of the .eh_frame section: + +00000000 00000014 00000000 CIE "zR" cf=1 df=-8 ra=16 + LOC CFA ra +0000000000000000 rsp+8 c-8 + +00000018 00000024 0000001c FDE cie=00000000 pc=004003b0..004003d0 + LOC CFA ra +00000000004003b0 rsp+16 c-8 +00000000004003b6 rsp+24 c-8 +00000000004003c0 exp c-8 + +00000040 0000001c 00000044 FDE cie=00000000 pc=004004b4..004004ba + LOC CFA rbp ra +00000000004004b4 rsp+8 u c-8 +00000000004004b5 rsp+16 c-16 c-8 +00000000004004b8 rbp+16 c-16 c-8 +00000000004004b9 rsp+8 c-16 c-8 + +00000060 00000024 00000064 FDE cie=00000000 pc=004004c0..00400549 + LOC CFA rbx rbp r12 r13 r14 r15 ra +00000000004004c0 rsp+8 u u u u u u c-8 +00000000004004d1 rsp+8 u c-48 c-40 u u u c-8 +00000000004004f0 rsp+64 c-56 c-48 c-40 c-32 c-24 c-16 c-8 +0000000000400548 rsp+8 c-56 c-48 c-40 c-32 c-24 c-16 c-8 + +00000088 00000014 0000008c FDE cie=00000000 pc=00400550..00400552 + LOC CFA ra +0000000000400550 rsp+8 c-8 + +000000a0 ZERO terminator +*) + + + +(*val mytoList : forall 'a. SetType 'a => set 'a -> list 'a*) + +let register_footprint_rrp (rrp: register_rule_map) : cfa_register Pset.set= + (Pset.from_list Nat_big_num.compare (Lem_list.map fst rrp)) + +let register_footprint (rows: cfa_table_row list) : cfa_register list= + (Pset.elements (bigunionListMap + instance_Basic_classes_SetType_Num_natural_dict (fun row -> register_footprint_rrp row.ctr_regs) rows)) + + +(*val max_lengths : list (list string) -> list natural*) +let rec max_lengths xss:(Nat_big_num.num)list= + ((match xss with + | [] -> failwith "max_lengths" + | xs::xss' -> + let lens = (Lem_list.map (fun x -> Nat_big_num.of_int (String.length x)) xs) in + if (listEqualBy (listEqualBy (=)) xss' []) then lens + else + let lens' = (max_lengths xss') in + let z = (Lem_list.list_combine lens lens') in + let lens'' = (Lem_list.map (fun (l1,l2)-> Nat_big_num.max l1 l2) z) in + lens'' + )) + +let rec pad_row xs lens:(string)list= + ((match (xs,lens) with + | ([],[]) -> [] + | (x::xs', len::lens') -> right_space_padded_to len x :: pad_row xs' lens' + )) + +let pad_rows (xss : ( string list) list) : string= + (let lens = (max_lengths xss) in + myconcat "" (Lem_list.map (fun xs -> myconcat " " (pad_row xs lens) ^ "\n") xss)) + +let pp_evaluated_fde (fde1, (rows: cfa_table_row list)) : string= + (let regs = (register_footprint rows) in + let header : string list = ("LOC" :: ("CFA" :: Lem_list.map + (pp_cfa_register instance_Show_Show_Num_natural_dict) regs)) in + let ppd_rows : ( string list) list = + (Lem_list.map (fun row -> pphex row.ctr_loc :: (pp_cfa_rule row.ctr_cfa :: Lem_list.map (fun r -> pp_register_rule (rrp_lookup r row.ctr_regs)) regs)) rows) in + pad_rows (header :: ppd_rows)) + + + +(** evaluation of cfa information from .debug_frame *) + +let evaluate_call_frame_instruction (fi: frame_info) (cie1: cie) (state1: cfa_state) (cfi: call_frame_instruction) : cfa_state= + + (let create_row (loc: Nat_big_num.num)= + (let row = ({ state1.cs_current_row with ctr_loc = loc }) in + { state1 with cs_current_row = row; cs_previous_rows = (state1.cs_current_row::state1.cs_previous_rows) }) in + + let update_cfa (cr:cfa_rule)= + (let row = ({ state1.cs_current_row with ctr_cfa = cr }) in + { state1 with cs_current_row = row }) in + + let update_reg r rr= + (let row = ({ state1.cs_current_row with ctr_regs = (rrp_update state1.cs_current_row.ctr_regs r rr) }) in + { state1 with cs_current_row = row }) in + + (match cfi with + (* Row Creation Instructions *) + | DW_CFA_set_loc a -> + create_row a + | DW_CFA_advance_loc d -> + create_row ( Nat_big_num.add state1.cs_current_row.ctr_loc (Nat_big_num.mul d cie1.cie_code_alignment_factor)) + | DW_CFA_advance_loc1 d -> + create_row ( Nat_big_num.add state1.cs_current_row.ctr_loc (Nat_big_num.mul d cie1.cie_code_alignment_factor)) + | DW_CFA_advance_loc2 d -> + create_row ( Nat_big_num.add state1.cs_current_row.ctr_loc (Nat_big_num.mul d cie1.cie_code_alignment_factor)) + | DW_CFA_advance_loc4 d -> + create_row ( Nat_big_num.add state1.cs_current_row.ctr_loc (Nat_big_num.mul d cie1.cie_code_alignment_factor)) + + (* CFA Definition Instructions *) + | DW_CFA_def_cfa( r, n) -> + update_cfa (CR_register( r, ( n))) + | DW_CFA_def_cfa_sf( r, i) -> + update_cfa (CR_register( r, ( Nat_big_num.mul i cie1.cie_data_alignment_factor))) + | DW_CFA_def_cfa_register r -> + (match state1.cs_current_row.ctr_cfa with + | CR_register( r', i) -> + update_cfa (CR_register( r, i)) + | _ -> failwith "DW_CFA_def_cfa_register: current rule is not CR_register" + ) + | DW_CFA_def_cfa_offset n -> + (match state1.cs_current_row.ctr_cfa with + | CR_register( r, i) -> + update_cfa (CR_register( r, ( n))) + | _ -> failwith "DW_CFA_def_cfa_offset: current rule is not CR_register" + ) + | DW_CFA_def_cfa_offset_sf i -> + (match state1.cs_current_row.ctr_cfa with + | CR_register( r, i') -> + update_cfa (CR_register( r, ( Nat_big_num.mul i' cie1.cie_data_alignment_factor))) + | _ -> failwith "DW_CFA_def_cfa_offset_sf: current rule is not CR_register" + ) + | DW_CFA_def_cfa_expression b -> + update_cfa (CR_expression b) + + (* Register Rule Instrutions *) + | DW_CFA_undefined r -> + update_reg r (RR_undefined) + | DW_CFA_same_value r -> + update_reg r (RR_same_value) + | DW_CFA_offset( r, n) -> + update_reg r (RR_offset ( Nat_big_num.mul( n) cie1.cie_data_alignment_factor)) + | DW_CFA_offset_extended( r, n) -> + update_reg r (RR_offset ( Nat_big_num.mul( n) cie1.cie_data_alignment_factor)) + | DW_CFA_offset_extended_sf( r, i) -> + update_reg r (RR_offset ( Nat_big_num.mul i cie1.cie_data_alignment_factor)) + | DW_CFA_val_offset( r, n) -> + update_reg r (RR_val_offset ( Nat_big_num.mul( n) cie1.cie_data_alignment_factor)) + | DW_CFA_val_offset_sf( r, i) -> + update_reg r (RR_val_offset ( Nat_big_num.mul i cie1.cie_data_alignment_factor)) + | DW_CFA_register( r1, r2) -> + update_reg r1 (RR_register r2) + | DW_CFA_expression( r, b) -> + update_reg r (RR_expression b) + | DW_CFA_val_expression( r, b) -> + update_reg r (RR_val_expression b) + | DW_CFA_restore r -> + update_reg r (rrp_lookup r state1.cs_initial_instructions_row.ctr_regs) +(* RR_undefined if the lookup fails? *) + | DW_CFA_restore_extended r -> + update_reg r (rrp_lookup r state1.cs_initial_instructions_row.ctr_regs) + +(* Row State Instructions *) +(* do these also push and restore the CFA rule? *) + | DW_CFA_remember_state -> + { state1 with cs_row_stack = (state1.cs_current_row :: state1.cs_row_stack) } + | DW_CFA_restore_state -> + (match state1.cs_row_stack with + | r::rs -> { state1 with cs_current_row = r; cs_row_stack = rs } + | [] -> failwith "DW_CFA_restore_state: empty row stack" + ) +(* Padding Instruction *) + | DW_CFA_nop -> + state1 + +(* Unknown *) + | DW_CFA_unknown b -> + failwith ("evaluate_call_frame_instruction: DW_CFA_unknown " ^ hex_string_of_byte b) + + )) + + + +let rec evaluate_call_frame_instructions (fi: frame_info) (cie1: cie) (state1: cfa_state) (cfis: call_frame_instruction list) : cfa_state= + ((match cfis with + | [] -> state1 + | cfi::cfis' -> + let state' = (evaluate_call_frame_instruction fi cie1 state1 cfi) in + evaluate_call_frame_instructions fi cie1 state' cfis' + )) + + +let evaluate_fde (fi: frame_info) (fde1:fde) : cfa_table_row list= + (let cie1 = (find_cie fi fde1.fde_cie_pointer) in + let final_location = (Nat_big_num.add fde1.fde_initial_location_address fde1.fde_address_range) in + let initial_cfa_state = + (let initial_row = + ({ + ctr_loc = (fde1.fde_initial_location_address); + ctr_cfa = CR_undefined; + ctr_regs = rrp_empty; + }) in + { + cs_current_row = initial_row; + cs_previous_rows = ([]); + cs_initial_instructions_row = initial_row; + cs_row_stack = ([]); + }) + in + let state' = + (evaluate_call_frame_instructions fi cie1 initial_cfa_state cie1.cie_initial_instructions) in + let initial_row' = (state'.cs_current_row) in + let state'' = ({ initial_cfa_state with cs_current_row = initial_row'; cs_initial_instructions_row = initial_row' }) in + let state''' = + (evaluate_call_frame_instructions fi cie1 (*final_location*) state'' fde1.fde_instructions) in + List.rev (state'''.cs_current_row:: state'''.cs_previous_rows)) + + + +(*val evaluate_frame_info : dwarf -> evaluated_frame_info*) +let evaluate_frame_info (d: dwarf) : evaluated_frame_info= + (Lem_list.mapMaybe (fun fie -> (match fie with FIE_fde fde1 -> Some (fde1, (evaluate_fde d.d_frame_info fde1)) | FIE_cie _ -> None )) d.d_frame_info) + +let pp_evaluated_frame_info (efi: evaluated_frame_info):string= + (myconcat "\n" (Lem_list.map pp_evaluated_fde efi)) + + + +(** ************************************************************ *) +(** ** analysis of location and frame data for reverse mapping *) +(** ************************************************************ *) + +(** analysis *) + +(*val find_dies_in_die : (die->bool) -> compilation_unit -> list die -> die -> list (compilation_unit * (list die) * die)*) +let rec find_dies_in_die (p:die->bool) (cu:compilation_unit) (parents: die list) (d: die):(compilation_unit*(die)list*die)list= + (let ds = (List.concat (map (find_dies_in_die p cu (d::parents)) d.die_children)) in + if p d then (cu,parents,d)::ds else ds) + +let find_dies (p:die->bool) (d: dwarf) : (compilation_unit * ( die list) * die) list= + (List.concat (map (fun cu -> find_dies_in_die p cu [] cu.cu_die) d.d_compilation_units)) + + +(** simple-minded analysis of location *) + +let analyse_locations_raw c (d: dwarf):string= + + (let (cuh_default : compilation_unit_header) = (let cu = (myhead d.d_compilation_units) in cu.cu_header) in + + (* find all DW_TAG_variable and DW_TAG_formal_parameter dies with a DW_AT_name attribute *) + let tags = (Lem_list.map tag_encode ["DW_TAG_variable"; "DW_TAG_formal_parameter"]) in + let dies : (compilation_unit * ( die list) * die) list = + (find_dies + (fun die1 -> + Lem_list.elem + instance_Basic_classes_Eq_Num_natural_dict die1.die_abbreviation_declaration.ad_tag tags + && has_attribute "DW_AT_name" die1) + d) in + + myconcat "" + (Lem_list.map + (fun (cu,parents,die1) -> + + let ats = (Lem_list.list_combine + die1.die_abbreviation_declaration.ad_attribute_specifications + die1.die_attribute_values) in + + let find_ats (s:string)= (myfindNonPure (fun (((at: Nat_big_num.num), (af: Nat_big_num.num)), ((pos: Nat_big_num.num),(av:attribute_value))) -> Nat_big_num.equal (attribute_encode s) at) ats) in + + let ((_,_),(_,av_name)) = (find_ats "DW_AT_name") in + + let name1 = + ((match av_name with + | AV_string bs -> string_of_bytes bs + | AV_strp n -> pp_debug_str_entry d.d_str n + | _ -> "av_name AV not understood" + )) in + + + let ((_,_),(_,av_location)) = (find_ats "DW_AT_location") in + + let ppd_location = + ((match av_location with + | AV_exprloc( n, bs) -> " "^(parse_and_pp_operations c cuh_default bs^"\n") + | AV_block( n, bs) -> " "^(parse_and_pp_operations c cuh_default bs^"\n") + | AV_sec_offset n -> + let location_list1 = (myfindNonPure (fun (n',_)->Nat_big_num.equal n' n) d.d_loc) in + pp_location_list c cuh_default location_list1 + | _ -> "av_location AV not understood" + )) in + + pp_tag_encoding die1.die_abbreviation_declaration.ad_tag ^ (" " ^ (name1 ^ (":\n" ^ (ppd_location ^ "\n")))) ) + + dies)) + + +(** more proper analysis of locations *) + +(* TODO: handle this: +In a variable entry representing the definition of a variable (that is, with no +DW_AT_declaration attribute) if no location attribute is present, or if the location attribute is +present but has an empty location description (as described in Section 2.6), the variable is +assumed to exist in the source code but not in the executable program (but see number 10, +below). +In a variable entry representing a non-defining declaration of a variable, the location +specified modifies the location specified by the defining declaration and only applies for the +scope of the variable entry; if no location is specified, then the location specified in the +defining declaration applies. +The location of a variable may be further specified with a DW_AT_segment attribute, if +appropriate. +*) + + +(* +if there's a DW_AT_location that's a location list (DW_FORM_sec_offset/AV_sec_offset) : use that for both the range(s) and location; interpret the range(s) wrt the applicable base address of the compilation unit + +if there's a DW_AT_location that's a location expression (DW_FORM_exprloc/AV_exprloc or DW_block/AV_block), look for the closest enclosing range: + - DW_AT_low_pc (AV_addr) and no DW_AT_high_pc or DW_AT_ranges: just the singleton address + - DW_AT_low_pc (AV_addr) and DW_AT_high_pc (either an absolute AV_addr or an offset AV_constantN/AV_constant_SLEB128/AV_constantULEB128) : that range + - DW_AT_ranges (DW_FORM_sec_offset/AV_sec_offset) : get a range list from .debug_ranges; interpret wrt the applicable base address of the compilation unit + - for compilation units: a DW_AT_ranges together with a DW_AT_low_pc to specify the default base address to use in interpeting location and range lists + +DW_OP_fbreg in location expressions evaluate the DW_AT_frame_base of +the closest enclosing function - which is either a location expression +or a location list (what happens if the ranges of that location list +don't cover where we are?) + +For each variable and formal parameter that has a DW_AT_name, we'll calculate a list of pairs of a concrete (low,high) range and a location expression. +*) + +let rec closest_enclosing_range c (dranges: range_list_list) (cu_base_address1: Nat_big_num.num) (parents: die list) : ( (Nat_big_num.num * Nat_big_num.num)list)option= + ((match parents with + | [] -> None + | die1::parents' -> + (match (find_attribute_value "DW_AT_low_pc" die1, find_attribute_value "DW_AT_high_pc" die1, find_attribute_value "DW_AT_ranges" die1) with + | (Some (AV_addr n), None, None ) -> Some [(n,Nat_big_num.add n(Nat_big_num.of_int 1))] (* unclear if this case is used? *) + | (Some (AV_addr n1), Some (AV_addr n2), None ) -> Some [(n1,n2)] + | (Some (AV_addr n1), Some (AV_constant_ULEB128 n2), None ) -> Some [(n1,Nat_big_num.add n1 n2)] (* should be mod all? *) + | (Some (AV_addr n1), Some (AV_constant_SLEB128 i2), None ) -> Some [(n1, Nat_big_num.abs ( Nat_big_num.add( n1) i2))] (* should + be mod all? *) + | (Some (AV_addr n1), Some (AV_constantN( _, _)), None ) -> failwith "AV_constantN in closest_enclosing_range" + + | (Some (AV_addr n1), Some (AV_block( n, bs)), None ) -> let n2 = (natural_of_bytes c.endianness bs) in Some [(n1,Nat_big_num.add n1 n2)] (* should be mod all? *) (* signed or unsigned interp? *) + + | (_, None, Some (AV_sec_offset n)) -> + let rlis = (snd (find_range_list dranges n)) in + let nns = (interpret_range_list cu_base_address1 rlis) in + Some nns + | (None, None, None ) -> closest_enclosing_range c dranges cu_base_address1 parents' + | (_, _, _ ) -> Some [] (*Assert_extra.failwith "unexpected attribute values in closest_enclosing_range"*) + ) + )) + +(* +If one of the DW_FORM_data<n> forms is used to represent a signed or unsigned integer, it +can be hard for a consumer to discover the context necessary to determine which +interpretation is intended. Producers are therefore strongly encouraged to use +DW_FORM_sdata or DW_FORM_udata for signed and unsigned integers respectively, +rather than DW_FORM_data<n>. +no kidding - if we get an AV_constantN for DW_AT_high_pc, should it be interpreted as signed or unsigned? *) + + +let rec closest_enclosing_frame_base dloc (base_address1: Nat_big_num.num) (parents: die list) : attribute_value option= + ((match parents with + | [] -> None + | die1::parents' -> + (match find_attribute_value "DW_AT_frame_base" die1 with + | Some av -> Some av + | None -> closest_enclosing_frame_base dloc base_address1 parents' + ) + )) + + + + +let interpreted_location_of_die c cuh (dloc: location_list_list) (dranges: range_list_list) (base_address1: Nat_big_num.num) (parents: die list) (die1: die) : ( (Nat_big_num.num * Nat_big_num.num * single_location_description)list)option= +( + + (* for a simple location expression bs, we look in the enclosing die + tree to find the associated pc range *)let location bs= + ((match closest_enclosing_range c dranges base_address1 (die1::parents) with + | Some nns -> + Some (Lem_list.map (fun (n1,n2) -> (n1,n2,bs)) nns) + | None -> + (* if there is no such range, we take the full 0 - 0xfff.fff range*) + Some [(Nat_big_num.of_int 0,(arithmetic_context_of_cuh cuh).ac_max,bs)] + )) in + + (match find_attribute_value "DW_AT_location" die1 with + | Some (AV_exprloc( n, bs)) -> location bs + | Some (AV_block( n, bs)) -> location bs + (* while for a location list, we take the associated pc range from + each element of the list *) + | Some (AV_sec_offset n) -> + let (_,llis) = (find_location_list dloc n) in + Some (interpret_location_list base_address1 llis) + | None -> None + )) + + +let cu_base_address cu:Nat_big_num.num= + ((match find_attribute_value "DW_AT_low_pc" cu.cu_die with + | Some (AV_addr n) -> n + | _ ->Nat_big_num.of_int 0 (*Nothing*) (*Assert_extra.failwith "no cu DW_AT_low_pc"*) + )) + + +(*val analyse_locations : dwarf -> analysed_location_data*) +let analyse_locations (d: dwarf) : analysed_location_data= + + (let c : p_context = ({ endianness = (d.d_endianness) }) in + + let (cuh_default : compilation_unit_header) = (let cu = (myhead d.d_compilation_units) in cu.cu_header) in + + (* find all DW_TAG_variable and DW_TAG_formal_parameter dies with a DW_AT_name and DW_AT_location attribute *) + let tags = (Lem_list.map tag_encode ["DW_TAG_variable"; "DW_TAG_formal_parameter"]) in + let dies : (compilation_unit * ( die list) * die) list = + (find_dies + (fun die1 -> + Lem_list.elem + instance_Basic_classes_Eq_Num_natural_dict die1.die_abbreviation_declaration.ad_tag tags + && (has_attribute "DW_AT_name" die1 + && has_attribute "DW_AT_location" die1)) + d) in + + Lem_list.map + (fun ((((cu:compilation_unit), (parents: die list), (die1: die)) as x)) -> + let base_address1 = (cu_base_address cu) in + let interpreted_locations : ( (Nat_big_num.num * Nat_big_num.num * single_location_description)list)option = + (interpreted_location_of_die c cuh_default d.d_loc d.d_ranges base_address1 parents die1) in + (x,interpreted_locations) + ) + dies) + + + +let pp_analysed_locations1 c cuh (nnls: (Nat_big_num.num * Nat_big_num.num * single_location_description) list) : string= + (myconcat "" + (Lem_list.map + (fun (n1,n2,bs) -> " " ^ (pphex n1 ^ (" " ^ (pphex n2 ^ (" " ^ (parse_and_pp_operations c cuh bs ^ "\n")))))) + nnls)) + +let pp_analysed_locations2 c cuh mnnls:string= + ((match mnnls with + | Some nnls -> pp_analysed_locations1 c cuh nnls + | None -> " <no locations>\n" + )) + +let pp_analysed_locations3 c cuh str (als: analysed_location_data) : string= + (myconcat "\n" + (Lem_list.map + (fun ((cu,parents,die1),mnnls) -> + pp_die_abbrev c cuh str(Nat_big_num.of_int 0) false parents die1 + ^ pp_analysed_locations2 c cuh mnnls + ) + als + )) + +let pp_analysed_location_data (d: dwarf) (als: analysed_location_data) : string= + (let c : p_context = ({ endianness = (d.d_endianness) }) in + let (cuh_default : compilation_unit_header) = (let cu = (myhead d.d_compilation_units) in cu.cu_header) in + pp_analysed_locations3 c (*HACK*) cuh_default d.d_str als) + + + +let pp_analysed_location_data_at_pc (d: dwarf) (alspc: analysed_location_data_at_pc) : string= + (myconcat "" (Lem_list.map + (fun ((cu,parents,die1),(n1,n2,sld,esl)) -> + " " ^ + (let name1 = + ((match find_name_of_die d.d_str die1 with + | Some s -> s + | None -> "<no name>\n" + )) in + (match esl with + | Success sl -> + name1 ^ (" @ " ^ (pp_single_location sl ^"\n")) + + | Fail e -> name1 ^ (" @ " ^ ("<fail: " ^ (e ^ ">\n"))) + )) + ) + alspc)) + + +(*val analysed_locations_at_pc : evaluation_context -> dwarf_static -> natural -> analysed_location_data_at_pc*) +let analysed_locations_at_pc + (ev) + (ds: dwarf_static) + (pc: Nat_big_num.num) + : analysed_location_data_at_pc= + +(let c : p_context = ({ endianness = (ds.ds_dwarf.d_endianness) }) in + + let xs = + (Lem_list.mapMaybe + (fun (cupd,mnns) -> + (match mnns with + | None -> None + | Some nns -> + let nns' = (List.filter (fun (n1,n2,sld) -> Nat_big_num.greater_equal pc n1 && Nat_big_num.less pc n2) nns) in + (match nns' with + | [] -> None + | _ -> Some (cupd,nns') + ) + )) + ds.ds_analysed_location_data) +in + +List.concat + (Lem_list.map + (fun ((cu,parents,die1),nns) -> + let ac = (arithmetic_context_of_cuh cu.cu_header) in + let base_address1 = (cu_base_address cu) in + let mfbloc : attribute_value option = + (closest_enclosing_frame_base ds.ds_dwarf.d_loc base_address1 parents) in + Lem_list.map + (fun (n1,n2,sld) -> + let el : single_location error = + (evaluate_location_description_bytes c ds.ds_dwarf.d_loc ds.ds_evaluated_frame_info cu.cu_header ac ev mfbloc pc sld) in + ((cu,parents,die1),(n1,n2,sld,el)) + ) + nns + ) + xs)) + +(*val names_of_address : dwarf -> analysed_location_data_at_pc -> natural -> list string*) +let names_of_address + (d: dwarf) + (alspc: analysed_location_data_at_pc) + (address: Nat_big_num.num) + : string list= + +(Lem_list.mapMaybe + (fun ((cu,parents,die1),(n1,n2,sld,esl)) -> + (match esl with + | Success (SL_simple (SL_memory_address a)) -> + if Nat_big_num.equal a address then + (match find_name_of_die d.d_str die1 with + | Some s -> Some s + | None -> None + ) + else + None + | Success _ -> None (* just suppress? *) + | Fail e -> None (* just suppress? *) + ) + ) + alspc) + + +(** ************************************************************ *) +(** ** evaluation of line-number info *) +(** ************************************************************ *) + +let initial_line_number_registers (lnh: line_number_header) : line_number_registers= + ({ + lnr_address =(Nat_big_num.of_int 0); + lnr_op_index =(Nat_big_num.of_int 0); + lnr_file =(Nat_big_num.of_int 1); + lnr_line =(Nat_big_num.of_int 1); + lnr_column =(Nat_big_num.of_int 0); + lnr_is_stmt = (lnh.lnh_default_is_stmt); + lnr_basic_block = false; + lnr_end_sequence = false; + lnr_prologue_end = false; + lnr_epilogue_begin = false; + lnr_isa =(Nat_big_num.of_int 0); + lnr_discriminator =(Nat_big_num.of_int 0); + }) + +let evaluate_line_number_operation + (lnh: line_number_header) + ((s: line_number_registers), (lnrs: line_number_registers list)) + (lno: line_number_operation) + : line_number_registers * line_number_registers list= + + (let new_address s operation_advance= (Nat_big_num.add s.lnr_address (Nat_big_num.mul + lnh.lnh_minimum_instruction_length + (Nat_big_num.div( Nat_big_num.add s.lnr_op_index operation_advance)lnh.lnh_maximum_operations_per_instruction))) in + let new_op_index s operation_advance= (Nat_big_num.modulus + ( Nat_big_num.add s.lnr_op_index operation_advance) lnh.lnh_maximum_operations_per_instruction) in + + (match lno with + | DW_LN_special adjusted_opcode -> + let operation_advance = (Nat_big_num.div adjusted_opcode lnh.lnh_line_range) in + let line_increment = (Nat_big_num.add lnh.lnh_line_base (( Nat_big_num.modulus adjusted_opcode lnh.lnh_line_range))) in + let s' = + ({ s with + lnr_line = (partialNaturalFromInteger ( Nat_big_num.add( s.lnr_line) line_increment)); + lnr_address = (new_address s operation_advance); + lnr_op_index = (new_op_index s operation_advance); + }) in + let lnrs' = (s'::lnrs) in + let s'' = +({ s' with + lnr_basic_block = false; + lnr_prologue_end = false; + lnr_epilogue_begin = false; + lnr_discriminator =(Nat_big_num.of_int 0); + }) in + (s'', lnrs') + | DW_LNS_copy -> + let lnrs' = (s::lnrs) in + let s' = +({ s with + lnr_basic_block = false; + lnr_prologue_end = false; + lnr_epilogue_begin = false; + lnr_discriminator =(Nat_big_num.of_int 0); + }) in + (s', lnrs') + | DW_LNS_advance_pc operation_advance -> + let s' = + ({ s with + lnr_address = (new_address s operation_advance); + lnr_op_index = (new_op_index s operation_advance); + }) in + (s', lnrs) + | DW_LNS_advance_line line_increment -> + let s' = ({ s with lnr_line = (partialNaturalFromInteger ( Nat_big_num.add( s.lnr_line) line_increment)) }) in (s', lnrs) + | DW_LNS_set_file n -> + let s' = ({ s with lnr_file = n }) in (s', lnrs) + | DW_LNS_set_column n -> + let s' = ({ s with lnr_column = n }) in (s', lnrs) + | DW_LNS_negate_stmt -> + let s' = ({ s with lnr_is_stmt = (not s.lnr_is_stmt) }) in (s', lnrs) + | DW_LNS_set_basic_block -> + let s' = ({ s with lnr_basic_block = true }) in (s', lnrs) + | DW_LNS_const_add_pc -> + let opcode =(Nat_big_num.of_int 255) in + let adjusted_opcode = (Nat_big_num.sub_nat opcode lnh.lnh_opcode_base) in + let operation_advance = (Nat_big_num.div adjusted_opcode lnh.lnh_line_range) in + let s' = + ({ s with + lnr_address = (new_address s operation_advance); + lnr_op_index = (new_op_index s operation_advance); + }) in + (s', lnrs) + | DW_LNS_fixed_advance_pc n -> + let s' = + ({ s with + lnr_address = (Nat_big_num.add s.lnr_address n); + lnr_op_index =(Nat_big_num.of_int 0); + }) in + (s', lnrs) + | DW_LNS_set_prologue_end -> + let s' = ({ s with lnr_prologue_end = true }) in (s', lnrs) + | DW_LNS_set_epilogue_begin -> + let s' = ({ s with lnr_epilogue_begin = true }) in (s', lnrs) + | DW_LNS_set_isa n -> + let s' = ({ s with lnr_isa = n }) in (s', lnrs) + | DW_LNE_end_sequence -> + let s' = ({ s with lnr_end_sequence = true }) in + let lnrs' = (s' :: lnrs) in + let s'' = (initial_line_number_registers lnh) in + (s'', lnrs') + | DW_LNE_set_address n -> + let s' = + ({ s with + lnr_address = n; + lnr_op_index =(Nat_big_num.of_int 0); + }) in + (s', lnrs) + | DW_LNE_define_file( s, n1, n2, n3) -> + failwith "DW_LNE_define_file not implemented" (*TODO: add to file list in header - but why is this in the spec? *) + | DW_LNE_set_discriminator n -> + let s' = ({ s with lnr_discriminator = n }) in (s', lnrs) + )) + +let rec evaluate_line_number_operations + (lnh: line_number_header) + ((s: line_number_registers), (lnrs: line_number_registers list)) + (lnos: line_number_operation list) + : line_number_registers * line_number_registers list= + ((match lnos with + | [] -> (s,lnrs) + | lno :: lnos' -> + let (s',lnrs') = + (evaluate_line_number_operation lnh (s,lnrs) lno) in + evaluate_line_number_operations lnh (s',lnrs') lnos' + )) + +let evaluate_line_number_program + (lnp:line_number_program) + : line_number_registers list= + (List.rev (snd (evaluate_line_number_operations lnp.lnp_header ((initial_line_number_registers lnp.lnp_header),[]) lnp.lnp_operations))) + + +let pp_line_number_registers lnr:string= + ("" + ^ ("address = " ^ (pphex lnr.lnr_address ^ ("\n" + ^ ("op_index = " ^ (Nat_big_num.to_string lnr.lnr_op_index ^ ("\n" + ^ ("file = " ^ (Nat_big_num.to_string lnr.lnr_file ^ ("\n" + ^ ("line = " ^ (Nat_big_num.to_string lnr.lnr_line ^ ("\n" + ^ ("column = " ^ (Nat_big_num.to_string lnr.lnr_column ^ ("\n" + ^ ("is_stmt = " ^ (string_of_bool lnr.lnr_is_stmt ^ ("\n" + ^ ("basic_block = " ^ (string_of_bool lnr.lnr_basic_block ^ ("\n" + ^ ("end_sequence = " ^ (string_of_bool lnr.lnr_end_sequence ^ ("\n" + ^ ("prologue_end = " ^ (string_of_bool lnr.lnr_prologue_end ^ ("\n" + ^ ("epilogue_begin = " ^ (string_of_bool lnr.lnr_epilogue_begin ^ ("\n" + ^ ("isa = " ^ (Nat_big_num.to_string lnr.lnr_isa ^ ("\n" + ^ ("discriminator = " ^ (pphex lnr.lnr_discriminator ^ "\n")))))))))))))))))))))))))))))))))))) + +let pp_line_number_registers_tight lnr : string list= + ([ + pphex lnr.lnr_address ; + Nat_big_num.to_string lnr.lnr_op_index ; + Nat_big_num.to_string lnr.lnr_file ; + Nat_big_num.to_string lnr.lnr_line ; + Nat_big_num.to_string lnr.lnr_column ; + string_of_bool lnr.lnr_is_stmt ; + string_of_bool lnr.lnr_basic_block ; + string_of_bool lnr.lnr_end_sequence ; + string_of_bool lnr.lnr_prologue_end ; + string_of_bool lnr.lnr_epilogue_begin ; + Nat_big_num.to_string lnr.lnr_isa ; + pphex lnr.lnr_discriminator + ]) + +let pp_line_number_registerss lnrs:string= + (pad_rows + ( + ["address"; "op_index"; "file"; "line"; "column"; "is_stmt"; "basic_block"; "end_sequence"; "prologue_end"; "epilogue_begin"; "isa"; "discriminator"] + :: + (Lem_list.map pp_line_number_registers_tight lnrs) + )) + +let pp_evaluated_line_info (eli: evaluated_line_info) : string= + (myconcat "\n" (Lem_list.map (fun (lnh,lnrs) -> pp_line_number_header lnh ^ ("\n" ^ pp_line_number_registerss lnrs)) eli)) + +(* readef example: +Decoded dump of debug contents of section .debug_line: + +CU: /var/local/stephen/work/devel/rsem/ppcmem2/system/tests-adhoc/simple-malloc/test-concurrent.c: +File name Line number Starting address +test-concurrent.c 11 0x400144 + +test-concurrent.c 12 0x40014c +test-concurrent.c 13 0x400154 +test-concurrent.c 14 0x400158 +test-concurrent.c 17 0x400160 + +/var/local/stephen/work/devel/rsem/ppcmem2/system/tests-adhoc/simple-malloc/../thread_start_aarch64.h: +thread_start_aarch64.h 34 0x400168 +thread_start_aarch64.h 36 0x400174 + +/var/local/stephen/work/devel/rsem/ppcmem2/system/tests-adhoc/simple-malloc/test-concurrent.c: +test-concurrent.c 19 0x400174 + +test-concurrent.c 20 0x40017c +test-concurrent.c 22 0x400180 + +CU: /var/local/stephen/work/devel/rsem/ppcmem2/system/tests-adhoc/simple-malloc/malloc.c: +... +*) + + +let source_lines_of_address (ds:dwarf_static) (a: Nat_big_num.num) : (string * Nat_big_num.num * line_number_registers) list= + (List.concat + (Lem_list.map + (fun (lnh, lnrs) -> + myfiltermaybe + (fun lnr -> + if Nat_big_num.equal a lnr.lnr_address && not lnr.lnr_end_sequence then + (match mynth ( Nat_big_num.sub_nat lnr.lnr_file(Nat_big_num.of_int 1)) lnh.lnh_file_names with + | Some lnfe -> + Some (string_of_bytes lnfe.lnfe_path, lnr.lnr_line, lnr) + | None -> + Some ("<source_lines_of_address: file entry not found>",Nat_big_num.of_int 0, lnr) + ) + else + None) + lnrs + ) + ds.ds_evaluated_line_info + )) + + +(** ************************************************************ *) +(** ** collecting all the statically calculated analysis info *) +(** ************************************************************ *) + +(*val extract_dwarf_static : elf_file -> maybe dwarf_static*) +let extract_dwarf_static f1:(dwarf_static)option= + ((match extract_dwarf f1 with + | None -> None + | Some dwarf1 -> + let _ = (my_debug5 (pp_dwarf dwarf1)) in + + let ald : analysed_location_data = + (analyse_locations dwarf1) in + let efi : evaluated_frame_info = + (evaluate_frame_info dwarf1) in + let eli : evaluated_line_info = + (Lem_list.map (fun lnp -> (lnp.lnp_header, evaluate_line_number_program lnp)) dwarf1.d_line_info) in + let ds = + ({ + ds_dwarf = dwarf1; + ds_analysed_location_data = ald; + ds_evaluated_frame_info = efi; + ds_evaluated_line_info = eli; + }) in + Some ds + )) + + + + +(** ************************************************************ *) +(** ** top level for main_elf ******************************** *) +(** ************************************************************ *) + +(*val harness_string_of_elf : elf_file -> byte_sequence -> string*) +let harness_string_of_elf f1 bs:string= + (let mds = (extract_dwarf_static f1) in + (match mds with + | None -> "<no dwarf information extracted>" + | Some ds -> + pp_dwarf ds.ds_dwarf + (* ^ analyse_locations_raw c d *) + ^ ("************** evaluation of frame data *************************\n" + ^ (pp_evaluated_frame_info ds.ds_evaluated_frame_info + ^ ("************** analysis of location data *************************\n" + ^ (pp_analysed_location_data ds.ds_dwarf ds.ds_analysed_location_data + ^ ("************** line info *************************\n" + ^ pp_evaluated_line_info ds.ds_evaluated_line_info))))) + )) + + +(*val harness_string_of_elf64_debug_info_section : elf64_file -> byte_sequence -> (*(natural -> string) -> (natural -> string) -> (natural -> string) -> elf64_header -> elf64_section_header_table -> string_table -> *) string*) +let harness_string_of_elf64_debug_info_section f1 bs0:string= + ( (*os proc usr hdr sht stbl*)harness_string_of_elf (ELF_File_64 f1) bs0) + +(*val harness_string_of_elf32_debug_info_section : elf32_file -> byte_sequence -> (* (natural -> string) -> (natural -> string) -> (natural -> string) -> elf32_header -> elf32_section_header_table -> string_table ->*) string*) +let harness_string_of_elf32_debug_info_section f1 bs0:string= + ( (*os proc usr hdr sht stbl*)harness_string_of_elf (ELF_File_32 f1) bs0) + |