summaryrefslogtreecommitdiff
path: root/lib/ocaml_rts/linksem/dwarf.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2018-01-18 18:16:45 +0000
committerAlasdair Armstrong2018-01-18 18:31:26 +0000
commit0fa42d315e20f819af93c2a822ab1bc032dc4535 (patch)
tree7ef4ea3444ba5938457e7c852f9ad9957055fe41 /lib/ocaml_rts/linksem/dwarf.ml
parent24dc13511053ab79ccb66ae24e3b8ffb9cad0690 (diff)
Modified ocaml backend to use ocamlfind for linksem and lem
Fixed test cases for ocaml backend and interpreter
Diffstat (limited to 'lib/ocaml_rts/linksem/dwarf.ml')
-rw-r--r--lib/ocaml_rts/linksem/dwarf.ml4619
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)
-
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 16:54:11 +0000