diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/dwarf.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/dwarf.ml | 4619 |
1 files changed, 0 insertions, 4619 deletions
diff --git a/lib/ocaml_rts/linksem/dwarf.ml b/lib/ocaml_rts/linksem/dwarf.ml deleted file mode 100644 index 9e5a31aa..00000000 --- a/lib/ocaml_rts/linksem/dwarf.ml +++ /dev/null @@ -1,4619 +0,0 @@ -(*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) - |