diff --git a/.gitignore b/.gitignore index 80f86a0..1b49b53 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,7 @@ src/**/*.ml !src/utility.ml !src/uint32_wrapper.ml !src/uint64_wrapper.ml +!src/sym_ocaml.ml !src/ml_bindings.ml !src/byte_sequence_wrapper.ml !src/filesystem_wrapper.ml @@ -30,3 +31,7 @@ src/build_num src/build_zarith src/_build src/byte_sequence_impl.lem + +_opam + +.vscode diff --git a/src/abis/aarch64/abi_aarch64_symbolic_relocation.lem b/src/abis/aarch64/abi_aarch64_symbolic_relocation.lem new file mode 100644 index 0000000..d5e23e4 --- /dev/null +++ b/src/abis/aarch64/abi_aarch64_symbolic_relocation.lem @@ -0,0 +1,182 @@ +open import Missing_pervasives +open import Error +open import Maybe + +open import Num +open import Basic_classes +open import String + +open import Elf_types_native_uint +open import Elf_file +open import Elf_header +open import Elf_relocation +open import Elf_symbolic + +open import Abi_aarch64_relocation +open import Abi_utilities +open import Abi_symbolic_relocation + +type aarch64_relocation_target + = Data64 + | Data32 + | ADRP + | ADD + | LDST of int + | CALL + | CONDBR + | B + +val abi_aarch64_apply_relocation_symbolic : relocation_spec aarch64_relocation_target +let abi_aarch64_apply_relocation_symbolic rel_type = + (** No width, no calculation *) + if rel_type = r_aarch64_none then + return Nothing + (** No width, no calculation *) + else if rel_type = r_aarch64_withdrawn then + return Nothing + (** Signed 64 bit width, calculation: S + A *) + else if rel_type = r_aarch64_abs64 then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [] + ; rel_desc_mask = (63, 0) + ; rel_desc_target = Data64 + |> + ) + (** Signed 32 bit width, calculation: S + A *) + else if rel_type = r_aarch64_abs32 then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Overflow (~(2**31), 2**32)] + ; rel_desc_mask = (31, 0) + ; rel_desc_target = Data32 + |> + ) + (** Signed 64 bit width, calculation: S + A - P *) + else if rel_type = r_aarch64_prel64 then + let result = Minus(Plus(Lift S, Lift A), Lift P) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [] + ; rel_desc_mask = (63, 0) + ; rel_desc_target = Data64 + |> + ) + (** Signed 32 bit width, calculation: S + A - P *) + else if rel_type = r_aarch64_prel32 then + let result = Minus(Plus(Lift S, Lift A), Lift P) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Overflow (~(2**31), 2**32)] + ; rel_desc_mask = (31, 0) + ; rel_desc_target = Data32 + |> + ) + else if rel_type = r_aarch64_adr_prel_pg_hi21 then + let result = Minus(Apply(Page, Plus(Lift S, Lift A)), Apply(Page, Lift P)) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Overflow (~(2**32), 2**32)] + ; rel_desc_mask = (32, 12) + ; rel_desc_target = ADRP + |> + ) + else if rel_type = r_aarch64_add_abs_lo12_nc then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [] + ; rel_desc_mask = (11, 0) + ; rel_desc_target = ADD + |> + ) + else if rel_type = r_aarch64_ldst8_abs_lo12_nc then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [] + ; rel_desc_mask = (11, 0) + ; rel_desc_target = LDST 0 + |> + ) + else if rel_type = r_aarch64_ldst16_abs_lo12_nc then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Alignment 1] + ; rel_desc_mask = (11, 1) + ; rel_desc_target = LDST 1 + |> + ) + else if rel_type = r_aarch64_ldst32_abs_lo12_nc then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Alignment 2] + ; rel_desc_mask = (11, 2) + ; rel_desc_target = LDST 2 + |> + ) + else if rel_type = r_aarch64_ldst64_abs_lo12_nc then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Alignment 3] + ; rel_desc_mask = (11, 3) + ; rel_desc_target = LDST 3 + |> + ) + else if rel_type = r_aarch64_ldst128_abs_lo12_nc then + let result = Plus(Lift S, Lift A) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Alignment 4] + ; rel_desc_mask = (11, 4) + ; rel_desc_target = LDST 4 + |> + ) + else if rel_type = r_aarch64_call26 then + let result = Minus(Plus(Lift S, Lift A), Lift P) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Overflow (~(2**27), 2**27); Alignment 2] + ; rel_desc_mask = (27, 2) + ; rel_desc_target = CALL + |> + ) + else if rel_type = r_aarch64_condbr19 then + let result = Minus(Plus(Lift S, Lift A), Lift P) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Overflow (~(2**20), 2**20); Alignment 2] + ; rel_desc_mask = (20, 2) + ; rel_desc_target = CONDBR + |> + ) + else if rel_type = r_aarch64_jump26 then + let result = Minus(Plus(Lift S, Lift A), Lift P) in + return (Just + <| rel_desc_value = result + ; rel_desc_checks = [Overflow (~(2**27), 2**27); Alignment 2] + ; rel_desc_mask = (27, 2) + ; rel_desc_target = B + |> + ) + else + fail ("Unsupported AARCH64 relocation type " ^ (string_of_aarch64_relocation_type rel_type)) + +let aarch64_relocation_target_to_data_target = function + | Data32 -> return Elf_symbolic.Data32 + | Data64 -> return Elf_symbolic.Data64 + | _ -> fail "Not a data relocation" +end + +let aarch64_relocation_interpreter = + abi_relocation_interpreter abi_aarch64_apply_relocation_symbolic + +let aarch64_data_relocation_interpreter = + relocation_interpreter_map_target + aarch64_relocation_interpreter + aarch64_relocation_target_to_data_target diff --git a/src/abis/abi_symbolic_relocation.lem b/src/abis/abi_symbolic_relocation.lem new file mode 100644 index 0000000..556df76 --- /dev/null +++ b/src/abis/abi_symbolic_relocation.lem @@ -0,0 +1,77 @@ +open import Num +open import Maybe +open import Bool +open import Basic_classes +open import String + +open import Error + +open import Abi_utilities + +open import Elf_types_native_uint +open import Elf_symbol_table +open import Elf_symbolic +open import Elf_relocation +open import Elf_file +open import Elf_header +open import Elf_section_header_table +open import Elf_interpreted_section + +type relocation_param = S | A | P + +let rec eval_op_exp s_val a_val p_val op: error symbolic_expression = + let f = eval_op_exp s_val a_val p_val in + match op with + | Lift S -> return s_val + | Lift A -> return a_val + | Lift P -> return p_val + | Plus (x, y) -> + f x >>= fun a -> + f y >>= fun b -> + return (BinOp (a, Add, b)) + | Minus (x, y) -> + f x >>= fun a -> + f y >>= fun b -> + return (BinOp (a, Sub, b)) + | Apply(Page, x) -> + f x >>= fun a -> + return (BinOp (a, And, UnOp (Not, Const 4095 (*0xFFF*)))) + | _ -> fail "Not supported" + end + +let eval_relocation s_val a_val p_val desc= + eval_op_exp s_val a_val p_val desc.rel_desc_value >>= fun value -> + return <| rel_desc_value = value + ; rel_desc_checks = desc.rel_desc_checks + ; rel_desc_mask = desc.rel_desc_mask + ; rel_desc_target = desc.rel_desc_target + |> + +type relocation_spec 'a = natural -> error (maybe (relocation_description (relocation_operator_expression relocation_param) 'a)) + +let relocation_spec_map_target f spec rel_type = + spec rel_type >>= function + | Nothing -> return Nothing + | Just desc -> return (Just (relocation_map_target f desc)) + end + +val abi_relocation_interpreter : forall 'a. relocation_spec 'a -> relocation_interpreter 'a +let abi_relocation_interpreter spec ef symtab sidx rel = + if is_elf64_relocatable_file ef.elf64_file_header then + section_with_offset ef sidx rel.elf64_ra_offset >>= fun p_val -> + let (rel_type, sym) = parse_elf64_relocation_info rel.elf64_ra_info in + let a_val = Const (integer_of_elf64_sxword rel.elf64_ra_addend) in + let addr = rel.elf64_ra_offset in + match symbolic_address_of_symbol ef symtab (natFromNatural sym) with + | Just x -> x + | Nothing -> fail "Invalid symbol table index" + end >>= fun s_val -> + spec rel_type >>= function + | Nothing -> return Map.empty + | Just rel_desc -> + eval_relocation s_val a_val p_val rel_desc >>= fun x -> + return (Map.singleton addr x) + end + else + fail "abi_relocation_interpreter: not a relocatable file" + diff --git a/src/adaptors/harness_interface.lem b/src/adaptors/harness_interface.lem index d8f4020..5837291 100644 --- a/src/adaptors/harness_interface.lem +++ b/src/adaptors/harness_interface.lem @@ -16,6 +16,7 @@ open import Default_printing open import Endianness open import String_table +open import Abi_utilities open import Elf_dynamic open import Elf_file open import Elf_header @@ -514,12 +515,13 @@ let {ocaml} harness_string_of_elf64_reloc_a_entry os symtab sht stbl sechdr_stbl let off = natural_of_elf64_addr rel.elf64_ra_offset in let inf = natural_of_elf64_xword rel.elf64_ra_info in let add = integer_of_elf64_sxword rel.elf64_ra_addend in - let typ = Missing_pervasives.unsafe_string_take 22 (os 0) in (*FIXME *) + let (typ, sym) = parse_elf64_relocation_info rel.elf64_ra_info in + let typ = Missing_pervasives.unsafe_string_take 22 (os typ) in let typs = let len = naturalFromNat (22 - String.stringLength typ) in concatS (replicate len " ") in - let idx = 0 in (* FIXME *) + let idx = sym in let (nm, value, symtyp, secthdr) = match List.index symtab (unsafe_nat_of_natural idx) with | Nothing -> (stn_undef, 0, 0, 0) diff --git a/src/dwarf.lem b/src/dwarf.lem index 070c228..9e121b8 100644 --- a/src/dwarf.lem +++ b/src/dwarf.lem @@ -27,7 +27,10 @@ open import Elf_relocation open import Elf_section_header_table open import Elf_symbol_table open import Elf_types_native_uint +open import Elf_symbolic +open import Sym +open import Dwarf_byte_sequence (** ***************** experimental DWARF reading *********** *) @@ -62,8 +65,8 @@ 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 + val analysed_locations_at_pc : evaluation_context -> dwarf_static -> sym_natural -> analysed_location_data_at_pc + val names_of_address : dwarf -> analysed_location_data_at_pc -> sym_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 @@ -109,7 +112,7 @@ 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 +into just sym_natural, integer, and byte sequences. The lem sym_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. @@ -128,9 +131,78 @@ declare ocaml target_rep function print_endline = `print_endline` let my_debug s = () (*print_endline s*) let my_debug2 s = () (*print_endline s*) let my_debug3 s = () (*print_endline s*) -let my_debug4 s = print_endline s -let my_debug5 s = print_endline s +let my_debug4 s = () (*print_endline s*) +let my_debug5 s = () (*print_endline s*) +(** ************************************************************ *) +(** ** missing pervasives ************************************ *) +(** ************************************************************ *) + +(* natural version of List.index *) +val index_natural : forall 'a. list 'a -> natural -> maybe 'a +let rec index_natural l n = match l with + | [] -> Nothing + | x :: xs -> if n = 0 then Just x else index_natural xs (n-1) +end + +let partialNaturalFromInteger (i:integer) : natural = + if i<0 then Assert_extra.failwith "partialNaturalFromInteger" else naturalFromInteger i + +val natural_nat_shift_left : natural -> nat -> natural +declare ocaml target_rep function natural_nat_shift_left = `Nat_big_num.shift_left` + +val natural_nat_shift_right : natural -> nat -> natural +declare ocaml target_rep function natural_nat_shift_right = `Nat_big_num.shift_right` + +let rec sym_integer_of_symbolic_expression x = match x with + | Section s -> sym_integer_section s + | Const x -> sym_integer_const x + | BinOp (x, Add, y) -> (sym_integer_of_symbolic_expression x) + (sym_integer_of_symbolic_expression y) + | BinOp (x, Sub, y) -> (sym_integer_of_symbolic_expression x) - (sym_integer_of_symbolic_expression y) + (* | AssertRange (x, _, _) -> sym_integer_of_symbolic_expression x (*TODO*) + | AssertAlignment (x, _) -> sym_integer_of_symbolic_expression x (*TODO*) + | Mask (x, _, _) -> sym_integer_of_symbolic_expression x TODO *) +end + +let sym_natural_of_symbolic_expression x = + partialSymNaturalFromInteger (sym_integer_of_symbolic_expression x) + +let sym_natural_land = sym_natural_map2 natural_land +let sym_natural_lxor = sym_natural_map2 natural_lxor +let sym_natural_lor = sym_natural_map2 natural_lor + +let natFromSymNatural x = natFromNatural (sym_natural_expect_const x (*"symIntegerFromNatural"*)) + +let symNaturalFromNat x = sym_natural_const (naturalFromNat x) + +let sym_natural_of_hex x = sym_natural_const (natural_of_hex x) + +let sym_natural_of_byte x = sym_natural_const (natural_of_byte x) + +let symNaturalPow x y = sym_natural_map (fun x -> naturalPow x y) x + +let index_sym_natural l n = index_natural l (sym_natural_expect_const n (*"index_sym_natural"*)) + +let sym_natural_nat_shift_left x sh = sym_natural_map (fun x -> natural_nat_shift_left x sh) x +let sym_natural_nat_shift_right x sh = sym_natural_map (fun x -> natural_nat_shift_right x sh) x + +(* byte sequence *) + +let sym_byte_sequence_of_byte_list l = sym_bs_construct (byte_sequence_of_byte_list l) Map.empty + +let construct_sym_byte_sequence bs rel = + let rel_list = Map_extra.toList rel in + let sym_list = List.map (fun (pos, rel) -> + ( + natural_of_elf64_addr pos, + ( + reloc_width_bytes rel.rel_desc_target, + sym_natural_of_symbolic_expression rel.rel_desc_value + ) + ) + ) rel_list in + let sym_map = Map.fromList sym_list in + sym_bs_construct bs sym_map (** ************************************************************ *) (** ** dwarf representation types **************************** *) @@ -170,18 +242,18 @@ type operation_argument_type = | OAT_block type operation_argument_value = - | OAV_natural of natural - | OAV_integer of integer - | OAV_block of natural * byte_sequence + | OAV_natural of sym_natural + | OAV_integer of sym_integer + | OAV_block of sym_natural * sym_byte_sequence -type operation_stack = list natural +type operation_stack = list sym_natural type arithmetic_context = <| - ac_bitwidth: natural; - ac_half: natural; (* 2 ^ (ac_bitwidth -1) *) - ac_all: natural; (* 2 ^ ac_bitwidth *) - ac_max: natural; (* (2 ^ ac_bitwidth) -1 *) (* also the representation of -1 *) + ac_bitwidth: sym_natural; + ac_half: sym_natural; (* 2 ^ (ac_bitwidth -1) *) + ac_all: sym_natural; (* 2 ^ ac_bitwidth *) + ac_max: sym_natural; (* (2 ^ ac_bitwidth) -1 *) (* also the representation of -1 *) |> type operation_semantics = @@ -189,9 +261,9 @@ type operation_semantics = | OpSem_deref | OpSem_stack of (arithmetic_context -> operation_stack -> list operation_argument_value -> maybe operation_stack) | OpSem_not_supported - | OpSem_binary of (arithmetic_context -> natural -> natural -> maybe natural) - | OpSem_unary of (arithmetic_context -> natural -> maybe natural) - | OpSem_opcode_lit of natural + | OpSem_binary of (arithmetic_context -> sym_natural -> sym_natural -> maybe sym_natural) + | OpSem_unary of (arithmetic_context -> sym_natural -> maybe sym_natural) + | OpSem_opcode_lit of sym_natural | OpSem_reg | OpSem_breg | OpSem_bregx @@ -206,7 +278,7 @@ type operation_semantics = type operation = <| - op_code: natural; + op_code: sym_natural; op_string: string; op_argument_values: list operation_argument_value; op_semantics: operation_semantics; @@ -216,14 +288,14 @@ type operation = (* the result of a location expression evaluation is a single_location (or failure) *) type simple_location = - | SL_memory_address of natural - | SL_register of natural - | SL_implicit of byte_sequence (* used for implicit and stack values *) + | SL_memory_address of sym_natural + | SL_register of sym_natural + | SL_implicit of sym_byte_sequence (* used for implicit and stack values *) | SL_empty type composite_location_piece = - | CLP_piece of natural * simple_location - | CLP_bit_piece of natural * natural * simple_location + | CLP_piece of sym_natural * simple_location + | CLP_bit_piece of sym_natural * sym_natural * simple_location type single_location = | SL_simple of simple_location @@ -241,19 +313,19 @@ type state = (* location expression evaluation can involve register and memory reads, via the following interface *) type register_read_result 'a = - | RRR_result of natural + | RRR_result of sym_natural | RRR_not_currently_available | RRR_bad_register_number type memory_read_result 'a = - | MRR_result of natural + | MRR_result of sym_natural | MRR_not_currently_available | MRR_bad_address type evaluation_context = <| - read_register: natural -> register_read_result natural; - read_memory: natural -> natural -> memory_read_result natural; + read_register: sym_natural -> register_read_result sym_natural; + read_memory: sym_natural -> sym_natural -> memory_read_result sym_natural; |> @@ -267,55 +339,55 @@ type dwarf_format = type abbreviation_declaration = <| - ad_abbreviation_code: natural; - ad_tag: natural; + ad_abbreviation_code: sym_natural; + ad_tag: sym_natural; ad_has_children: bool; - ad_attribute_specifications: list (natural * natural); + ad_attribute_specifications: list (sym_natural * sym_natural); |> type abbreviations_table = <| - at_offset: natural; + at_offset: sym_natural; at_table: list abbreviation_declaration; |> (* .debug_info section *) type attribute_value = (* following Figure 3 *) - | AV_addr of natural - | AV_block of natural * byte_sequence - | AV_constantN of natural * byte_sequence - | AV_constant_SLEB128 of integer - | AV_constant_ULEB128 of natural - | AV_exprloc of natural * byte_sequence + | AV_addr of sym_natural + | AV_block of sym_natural * sym_byte_sequence + | AV_constantN of sym_natural * sym_byte_sequence + | AV_constant_SLEB128 of sym_integer + | AV_constant_ULEB128 of sym_natural + | AV_exprloc of sym_natural * sym_byte_sequence | AV_flag of bool - | AV_ref of natural - | AV_ref_addr of natural (* dwarf_format dependent *) - | AV_ref_sig8 of natural - | AV_sec_offset of natural - | AV_string of byte_sequence (* not including terminating null *) - | AV_strp of natural (* dwarf_format dependent *) + | AV_ref of sym_natural + | AV_ref_addr of sym_natural (* dwarf_format dependent *) + | AV_ref_sig8 of sym_natural + | AV_sec_offset of sym_natural + | AV_string of sym_byte_sequence (* not including terminating null *) + | AV_strp of sym_natural (* dwarf_format dependent *) type die = <| - die_offset: natural; - die_abbreviation_code: natural; + die_offset: sym_natural; + die_abbreviation_code: sym_natural; die_abbreviation_declaration: abbreviation_declaration; - die_attribute_values: list (natural (*pos*) * attribute_value); + die_attribute_values: list (sym_natural (*pos*) * attribute_value); die_children: list die; |> -type die_index = Map.map natural (list die * die) +type die_index = Map.map sym_natural (list die * die) type compilation_unit_header = <| - cuh_offset: natural; + cuh_offset: sym_natural; cuh_dwarf_format: dwarf_format; - cuh_unit_length: natural; - cuh_version: natural; - cuh_debug_abbrev_offset: natural; - cuh_address_size: natural; + cuh_unit_length: sym_natural; + cuh_version: sym_natural; + cuh_debug_abbrev_offset: sym_natural; + cuh_address_size: sym_natural; |> type compilation_unit = @@ -333,8 +405,8 @@ type compilation_units = list compilation_unit type type_unit_header = <| tuh_cuh: compilation_unit_header; - tuh_type_signature: natural; - tuh_type_offset: natural; + tuh_type_signature: sym_natural; + tuh_type_offset: sym_natural; |> type type_unit = @@ -348,25 +420,25 @@ type type_units = list type_unit (* .debug_loc section *) -type single_location_description = byte_sequence +type single_location_description = sym_byte_sequence type location_list_entry = <| - lle_beginning_address_offset: natural; - lle_ending_address_offset: natural; + lle_beginning_address_offset: sym_natural; + lle_ending_address_offset: sym_natural; lle_single_location_description: single_location_description; |> type base_address_selection_entry = <| - base_address: natural; + base_address: sym_natural; |> type location_list_item = | LLI_lle of location_list_entry | LLI_base of base_address_selection_entry -type location_list = natural (*offset*) * list location_list_item +type location_list = sym_natural (*offset*) * list location_list_item type location_list_list = list location_list @@ -374,26 +446,26 @@ type location_list_list = list location_list type range_list_entry = <| - rle_beginning_address_offset: natural; - rle_ending_address_offset: natural; + rle_beginning_address_offset: sym_natural; + rle_ending_address_offset: sym_natural; |> type range_list_item = | RLI_rle of range_list_entry | RLI_base of base_address_selection_entry -type range_list = natural (*offset (of range_list from start of .debug_ranges section?) *) * list range_list_item +type range_list = sym_natural (*offset (of range_list from start of .debug_ranges section?) *) * list range_list_item type range_list_list = list range_list (* .debug_frame section: call frame instructions *) -type cfa_address = natural -type cfa_block = byte_sequence -type cfa_delta = natural -type cfa_offset = natural -type cfa_register = natural -type cfa_sfoffset = integer +type cfa_address = sym_natural +type cfa_block = sym_byte_sequence +type cfa_delta = sym_natural +type cfa_offset = sym_natural +type cfa_register = sym_natural +type cfa_sfoffset = sym_integer type call_frame_argument_type = | CFAT_address @@ -448,29 +520,29 @@ type call_frame_instruction = type cie = <| - cie_offset: natural; - cie_length: natural; - cie_id: natural; - cie_version: natural; - cie_augmentation: byte_sequence; (* not including terminating null *) - cie_address_size: maybe natural; - cie_segment_size: maybe natural; - cie_code_alignment_factor: natural; - cie_data_alignment_factor: integer; + cie_offset: sym_natural; + cie_length: sym_natural; + cie_id: sym_natural; + cie_version: sym_natural; + cie_augmentation: sym_byte_sequence; (* not including terminating null *) + cie_address_size: maybe sym_natural; + cie_segment_size: maybe sym_natural; + cie_code_alignment_factor: sym_natural; + cie_data_alignment_factor: sym_integer; cie_return_address_register: cfa_register; - cie_initial_instructions_bytes: byte_sequence; + cie_initial_instructions_bytes: sym_byte_sequence; cie_initial_instructions: list call_frame_instruction; |> type fde = <| - fde_offset: natural; - fde_length: natural; - fde_cie_pointer: natural; - fde_initial_location_segment_selector: maybe natural; - fde_initial_location_address: natural; - fde_address_range: natural; - fde_instructions_bytes: byte_sequence; + fde_offset: sym_natural; + fde_length: sym_natural; + fde_cie_pointer: sym_natural; + fde_initial_location_segment_selector: maybe sym_natural; + fde_initial_location_address: sym_natural; + fde_address_range: sym_natural; + fde_instructions_bytes: sym_byte_sequence; fde_instructions: list call_frame_instruction; |> @@ -485,7 +557,7 @@ type frame_info = list frame_info_element type cfa_rule = | CR_undefined - | CR_register of cfa_register * integer + | CR_register of cfa_register * sym_integer | CR_expression of single_location_description type register_rule = @@ -493,11 +565,11 @@ type register_rule = (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 integer (* The previous value of this register is saved at the address CFA+N where CFA + | RR_offset of sym_integer (* 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 integer (* The previous value of this register is the value CFA+N where CFA is the + | RR_val_offset of sym_integer (* 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 natural (* The previous value of this register is stored in another register numbered R.*) + | RR_register of sym_natural (* 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 @@ -508,7 +580,7 @@ type register_rule_map = list (cfa_register * register_rule) type cfa_table_row = <| - ctr_loc: natural; + ctr_loc: sym_natural; ctr_cfa: cfa_rule; ctr_regs: register_rule_map; |> @@ -536,57 +608,57 @@ type line_number_argument_type = | LNAT_string type line_number_argument_value = - | LNAV_address of natural - | LNAV_ULEB128 of natural - | LNAV_SLEB128 of integer - | LNAV_uint16 of natural - | LNAV_string of byte_sequence (* not including terminating null *) + | LNAV_address of sym_natural + | LNAV_ULEB128 of sym_natural + | LNAV_SLEB128 of sym_integer + | LNAV_uint16 of sym_natural + | LNAV_string of sym_byte_sequence (* not including terminating null *) type line_number_operation = (* standard *) | DW_LNS_copy - | DW_LNS_advance_pc of natural - | DW_LNS_advance_line of integer - | DW_LNS_set_file of natural - | DW_LNS_set_column of natural + | DW_LNS_advance_pc of sym_natural + | DW_LNS_advance_line of sym_integer + | DW_LNS_set_file of sym_natural + | DW_LNS_set_column of sym_natural | DW_LNS_negate_stmt | DW_LNS_set_basic_block | DW_LNS_const_add_pc - | DW_LNS_fixed_advance_pc of natural + | DW_LNS_fixed_advance_pc of sym_natural | DW_LNS_set_prologue_end | DW_LNS_set_epilogue_begin - | DW_LNS_set_isa of natural + | DW_LNS_set_isa of sym_natural (* extended *) | DW_LNE_end_sequence - | DW_LNE_set_address of natural - | DW_LNE_define_file of byte_sequence * natural * natural * natural - | DW_LNE_set_discriminator of natural + | DW_LNE_set_address of sym_natural + | DW_LNE_define_file of sym_byte_sequence * sym_natural * sym_natural * sym_natural + | DW_LNE_set_discriminator of sym_natural (* special *) - | DW_LN_special of natural (* the adjusted opcode *) + | DW_LN_special of sym_natural (* the adjusted opcode *) type line_number_file_entry = <| - lnfe_path: byte_sequence; - lnfe_directory_index: natural; - lnfe_last_modification: natural; - lnfe_length: natural; + lnfe_path: sym_byte_sequence; + lnfe_directory_index: sym_natural; + lnfe_last_modification: sym_natural; + lnfe_length: sym_natural; |> type line_number_header = <| - lnh_offset: natural; + lnh_offset: sym_natural; lnh_dwarf_format: dwarf_format; - lnh_unit_length: natural; - lnh_version: natural; - lnh_header_length: natural; - lnh_minimum_instruction_length: natural; - lnh_maximum_operations_per_instruction: natural; + lnh_unit_length: sym_natural; + lnh_version: sym_natural; + lnh_header_length: sym_natural; + lnh_minimum_instruction_length: sym_natural; + lnh_maximum_operations_per_instruction: sym_natural; lnh_default_is_stmt: bool; - lnh_line_base: integer; - lnh_line_range: natural; - lnh_opcode_base: natural; - lnh_standard_opcode_lengths: list natural; - lnh_include_directories: list (byte_sequence); + lnh_line_base: sym_integer; + lnh_line_range: sym_natural; + lnh_opcode_base: sym_natural; + lnh_standard_opcode_lengths: list sym_natural; + lnh_include_directories: list (sym_byte_sequence); lnh_file_entries: list line_number_file_entry; lnh_comp_dir: maybe string; (* passed down from cu DW_AT_comp_dir *) |> @@ -601,18 +673,18 @@ type line_number_program = type line_number_registers = <| - lnr_address: natural; - lnr_op_index: natural; - lnr_file: natural; - lnr_line: natural; - lnr_column: natural; + lnr_address: sym_natural; + lnr_op_index: sym_natural; + lnr_file: sym_natural; + lnr_line: sym_natural; + lnr_column: sym_natural; lnr_is_stmt: bool; lnr_basic_block: bool; lnr_end_sequence: bool; lnr_prologue_end: bool; lnr_epilogue_begin: bool; - lnr_isa: natural; - lnr_discriminator: natural; + lnr_isa: sym_natural; + lnr_discriminator: sym_natural; |> type unpacked_file_entry = (maybe string (*comp_dir*)) * (maybe string (*dir*)) * string (*file*) @@ -625,7 +697,7 @@ type unpacked_decl = unpacked_file_entry * nat(*line*) * string(*subprogram name type dwarf = <| d_endianness: Endianness.endianness; (* from the ELF *) - d_str: byte_sequence; + d_str: sym_byte_sequence; d_compilation_units: compilation_units; d_type_units: type_units; d_loc: location_list_list; @@ -636,9 +708,9 @@ type dwarf = (* analysed location data *) -type analysed_location_data = list ((compilation_unit * (list die) * die) * maybe (list (natural * natural * single_location_description))) +type analysed_location_data = list ((compilation_unit * (list die) * die) * maybe (list (sym_natural * sym_natural * single_location_description))) -type analysed_location_data_at_pc = list ((compilation_unit * (list die) * die) * (natural * natural * single_location_description * error single_location)) +type analysed_location_data_at_pc = list ((compilation_unit * (list die) * die) * (sym_natural * sym_natural * single_location_description * error single_location)) (* evaluated line data *) @@ -652,7 +724,7 @@ type dwarf_static = ds_analysed_location_data: analysed_location_data; ds_evaluated_frame_info: evaluated_frame_info; ds_evaluated_line_info: evaluated_line_info; - ds_subprogram_line_extents: list (unpacked_file_entry * list (string * unpacked_file_entry * natural) ); + ds_subprogram_line_extents: list (unpacked_file_entry * list (string * unpacked_file_entry * sym_natural) ); |> type dwarf_dynamic_at_pc = analysed_location_data_at_pc @@ -674,30 +746,30 @@ type cupdie = compilation_unit * (list die) * die type decl = <| decl_file: maybe string; - decl_line: maybe natural; + decl_line: maybe sym_natural; |> -type array_dimension 't = maybe natural(*count*) * maybe 't(*subrange type*) +type array_dimension 't = maybe sym_natural(*count*) * maybe 't(*subrange type*) -type struct_union_member 't = cupdie * (maybe string)(*mname*) * 't * maybe natural(*data_member_location, non-Nothing for structs*) +type struct_union_member 't = cupdie * (maybe string)(*mname*) * 't * maybe sym_natural(*data_member_location, non-Nothing for structs*) type struct_union_type_kind = | Atk_structure | Atk_union -type enumeration_member = cupdie * (maybe string)(*mname*) * integer(*const_value*) +type enumeration_member = cupdie * (maybe string)(*mname*) * sym_integer(*const_value*) type c_type_top 't = | CT_missing of cupdie - | CT_base of cupdie * string(*name*) * natural(*encoding*) * (maybe natural)(*byte_size*) + | CT_base of cupdie * string(*name*) * sym_natural(*encoding*) * (maybe sym_natural)(*byte_size*) | CT_pointer of cupdie * maybe 't | CT_const of cupdie * maybe 't | CT_volatile of cupdie * 't | CT_restrict of cupdie * 't | CT_typedef of cupdie * string(*name*) * 't * decl | CT_array of cupdie * 't * list (array_dimension 't) - | CT_struct_union of cupdie * struct_union_type_kind * (maybe string)(*mname*) * (maybe natural)(*byte_size*) * decl * maybe (list (struct_union_member 't)(*members*)) - | CT_enumeration of cupdie * (maybe string)(*mname*) * (maybe 't)(*mtyp*) * (maybe natural)(*mbyte_size*) * decl * maybe (list (enumeration_member)(*members*)) + | CT_struct_union of cupdie * struct_union_type_kind * (maybe string)(*mname*) * (maybe sym_natural)(*byte_size*) * decl * maybe (list (struct_union_member 't)(*members*)) + | CT_enumeration of cupdie * (maybe string)(*mname*) * (maybe 't)(*mtyp*) * (maybe sym_natural)(*mbyte_size*) * decl * maybe (list (enumeration_member)(*members*)) | CT_subroutine of cupdie * (bool)(*prototyped*) * (maybe 't)(*mresult_type*) * (list 't)(*parameter_types*) * (bool)(*variable_parameter_list*) (* In the CT_struct_union and C_enumeration cases, the final maybe(list(...member)) is Nothing if the analysis has not been recursed into the members, and Just ... if it has - which will typically be only one level deep *) @@ -728,10 +800,11 @@ type sdt_variable_or_formal_parameter = svfp_kind : variable_or_formal_parameter_kind; svfp_type : maybe c_type; svfp_abstract_origin : maybe sdt_variable_or_formal_parameter; (* invariant: non-Nothing iff inlined *) - svfp_const_value : maybe integer; + svfp_const_value : maybe sym_integer; svfp_external : bool; svfp_declaration : bool; - svfp_locations : maybe (list (natural * natural * list operation (*the parsed single_location_description*))); + svfp_locations_frame_base : maybe (list (sym_natural * sym_natural * list operation)); + svfp_locations : maybe (list (sym_natural * sym_natural * list operation (*the parsed single_location_description*))); svfp_decl : maybe unpacked_decl; |> @@ -748,8 +821,8 @@ type sdt_subroutine = (* subprogram or inlined subroutine *) ss_abstract_origin : maybe sdt_subroutine; (* invariant: non-Nothing iff inlined *) ss_type : maybe c_type; ss_vars : list sdt_variable_or_formal_parameter; - ss_pc_ranges : maybe (list (natural*natural)); - ss_entry_address : maybe natural; + ss_pc_ranges : maybe (list (sym_natural*sym_natural)); + ss_entry_address : maybe sym_natural; ss_unspecified_parameters : list sdt_unspecified_parameter; ss_subroutines : list sdt_subroutine; (* invariant: all inlined*) ss_lexical_blocks : list sdt_lexical_block; @@ -762,7 +835,7 @@ and sdt_lexical_block = <| slb_cupdie : cupdie; slb_vars : list sdt_variable_or_formal_parameter; (* invariant: all variables *) - slb_pc_ranges : maybe (list (natural*natural)); + slb_pc_ranges : maybe (list (sym_natural*sym_natural)); slb_subroutines : list sdt_subroutine; (* invariant: all inlined*) slb_lexical_blocks : list sdt_lexical_block; |> @@ -773,7 +846,7 @@ type sdt_compilation_unit = scu_name : string; scu_subroutines : list sdt_subroutine; (* invariant: none inlined(?) *) scu_vars : list sdt_variable_or_formal_parameter; - scu_pc_ranges : maybe (list (natural*natural)); + scu_pc_ranges : maybe (list (sym_natural*sym_natural)); |> type sdt_dwarf = @@ -786,7 +859,7 @@ type sdt_dwarf = type inlined_subroutine_const_param = <| iscp_abstract_origin: compilation_unit * (list die) * die; - iscp_value: integer; + iscp_value: sym_integer; |> type inlined_subroutine = @@ -797,48 +870,23 @@ type inlined_subroutine = is_inlined_subroutine_sdt_parents: list sdt_subroutine; is_name : string; is_call_file: unpacked_file_entry; - is_call_line: natural; - is_pc_ranges: list (natural * natural); + is_call_line: sym_natural; + is_pc_ranges: list (sym_natural * sym_natural); is_const_params : list inlined_subroutine_const_param; |> (* ignoring the nesting structure of inlined subroutines for now *) type inlined_subroutine_data = list inlined_subroutine -type inlined_subroutine_data_by_range_entry = (natural*natural)(*range*) * (natural*natural) (*range m-of-n*) * inlined_subroutine +type inlined_subroutine_data_by_range_entry = (sym_natural*sym_natural)(*range*) * (sym_natural*sym_natural) (*range m-of-n*) * inlined_subroutine type inlined_subroutine_data_by_range = list inlined_subroutine_data_by_range_entry -(*type inlined_subroutine_data_at_pc = list ((compilation_unit * (list die) * die) * (natural * natural * single_location_description * error single_location))*) - - - - +(*type inlined_subroutine_data_at_pc = list ((compilation_unit * (list die) * die) * (sym_natural * sym_natural * single_location_description * error single_location))*) -(** ************************************************************ *) -(** ** missing pervasives ************************************ *) -(** ************************************************************ *) - -(* natural version of List.index *) -val index_natural : forall 'a. list 'a -> natural -> maybe 'a -let rec index_natural l n = match l with - | [] -> Nothing - | x :: xs -> if n = 0 then Just x else index_natural xs (n-1) -end - -let partialNaturalFromInteger (i:integer) : natural = - if i<0 then Assert_extra.failwith "partialNaturalFromInteger" else naturalFromInteger i - -val natural_nat_shift_left : natural -> nat -> natural -declare ocaml target_rep function natural_nat_shift_left = `Nat_big_num.shift_left` - -val natural_nat_shift_right : natural -> nat -> natural -declare ocaml target_rep function natural_nat_shift_right = `Nat_big_num.shift_right` - - (** ************************************************************ *) (** ** endianness *************************************** *) (** ************************************************************ *) @@ -855,389 +903,389 @@ let p_context_of_d (d:dwarf) : p_context = <| endianness = d.d_endianness |> (* tag encoding *) let tag_encodings = [ - ("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") + ("DW_TAG_array_type" , sym_natural_of_hex "0x01" ); + ("DW_TAG_class_type" , sym_natural_of_hex "0x02" ); + ("DW_TAG_entry_point" , sym_natural_of_hex "0x03" ); + ("DW_TAG_enumeration_type" , sym_natural_of_hex "0x04" ); + ("DW_TAG_formal_parameter" , sym_natural_of_hex "0x05" ); + ("DW_TAG_imported_declaration" , sym_natural_of_hex "0x08" ); + ("DW_TAG_label" , sym_natural_of_hex "0x0a" ); + ("DW_TAG_lexical_block" , sym_natural_of_hex "0x0b" ); + ("DW_TAG_member" , sym_natural_of_hex "0x0d" ); + ("DW_TAG_pointer_type" , sym_natural_of_hex "0x0f" ); + ("DW_TAG_reference_type" , sym_natural_of_hex "0x10" ); + ("DW_TAG_compile_unit" , sym_natural_of_hex "0x11" ); + ("DW_TAG_string_type" , sym_natural_of_hex "0x12" ); + ("DW_TAG_structure_type" , sym_natural_of_hex "0x13" ); + ("DW_TAG_subroutine_type" , sym_natural_of_hex "0x15" ); + ("DW_TAG_typedef" , sym_natural_of_hex "0x16" ); + ("DW_TAG_union_type" , sym_natural_of_hex "0x17" ); + ("DW_TAG_unspecified_parameters" , sym_natural_of_hex "0x18" ); + ("DW_TAG_variant" , sym_natural_of_hex "0x19" ); + ("DW_TAG_common_block" , sym_natural_of_hex "0x1a" ); + ("DW_TAG_common_inclusion" , sym_natural_of_hex "0x1b" ); + ("DW_TAG_inheritance" , sym_natural_of_hex "0x1c" ); + ("DW_TAG_inlined_subroutine" , sym_natural_of_hex "0x1d" ); + ("DW_TAG_module" , sym_natural_of_hex "0x1e" ); + ("DW_TAG_ptr_to_member_type" , sym_natural_of_hex "0x1f" ); + ("DW_TAG_set_type" , sym_natural_of_hex "0x20" ); + ("DW_TAG_subrange_type" , sym_natural_of_hex "0x21" ); + ("DW_TAG_with_stmt" , sym_natural_of_hex "0x22" ); + ("DW_TAG_access_declaration" , sym_natural_of_hex "0x23" ); + ("DW_TAG_base_type" , sym_natural_of_hex "0x24" ); + ("DW_TAG_catch_block" , sym_natural_of_hex "0x25" ); + ("DW_TAG_const_type" , sym_natural_of_hex "0x26" ); + ("DW_TAG_constant" , sym_natural_of_hex "0x27" ); + ("DW_TAG_enumerator" , sym_natural_of_hex "0x28" ); + ("DW_TAG_file_type" , sym_natural_of_hex "0x29" ); + ("DW_TAG_friend" , sym_natural_of_hex "0x2a" ); + ("DW_TAG_namelist" , sym_natural_of_hex "0x2b" ); + ("DW_TAG_namelist_item" , sym_natural_of_hex "0x2c" ); + ("DW_TAG_packed_type" , sym_natural_of_hex "0x2d" ); + ("DW_TAG_subprogram" , sym_natural_of_hex "0x2e" ); + ("DW_TAG_template_type_parameter" , sym_natural_of_hex "0x2f" ); + ("DW_TAG_template_value_parameter" , sym_natural_of_hex "0x30" ); + ("DW_TAG_thrown_type" , sym_natural_of_hex "0x31" ); + ("DW_TAG_try_block" , sym_natural_of_hex "0x32" ); + ("DW_TAG_variant_part" , sym_natural_of_hex "0x33" ); + ("DW_TAG_variable" , sym_natural_of_hex "0x34" ); + ("DW_TAG_volatile_type" , sym_natural_of_hex "0x35" ); + ("DW_TAG_dwarf_procedure" , sym_natural_of_hex "0x36" ); + ("DW_TAG_restrict_type" , sym_natural_of_hex "0x37" ); + ("DW_TAG_interface_type" , sym_natural_of_hex "0x38" ); + ("DW_TAG_namespace" , sym_natural_of_hex "0x39" ); + ("DW_TAG_imported_module" , sym_natural_of_hex "0x3a" ); + ("DW_TAG_unspecified_type" , sym_natural_of_hex "0x3b" ); + ("DW_TAG_partial_unit" , sym_natural_of_hex "0x3c" ); + ("DW_TAG_imported_unit" , sym_natural_of_hex "0x3d" ); + ("DW_TAG_condition" , sym_natural_of_hex "0x3f" ); + ("DW_TAG_shared_type" , sym_natural_of_hex "0x40" ); + ("DW_TAG_type_unit" , sym_natural_of_hex "0x41" ); + ("DW_TAG_rvalue_reference_type" , sym_natural_of_hex "0x42" ); + ("DW_TAG_template_alias" , sym_natural_of_hex "0x43" ); + ("DW_TAG_lo_user" , sym_natural_of_hex "0x4080"); + ("DW_TAG_hi_user" , sym_natural_of_hex "0xffff") ] (* child determination encoding *) -let vDW_CHILDREN_no = natural_of_hex "0x00" -let vDW_CHILDREN_yes = natural_of_hex "0x01" +let vDW_CHILDREN_no = sym_natural_of_hex "0x00" +let vDW_CHILDREN_yes = sym_natural_of_hex "0x01" (* attribute encoding *) let attribute_encodings = [ - ("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_sibling" , sym_natural_of_hex "0x01", [DWA_reference]) ; + ("DW_AT_location" , sym_natural_of_hex "0x02", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_name" , sym_natural_of_hex "0x03", [DWA_string]) ; + ("DW_AT_ordering" , sym_natural_of_hex "0x09", [DWA_constant]) ; + ("DW_AT_byte_size" , sym_natural_of_hex "0x0b", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_bit_offset" , sym_natural_of_hex "0x0c", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_bit_size" , sym_natural_of_hex "0x0d", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_stmt_list" , sym_natural_of_hex "0x10", [DWA_lineptr]) ; + ("DW_AT_low_pc" , sym_natural_of_hex "0x11", [DWA_address]) ; + ("DW_AT_high_pc" , sym_natural_of_hex "0x12", [DWA_address; DWA_constant]) ; + ("DW_AT_language" , sym_natural_of_hex "0x13", [DWA_constant]) ; + ("DW_AT_discr" , sym_natural_of_hex "0x15", [DWA_reference]) ; + ("DW_AT_discr_value" , sym_natural_of_hex "0x16", [DWA_constant]) ; + ("DW_AT_visibility" , sym_natural_of_hex "0x17", [DWA_constant]) ; + ("DW_AT_import" , sym_natural_of_hex "0x18", [DWA_reference]) ; + ("DW_AT_string_length" , sym_natural_of_hex "0x19", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_common_reference" , sym_natural_of_hex "0x1a", [DWA_reference]) ; + ("DW_AT_comp_dir" , sym_natural_of_hex "0x1b", [DWA_string]) ; + ("DW_AT_const_value" , sym_natural_of_hex "0x1c", [DWA_block; DWA_constant; DWA_string]) ; + ("DW_AT_containing_type" , sym_natural_of_hex "0x1d", [DWA_reference]) ; + ("DW_AT_default_value" , sym_natural_of_hex "0x1e", [DWA_reference]) ; + ("DW_AT_inline" , sym_natural_of_hex "0x20", [DWA_constant]) ; + ("DW_AT_is_optional" , sym_natural_of_hex "0x21", [DWA_flag]) ; + ("DW_AT_lower_bound" , sym_natural_of_hex "0x22", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_producer" , sym_natural_of_hex "0x25", [DWA_string]) ; + ("DW_AT_prototyped" , sym_natural_of_hex "0x27", [DWA_flag]) ; + ("DW_AT_return_addr" , sym_natural_of_hex "0x2a", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_start_scope" , sym_natural_of_hex "0x2c", [DWA_constant; DWA_rangelistptr]) ; + ("DW_AT_bit_stride" , sym_natural_of_hex "0x2e", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_upper_bound" , sym_natural_of_hex "0x2f", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_abstract_origin" , sym_natural_of_hex "0x31", [DWA_reference]) ; + ("DW_AT_accessibility" , sym_natural_of_hex "0x32", [DWA_constant]) ; + ("DW_AT_address_class" , sym_natural_of_hex "0x33", [DWA_constant]) ; + ("DW_AT_artificial" , sym_natural_of_hex "0x34", [DWA_flag]) ; + ("DW_AT_base_types" , sym_natural_of_hex "0x35", [DWA_reference]) ; + ("DW_AT_calling_convention" , sym_natural_of_hex "0x36", [DWA_constant]) ; + ("DW_AT_count" , sym_natural_of_hex "0x37", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_data_member_location" , sym_natural_of_hex "0x38", [DWA_constant; DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_decl_column" , sym_natural_of_hex "0x39", [DWA_constant]) ; + ("DW_AT_decl_file" , sym_natural_of_hex "0x3a", [DWA_constant]) ; + ("DW_AT_decl_line" , sym_natural_of_hex "0x3b", [DWA_constant]) ; + ("DW_AT_declaration" , sym_natural_of_hex "0x3c", [DWA_flag]) ; + ("DW_AT_discr_list" , sym_natural_of_hex "0x3d", [DWA_block]) ; + ("DW_AT_encoding" , sym_natural_of_hex "0x3e", [DWA_constant]) ; + ("DW_AT_external" , sym_natural_of_hex "0x3f", [DWA_flag]) ; + ("DW_AT_frame_base" , sym_natural_of_hex "0x40", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_friend" , sym_natural_of_hex "0x41", [DWA_reference]) ; + ("DW_AT_identifier_case" , sym_natural_of_hex "0x42", [DWA_constant]) ; + ("DW_AT_macro_info" , sym_natural_of_hex "0x43", [DWA_macptr]) ; + ("DW_AT_namelist_item" , sym_natural_of_hex "0x44", [DWA_reference]) ; + ("DW_AT_priority" , sym_natural_of_hex "0x45", [DWA_reference]) ; + ("DW_AT_segment" , sym_natural_of_hex "0x46", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_specification" , sym_natural_of_hex "0x47", [DWA_reference]) ; + ("DW_AT_static_link" , sym_natural_of_hex "0x48", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_type" , sym_natural_of_hex "0x49", [DWA_reference]) ; + ("DW_AT_use_location" , sym_natural_of_hex "0x4a", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_variable_parameter" , sym_natural_of_hex "0x4b", [DWA_flag]) ; + ("DW_AT_virtuality" , sym_natural_of_hex "0x4c", [DWA_constant]) ; + ("DW_AT_vtable_elem_location" , sym_natural_of_hex "0x4d", [DWA_exprloc; DWA_loclistptr]) ; + ("DW_AT_allocated" , sym_natural_of_hex "0x4e", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_associated" , sym_natural_of_hex "0x4f", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_data_location" , sym_natural_of_hex "0x50", [DWA_exprloc]) ; + ("DW_AT_byte_stride" , sym_natural_of_hex "0x51", [DWA_constant; DWA_exprloc; DWA_reference]) ; + ("DW_AT_entry_pc" , sym_natural_of_hex "0x52", [DWA_address]) ; + ("DW_AT_use_UTF8" , sym_natural_of_hex "0x53", [DWA_flag]) ; + ("DW_AT_extension" , sym_natural_of_hex "0x54", [DWA_reference]) ; + ("DW_AT_ranges" , sym_natural_of_hex "0x55", [DWA_rangelistptr]) ; + ("DW_AT_trampoline" , sym_natural_of_hex "0x56", [DWA_address; DWA_flag; DWA_reference; DWA_string]); + ("DW_AT_call_column" , sym_natural_of_hex "0x57", [DWA_constant]) ; + ("DW_AT_call_file" , sym_natural_of_hex "0x58", [DWA_constant]) ; + ("DW_AT_call_line" , sym_natural_of_hex "0x59", [DWA_constant]) ; + ("DW_AT_description" , sym_natural_of_hex "0x5a", [DWA_string]) ; + ("DW_AT_binary_scale" , sym_natural_of_hex "0x5b", [DWA_constant]) ; + ("DW_AT_decimal_scale" , sym_natural_of_hex "0x5c", [DWA_constant]) ; + ("DW_AT_small" , sym_natural_of_hex "0x5d", [DWA_reference]) ; + ("DW_AT_decimal_sign" , sym_natural_of_hex "0x5e", [DWA_constant]) ; + ("DW_AT_digit_count" , sym_natural_of_hex "0x5f", [DWA_constant]) ; + ("DW_AT_picture_string" , sym_natural_of_hex "0x60", [DWA_string]) ; + ("DW_AT_mutable" , sym_natural_of_hex "0x61", [DWA_flag]) ; + ("DW_AT_threads_scaled" , sym_natural_of_hex "0x62", [DWA_flag]) ; + ("DW_AT_explicit" , sym_natural_of_hex "0x63", [DWA_flag]) ; + ("DW_AT_object_pointer" , sym_natural_of_hex "0x64", [DWA_reference]) ; + ("DW_AT_endianity" , sym_natural_of_hex "0x65", [DWA_constant]) ; + ("DW_AT_elemental" , sym_natural_of_hex "0x66", [DWA_flag]) ; + ("DW_AT_pure" , sym_natural_of_hex "0x67", [DWA_flag]) ; + ("DW_AT_recursive" , sym_natural_of_hex "0x68", [DWA_flag]) ; + ("DW_AT_signature" , sym_natural_of_hex "0x69", [DWA_reference]) ; + ("DW_AT_main_subprogram" , sym_natural_of_hex "0x6a", [DWA_flag]) ; + ("DW_AT_data_bit_offset" , sym_natural_of_hex "0x6b", [DWA_constant]) ; + ("DW_AT_const_expr" , sym_natural_of_hex "0x6c", [DWA_flag]) ; + ("DW_AT_enum_class" , sym_natural_of_hex "0x6d", [DWA_flag]) ; + ("DW_AT_linkage_name" , sym_natural_of_hex "0x6e", [DWA_string]) ; (* DW_AT_noreturn is a gcc extension to support the C11 _Noreturn keyword*) - ("DW_AT_noreturn" , natural_of_hex "0x87", [DWA_flag]) ; - ("DW_AT_alignment" , natural_of_hex "0x88", [DWA_constant]) ; - ("DW_AT_lo_user" , natural_of_hex "0x2000", [DWA_dash]) ; - ("DW_AT_hi_user" , natural_of_hex "0x3fff", [DWA_dash]) + ("DW_AT_noreturn" , sym_natural_of_hex "0x87", [DWA_flag]) ; + ("DW_AT_alignment" , sym_natural_of_hex "0x88", [DWA_constant]) ; + ("DW_AT_lo_user" , sym_natural_of_hex "0x2000", [DWA_dash]) ; + ("DW_AT_hi_user" , sym_natural_of_hex "0x3fff", [DWA_dash]) ] (* attribute form encoding *) let attribute_form_encodings = [ - ("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]) + ("DW_FORM_addr" , sym_natural_of_hex "0x01", [DWA_address]) ; + ("DW_FORM_block2" , sym_natural_of_hex "0x03", [DWA_block]) ; + ("DW_FORM_block4" , sym_natural_of_hex "0x04", [DWA_block]) ; + ("DW_FORM_data2" , sym_natural_of_hex "0x05", [DWA_constant]) ; + ("DW_FORM_data4" , sym_natural_of_hex "0x06", [DWA_constant]) ; + ("DW_FORM_data8" , sym_natural_of_hex "0x07", [DWA_constant]) ; + ("DW_FORM_string" , sym_natural_of_hex "0x08", [DWA_string]) ; + ("DW_FORM_block" , sym_natural_of_hex "0x09", [DWA_block]) ; + ("DW_FORM_block1" , sym_natural_of_hex "0x0a", [DWA_block]) ; + ("DW_FORM_data1" , sym_natural_of_hex "0x0b", [DWA_constant]) ; + ("DW_FORM_flag" , sym_natural_of_hex "0x0c", [DWA_flag]) ; + ("DW_FORM_sdata" , sym_natural_of_hex "0x0d", [DWA_constant]) ; + ("DW_FORM_strp" , sym_natural_of_hex "0x0e", [DWA_string]) ; + ("DW_FORM_udata" , sym_natural_of_hex "0x0f", [DWA_constant]) ; + ("DW_FORM_ref_addr" , sym_natural_of_hex "0x10", [DWA_reference]); + ("DW_FORM_ref1" , sym_natural_of_hex "0x11", [DWA_reference]); + ("DW_FORM_ref2" , sym_natural_of_hex "0x12", [DWA_reference]); + ("DW_FORM_ref4" , sym_natural_of_hex "0x13", [DWA_reference]); + ("DW_FORM_ref8" , sym_natural_of_hex "0x14", [DWA_reference]); + ("DW_FORM_ref_udata" , sym_natural_of_hex "0x15", [DWA_reference]); + ("DW_FORM_indirect" , sym_natural_of_hex "0x16", [DWA_7_5_3]) ; + ("DW_FORM_sec_offset" , sym_natural_of_hex "0x17", [DWA_lineptr; DWA_loclistptr; DWA_macptr; DWA_rangelistptr]) ; + ("DW_FORM_exprloc" , sym_natural_of_hex "0x18", [DWA_exprloc]) ; + ("DW_FORM_flag_present", sym_natural_of_hex "0x19", [DWA_flag]) ; + ("DW_FORM_ref_sig8" , sym_natural_of_hex "0x20", [DWA_reference]) ] (* operation encoding *) let operation_encodings = [ -("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 -> Just (v::v::vs) | _ -> Nothing end)); (*0*) -("DW_OP_drop", natural_of_hex "0x13", [] , OpSem_stack (fun ac vs args -> match vs with v::vs -> Just vs | _ -> Nothing end)); (*0*) -("DW_OP_over", natural_of_hex "0x14", [] , OpSem_stack (fun ac vs args -> match vs with v::v'::vs -> Just (v'::v::v'::vs) | _ -> Nothing end)); (*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 Just v -> Just (v::vs) | Nothing -> Nothing end | _ -> Nothing end)); (*1*) (* 1-byte stack index *) -("DW_OP_swap", natural_of_hex "0x16", [] , OpSem_stack (fun ac vs args -> match vs with v::v'::vs -> Just (v'::v::vs) | _ -> Nothing end)); (*0*) -("DW_OP_rot", natural_of_hex "0x17", [] , OpSem_stack (fun ac vs args -> match vs with v::v'::v''::vs -> Just (v'::v''::v::vs) | _ -> Nothing end)); (*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 v < ac.ac_half then Just v else if v=ac.ac_max then Nothing else Just (ac.ac_all-v))); (*0*) -("DW_OP_and", natural_of_hex "0x1a", [] , OpSem_binary (fun ac v1 v2 -> Just (natural_land 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 -> Just (partialNaturalFromInteger ((integerFromNatural v1 - integerFromNatural v2) mod (integerFromNatural ac.ac_all))))); (*0*) -("DW_OP_mod", natural_of_hex "0x1d", [] , OpSem_binary (fun ac v1 v2 -> Just (v1 mod v2))); (*0*) -("DW_OP_mul", natural_of_hex "0x1e", [] , OpSem_binary (fun ac v1 v2 -> Just (partialNaturalFromInteger ((integerFromNatural v1 * integerFromNatural v2) mod (integerFromNatural ac.ac_all))))); (*0*) -("DW_OP_neg", natural_of_hex "0x1f", [] , OpSem_unary (fun ac v -> if v < ac.ac_half then Just (ac.ac_max - v) else if v=ac.ac_half then Nothing else Just (ac.ac_all - v))); (*0*) -("DW_OP_not", natural_of_hex "0x20", [] , OpSem_unary (fun ac v -> Just (natural_lxor v ac.ac_max))); (*0*) -("DW_OP_or", natural_of_hex "0x21", [] , OpSem_binary (fun ac v1 v2 -> Just (natural_lor v1 v2))); (*0*) -("DW_OP_plus", natural_of_hex "0x22", [] , OpSem_binary (fun ac v1 v2 -> Just ((v1 + v2) mod 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' = (v+n) mod ac.ac_all in Just (v'::vs) | [] -> Nothing end | _ -> Nothing end)); (*1*) (* ULEB128 addend *) -("DW_OP_shl", natural_of_hex "0x24", [] , OpSem_binary (fun ac v1 v2 -> if v2 >= ac.ac_bitwidth then Just 0 else Just (natural_nat_shift_left v1 (natFromNatural v2)))); (*0*) -("DW_OP_shr", natural_of_hex "0x25", [] , OpSem_binary (fun ac v1 v2 -> if v2 >= ac.ac_bitwidth then Just 0 else Just (natural_nat_shift_right v1 (natFromNatural v2)))); (*0*) -("DW_OP_shra", natural_of_hex "0x26", [] , OpSem_binary (fun ac v1 v2 -> if v1 < ac.ac_half then (if v2 >= ac.ac_bitwidth then Just 0 else Just (natural_nat_shift_right v1 (natFromNatural v2))) else (if v2 >= ac.ac_bitwidth then Just ac.ac_max else Just (ac.ac_max - (natural_nat_shift_right (ac.ac_max - v1) (natFromNatural v2)))))); (*0*) -("DW_OP_xor", natural_of_hex "0x27", [] , OpSem_binary (fun ac v1 v2 -> Just (natural_lxor 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*) +("DW_OP_addr", sym_natural_of_hex "0x03", [OAT_addr] , OpSem_lit); (*1*) (*constant address (size target specific)*) +("DW_OP_deref", sym_natural_of_hex "0x06", [] , OpSem_deref); (*0*) +("DW_OP_const1u", sym_natural_of_hex "0x08", [OAT_uint8] , OpSem_lit); (*1*) (* 1-byte constant *) +("DW_OP_const1s", sym_natural_of_hex "0x09", [OAT_sint8] , OpSem_lit); (*1*) (* 1-byte constant *) +("DW_OP_const2u", sym_natural_of_hex "0x0a", [OAT_uint16] , OpSem_lit); (*1*) (* 2-byte constant *) +("DW_OP_const2s", sym_natural_of_hex "0x0b", [OAT_sint16] , OpSem_lit); (*1*) (* 2-byte constant *) +("DW_OP_const4u", sym_natural_of_hex "0x0c", [OAT_uint32] , OpSem_lit); (*1*) (* 4-byte constant *) +("DW_OP_const4s", sym_natural_of_hex "0x0d", [OAT_sint32] , OpSem_lit); (*1*) (* 4-byte constant *) +("DW_OP_const8u", sym_natural_of_hex "0x0e", [OAT_uint64] , OpSem_lit); (*1*) (* 8-byte constant *) +("DW_OP_const8s", sym_natural_of_hex "0x0f", [OAT_sint64] , OpSem_lit); (*1*) (* 8-byte constant *) +("DW_OP_constu", sym_natural_of_hex "0x10", [OAT_ULEB128] , OpSem_lit); (*1*) (* ULEB128 constant *) +("DW_OP_consts", sym_natural_of_hex "0x11", [OAT_SLEB128] , OpSem_lit); (*1*) (* SLEB128 constant *) +("DW_OP_dup", sym_natural_of_hex "0x12", [] , OpSem_stack (fun ac vs args -> match vs with v::vs -> Just (v::v::vs) | _ -> Nothing end)); (*0*) +("DW_OP_drop", sym_natural_of_hex "0x13", [] , OpSem_stack (fun ac vs args -> match vs with v::vs -> Just vs | _ -> Nothing end)); (*0*) +("DW_OP_over", sym_natural_of_hex "0x14", [] , OpSem_stack (fun ac vs args -> match vs with v::v'::vs -> Just (v'::v::v'::vs) | _ -> Nothing end)); (*0*) +("DW_OP_pick", sym_natural_of_hex "0x15", [OAT_uint8] , OpSem_stack (fun ac vs args -> match args with [OAV_natural n] -> match index_sym_natural vs n with Just v -> Just (v::vs) | Nothing -> Nothing end | _ -> Nothing end)); (*1*) (* 1-byte stack index *) +("DW_OP_swap", sym_natural_of_hex "0x16", [] , OpSem_stack (fun ac vs args -> match vs with v::v'::vs -> Just (v'::v::vs) | _ -> Nothing end)); (*0*) +("DW_OP_rot", sym_natural_of_hex "0x17", [] , OpSem_stack (fun ac vs args -> match vs with v::v'::v''::vs -> Just (v'::v''::v::vs) | _ -> Nothing end)); (*0*) +("DW_OP_xderef", sym_natural_of_hex "0x18", [] , OpSem_not_supported); (*0*) +("DW_OP_abs", sym_natural_of_hex "0x19", [] , OpSem_unary (fun ac v -> if v < ac.ac_half then Just v else if v=ac.ac_max then Nothing else Just (ac.ac_all-v))); (*0*) +("DW_OP_and", sym_natural_of_hex "0x1a", [] , OpSem_binary (fun ac v1 v2 -> Just (sym_natural_land v1 v2))); (*0*) +("DW_OP_div", sym_natural_of_hex "0x1b", [] , OpSem_not_supported) (*TODO*); (*0*) +("DW_OP_minus", sym_natural_of_hex "0x1c", [] , OpSem_binary (fun ac v1 v2 -> Just (partialSymNaturalFromInteger ((symIntegerFromNatural v1 - symIntegerFromNatural v2) mod (symIntegerFromNatural ac.ac_all))))); (*0*) +("DW_OP_mod", sym_natural_of_hex "0x1d", [] , OpSem_binary (fun ac v1 v2 -> Just (v1 mod v2))); (*0*) +("DW_OP_mul", sym_natural_of_hex "0x1e", [] , OpSem_binary (fun ac v1 v2 -> Just (partialSymNaturalFromInteger ((symIntegerFromNatural v1 * symIntegerFromNatural v2) mod (symIntegerFromNatural ac.ac_all))))); (*0*) +("DW_OP_neg", sym_natural_of_hex "0x1f", [] , OpSem_unary (fun ac v -> if v < ac.ac_half then Just (ac.ac_max - v) else if v=ac.ac_half then Nothing else Just (ac.ac_all - v))); (*0*) +("DW_OP_not", sym_natural_of_hex "0x20", [] , OpSem_unary (fun ac v -> Just (sym_natural_lxor v ac.ac_max))); (*0*) +("DW_OP_or", sym_natural_of_hex "0x21", [] , OpSem_binary (fun ac v1 v2 -> Just (sym_natural_lor v1 v2))); (*0*) +("DW_OP_plus", sym_natural_of_hex "0x22", [] , OpSem_binary (fun ac v1 v2 -> Just ((v1 + v2) mod ac.ac_all))); (*0*) +("DW_OP_plus_uconst", sym_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' = (v+n) mod ac.ac_all in Just (v'::vs) | [] -> Nothing end | _ -> Nothing end)); (*1*) (* ULEB128 addend *) +("DW_OP_shl", sym_natural_of_hex "0x24", [] , OpSem_binary (fun ac v1 v2 -> if v2 >= ac.ac_bitwidth then Just 0 else Just (sym_natural_nat_shift_left v1 (natFromSymNatural v2)))); (*0*) +("DW_OP_shr", sym_natural_of_hex "0x25", [] , OpSem_binary (fun ac v1 v2 -> if v2 >= ac.ac_bitwidth then Just 0 else Just (sym_natural_nat_shift_right v1 (natFromSymNatural v2)))); (*0*) +("DW_OP_shra", sym_natural_of_hex "0x26", [] , OpSem_binary (fun ac v1 v2 -> if v1 < ac.ac_half then (if v2 >= ac.ac_bitwidth then Just 0 else Just (sym_natural_nat_shift_right v1 (natFromSymNatural v2))) else (if v2 >= ac.ac_bitwidth then Just ac.ac_max else Just (ac.ac_max - (sym_natural_nat_shift_right (ac.ac_max - v1) (natFromSymNatural v2)))))); (*0*) +("DW_OP_xor", sym_natural_of_hex "0x27", [] , OpSem_binary (fun ac v1 v2 -> Just (sym_natural_lxor v1 v2))); (*0*) +("DW_OP_skip", sym_natural_of_hex "0x2f", [OAT_sint16] , OpSem_not_supported); (*1*) (* signed 2-byte constant *) +("DW_OP_bra", sym_natural_of_hex "0x28", [OAT_sint16] , OpSem_not_supported); (*1*) (* signed 2-byte constant *) +("DW_OP_eq", sym_natural_of_hex "0x29", [] , OpSem_not_supported); (*0*) +("DW_OP_ge", sym_natural_of_hex "0x2a", [] , OpSem_not_supported); (*0*) +("DW_OP_gt", sym_natural_of_hex "0x2b", [] , OpSem_not_supported); (*0*) +("DW_OP_le", sym_natural_of_hex "0x2c", [] , OpSem_not_supported); (*0*) +("DW_OP_lt", sym_natural_of_hex "0x2d", [] , OpSem_not_supported); (*0*) +("DW_OP_ne", sym_natural_of_hex "0x2e", [] , OpSem_not_supported); (*0*) +("DW_OP_lit0", sym_natural_of_hex "0x30", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) (* literals 0..31 =(DW_OP_lit0 + literal) *) +("DW_OP_lit1", sym_natural_of_hex "0x31", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit2", sym_natural_of_hex "0x32", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit3", sym_natural_of_hex "0x33", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit4", sym_natural_of_hex "0x34", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit5", sym_natural_of_hex "0x35", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit6", sym_natural_of_hex "0x36", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit7", sym_natural_of_hex "0x37", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit8", sym_natural_of_hex "0x38", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit9", sym_natural_of_hex "0x39", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit10", sym_natural_of_hex "0x3a", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit11", sym_natural_of_hex "0x3b", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit12", sym_natural_of_hex "0x3c", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit13", sym_natural_of_hex "0x3d", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit14", sym_natural_of_hex "0x3e", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit15", sym_natural_of_hex "0x3f", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit16", sym_natural_of_hex "0x40", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit17", sym_natural_of_hex "0x41", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit18", sym_natural_of_hex "0x42", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit19", sym_natural_of_hex "0x43", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit20", sym_natural_of_hex "0x44", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit21", sym_natural_of_hex "0x45", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit22", sym_natural_of_hex "0x46", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit23", sym_natural_of_hex "0x47", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit24", sym_natural_of_hex "0x48", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit25", sym_natural_of_hex "0x49", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit26", sym_natural_of_hex "0x4a", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit27", sym_natural_of_hex "0x4b", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit28", sym_natural_of_hex "0x4c", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit29", sym_natural_of_hex "0x4d", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit30", sym_natural_of_hex "0x4e", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_lit31", sym_natural_of_hex "0x4f", [] , OpSem_opcode_lit (sym_natural_of_hex "0x30")); (*0*) +("DW_OP_reg0", sym_natural_of_hex "0x50", [] , OpSem_reg); (*1*) (* reg 0..31 = (DW_OP_reg0 + regnum) *) +("DW_OP_reg1", sym_natural_of_hex "0x51", [] , OpSem_reg); (*1*) +("DW_OP_reg2", sym_natural_of_hex "0x52", [] , OpSem_reg); (*1*) +("DW_OP_reg3", sym_natural_of_hex "0x53", [] , OpSem_reg); (*1*) +("DW_OP_reg4", sym_natural_of_hex "0x54", [] , OpSem_reg); (*1*) +("DW_OP_reg5", sym_natural_of_hex "0x55", [] , OpSem_reg); (*1*) +("DW_OP_reg6", sym_natural_of_hex "0x56", [] , OpSem_reg); (*1*) +("DW_OP_reg7", sym_natural_of_hex "0x57", [] , OpSem_reg); (*1*) +("DW_OP_reg8", sym_natural_of_hex "0x58", [] , OpSem_reg); (*1*) +("DW_OP_reg9", sym_natural_of_hex "0x59", [] , OpSem_reg); (*1*) +("DW_OP_reg10", sym_natural_of_hex "0x5a", [] , OpSem_reg); (*1*) +("DW_OP_reg11", sym_natural_of_hex "0x5b", [] , OpSem_reg); (*1*) +("DW_OP_reg12", sym_natural_of_hex "0x5c", [] , OpSem_reg); (*1*) +("DW_OP_reg13", sym_natural_of_hex "0x5d", [] , OpSem_reg); (*1*) +("DW_OP_reg14", sym_natural_of_hex "0x5e", [] , OpSem_reg); (*1*) +("DW_OP_reg15", sym_natural_of_hex "0x5f", [] , OpSem_reg); (*1*) +("DW_OP_reg16", sym_natural_of_hex "0x60", [] , OpSem_reg); (*1*) +("DW_OP_reg17", sym_natural_of_hex "0x61", [] , OpSem_reg); (*1*) +("DW_OP_reg18", sym_natural_of_hex "0x62", [] , OpSem_reg); (*1*) +("DW_OP_reg19", sym_natural_of_hex "0x63", [] , OpSem_reg); (*1*) +("DW_OP_reg20", sym_natural_of_hex "0x64", [] , OpSem_reg); (*1*) +("DW_OP_reg21", sym_natural_of_hex "0x65", [] , OpSem_reg); (*1*) +("DW_OP_reg22", sym_natural_of_hex "0x66", [] , OpSem_reg); (*1*) +("DW_OP_reg23", sym_natural_of_hex "0x67", [] , OpSem_reg); (*1*) +("DW_OP_reg24", sym_natural_of_hex "0x68", [] , OpSem_reg); (*1*) +("DW_OP_reg25", sym_natural_of_hex "0x69", [] , OpSem_reg); (*1*) +("DW_OP_reg26", sym_natural_of_hex "0x6a", [] , OpSem_reg); (*1*) +("DW_OP_reg27", sym_natural_of_hex "0x6b", [] , OpSem_reg); (*1*) +("DW_OP_reg28", sym_natural_of_hex "0x6c", [] , OpSem_reg); (*1*) +("DW_OP_reg29", sym_natural_of_hex "0x6d", [] , OpSem_reg); (*1*) +("DW_OP_reg30", sym_natural_of_hex "0x6e", [] , OpSem_reg); (*1*) +("DW_OP_reg31", sym_natural_of_hex "0x6f", [] , OpSem_reg); (*1*) +("DW_OP_breg0", sym_natural_of_hex "0x70", [OAT_SLEB128] , OpSem_breg); (*1*) (* base register 0..31 = (DW_OP_breg0 + regnum) *) +("DW_OP_breg1", sym_natural_of_hex "0x71", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg2", sym_natural_of_hex "0x72", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg3", sym_natural_of_hex "0x73", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg4", sym_natural_of_hex "0x74", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg5", sym_natural_of_hex "0x75", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg6", sym_natural_of_hex "0x76", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg7", sym_natural_of_hex "0x77", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg8", sym_natural_of_hex "0x78", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg9", sym_natural_of_hex "0x79", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg10", sym_natural_of_hex "0x7a", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg11", sym_natural_of_hex "0x7b", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg12", sym_natural_of_hex "0x7c", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg13", sym_natural_of_hex "0x7d", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg14", sym_natural_of_hex "0x7e", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg15", sym_natural_of_hex "0x7f", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg16", sym_natural_of_hex "0x80", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg17", sym_natural_of_hex "0x81", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg18", sym_natural_of_hex "0x82", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg19", sym_natural_of_hex "0x83", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg20", sym_natural_of_hex "0x84", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg21", sym_natural_of_hex "0x85", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg22", sym_natural_of_hex "0x86", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg23", sym_natural_of_hex "0x87", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg24", sym_natural_of_hex "0x88", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg25", sym_natural_of_hex "0x89", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg26", sym_natural_of_hex "0x8a", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg27", sym_natural_of_hex "0x8b", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg28", sym_natural_of_hex "0x8c", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg29", sym_natural_of_hex "0x8d", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg30", sym_natural_of_hex "0x8e", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_breg31", sym_natural_of_hex "0x8f", [OAT_SLEB128] , OpSem_breg); (*1*) +("DW_OP_regx", sym_natural_of_hex "0x90", [OAT_ULEB128] , OpSem_lit); (*1*) (* ULEB128 register *) +("DW_OP_fbreg", sym_natural_of_hex "0x91", [OAT_SLEB128] , OpSem_fbreg); (*1*) (* SLEB128 offset *) +("DW_OP_bregx", sym_natural_of_hex "0x92", [OAT_ULEB128; OAT_SLEB128] , OpSem_bregx); (*2*) (* ULEB128 register followed by SLEB128 offset *) +("DW_OP_piece", sym_natural_of_hex "0x93", [OAT_ULEB128] , OpSem_piece); (*1*) (* ULEB128 size of piece addressed *) +("DW_OP_deref_size", sym_natural_of_hex "0x94", [OAT_uint8] , OpSem_deref_size); (*1*) (* 1-byte size of data retrieved *) +("DW_OP_xderef_size", sym_natural_of_hex "0x95", [OAT_uint8] , OpSem_not_supported); (*1*) (* 1-byte size of data retrieved *) +("DW_OP_nop", sym_natural_of_hex "0x96", [] , OpSem_nop); (*0*) +("DW_OP_push_object_address", sym_natural_of_hex "0x97", [] , OpSem_not_supported); (*0*) +("DW_OP_call2", sym_natural_of_hex "0x98", [OAT_uint16] , OpSem_not_supported); (*1*) (* 2-byte offset of DIE *) +("DW_OP_call4", sym_natural_of_hex "0x99", [OAT_uint32] , OpSem_not_supported); (*1*) (* 4-byte offset of DIE *) +("DW_OP_call_ref", sym_natural_of_hex "0x9a", [OAT_dwarf_format_t] , OpSem_not_supported); (*1*) (* 4- or 8-byte offset of DIE *) +("DW_OP_form_tls_address", sym_natural_of_hex "0x9b", [] , OpSem_not_supported); (*0*) +("DW_OP_call_frame_cfa", sym_natural_of_hex "0x9c", [] , OpSem_call_frame_cfa); (*0*) +("DW_OP_bit_piece", sym_natural_of_hex "0x9d", [OAT_ULEB128; OAT_ULEB128] , OpSem_bit_piece); (*2*) (* ULEB128 size followed by ULEB128 offset *) +("DW_OP_implicit_value", sym_natural_of_hex "0x9e", [OAT_block] , OpSem_implicit_value); (*2*) (* ULEB128 size followed by block of that size *) +("DW_OP_stack_value", sym_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", [] , ); +("DW_OP_lo_user", sym_natural_of_hex "0xe0", [] , ); +("DW_OP_hi_user", sym_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) +("DW_GNU_OP_entry_value", sym_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", sym_natural_of_hex "0xf2", [OAT_dwarf_format_t;OAT_SLEB128], OpSem_not_supported) ] -let vDW_OP_reg0 = natural_of_hex "0x50" -let vDW_OP_breg0 = natural_of_hex "0x70" +let vDW_OP_reg0 = sym_natural_of_hex "0x50" +let vDW_OP_breg0 = sym_natural_of_hex "0x70" (* call frame instruction encoding *) -let call_frame_instruction_encoding : list (string * natural * natural * list call_frame_argument_type * ((list call_frame_argument_value) -> maybe call_frame_instruction)) = [ +let call_frame_instruction_encoding : list (string * sym_natural * sym_natural * list call_frame_argument_type * ((list call_frame_argument_value) -> maybe call_frame_instruction)) = [ (* high-order 2 bits low-order 6 bits uniformly parsed arguments *) (* instructions using low-order 6 bits for first argument *) @@ -1247,53 +1295,53 @@ let call_frame_instruction_encoding : list (string * natural * natural * list ca ("DW_CFA_restore", 3, 0,(*register*) []); *) (* instructions using low-order 6 bits as part of opcode *) -("DW_CFA_nop", 0, natural_of_hex "0x00", [], (* *) +("DW_CFA_nop", 0, sym_natural_of_hex "0x00", [], (* *) fun avs -> match avs with [] -> Just (DW_CFA_nop) | _ -> Nothing end); -("DW_CFA_set_loc", 0, natural_of_hex "0x01", [CFAT_address], (* address *) +("DW_CFA_set_loc", 0, sym_natural_of_hex "0x01", [CFAT_address], (* address *) fun avs -> match avs with [CFAV_address a] -> Just (DW_CFA_set_loc a) | _ -> Nothing end); -("DW_CFA_advance_loc1", 0, natural_of_hex "0x02", [CFAT_delta1], (* 1-byte delta *) +("DW_CFA_advance_loc1", 0, sym_natural_of_hex "0x02", [CFAT_delta1], (* 1-byte delta *) fun avs -> match avs with [CFAV_delta d] -> Just (DW_CFA_advance_loc1 d) | _ -> Nothing end); -("DW_CFA_advance_loc2", 0, natural_of_hex "0x03", [CFAT_delta2], (* 2-byte delta *) +("DW_CFA_advance_loc2", 0, sym_natural_of_hex "0x03", [CFAT_delta2], (* 2-byte delta *) fun avs -> match avs with [CFAV_delta d] -> Just (DW_CFA_advance_loc2 d) | _ -> Nothing end); -("DW_CFA_advance_loc4", 0, natural_of_hex "0x04", [CFAT_delta4], (* 4-byte delta *) +("DW_CFA_advance_loc4", 0, sym_natural_of_hex "0x04", [CFAT_delta4], (* 4-byte delta *) fun avs -> match avs with [CFAV_delta d] -> Just (DW_CFA_advance_loc4 d) | _ -> Nothing end); -("DW_CFA_offset_extended", 0, natural_of_hex "0x05", [CFAT_register; CFAT_offset], (* ULEB128 register ULEB128 offset *) +("DW_CFA_offset_extended", 0, sym_natural_of_hex "0x05", [CFAT_register; CFAT_offset], (* ULEB128 register ULEB128 offset *) fun avs -> match avs with [CFAV_register r; CFAV_offset n] -> Just (DW_CFA_offset_extended r n) | _ -> Nothing end); -("DW_CFA_restore_extended", 0, natural_of_hex "0x06", [CFAT_register], (* ULEB128 register *) +("DW_CFA_restore_extended", 0, sym_natural_of_hex "0x06", [CFAT_register], (* ULEB128 register *) fun avs -> match avs with [CFAV_register r] -> Just (DW_CFA_restore_extended r) | _ -> Nothing end); -("DW_CFA_undefined", 0, natural_of_hex "0x07", [CFAT_register], (* ULEB128 register *) +("DW_CFA_undefined", 0, sym_natural_of_hex "0x07", [CFAT_register], (* ULEB128 register *) fun avs -> match avs with [CFAV_register r] -> Just (DW_CFA_undefined r) | _ -> Nothing end); -("DW_CFA_same_value", 0, natural_of_hex "0x08", [CFAT_register], (* ULEB128 register *) +("DW_CFA_same_value", 0, sym_natural_of_hex "0x08", [CFAT_register], (* ULEB128 register *) fun avs -> match avs with [CFAV_register r] -> Just (DW_CFA_same_value r) | _ -> Nothing end); -("DW_CFA_register", 0, natural_of_hex "0x09", [CFAT_register; CFAT_register], (* ULEB128 register ULEB128 register *) +("DW_CFA_register", 0, sym_natural_of_hex "0x09", [CFAT_register; CFAT_register], (* ULEB128 register ULEB128 register *) fun avs -> match avs with [CFAV_register r1; CFAV_register r2] -> Just (DW_CFA_register r1 r2) | _ -> Nothing end); -("DW_CFA_remember_state", 0, natural_of_hex "0x0a", [], (* *) +("DW_CFA_remember_state", 0, sym_natural_of_hex "0x0a", [], (* *) fun avs -> match avs with [] -> Just (DW_CFA_remember_state) | _ -> Nothing end); -("DW_CFA_restore_state", 0, natural_of_hex "0x0b", [], (* *) +("DW_CFA_restore_state", 0, sym_natural_of_hex "0x0b", [], (* *) fun avs -> match avs with [] -> Just (DW_CFA_restore_state) | _ -> Nothing end); -("DW_CFA_def_cfa", 0, natural_of_hex "0x0c", [CFAT_register; CFAT_offset], (* ULEB128 register ULEB128 offset *) +("DW_CFA_def_cfa", 0, sym_natural_of_hex "0x0c", [CFAT_register; CFAT_offset], (* ULEB128 register ULEB128 offset *) fun avs -> match avs with [CFAV_register r; CFAV_offset n] -> Just (DW_CFA_def_cfa r n) | _ -> Nothing end); -("DW_CFA_def_cfa_register", 0, natural_of_hex "0x0d", [CFAT_register], (* ULEB128 register *) +("DW_CFA_def_cfa_register", 0, sym_natural_of_hex "0x0d", [CFAT_register], (* ULEB128 register *) fun avs -> match avs with [CFAV_register r] -> Just (DW_CFA_def_cfa_register r) | _ -> Nothing end); -("DW_CFA_def_cfa_offset", 0, natural_of_hex "0x0e", [CFAT_offset], (* ULEB128 offset *) +("DW_CFA_def_cfa_offset", 0, sym_natural_of_hex "0x0e", [CFAT_offset], (* ULEB128 offset *) fun avs -> match avs with [CFAV_offset n] -> Just (DW_CFA_def_cfa_offset n) | _ -> Nothing end); -("DW_CFA_def_cfa_expression", 0, natural_of_hex "0x0f", [CFAT_block], (* BLOCK *) +("DW_CFA_def_cfa_expression", 0, sym_natural_of_hex "0x0f", [CFAT_block], (* BLOCK *) fun avs -> match avs with [CFAV_block b] -> Just (DW_CFA_def_cfa_expression b) | _ -> Nothing end); -("DW_CFA_expression", 0, natural_of_hex "0x10", [CFAT_register; CFAT_block], (* ULEB128 register BLOCK *) +("DW_CFA_expression", 0, sym_natural_of_hex "0x10", [CFAT_register; CFAT_block], (* ULEB128 register BLOCK *) fun avs -> match avs with [CFAV_register r; CFAV_block b] -> Just (DW_CFA_expression r b) | _ -> Nothing end); -("DW_CFA_offset_extended_sf", 0, natural_of_hex "0x11", [CFAT_register; CFAT_sfoffset], (* ULEB128 register SLEB128 offset *) +("DW_CFA_offset_extended_sf", 0, sym_natural_of_hex "0x11", [CFAT_register; CFAT_sfoffset], (* ULEB128 register SLEB128 offset *) fun avs -> match avs with [CFAV_register r; CFAV_sfoffset i] -> Just (DW_CFA_offset_extended_sf r i) | _ -> Nothing end); -("DW_CFA_def_cfa_sf", 0, natural_of_hex "0x12", [CFAT_register; CFAT_sfoffset], (* ULEB128 register SLEB128 offset *) +("DW_CFA_def_cfa_sf", 0, sym_natural_of_hex "0x12", [CFAT_register; CFAT_sfoffset], (* ULEB128 register SLEB128 offset *) fun avs -> match avs with [CFAV_register r; CFAV_sfoffset i] -> Just (DW_CFA_def_cfa_sf r i) | _ -> Nothing end); -("DW_CFA_def_cfa_offset_sf", 0, natural_of_hex "0x13", [CFAT_sfoffset], (* SLEB128 offset *) +("DW_CFA_def_cfa_offset_sf", 0, sym_natural_of_hex "0x13", [CFAT_sfoffset], (* SLEB128 offset *) fun avs -> match avs with [CFAV_sfoffset i] -> Just (DW_CFA_def_cfa_offset_sf i) | _ -> Nothing end); -("DW_CFA_val_offset", 0, natural_of_hex "0x14", [CFAT_register; CFAT_offset], (* ULEB128 ULEB128 *) +("DW_CFA_val_offset", 0, sym_natural_of_hex "0x14", [CFAT_register; CFAT_offset], (* ULEB128 ULEB128 *) fun avs -> match avs with [CFAV_register r; CFAV_offset n] -> Just (DW_CFA_val_offset r n) | _ -> Nothing end); -("DW_CFA_val_offset_sf", 0, natural_of_hex "0x15", [CFAT_register; CFAT_sfoffset], (* ULEB128 SLEB128 *) +("DW_CFA_val_offset_sf", 0, sym_natural_of_hex "0x15", [CFAT_register; CFAT_sfoffset], (* ULEB128 SLEB128 *) fun avs -> match avs with [CFAV_register r; CFAV_sfoffset i] -> Just (DW_CFA_val_offset_sf r i) | _ -> Nothing end); -("DW_CFA_val_expression", 0, natural_of_hex "0x16", [CFAT_register; CFAT_block], (* ULEB128 BLOCK *) +("DW_CFA_val_expression", 0, sym_natural_of_hex "0x16", [CFAT_register; CFAT_block], (* ULEB128 BLOCK *) fun avs -> match avs with [CFAV_register r; CFAV_block b] -> Just (DW_CFA_val_expression r b) | _ -> Nothing end); -("DW_CFA_AARCH64_negate_ra_state", 0, natural_of_hex "0x2d", [], (* *) +("DW_CFA_AARCH64_negate_ra_state", 0, sym_natural_of_hex "0x2d", [], (* *) fun avs -> match avs with [] -> Just (DW_CFA_AARCH64_negate_ra_state) | _ -> Nothing end); ] (* @@ -1310,55 +1358,55 @@ p10 says "The RA_SIGN_STATE pseudo-register records whether the return address h For our purposes it seems fine to nop-this. *) (* -("DW_CFA_lo_user", 0, natural_of_hex "0x1c", []); (* *) -("DW_CFA_hi_user", 0, natural_of_hex "0x3f", []); (* *) +("DW_CFA_lo_user", 0, sym_natural_of_hex "0x1c", []); (* *) +("DW_CFA_hi_user", 0, sym_natural_of_hex "0x3f", []); (* *) *) (* line number encodings *) let line_number_standard_encodings = [ - ("DW_LNS_copy" , natural_of_hex "0x01", [ ], + ("DW_LNS_copy" , sym_natural_of_hex "0x01", [ ], fun lnvs -> match lnvs with [] -> Just DW_LNS_copy | _ -> Nothing end); - ("DW_LNS_advance_pc" , natural_of_hex "0x02", [LNAT_ULEB128 ], + ("DW_LNS_advance_pc" , sym_natural_of_hex "0x02", [LNAT_ULEB128 ], fun lnvs -> match lnvs with [LNAV_ULEB128 n] -> Just (DW_LNS_advance_pc n) | _ -> Nothing end); - ("DW_LNS_advance_line" , natural_of_hex "0x03", [LNAT_SLEB128 ], + ("DW_LNS_advance_line" , sym_natural_of_hex "0x03", [LNAT_SLEB128 ], fun lnvs -> match lnvs with [LNAV_SLEB128 i] -> Just (DW_LNS_advance_line i) | _ -> Nothing end); - ("DW_LNS_set_file" , natural_of_hex "0x04", [LNAT_ULEB128 ], + ("DW_LNS_set_file" , sym_natural_of_hex "0x04", [LNAT_ULEB128 ], fun lnvs -> match lnvs with [LNAV_ULEB128 n] -> Just (DW_LNS_set_file n) | _ -> Nothing end); - ("DW_LNS_set_column" , natural_of_hex "0x05", [LNAT_ULEB128 ], + ("DW_LNS_set_column" , sym_natural_of_hex "0x05", [LNAT_ULEB128 ], fun lnvs -> match lnvs with [LNAV_ULEB128 n] -> Just (DW_LNS_set_column n) | _ -> Nothing end); - ("DW_LNS_negate_stmt" , natural_of_hex "0x06", [ ], + ("DW_LNS_negate_stmt" , sym_natural_of_hex "0x06", [ ], fun lnvs -> match lnvs with [] -> Just (DW_LNS_negate_stmt) | _ -> Nothing end); - ("DW_LNS_set_basic_block" , natural_of_hex "0x07", [ ], + ("DW_LNS_set_basic_block" , sym_natural_of_hex "0x07", [ ], fun lnvs -> match lnvs with [] -> Just (DW_LNS_set_basic_block) | _ -> Nothing end); - ("DW_LNS_const_add_pc" , natural_of_hex "0x08", [ ], + ("DW_LNS_const_add_pc" , sym_natural_of_hex "0x08", [ ], fun lnvs -> match lnvs with [] -> Just (DW_LNS_const_add_pc) | _ -> Nothing end); - ("DW_LNS_fixed_advance_pc" , natural_of_hex "0x09", [LNAT_uint16 ], + ("DW_LNS_fixed_advance_pc" , sym_natural_of_hex "0x09", [LNAT_uint16 ], fun lnvs -> match lnvs with [LNAV_uint16 n] -> Just (DW_LNS_fixed_advance_pc n) | _ -> Nothing end); - ("DW_LNS_set_prologue_end" , natural_of_hex "0x0a", [ ], + ("DW_LNS_set_prologue_end" , sym_natural_of_hex "0x0a", [ ], fun lnvs -> match lnvs with [] -> Just (DW_LNS_set_prologue_end) | _ -> Nothing end); - ("DW_LNS_set_epilogue_begin" , natural_of_hex "0x0b", [ ], + ("DW_LNS_set_epilogue_begin" , sym_natural_of_hex "0x0b", [ ], fun lnvs -> match lnvs with [] -> Just (DW_LNS_set_epilogue_begin) | _ -> Nothing end); - ("DW_LNS_set_isa" , natural_of_hex "0x0c", [LNAT_ULEB128 ], + ("DW_LNS_set_isa" , sym_natural_of_hex "0x0c", [LNAT_ULEB128 ], fun lnvs -> match lnvs with [LNAV_ULEB128 n] -> Just (DW_LNS_set_isa n) | _ -> Nothing end) ] let line_number_extended_encodings = [ - ("DW_LNE_end_sequence" , natural_of_hex "0x01", [], + ("DW_LNE_end_sequence" , sym_natural_of_hex "0x01", [], fun lnvs -> match lnvs with [] -> Just (DW_LNE_end_sequence) | _ -> Nothing end); - ("DW_LNE_set_address" , natural_of_hex "0x02", [LNAT_address], + ("DW_LNE_set_address" , sym_natural_of_hex "0x02", [LNAT_address], fun lnvs -> match lnvs with [LNAV_address n] -> Just (DW_LNE_set_address n) | _ -> Nothing end); - ("DW_LNE_define_file" , natural_of_hex "0x03", [LNAT_string; LNAT_ULEB128; LNAT_ULEB128; LNAT_ULEB128], + ("DW_LNE_define_file" , sym_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] -> Just (DW_LNE_define_file s n1 n2 n3) | _ -> Nothing end); - ("DW_LNE_set_discriminator" , natural_of_hex "0x04", [LNAT_ULEB128], + ("DW_LNE_set_discriminator" , sym_natural_of_hex "0x04", [LNAT_ULEB128], fun lnvs -> match lnvs with [LNAV_ULEB128 n] -> Just (DW_LNE_set_discriminator n) | _ -> Nothing end) (* 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"); +(DW_LNE_lo_user , sym_natural_of_hex "0x80", "DW_LNE_lo_user"); +(DW_LNE_hi_user , sym_natural_of_hex "0xff", "DW_LNE_hi_user"); *) @@ -1367,26 +1415,26 @@ let line_number_extended_encodings = [ (* base type attribute encoding *) let base_type_attribute_encodings = [ - ("DW_ATE_address" , natural_of_hex "0x01"); - ("DW_ATE_boolean" , natural_of_hex "0x02"); - ("DW_ATE_complex_float" , natural_of_hex "0x03"); - ("DW_ATE_float" , natural_of_hex "0x04"); - ("DW_ATE_signed" , natural_of_hex "0x05"); - ("DW_ATE_signed_char" , natural_of_hex "0x06"); - ("DW_ATE_unsigned" , natural_of_hex "0x07"); - ("DW_ATE_unsigned_char" , natural_of_hex "0x08"); - ("DW_ATE_imaginary_float" , natural_of_hex "0x09"); - ("DW_ATE_packed_decimal" , natural_of_hex "0x0a"); - ("DW_ATE_numeric_string" , natural_of_hex "0x0b"); - ("DW_ATE_edited" , natural_of_hex "0x0c"); - ("DW_ATE_signed_fixed" , natural_of_hex "0x0d"); - ("DW_ATE_unsigned_fixed" , natural_of_hex "0x0e"); - ("DW_ATE_decimal_float" , natural_of_hex "0x0f"); - ("DW_ATE_UTF" , natural_of_hex "0x10"); - ("DW_ATE_lo_user" , natural_of_hex "0x80"); - ("DW_ATE_signed_capability_hack_a0" , natural_of_hex "0xa0"); - ("DW_ATE_unsigned_capability_hack_a1" , natural_of_hex "0xa1"); - ("DW_ATE_hi_user" , natural_of_hex "0xff") + ("DW_ATE_address" , sym_natural_of_hex "0x01"); + ("DW_ATE_boolean" , sym_natural_of_hex "0x02"); + ("DW_ATE_complex_float" , sym_natural_of_hex "0x03"); + ("DW_ATE_float" , sym_natural_of_hex "0x04"); + ("DW_ATE_signed" , sym_natural_of_hex "0x05"); + ("DW_ATE_signed_char" , sym_natural_of_hex "0x06"); + ("DW_ATE_unsigned" , sym_natural_of_hex "0x07"); + ("DW_ATE_unsigned_char" , sym_natural_of_hex "0x08"); + ("DW_ATE_imaginary_float" , sym_natural_of_hex "0x09"); + ("DW_ATE_packed_decimal" , sym_natural_of_hex "0x0a"); + ("DW_ATE_numeric_string" , sym_natural_of_hex "0x0b"); + ("DW_ATE_edited" , sym_natural_of_hex "0x0c"); + ("DW_ATE_signed_fixed" , sym_natural_of_hex "0x0d"); + ("DW_ATE_unsigned_fixed" , sym_natural_of_hex "0x0e"); + ("DW_ATE_decimal_float" , sym_natural_of_hex "0x0f"); + ("DW_ATE_UTF" , sym_natural_of_hex "0x10"); + ("DW_ATE_lo_user" , sym_natural_of_hex "0x80"); + ("DW_ATE_signed_capability_hack_a0" , sym_natural_of_hex "0xa0"); + ("DW_ATE_unsigned_capability_hack_a1" , sym_natural_of_hex "0xa1"); + ("DW_ATE_hi_user" , sym_natural_of_hex "0xff") ] (** ************************************************************ *) @@ -1439,9 +1487,9 @@ let rec myfiltermaybe f xs = -val bytes_of_natural: endianness -> natural (*size*) -> natural (*value*) -> byte_sequence +val bytes_of_natural: endianness -> natural (*size*) -> natural (*value*) -> sym_byte_sequence let bytes_of_natural en size n = - byte_sequence_of_byte_list ( + sym_byte_sequence_of_byte_list ( if size = 8 then bytes_of_elf64_xword en (elf64_xword_of_natural n) else if size = 4 then @@ -1449,25 +1497,29 @@ let bytes_of_natural en size n = else Assert_extra.failwith "bytes_of_natural given size that is not 4 or 8") +let bytes_of_sym_natural en size n = bytes_of_natural en (sym_natural_expect_const size (*"bytes_of_sym_natural size"*)) (sym_natural_expect_const n (*"bytes_of_sym_natural n"*)) + let rec natural_of_bytes_little bs : natural = - match read_char bs with + match sym_read_char bs with | Fail _ -> 0 | Success (b, bs') -> natural_of_byte b + 256 * natural_of_bytes_little bs' end let rec natural_of_bytes_big acc bs = - match read_char bs with + match sym_read_char bs with | Fail _ -> acc | Success (b, bs') -> natural_of_bytes_big (natural_of_byte b + 256 * acc) bs' end -val natural_of_bytes: endianness -> byte_sequence -> natural +val natural_of_bytes: endianness -> sym_byte_sequence -> natural let natural_of_bytes en bs = match en with | Little -> natural_of_bytes_little bs | Big -> natural_of_bytes_big 0 bs end +let sym_natural_of_bytes en bs = sym_natural_const (natural_of_bytes en bs) + (* TODO: generalise *) (* @@ -1517,12 +1569,12 @@ let rec mytake' (n:natural) acc xs = | (_, x::xs') -> mytake' (n-1) (x::acc) xs' end -val mytake : forall 'a. natural -> (list 'a) -> maybe (list 'a * list 'a) -let mytake n xs = mytake' n [] xs +val mytake : forall 'a. sym_natural -> (list 'a) -> maybe (list 'a * list 'a) +let mytake n xs = mytake' (sym_natural_expect_const n (*"mytake"*)) [] xs -val mynth : forall 'a. natural -> (list 'a) -> maybe 'a -let rec mynth (n:natural) xs = - match (n,xs) with +val mynth : forall 'a. sym_natural -> (list 'a) -> maybe 'a +let rec mynth (n:sym_natural) xs = + match (sym_natural_expect_const n (*"mynth"*),xs) with | (0, x::xs') -> Just x | (0, []) -> Nothing (*Assert_extra.failwith "mynth"*) | (_, x::xs') -> mynth (n-1) xs' @@ -1534,6 +1586,9 @@ let rec mynth (n:natural) xs = let pphexplain n = unsafe_hex_string_of_natural 0 n let pphex n = "0x" ^ pphexplain n +let pphexplain_sym = sym_natural_pp pphexplain +let pphex_sym = sym_natural_pp pphex + val abs : integer -> natural (*declare hol target_rep function abs = `int_of_num` *) declare ocaml target_rep function abs = `Nat_big_num.abs` @@ -1543,15 +1598,15 @@ declare coq target_rep function abs n = (`Zpred` (`Zpos` (`P_of_succ_nat` n let pphex_integer n = if n<0 then "-" ^ pphex (abs n) else pphex (abs n) -let ppbytes bs = show (List.map (fun x -> show x) (byte_list_of_byte_sequence bs)) +let ppbytes = sym_ppbytes let rec ppbytes2 n bs = - match read_char bs with + match sym_read_char bs with | Fail _ -> "" | Success (x,xs') -> "<" ^ pphex n ^ "> " ^ show x ^ "\n" ^ ppbytes2 (n+1) xs' end -let rec ppbytesplain (c:p_context) (n:natural) bs = show (natural_of_bytes c.endianness bs) +let rec ppbytesplain (c:p_context) (n:sym_natural) bs = show (natural_of_bytes c.endianness bs) (* unsafe_hex_string_of_uc_list (List.map unsigned_char_of_byte xs) (*match xs with | [] -> "" | x::xs' -> pphexplain x ^ ppbytesplain (n+1) xs' end*) *) @@ -1573,17 +1628,17 @@ let just_one s xs = -let max_address (as': natural) : natural = - match as' with - | 4 -> natural_of_hex "0xffffffff" - | 8 -> natural_of_hex "0xffffffffffffffff" +let max_address (as': sym_natural) : sym_natural = + match sym_natural_expect_const as' (*"max_addres"*) with + | 4 -> sym_natural_of_hex "0xffffffff" + | 8 -> sym_natural_of_hex "0xffffffffffffffff" | _ -> Assert_extra.failwith "max_address size not 4 or 8" end -let range_address (as': natural) : natural = - match as' with - | 4 -> natural_of_hex "0x100000000" - | 8 -> natural_of_hex "0x10000000000000000" +let range_address (as': sym_natural) : sym_natural = + match sym_natural_expect_const as' (*"max_addres"*) with + | 4 -> sym_natural_of_hex "0x100000000" + | 8 -> sym_natural_of_hex "0x10000000000000000" | _ -> Assert_extra.failwith "range_address size not 4 or 8" end @@ -1651,32 +1706,32 @@ let rec lookup_abCde_de z0 xyzwus = end -let pp_maybe ppf n = match ppf n with Just s -> s | Nothing -> "Unknown AT value: " ^ pphexplain n (*encoding not found: "" ^ pphex n*) end +let pp_maybe ppf n = match ppf n with Just s -> s | Nothing -> "Unknown AT value: " ^ pphexplain_sym n (*encoding not found: "" ^ pphex n*) end let pp_tag_encoding n = pp_maybe (fun n -> lookup_aB_a n tag_encodings) n let pp_attribute_encoding n = pp_maybe (fun n -> lookup_aBc_a n attribute_encodings) n let pp_attribute_form_encoding n = pp_maybe (fun n -> lookup_aBc_a n attribute_form_encodings) n let pp_operation_encoding n = pp_maybe (fun n -> lookup_aBcd_a n operation_encodings) n -let tag_encode (s: string) : natural = +let tag_encode (s: string) : sym_natural = match lookup_Ab_b s tag_encodings with | Just n -> n | Nothing -> Assert_extra.failwith ("tag_encode: \""^s^"\"") end -let attribute_encode (s: string) : natural = +let attribute_encode (s: string) : sym_natural = match lookup_Abc_b s attribute_encodings with | Just n -> n | Nothing -> Assert_extra.failwith ("attribute_encode: \""^s^"\"") end -let attribute_form_encode (s: string) : natural = +let attribute_form_encode (s: string) : sym_natural = match lookup_Abc_b s attribute_form_encodings with | Just n -> n | Nothing -> Assert_extra.failwith "attribute_form_encode" end -let base_type_attribute_encode (s: string) : natural = +let base_type_attribute_encode (s: string) : sym_natural = match lookup_Ab_b s base_type_attribute_encodings with | Just n -> n | Nothing -> Assert_extra.failwith "base_type_attribute_encode" @@ -1690,7 +1745,7 @@ let base_type_attribute_encode (s: string) : natural = (* parsing combinators *) -type parse_context = <| pc_bytes: byte_sequence; pc_offset: natural |> +type parse_context = <| pc_bytes: sym_byte_sequence; pc_offset: natural |> type parse_result 'a = | PR_success of 'a * parse_context @@ -1743,8 +1798,8 @@ val pr_post_map : forall 'a 'b. (parser 'a) -> ('a -> 'b) -> (parser 'b) let pr_post_map p f = 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 = fun pc -> pr_map (fun x -> (pc.pc_offset,x)) (p pc) +val pr_with_pos : forall 'a. (parser 'a) -> (parser (sym_natural * 'a)) +let pr_with_pos p = fun pc -> pr_map (fun x -> (sym_natural_const pc.pc_offset,x)) (p pc) val parse_pair : forall 'a 'b. (parser 'a) -> (parser 'b) -> (parser ('a * 'b)) @@ -1816,7 +1871,7 @@ let rec parse_parser_list ps = val parse_maybe : forall 'a. parser 'a -> parser (maybe 'a) let parse_maybe p = fun pc -> - match Byte_sequence.length pc.pc_bytes with + match sym_bs_length pc.pc_bytes with | 0 -> pr_return Nothing pc | _ -> match p pc with @@ -1836,10 +1891,10 @@ let parse_demaybe s p = end -val parse_restrict_length : forall 'a. natural -> parser 'a -> parser 'a +val parse_restrict_length : forall 'a. sym_natural -> parser 'a -> parser 'a let parse_restrict_length n p = fun pc -> - match partition n pc.pc_bytes with + match sym_partition (sym_natural_expect_const n (*"parse_strict_length"*)) pc.pc_bytes with | Fail _ -> Assert_extra.failwith "parse_restrict_length not given enough bytes" | Success (xs,ys) -> let pc' = <| pc_bytes = xs; pc_offset = pc.pc_offset |> in @@ -1851,88 +1906,94 @@ let parse_restrict_length n p = let parse_byte : parser(byte) = fun (pc:parse_context) -> - match read_char pc.pc_bytes with + match sym_read_char pc.pc_bytes with | Fail _ -> PR_fail "parse_byte" pc | Success (b,bs) -> PR_success b (<|pc_bytes=bs; pc_offset= pc.pc_offset + 1 |> ) end -let parse_n_bytes (n:natural) : parser (byte_sequence) = +let parse_n_bytes (n:sym_natural) : parser (sym_byte_sequence) = fun (pc:parse_context) -> - match partition n pc.pc_bytes with - | Fail _ -> PR_fail ("parse_n_bytes n=" ^ pphex n) pc + match sym_partition (sym_natural_expect_const n (*"parse_n_bytes"*)) pc.pc_bytes with + | Fail _ -> PR_fail ("parse_n_bytes n=" ^ pphex_sym n) pc | Success (xs,bs) -> - PR_success xs (<|pc_bytes=bs; pc_offset= pc.pc_offset + (Byte_sequence.length xs) |> ) + PR_success xs (<|pc_bytes=bs; pc_offset= pc.pc_offset + (sym_bs_length xs) |> ) end let bzero = byte_of_natural 0 -let parse_string : parser (byte_sequence) = +let parse_string : parser (sym_byte_sequence) = fun (pc:parse_context) -> - match find_byte pc.pc_bytes bzero with + match sym_find_byte pc.pc_bytes bzero with | Nothing -> PR_fail "parse_string" pc | Just n -> - pr_bind (parse_n_bytes n pc) (fun res pc -> + pr_bind (parse_n_bytes (sym_natural_const n) pc) (fun res pc -> (*todo find byte should respect relocs*) pr_bind (parse_byte pc) (fun _ pc -> pr_return res pc)) end (* parse a null-terminated string; return Nothing if it is empty, Just s otherwise *) -let parse_non_empty_string : parser (maybe byte_sequence) = +let parse_non_empty_string : parser (maybe sym_byte_sequence) = fun (pc:parse_context) -> pr_bind (parse_string pc) (fun str pc -> - if Byte_sequence.length str = 0 then + if sym_bs_length str = 0 then pr_return Nothing pc else pr_return (Just str) pc) -let parse_uint8 : parser natural = +(* TODO relocations *) +let parse_uint8 : parser sym_natural= fun (pc:parse_context) -> let _ = my_debug "uint8 " in - match read_char pc.pc_bytes with + match sym_read_char pc.pc_bytes with | Success (b, bytes) -> let v = natural_of_byte b in - PR_success v (<| pc_bytes = bytes; pc_offset = pc.pc_offset + 1 |>) + PR_success (sym_natural_const v) (<| pc_bytes = bytes; pc_offset = pc.pc_offset + 1 |>) | _ -> PR_fail "parse_uint32 not given enough bytes" pc end -let parse_uint8_constant (v:natural) : parser natural = +let parse_uint8_constant (v:sym_natural) : parser sym_natural= fun (pc:parse_context) -> let _ = my_debug "uint8_constant " in PR_success v pc - -let parse_uint16 c : parser natural = + +(* TODO relocations *) +let parse_uint16 c : parser sym_natural= fun (pc:parse_context) -> let _ = my_debug "uint16 " in - match read_2_bytes_be pc.pc_bytes with + match sym_read_2_bytes_be pc.pc_bytes with | Success ((b0,b1),bytes') -> let v = if c.endianness=Little then natural_of_byte b0 + 256*natural_of_byte b1 else natural_of_byte b1 + 256*natural_of_byte b0 in - PR_success v (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 2 |>) + PR_success (sym_natural_const v) (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 2 |>) | _ -> PR_fail "parse_uint32 not given enough bytes" pc end -let parse_uint32 c : parser natural = +(* TODO relocations *) +let parse_uint32 c : parser sym_natural= fun (pc:parse_context) -> let _ = my_debug "uint32 " in - match read_4_bytes_be pc.pc_bytes with - | Success ((b0,b1,b2,b3),bytes') -> + match sym_read_4_bytes_be_symbolic pc.pc_bytes with + | Success (Bytes (b0,b1,b2,b3),bytes') -> let v = if c.endianness=Little then natural_of_byte b0 + 256*natural_of_byte b1 + 256*256*natural_of_byte b2 + 256*256*256*natural_of_byte b3 else natural_of_byte b3 + 256*natural_of_byte b2 + 256*256*natural_of_byte b1 + 256*256*256*natural_of_byte b0 in - PR_success v (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 4 |>) + PR_success (sym_natural_const v) (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 4 |>) + | Success (Sym n, bytes') -> + PR_success n (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 4 |>) | _ -> PR_fail "parse_uint32 not given enough bytes" pc end -let parse_uint64 c : parser natural = +(* TODO relocations *) +let parse_uint64 c : parser sym_natural= fun (pc:parse_context) -> let _ = my_debug "uint64 " in - match read_8_bytes_be pc.pc_bytes with - | Success ((b0,b1,b2,b3,b4,b5,b6,b7),bytes') -> + match sym_read_8_bytes_be_symbolic pc.pc_bytes with + | Success (Bytes (b0,b1,b2,b3,b4,b5,b6,b7),bytes') -> (*TODO*) let v = if c.endianness=Little then natural_of_byte b0 + 256*natural_of_byte b1 + 256*256*natural_of_byte b2 + 256*256*256*natural_of_byte b3 + (256*256*256*256*(natural_of_byte b4 + 256*natural_of_byte b5 + 256*256*natural_of_byte b6 + 256*256*256*natural_of_byte b7)) @@ -1940,35 +2001,37 @@ let parse_uint64 c : parser natural = natural_of_byte b7 + 256*natural_of_byte b6 + 256*256*natural_of_byte b5 + 256*256*256*natural_of_byte b4 + (256*256*256*256*(natural_of_byte b3 + 256*natural_of_byte b2 + 256*256*natural_of_byte b1 + 256*256*256*natural_of_byte b0)) in - PR_success v (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 8 |>) + PR_success (sym_natural_const v) (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 8 |>) + | Success (Sym n, bytes') -> + PR_success n (<| pc_bytes = bytes'; pc_offset = pc.pc_offset + 8 |>) | _ -> PR_fail "parse_uint64 not given enough bytes" pc end -let integerFromTwosComplementNatural (n:natural) (half: natural) (all:integer) : integer = - if n < half then integerFromNatural n else integerFromNatural n - all -let partialTwosComplementNaturalFromInteger (i:integer) (half: natural) (all:integer) : natural = - if i >=0 && i < integerFromNatural half then partialNaturalFromInteger i - else if i >= (0-integerFromNatural half) && i < 0 then partialNaturalFromInteger (all + i) - else Assert_extra.failwith "partialTwosComplementNaturalFromInteger" +let integerFromTwosComplementNatural (n:sym_natural) (half: sym_natural) (all:sym_integer) : sym_integer = + if n < half then symIntegerFromNatural n else symIntegerFromNatural n - all +let partialTwosComplementNaturalFromInteger (i:sym_integer) (half: sym_natural) (all:sym_integer) : sym_natural = + if i >=0 && i < symIntegerFromNatural half then partialSymNaturalFromInteger i + else if i >= (0-symIntegerFromNatural half) && i < 0 then partialSymNaturalFromInteger (all + i) + else Assert_extra.failwith "partialTwosComplementNaturalFromInteger" -let parse_sint8 : parser integer = +let parse_sint8 : parser sym_integer = pr_post_map (parse_uint8) (fun n -> integerFromTwosComplementNatural n 128 256) -let parse_sint16 c : parser integer = +let parse_sint16 c : parser sym_integer = pr_post_map (parse_uint16 c) (fun n -> integerFromTwosComplementNatural n (128*256) (256*256)) -let parse_sint32 c : parser integer = +let parse_sint32 c : parser sym_integer = pr_post_map (parse_uint32 c) (fun n -> integerFromTwosComplementNatural n (128*256*256*256) (256*256*256*256)) -let parse_sint64 c : parser integer = +let parse_sint64 c : parser sym_integer = pr_post_map (parse_uint64 c) (fun n -> integerFromTwosComplementNatural n (128*256*256*256*256*256*256*256) (256*256*256*256*256*256*256*256)) let rec parse_ULEB128' (acc: natural) (shift_factor: natural) : parser natural = fun (pc:parse_context) -> let _ = my_debug "ULEB128' " in - match read_char pc.pc_bytes with + match sym_read_char pc.pc_bytes with | Success (b,bytes') -> let n = natural_of_byte b in let acc' = (natural_land n 127) * shift_factor + acc in @@ -1982,14 +2045,14 @@ let rec parse_ULEB128' (acc: natural) (shift_factor: natural) : parser natural = PR_fail "parse_ULEB128' not given enough bytes" pc end -let parse_ULEB128 : parser natural = +let parse_ULEB128 : parser sym_natural = fun (pc:parse_context) -> - parse_ULEB128' 0 1 pc + pr_map (fun x -> sym_natural_const x) (parse_ULEB128' 0 1 pc) let rec parse_SLEB128' (acc: natural) (shift_factor: natural) : parser (bool * natural * natural) = fun (pc:parse_context) -> let _ = my_debug "SLEB128' " in - match read_char pc.pc_bytes with + match sym_read_char pc.pc_bytes with | Success (b,bytes') -> let n = natural_of_byte b in let acc' = acc + (natural_land n 127) * shift_factor in @@ -2005,35 +2068,35 @@ let rec parse_SLEB128' (acc: natural) (shift_factor: natural) : parser (bool * n PR_fail "parse_SLEB128' not given enough bytes" pc end -let parse_SLEB128 : parser integer = +let parse_SLEB128 : parser sym_integer = pr_post_map (parse_SLEB128' 0 1) (fun (positive, shift_factor, acc) -> - if positive then integerFromNatural acc else integerFromNatural acc - integerFromNatural shift_factor) + sym_integer_const (if positive then integerFromNatural acc else integerFromNatural acc - integerFromNatural shift_factor)) -let parse_nonzero_ULEB128_pair : parser (maybe (natural*natural)) = +let parse_nonzero_ULEB128_pair : parser (maybe (sym_natural*sym_natural)) = let _ = my_debug "nonzero_ULEB128_pair " in pr_post_map (parse_pair parse_ULEB128 parse_ULEB128) (fun (n1,n2) -> if n1=0 && n2=0 then Nothing else Just (n1,n2)) -let parse_zero_terminated_ULEB128_pair_list : parser (list (natural*natural)) = +let parse_zero_terminated_ULEB128_pair_list : parser (list (sym_natural*sym_natural)) = let _ = my_debug "zero_terminated_ULEB128_pair_list " in parse_list parse_nonzero_ULEB128_pair -let parse_uintDwarfN c (df: dwarf_format) : parser natural = +let parse_uintDwarfN c (df: dwarf_format) : parser sym_natural = match df with - | Dwarf32 -> (parse_uint32 c) - | Dwarf64 -> (parse_uint64 c) - end + | Dwarf32 -> (parse_uint32 c) + | Dwarf64 -> (parse_uint64 c) + end -let parse_uint_address_size c (as': natural) : parser natural = - match as' with +let parse_uint_address_size c (as': sym_natural) : parser sym_natural = + match sym_natural_expect_const as' (**"parse_uint_address_size"*) with | 4 -> (parse_uint32 c) | 8 -> (parse_uint64 c) | _ -> Assert_extra.failwith ("cuh_address_size not 4 or 8: " ^ show as') end -let parse_uint_segment_selector_size c (ss: natural) : parser (maybe natural) = - match ss with +let parse_uint_segment_selector_size c (ss: sym_natural) : parser (maybe sym_natural) = + match sym_natural_expect_const ss (*"parse_uint_segment_selector_size_size"*) with | 0 -> pr_return Nothing | 1 -> pr_post_map (parse_uint8) (fun n -> Just n) | 2 -> pr_post_map (parse_uint16 c) (fun n -> Just n) @@ -2067,7 +2130,7 @@ let pp_abbreviation_declaration (x:abbreviation_declaration) = let pp_abbreviations_table (x:abbreviations_table) = - "offset: "^pphex x.at_offset^"\n" + "offset: "^pphex_sym x.at_offset^"\n" ^ String.concat "" (List.map (pp_abbreviation_declaration) x.at_table) (* print the distinct abbreviation tables used by all compilation units *) @@ -2082,7 +2145,7 @@ let rec remove_duplicates xys xys_acc = end let pp_abbreviations_tables (d:dwarf) = - let xs : list (natural * abbreviations_table) = + let xs : list (sym_natural * abbreviations_table) = List.map (fun cu -> (cu.cu_header.cuh_debug_abbrev_offset, cu.cu_abbreviations_table)) d.d_compilation_units in @@ -2118,29 +2181,29 @@ let parse_abbreviations_table c = (** debug_str entry *) -let rec null_terminated_bs (bs: byte_sequence) : byte_sequence = - match find_byte bs bzero with +let rec null_terminated_bs (bs: sym_byte_sequence) : sym_byte_sequence = + match sym_find_byte bs bzero with | Just i -> - match takebytes i bs with + match sym_takebytes i bs with | Success bs' -> bs' | Fail _ -> Assert_extra.failwith "find_byte or take_byte is broken" end | Nothing -> bs end -let pp_debug_str_entry (str: byte_sequence) (n: natural) : string = - match dropbytes n str with +let pp_debug_str_entry (str: sym_byte_sequence) (n: sym_natural) : string = + match sym_dropbytes (sym_natural_expect_const n (*"pp_debug_str_entry"*)) str with | Fail _ -> "strp beyond .debug_str extent" - | Success bs -> string_of_byte_sequence (null_terminated_bs bs) + | Success bs -> string_of_sym_byte_sequence (null_terminated_bs bs) end (** 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 -> pphex_integer n (* show n*) - | OAV_block n bs -> pphex n ^ " " ^ ppbytes bs + | OAV_natural n -> pphex_sym n + | OAV_integer n -> sym_integer_pp pphex_integer n (* show n*) + | OAV_block n bs -> pphex_sym n ^ " " ^ ppbytes bs end let pp_operation_semantics (os: operation_semantics) : string = @@ -2205,7 +2268,7 @@ let parse_operation c cuh pc = | PR_fail s pc' -> PR_success Nothing pc | PR_success code pc' -> match lookup_aBcd_acd code operation_encodings with - | Nothing -> PR_fail ("encoding not found: " ^ pphex code) pc + | Nothing -> PR_fail ("encoding not found: " ^ pphex_sym code) pc | Just (s,oats,opsem) -> let ps = List.map (parser_of_operation_argument_type c cuh) oats in (pr_post_map @@ -2225,20 +2288,20 @@ let parse_operations_bs c cuh bs : list operation = match parse_operations c cuh pc with | PR_fail s pc' -> Assert_extra.failwith ("parse_operations_bs fail: " ^ pp_parse_fail s pc') | PR_success ops pc' -> - let _ = if Byte_sequence.length pc'.pc_bytes <> 0 then Assert_extra.failwith ("parse_operations_bs extra non-parsed bytes") else () in + let _ = if sym_bs_length pc'.pc_bytes <> 0 then Assert_extra.failwith ("parse_operations_bs extra non-parsed bytes") else () in ops end -val parse_and_pp_operations : p_context -> compilation_unit_header -> byte_sequence -> string +val parse_and_pp_operations : p_context -> compilation_unit_header -> sym_byte_sequence -> string let parse_and_pp_operations c cuh bs = let pc = <|pc_bytes = bs; pc_offset = 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 Byte_sequence.length pc'.pc_bytes <> 0 then " Warning: extra non-parsed bytes" else "" + ^ if sym_bs_length pc'.pc_bytes <> 0 then " Warning: extra non-parsed bytes" else "" end @@ -2247,7 +2310,7 @@ let parse_and_pp_operations c cuh bs = val pp_attribute_value_plain : attribute_value -> string let pp_attribute_value_plain av = match av with - | AV_addr x -> "AV_addr " ^ pphex x + | AV_addr x -> "AV_addr " ^ pphex_sym x | AV_block n bs -> "AV_block " ^ show n ^ " " ^ ppbytes bs | AV_constantN n bs -> "AV_constantN " ^ show n ^ " " ^ ppbytes bs | AV_constant_SLEB128 i -> "AV_constant_SLEB128 " ^ show i @@ -2255,19 +2318,19 @@ let pp_attribute_value_plain av = | AV_exprloc n bs -> String.concat " " ["AV_exprloc"; show n; ppbytes bs] | AV_flag b -> "AV_flag " ^ show 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_byte_sequence bs - | AV_strp n -> "AV_sec_offset " ^ pphex n ^ " " + | AV_ref n -> "AV_ref " ^ pphex_sym n + | AV_ref_addr n -> "AV_ref_addr " ^ pphex_sym n + | AV_ref_sig8 n -> "AV_ref_sig8 " ^ pphex_sym n + | AV_sec_offset n -> "AV_sec_offset " ^ pphex_sym n + | AV_string bs -> string_of_sym_byte_sequence bs + | AV_strp n -> "AV_sec_offset " ^ pphex_sym n ^ " " end -val pp_attribute_value : p_context -> compilation_unit_header -> byte_sequence -> natural (*attribute tag*) -> attribute_value -> string +val pp_attribute_value : p_context -> compilation_unit_header -> sym_byte_sequence -> sym_natural (*attribute tag*) -> attribute_value -> string let pp_attribute_value c cuh str at av = match av with - | AV_addr x -> "AV_addr " ^ pphex x + | AV_addr x -> "AV_addr " ^ pphex_sym x | AV_block n bs -> "AV_block " ^ show n ^ " " ^ ppbytes bs ^ if at = attribute_encode "DW_AT_location" then " " ^ parse_and_pp_operations c cuh bs else "" | AV_constantN n bs -> "AV_constantN " ^ show n ^ " " ^ ppbytes bs @@ -2276,19 +2339,19 @@ let pp_attribute_value c cuh str at av = | AV_exprloc n bs -> String.concat " " ["AV_exprloc"; show n; ppbytes bs; parse_and_pp_operations c cuh bs] | AV_flag b -> "AV_flag " ^ show 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_byte_sequence bs - | AV_strp n -> "AV_sec_offset " ^ pphex n ^ " " + | AV_ref n -> "AV_ref " ^ pphex_sym n + | AV_ref_addr n -> "AV_ref_addr " ^ pphex_sym n + | AV_ref_sig8 n -> "AV_ref_sig8 " ^ pphex_sym n + | AV_sec_offset n -> "AV_sec_offset " ^ pphex_sym n + | AV_string bs -> string_of_sym_byte_sequence bs + | AV_strp n -> "AV_sec_offset " ^ pphex_sym n ^ " " ^ pp_debug_str_entry str n end -val pp_attribute_value_like_objdump : p_context -> compilation_unit_header -> byte_sequence -> natural (*attribute tag*) -> attribute_value -> string +val pp_attribute_value_like_objdump : p_context -> compilation_unit_header -> sym_byte_sequence -> sym_natural (*attribute tag*) -> attribute_value -> string let pp_attribute_value_like_objdump c cuh str at av = match av with - | AV_addr x -> (*"AV_addr " ^*) pphex x + | AV_addr x -> (*"AV_addr " ^*) pphex_sym x | AV_block n bs -> (*"AV_block " ^ show n ^ " " ^ ppbytes bs ^ if at = attribute_encode "DW_AT_location" then " " ^ parse_and_pp_operations c cuh bs else ""*) (* show n ^ " byte block: " *) ppbytesplain c n bs @@ -2299,21 +2362,21 @@ let pp_attribute_value_like_objdump c cuh str at av = | AV_exprloc n bs -> (*"AV_exprloc " ^ show n ^ " " ^*) ppbytes bs ^ " " ^ parse_and_pp_operations c cuh bs | AV_flag b -> (*"AV_flag " ^*)if b then "1" else "0" - | AV_ref n -> (*"AV_ref " ^*) "<"^pphex (n + cuh.cuh_offset)^">" - | 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_ref n -> (*"AV_ref " ^*) "<"^pphex_sym (n + cuh.cuh_offset)^">" + | AV_ref_addr n -> (*"AV_ref_addr " ^*) "<"^pphex_sym n^">" + | AV_ref_sig8 n -> "AV_ref_sig8 " ^ pphex_sym n + | AV_sec_offset n -> (*"AV_sec_offset " ^*) pphex_sym n ^ if at = attribute_encode "DW_AT_location" then " (location list)" else "" - | AV_string bs -> string_of_byte_sequence bs - | AV_strp n -> (*"AV_sec_offset " ^ pphex n ^ " " + | AV_string bs -> string_of_sym_byte_sequence bs + | AV_strp n -> (*"AV_sec_offset " ^ pphex_sym n ^ " " ^ pp_debug_str_entry str n*) - "(indirect string, offset: "^pphex n ^ "): " ^ pp_debug_str_entry str n + "(indirect string, offset: "^pphex_sym n ^ "): " ^ pp_debug_str_entry str n end -val parser_of_attribute_form_non_indirect : p_context -> compilation_unit_header -> natural -> parser attribute_value +val parser_of_attribute_form_non_indirect : p_context -> compilation_unit_header -> sym_natural -> parser attribute_value let parser_of_attribute_form_non_indirect c cuh n = (* address*) if n = attribute_form_encode "DW_FORM_addr" then @@ -2396,7 +2459,7 @@ let parser_of_attribute_form c cuh n = (* *** where to put this? *) -let pp_pos pos = "<" ^ pphexplain pos ^">" +let pp_pos pos = "<" ^ sym_natural_pp pphexplain pos ^">" let pp_cupdie (cu,parents,die) = pp_pos cu.cu_header.cuh_offset ^ "/" ^ pp_pos die.die_offset @@ -2445,31 +2508,31 @@ let find_dies (p:die->bool) (d: dwarf) : list cupdie = let string_of_string_attribute_value str av : string = match av with - | AV_string bs -> string_of_byte_sequence bs + | AV_string bs -> string_of_sym_byte_sequence bs | AV_strp n -> pp_debug_str_entry str n | _ -> "find_string_attribute_value_of_die AV not understood" end -let maybe_natural_of_constant_attribute_value die1 c av : maybe natural = +let maybe_natural_of_constant_attribute_value die1 c av : maybe sym_natural = match av with | AV_constantN n bs -> Just n | AV_constant_ULEB128 n -> Just n - | AV_block n bs -> Just (natural_of_bytes c.endianness bs) + | AV_block n bs -> Just (sym_natural_of_bytes c.endianness bs) | _ -> Nothing end -let natural_of_constant_attribute_value die1 c av : natural = +let natural_of_constant_attribute_value die1 c av : sym_natural = match maybe_natural_of_constant_attribute_value die1 c av with | Just n -> n | Nothing -> Assert_extra.failwith ("natural_of_constant_attribute_value fail at " ^ (pp_pos die1.die_offset ^ (" with av= " ^ pp_attribute_value_plain av))) end -let integer_of_constant_attribute_value c av : integer = +let integer_of_constant_attribute_value c av : sym_integer = match av with - | AV_constantN n bs -> integerFromNatural n - | AV_constant_ULEB128 n -> integerFromNatural n + | AV_constantN n bs -> symIntegerFromNatural n + | AV_constant_ULEB128 n -> symIntegerFromNatural n | AV_constant_SLEB128 n -> n - | AV_block n bs -> integerFromNatural (natural_of_bytes c.endianness bs) + | AV_block n bs -> symIntegerFromNatural (sym_natural_of_bytes c.endianness bs) | _ -> Assert_extra.failwith ("integer_of_constant_attribute_value fail") end @@ -2507,7 +2570,7 @@ let find_attribute_value (an: string) (die:die) : maybe attribute_value = die.die_abbreviation_declaration.ad_attribute_specifications die.die_attribute_values in myfindmaybe - (fun (((at': natural), (af: natural)), ((pos: natural),(av:attribute_value))) -> + (fun (((at': sym_natural), (af: sym_natural)), ((pos: sym_natural),(av:attribute_value))) -> if at' = at then Just av else Nothing) ats @@ -2521,7 +2584,7 @@ let find_string_attribute_value_of_die (an: string) str (die:die) : maybe string Nothing end -let find_natural_attribute_value_of_die c (an: string) (die:die) : maybe natural = +let find_natural_attribute_value_of_die c (an: string) (die:die) : maybe sym_natural = match find_attribute_value an die with | Just av -> let n = natural_of_constant_attribute_value die c av in @@ -2530,7 +2593,7 @@ let find_natural_attribute_value_of_die c (an: string) (die:die) : maybe natural Nothing end -let find_integer_attribute_value_of_die c (an: string) (die:die) : maybe integer = +let find_integer_attribute_value_of_die c (an: string) (die:die) : maybe sym_integer = match find_attribute_value an die with | Just av -> let n = integer_of_constant_attribute_value c av in @@ -2628,21 +2691,21 @@ let find_flag_attribute_value_of_die_using_abstract_origin d (an: string) ((cu,p let pp_dwarf_format df = match df with Dwarf32 -> "(32-bit)" | Dwarf64 -> "(64-bit)" end let pp_unit_header (s:string) (x:compilation_unit_header) : string = - "**" ^ s ^ " Unit @ offset " ^ pphex x.cuh_offset ^ "\n" - ^ " " ^ s ^ " Unit @ offset " ^ pphex x.cuh_offset ^ ":\n" - ^ " Length: " ^ pphex x.cuh_unit_length ^ " " ^ pp_dwarf_format x.cuh_dwarf_format ^ "\n" + "**" ^ s ^ " Unit @ offset " ^ pphex_sym x.cuh_offset ^ "\n" + ^ " " ^ s ^ " Unit @ offset " ^ pphex_sym x.cuh_offset ^ ":\n" + ^ " Length: " ^ pphex_sym x.cuh_unit_length ^ " " ^ pp_dwarf_format x.cuh_dwarf_format ^ "\n" ^ " Version: " ^ show x.cuh_version ^ "\n" - ^ " Abbrev Offset: " ^ pphex x.cuh_debug_abbrev_offset ^ "\n" + ^ " Abbrev Offset: " ^ pphex_sym x.cuh_debug_abbrev_offset ^ "\n" ^ " Pointer Size: " ^ show 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 : parser (dwarf_format * natural) = +let parse_unit_length c : parser (dwarf_format * sym_natural) = fun (pc: parse_context) -> pr_bind (parse_uint32 c pc) (fun x pc' -> - if x < natural_of_hex "0xfffffff0" then PR_success (Dwarf32,x) pc' - else if x <> natural_of_hex "0xffffffff" then PR_fail "bad unit_length" pc + if x < sym_natural_of_hex "0xfffffff0" then PR_success (Dwarf32,x) pc' + else if x <> sym_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')) @@ -2676,8 +2739,8 @@ let parse_compilation_unit_header c : parser compilation_unit_header = 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" + ^ " Type Signature: " ^ pphex_sym x.tuh_type_signature ^ "\n" + ^ " Type Offset: " ^ pphex_sym x.tuh_type_offset ^ "\n" let parse_type_unit_header c : parser type_unit_header = @@ -2726,7 +2789,7 @@ let indent_level_plus_one indent level = else " "^" " -let pp_die_attribute c (cuh:compilation_unit_header) (str : byte_sequence) (indent:bool) (level: natural) (((at: natural), (af: natural)), ((pos: natural),(av:attribute_value))) : string = +let pp_die_attribute c (cuh:compilation_unit_header) (str : sym_byte_sequence) (indent:bool) (level: natural) (((at: sym_natural), (af: sym_natural)), ((pos: sym_natural),(av:attribute_value))) : string = indent_level_plus_one indent level ^ pp_pos pos ^ " " ^ right_space_padded_to 18 (pp_attribute_encoding at) ^ ": " ^ @@ -2738,7 +2801,7 @@ let pp_die_attribute c (cuh:compilation_unit_header) (str : byte_sequence) (inde pp_attribute_value_like_objdump c cuh str at av ^ "\n" -val pp_die : p_context -> compilation_unit_header -> byte_sequence -> bool -> natural -> bool -> die -> string +val pp_die : p_context -> compilation_unit_header -> sym_byte_sequence -> bool -> natural -> bool -> die -> string let rec pp_die c cuh str indent level (pp_children:bool) die = indent_level indent level ^ "<" ^ show level ^ ">" ^ pp_pos die.die_offset @@ -2752,7 +2815,7 @@ let rec pp_die c cuh str indent level (pp_children:bool) die = ^ if pp_children then String.concat "" (List.map (pp_die c cuh str indent (level +1) pp_children) die.die_children) else "" -val pp_die_abbrev : p_context -> compilation_unit_header -> byte_sequence -> natural -> bool -> (list die) -> die -> string +val pp_die_abbrev : p_context -> compilation_unit_header -> sym_byte_sequence -> natural -> bool -> (list die) -> die -> string let rec pp_die_abbrev c cuh str level (pp_children:bool) parents die = indent_level true level ^ pp_tag_encoding die.die_abbreviation_declaration.ad_tag @@ -2768,7 +2831,7 @@ let rec pp_die_abbrev c cuh str level (pp_children:bool) parents die = (* condensed pp for variables *) -val pp_die_abbrev_var : p_context -> dwarf -> compilation_unit -> byte_sequence -> bool -> (list die) -> die -> (string (*name*) * string (*offset*) * string (*kind*)) +val pp_die_abbrev_var : p_context -> dwarf -> compilation_unit -> sym_byte_sequence -> bool -> (list die) -> die -> (string (*name*) * string (*offset*) * string (*kind*)) let rec pp_die_abbrev_var c d cu str (pp_children:bool) parents die = (* (indent_level true level*) (* ^ pp_tag_encoding die.die_abbreviation_declaration.ad_tag*) @@ -2785,7 +2848,7 @@ let rec pp_die_abbrev_var c d cu str (pp_children:bool) parents die = ) (* condensed pp for variable parents *) -val pp_die_abbrev_var_parent : p_context -> dwarf -> compilation_unit -> byte_sequence -> die -> string +val pp_die_abbrev_var_parent : p_context -> dwarf -> compilation_unit -> sym_byte_sequence -> die -> string let pp_die_abbrev_var_parent c d cu str die = (* (indent_level true level*) (* ^ pp_tag_encoding die.die_abbreviation_declaration.ad_tag*) @@ -2800,7 +2863,7 @@ let pp_die_abbrev_var_parent c d cu str die = -val pp_die_abbrev_var_parents : p_context -> dwarf -> compilation_unit -> byte_sequence -> list die -> string +val pp_die_abbrev_var_parents : p_context -> dwarf -> compilation_unit -> sym_byte_sequence -> list die -> string let pp_die_abbrev_var_parents c d cu str parents = String.concat ":" (List.map (fun die -> pp_die_abbrev_var_parent c d cu str die) parents) @@ -2814,14 +2877,14 @@ let pp_die_abbrev_var_parents c d cu str parents = -val parse_die : p_context -> byte_sequence -> compilation_unit_header -> (natural->abbreviation_declaration) -> parser (maybe die) +val parse_die : p_context -> sym_byte_sequence -> compilation_unit_header -> (sym_natural->abbreviation_declaration) -> parser (maybe die) let rec parse_die c str cuh find_abbreviation_declaration = fun (pc: parse_context) -> - (* let _ = my_debug3 ("parse_die called at " ^ pp_parse_context pc ^ "\n") in *) + let _ = my_debug3 ("parse_die called at " ^ pp_parse_context pc ^ "\n") in pr_bind (parse_ULEB128 pc) (fun abbreviation_code pc' -> if abbreviation_code = 0 then PR_success Nothing pc' else - (* let _ = my_debug3 ("parse_die abbreviation code "^pphex abbreviation_code ^"\n") in *) + let _ = my_debug3 ("parse_die abbreviation code "^pphex_sym abbreviation_code ^"\n") in let ad = find_abbreviation_declaration abbreviation_code in let attribute_value_parsers = 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'' -> @@ -2841,7 +2904,7 @@ let rec parse_die c str cuh find_abbreviation_declaration = (fun dies pc''' -> PR_success (Just ( let die = <| - die_offset = pc.pc_offset; + die_offset = sym_natural_const pc.pc_offset; die_abbreviation_code = abbreviation_code; die_abbreviation_declaration = ad; die_attribute_values = avs; @@ -2858,7 +2921,7 @@ let has_attribute (an: string) (die: die) : bool = (** compilation units: pp and parsing *) -let pp_compilation_unit c (indent:bool) (debug_str_section_body: byte_sequence) cu = +let pp_compilation_unit c (indent:bool) (debug_str_section_body: sym_byte_sequence) cu = "" (* "*** compilation unit header ***\n"*) ^ pp_compilation_unit_header cu.cu_header @@ -2873,7 +2936,7 @@ let pp_compilation_units c (indent:bool) debug_string_section_body (compilation_ String.concat "" (List.map (pp_compilation_unit c indent debug_string_section_body) compilation_units) -let pp_compilation_unit_abbrev c (debug_str_section_body: byte_sequence) cu = +let pp_compilation_unit_abbrev c (debug_str_section_body: sym_byte_sequence) cu = 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 0 true [] cu.cu_die @@ -2886,10 +2949,10 @@ let rec add_die_to_index acc parents die = let nacc : die_index = Map.insert die.die_offset (parents,die) acc in List.foldl (fun acc ndie -> add_die_to_index acc (die::parents) ndie) nacc die.die_children -let parse_compilation_unit c (debug_str_section_body: byte_sequence) (debug_abbrev_section_body: byte_sequence) : parser (maybe compilation_unit) = +let parse_compilation_unit c (debug_str_section_body: sym_byte_sequence) (debug_abbrev_section_body: sym_byte_sequence) : parser (maybe compilation_unit) = fun (pc:parse_context) -> - if Byte_sequence.length pc.pc_bytes = 0 then PR_success Nothing pc else + if sym_bs_length pc.pc_bytes = 0 then PR_success Nothing pc else let (cuh, pc') = @@ -2902,22 +2965,22 @@ let _ = my_debug4 (pp_compilation_unit_header cuh) in if cuh.cuh_unit_length = 0 then PR_success Nothing pc' else - let pc_abbrev = <|pc_bytes = match dropbytes cuh.cuh_debug_abbrev_offset debug_abbrev_section_body with Success bs -> bs | Fail _ -> Assert_extra.failwith "mydrop of debug_abbrev" end; pc_offset = cuh.cuh_debug_abbrev_offset |> in + let pc_abbrev = <|pc_bytes = match sym_dropbytes (sym_natural_expect_const cuh.cuh_debug_abbrev_offset (*"mydrop of pc_abbrev"*)) debug_abbrev_section_body with Success bs -> bs | Fail _ -> Assert_extra.failwith "mydrop of debug_abbrev" end; pc_offset = sym_natural_expect_const cuh.cuh_debug_abbrev_offset (*"mydrop of pc_abbrev"*)|> in (* todo: this is reparsing the abbreviations table for each cu *) let abbreviations_table = match parse_abbreviations_table c pc_abbrev with | PR_fail s pc_abbrev' -> Assert_extra.failwith ("parse_abbrevations_table fail: " ^ pp_parse_fail s pc_abbrev') - | PR_success at pc_abbrev' -> <| at_offset=pc_abbrev.pc_offset; at_table= at|> + | PR_success at pc_abbrev' -> <| at_offset=sym_natural_const pc_abbrev.pc_offset; at_table= at|> end in - (* let _ = my_debug4 (pp_abbreviations_table abbreviations_table) in *) + let _ = my_debug4 (pp_abbreviations_table abbreviations_table) in - let find_abbreviation_declaration (ac:natural) : abbreviation_declaration = + let find_abbreviation_declaration (ac:sym_natural) : abbreviation_declaration = (* let _ = my_debug4 ("find_abbreviation_declaration "^pphex ac) in *) - myfindNonPure (fun ad -> ad.ad_abbreviation_code = ac) abbreviations_table.at_table in + myfindNonPure (fun ad -> sym_eq ad.ad_abbreviation_code ac) abbreviations_table.at_table in - (* let _ = my_debug3 (pp_abbreviations_table abbreviations_table) in *) + let _ = my_debug3 (pp_abbreviations_table abbreviations_table) in match parse_die c debug_str_section_body cuh find_abbreviation_declaration pc' with | PR_fail s pc'' -> Assert_extra.failwith ("parse_die fail: " ^ pp_parse_fail s pc'') @@ -2933,14 +2996,14 @@ let _ = my_debug4 (pp_compilation_unit_header cuh) in PR_success (Just cu) pc'' end -let parse_compilation_units c (debug_str_section_body: byte_sequence) (debug_abbrev_section_body: byte_sequence): parser (list compilation_unit) +let parse_compilation_units c (debug_str_section_body: sym_byte_sequence) (debug_abbrev_section_body: sym_byte_sequence): parser (list compilation_unit) = 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: byte_sequence) tu = +let pp_type_unit c (debug_str_section_body: sym_byte_sequence) tu = 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 true 0 true tu.tu_die @@ -2949,10 +3012,10 @@ let pp_type_units c debug_string_section_body (type_units: list type_unit) : str String.concat "" (List.map (pp_type_unit c debug_string_section_body) type_units) -let parse_type_unit c (debug_str_section_body: byte_sequence) (debug_abbrev_section_body: byte_sequence) : parser (maybe type_unit) = +let parse_type_unit c (debug_str_section_body: sym_byte_sequence) (debug_abbrev_section_body: sym_byte_sequence) : parser (maybe type_unit) = fun (pc:parse_context) -> - if Byte_sequence.length pc.pc_bytes = 0 then PR_success Nothing pc else + if sym_bs_length pc.pc_bytes = 0 then PR_success Nothing pc else let (tuh, pc') = match parse_type_unit_header c pc with @@ -2962,19 +3025,19 @@ let parse_type_unit c (debug_str_section_body: byte_sequence) (debug_abbrev_sect (* 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 dropbytes n debug_abbrev_section_body with Success bs -> bs | Fail _ -> Assert_extra.failwith "mydrop of debug_abbrev" end; pc_offset = n |> in + let pc_abbrev = let n = tuh.tuh_cuh.cuh_debug_abbrev_offset in <|pc_bytes = match sym_dropbytes (sym_natural_expect_const n (*"mydrop of pc_abbrev"*)) debug_abbrev_section_body with Success bs -> bs | Fail _ -> Assert_extra.failwith "mydrop of debug_abbrev" end; pc_offset = sym_natural_expect_const n (*"mydrop of pc_abbrev"*) |> in let abbreviations_table = match parse_abbreviations_table c pc_abbrev with | PR_fail s pc_abbrev' -> Assert_extra.failwith ("parse_abbrevations_table fail: " ^ pp_parse_fail s pc_abbrev') - | PR_success at pc_abbrev' -> <| at_offset=pc_abbrev.pc_offset; at_table= at|> + | PR_success at pc_abbrev' -> <| at_offset=sym_natural_const pc_abbrev.pc_offset; at_table= at|> end in (* let _ = my_debug4 (pp_abbreviations_table abbreviations_table) in *) - let find_abbreviation_declaration (ac:natural) : abbreviation_declaration = + let find_abbreviation_declaration (ac:sym_natural) : abbreviation_declaration = (* let _ = my_debug4 ("find_abbreviation_declaration "^pphex ac) in *) - myfindNonPure (fun ad -> ad.ad_abbreviation_code = ac) abbreviations_table.at_table in + myfindNonPure (fun ad -> sym_eq ad.ad_abbreviation_code ac) abbreviations_table.at_table in (* let _ = my_debug3 (pp_abbreviations_table abbreviations_table) in *) @@ -2991,7 +3054,7 @@ let parse_type_unit c (debug_str_section_body: byte_sequence) (debug_abbrev_sect PR_success (Just tu) pc'' end -let parse_type_units c (debug_str_section_body: byte_sequence) (debug_abbrev_section_body: byte_sequence): parser (list type_unit) +let parse_type_units c (debug_str_section_body: sym_byte_sequence) (debug_abbrev_section_body: sym_byte_sequence): parser (list type_unit) = parse_list (parse_type_unit c debug_str_section_body debug_abbrev_section_body) @@ -3010,27 +3073,27 @@ Contents of the .debug_loc section: -let pp_location_list_entry c (cuh:compilation_unit_header) (offset:natural) (x:location_list_entry) : string = - " " ^ pphex offset - ^ " " ^ pphex x.lle_beginning_address_offset - ^ " " ^ pphex x.lle_ending_address_offset +let pp_location_list_entry c (cuh:compilation_unit_header) (offset:sym_natural) (x:location_list_entry) : string = + " " ^ pphex_sym offset + ^ " " ^ pphex_sym x.lle_beginning_address_offset + ^ " " ^ pphex_sym 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:natural) (x:base_address_selection_entry) : string = - " " ^ pphex offset - ^ " " ^ pphex x.base_address +let pp_base_address_selection_entry c (cuh:compilation_unit_header) (offset:sym_natural) (x:base_address_selection_entry) : string = + " " ^ pphex_sym offset + ^ " " ^ pphex_sym x.base_address ^ "\n" -let pp_location_list_item c (cuh: compilation_unit_header) (offset: natural) (x:location_list_item) = +let pp_location_list_item c (cuh: compilation_unit_header) (offset: sym_natural) (x:location_list_item) = 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 end -let pp_location_list c (cuh: compilation_unit_header) ((offset:natural), (llis: list location_list_item)) = +let pp_location_list c (cuh: compilation_unit_header) ((offset:sym_natural), (llis: list location_list_item)) = String.concat "" (List.map (pp_location_list_item c cuh offset) llis) -(* ^ " " ^ pphex offset ^ " \n"*) +(* ^ " " ^ pphex_sym offset ^ " \n"*) let pp_loc c (cuh: compilation_unit_header) (lls: list location_list) = " Offset Begin End Expression\n" @@ -3052,7 +3115,7 @@ let parse_location_list_item c (cuh: compilation_unit_header) : parser (maybe lo (parse_uint_address_size c cuh.cuh_address_size) (parse_uint_address_size c cuh.cuh_address_size) pc) - (fun ((a1: natural),(a2:natural)) pc' -> + (fun ((a1: sym_natural),(a2:sym_natural)) pc' -> (* let _ = my_debug4 ("offset="^pphex pc.pc_offset ^ " begin=" ^ pphex a1 ^ " end=" ^ pphex a2) in *) if a1=0 && a2=0 then PR_success Nothing pc' @@ -3077,23 +3140,23 @@ let parse_location_list_item c (cuh: compilation_unit_header) : parser (maybe lo let parse_location_list c cuh : parser (maybe location_list) = fun (pc: parse_context) -> - if Byte_sequence.length pc.pc_bytes = 0 then + if sym_bs_length pc.pc_bytes = 0 then PR_success Nothing pc else pr_post_map1 (parse_list (parse_location_list_item c cuh) pc) - (fun llis -> (Just (pc.pc_offset, llis))) + (fun llis -> (Just (sym_natural_const pc.pc_offset, llis))) let parse_location_list_list c cuh : parser location_list_list = parse_list (parse_location_list c cuh) let find_location_list dloc n : location_list = - myfindNonPure (fun (n',_)-> n'=n) dloc + myfindNonPure (fun (n',_)-> sym_eq 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_address: natural) (llis: list location_list_item) : list (natural * natural * single_location_description) = +let rec interpret_location_list (base_address: sym_natural) (llis: list location_list_item) : list (sym_natural * sym_natural * single_location_description) = match llis with | [] -> [] | LLI_base base::llis' -> interpret_location_list base.base_address llis' @@ -3121,22 +3184,22 @@ Contents of the .debug_ranges section: *) -let pp_range_list_entry c (cuh:compilation_unit_header) (offset:natural) (x:range_list_entry) : string = - " " ^ pphex offset - ^ " " ^ pphex x.rle_beginning_address_offset - ^ " " ^ pphex x.rle_ending_address_offset +let pp_range_list_entry c (cuh:compilation_unit_header) (offset:sym_natural) (x:range_list_entry) : string = + " " ^ pphex_sym offset + ^ " " ^ pphex_sym x.rle_beginning_address_offset + ^ " " ^ pphex_sym x.rle_ending_address_offset ^ (if x.rle_beginning_address_offset = x.rle_ending_address_offset then " (start == end)" else "") ^ "\n" -let pp_range_list_item c (cuh: compilation_unit_header) (offset: natural) (x:range_list_item) = +let pp_range_list_item c (cuh: compilation_unit_header) (offset: sym_natural) (x:range_list_item) = 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 end -let pp_range_list c (cuh: compilation_unit_header) ((offset:natural), (rlis: list range_list_item)) = +let pp_range_list c (cuh: compilation_unit_header) ((offset:sym_natural), (rlis: list range_list_item)) = String.concat "" (List.map (pp_range_list_item c cuh offset) rlis) - ^ " " ^ pphex offset ^ " \n" + ^ " " ^ pphex_sym offset ^ " \n" let pp_ranges c (cuh: compilation_unit_header) (rls: list range_list) = " Offset Begin End\n" @@ -3153,7 +3216,7 @@ let parse_range_list_item c (cuh: compilation_unit_header) : parser (maybe range (parse_uint_address_size c cuh.cuh_address_size) (parse_uint_address_size c cuh.cuh_address_size) pc) - (fun ((a1: natural),(a2:natural)) pc' -> + (fun ((a1: sym_natural),(a2:sym_natural)) pc' -> (* let _ = my_debug4 ("offset="^pphex pc.pc_offset ^ " begin=" ^ pphex a1 ^ " end=" ^ pphex a2) in *) if a1=0 && a2=0 then PR_success Nothing pc' @@ -3180,23 +3243,23 @@ let rec expand_range_list_suffixes cuh (offset,(rlis: list range_list_item)) : l let parse_range_list c cuh : parser (maybe (list range_list)) = fun (pc: parse_context) -> - if Byte_sequence.length pc.pc_bytes = 0 then + if sym_bs_length pc.pc_bytes = 0 then PR_success Nothing pc else pr_post_map1 (parse_list (parse_range_list_item c cuh) pc) - (fun rlis -> (Just (expand_range_list_suffixes cuh (pc.pc_offset, rlis)))) + (fun rlis -> (Just (expand_range_list_suffixes cuh (sym_natural_const pc.pc_offset, rlis)))) let parse_range_list_list c cuh : parser range_list_list = pr_map2 List.concat (parse_list (parse_range_list c cuh)) let find_range_list dranges n : maybe range_list = - List.find (fun (n',_)-> n'=n) dranges + List.find (fun (n',_)-> sym_eq 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_address: natural) (rlis: list range_list_item) : list (natural * natural) = +let rec interpret_range_list (base_address: sym_natural) (rlis: list range_list_item) : list (sym_natural * sym_natural) = match rlis with | [] -> [] | RLI_base base::rlis' -> interpret_range_list base.base_address rlis' @@ -3244,16 +3307,16 @@ Contents of the .debug_frame section: -let pp_cfa_address a = pphex a +let pp_cfa_address a = pphex_sym a let pp_cfa_block b = ppbytes b -let pp_cfa_delta d = pphex d +let pp_cfa_delta d = pphex_sym d (*let pp_cfa_offset n = pphex n let pp_cfa_register r = show r*) let pp_cfa_sfoffset i = show i let pp_cfa_register r = "r"^show r (*TODO: arch-specific register names *) -let pp_cfa_offset (i:integer) = if i=0 then "" else if i<0 then show i else "+" ^ show i +let pp_cfa_offset (i:sym_integer) = if i=0 then "" else if i<0 then show i else "+" ^ show i let pp_cfa_rule (cr:cfa_rule) : string = match cr with @@ -3279,29 +3342,29 @@ let pp_register_rule (rr:register_rule) : string = (*TODO make this more readel let pp_call_frame_instruction i = 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 r ^ " " ^ pp_cfa_offset (integerFromNatural n) + | DW_CFA_offset r n -> "DW_CFA_offset" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_offset (symIntegerFromNatural n) | DW_CFA_restore r -> "DW_CFA_restore" ^ " " ^ pp_cfa_register 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 r ^ " " ^ pp_cfa_offset (integerFromNatural n) + | DW_CFA_offset_extended r n -> "DW_CFA_offset_extended" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_offset (symIntegerFromNatural n) | DW_CFA_restore_extended r -> "DW_CFA_restore_extended" ^ " " ^ pp_cfa_register r | DW_CFA_undefined r -> "DW_CFA_undefined" ^ " " ^ pp_cfa_register r | DW_CFA_same_value r -> "DW_CFA_same_value" ^ " " ^ pp_cfa_register r | DW_CFA_register r1 r2 -> "DW_CFA_register" ^ " " ^ pp_cfa_register r1 ^ " " ^ pp_cfa_register 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 r ^ " " ^ pp_cfa_offset (integerFromNatural n) + | DW_CFA_def_cfa r n -> "DW_CFA_def_cfa" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_offset (symIntegerFromNatural n) | DW_CFA_def_cfa_register r -> "DW_CFA_def_cfa_register" ^ " " ^ pp_cfa_register r - | DW_CFA_def_cfa_offset n -> "DW_CFA_def_cfa_offset" ^ " " ^ pp_cfa_offset (integerFromNatural n) + | DW_CFA_def_cfa_offset n -> "DW_CFA_def_cfa_offset" ^ " " ^ pp_cfa_offset (symIntegerFromNatural n) | DW_CFA_def_cfa_expression b -> "DW_CFA_def_cfa_expression" ^ " " ^ pp_cfa_block b | DW_CFA_expression r b -> "DW_CFA_expression" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_block b | DW_CFA_offset_extended_sf r i -> "DW_CFA_offset_extended_sf" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_sfoffset i | DW_CFA_def_cfa_sf r i -> "DW_CFA_def_cfa_sf" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_sfoffset i | DW_CFA_def_cfa_offset_sf i -> "DW_CFA_def_cfa_offset_sf" ^ " " ^ pp_cfa_sfoffset i - | DW_CFA_val_offset r n -> "DW_CFA_val_offset" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_offset (integerFromNatural n) + | DW_CFA_val_offset r n -> "DW_CFA_val_offset" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_offset (symIntegerFromNatural n) | DW_CFA_val_offset_sf r i -> "DW_CFA_val_offset_sf" ^ pp_cfa_register r ^ " " ^ pp_cfa_sfoffset i | DW_CFA_val_expression r b -> "DW_CFA_val_expression" ^ " " ^ pp_cfa_register r ^ " " ^ pp_cfa_block b | DW_CFA_AARCH64_negate_ra_state -> "DW_CFA_AARCH64_negate_ra_state" @@ -3328,13 +3391,13 @@ let parser_of_call_frame_argument_type c cuh (cfat: call_frame_argument_type) : let parse_call_frame_instruction c cuh : parser (maybe call_frame_instruction) = fun pc -> - match read_char pc.pc_bytes with + match sym_read_char pc.pc_bytes with | Fail _ -> PR_success Nothing pc | Success (b,bs') -> let pc' = <| pc_bytes = bs'; pc_offset = pc.pc_offset + 1 |> in let ch = unsigned_char_of_byte b in let high_bits = unsigned_char_land ch (unsigned_char_of_natural 192) in - let low_bits = natural_of_unsigned_char (unsigned_char_land ch (unsigned_char_of_natural 63)) in + let low_bits = sym_natural_const (natural_of_unsigned_char (unsigned_char_land ch (unsigned_char_of_natural 63))) in if high_bits = unsigned_char_of_natural 0 then match lookup_abCde_de low_bits call_frame_instruction_encoding with | Just ((args: list call_frame_argument_type), result) -> @@ -3369,14 +3432,14 @@ let parse_call_frame_instruction c cuh : parser (maybe call_frame_instruction) = let parse_call_frame_instructions c cuh : parser (list call_frame_instruction) = parse_list (parse_call_frame_instruction c cuh) -val parse_and_pp_call_frame_instructions : p_context -> compilation_unit_header -> byte_sequence -> string +val parse_and_pp_call_frame_instructions : p_context -> compilation_unit_header -> sym_byte_sequence -> string let parse_and_pp_call_frame_instructions c cuh bs = let pc = <|pc_bytes = bs; pc_offset = 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 Byte_sequence.length pc'.pc_bytes <> 0 then " Warning: extra non-parsed bytes" else "" + ^ if sym_bs_length pc'.pc_bytes <> 0 then " Warning: extra non-parsed bytes" else "" end @@ -3388,12 +3451,12 @@ let pp_call_frame_instructions' c cuh bs = let pp_cie c cuh cie = - pphex cie.cie_offset - ^ " " ^ pphex cie.cie_length - ^ " " ^ pphex cie.cie_id + pphex_sym cie.cie_offset + ^ " " ^ pphex_sym cie.cie_length + ^ " " ^ pphex_sym cie.cie_id ^ " CIE\n" ^ " Version: " ^ show cie.cie_version ^ "\n" - ^ " Augmentation: \""^ show (string_of_byte_sequence cie.cie_augmentation) ^ "\"\n" + ^ " Augmentation: \""^ show (string_of_sym_byte_sequence cie.cie_augmentation) ^ "\"\n" ^ " Code alignment factor: " ^ show cie.cie_code_alignment_factor ^ "\n" ^ " Data alignment factor: " ^ show cie.cie_data_alignment_factor ^ "\n" ^ " Return address column: " ^ show cie.cie_return_address_register ^ "\n" @@ -3401,18 +3464,18 @@ let pp_cie c cuh cie = ^ ppbytes cie.cie_initial_instructions_bytes ^ "\n" ^ pp_call_frame_instructions cie.cie_initial_instructions -(* cie_address_size: natural; (* not shown by readelf - must match compilation unit *)*) -(* cie_segment_size: natural; (* not shown by readelf *)*) +(* cie_address_size: sym_natural; (* not shown by readelf - must match compilation unit *)*) +(* cie_segment_size: sym_natural; (* not shown by readelf *)*) (* readelf says "Return address column", but the DWARF spec says "Return address register" *) let pp_fde c cuh fde = - pphex fde.fde_offset - ^ " " ^ pphex fde.fde_length - ^ " " ^ pphex fde.fde_cie_pointer (* not what this field of readelf output is *) + pphex_sym fde.fde_offset + ^ " " ^ pphex_sym fde.fde_length + ^ " " ^ pphex_sym fde.fde_cie_pointer (* not what this field of readelf output is *) ^ " FDE" - ^ " cie=" ^ pphex fde.fde_cie_pointer (* duplicated?? *) - ^ " pc=" ^ match fde.fde_initial_location_segment_selector with Nothing -> "" | Just segment_selector -> "("^pphex segment_selector^")" end ^ pphex fde.fde_initial_location_address ^ ".." ^ pphex (fde.fde_initial_location_address + fde.fde_address_range) ^ "\n" + ^ " cie=" ^ pphex_sym fde.fde_cie_pointer (* duplicated?? *) + ^ " pc=" ^ match fde.fde_initial_location_segment_selector with Nothing -> "" | Just segment_selector -> "("^pphex_sym segment_selector^")" end ^ pphex_sym fde.fde_initial_location_address ^ ".." ^ pphex_sym (fde.fde_initial_location_address + fde.fde_address_range) ^ "\n" ^ ppbytes fde.fde_instructions_bytes ^ "\n" ^ pp_call_frame_instructions fde.fde_instructions @@ -3433,10 +3496,10 @@ let rec find_cie fi cie_id = match fi with | [] -> Assert_extra.failwith "find_cie: cie_id not found" | FIE_fde _ :: fi' -> find_cie fi' cie_id - | FIE_cie cie :: fi' -> if cie_id = cie.cie_offset then cie else find_cie fi' cie_id + | FIE_cie cie :: fi' -> if sym_eq cie_id cie.cie_offset then cie else find_cie fi' cie_id end -let parse_initial_location c cuh mss mas' : parser ((maybe natural) * natural) = (*(segment selector and target address)*) +let parse_initial_location c cuh mss mas' : parser ((maybe sym_natural) * sym_natural) = (*(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 Just n -> n | Nothing -> 0 end)) @@ -3445,7 +3508,7 @@ let parse_initial_location c cuh mss mas' : parser ((maybe natural) * natural) = let parse_call_frame_instruction_bytes offset' ul = fun (pc: parse_context) -> - parse_n_bytes (ul - (pc.pc_offset - offset')) pc + parse_n_bytes (ul - (sym_natural_const pc.pc_offset - offset')) pc let parse_frame_info_element c cuh (fi: list frame_info_element) : parser frame_info_element = parse_dependent @@ -3459,8 +3522,8 @@ let parse_frame_info_element c cuh (fi: list frame_info_element) : parser frame_ (fun (offset,((df,ul),(offset',cie_id))) -> if (cie_id = match df with - | Dwarf32 -> natural_of_hex "0xffffffff" - | Dwarf64 -> natural_of_hex "0xffffffffffffffff" + | Dwarf32 -> sym_natural_of_hex "0xffffffff" + | Dwarf64 -> sym_natural_of_hex "0xffffffffffffffff" end) then (* parse cie *) @@ -3540,7 +3603,7 @@ 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 = fun pc -> - if Byte_sequence.length pc.pc_bytes = 0 then + if sym_bs_length pc.pc_bytes = 0 then PR_success (List.reverse acc) pc else pr_bind @@ -3560,14 +3623,14 @@ let parse_frame_info c cuh : parser frame_info (** line numbers .debug_line, pp and parsing *) let pp_line_number_file_entry lnfe = - "lnfe_path = " ^ string_of_byte_sequence lnfe.lnfe_path ^ "\n" + "lnfe_path = " ^ string_of_sym_byte_sequence lnfe.lnfe_path ^ "\n" ^ "lnfe_directory_index " ^ show lnfe.lnfe_directory_index ^ "\n" ^ "lnfe_last_modification = " ^ show lnfe.lnfe_last_modification ^ "\n" ^ "lnfe_length = " ^ show lnfe.lnfe_length ^ "\n" let pp_line_number_header lnh = - "offset = " ^ pphex lnh.lnh_offset ^ "\n" + "offset = " ^ pphex_sym lnh.lnh_offset ^ "\n" ^ "dwarf_format = " ^ pp_dwarf_format lnh.lnh_dwarf_format ^ "\n" ^ "unit_length = " ^ show lnh.lnh_unit_length ^ "\n" ^ "version = " ^ show lnh.lnh_version ^ "\n" @@ -3580,7 +3643,7 @@ let pp_line_number_header lnh = ^ "opcode_base = " ^ show lnh.lnh_opcode_base ^ "\n" ^ "standard_opcode_lengths = " ^ show lnh.lnh_standard_opcode_lengths ^ "\n" ^ "comp_dir = " ^ show lnh.lnh_comp_dir ^ "\n" -^ "include_directories = " ^ String.concat ", " (List.map string_of_byte_sequence lnh.lnh_include_directories) ^ "\n" +^ "include_directories = " ^ String.concat ", " (List.map string_of_sym_byte_sequence lnh.lnh_include_directories) ^ "\n" ^ "file_entries = \n\n" ^ String.concat "\n" (List.map pp_line_number_file_entry lnh.lnh_file_entries) ^ "\n" @@ -3599,7 +3662,7 @@ let pp_line_number_operation lno = | DW_LNS_set_epilogue_begin -> "DW_LNS_set_epilogue_begin" | DW_LNS_set_isa n -> "DW_LNS_set_isa" ^ " " ^ show n | DW_LNE_end_sequence -> "DW_LNE_end_sequence" - | DW_LNE_set_address n -> "DW_LNE_set_address" ^ " " ^ pphex n + | DW_LNE_set_address n -> "DW_LNE_set_address" ^ " " ^ pphex_sym n | DW_LNE_define_file s n1 n2 n3 -> "DW_LNE_define_file" ^ " " ^ show s ^ " " ^ show n1 ^ " " ^ show n2 ^ " " ^ show n3 | DW_LNE_set_discriminator n -> "DW_LNE_set_discriminator" ^ " " ^ show n | DW_LN_special n -> "DW_LN_special" ^ " " ^ show n @@ -3669,8 +3732,8 @@ let parse_line_number_header c (comp_dir:maybe string) : parser line_number_head (parse_triple (parse_uintDwarfN c df) (* header_length *) (parse_uint8) (* minimum_instruction_length *) - (if v<4 then (* maximum_operations_per_instruction*)(* NOT IN DWARF 2 or 3; in DWARF 4*) - (parse_uint8_constant 1) + (if v pr_post_map (parse_triple - (pr_post_map (parse_n_bytes (ob-1)) (fun bs -> List.map natural_of_byte (byte_list_of_byte_sequence bs))) (* standard_opcode_lengths *) + (pr_post_map (parse_n_bytes (ob-sym_natural_const 1)) (fun bs -> List.map sym_natural_of_byte (byte_list_of_sym_byte_sequence bs))) (* standard_opcode_lengths *) ((*pr_return [[]]*) parse_list parse_non_empty_string) (* include_directories *) (parse_list parse_line_number_file_entry) (* file names *) ) @@ -3789,7 +3852,7 @@ let parse_line_number_program c (cuh:compilation_unit_header) (comp_dir:maybe st let line_number_offset_of_compilation_unit c cu = match find_attribute_value "DW_AT_stmt_list" cu.cu_die with | Just (AV_sec_offset n) -> n - | Just (AV_block n bs) -> natural_of_bytes c.endianness bs + | Just (AV_block n bs) -> sym_natural_of_bytes c.endianness bs (* a 32-bit MIPS example used a 4-byte AV_block not AV_sec_offset *) | Just _ -> (Assert_extra.failwith ("compilation unit DW_AT_stmt_list attribute was not an AV_sec_offset" ^ pp_compilation_unit_header cu.cu_header)) | _ -> Assert_extra.failwith ("compilation unit did not have a DW_AT_stmt_list attribute\n" ^ pp_compilation_unit_header cu.cu_header ^ "\n") @@ -3798,7 +3861,7 @@ let line_number_offset_of_compilation_unit c cu = let line_number_program_of_compilation_unit d cu = let c = p_context_of_d d in let offset = line_number_offset_of_compilation_unit c cu in - match List.find (fun lnp -> lnp.lnp_header.lnh_offset = offset) d.d_line_info with + match List.find (fun lnp -> sym_eq lnp.lnp_header.lnh_offset offset) d.d_line_info with | Nothing -> Assert_extra.failwith "compilation unit line number offset not found" | Just lnp ->lnp end @@ -3808,7 +3871,7 @@ let filename d cu n = if n=0 then Nothing else match mynth (n - 1) lnp.lnp_header.lnh_file_entries with | Just lnfe -> - Just (string_of_byte_sequence lnfe.lnfe_path) + Just (string_of_sym_byte_sequence lnfe.lnfe_path) | Nothing -> Assert_extra.failwith ("line number file entry not found") end @@ -3821,11 +3884,11 @@ let unpack_file_entry lnh file : unpacked_file_entry = Nothing else match mynth (lnfe.lnfe_directory_index - 1) lnh.lnh_include_directories with - | Just d -> Just (string_of_byte_sequence d) + | Just d -> Just (string_of_sym_byte_sequence d) | Nothing -> Just "" end in - (lnh.lnh_comp_dir, directory, string_of_byte_sequence lnfe.lnfe_path) + (lnh.lnh_comp_dir, directory, string_of_sym_byte_sequence lnfe.lnfe_path) | Nothing -> (Nothing,Nothing,"") end @@ -3851,10 +3914,10 @@ let pp_ufe_brief (((mcomp_dir,mdir,file) as ufe) : unpacked_file_entry) : string ^ " comp_dir=" ^ match mcomp_dir with | Just s->s|Nothing->"" end *) -let parse_line_number_info c str (d_line: byte_sequence) (cu: compilation_unit) : line_number_program = +let parse_line_number_info c str (d_line: sym_byte_sequence) (cu: compilation_unit) : line_number_program = let comp_dir = find_string_attribute_value_of_die "DW_AT_comp_dir" str cu.cu_die in let f n = - let d_line' = match dropbytes n d_line with Success xs -> xs | Fail _ -> Assert_extra.failwith "parse_line_number_info drop" end in + let d_line' = match sym_dropbytes n d_line with Success xs -> xs | Fail _ -> Assert_extra.failwith "parse_line_number_info drop" end in let pc = <| pc_bytes = d_line'; pc_offset = n|> in match parse_line_number_program c cu.cu_header comp_dir pc with | PR_success lnp pc' -> @@ -3862,7 +3925,7 @@ let parse_line_number_info c str (d_line: byte_sequence) (cu: compilation_unit) lnp | PR_fail s pc' -> Assert_extra.failwith ("parse_line_number_header failed: " ^ s) end in - f (line_number_offset_of_compilation_unit c cu) + f (sym_natural_expect_const (line_number_offset_of_compilation_unit c cu) (*"parse_line_number_info"*)) let parse_line_number_infos c str debug_line_section_body compilation_units = @@ -3915,13 +3978,13 @@ let pp_dwarf d = (* TODO: don't use lists of bytes here! *) let parse_dwarf c - (debug_info_section_body: byte_sequence) - (debug_abbrev_section_body: byte_sequence) - (debug_str_section_body: byte_sequence) - (debug_loc_section_body: byte_sequence) - (debug_ranges_section_body: byte_sequence) - (debug_frame_section_body: byte_sequence) - (debug_line_section_body: byte_sequence) + (debug_info_section_body: sym_byte_sequence) + (debug_abbrev_section_body: sym_byte_sequence) + (debug_str_section_body: sym_byte_sequence) + (debug_loc_section_body: sym_byte_sequence) + (debug_ranges_section_body: sym_byte_sequence) + (debug_frame_section_body: sym_byte_sequence) + (debug_line_section_body: sym_byte_sequence) : dwarf = let pc_info = <|pc_bytes = debug_info_section_body; pc_offset = 0 |> in @@ -3932,7 +3995,7 @@ let parse_dwarf c | PR_success cus pc_info' -> cus end in - (*let _ = my_debug5 (pp_compilation_units c debug_str_section_body compilation_units) in*) + let _ = my_debug5 (pp_compilation_units c false 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 *) @@ -3957,8 +4020,6 @@ let parse_dwarf c let pc_frame = <|pc_bytes = debug_frame_section_body; pc_offset = 0 |> in let fi = - (* let _ = my_debug5 ("debug_frame_section_body:\n" ^ ppbytes2 0 debug_frame_section_body) in *) - match parse_frame_info c cuh_default pc_frame with | PR_fail s pc_info' -> Assert_extra.failwith ("parse_frame_info: " ^ pp_parse_fail s pc_info') | PR_success fi pc_loc' -> fi @@ -3977,8 +4038,8 @@ let parse_dwarf c d_line_info = li; |> -val extract_section_body : elf_file -> string -> bool -> p_context * natural * byte_sequence -let extract_section_body (f:elf_file) (section_name:string) (strict: bool) = +val extract_section_body : elf_file -> relocation_interpreter reloc_target_data -> string -> bool -> p_context * sym_natural * sym_byte_sequence +let extract_section_body (f:elf_file) (ri:relocation_interpreter reloc_target_data) (section_name:string) (strict: bool) = let (en: Endianness.endianness) = match f with | ELF_File_32 f32 -> Elf_header.get_elf32_header_endianness f32.Elf_file.elf32_file_header @@ -3994,16 +4055,25 @@ let extract_section_body (f:elf_file) (section_name:string) (strict: bool) = ) f32.elf32_file_interpreted_sections in match sections with | [section] -> - let section_addr = section.Elf_interpreted_section.elf32_section_addr in + let section_addr = if is_elf32_relocatable_file f32.elf32_file_header then + sym_natural_section section_name + else + sym_natural_const section.Elf_interpreted_section.elf32_section_addr + in let section_body = section.Elf_interpreted_section.elf32_section_body in (* let _ = my_debug4 (section_name ^ (": \n" ^ (Elf_interpreted_section.string_of_elf32_interpreted_section section ^ "\n" * ^ " body = " ^ ppbytes2 0 section_body ^ "\n"))) in *) + let section_body = if is_elf32_relocatable_file f32.elf32_file_header then + Assert_extra.failwith "Not implemented" + else + sym_bs_construct section_body Map.empty + in (c,section_addr,section_body) | [] -> if strict then Assert_extra.failwith ("" ^ section_name ^ " section not present") else - (c,0,Byte_sequence.empty) + (c,0,sym_bs_empty) | _ -> Assert_extra.failwith ("multiple " ^ section_name ^ " sections present") end @@ -4016,34 +4086,52 @@ let extract_section_body (f:elf_file) (section_name:string) (strict: bool) = ) f64.elf64_file_interpreted_sections in match sections with | [section] -> - let section_addr = section.Elf_interpreted_section.elf64_section_addr in + let section_addr = if is_elf64_relocatable_file f64.elf64_file_header then + sym_natural_section section_name + else + sym_natural_const section.Elf_interpreted_section.elf64_section_addr + in let section_body = section.Elf_interpreted_section.elf64_section_body in - (c,section_addr,section_body) + let _ = my_debug "extracted section body" in + match extract_elf64_relocations_for_section f64 ri section_name with + | Success relocations -> + let _ = my_debug "extracted relocations" in + let section_body = construct_sym_byte_sequence section_body relocations in + (c,section_addr,section_body) + | Fail err -> Assert_extra.failwith ("failed extracting relocations: " ^ err) + end | [] -> if strict then Assert_extra.failwith ("" ^ section_name ^ " section not present") else - (c,0,Byte_sequence.empty) + (c,0,sym_bs_empty) | _ -> Assert_extra.failwith ("multiple " ^ section_name ^ " sections present") end end -val extract_dwarf : elf_file -> maybe dwarf -let extract_dwarf f = - let (c, _, debug_info_section_body) = extract_section_body f ".debug_info" true in - let (c, _, debug_abbrev_section_body) = extract_section_body f ".debug_abbrev" false in - let (c, _, debug_str_section_body) = extract_section_body f ".debug_str" false in - let (c, _, debug_loc_section_body) = extract_section_body f ".debug_loc" false in - let (c, _, debug_ranges_section_body) = extract_section_body f ".debug_ranges" false in - let (c, _, debug_frame_section_body) = extract_section_body f ".debug_frame" false in - let (c, _, debug_line_section_body) = extract_section_body f ".debug_line" false in +let extract_section_body_without_relocations f section_name strict = + let err_on_relocation ef symtab_map sidx rel = Assert_extra.failwith "Relocation found while extracting a section without relocations" in + let (c, addr, body) = extract_section_body f err_on_relocation section_name strict in + (c, addr, sym_bs_expect_const body) + +val extract_dwarf : elf_file -> relocation_interpreter reloc_target_data -> maybe dwarf +let extract_dwarf f ri = + let _ = my_debug "extract dwarf" in + + let (c, _, debug_info_section_body) = extract_section_body f ri ".debug_info" true in + let (c, _, debug_abbrev_section_body) = extract_section_body f ri ".debug_abbrev" false in + let (c, _, debug_str_section_body) = extract_section_body f ri ".debug_str" false in + let (c, _, debug_loc_section_body) = extract_section_body f ri ".debug_loc" false in + let (c, _, debug_ranges_section_body) = extract_section_body f ri ".debug_ranges" false in + let (c, _, debug_frame_section_body) = extract_section_body f ri ".debug_frame" false in + let (c, _, debug_line_section_body) = extract_section_body f ri ".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 Just d -val extract_text : elf_file -> p_context * natural * byte_sequence (* (p_context, elf32/64_section_addr, elf32/64_section_body) *) -let extract_text f = extract_section_body f ".text" true +val extract_text : elf_file -> relocation_interpreter reloc_target_data -> p_context * sym_natural * sym_byte_sequence (* (p_context, elf32/64_section_addr, elf32/64_section_body) *) +let extract_text f ri = extract_section_body f ri ".text" true (** ************************************************************ *) @@ -4056,7 +4144,7 @@ let extract_text f = extract_section_body f ".text" true val pp_simple_location : simple_location -> string let pp_simple_location sl = match sl with - | SL_memory_address n -> pphex n + | SL_memory_address n -> pphex_sym n | SL_register n -> "reg" ^ show n | SL_implicit bs -> "value: " ^ ppbytes bs | SL_empty -> "" @@ -4162,25 +4250,25 @@ accumulated so far *) let arithmetic_context_of_cuh cuh = - match cuh.cuh_address_size with + match sym_natural_expect_const cuh.cuh_address_size (*"arithmetic_context_of_cuh"*) with | 8 -> <| ac_bitwidth = 64; - ac_half = naturalPow 2 32; - ac_all = naturalPow 2 64; - ac_max = (naturalPow 2 64) - 1; + ac_half = symNaturalPow 2 32; + ac_all = symNaturalPow 2 64; + ac_max = (symNaturalPow 2 64) - 1; |> | 4 -> <| ac_bitwidth = 32; - ac_half = naturalPow 2 16; - ac_all = naturalPow 2 32; - ac_max = (naturalPow 2 32) - 1; + ac_half = symNaturalPow 2 16; + ac_all = symNaturalPow 2 32; + ac_max = (symNaturalPow 2 32) - 1; |> | _ -> Assert_extra.failwith "arithmetic_context_of_cuh given non-4/8 size" end -let find_cfa_table_row_for_pc (evaluated_frame_info: evaluated_frame_info) (pc: natural) : cfa_table_row = +let find_cfa_table_row_for_pc (evaluated_frame_info: evaluated_frame_info) (pc: sym_natural) : cfa_table_row = match myfind (fun (fde,rows) -> pc >= fde.fde_initial_location_address && pc < fde.fde_initial_location_address + fde.fde_address_range) @@ -4195,11 +4283,11 @@ let find_cfa_table_row_for_pc (evaluated_frame_info: evaluated_frame_info) (pc: end -let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evaluated_frame_info: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: maybe attribute_value) (pc: natural) (s: state) (ops: list operation) : error single_location = +let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evaluated_frame_info: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: maybe attribute_value) (pc: sym_natural) (s: state) (ops: list operation) : error single_location = 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: maybe natural) vs' (err:string) op = + let push_memory_address_maybe (mv: maybe sym_natural) vs' (err:string) op = match mv with | Just v -> push_memory_address v vs' | Nothing -> Fail (err ^ pp_operation op) @@ -4207,7 +4295,7 @@ let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evalua let bregxi r i = match ev.read_register r with - | RRR_result v -> push_memory_address (partialNaturalFromInteger ((integerFromNatural v+i) mod (integerFromNatural ac.ac_all))) s.s_stack + | RRR_result v -> push_memory_address (partialSymNaturalFromInteger ((symIntegerFromNatural v+i) mod (symIntegerFromNatural ac.ac_all))) s.s_stack | RRR_not_currently_available -> Fail "RRR_not_currently_available" | RRR_bad_register_number -> Fail ("RRR_bad_register_number " ^ show r) end in @@ -4241,7 +4329,7 @@ let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evalua | (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 (integerFromNatural ac.ac_all)) s.s_stack + push_memory_address (partialTwosComplementNaturalFromInteger i ac.ac_half (symIntegerFromNatural ac.ac_all)) s.s_stack | (OpSem_stack f, []) -> match f ac s.s_stack op.op_argument_values with | Just stack' -> @@ -4289,9 +4377,9 @@ let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evalua match l with | SL_simple (SL_memory_address a) -> (*let _ = my_debug5 ("OpSem_fbreg: a = "^ pphex a ^ "\n") in*) - let vi = ((integerFromNatural a) + i) mod (integerFromNatural ac.ac_all) in + let vi = ((symIntegerFromNatural a) + i) mod (symIntegerFromNatural 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 + let v = partialSymNaturalFromInteger vi (*ac.ac_half (symIntegerFromNatural ac.ac_all)*) in push_memory_address v s.s_stack | _ -> Fail "OpSem_fbreg got a non-SL_simple (SL_memory_address _) result" @@ -4333,7 +4421,7 @@ let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evalua 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 + let value' = SL_implicit (bytes_of_sym_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" @@ -4362,18 +4450,18 @@ let rec evaluate_operation_list (c:p_context) (dloc: location_list_list) (evalua end end -and evaluate_location_description_bytes (c:p_context) (dloc: location_list_list) (evaluated_frame_info: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: maybe attribute_value) (pc: natural) (bs: byte_sequence) : error single_location = +and evaluate_location_description_bytes (c:p_context) (dloc: location_list_list) (evaluated_frame_info: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: maybe attribute_value) (pc: sym_natural) (bs: sym_byte_sequence) : error single_location = let parse_context = <|pc_bytes = bs; pc_offset = 0 |> in match parse_operations c cuh parse_context with | PR_fail s pc' -> Fail ("evaluate_location_description_bytes: parse_operations fail: " ^ pp_parse_fail s pc') | PR_success ops pc' -> - if Byte_sequence.length pc'.pc_bytes <> 0 then + if sym_bs_length pc'.pc_bytes <> 0 then Fail "evaluate_location_description_bytes: extra non-parsed bytes" else evaluate_operation_list c dloc evaluated_frame_info cuh ac ev mfbloc pc initial_state ops end -and evaluate_location_description (c:p_context) (dloc: location_list_list) (evaluated_frame_info: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: maybe attribute_value) (pc: natural) (loc:attribute_value) : error single_location = +and evaluate_location_description (c:p_context) (dloc: location_list_list) (evaluated_frame_info: evaluated_frame_info) (cuh: compilation_unit_header) (ac: arithmetic_context) (ev: evaluation_context) (mfbloc: maybe attribute_value) (pc: sym_natural) (loc:attribute_value) : error single_location = match loc with | AV_exprloc n bs -> evaluate_location_description_bytes c dloc evaluated_frame_info cuh ac ev mfbloc pc bs @@ -4504,10 +4592,10 @@ let pp_evaluated_fde (fde, (rows: list cfa_table_row)) : string = let regs = register_footprint rows in let header : list string = "LOC" :: "CFA" :: List.map pp_cfa_register regs in let ppd_rows : list (list string) = - List.map (fun row -> pphex row.ctr_loc :: pp_cfa_rule row.ctr_cfa :: List.map (fun r -> pp_register_rule (rrp_lookup r row.ctr_regs)) regs) rows in + List.map (fun row -> pphex_sym row.ctr_loc :: pp_cfa_rule row.ctr_cfa :: List.map (fun r -> pp_register_rule (rrp_lookup r row.ctr_regs)) regs) rows in pad_rows (header :: ppd_rows) -let semi_pp_evaluated_fde (fde, (rows: list cfa_table_row)) : list (natural (*address*) * string (*cfa*) * list (string*string) (*register rules*) ) = +let semi_pp_evaluated_fde (fde, (rows: list cfa_table_row)) : list (sym_natural (*address*) * string (*cfa*) * list (string*string) (*register rules*) ) = let regs = register_footprint rows in let ppd_rows = List.map @@ -4518,7 +4606,7 @@ let semi_pp_evaluated_fde (fde, (rows: list cfa_table_row)) : list (natural (*ad rows in ppd_rows -val semi_pp_evaluated_frame_info : evaluated_frame_info -> list (natural (*address*) * string (*cfa*) * list (string*string) (*register rules*) ) +val semi_pp_evaluated_frame_info : evaluated_frame_info -> list (sym_natural (*address*) * string (*cfa*) * list (string*string) (*register rules*) ) let semi_pp_evaluated_frame_info efi = List.concat (List.map semi_pp_evaluated_fde efi) @@ -4528,7 +4616,7 @@ let semi_pp_evaluated_frame_info efi = let evaluate_call_frame_instruction (fi: frame_info) (cie: cie) (state: cfa_state) (cfi: call_frame_instruction) : cfa_state = - let create_row (loc: natural) = + let create_row (loc: sym_natural) = let row = <| state.cs_current_row with ctr_loc = loc |> in <| state with cs_current_row = row; cs_previous_rows = state.cs_current_row::state.cs_previous_rows |> in @@ -4555,7 +4643,7 @@ let evaluate_call_frame_instruction (fi: frame_info) (cie: cie) (state: cfa_stat (* CFA Definition Instructions *) | DW_CFA_def_cfa r n -> - update_cfa (CR_register r (integerFromNatural n)) + update_cfa (CR_register r (symIntegerFromNatural n)) | DW_CFA_def_cfa_sf r i -> update_cfa (CR_register r (i * cie.cie_data_alignment_factor)) | DW_CFA_def_cfa_register r -> @@ -4574,7 +4662,7 @@ let evaluate_call_frame_instruction (fi: frame_info) (cie: cie) (state: cfa_stat | DW_CFA_def_cfa_offset n -> match state.cs_current_row.ctr_cfa with | CR_register r i -> - update_cfa (CR_register r (integerFromNatural n)) + update_cfa (CR_register r (symIntegerFromNatural n)) | _ -> Assert_extra.failwith "DW_CFA_def_cfa_offset: current rule is not CR_register" end | DW_CFA_def_cfa_offset_sf i -> @@ -4592,13 +4680,13 @@ let evaluate_call_frame_instruction (fi: frame_info) (cie: cie) (state: cfa_stat | DW_CFA_same_value r -> update_reg r (RR_same_value) | DW_CFA_offset r n -> - update_reg r (RR_offset ((integerFromNatural n) * cie.cie_data_alignment_factor)) + update_reg r (RR_offset ((symIntegerFromNatural n) * cie.cie_data_alignment_factor)) | DW_CFA_offset_extended r n -> - update_reg r (RR_offset ((integerFromNatural n) * cie.cie_data_alignment_factor)) + update_reg r (RR_offset ((symIntegerFromNatural n) * cie.cie_data_alignment_factor)) | DW_CFA_offset_extended_sf r i -> update_reg r (RR_offset (i * cie.cie_data_alignment_factor)) | DW_CFA_val_offset r n -> - update_reg r (RR_val_offset ((integerFromNatural n) * cie.cie_data_alignment_factor)) + update_reg r (RR_val_offset ((symIntegerFromNatural n) * cie.cie_data_alignment_factor)) | DW_CFA_val_offset_sf r i -> update_reg r (RR_val_offset (i * cie.cie_data_alignment_factor)) | DW_CFA_register r1 r2 -> @@ -4780,7 +4868,8 @@ let analyse_type_info_top c (d: dwarf) (r:bool(*recurse into members*)) (cupdie: let typ' = strict s (find_DW_AT_type_of_die c d cu d.d_str die') in let mdata_member_location' = match atk with - | Atk_structure -> Just (strict s (find_natural_attribute_value_of_die c "DW_AT_data_member_location" die')) +(* PS 2025-06-10 make the DW_AT_data_member_location non-strict so that it doesn't fail on struct bitfield members, which have a DW_AT_bit_size and DW_AT_data_bit_offset instead. TODO: support those properly *) + | Atk_structure -> (*Just*) ((*strict s*) (find_natural_attribute_value_of_die c "DW_AT_data_member_location" die')) | Atk_union -> (find_natural_attribute_value_of_die c "DW_AT_data_member_location" die') end in (cupdie',mname',typ',mdata_member_location')) @@ -4837,7 +4926,7 @@ let analyse_type_info_top c (d: dwarf) (r:bool(*recurse into members*)) (cupdie: else - Assert_extra.failwith ("analyse_type_info_top didn't recognise tag: " ^ pphex die.die_abbreviation_declaration.ad_tag ^ " for DIE " ^ pp_cupdie3 cupdie) + Assert_extra.failwith ("analyse_type_info_top didn't recognise tag: " ^ pphex_sym die.die_abbreviation_declaration.ad_tag ^ " for DIE " ^ pp_cupdie3 cupdie) let rec analyse_type_info_deep (d: dwarf) (r:bool(*recurse_into_members*)) cupdie : c_type = @@ -5054,13 +5143,13 @@ let analyse_locations_raw c (d: dwarf) = die.die_abbreviation_declaration.ad_attribute_specifications die.die_attribute_values in - let find_ats (s:string) = myfindNonPure (fun (((at: natural), (af: natural)), ((pos: natural),(av:attribute_value))) -> attribute_encode s = at) ats in + let find_ats (s:string) = myfindNonPure (fun (((at: sym_natural), (af: sym_natural)), ((pos: sym_natural),(av:attribute_value))) -> sym_eq (attribute_encode s) at) ats in let ((_,_),(_,av_name)) = find_ats "DW_AT_name" in let name = match av_name with - | AV_string bs -> string_of_byte_sequence bs + | AV_string bs -> string_of_sym_byte_sequence bs | AV_strp n -> pp_debug_str_entry d.d_str n | _ -> "av_name AV not understood" end in @@ -5073,7 +5162,7 @@ let analyse_locations_raw c (d: dwarf) = | 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_list = myfindNonPure (fun (n',_)-> n'=n) d.d_loc in + let location_list = myfindNonPure (fun (n',_)-> sym_eq n' n) d.d_loc in pp_location_list c cuh_default location_list | _ -> "av_location AV not understood" end in @@ -5124,15 +5213,15 @@ let cu_base_address cu = -let range_of_die c cuh str (dranges: range_list_list) (cu_base_address: natural) (die: die) : maybe (list (natural * natural)) = +let range_of_die c cuh str (dranges: range_list_list) (cu_base_address: sym_natural) (die: die) : maybe (list (sym_natural * sym_natural)) = match (find_attribute_value "DW_AT_low_pc" die, find_attribute_value "DW_AT_high_pc" die, find_attribute_value "DW_AT_ranges" die) with | (Just (AV_addr n), Nothing, Nothing ) -> Just [(n,n+1)] (* unclear if this case is used? *) | (Just (AV_addr n1), Just (AV_addr n2), Nothing ) -> Just [(n1,n2)] | (Just (AV_addr n1), Just (AV_constant_ULEB128 n2), Nothing ) -> Just [(n1, n1+n2)] (* should be mod all? *) - | (Just (AV_addr n1), Just (AV_constant_SLEB128 i2), Nothing ) -> Just [(n1, naturalFromInteger (integerFromNatural n1 + i2))] (* should be mod all? *) + | (Just (AV_addr n1), Just (AV_constant_SLEB128 i2), Nothing ) -> Just [(n1, partialSymNaturalFromInteger (symIntegerFromNatural n1 + i2))] (* should be mod all? *) | (Just (AV_addr n1), Just (AV_constantN _ _), Nothing ) -> Assert_extra.failwith "AV_constantN in range_of_die" - | (Just (AV_addr n1), Just (AV_block n bs), Nothing ) -> let n2 = natural_of_bytes c.endianness bs in Just [(n1, n1+n2)] (* should be mod all? *) (* signed or unsigned interp? *) + | (Just (AV_addr n1), Just (AV_block n bs), Nothing ) -> let n2 = sym_natural_of_bytes c.endianness bs in Just [(n1, n1+n2)] (* should be mod all? *) (* signed or unsigned interp? *) | (_, Nothing, Just (AV_sec_offset n)) -> let rlis = Tuple.snd (match find_range_list dranges n with Just rlis->rlis | None -> Assert_extra.failwith ("find_range_list failed on AV_sec_offset n=" ^ show n ^ " for die\n" ^ pp_die c cuh str false 0 false die) end) in let nns = interpret_range_list cu_base_address rlis in @@ -5141,18 +5230,18 @@ let range_of_die c cuh str (dranges: range_list_list) (cu_base_address: natural) | (_, _, _ ) -> Just [] (*Assert_extra.failwith "unexpected attribute values in closest_enclosing_range"*) end -let range_of_die_d (d:dwarf) cu (die: die) : maybe (list (natural * natural)) = +let range_of_die_d (d:dwarf) cu (die: die) : maybe (list (sym_natural * sym_natural)) = let c = p_context_of_d d in range_of_die c cu.cu_header d.d_str d.d_ranges (cu_base_address cu) die -let entry_address (die:die) : maybe natural = +let entry_address (die:die) : maybe sym_natural = match (find_attribute_value "DW_AT_low_pc" die, find_attribute_value "DW_AT_entry_pc" die) with | (_, Just (AV_addr n)) -> Just n | (Just (AV_addr n), _) -> Just n | (Nothing,Nothing) -> Nothing end -let rec closest_enclosing_range c cuh str (dranges: range_list_list) (cu_base_address: natural) (parents: list die) : maybe (list (natural * natural)) = +let rec closest_enclosing_range c cuh str (dranges: range_list_list) (cu_base_address: sym_natural) (parents: list die) : maybe (list (sym_natural * sym_natural)) = match parents with | [] -> Nothing | die::parents' -> @@ -5172,7 +5261,7 @@ rather than DW_FORM_data. 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_address: natural) (parents: list die) : maybe attribute_value = +let rec closest_enclosing_frame_base dloc (base_address: sym_natural) (parents: list die) : maybe attribute_value = match parents with | [] -> Nothing | die::parents' -> @@ -5182,15 +5271,11 @@ let rec closest_enclosing_frame_base dloc (base_address: natural) (parents: list end end - - - -let interpreted_location_of_die c cuh str (dloc: location_list_list) (dranges: range_list_list) (base_address: natural) (parents: list die) (die: die) : maybe (list (natural * natural * single_location_description)) = - +let interpreted_location c cuh str (dloc: location_list_list) (dranges: range_list_list) (base_address: sym_natural) (parents: list die) loc : maybe (list (sym_natural * sym_natural * single_location_description)) = (* 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 cuh str dranges base_address (die::parents) with + match closest_enclosing_range c cuh str dranges base_address parents with | Just nns -> Just (List.map (fun (n1,n2) -> (n1,n2,bs)) nns) | Nothing -> @@ -5198,7 +5283,7 @@ let interpreted_location_of_die c cuh str (dloc: location_list_list) (dranges: r Just [(0,(arithmetic_context_of_cuh cuh).ac_max,bs)] end in - match find_attribute_value "DW_AT_location" die with + match loc with | Just (AV_exprloc n bs) -> location bs | Just (AV_block n bs) -> location bs (* while for a location list, we take the associated pc range from @@ -5209,7 +5294,9 @@ let interpreted_location_of_die c cuh str (dloc: location_list_list) (dranges: r | Nothing -> Nothing end - +let interpreted_location_of_die c cuh str (dloc: location_list_list) (dranges: range_list_list) (base_address: sym_natural) (parents: list die) (die: die) : maybe (list (sym_natural * sym_natural * single_location_description)) = + let loc = find_attribute_value "DW_AT_location" die in + interpreted_location c cuh str dloc dranges base_address (die::parents) loc val analyse_locations : dwarf -> analysed_location_data let analyse_locations (d: dwarf) : analysed_location_data = @@ -5232,7 +5319,7 @@ let analyse_locations (d: dwarf) : analysed_location_data = List.map (fun (((cu:compilation_unit), (parents: list die), (die: die)) as x) -> let base_address = cu_base_address cu in - let interpreted_locations : maybe (list (natural * natural * single_location_description)) = + let interpreted_locations : maybe (list (sym_natural * sym_natural * single_location_description)) = interpreted_location_of_die c cu.cu_header d.d_str d.d_loc d.d_ranges base_address parents die in (x,interpreted_locations) ) @@ -5240,10 +5327,10 @@ let analyse_locations (d: dwarf) : analysed_location_data = -let pp_analysed_locations1 c cuh (nnls: list (natural * natural * single_location_description)) : string = +let pp_analysed_locations1 c cuh (nnls: list (sym_natural * sym_natural * single_location_description)) : string = String.concat "" (List.map - (fun (n1,n2,bs) -> " " ^ pphex n1 ^ " " ^ pphex n2 ^ " " ^ parse_and_pp_operations c cuh bs) + (fun (n1,n2,bs) -> " " ^ pphex_sym n1 ^ " " ^ pphex_sym n2 ^ " " ^ parse_and_pp_operations c cuh bs) nnls) let pp_analysed_locations2 c cuh mnnls = @@ -5362,11 +5449,11 @@ let pp_analysed_location_data_at_pc (d: dwarf) (alspc: analysed_location_data_at -val analysed_locations_at_pc : evaluation_context -> dwarf_static -> natural -> analysed_location_data_at_pc +val analysed_locations_at_pc : evaluation_context -> dwarf_static -> sym_natural -> analysed_location_data_at_pc let analysed_locations_at_pc (ev) (ds: dwarf_static) - (pc: natural) + (pc: sym_natural) : analysed_location_data_at_pc = let c : p_context = (<| endianness = ds.ds_dwarf.d_endianness |>) in @@ -5403,11 +5490,11 @@ let analysed_locations_at_pc ) xs) -val names_of_address : dwarf -> analysed_location_data_at_pc -> natural -> list string +val names_of_address : dwarf -> analysed_location_data_at_pc -> sym_natural -> list string let names_of_address (d: dwarf) (alspc: analysed_location_data_at_pc) - (address: natural) + (address: sym_natural) : list string = List.mapMaybe @@ -5428,7 +5515,7 @@ let names_of_address alspc -val filtered_analysed_location_data : dwarf_static -> natural -> analysed_location_data +val filtered_analysed_location_data : dwarf_static -> sym_natural -> analysed_location_data let filtered_analysed_location_data ds pc = List.mapMaybe (fun (cupd,mnns) -> @@ -5480,7 +5567,7 @@ let filtered_analysed_location_data ds pc = -let subprogram_line_extents_compilation_unit d cu : list (string * unpacked_file_entry * natural) = +let subprogram_line_extents_compilation_unit d cu : list (string * unpacked_file_entry * sym_natural) = let c = p_context_of_d d in let subprogram_dies = List.filter (fun die' -> die'.die_abbreviation_declaration.ad_tag = tag_encode "DW_TAG_subprogram") cu.cu_die.die_children in @@ -5530,8 +5617,8 @@ let rec partitionby f lt xs acc = partitionby f lt xs' acc'' end -let subprogram_line_extents d : list (unpacked_file_entry * list (string * unpacked_file_entry * natural) ) = - let subprograms : list (string * unpacked_file_entry * natural) = +let subprogram_line_extents d : list (unpacked_file_entry * list (string * unpacked_file_entry * sym_natural) ) = + let subprograms : list (string * unpacked_file_entry * sym_natural) = List.concatMap (subprogram_line_extents_compilation_unit d) d.d_compilation_units in partitionby (fun (name, ufe, line) -> ufe) (fun (name,ufe,line) -> fun (name',ufe',line') -> line < line') subprograms [] @@ -5550,7 +5637,7 @@ let rec find_by_line line sles line_last name_last = if line >= line_last && line < line' then name_last else find_by_line line sles' line' name' end -let subprogram_at_line subprogram_line_extents (ufe:unpacked_file_entry) (line:natural) : string = +let subprogram_at_line subprogram_line_extents (ufe:unpacked_file_entry) (line:sym_natural) : string = match List.lookup ufe subprogram_line_extents with | Nothing -> "no matching unpacked_file_entry" | Just sles -> find_by_line line sles 0 "file preamble" @@ -5596,7 +5683,7 @@ let analyse_subprograms (d: dwarf) : analysed_location_data = | let base_address = cu_base_address cu in - let interpreted_locations : maybe (list (natural * natural * single_location_description)) = + let interpreted_locations : maybe (list (sym_natural * sym_natural * single_location_description)) = interpreted_location_of_die c cuh_default d.d_loc d.d_ranges base_address parents die in (x,interpreted_locations) ) @@ -5639,10 +5726,10 @@ let evaluate_line_number_operation match lno with | DW_LN_special adjusted_opcode -> let operation_advance = adjusted_opcode / lnh.lnh_line_range in - let line_increment = lnh.lnh_line_base + integerFromNatural (adjusted_opcode mod lnh.lnh_line_range) in + let line_increment = lnh.lnh_line_base + symIntegerFromNatural (adjusted_opcode mod lnh.lnh_line_range) in let s' = <| s with - lnr_line = partialNaturalFromInteger ((integerFromNatural s.lnr_line) + line_increment); + lnr_line = partialSymNaturalFromInteger ((symIntegerFromNatural s.lnr_line) + line_increment); lnr_address = new_address s operation_advance; lnr_op_index = new_op_index s operation_advance; |> in @@ -5673,7 +5760,7 @@ let evaluate_line_number_operation |> in (s', lnrs) | DW_LNS_advance_line line_increment -> - let s' = <| s with lnr_line = partialNaturalFromInteger ((integerFromNatural s.lnr_line) + line_increment) |> in (s', lnrs) + let s' = <| s with lnr_line = partialSymNaturalFromInteger ((symIntegerFromNatural 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 -> @@ -5745,7 +5832,7 @@ let evaluate_line_number_program let evaluated_line_info_of_compilation_unit d cu evaluated_line_info = let c = p_context_of_d d in let offset = line_number_offset_of_compilation_unit c cu in - match List.find (fun (lnh,lnrs) -> lnh.lnh_offset = offset) evaluated_line_info with + match List.find (fun (lnh,lnrs) -> sym_eq lnh.lnh_offset offset) evaluated_line_info with | Nothing -> Assert_extra.failwith "compilation unit line number offset not found" | Just (lnh,lnrs) ->lnrs end @@ -5753,7 +5840,7 @@ let evaluated_line_info_of_compilation_unit d cu evaluated_line_info = let pp_line_number_registers lnr = "" - ^ "address = " ^ pphex lnr.lnr_address ^ "\n" + ^ "address = " ^ pphex_sym lnr.lnr_address ^ "\n" ^ "op_index = " ^ show lnr.lnr_op_index ^ "\n" ^ "file = " ^ show lnr.lnr_file ^ "\n" ^ "line = " ^ show lnr.lnr_line ^ "\n" @@ -5764,11 +5851,11 @@ let pp_line_number_registers lnr = ^ "prologue_end = " ^ show lnr.lnr_prologue_end ^ "\n" ^ "epilogue_begin = " ^ show lnr.lnr_epilogue_begin ^ "\n" ^ "isa = " ^ show lnr.lnr_isa ^ "\n" - ^ "discriminator = " ^ pphex lnr.lnr_discriminator ^ "\n" + ^ "discriminator = " ^ pphex_sym lnr.lnr_discriminator ^ "\n" let pp_line_number_registers_tight lnr : list string = [ - pphex lnr.lnr_address ; + pphex_sym lnr.lnr_address ; show lnr.lnr_op_index ; show lnr.lnr_file ; show lnr.lnr_line ; @@ -5779,7 +5866,7 @@ let pp_line_number_registers_tight lnr : list string = show lnr.lnr_prologue_end ; show lnr.lnr_epilogue_begin ; show lnr.lnr_isa ; - pphex lnr.lnr_discriminator + pphex_sym lnr.lnr_discriminator ] let pp_line_number_registerss lnrs = @@ -5821,7 +5908,7 @@ CU: /var/local/stephen/work/devel/rsem/ppcmem2/system/tests-adhoc/simple-malloc/ -let source_lines_of_address (ds:dwarf_static) (a: natural) : list ( unpacked_file_entry * natural * line_number_registers * string (*function*)) = +let source_lines_of_address (ds:dwarf_static) (a: sym_natural) : list ( unpacked_file_entry * sym_natural * line_number_registers * string (*function*)) = List.concat (List.map (fun (lnh, lnrs) -> @@ -5843,12 +5930,12 @@ let source_lines_of_address (ds:dwarf_static) (a: natural) : list ( unpacked_fil (** ** collecting all the statically calculated analysis info *) (** ************************************************************ *) -val extract_dwarf_static : elf_file -> maybe dwarf_static -let extract_dwarf_static f1 = - match extract_dwarf f1 with +val extract_dwarf_static : elf_file -> relocation_interpreter reloc_target_data -> maybe dwarf_static +let extract_dwarf_static f1 ri = + match extract_dwarf f1 ri with | Nothing -> Nothing | Just dwarf -> - (*let _ = my_debug5 (pp_dwarf dwarf) in *) + let _ = my_debug5 (pp_dwarf dwarf) in let ald : analysed_location_data = analyse_locations dwarf in @@ -5883,7 +5970,7 @@ let decl_of_die d subprogram_line_extents cu die : maybe (unpacked_file_entry * | (Just file, Just line) -> let ufe = unpack_file_entry lnh file in let subprogram_name = subprogram_at_line subprogram_line_extents ufe line in - Just (ufe, natFromNatural line, subprogram_name) + Just (ufe, natFromSymNatural line, subprogram_name) | (_,_) -> Nothing end @@ -5897,7 +5984,7 @@ let call_site_of_die d subprogram_line_extents cu die : maybe (unpacked_file_ent | (Just file, Just line) -> let ufe = unpack_file_entry lnh file in let subprogram_name = subprogram_at_line subprogram_line_extents ufe line in - Just (ufe, natFromNatural line, subprogram_name) + Just (ufe, natFromSymNatural line, subprogram_name) | (_,_) -> Nothing end @@ -5931,6 +6018,8 @@ let rec mk_sdt_variable_or_formal_parameter (d:dwarf) subprogram_line_extents cu (* find aDW_AT_specification die, if it exists. TODO: how should this interact with abstract origins? *) let mcupdie_spec = find_reference_attribute_of_die c d cu d.d_str "DW_AT_specification" die in + let base_address = cu_base_address cu in + Just ( <| svfp_cupdie = cupdie; @@ -5948,9 +6037,12 @@ let rec mk_sdt_variable_or_formal_parameter (d:dwarf) subprogram_line_extents cu svfp_const_value = find_integer_attribute_value_of_die c "DW_AT_const_value" die; svfp_external = match find_flag_attribute_value_of_die_using_abstract_origin d "DW_AT_external" cupdie with Just b -> b | Nothing -> false end; svfp_declaration = match find_flag_attribute_value_of_die_using_abstract_origin d "DW_AT_declaration" cupdie with Just b -> b | Nothing -> false end; + svfp_locations_frame_base = + let frame_base = closest_enclosing_frame_base d.d_loc base_address (die::parents) in + let interpreted_frame_base = interpreted_location c cu.cu_header d.d_str d.d_loc d.d_ranges base_address (die::parents) frame_base in + Maybe.map (fun nnbss -> List.map (fun (n1,n2,bs) -> (n1,n2,parse_operations_bs c cu.cu_header bs)) nnbss) interpreted_frame_base; svfp_locations = - let base_address = cu_base_address cu in - let interpreted_locations : maybe (list (natural * natural * single_location_description)) = + let interpreted_locations : maybe (list (sym_natural * sym_natural * single_location_description)) = interpreted_location_of_die c cu.cu_header d.d_str d.d_loc d.d_ranges base_address parents die in Maybe.map (fun nnbss -> List.map (fun (n1,n2,bs) -> (n1,n2,parse_operations_bs c cu.cu_header bs)) nnbss) interpreted_locations; svfp_decl = decl_of_die d subprogram_line_extents cu die; @@ -6048,20 +6140,20 @@ let mk_sdt_dwarf (d:dwarf) subprogram_line_extents : sdt_dwarf = let pp_sdt_unspecified_parameter (level:natural) (sup:sdt_unspecified_parameter) : string = indent_level true level ^ "unspecified parameters" ^ "\n" -let pp_parsed_single_location_description (level:natural) ((n1:natural), (n2:natural), (ops:list operation)) : string = +let pp_parsed_single_location_description (level:natural) ((n1:sym_natural), (n2:sym_natural), (ops:list operation)) : string = let indent = indent_level true level in indent - ^ pphex n1 - ^ " " ^ pphex n2 + ^ pphex_sym n1 + ^ " " ^ pphex_sym n2 ^ " (" ^ pp_operations ops ^")" ^"\n" -let pp_pc_ranges (level:natural) (rso:maybe (list (natural*natural))) = +let pp_pc_ranges (level:natural) (rso:maybe (list (sym_natural*sym_natural))) = match rso with | Nothing -> "none\n" | Just rs -> let indent = indent_level true level in - "\n" ^ String.concat "" (List.map (fun (n1,n2) -> indent ^ pphex n1 ^ " " ^ pphex n2 ^ "\n") rs) + "\n" ^ String.concat "" (List.map (fun (n1,n2) -> indent ^ pphex_sym n1 ^ " " ^ pphex_sym n2 ^ "\n") rs) end let pp_sdt_maybe x f = match x with Nothing -> "none\n" | Just y -> f y end @@ -6093,7 +6185,7 @@ let rec pp_sdt_subroutine (level:natural) (ss:sdt_subroutine) : string = ^ indent ^ "type:" ^ pp_sdt_maybe ss.ss_type (fun typ -> pp_type_info_deep typ ^"\n") ^ indent ^ "vars:" ^ pp_sdt_list ss.ss_vars (pp_sdt_variable_or_formal_parameter (level+1)) ^ indent ^ "unspecified_parameters:" ^ pp_sdt_list ss.ss_unspecified_parameters (pp_sdt_unspecified_parameter (level+1)) - ^ indent ^ "entry address: " ^ pp_sdt_maybe ss.ss_entry_address (fun n -> pphex n^"\n") + ^ indent ^ "entry address: " ^ pp_sdt_maybe ss.ss_entry_address (fun n -> pphex_sym n^"\n") ^ indent ^ "pc ranges:" ^ pp_pc_ranges (level+1) ss.ss_pc_ranges ^ indent ^ "subroutines:" ^ pp_sdt_list ss.ss_subroutines (pp_sdt_subroutine (level+1)) ^ indent ^ "lexical_blocks:" ^ pp_sdt_list ss.ss_lexical_blocks (pp_sdt_lexical_block (level+1)) @@ -6164,7 +6256,7 @@ let rec pp_sdt_locals_subroutine (level:natural) (ss:sdt_subroutine) : string = ^ indent (*^ "name:" ^*) ^ pp_sdt_maybe ss.ss_name (fun name -> name ^ "\n") (* ^ indent ^ "cupdie:" ^ pp_cupdie3 ss.ss_cupdie ^ "\n"*) ^ indent ^ "kind:" ^ (match ss.ss_kind with SSK_subprogram -> "subprogram" | SSK_inlined_subroutine -> "inlined subroutine" end) ^ "\n" - ^ indent ^ "entry address: " ^ pp_sdt_maybe ss.ss_entry_address (fun n -> pphex n^"\n") + ^ indent ^ "entry address: " ^ pp_sdt_maybe ss.ss_entry_address (fun n -> pphex_sym n^"\n") ^ indent ^ "call site:" ^ pp_sdt_maybe ss.ss_call_site (fun ud -> "\n" ^ indent_level true (level+1) ^ pp_ud ud ^ "\n") ^ indent ^ "abstract origin:" ^ pp_sdt_maybe ss.ss_abstract_origin (fun s -> "\n" ^ pp_sdt_locals_subroutine (level+1) s) (* ^ indent ^ "type:" ^ pp_sdt_maybe ss.ss_type (fun typ -> pp_type_info_deep typ ^"\n" end)*) @@ -6239,8 +6331,8 @@ let analyse_inlined_subroutines (d: dwarf) : inlined_subroutine_data = let file_index = strict_ais (find_natural_attribute_value_of_die c "DW_AT_call_file" die) "no DW_AT_call_file" s inlined_subroutine in unpack_file_entry (line_number_program_of_compilation_unit d cu).lnp_header file_index in (* match filename d cu file_index with | Just s -> s | Nothing -> "none" end in*) - let call_line : natural = strict_ais (find_natural_attribute_value_of_die c "DW_AT_call_line" die) "no DW_AT_call_line" s inlined_subroutine in - let pc_ranges : list (natural*natural) = + let call_line : sym_natural = strict_ais (find_natural_attribute_value_of_die c "DW_AT_call_line" die) "no DW_AT_call_line" s inlined_subroutine in + let pc_ranges : list (sym_natural*sym_natural) = strict_ais (closest_enclosing_range c d.d_ranges (cu_base_address cu) [die](*deliberately ignore parents*)) "no pc ranges" s inlined_subroutine in let const_params = @@ -6291,10 +6383,10 @@ let rec analyse_inlined_subroutines_sdt_subroutine (sdt_parents: list sdt_subrou let this : list inlined_subroutine = match (ss.ss_kind, ss.ss_abstract_origin) with | (SSK_inlined_subroutine, Just ss') -> - let ((call_file:unpacked_file_entry),(call_line:natural)) = + let ((call_file:unpacked_file_entry),(call_line:sym_natural)) = match ss.ss_call_site with | Just (((ufe,line,subprogram_name) as ud):unpacked_decl) -> - (ufe,naturalFromNat line) + (ufe,symNaturalFromNat line) | Nothing -> Assert_extra.failwith "analyse_inlined_subroutines_sdt_subroutine found no ss_call_site" end in @@ -6337,7 +6429,7 @@ let analyse_inlined_subroutines_sdt_dwarf (sd: sdt_dwarf) : list inlined_subrout let analyse_inlined_subroutine_by_range (is:inlined_subroutine) : inlined_subroutine_data_by_range = let n_ranges = List.length is.is_pc_ranges in - List.mapi (fun i -> fun (n1,n2) -> ((n1,n2),(naturalFromNat i, naturalFromNat n_ranges),is)) is.is_pc_ranges + List.mapi (fun i -> fun (n1,n2) -> ((n1,n2),(symNaturalFromNat i, symNaturalFromNat n_ranges),is)) is.is_pc_ranges let is_lt ((n1,n2),(m,n),is) ((n1',n2'),(m',n'),is') = n1 < n1' || (n1 = n1' && n2 > n2') @@ -6354,7 +6446,7 @@ let rec pp_inlined_subroutine_parents (ds:list die) : string = pp_pos die.die_offset ^ ":" ^ pp_inlined_subroutine_parents ds' else if die.die_abbreviation_declaration.ad_tag = tag_encode "DW_TAG_lexical_block" then ":" ^ pp_inlined_subroutine_parents ds' else if die.die_abbreviation_declaration.ad_tag = tag_encode "DW_TAG_subprogram" then "" - else "" + else "" end @@ -6387,16 +6479,16 @@ let pp_inlined_subroutine_const_params d is = let pp_inlined_subroutine ds is = pp_inlined_subroutine_header ds is ^ "\n" - ^ String.concat "" (List.map (fun (n1,n2) -> " " ^ pphex n1 ^ " " ^ pphex n2 ^ "\n") is.is_pc_ranges) + ^ String.concat "" (List.map (fun (n1,n2) -> " " ^ pphex_sym n1 ^ " " ^ pphex_sym n2 ^ "\n") is.is_pc_ranges) ^ pp_inlined_subroutine_const_params ds.ds_dwarf is let pp_inlined_subroutines ds iss = String.concat "" (List.map (pp_inlined_subroutine ds) iss) -let pp_inlined_subroutine_by_range ds ((n1,n2),((m:natural),(n:natural)),is) = - pphex n1 ^ " " ^ pphex n2 ^ " " - ^ (if n<>1 then "("^show m^" of "^show n^") " else "") +let pp_inlined_subroutine_by_range ds ((n1,n2),((m:sym_natural),(n:sym_natural)),is) = + pphex_sym n1 ^ " " ^ pphex_sym n2 ^ " " + ^ (if n<>(sym_natural_const 1) then "("^show m^" of "^show n^") " else "") ^ pp_inlined_subroutine_header ds is ^"\n" ^ (if m=0 then pp_inlined_subroutine_const_params ds.ds_dwarf is else "") @@ -6411,30 +6503,30 @@ let pp_inlined_subroutines_by_range ds iss = (* assume 4-byte ARM instructions *) -let rec words_of_byte_sequence (addr:natural) (bs:byte_sequence) (acc:list (natural * natural)) : list (natural * natural) = - match read_4_bytes_be bs with - | Success ((b0,b1,b2,b3), bs') -> - let i : natural = natural_of_byte b0 + 256*natural_of_byte b1 + 65536*natural_of_byte b2 + 65536*256*natural_of_byte b3 in - words_of_byte_sequence (addr+4) bs' ((addr,i)::acc) +let rec words_of_sym_byte_sequence (addr:sym_natural) (bs:sym_byte_sequence) (acc:list (sym_natural * sym_natural)) : list (sym_natural * sym_natural) = + match sym_read_4_bytes_be_symbolic bs with + | Success (Bytes (b0,b1,b2,b3), bs') -> (*TODO allow symbolic? *) + let i : sym_natural = sym_natural_const (natural_of_byte b0 + 256*natural_of_byte b1 + 65536*natural_of_byte b2 + 65536*256*natural_of_byte b3) in + words_of_sym_byte_sequence (addr+4) bs' ((addr,i)::acc) | Fail _ -> List.reverse acc end -let pp_instruction ((addr:natural),(i:natural)) = - hex_string_of_big_int_pad8 addr ^ " " ^ hex_string_of_big_int_pad8 i ^ "\n" +let pp_instruction ((addr:sym_natural),(i:sym_natural)) = + hex_string_of_big_int_pad8 (sym_natural_expect_const addr (*"pp_instruction"*)) ^ " " ^ hex_string_of_big_int_pad8 (sym_natural_expect_const i (*"pp_instruction"*)) ^ "\n" -val pp_text_section : elf_file -> string -let pp_text_section f = - let (p_context, addr, bs) = extract_text f in - let instructions : list (natural * natural) = words_of_byte_sequence addr bs [] in +val pp_text_section : elf_file -> relocation_interpreter reloc_target_data -> string +let pp_text_section f ri = + let (p_context, addr, bs) = extract_text f ri in + let instructions : list (sym_natural * sym_natural) = words_of_sym_byte_sequence addr bs [] in String.concat "" (List.map pp_instruction instructions) (** ************************************************************ *) (** ** top level for main_elf ******************************** *) (** ************************************************************ *) -val harness_string_of_elf_like_objdump : elf_file -> byte_sequence -> string -let harness_string_of_elf_like_objdump f1 bs = - let mds = extract_dwarf_static f1 in +val harness_string_of_elf_like_objdump : elf_file -> relocation_interpreter reloc_target_data -> string +let harness_string_of_elf_like_objdump f1 ri = + let mds = extract_dwarf_static f1 ri in match mds with | Nothing -> "" | Just ds -> @@ -6443,9 +6535,9 @@ let harness_string_of_elf_like_objdump f1 bs = end -val harness_string_of_elf : elf_file -> byte_sequence -> string -let harness_string_of_elf f1 bs = -let mds = extract_dwarf_static f1 in +val harness_string_of_elf : elf_file -> relocation_interpreter reloc_target_data -> string +let harness_string_of_elf f1 ri = +let mds = extract_dwarf_static f1 ri in match mds with | Nothing -> "" | Just ds -> @@ -6481,22 +6573,22 @@ let mds = extract_dwarf_static f1 in end -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 {ocaml} harness_string_of_elf64_debug_info_section f1 bs0 (*os proc usr hdr sht stbl*) = - harness_string_of_elf (ELF_File_64 f1) bs0 +val harness_string_of_elf64_debug_info_section : elf64_file -> relocation_interpreter reloc_target_data -> (*(sym_natural -> string) -> (sym_natural -> string) -> (sym_natural -> string) -> elf64_header -> elf64_section_header_table -> string_table -> *) string +let {ocaml} harness_string_of_elf64_debug_info_section f1 (*os proc usr hdr sht stbl*) = + harness_string_of_elf (ELF_File_64 f1) -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 {ocaml} harness_string_of_elf32_debug_info_section f1 bs0 (*os proc usr hdr sht stbl*) = - harness_string_of_elf (ELF_File_32 f1) bs0 +val harness_string_of_elf32_debug_info_section : elf32_file -> relocation_interpreter reloc_target_data -> (* (sym_natural -> string) -> (sym_natural -> string) -> (sym_natural -> string) -> elf32_header -> elf32_section_header_table -> string_table ->*) string +let {ocaml} harness_string_of_elf32_debug_info_section f1 (*os proc usr hdr sht stbl*) = + harness_string_of_elf (ELF_File_32 f1) -val harness_string_of_elf64_like_objdump : elf64_file -> byte_sequence -> (*(natural -> string) -> (natural -> string) -> (natural -> string) -> elf64_header -> elf64_section_header_table -> string_table -> *) string -let {ocaml} harness_string_of_elf64_like_objdump f1 bs0 (*os proc usr hdr sht stbl*) = - harness_string_of_elf_like_objdump (ELF_File_64 f1) bs0 +val harness_string_of_elf64_like_objdump : elf64_file -> relocation_interpreter reloc_target_data -> (*(sym_natural -> string) -> (sym_natural -> string) -> (sym_natural -> string) -> elf64_header -> elf64_section_header_table -> string_table -> *) string +let {ocaml} harness_string_of_elf64_like_objdump f1 (*os proc usr hdr sht stbl*) = + harness_string_of_elf_like_objdump (ELF_File_64 f1) -val harness_string_of_elf32_like_objdump : elf32_file -> byte_sequence -> (* (natural -> string) -> (natural -> string) -> (natural -> string) -> elf32_header -> elf32_section_header_table -> string_table ->*) string -let {ocaml} harness_string_of_elf32_like_objdump f1 bs0 (*os proc usr hdr sht stbl*) = - harness_string_of_elf_like_objdump (ELF_File_32 f1) bs0 +val harness_string_of_elf32_like_objdump : elf32_file -> relocation_interpreter reloc_target_data -> (* (sym_natural -> string) -> (sym_natural -> string) -> (sym_natural -> string) -> elf32_header -> elf32_section_header_table -> string_table ->*) string +let {ocaml} harness_string_of_elf32_like_objdump f1 (*os proc usr hdr sht stbl*) = + harness_string_of_elf_like_objdump (ELF_File_32 f1) diff --git a/src/dwarf_byte_sequence.lem b/src/dwarf_byte_sequence.lem new file mode 100644 index 0000000..a94fb98 --- /dev/null +++ b/src/dwarf_byte_sequence.lem @@ -0,0 +1,209 @@ +open import Byte_sequence +open import Sym +open import Num +open import Map +open import Set +open import Error +open import Maybe +open import Bool +open import Basic_classes +open import Show +open import String +open import List + +type sym_mask_entry = + | NoSym of natural + | SymVal of natural * sym_natural + +let rec sym_mask_pp sm = match sm with +| NoSym x :: sm -> "NoSym(" ^ show x ^ ")," ^ sym_mask_pp sm +| SymVal x v :: sm -> "SymVal(" ^ show x ^ "," ^ show v ^ ")," ^ sym_mask_pp sm +| [] -> "" +end + + +let rec sym_mask_partition n sm = + if n = 0 then + ([], sm) + else + match sm with + | NoSym k :: sm -> + if k > n then + ([NoSym n], NoSym (k-n) :: sm) + else + let (l,r) = sym_mask_partition (n-k) sm in + (NoSym k :: l, r) + | SymVal k v :: sm -> + if k > n then + Assert_extra.failwith "Attempting to split seqence in the middle of symbolic part" + else + let (l,r) = sym_mask_partition (n-k) sm in + (SymVal k v :: l, r) + end + +let sym_mask_dropbytes n sm = + let (_,r) = sym_mask_partition n sm in r + +let sym_mask_takebytes n sm = + let (l,_) = sym_mask_partition n sm in l + +let sym_mask_is_symbolic = function +| [NoSym _] -> false +| [] -> false +| _ -> true +end + +let sym_mask_pad_nosym n sm = + if n = 0 then + sm + else match sm with + | NoSym m :: sm -> NoSym (n+m) :: sm + | _ -> NoSym n :: sm +end + +(* TODO strict mode? *) +let rec sym_mask_from_map' m i l acc = + if i = l then + List.reverse acc + else + match Map.lookup i m with + | Nothing -> sym_mask_from_map' m (i+1) l (sym_mask_pad_nosym 1 acc) + | Just (w, v) -> sym_mask_from_map' m (i + w) l (SymVal w v :: acc) + end + +let sym_mask_from_map m l = + sym_mask_from_map' m 0 l [] + +(* ================= *) +(* sym_byte_sequence *) +(* ================= *) + +type sym_byte_sequence = +<| sbs_bytes : byte_sequence + ; sbs_symbolic : list sym_mask_entry + |> + +let sym_read_char bs = + read_char bs.sbs_bytes >>= fun (c, bs') -> + match bs.sbs_symbolic with + | SymVal n v :: _ -> Assert_extra.failwith + ("Read char: is symbolic (width: " ^ show n ^ ") " ^ show v) + | _ -> + return (c, <| sbs_bytes=bs'; sbs_symbolic = sym_mask_dropbytes 1 bs.sbs_symbolic |>) + end + +let sym_read_2_bytes_be bs0 = + sym_read_char bs0 >>= fun (b0, bs1) -> + sym_read_char bs1 >>= fun (b1, bs2) -> + return ((b0, b1), bs2) + +let sym_read_4_bytes_be bs0 = + sym_read_char bs0 >>= fun (b0, bs1) -> + sym_read_char bs1 >>= fun (b1, bs2) -> + sym_read_char bs2 >>= fun (b2, bs3) -> + sym_read_char bs3 >>= fun (b3, bs4) -> + return ((b0, b1, b2, b3), bs4) + +let sym_read_8_bytes_be bs0 = + sym_read_char bs0 >>= fun (b0, bs1) -> + sym_read_char bs1 >>= fun (b1, bs2) -> + sym_read_char bs2 >>= fun (b2, bs3) -> + sym_read_char bs3 >>= fun (b3, bs4) -> + sym_read_char bs4 >>= fun (b4, bs5) -> + sym_read_char bs5 >>= fun (b5, bs6) -> + sym_read_char bs6 >>= fun (b6, bs7) -> + sym_read_char bs7 >>= fun (b7, bs8) -> + return ((b0, b1, b2, b3, b4, b5, b6, b7), bs8) + +let sym_dropbytes n bs = + dropbytes n bs.sbs_bytes >>= fun bs' -> + return <| sbs_bytes=bs'; sbs_symbolic=sym_mask_dropbytes n bs.sbs_symbolic |> + +let sym_takebytes n bs = + takebytes n bs.sbs_bytes >>= fun bs' -> + return <| sbs_bytes=bs'; sbs_symbolic=sym_mask_takebytes n bs.sbs_symbolic |> + +let sym_partition idx bs0 = + sym_takebytes idx bs0 >>= fun l -> + sym_dropbytes idx bs0 >>= fun r -> + return (l, r) + +let sym_bs_length bs = + Byte_sequence.length bs.sbs_bytes + +val print_endline : string -> unit +declare ocaml target_rep function print_endline = `print_endline` +(* +let symbolic_bytes_in_range off len bs = + let _ = print_endline "slow operation" in + let sym_positions = Map.domain bs.sbs_symbolic in + Set.any (fun x -> x >= bs.sbs_pos + off && x < bs.sbs_pos + off + len) sym_positions *) + +let sym_bs_expect_const bs = + let len = sym_bs_length bs in + if sym_mask_is_symbolic bs.sbs_symbolic then + Assert_extra.failwith "Byte sequence is symbolic" + else + bs.sbs_bytes + +let sym_bs_construct bs sym = + let len = Byte_sequence.length bs in + <| sbs_bytes=bs; sbs_symbolic=sym_mask_from_map sym len |> + +let sym_find_byte bs b = + match find_byte bs.sbs_bytes b with + | Nothing -> + if sym_mask_is_symbolic bs.sbs_symbolic then + Assert_extra.failwith "Find encountered symbolic bytes" + else + Nothing + | Just n -> + if sym_mask_is_symbolic (sym_mask_takebytes n bs.sbs_symbolic) then + Assert_extra.failwith "Find encountered symbolic bytes" + else + Just n + end + +let sym_bs_empty = sym_bs_construct Byte_sequence.empty Map.empty + +let byte_list_of_sym_byte_sequence rbs = + byte_list_of_byte_sequence (sym_bs_expect_const rbs) + +let string_of_sym_byte_sequence rbs = + string_of_byte_sequence (sym_bs_expect_const rbs) + +instance (Show sym_byte_sequence) + let show = string_of_sym_byte_sequence +end +(* Symbolic reads *) + +type read_result 'a = + | Bytes of 'a + | Sym of sym_natural + +let sym_read_4_bytes_be_symbolic bs = + match bs.sbs_symbolic with + | SymVal 4 v :: _ -> + sym_dropbytes 4 bs >>= fun bs' -> + return (Sym v, bs') + | _ -> sym_read_4_bytes_be bs >>= fun (b, bs') -> + return (Bytes b, bs') + end + +let sym_read_8_bytes_be_symbolic bs = + match bs.sbs_symbolic with + | SymVal 8 v :: _ -> + sym_dropbytes 8 bs >>= fun bs' -> + return (Sym v, bs') + | _ -> sym_read_8_bytes_be bs >>= fun (b, bs') -> + return (Bytes b, bs') + end + +let sym_ppbytes bs = + let symmsg = + if sym_mask_is_symbolic bs.sbs_symbolic then + "With symbolic bytes! " (*TODO print them*) + else + "" + in + symmsg ^ (show (List.map (fun x -> show x) (byte_list_of_byte_sequence bs.sbs_bytes))) diff --git a/src/elf_symbolic.lem b/src/elf_symbolic.lem new file mode 100644 index 0000000..23b1377 --- /dev/null +++ b/src/elf_symbolic.lem @@ -0,0 +1,150 @@ +open import Basic_classes +open import Num +open import Error +open import Byte_sequence +open import Bool +open import Maybe +open import String +open import Show + +(* TODO for debugging, remove *) +val print_endline : string -> unit +declare ocaml target_rep function print_endline = `print_endline` + + +open import Elf_types_native_uint +open import Elf_relocation +open import Elf_symbol_table +open import Elf_file +open import Elf_header +open import Elf_section_header_table +open import Elf_interpreted_section + +(* Symbolic expressions *) + +(* TODO *) +type binary_operation + = Add + | Sub + | And + +type unary_operation = | Not + +(* TODO *) +type symbolic_expression + = Section of string + | Const of integer + | BinOp of (symbolic_expression * binary_operation * symbolic_expression) + | UnOp of (unary_operation * symbolic_expression) + +let rec pp_sym_expr sx = match sx with + | Section s -> s + | Const x -> show x + | BinOp (a, Add, b) -> "(" ^ (pp_sym_expr a) ^ "+" ^ (pp_sym_expr b) ^ ")" + | BinOp (a, Sub, b) -> "(" ^ (pp_sym_expr a) ^ "-" ^ (pp_sym_expr b) ^ ")" + | BinOp (a, And, b) -> "(" ^ (pp_sym_expr a) ^ "&" ^ (pp_sym_expr b) ^ ")" + | UnOp (Not, b) -> "(" ^ "~" ^ (pp_sym_expr b) ^ ")" +end + +val section_with_offset : elf64_file -> elf64_half -> elf64_addr -> error symbolic_expression +let section_with_offset f sidx offset = + match List.index f.elf64_file_interpreted_sections (natFromNatural (natural_of_elf64_half sidx)) with + | Nothing -> fail ("Invalid secion id " ^ show sidx) + | Just sec -> return (BinOp(Section sec.elf64_section_name_as_string, Add, Const (integerFromNatural (natural_of_elf64_addr offset)))) +end + +(* TODO handle special shndx *) +let symbolic_address_from_elf64_symbol_table_entry f ste = + if natural_of_elf64_half ste.elf64_st_shndx = shn_undef then + let name = natural_of_elf64_word ste.elf64_st_name in + get_elf64_file_symbol_string_table f >>= fun strtab -> + String_table.get_string_at name strtab >>= fun str -> + return (Section ("UND."^str)) + else + section_with_offset f ste.elf64_st_shndx ste.elf64_st_value + +let symbolic_address_of_symbol f symtab sym = + match List.index symtab sym with + | Nothing -> Nothing + | Just ste -> Just (symbolic_address_from_elf64_symbol_table_entry f ste) + end + +(* Relocation expressions *) + +type safety_check = +| Overflow of (integer * integer) +| Alignment of natural + +type relocation_description 'v 'tar = +<| rel_desc_value : 'v + ; rel_desc_checks : list safety_check + ; rel_desc_mask : (natural * natural) + ; rel_desc_target : 'tar + |> + +let relocation_map_target f desc = + f desc.rel_desc_target >>= fun target -> + return <| rel_desc_value = desc.rel_desc_value + ; rel_desc_checks = desc.rel_desc_checks + ; rel_desc_mask = desc.rel_desc_mask + ; rel_desc_target = target + |> + +(* TODO rename *) +type universal_relocation 'a = relocation_description symbolic_expression 'a + +type reloc_target_data = + | Data32 + | Data64 + +let reloc_width_bytes : reloc_target_data -> natural = function + | Data32 -> 4 + | Data64 -> 8 +end + +type relocation_interpreter 'a = elf64_file -> elf64_symbol_table -> elf64_half -> elf64_relocation_a -> + error (Map.map elf64_addr (universal_relocation 'a)) + +let relocation_interpreter_map_target interp conv ef symtab sidx rel = + interp ef symtab sidx rel >>= fun arels -> + map_mapM (fun arel -> + relocation_map_target conv arel + ) arels + +val extract_elf64_relocations_for_section' : forall 'a. elf64_file -> relocation_interpreter 'a -> elf64_half -> error (Map.map elf64_addr (universal_relocation 'a)) +let extract_elf64_relocations_for_section' f1 interp sidx = + let hdr = f1.elf64_file_header in + let sections = f1.elf64_file_interpreted_sections in + let endian = get_elf64_header_endianness hdr in + let cond x = + (x.elf64_section_type = sht_rela) && (x.elf64_section_info = natural_of_elf64_half sidx) + in + match List.filter cond sections with + | [] -> return Map.empty + | [rel_sec] -> + let lnk = rel_sec.elf64_section_link in + let rels = rel_sec.elf64_section_body in + Elf_relocation.read_elf64_relocation_a_section' endian rels >>= fun rels -> + Elf_file.get_elf64_symbol_table_by_index f1 lnk >>= fun symtab -> + (* let symtab_map = symbol_map_from_elf64_symtab f1 symtab in *) + mapM (interp f1 symtab sidx) rels >>= fun rel_maps -> + let rel_map = Map.fromList (List.concatMap Map_extra.toList rel_maps) in + if Map.size rel_map <> List.length rels then + fail "Multiple relocations at the same location" + else + return rel_map + | _ -> fail "Multiple relocation sections for this section" +end + +val extract_elf64_relocations_for_section : forall 'a. elf64_file -> relocation_interpreter 'a -> string -> error (Map.map elf64_addr (universal_relocation 'a)) +let extract_elf64_relocations_for_section f1 interp section_name = + match List.findIndices + (fun x -> x.elf64_section_name_as_string = section_name) + f1.elf64_file_interpreted_sections + with + | [sidx] -> + let sidx = elf64_half_of_natural (naturalFromNat sidx) in + extract_elf64_relocations_for_section' f1 interp sidx + | [] -> fail ("" ^ section_name ^ " section not present") + | _ -> fail ("multiple " ^ section_name ^ " sections present") +end \ No newline at end of file diff --git a/src/error.lem b/src/error.lem index 57c4165..849b154 100644 --- a/src/error.lem +++ b/src/error.lem @@ -1,5 +1,7 @@ open import Basic_classes open import List +open import Map +open import Map_extra open import Maybe open import Num open import String @@ -128,3 +130,7 @@ let string_of_error e = instance forall 'a. Show 'a => (Show (error 'a)) let show = string_of_error end + +let map_mapM f mp = + mapM (fun (k, v) -> f v >>= fun v -> return (k, v)) (Map_extra.toList mp) >>= fun xs -> + return (Map.fromList xs) diff --git a/src/lem.mk b/src/lem.mk index 127b4b8..2ebcd2a 100644 --- a/src/lem.mk +++ b/src/lem.mk @@ -29,7 +29,7 @@ else OCAML_BYTE_SEQUENCE_IMPL=byte_sequence_ocaml.lem endif -LEM_UTIL_SRC := default_printing.lem missing_pervasives.lem show.lem endianness.lem multimap.lem error.lem filesystem.lem +LEM_UTIL_SRC := default_printing.lem missing_pervasives.lem show.lem endianness.lem multimap.lem error.lem filesystem.lem sym.lem # Some of the utility code is directly in ML, some in Lem; order matters! # NOTE: LEM_UTIL_SRC and ALL_UTIL_ML need to be kept in sync manually. # GAH. doing a topsort manually is a sign of failure. @@ -37,8 +37,9 @@ ALL_UTIL_ML := \ uint64_wrapper.ml uint32_wrapper.ml \ show.ml endianness.ml error.ml ml_bindings.ml missing_pervasives.ml multimap.ml \ default_printing.ml byte_sequence_wrapper.ml byte_sequence_impl.ml \ - filesystem.ml filesystem_wrapper.ml - # missing_pervasivesAuxiliary.ml multimapAuxiliary.ml + filesystem.ml filesystem_wrapper.ml \ + sym_ocaml.ml sym.ml \ + # missing_pervasivesAuxiliary.ml multimapAuxiliary.ml ALL_UTIL_ML_WO_LEM := $(filter-out $(patsubst %.lem,%.ml,$(LEM_UTIL_SRC)) $(patsubst %.lem,%Auxiliary.ml,$(LEM_UTIL_SRC)),$(ALL_UTIL_ML)) # Nasty cycle: @@ -56,11 +57,14 @@ LEM_ELF_SRC := byte_sequence.lem byte_pattern.lem byte_pattern_extra.lem \ elf_relocation.lem \ elf_interpreted_segment.lem elf_interpreted_section.lem \ elf_note.lem elf_file.lem elf_dynamic.lem \ + elf_symbolic.lem \ + dwarf_byte_sequence.lem \ dwarf_ctypes.lem dwarf.lem ldconfig.lem LEM_ABI_SRC := \ abis/abi_classes.lem memory_image.lem memory_image_orderings.lem \ abis/abi_utilities.lem \ + abis/abi_symbolic_relocation.lem \ gnu_extensions/gnu_ext_abi.lem \ abis/power64/abi_power64.lem \ abis/power64/abi_power64_elf_header.lem \ @@ -72,6 +76,7 @@ LEM_ABI_SRC := \ abis/aarch64/abi_aarch64_program_header_table.lem \ abis/aarch64/abi_aarch64_le_serialisation.lem \ abis/aarch64/abi_aarch64_relocation.lem \ + abis/aarch64/abi_aarch64_symbolic_relocation.lem \ abis/aarch64/abi_aarch64_le.lem \ abstract_linker_script.lem \ abis/amd64/abi_amd64_elf_header.lem \ diff --git a/src/main_elf.lem b/src/main_elf.lem index e867dea..74c3b71 100644 --- a/src/main_elf.lem +++ b/src/main_elf.lem @@ -32,11 +32,14 @@ open import Elf_file open import Elf_program_header_table open import Elf_section_header_table open import Elf_types_native_uint +open import Elf_symbolic open import Harness_interface open import Sail_interface +open import Abi_symbolic_relocation open import Abi_aarch64_relocation +open import Abi_aarch64_symbolic_relocation open import Abi_amd64_elf_header open import Abi_amd64_relocation @@ -186,7 +189,15 @@ let obtain_abi_specific_string_of_reloc_type mach = string_of_mips64_relocation_type*) else const "Cannot deduce ABI" - + +val interpret_data_relocation : natural -> relocation_interpreter reloc_target_data +let interpret_data_relocation mach ef symtab_map sidx rel = + if mach = elf_ma_aarch64 then + aarch64_data_relocation_interpreter ef symtab_map sidx rel + else + Error.fail "Unsupported machine" + + let _ = let res = let (flag, arg) = @@ -262,31 +273,9 @@ let _ = return lines end else if flag = "--debug-dump=info" then - Elf_file.read_elf32_file bs0 >>= fun f1 -> - get_elf32_file_section_header_string_table f1 >>= fun stbl -> - return (Dwarf.harness_string_of_elf32_debug_info_section - f1 - bs0 - (*string_of_gnu_ext_section_type - (fun x -> show x) - (fun x -> show x) - f1.elf32_file_header - f1.elf32_file_section_header_table - stbl*) - ) + Error.fail "not implemented" else if flag = "--debug-dump=dies" then - Elf_file.read_elf32_file bs0 >>= fun f1 -> - get_elf32_file_section_header_string_table f1 >>= fun stbl -> - return (Dwarf.harness_string_of_elf32_like_objdump - f1 - bs0 - (*string_of_gnu_ext_section_type - (fun x -> show x) - (fun x -> show x) - f1.elf32_file_header - f1.elf32_file_section_header_table - stbl*) - ) + Error.fail "not implemented" else failwith "Unrecognised flag" in @@ -358,7 +347,7 @@ let _ = get_elf64_file_section_header_string_table f1 >>= fun stbl -> return (Dwarf.harness_string_of_elf64_debug_info_section f1 - bs0 + (interpret_data_relocation (natural_of_elf64_half f1.elf64_file_header.elf64_machine)) (*string_of_gnu_ext_section_type (fun x -> show x) (fun x -> show x) @@ -371,7 +360,7 @@ let _ = get_elf64_file_section_header_string_table f1 >>= fun stbl -> return ("\n"^arg^": file format [...]" ^"\n\n"^ Dwarf.harness_string_of_elf64_like_objdump f1 - bs0 + (interpret_data_relocation (natural_of_elf64_half f1.elf64_file_header.elf64_machine)) (*string_of_gnu_ext_section_type (fun x -> show x) (fun x -> show x) diff --git a/src/sym.lem b/src/sym.lem new file mode 100644 index 0000000..539ae3a --- /dev/null +++ b/src/sym.lem @@ -0,0 +1,207 @@ +open import Num +open import Show +open import Bool Basic_classes + +class (SymEq 'a) + val sym_eq : 'a -> 'a -> bool +end + +(* =========== *) +(* sym_natural *) +(* =========== *) +type sym_natural +declare ocaml target_rep type sym_natural = `Sym_ocaml.Num.t` + +val sym_natural_const : natural -> sym_natural +declare ocaml target_rep function sym_natural_const = `Sym_ocaml.Num.of_num` + +val sym_natural_section : string -> sym_natural +declare ocaml target_rep function sym_natural_section = `Sym_ocaml.Num.section` + +val sym_natural_expect_const : sym_natural -> natural +declare ocaml target_rep function sym_natural_expect_const = `Sym_ocaml.Num.to_num` + +val sym_natural_map : (natural -> natural) -> sym_natural -> sym_natural +declare ocaml target_rep function sym_natural_map = `Sym_ocaml.Num.map` + +val sym_natural_map2 : (natural -> natural -> natural) -> sym_natural -> sym_natural -> sym_natural +declare ocaml target_rep function sym_natural_map2 = `Sym_ocaml.Num.map2` + +instance (Numeral sym_natural) + let fromNumeral = fun x -> sym_natural_const (fromNumeral x) +end + +val sym_natural_pp : (natural -> string) -> sym_natural -> string +declare ocaml target_rep function sym_natural_pp = `Sym_ocaml.Num.ppf` + +instance (Show sym_natural) + let show = sym_natural_pp show +end + +val sym_natural_add : sym_natural -> sym_natural -> sym_natural +declare ocaml target_rep function sym_natural_add = `Sym_ocaml.Num.add` + + +instance (NumAdd sym_natural) + let (+) = sym_natural_add +end + +val sym_natural_sub : sym_natural -> sym_natural -> sym_natural +declare ocaml target_rep function sym_natural_sub = `Sym_ocaml.Num.sub_nat` + +instance (NumMinus sym_natural) + let (-) = sym_natural_sub +end + +val sym_natural_mul : sym_natural -> sym_natural -> sym_natural +declare ocaml target_rep function sym_natural_mul = `Sym_ocaml.Num.mul` + +instance (NumMult sym_natural) + let ( * ) = sym_natural_mul +end + +val sym_natural_div : sym_natural -> sym_natural -> sym_natural +declare ocaml target_rep function sym_natural_div = `Sym_ocaml.Num.div` + +instance (NumDivision sym_natural) + let (/) = sym_natural_div +end + +val sym_natural_mod : sym_natural -> sym_natural -> sym_natural +declare ocaml target_rep function sym_natural_mod = `Sym_ocaml.Num.modulus` + +instance (NumRemainder sym_natural) + let (mod) = sym_natural_mod +end + +val sym_natural_compare : sym_natural -> sym_natural -> ordering +val sym_natural_less : sym_natural -> sym_natural -> bool +val sym_natural_less_equal : sym_natural -> sym_natural -> bool +val sym_natural_greater : sym_natural -> sym_natural -> bool +val sym_natural_greater_equal : sym_natural -> sym_natural -> bool +val sym_natural_eq : sym_natural -> sym_natural -> bool + +declare ocaml target_rep function sym_natural_compare = `Sym_ocaml.Num.compare` +declare ocaml target_rep function sym_natural_less = `Sym_ocaml.Num.less` +declare ocaml target_rep function sym_natural_less_equal = `Sym_ocaml.Num.less_equal` +declare ocaml target_rep function sym_natural_greater = `Sym_ocaml.Num.greater` +declare ocaml target_rep function sym_natural_greater_equal = `Sym_ocaml.Num.greater_equal` +declare ocaml target_rep function sym_natural_eq = `Sym_ocaml.Num.equal` + +instance (Ord sym_natural) + let compare = sym_natural_compare + let (<) = sym_natural_less + let (<=) = sym_natural_less_equal + let (>) = sym_natural_greater + let (>=) = sym_natural_greater_equal +end + +instance (SymEq sym_natural) + let sym_eq = sym_natural_eq +end + + +(* =========== *) +(* sym_integer *) +(* =========== *) +type sym_integer +declare ocaml target_rep type sym_integer = `Sym_ocaml.Num.t` + +val sym_integer_const : integer -> sym_integer +declare ocaml target_rep function sym_integer_const = `Sym_ocaml.Num.of_num` + +val sym_integer_section : string -> sym_integer +declare ocaml target_rep function sym_integer_section = `Sym_ocaml.Num.section` + +val sym_integer_expect_const : sym_integer -> integer +declare ocaml target_rep function sym_integer_expect_const = `Sym_ocaml.Num.to_num` + +val sym_integer_map : (integer -> integer) -> sym_integer -> sym_integer +declare ocaml target_rep function sym_integer_map = `Sym_ocaml.Num.map` + +val sym_integer_map2 : (integer -> integer -> integer) -> sym_integer -> sym_integer -> sym_integer +declare ocaml target_rep function sym_integer_map2 = `Sym_ocaml.Num.map2` + +instance (Numeral sym_integer) + let fromNumeral = fun x -> sym_integer_const (fromNumeral x) +end + +val sym_integer_pp : (integer -> string) -> sym_integer -> string +declare ocaml target_rep function sym_integer_pp = `Sym_ocaml.Num.ppf` + +instance (Show sym_integer) + let show = sym_integer_pp show +end + +val sym_integer_add : sym_integer -> sym_integer -> sym_integer +declare ocaml target_rep function sym_integer_add = `Sym_ocaml.Num.add` + + +instance (NumAdd sym_integer) + let (+) = sym_integer_add +end + +val sym_integer_sub : sym_integer -> sym_integer -> sym_integer +declare ocaml target_rep function sym_integer_sub = `Sym_ocaml.Num.sub` + +instance (NumMinus sym_integer) + let (-) = sym_integer_sub +end + +val sym_integer_mul : sym_integer -> sym_integer -> sym_integer +declare ocaml target_rep function sym_integer_mul = `Sym_ocaml.Num.mul` + +instance (NumMult sym_integer) + let ( * ) = sym_integer_mul +end + +val sym_integer_div : sym_integer -> sym_integer -> sym_integer +declare ocaml target_rep function sym_integer_div = `Sym_ocaml.Num.div` + +instance (NumDivision sym_integer) + let (/) = sym_integer_div +end + +val sym_integer_mod : sym_integer -> sym_integer -> sym_integer +declare ocaml target_rep function sym_integer_mod = `Sym_ocaml.Num.modulus` + +instance (NumRemainder sym_integer) + let (mod) = sym_integer_mod +end + +val sym_integer_compare : sym_integer -> sym_integer -> ordering +val sym_integer_less : sym_integer -> sym_integer -> bool +val sym_integer_less_equal : sym_integer -> sym_integer -> bool +val sym_integer_greater : sym_integer -> sym_integer -> bool +val sym_integer_greater_equal : sym_integer -> sym_integer -> bool +val sym_integer_eq : sym_integer -> sym_integer -> bool + +declare ocaml target_rep function sym_integer_compare = `Sym_ocaml.Num.compare` +declare ocaml target_rep function sym_integer_less = `Sym_ocaml.Num.less` +declare ocaml target_rep function sym_integer_less_equal = `Sym_ocaml.Num.less_equal` +declare ocaml target_rep function sym_integer_greater = `Sym_ocaml.Num.greater` +declare ocaml target_rep function sym_integer_greater_equal = `Sym_ocaml.Num.greater_equal` +declare ocaml target_rep function sym_integer_eq = `Sym_ocaml.Num.equal` + +instance (Ord sym_integer) + let compare = sym_integer_compare + let (<) = sym_integer_less + let (<=) = sym_integer_less_equal + let (>) = sym_integer_greater + let (>=) = sym_integer_greater_equal +end + +instance (SymEq sym_integer) + let sym_eq = sym_integer_eq +end + +(* ======== *) +(* from *) +(* ======== *) + +val symIntegerFromNatural : sym_natural -> sym_integer +declare ocaml target_rep function symIntegerFromNatural x= ``x + +val partialSymNaturalFromInteger : sym_integer -> sym_natural +declare ocaml target_rep function partialSymNaturalFromInteger = `Sym_ocaml.Num.expect_nonneg` + \ No newline at end of file diff --git a/src/sym_ocaml.ml b/src/sym_ocaml.ml new file mode 100644 index 0000000..9b42fe2 --- /dev/null +++ b/src/sym_ocaml.ml @@ -0,0 +1,160 @@ +(* module type Nat_big_num = sig + type num + val zero : num + val succ : num -> num + val pred : num -> num + val pred_nat : num -> num + val negate : num -> num + + val add : num -> num -> num + val sub : num -> num -> num + val sub_nat : num -> num -> num + val div : num -> num -> num + val mul : num -> num -> num + val pow_int : num -> int -> num + val pow_int_positive : int -> int -> num + + + val quomod : num -> num -> num * num + val abs : num -> num + val modulus : num -> num -> num + + val min : num -> num -> num + val max : num -> num -> num + + val less : num -> num -> bool + val greater : num -> num -> bool + val less_equal : num -> num -> bool + val greater_equal : num -> num -> bool + + val compare : num -> num -> int + val equal : num -> num -> bool + + val bitwise_or : num -> num -> num + val bitwise_and : num -> num -> num + val bitwise_xor : num -> num -> num + val shift_left : num -> int -> num + val shift_right : num -> int -> num + + val extract_num : num -> int -> int -> num + + val of_int : int -> num + val of_int32 : Int32.t -> num + val of_int64 : Int64.t -> num + + val to_int : num -> int + val to_int32 : num -> Int32.t + val to_int64 : num -> Int64.t + + val to_string : num -> string + val of_string : string -> num + val of_string_nat : string -> num + val integerDiv_t : num -> num -> num + val integerRem_t : num -> num -> num + val integerRem_f : num -> num -> num +end + +module Make (Nat_big_num : Nat_big_num) = struct *) +(* TODO remove ^ hack for the language server to work *) + + +let fail s = failwith ("Symbolic operation failed: " ^ s) + +(* TODO context? *) +module Num = struct + module NBN = Nat_big_num + + type t = + | Offset of string * NBN.num + | Absolute of NBN.num + + let ppf p = function + | Absolute x -> p x + | Offset (s,x) -> s^"+"^p x + + let to_string = ppf NBN.to_string + + let section s = + if String.starts_with ~prefix:".debug" s then + Absolute NBN.zero + else + Offset (s, NBN.zero) + + let of_num x = Absolute x + + let to_num x = match x with + | Absolute x -> x + | _ -> fail ("to_num " ^ to_string x) + + let add x y = match (x,y) with + | (Absolute x, Absolute y) -> Absolute (NBN.add x y) + | (Offset (s, x), Absolute y) -> Offset (s, NBN.add x y) + | (Absolute x, Offset (s, y)) -> Offset (s, NBN.add x y) + | _ -> fail ("add "^to_string x^" "^to_string y) + + let sub x y = + match (x, y) with + | (Absolute x, Absolute y) -> Absolute (NBN.sub x y) + | (Offset (s, x), Absolute y) -> Offset (s, NBN.sub x y) + | (Offset (s, x'), Offset (t, y')) -> + if s = t then + Absolute (NBN.sub x' y') + else + fail ("sub "^to_string x^" "^to_string y) + | _ -> fail ("sub "^to_string x^" "^to_string y) + + let sub_nat x y = + match (x, y) with + | (Absolute x, Absolute y) -> Absolute (NBN.sub_nat x y) + | (Offset (s, x'), Absolute y') -> + if NBN.greater_equal x' y' then + Offset (s, NBN.sub_nat x' y') + else + fail ("sub_nat "^to_string x^" "^to_string y) + | (Offset (s, x'), Offset (t, y')) -> + if s = t then + Absolute (NBN.sub_nat x' y') + else + fail ("sub_nat "^to_string x^" "^to_string y) + | _ -> fail ("sub_nat "^to_string x^" "^to_string y) + + let map f x = of_num (f(to_num x)) + + let map2 f x y = of_num (f(to_num x)(to_num y)) + + let mul = map2 NBN.mul + let div = map2 NBN.div + + let modulus x y = + let y = to_num y in + match x with + | Absolute x -> Absolute (NBN.modulus x y) + | Offset (s, x) -> Offset (s, NBN.modulus x y) (*Unsafe*) + + let comp f a b = match (a, b) with + | (Absolute a, Absolute b) -> f a b + | (Offset (s, a'), Offset(t, b')) -> if s = t then + f a' b' + else + fail ("comp "^to_string a^" "^to_string b) + | _ -> fail ("comp "^to_string a^" "^to_string b) + + let compare = comp NBN.compare + let less = comp NBN.less + let greater = comp NBN.greater + let less_equal = comp NBN.less_equal + let greater_equal = comp NBN.greater_equal + let equal = comp NBN.equal + + let expect_nonneg x = + let nonneg = match x with + | Absolute x -> NBN.greater_equal x NBN.zero + | Offset (s, x) -> NBN.greater_equal x NBN.zero + in + if nonneg then + x + else + fail (to_string x^" can be negative") +end + +(* end *)