path: root/lib/ocaml_rts/linksem/dwarf.ml

(*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)