diff --git a/src/analyse/CallGraph.ml b/src/analyse/CallGraph.ml index e90602e1..1a070b26 100644 --- a/src/analyse/CallGraph.ml +++ b/src/analyse/CallGraph.ml @@ -60,7 +60,7 @@ type call_graph_node = addr * index * string list let mk_call_graph test (an : CollectedType.analysis) = let mask_addr x:natural = if !Globals.morello - then Nat_big_num.shift_left (Nat_big_num.shift_right x 1) 1 + then Sym.shift_left (Sym.shift_right x 1) 1 else x in (* take the nodes to be all the elf symbol addresses of stt_func symbol type (each with their list of elf symbol names) together @@ -110,7 +110,7 @@ let mk_call_graph test (an : CollectedType.analysis) = if not (List.exists - (function (a'', _) -> Nat_big_num.equal a' a'') + (function (a'', _) -> Sym.Ordered.equal a' a'') elf_symbols) then Some (a', ["FROM BL:" ^ s']) else None) @@ -122,7 +122,7 @@ let mk_call_graph test (an : CollectedType.analysis) = match axs with | [] -> acc | (a, x) :: axs' -> - if not (List.exists (function (a', _) -> Nat_big_num.equal a a') acc) then + if not (List.exists (function (a', _) -> Sym.Ordered.equal a a') acc) then dedup axs' ((a, x) :: acc) else dedup axs' acc in @@ -133,7 +133,7 @@ let mk_call_graph test (an : CollectedType.analysis) = List.sort (function | (a, _) -> ( - function (a', _) -> Nat_big_num.compare a a' + function (a', _) -> Sym.Ordered.compare a a' )) (elf_symbols @ extra_bl_targets) in diff --git a/src/analyse/ControlFlow.ml b/src/analyse/ControlFlow.ml index 166a80c3..8eefb233 100644 --- a/src/analyse/ControlFlow.ml +++ b/src/analyse/ControlFlow.ml @@ -119,11 +119,11 @@ let branch_table_target_addresses test filename_branch_table_option : (addr * ad with | (a_br, a_table, n, shift, a_offset) -> Some - ( Nat_big_num.of_int a_br, - ( Nat_big_num.of_int a_table, - Nat_big_num.of_int n, + ( Sym.of_int a_br, + ( Sym.of_int a_table, + Sym.of_int n, shift, - Nat_big_num.of_int a_offset ) ) + Sym.of_int a_offset ) ) | exception _ -> fatal "couldn't parse branch table data file line: \"%s\"\n" s in List.filter_map parse_line (List.tl (Array.to_list lines)) @@ -131,49 +131,50 @@ let branch_table_target_addresses test filename_branch_table_option : (addr * ad in (* pull out .rodata section from ELF *) - let ((_, rodata_addr, bs) as _rodata : Dwarf.p_context * Nat_big_num.num * BytesSeq.t) = - Dwarf.extract_section_body test.elf_file ".rodata" false + let ((_, rodata_addr, bs) as _rodata : Dwarf.p_context * Sym.t * BytesSeq.t) = + Dwarf.extract_section_body_without_relocations test.elf_file ".rodata" false in (* chop into bytes *) let rodata_bytes : char array = BytesSeq.to_array bs in (* chop into 4-byte words - as needed for branch offset tables, though not for all other things in .rodata *) - let rodata_words : (natural * natural) list = Dwarf.words_of_byte_sequence rodata_addr bs [] in + let rodata_words : (natural * natural) list = + Dwarf.words_of_sym_byte_sequence rodata_addr (Dwarf_byte_sequence.sym_bs_construct bs (Pmap.empty Nat_big_num.compare)) [] in (*HACK*) let read_rodata_b addr = - Elf_types_native_uint.natural_of_byte - rodata_bytes.(Nat_big_num.to_int (Nat_big_num.sub addr rodata_addr)) + Dwarf.sym_natural_of_byte + rodata_bytes.(Sym.to_int (Sym.sub addr rodata_addr)) in let read_rodata_h addr = - Nat_big_num.add (read_rodata_b addr) - (Nat_big_num.mul (Nat_big_num.of_int 256) - (read_rodata_b (Nat_big_num.add addr (Nat_big_num.of_int 1)))) + Sym.add (read_rodata_b addr) + (Sym.mul (Sym.of_int 256) + (read_rodata_b (Sym.add addr (Sym.of_int 1)))) in let sign_extend_W n = - let half = Nat_big_num.mul (Nat_big_num.of_int 65536) (Nat_big_num.of_int 32768) in - let whole = Nat_big_num.mul half (Nat_big_num.of_int 2) in - if Nat_big_num.greater_equal n half then Nat_big_num.sub n whole else n + let half = Sym.mul (Sym.of_int 65536) (Sym.of_int 32768) in + let whole = Sym.mul half (Sym.of_int 2) in + if Sym.greater_equal n half then Sym.sub n whole else n in let read_rodata_W addr = sign_extend_W - (Nat_big_num.add (read_rodata_b addr) - (Nat_big_num.add - (Nat_big_num.mul (Nat_big_num.of_int 256) - (read_rodata_b (Nat_big_num.add addr (Nat_big_num.of_int 1)))) - (Nat_big_num.add - (Nat_big_num.mul (Nat_big_num.of_int 65536) - (read_rodata_b (Nat_big_num.add addr (Nat_big_num.of_int 2)))) - (Nat_big_num.mul (Nat_big_num.of_int 16777216) - (read_rodata_b (Nat_big_num.add addr (Nat_big_num.of_int 3))))))) + (Sym.add (read_rodata_b addr) + (Sym.add + (Sym.mul (Sym.of_int 256) + (read_rodata_b (Sym.add addr (Sym.of_int 1)))) + (Sym.add + (Sym.mul (Sym.of_int 65536) + (read_rodata_b (Sym.add addr (Sym.of_int 2)))) + (Sym.mul (Sym.of_int 16777216) + (read_rodata_b (Sym.add addr (Sym.of_int 3))))))) in let rec natural_assoc_opt n nys = match nys with | [] -> None - | (n', y) :: nys' -> if Nat_big_num.equal n n' then Some y else natural_assoc_opt n nys' + | (n', y) :: nys' -> if Sym.equal n n' then Some y else natural_assoc_opt n nys' in (* this is the evaluator for a little stack-machine language used in the hafnium.branch-table files to describe the access pattern for each branch table *) @@ -187,8 +188,8 @@ let branch_table_target_addresses test filename_branch_table_option : (addr * ad h read two bytes from the branch table W read four byte from the branch table and sign-extend *) - let rec eval_shift_expression (shift : string) (a_table : Nat_big_num.num) - (a_offset : Nat_big_num.num) (i : Nat_big_num.num) (stack : Nat_big_num.num list) (pc : int) + let rec eval_shift_expression (shift : string) (a_table : Sym.t) + (a_offset : Sym.t) (i : Sym.t) (stack : Sym.t list) (pc : int) = if pc = String.length shift then match stack with @@ -205,8 +206,8 @@ let branch_table_target_addresses test filename_branch_table_option : (addr * ad match stack with | a :: stack' -> let a' = - Nat_big_num.mul a - (Nat_big_num.pow_int_positive 2 (Char.code command - Char.code '0')) + Sym.mul a + (Sym.pow_int_positive 2 (Char.code command - Char.code '0')) in eval_shift_expression shift a_table a_offset i (a' :: stack') (pc + 1) | _ -> fatal "eval_shift_expression shift empty stack" @@ -222,7 +223,7 @@ let branch_table_target_addresses test filename_branch_table_option : (addr * ad (* plus *) match stack with | a1 :: a2 :: stack' -> - let a' = Nat_big_num.add a1 a2 in + let a' = Sym.add a1 a2 in eval_shift_expression shift a_table a_offset i (a' :: stack') (pc + 1) | _ -> fatal "eval_shift_expression plus emptyish stack" else if command = 'b' then @@ -254,24 +255,24 @@ let branch_table_target_addresses test filename_branch_table_option : (addr * ad (function | (a_br, (a_table, size, shift, a_offset)) -> let rec f i = - if i > Nat_big_num.to_int size then [] + if i > Sym.to_int size then [] else let a_target = if shift = "2" then - let table_entry_addr = Nat_big_num.add a_table (Nat_big_num.of_int (4 * i)) in + let table_entry_addr = Sym.add a_table (Sym.of_int (4 * i)) in match natural_assoc_opt table_entry_addr rodata_words with | None -> fatal "no branch table entry for address %s\n" (pp_addr table_entry_addr) | Some table_entry -> let a_target = - Nat_big_num.modulus - (Nat_big_num.add a_table table_entry) - (Nat_big_num.pow_int_positive 2 32) + Sym.modulus + (Sym.add a_table table_entry) + (Sym.pow_int_positive 2 32) in (* that 32 is good for the sign-extended negative 32-bit offsets we see in the old hafnium-playground-src branch tables *) a_target - else eval_shift_expression shift a_table a_offset (Nat_big_num.of_int i) [] 0 + else eval_shift_expression shift a_table a_offset (Sym.of_int i) [] 0 in a_target :: f (i + 1) in @@ -289,14 +290,14 @@ let branch_table_target_addresses test filename_branch_table_option : (addr * ad let parse_addr (s : string) : natural = try - Scanf.sscanf s "0x%Lx" (fun i64 -> Nat_big_num.of_int64 i64) + Scanf.sscanf s "0x%Lx" (fun i64 -> Sym.of_int64 i64) with - Scanf.Scan_failure _ -> - Scanf.sscanf s "%Lx" (fun i64 -> Nat_big_num.of_int64 i64) + (Scanf.Scan_failure _ | End_of_file) -> + Scanf.sscanf s "%Lx" (fun i64 -> Sym.of_int64 i64) -let parse_target s = +let parse_target base s = match Scanf.sscanf s " %s %s" (fun s1 s2 -> (s1, s2)) with - | (s1, s2) -> Some (parse_addr s1, s2) + | (s1, s2) -> Some (Sym.add base (parse_addr s1), s2) | exception _ -> None let parse_drop_one s = @@ -308,7 +309,20 @@ let parse_drop_one s = | (_, s') -> Some s' | exception _ -> None -let parse_control_flow_instruction s mnemonic s' : control_flow_insn = +let parse_relocation_target symbol_map s = + let s, offset = match String.split_on_char '+' s with + | [s1; s2] -> + s1, Scanf.sscanf s2 "0x%x" Fun.id + | [s] -> s, 0 + | _ -> fatal "Unable to parse relocation target '%s'" s + in + let addr = List.find_map (fun (name, (_,_,addr,_,_)) -> if name = s then Some addr else None) symbol_map in + Option.map (Sym.add (Sym.of_int offset)) addr + +let parse_control_flow_instruction symbol_map base s mnemonic s' relocation : control_flow_insn = + let relocation_target = Option.bind relocation (fun (_typ, target) -> + Option.map (fun a -> (a, target)) (parse_relocation_target symbol_map target) + ) in (* Printf.printf "s=\"%s\" mnemonic=\"%s\" mnemonic chars=\"%s\" s'=\"%s\" "s mnemonic (String.concat "," (List.map (function c -> string_of_int (Char.code c)) (char_list_of_string mnemonic))) s';flush stdout;*) let c = if List.mem String.equal mnemonic [".word"] then C_no_instruction @@ -319,9 +333,9 @@ let parse_control_flow_instruction s mnemonic s' : control_flow_insn = (String.length mnemonic >= 2 && String.sub mnemonic 0 2 = "b.") || List.mem String.equal mnemonic ["b"; "bl"] then - match parse_target s' with - | None -> raise (Failure ("b./b/bl parse error for: \"" ^ s ^ "\"\n")) - | Some (a, s) -> + match parse_target base s', relocation_target with + | None, None -> raise (Failure ("b./b/bl parse error for: \"" ^ s ^ "\"\n")) + | _, Some(a, s) | Some (a, s), None -> if mnemonic = "b" then C_branch (a, s) else if mnemonic = "bl" then C_branch_and_link (a, s) else C_branch_cond (mnemonic, a, s) @@ -329,9 +343,9 @@ let parse_control_flow_instruction s mnemonic s' : control_flow_insn = match parse_drop_one s' with | None -> raise (Failure ("cbz/cbnz 1 parse error for: " ^ s ^ "\n")) | Some s' -> ( - match parse_target s' with - | None -> raise (Failure ("cbz/cbnz 2 parse error for: " ^ s ^ "\n")) - | Some (a, s) -> C_branch_cond (mnemonic, a, s) + match parse_target base s', relocation_target with + | None, None -> raise (Failure ("cbz/cbnz 2 parse error for: " ^ s ^ "\n")) + | _, Some(a, s) | Some (a, s), None -> C_branch_cond (mnemonic, a, s) ) else if List.mem String.equal mnemonic ["tbz"; "tbnz"] then match parse_drop_one s' with @@ -340,9 +354,9 @@ let parse_control_flow_instruction s mnemonic s' : control_flow_insn = match parse_drop_one s'' with | None -> raise (Failure ("tbz/tbnz 2 parse error for: " ^ s ^ "\n")) | Some s''' -> ( - match parse_target s''' with - | None -> raise (Failure ("tbz/tbnz 3 parse error for: " ^ s ^ "\n")) - | Some (a, s'''') -> + match parse_target base s''', relocation_target with + | None, None -> raise (Failure ("tbz/tbnz 3 parse error for: " ^ s ^ "\n")) + | _, Some(a, s'''') | Some (a, s''''), None -> (* Printf.printf "s=%s mnemonic=%s s'=%s s''=%s s'''=%s s''''=%s\n"s mnemonic s' s'' s''' s'''';*) C_branch_cond (mnemonic, a, s'''') ) @@ -360,7 +374,7 @@ let parse_control_flow_instruction s mnemonic s' : control_flow_insn = let targets_of_control_flow_insn_without_index branch_table_targets (addr : natural) (opcode_bytes : int list) (c : control_flow_insn) : (target_kind * addr * string) list = - let succ_addr = Nat_big_num.add addr (Nat_big_num.of_int (List.length opcode_bytes)) in + let succ_addr = Sym.add addr (Sym.of_int (List.length opcode_bytes)) in let targets = match c with | C_no_instruction -> [] @@ -437,15 +451,31 @@ AArch64: 10004: 52800129 mov w9, #0x9 // #9 *) +let relocation_regexp_string = "[ \t][0-9a-fA-F]+:[ \t]\\([0-9A-Z_]+\\)\t\\(.*\\)" + let objdump_line_regexp = - Str.regexp " *\\([0-9a-fA-F]+\\):[ \t]\\([0-9a-fA-F ]+\\)\t\\([^ \r\t\n]+\\) *\\(.*\\)$" + Str.regexp (" *\\([0-9a-fA-F]+\\):[ \t]\\([0-9a-fA-F ]+\\)\t\\([^ \r\t\n]+\\)[ \t]*\\([^:]*\\)\\(" ^ relocation_regexp_string ^ "\\)?$") + +let section_start_line_regexp = + Str.regexp "Disassembly of section \\(.*\\):$" + +type relocation = string * string + +type raw_objdump_instruction = + int64 (*address*) * int list (*opcode bytes*) * string (*mnemonic*) * string * relocation option type objdump_instruction = - natural (*address*) * int list (*opcode bytes*) * string (*mnemonic*) * string + natural (*address*) * int list (*opcode bytes*) * string (*mnemonic*) * string * relocation option (*args etc*) -let parse_objdump_line (s : string) : objdump_instruction option = +let parse_section_start s = + if Str.string_match section_start_line_regexp s 0 then + Some (Str.matched_group 1 s) + else + None + +let parse_objdump_line (s : string) : raw_objdump_instruction option = let parse_hex_int64 s' = try Scanf.sscanf s' "%Lx" (fun i64 -> i64) with _ -> fatal "cannot parse address in objdump line %s\n" s @@ -464,8 +494,8 @@ let parse_objdump_line (s : string) : objdump_instruction option = in if Str.string_match objdump_line_regexp s 0 then begin + (* debug "matched line"; *) let addr_int64 = parse_hex_int64 (Str.matched_group 1 s) in - let addr = Nat_big_num.of_int64 addr_int64 in let op = Str.matched_group 2 s in let op = strip_whitespace op in let opcode_byte_strings = @@ -477,39 +507,70 @@ let parse_objdump_line (s : string) : objdump_instruction option = let opcode_bytes = List.map parse_hex_int opcode_byte_strings in let mnemonic = Str.matched_group 3 s in let operands = Str.matched_group 4 s in - Some (addr, opcode_bytes, mnemonic, operands) + let relocation = try + Some (Str.matched_group 6 s, Str.matched_group 7 s) + with + | Not_found -> None + in + Some (addr_int64, opcode_bytes, mnemonic, operands, relocation) end else None +(* let parse_objdump_relocation (s : string) : (string * string) option = + let parse_hex_int s' = + try Scanf.sscanf s' "%x" (fun i -> i) + with _ -> fatal "cannot parse relocation '%s' in objdump line %s\n" s' s + in + if Str.string_match objdump_line_regexp s 0 then + begin + let addr = Str.matched_group 1 s in + let op = Str.matched_group 2 s in + let op = strip_whitespace op in + let opcode_byte_strings = + [String.sub op 0 2; + String.sub op 2 2; + String.sub op 4 2; + String.sub op 6 2] + in + let opcode_bytes = List.map parse_hex_int opcode_byte_strings in + Some (addr, op) + end + else None *) + (* let parse_objdump_lines arch lines : objdump_instruction list = List.filter_map (parse_objdump_line arch) (Array.to_list lines) *) -let rec parse_objdump_lines arch lines (next_index : int) (last_address : natural option) : +let with_symbolic_address (section: string) (addr, opcode_bytes, mnemonic, operands, relocation) : objdump_instruction = + (Sym_ocaml.Num.Offset (section, Nat_big_num.of_int64 addr), opcode_bytes, mnemonic, operands, relocation) + +let rec parse_objdump_lines arch lines (next_index : int) (last_address : int64 option) (section: string option) : objdump_instruction list = if next_index >= Array.length lines then [] else + let section = Option.fold ~none:section ~some:Option.some @@ parse_section_start lines.(next_index) in match parse_objdump_line lines.(next_index) with (* skip over unparseable lines *) - | None -> parse_objdump_lines arch lines (next_index + 1) last_address - | Some ((addr, _opcode_bytes, _mnemonic, _operands) as i) -> ( + | None -> parse_objdump_lines arch lines (next_index + 1) last_address section + | Some ((addr, _opcode_bytes, _mnemonic, _operands, _relocation) as i) -> ( + let mki = with_symbolic_address (Option.get section) in match last_address with - | None -> i :: parse_objdump_lines arch lines (next_index + 1) (Some addr) + | None -> mki i :: parse_objdump_lines arch lines (next_index + 1) (Some addr) section | Some last_address' -> - let last_address'' = Nat_big_num.add last_address' (Nat_big_num.of_int 4) in + let last_address'' = Int64.add last_address' (Int64.of_int 4) in if addr > last_address'' then (* fake up "missing" instructions for any gaps in the address space*) (*warn "gap in objdump instruction address sequence at %s" (pp_addr last_address'');*) - (last_address'', [], "missing", "") - :: parse_objdump_lines arch lines next_index (Some last_address'') - else i :: parse_objdump_lines arch lines (next_index + 1) (Some addr) + mki (last_address'', [], "missing", "", None) + :: parse_objdump_lines arch lines next_index (Some last_address'') section + else mki i :: parse_objdump_lines arch lines (next_index + 1) (Some addr) section ) let parse_objdump_file arch filename_objdump_d : objdump_instruction array = match read_file_lines filename_objdump_d with | Error s -> fatal "%s\ncouldn't read objdump-d file: \"%s\"\n" s filename_objdump_d - | Ok lines -> Array.of_list (parse_objdump_lines arch lines 0 None) + | Ok lines -> Array.of_list (parse_objdump_lines arch lines 0 None None) (*****************************************************************************) (** parse control-flow instruction asm from objdump and branch table data *) @@ -532,7 +593,7 @@ let mk_instructions test filename_objdump_d filename_branch_table_option : Array.iteri (function | k -> ( - function (addr, _, _, _) -> Hashtbl.add tbl addr k + function (addr, _, _, _, _) -> Hashtbl.add tbl addr k )) objdump_instructions; ( (function @@ -549,9 +610,14 @@ let mk_instructions test filename_objdump_d filename_branch_table_option : let instructions = Array.map (function - | (addr, opcode_bytes, mnemonic, operands) -> + | (addr, opcode_bytes, mnemonic, operands, relocation) -> + (* a bit hacky *) + let base = match addr with + | Sym_ocaml.Num.Offset(s,_) -> Sym_ocaml.Num.section s + | Sym_ocaml.Num.Absolute(_) -> Sym.of_int 0 + in let c : control_flow_insn = - parse_control_flow_instruction ("objdump line " ^ pp_addr addr) mnemonic operands + parse_control_flow_instruction test.symbol_map base ("objdump line " ^ pp_addr addr) mnemonic operands relocation in let targets = @@ -565,12 +631,18 @@ let mk_instructions test filename_objdump_d filename_branch_table_option : i_operands = operands; i_control_flow = c; i_targets = targets; + i_relocation = relocation; }) objdump_instructions in let address_of_index k = instructions.(k).i_addr in + Array.sort + (fun i1 i2 -> + Sym.Ordered.compare (i1.i_addr) (i2.i_addr)) + instructions; + (instructions, index_of_address, index_option_of_address, address_of_index) (* pull out indirect branches *) @@ -602,11 +674,11 @@ let highlight c = (* highlight branch targets to earlier addresses*) let pp_target_addr_wrt (addr : natural) (c : control_flow_insn) (a : natural) = - (if highlight c && Nat_big_num.less a addr then "^" else "") ^ pp_addr a + (if highlight c && Sym.Ordered.less a addr then "^" else "") ^ pp_addr a (* highlight branch come-froms from later addresses*) let pp_come_from_addr_wrt (addr : natural) (c : control_flow_insn) (a : natural) = - (if highlight c && Nat_big_num.greater a addr then "v" else "") ^ pp_addr a + (if highlight c && Sym.Ordered.greater a addr then "v" else "") ^ pp_addr a (* let pp_branch_targets (xs : (addr * control_flow_insn * (target_kind * addr * int * string) list) list) diff --git a/src/analyse/ControlFlowPpDot.ml b/src/analyse/ControlFlowPpDot.ml index fc3f90ac..123c0c04 100644 --- a/src/analyse/ControlFlowPpDot.ml +++ b/src/analyse/ControlFlowPpDot.ml @@ -793,7 +793,7 @@ let mk_cfg test an visitedo node_name_prefix (recurse_flat : bool) (_inline_all let ((_comp_dir, _dir, _file) as ufe) = Dwarf.unpack_file_entry lnh lnr.lnr_file in - (ufe, Nat_big_num.to_int lnr.lnr_line)) + (ufe, Sym.to_int lnr.lnr_line)) an.line_info.(k)) in diff --git a/src/analyse/ControlFlowTypes.ml b/src/analyse/ControlFlowTypes.ml index 97815632..4ecb695f 100644 --- a/src/analyse/ControlFlowTypes.ml +++ b/src/analyse/ControlFlowTypes.ml @@ -83,6 +83,7 @@ type instruction = { i_operands : string; i_control_flow : control_flow_insn; i_targets : target list; + i_relocation : (string * string) option; } type come_from = { diff --git a/src/analyse/DwarfFrameInfo.ml b/src/analyse/DwarfFrameInfo.ml index 2b41c478..63da2fc1 100644 --- a/src/analyse/DwarfFrameInfo.ml +++ b/src/analyse/DwarfFrameInfo.ml @@ -53,14 +53,15 @@ open ControlFlowTypes let aof ((a : natural), (_cfa : string), (_regs : (string * string) list)) = a +(* TODO does Sym.Ordered work as we want? *) let rec f (aof : 'b -> natural) (a : natural) (last : 'b option) (bs : 'b list) : 'b option = match (last, bs) with | (None, []) -> None - | (Some b', []) -> if Nat_big_num.greater_equal a (aof b') then Some b' else None + | (Some b', []) -> if Sym.Ordered.greater_equal a (aof b') then Some b' else None | (None, b'' :: bs') -> f aof a (Some b'') bs' | (Some b', b'' :: bs') -> - if Nat_big_num.less a (aof b') then None - else if Nat_big_num.greater_equal a (aof b') && Nat_big_num.less a (aof b'') then Some b' + if Sym.Ordered.less a (aof b') then None + else if Sym.Ordered.greater_equal a (aof b') && Sym.Ordered.less a (aof b'') then Some b' else f aof a (Some b'') bs' let mk_frame_info test instructions : diff --git a/src/analyse/DwarfInliningInfo.ml b/src/analyse/DwarfInliningInfo.ml index bc6a1903..4180e17e 100644 --- a/src/analyse/DwarfInliningInfo.ml +++ b/src/analyse/DwarfInliningInfo.ml @@ -68,7 +68,7 @@ let mk_inlining test sdt instructions = let addr = i.i_addr in let issr_still_current = List.filter - (function (_label, ((_n1, n2), (_m, _n), _is)) -> Nat_big_num.less addr n2) + (function (_label, ((_n1, n2), (_m, _n), _is)) -> Sym.Ordered.less addr n2) issr_current in @@ -83,8 +83,8 @@ let mk_inlining test sdt instructions = let (issr_starting_here0, issr_rest') = find_first - (function ((_n1, n2), (_m, _n), _is) -> Nat_big_num.less_equal n2 addr) - (function ((n1, _n2), (_m, _n), _is) -> Nat_big_num.equal n1 addr) + (function ((_n1, n2), (_m, _n), _is) -> Sym.Ordered.less_equal n2 addr) + (function ((n1, _n2), (_m, _n), _is) -> Sym.Ordered.equal n1 addr) [] issr_rest in diff --git a/src/analyse/DwarfLineInfo.ml b/src/analyse/DwarfLineInfo.ml index cf126a41..2cbf4fef 100644 --- a/src/analyse/DwarfLineInfo.ml +++ b/src/analyse/DwarfLineInfo.ml @@ -86,18 +86,18 @@ type evaluated_line_info_for_instruction = { (* line number sequences can overlap, and we have to walk through instructions (not addresses), so we simplify by splitting all of them into individual entries, sort them by first address, and then walk through them painting a per-instruction array. This is algorithmically a bit terrible, but seems to add only a couple of seconds to read-dwarf rd *) let pp_line_number_header_concise (lnh : Dwarf.line_number_header) : string = - "lnh offset = " ^ Dwarf.pphex lnh.lnh_offset ^ "\n" + "lnh offset = " ^ Dwarf.pphex_sym lnh.lnh_offset ^ "\n" (*^ ("dwarf_format = " ^ (pp_dwarf_format lnh.lnh_dwarf_format ^ ("\n" -^ ("unit_length = " ^ (Nat_big_num.to_string lnh.lnh_unit_length ^ ("\n" -^ ("version = " ^ (Nat_big_num.to_string lnh.lnh_version ^ ("\n" -^ ("header_length = " ^ (Nat_big_num.to_string lnh.lnh_header_length ^ ("\n" -^ ("minimum_instruction_length = " ^ (Nat_big_num.to_string lnh.lnh_minimum_instruction_length ^ ("\n" -^ ("maximum_operations_per_instruction = " ^ (Nat_big_num.to_string lnh.lnh_maximum_operations_per_instruction ^ ("\n" +^ ("unit_length = " ^ (Sym.to_string lnh.lnh_unit_length ^ ("\n" +^ ("version = " ^ (Sym.to_string lnh.lnh_version ^ ("\n" +^ ("header_length = " ^ (Sym.to_string lnh.lnh_header_length ^ ("\n" +^ ("minimum_instruction_length = " ^ (Sym.to_string lnh.lnh_minimum_instruction_length ^ ("\n" +^ ("maximum_operations_per_instruction = " ^ (Sym.to_string lnh.lnh_maximum_operations_per_instruction ^ ("\n" ^ ("default_is_stmt = " ^ (string_of_bool lnh.lnh_default_is_stmt ^ ("\n" -^ ("line_base = " ^ (Nat_big_num.to_string lnh.lnh_line_base ^ ("\n" -^ ("line_range = " ^ (Nat_big_num.to_string lnh.lnh_line_range ^ ("\n" -^ ("opcode_base = " ^ (Nat_big_num.to_string lnh.lnh_opcode_base ^ ("\n" +^ ("line_base = " ^ (Sym.to_string lnh.lnh_line_base ^ ("\n" +^ ("line_range = " ^ (Sym.to_string lnh.lnh_line_range ^ ("\n" +^ ("opcode_base = " ^ (Sym.to_string lnh.lnh_opcode_base ^ ("\n" ^ ("standard_opcode_lengths = " ^ (string_of_list instance_Show_Show_Num_natural_dict lnh.lnh_standard_opcode_lengths ^ ("\n" ^ ("comp_dir = " ^ (string_of_maybe @@ -136,7 +136,8 @@ let split_into_sequences | None -> fatal "split_into_sequences found sequence of length 0" in let last = lnr.lnr_address in - if Nat_big_num.equal first last then fatal "split_into_sequences found first=last" + (* print_endline (Dwarf.pphex_sym first ^ " " ^ Dwarf.pphex_sym last); *) + if Sym.equal first last then fatal "split_into_sequences found first=last" else (); let elis = { @@ -160,8 +161,8 @@ let split_into_entries (s : evaluated_line_info_sequence) : evaluated_line_info_ { elie_first = l1.lnr_address; elie_last = - ( if Nat_big_num.equal l2.lnr_address l1.lnr_address then l1.lnr_address - else Nat_big_num.sub l2.lnr_address (Nat_big_num.of_int 1) + ( if Sym.equal l2.lnr_address l1.lnr_address then l1.lnr_address + else Sym.sub l2.lnr_address (Sym.of_int 1) ); elie_lnh = s.elis_lnh; elie_lnr = l1; @@ -176,9 +177,9 @@ let split_into_entries (s : evaluated_line_info_sequence) : evaluated_line_info_ let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_info_for_instruction option array = let sequences = List.flatten (List.map split_into_sequences eli) in - let compare_sequence s1 s2 = Nat_big_num.compare s1.elis_first s2.elis_first in + let compare_sequence s1 s2 = Sym.compare s1.elis_first s2.elis_first in let sequences_sorted = List.sort compare_sequence sequences in - (*let overlap_sequence s1 s2 = not( Nat_big_num.greater_equal s2.first s1.last || Nat_big_num.greater_equal s1.first s2.last) in*) + (*let overlap_sequence s1 s2 = not( Sym.greater_equal s2.first s1.last || Sym.greater_equal s1.first s2.last) in*) Printf.printf "mk_line_info\n%s" (String.concat "\n" (List.map pp_sequence_concise sequences_sorted)); @@ -189,12 +190,12 @@ let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_ let (discardable,remaining') = List.partition (function sequence -> - Nat_big_num.less_equal sequence.elis_last addr) + Sym.less_equal sequence.elis_last addr) remaining_sequences in let (sequences,remaining'') = List.partition (function sequence -> - Nat_big_num.less_equal sequence.elis_first addr) + Sym.less_equal sequence.elis_first addr) remaining' in (sequences,remaining'') in @@ -224,7 +225,7 @@ let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_ let addr = instructions.(k).i_addr in match remaining_lines with | l1::((l2::remaining_lines') as remaining_lines'') -> - if Nat_big_num.equal addr l1.lnr_address then + if Sym.equal addr l1.lnr_address then (* this instruction address exactly matches the first line of this sequence *) let elifi = { elifi_start = true; @@ -232,7 +233,7 @@ let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_ elifi_line = l1 } in elifis.(k) <- Some elifi; f active_sequence remaining_lines remaining_sequences (k+1) - else if Nat_big_num.less l1.lnr_address addr && Nat_big_num.less addr l2.lnr_address then + else if Sym.less l1.lnr_address addr && Sym.less addr l2.lnr_address then (* this instruction address is within the range of the first line, but not equal to it*) let elifi = { elifi_start = false; @@ -240,7 +241,7 @@ let mk_line_info (eli: Dwarf.evaluated_line_info) instructions : evaluated_line_ elifi_line = l1 } in elifis.(k) <- Some elifi; f active_sequence remaining_lines remaining_sequences (k+1) - else if Nat_big_num.greater_equal addr l2.lnr_address then + else if Sym.greater_equal addr l2.lnr_address then (* this instruction address is after the range of the first line *) if not(l2.lnr_end_sequence (* invariant: iff remaining'=[]*)) then (* there are more non-end lines left in this sequence: try again with the next *) @@ -268,11 +269,11 @@ let mk_line_info (eli : Dwarf.evaluated_line_info) instructions : let elifis = Array.make size [] in let sequences = List.flatten (List.map split_into_sequences eli) in - let compare_sequence s1 s2 = Nat_big_num.compare s1.elis_first s2.elis_first in + let compare_sequence s1 s2 = Sym.Ordered.compare s1.elis_first s2.elis_first in let sequences_sorted = List.sort compare_sequence sequences in let entries = List.flatten (List.map split_into_entries sequences_sorted) in - let compare_entry e1 e2 = Nat_big_num.compare e1.elie_first e2.elie_first in + let compare_entry e1 e2 = Sym.Ordered.compare e1.elie_first e2.elie_first in let entries_sorted = List.sort compare_entry entries in (*List.iter (function elie -> Printf.printf "%s" (pp_elie_concise elie)) entries_sorted;*) @@ -285,7 +286,7 @@ let mk_line_info (eli : Dwarf.evaluated_line_info) instructions : match remaining with | [] -> (acc, remaining) | elie :: remaining' -> - if Nat_big_num.less_equal elie.elie_first addr then + if Sym.Ordered.less_equal elie.elie_first addr then mk_new_perhaps_relevant (elie :: acc) remaining' else (acc, remaining) in @@ -293,7 +294,7 @@ let mk_line_info (eli : Dwarf.evaluated_line_info) instructions : let (new_perhaps_relevant, remaining') = mk_new_perhaps_relevant [] remaining_entries in let addr_in elie = - Nat_big_num.less_equal elie.elie_first addr && Nat_big_num.less_equal addr elie.elie_last + Sym.in_range elie.elie_first elie.elie_last addr in let still_active_entries = @@ -305,7 +306,7 @@ let mk_line_info (eli : Dwarf.evaluated_line_info) instructions : (function | elie -> let elifi = - { elifi_start = Nat_big_num.equal addr elie.elie_first; elifi_entry = elie } + { elifi_start = Sym.equal addr elie.elie_first; elifi_entry = elie } in elifi) still_active_entries; @@ -443,14 +444,14 @@ let pp_dwarf_source_file_lines' m (ds : Dwarf.dwarf_static) (pp_actual_line : bo | Ascii -> s | Html -> "@" ^ s ^ "@ " in wrap_link m (subprogram_name ^ ":" - ^ Nat_big_num.to_string lnr.lnr_line + ^ Sym.to_string lnr.lnr_line ^ "." - ^ Nat_big_num.to_string lnr.lnr_column + ^ Sym.to_string lnr.lnr_column ^ " (" ^ file ^ ")" ) (* ^ (if elifi.elifi_start then "S" else "s")*) @@ -463,10 +464,10 @@ let pp_dwarf_source_file_lines' m (ds : Dwarf.dwarf_static) (pp_actual_line : bo ^ " " ^ if pp_actual_line then - let line = Nat_big_num.to_int lnr.lnr_line in + let line = Sym.to_int lnr.lnr_line in if line = 0 then "line 0" else - pp_source_line (source_line (comp_dir, dir, file) line) (Nat_big_num.to_int lnr.lnr_column) + pp_source_line (source_line (comp_dir, dir, file) line) (Sym.to_int lnr.lnr_column) else "" (* OLD source line number for O0/2 correlation @@ -479,11 +480,11 @@ let rec dwarf_source_file_line_numbers' test recursion_limit (a : natural) : match sls with | [] -> dwarf_source_file_line_numbers' test (recursion_limit - 1) - (Nat_big_num.sub a (Nat_big_num.of_int 4)) + (Sym.sub a (Sym.of_int 4)) | _ -> List.map (fun ((comp_dir, dir, file), n, lnr, subprogram_name) -> - (subprogram_name, Nat_big_num.to_int n)) + (subprogram_name, Sym.to_int n)) sls let dwarf_source_file_line_numbers test (a : natural) = @@ -507,7 +508,7 @@ let dwarf_source_file_line_numbers_by_index test line_info k : Dwarf.subprogram_at_line test.dwarf_static.ds_subprogram_line_extents ufe lnr.lnr_line ) in - (subprogram_name, Nat_big_num.to_int lnr.lnr_line)) + (subprogram_name, Sym.to_int lnr.lnr_line)) elifis) in match lines with [_] -> lines | [] -> lines | _ -> [] diff --git a/src/analyse/DwarfVarInfo.ml b/src/analyse/DwarfVarInfo.ml index bd0709f0..8e1ffbec 100644 --- a/src/analyse/DwarfVarInfo.ml +++ b/src/analyse/DwarfVarInfo.ml @@ -76,7 +76,7 @@ let pp_sdt_concise_variable_or_formal_parameter_main (level : int) ^ (match svfp.svfp_type with None -> "none" | Some t -> Dwarf.pp_type_info_deep t) ^ " " (*^ indent ^ "const_value:"*) - ^ (match svfp.svfp_const_value with None -> "" | Some v -> "const:" ^ Nat_big_num.to_string v) + ^ (match svfp.svfp_const_value with None -> "" | Some v -> "const:" ^ Sym.to_string v) ^ " " (*^ indent ^ "external:" ^ show svfp.svfp_external ^ "\n"*) @@ -90,7 +90,7 @@ let pp_sdt_concise_variable_or_formal_parameter (level : int) (is_params : bool) ^ match svfp.svfp_locations with | None -> "no locations\n" - | Some [loc] -> " " ^ Dwarf.pp_parsed_single_location_description (Nat_big_num.of_int 0) loc + | Some [loc] -> " " ^ Dwarf.pp_parsed_single_location_description (Z.of_int 0) loc | Some locs -> "\n" ^ String.concat "" @@ -99,7 +99,7 @@ let pp_sdt_concise_variable_or_formal_parameter (level : int) (is_params : bool) | loc -> "+" ^ Dwarf.pp_parsed_single_location_description - (Nat_big_num.of_int (level + 1)) + (Z.of_int (level + 1)) loc) locs) @@ -150,14 +150,14 @@ let rec locals_subroutine context (ss : Dwarf.sdt_subroutine) = ^ (indent (*^ "name:" ^*) ^ (pp_sdt_maybe ss.ss_name (fun name1 -> name1 ^ "\n") (* ^ indent ^ "cupdie:" ^ pp_cupdie3 ss.ss_cupdie ^ "\n"*) ^ (indent ^ ("kind:" ^ (((match ss.ss_kind with SSK_subprogram -> "subprogram" | SSK_inlined_subroutine -> "inlined subroutine" )) ^ ("\n" - ^ (indent ^ ("call site:" ^ (pp_sdt_maybe ss.ss_call_site (fun ud -> "\n" ^ (indent_level true (Nat_big_num.add level(Nat_big_num.of_int 1)) ^ (pp_ud ud ^ "\n"))) - ^ (indent ^ ("abstract origin:" ^ (pp_sdt_maybe ss.ss_abstract_origin (fun s -> "\n" ^ locals__subroutine (Nat_big_num.add level(Nat_big_num.of_int 1)) s) + ^ (indent ^ ("call site:" ^ (pp_sdt_maybe ss.ss_call_site (fun ud -> "\n" ^ (indent_level true (Sym.add level(Sym.of_int 1)) ^ (pp_ud ud ^ "\n"))) + ^ (indent ^ ("abstract origin:" ^ (pp_sdt_maybe ss.ss_abstract_origin (fun s -> "\n" ^ locals__subroutine (Sym.add level(Sym.of_int 1)) s) (* ^ indent ^ "type:" ^ pp_sdt_maybe ss.ss_type (fun typ -> pp_type_info_deep typ ^"\n" end)*) - ^ (indent ^ ("vars:" ^ (pp_sdt_list ss.ss_vars (pp_sdt_concise_variable_or_formal_parameter (Nat_big_num.add level(Nat_big_num.of_int 1))) - ^ (indent ^ ("unspecified_parameters:" ^ (pp_sdt_list ss.ss_unspecified_parameters (pp_sdt_unspecified_parameter (Nat_big_num.add level(Nat_big_num.of_int 1))) + ^ (indent ^ ("vars:" ^ (pp_sdt_list ss.ss_vars (pp_sdt_concise_variable_or_formal_parameter (Sym.add level(Sym.of_int 1))) + ^ (indent ^ ("unspecified_parameters:" ^ (pp_sdt_list ss.ss_unspecified_parameters (pp_sdt_unspecified_parameter (Sym.add level(Sym.of_int 1))) (* ^ indent ^ "pc ranges:" ^ pp_pc_ranges (level+1) ss.ss_pc_ranges*) - ^ (indent ^ ("subroutines:" ^ (pp_sdt_list ss.ss_subroutines (locals__subroutine (Nat_big_num.add level(Nat_big_num.of_int 1))) - ^ (indent ^ ("lexical_blocks:" ^ (pp_sdt_list ss.ss_lexical_blocks (locals__lexical_block (Nat_big_num.add level(Nat_big_num.of_int 1))) + ^ (indent ^ ("subroutines:" ^ (pp_sdt_list ss.ss_subroutines (locals__subroutine (Sym.add level(Sym.of_int 1))) + ^ (indent ^ ("lexical_blocks:" ^ (pp_sdt_list ss.ss_lexical_blocks (locals__lexical_block (Sym.add level(Sym.of_int 1))) (* ^ indent ^ "decl:" ^ pp_sdt_maybe ss.ss_decl (fun ((ufe,line) as ud) -> "\n" ^ indent_level true (level+1) ^ pp_ufe ufe ^ " " ^ show line ^ "\n" end)*) (* ^ indent ^ "noreturn:" ^ show ss.ss_noreturn ^ "\n"*) (* ^ indent ^ "external:" ^ show ss.ss_external ^"\n"*) @@ -172,10 +172,10 @@ and locals_lexical_block context (lb : Dwarf.sdt_lexical_block) = (* "" (* ^ indent ^ "cupdie:" ^ pp_cupdie3 lb.slb_cupdie ^ "\n"*) - ^ (indent ^ ("vars:" ^ (pp_sdt_list lb.slb_vars (pp_sdt_concise_variable_or_formal_parameter (Nat_big_num.add level(Nat_big_num.of_int 1))) + ^ (indent ^ ("vars:" ^ (pp_sdt_list lb.slb_vars (pp_sdt_concise_variable_or_formal_parameter (Sym.add level(Sym.of_int 1))) (* ^ indent ^ "pc ranges:" ^ pp_pc_ranges (level+1) lb.slb_pc_ranges*) - ^ (indent ^ ("subroutines :" ^ (pp_sdt_list lb.slb_subroutines (locals__subroutine (Nat_big_num.add level(Nat_big_num.of_int 1))) - ^ (indent ^ ("lexical_blocks:" ^ (pp_sdt_list lb.slb_lexical_blocks (locals__lexical_block (Nat_big_num.add level(Nat_big_num.of_int 1))) + ^ (indent ^ ("subroutines :" ^ (pp_sdt_list lb.slb_subroutines (locals__subroutine (Sym.add level(Sym.of_int 1))) + ^ (indent ^ ("lexical_blocks:" ^ (pp_sdt_list lb.slb_lexical_blocks (locals__lexical_block (Sym.add level(Sym.of_int 1))) ^ "\n")))))))))) *) @@ -190,8 +190,8 @@ let locals_compilation_unit context (cu : Dwarf.sdt_compilation_unit) = "" ^ (indent (*^ "name:" *) ^ (cu.scu_name ^ ("\n" (* ^ indent ^ "cupdie:" ^ pp_cupdie3 cu.scu_cupdie ^ "\n"*) - ^ (indent ^ ("vars:" ^ (pp_sdt_list cu.scu_vars (pp_sdt_concise_variable_or_formal_parameter (Nat_big_num.add level(Nat_big_num.of_int 1))) - ^ (indent ^ ("subroutines :" ^ pp_sdt_list cu.scu_subroutines (locals__subroutine (Nat_big_num.add level(Nat_big_num.of_int 1)))))))))))) + ^ (indent ^ ("vars:" ^ (pp_sdt_list cu.scu_vars (pp_sdt_concise_variable_or_formal_parameter (Sym.add level(Sym.of_int 1))) + ^ (indent ^ ("subroutines :" ^ pp_sdt_list cu.scu_subroutines (locals__subroutine (Sym.add level(Sym.of_int 1)))))))))))) *) let locals_dwarf (sdt_d : Dwarf.sdt_dwarf) : (Dwarf.sdt_variable_or_formal_parameter * string list) (*context*) list = @@ -260,7 +260,7 @@ let pp_ranged_var (prefix : string) (var : ranged_var) : string = let pp_ranged_vars (prefix : string) (vars : ranged_var list) : string = String.concat "" (List.map (pp_ranged_var prefix) vars) -let compare_pc_ranges ((n1, _, _), _) ((n1', _, _), _) = compare n1 n1' +let compare_pc_ranges ((n1, _, _), _) ((n1', _, _), _) = Sym.Ordered.compare n1 n1' let local_by_pc_ranges (((svfp : Dwarf.sdt_variable_or_formal_parameter), _context) as var) : ranged_var list = @@ -299,14 +299,14 @@ let mk_ranged_vars_at_instructions (sdt_d : Dwarf.sdt_dwarf) instructions : if k >= size then () else let addr = instructions.(k).i_addr in - if not (Nat_big_num.less addr_prev addr) then + if not (Sym.Ordered.less addr_prev addr) then fatal "mk_ranged_vars_at_instructions found non-increasing address %s" (pp_addr addr); let (still_current, old) = - List.partition (function ((_, n2, _), _) -> Nat_big_num.less addr n2) prev + List.partition (function ((_, n2, _), _) -> Sym.Ordered.less addr n2) prev in let (new', remaining') = partition_first - (function ((n1, _n2, _ops), _var) as _rv -> Nat_big_num.greater_equal addr n1) + (function ((n1, _n2, _ops), _var) as _rv -> Sym.Ordered.greater_equal addr n1) remaining in (* TODO: do we need to drop any that have been totally skipped over? *) @@ -317,7 +317,7 @@ let mk_ranged_vars_at_instructions (sdt_d : Dwarf.sdt_dwarf) instructions : rvai_remaining.(k) <- remaining'; f addr current remaining' (k + 1) in - f (Nat_big_num.of_int (0 - 1)) [] locals_by_pc_ranges 0; + f (Sym.of_int (0 - 1)) [] locals_by_pc_ranges 0; { rvai_globals = globals_dwarf sdt_d; diff --git a/src/analyse/Elf.ml b/src/analyse/Elf.ml index 0be22494..574664ca 100644 --- a/src/analyse/Elf.ml +++ b/src/analyse/Elf.ml @@ -58,8 +58,8 @@ let pp_symbol_map (symbol_map : Elf_file.global_symbol_init_info) = String.concat "" (List.map (fun (name, (typ, _size, address, _mb, _binding)) -> - Printf.sprintf "**** name = %s address = %s typ = %d\n" name (pp_addr address) - (Nat_big_num.to_int typ)) + Printf.sprintf "**** name = %s address = %s typ = %d\n" name (pp_addr (Sym_ocaml.Num.Absolute address)) + (Sym.to_int (Sym_ocaml.Num.Absolute typ))) symbol_map) (*****************************************************************************) @@ -69,20 +69,23 @@ let pp_symbol_map (symbol_map : Elf_file.global_symbol_init_info) = let parse_elf_file (filename : string) : test = (* call ELF analyser on file *) - let info = Sail_interface.populate_and_obtain_global_symbol_init_info filename in - - let ( (elf_file : Elf_file.elf_file), - (elf_epi : Sail_interface.executable_process_image), - (symbol_map : Elf_file.global_symbol_init_info) ) = - match info with - | Error.Fail s -> fatal "populate_and_obtain_global_symbol_init_info: %s" s + let bs = match Byte_sequence.acquire filename with + | Error.Fail s -> fatal "Linksem: Byte_sequence.acquire: %s" s | Error.Success x -> x in - - let f64 = - match elf_file with Elf_file.ELF_File_64 f -> f | _ -> raise (Failure "not Elf64") + let f64 = match Elf_file.read_elf64_file bs with + | Error.Fail s -> fatal "Linksem: read_elf64_file: %s" s + | Error.Success x -> x in + let symbol_map = match Symbols.get_elf64_file_global_symbol_init f64 with + | Error.Fail s -> fatal "LinksemRelocatable: get_elf64_file_global_symbol_init: %s" s + | Error.Success x -> x + in + + let elf_file = Elf_file.ELF_File_64 f64 in + let entry = f64.elf64_file_header.elf64_entry in + let machine = f64.elf64_file_header.elf64_machine in (* linksem main_elf --symbols looks ok for gcc and clang That uses Elf_file.read_elf64_file bs0 >>= fun f1 -> @@ -125,49 +128,38 @@ let parse_elf_file (filename : string) : test = *) (* Debug.print_string "elf segments etc\n";*) - match (elf_epi, elf_file) with - | (Sail_interface.ELF_Class_32 _, _) -> fatal "%s" "cannot handle ELF_Class_32" - | (_, Elf_file.ELF_File_32 _) -> fatal "%s" "cannot handle ELF_File_32" - | (Sail_interface.ELF_Class_64 (segments, e_entry, e_machine), Elf_file.ELF_File_64 f1) -> - (* architectures from linksem elf_header.lem *) - let arch = - if f64.elf64_file_header.elf64_machine = Elf_header.elf_ma_aarch64 then AArch64 - else if f64.elf64_file_header.elf64_machine = Elf_header.elf_ma_x86_64 then X86 - else fatal "unrecognised ELF file architecture" - in - - (* remove all the auto generated segments (they contain only 0s) *) - let segments = - Lem_list.mapMaybe - (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None) - segments - in - let ds = - match Dwarf.extract_dwarf_static (Elf_file.ELF_File_64 f1) with - | None -> fatal "%s" "extract_dwarf_static failed" - | Some ds -> - (* Debug.print_string2 (Dwarf.pp_analysed_location_data ds.Dwarf.ds_dwarf - ds.Dwarf.ds_analysed_location_data); - Debug.print_string2 (Dwarf.pp_evaluated_frame_info - ds.Dwarf.ds_evaluated_frame_info);*) - ds - in - let dwarf_semi_pp_frame_info = - Dwarf.semi_pp_evaluated_frame_info ds.ds_evaluated_frame_info - in - let test = - { - elf_file; - arch; - symbol_map (*@ (symbols_for_stacks !Globals.elf_threads)*); - segments; - e_entry; - e_machine; - dwarf_static = ds; - dwarf_semi_pp_frame_info; - } - in - test + (* architectures from linksem elf_header.lem *) + let arch = + if f64.elf64_file_header.elf64_machine = Elf_header.elf_ma_aarch64 then AArch64 + else if f64.elf64_file_header.elf64_machine = Elf_header.elf_ma_x86_64 then X86 + else fatal "unrecognised ELF file architecture" + in + + let ds = + match Dwarf.extract_dwarf_static (Elf_file.ELF_File_64 f64) Abi_aarch64_symbolic_relocation.aarch64_data_relocation_interpreter with + | None -> fatal "%s" "extract_dwarf_static failed" + | Some ds -> + (* Debug.print_string2 (Dwarf.pp_analysed_location_data ds.Dwarf.ds_dwarf + ds.Dwarf.ds_analysed_location_data); + Debug.print_string2 (Dwarf.pp_evaluated_frame_info + ds.Dwarf.ds_evaluated_frame_info);*) + ds + in + let dwarf_semi_pp_frame_info = + Dwarf.semi_pp_evaluated_frame_info ds.ds_evaluated_frame_info + in + let test = + { + elf_file; + arch; + symbol_map (*@ (symbols_for_stacks !Globals.elf_threads)*); + e_entry = Sym_ocaml.Num.Absolute (entry); + e_machine = Sym_ocaml.Num.Absolute (machine); + dwarf_static = ds; + dwarf_semi_pp_frame_info; + } + in + test (*****************************************************************************) (** marshal and unmarshal test *) diff --git a/src/analyse/ElfTypes.ml b/src/analyse/ElfTypes.ml index a0795eb0..005a7ba6 100644 --- a/src/analyse/ElfTypes.ml +++ b/src/analyse/ElfTypes.ml @@ -62,8 +62,7 @@ type architecture = type test = { elf_file : Elf_file.elf_file; arch : architecture; - symbol_map : Elf_file.global_symbol_init_info; - segments : Elf_interpreted_segment.elf64_interpreted_segment list; + symbol_map : Symbols.global_symbol_init_info; e_entry : natural; e_machine : natural; dwarf_static : Dwarf.dwarf_static; diff --git a/src/analyse/Pp.ml b/src/analyse/Pp.ml index d9c749c3..cc57b5f6 100644 --- a/src/analyse/Pp.ml +++ b/src/analyse/Pp.ml @@ -74,6 +74,7 @@ type render_kind = | Render_vars_old | Render_inlining | Render_ctrlflow + | Render_relocation let render_colour = function | Render_symbol_star -> "gold" @@ -86,6 +87,7 @@ let render_colour = function | Render_vars_old -> "grey" | Render_inlining -> "red" | Render_ctrlflow -> "white" + | Render_relocation -> "purple" let render_class_name = function | Render_symbol_star -> "symbol-star" @@ -98,6 +100,7 @@ let render_class_name = function | Render_vars_old -> "vars-old" | Render_inlining -> "inlining" | Render_ctrlflow -> "ctrlflow" + | Render_relocation -> "relocation" type html_idiom = HI_span | HI_pre | HI_classless_span | HI_font @@ -327,13 +330,20 @@ let pp_instruction m test an rendered_control_flow_common_prefix_end k i = (ControlFlowPpText.pp_glyphs rendered_control_flow_common_prefix_end an.rendered_control_flow.(k)) (* the address and (hex) instruction *) - ^ css m Render_instruction - (pp_addr addr ^ ": " + ^ css m Render_instruction ( + pp_addr addr ^ ": " ^ pp_opcode_bytes test.arch i.i_opcode (* the dissassembly from objdump *) ^ " " ^ i.i_mnemonic ^ "\t" ^ i.i_operands ) + ^ css m Render_relocation + (match i.i_relocation with + | None -> "" + | Some (typ, targ) -> + "\t" ^ typ ^ " " ^ targ + ) + (* the instruction's control flow *) (* any indirect-branch control flow from this instruction *) ^ css m Render_ctrlflow (begin @@ -574,7 +584,7 @@ let pp_instructions_ranged m test an (low, high) = Printf.printf "pp_instructions_ranged indices: low=%i high=%i \n" (an.index_of_address low) (an.index_of_address high); *) let index_low = an.index_of_address low in - let index_high = (an.index_of_address (Nat_big_num.sub high (Nat_big_num.of_int 4)))+1 in + let index_high = (an.index_of_address (Sym.sub high (Sym.of_int 4)))+1 in let rec subarray_map_to_list f a k k' = if k >= k' then [] else f k a.(k) :: subarray_map_to_list f a (k + 1) k' in @@ -857,7 +867,6 @@ let pp_test_analysis m test an = call_graph ^ "* ************* transitive call graph **************\n" ^ transitive_call_graph | Html -> - "" - (* "\n* ************* instructions *****************\n" *) - (*pp_instruction_init (); - String.concat "" (Array.to_list (Array.mapi (pp_instruction m test an 0) an.instructions))*) + "\n* ************* instructions *****************\n" + ^ (pp_instruction_init (); + String.concat "" (Array.to_list (Array.mapi (pp_instruction m test an 0) an.instructions))) diff --git a/src/analyse/QemuLog.ml b/src/analyse/QemuLog.ml index 9591bef5..e25a65c0 100644 --- a/src/analyse/QemuLog.ml +++ b/src/analyse/QemuLog.ml @@ -64,8 +64,8 @@ let read_qemu_log an filename_qemu_log : bool array = (* Printf.printf "%s " s;*) match Scanf.sscanf s "0x%x:%s" (fun addr _ -> addr) with | addr -> - (*Printf.printf "PARSED %s\n" (pp_addr (Nat_big_num.of_int addr));*) - Some (Nat_big_num.of_int addr) + (*Printf.printf "PARSED %s\n" (pp_addr (Sym.of_int addr));*) + Some (Sym.of_int addr) | exception _ -> (*Printf.printf "NOT\n";*) None in List.filter_map parse_line (Array.to_list lines) diff --git a/src/analyse/Symbols.ml b/src/analyse/Symbols.ml new file mode 100644 index 00000000..d555ae9f --- /dev/null +++ b/src/analyse/Symbols.ml @@ -0,0 +1,77 @@ +(* TODO header *) + +open Logs.Logger (struct + let str = __MODULE__ +end) + +module SMap = Map.Make (String) + +type rels = + | AArch64 of (Z.t, Abi_aarch64_symbolic_relocation.aarch64_relocation_target Elf_symbolic.universal_relocation) Pmap.map + +type sym_data = +Byte_sequence_wrapper.byte_sequence * rels + + +(* Like in linksem, but address is section+offset, data has relocations and with a writable flag *) +type symbol = string * (Z.t * Z.t * Sym.t * sym_data * Z.t) + +type global_symbol_init_info = symbol list + +open Elf_symbol_table +open Elf_interpreted_section + +let get_elf64_file_global_symbol_init (f: Elf_file.elf64_file) : global_symbol_init_info Error.error = + let secs = f.elf64_file_interpreted_sections in + let machine = f.elf64_file_header.elf64_machine in + Error.bind (Elf_file.get_elf64_file_symbol_table f) @@ fun (symtab, strtab) -> + let rel_cache = ref SMap.empty in + let get_relocs section = + match SMap.find_opt section !rel_cache with + | Some rels -> Error.return rels + | None -> + if machine = Elf_header.elf_ma_aarch64 then + Error.bind + (Elf_symbolic.extract_elf64_relocations_for_section f Abi_aarch64_symbolic_relocation.aarch64_relocation_interpreter section) + @@ fun relocs -> + rel_cache := SMap.add section (AArch64 relocs) !rel_cache; + Error.return (AArch64 relocs) + else + Error.fail @@ "machine not supported " ^ (Elf_header.string_of_elf_machine_architecture machine) + in + List.filter_map ( + fun entry -> + let name = Uint32_wrapper.to_bigint entry.elf64_st_name in + let addr_offset = Uint64_wrapper.to_bigint entry.elf64_st_value in + let size = Uint64_wrapper.to_bigint entry.elf64_st_size in + let shndx = Uint32_wrapper.to_int entry.elf64_st_shndx in + let typ = Elf_symbol_table.extract_symbol_type entry.elf64_st_info in + let bnd = Elf_symbol_table.extract_symbol_binding entry.elf64_st_info in + Option.map ( + fun section -> + let addr = Sym_ocaml.Num.Offset (section.elf64_section_name_as_string, addr_offset) in + let data = if Byte_sequence.length0 section.elf64_section_body = Z.zero then + Error.return (Byte_sequence.zeros size) + else + Byte_sequence.offset_and_cut addr_offset size section.elf64_section_body + in + Error.bind (get_relocs section.elf64_section_name_as_string) @@ fun (AArch64 relocs) -> + let relocs = relocs + |> Pmap.bindings_list + |> List.fold_left (fun m (pos, r) -> + let sz = size in + let open Z in + let open Compare in + if pos >= addr_offset && pos < addr_offset + sz then + Pmap.add (pos - addr_offset) r m + else + m + ) (Pmap.empty Z.compare) + |> fun x -> AArch64 x + in + Error.bind data @@ fun data -> + Error.bind (String_table.get_string_at name strtab) @@ fun str -> + debug "Processed %s\n" str; + Error.return (str, (typ, size, addr, (data, relocs), bnd)) + ) (List.nth_opt secs shndx) + ) symtab |> Error.mapM Fun.id \ No newline at end of file diff --git a/src/analyse/Utils.ml b/src/analyse/Utils.ml index cf316505..5d79072b 100644 --- a/src/analyse/Utils.ml +++ b/src/analyse/Utils.ml @@ -49,13 +49,18 @@ open Logs.Logger (struct end) (** TODO: Maybe just use Z.t everywhere (it's shorter) *) -type natural = Nat_big_num.num +type natural = Sym.t (** machine address *) type addr = natural (* hackishly mask out bigint conversion failure *) -let pp_addr (a : natural) = try Ml_bindings.hex_string_of_big_int_pad8 a with Failure s -> let s' = "Failure: int64_of_big_int " ^ Nat_big_num.to_string a in (warn "pp_addr failure: %s" s); s'| e -> raise e +let pp_addr (a : natural) = + try + Sym_ocaml.Num.ppf Ml_bindings.hex_string_of_big_int_pad8 a + with + | Failure s -> let s' = "Failure: int64_of_big_int " ^ Sym.to_string a in (warn "pp_addr failure: %s" s); s' + | e -> raise e (** index into instruction-indexed arrays *) type index = int diff --git a/src/analyse/html-preamble-insts.html b/src/analyse/html-preamble-insts.html index 36645dfd..3b8adb8b 100644 --- a/src/analyse/html-preamble-insts.html +++ b/src/analyse/html-preamble-insts.html @@ -81,6 +81,9 @@ .ctrlflow { color: white; } + .relocation { + color: mediumpurple; + } a:link { color: aqua; background-color: transparent; diff --git a/src/arch/aarch64/sig.ml b/src/arch/aarch64/sig.ml index 18b0b18c..c46bb8b8 100644 --- a/src/arch/aarch64/sig.ml +++ b/src/arch/aarch64/sig.ml @@ -331,7 +331,7 @@ let get_abi api = State.set_reg_type state sp (Ctype.of_frag ~provenance:stack_provenance @@ DynFragment stack_frag_id); State.set_reg state r30 - (State.Tval.of_var ~ctyp:(Ctype.of_frag_somewhere Ctype.Global) RetAddr); + (State.Tval.of_var ~ctyp:(Ctype.of_frag_somewhere (Ctype.Global ".text")) RetAddr); (* TODO doesn't have to be .text *) let sp_exp = State.Exp.of_reg state.id sp in (* Assert that Sp is 16 bytes aligned *) State.push_assert state Exp.Typed.(extract ~last:3 ~first:0 sp_exp = bits_int ~size:4 0); @@ -360,7 +360,19 @@ let assemble_to_elf instr = Sys.remove obj_file; elf_file -let split_into_instrs = BytesSeq.to_listbs ~len:4 +let split_into_instrs (data: Elf.Symbol.data) = + let module IMap = Elf.Relocations.IMap in + let rawdata = BytesSeq.to_listbs ~len:4 data.data in + List.mapi (fun i bytes -> + let pos = 4 * i in + let (_, rel, rest) = IMap.split pos data.relocations in + if Option.is_some @@ IMap.find_first_opt (fun i -> i < pos + 4) rest then + Raise.fail "Misaligned relocation"; + Elf.Symbol.{ + data = bytes; + relocations = rel |> Option.map (IMap.singleton 0) |> Option.value ~default:IMap.empty; + } + ) rawdata (** https://developer.arm.com/documentation/ddi0596/2020-12/Base-Instructions/RET--Return-from-subroutine- *) let is_ret code = diff --git a/src/arch/riscv64/sig.ml b/src/arch/riscv64/sig.ml index 0e14e523..4f661598 100644 --- a/src/arch/riscv64/sig.ml +++ b/src/arch/riscv64/sig.ml @@ -289,7 +289,7 @@ let get_abi api = State.set_reg_type state sp (Ctype.of_frag ~provenance:stack_provenance @@ DynFragment stack_frag_id); State.set_reg state ra - (State.Tval.of_var ~ctyp:(Ctype.of_frag_somewhere Ctype.Global) RetAddr); + (State.Tval.of_var ~ctyp:(Ctype.of_frag_somewhere (Ctype.Global ".text")) RetAddr); let sp_exp = State.Exp.of_reg state.id sp in (* Assert that Sp is 16 bytes aligned *) State.push_assert state Exp.Typed.(extract ~last:3 ~first:0 sp_exp = bits_int ~size:4 0); @@ -317,7 +317,18 @@ let assemble_to_elf instr = Sys.remove obj_file; elf_file -let split_into_instrs = BytesSeq.to_listbs ~len:4 +let split_into_instrs (data: Elf.Symbol.data) = + let module IMap = Elf.Relocations.IMap in + let rawdata = BytesSeq.to_listbs ~len:4 data.data in + List.mapi (fun pos bytes -> + let (_, rel, rest) = IMap.split pos data.relocations in + if Option.is_some @@ IMap.find_first_opt (fun i -> i < pos + 4) rest then + Raise.fail "Misaligned relocation"; + Elf.Symbol.{ + data = bytes; + relocations = rel |> Option.map (IMap.singleton 0) |> Option.value ~default:IMap.empty; + } + ) rawdata let is_ret code = assert (BytesSeq.length code = 4); diff --git a/src/arch/sig.mli b/src/arch/sig.mli index 13268696..a355e3e6 100644 --- a/src/arch/sig.mli +++ b/src/arch/sig.mli @@ -109,7 +109,7 @@ val sp : unit -> State.Reg.t val assemble_to_elf : string -> string (** Split a byte-sequence into a list of instructions. *) -val split_into_instrs : BytesSeq.t -> BytesSeq.t list +val split_into_instrs : Elf.Symbol.data -> Elf.Symbol.data list (** Tell if an instruction is a return instruction. *) val is_ret : BytesSeq.t -> bool diff --git a/src/ast/manip.ml b/src/ast/manip.ml index 46a7ce9c..b21dffe7 100644 --- a/src/ast/manip.ml +++ b/src/ast/manip.ml @@ -350,3 +350,10 @@ let check_no_mem (e : ('a, 'v, 'b, 'm) exp) : bool = let expect_no_mem ?(handler = fun () -> failwith "Expected no mem") : ('a, 'v, 'b, 'm1) exp -> ('a, 'v, 'b, 'm2) exp = fun exp -> if check_no_mem exp then Obj.magic exp else handler () + + +let all_subterms e = + let rec recurse acc e = + e :: direct_exp_fold_left_exp recurse acc e + in + direct_exp_fold_left_exp recurse [] e \ No newline at end of file diff --git a/src/bin/copySources.ml b/src/bin/copySources.ml index d664698c..ed6def6f 100644 --- a/src/bin/copySources.ml +++ b/src/bin/copySources.ml @@ -79,13 +79,13 @@ let process_file () : unit = (function | lnfe -> ( lnh.lnh_comp_dir, - (let dir = Nat_big_num.to_int lnfe.lnfe_directory_index in + (let dir = Sym.to_int lnfe.lnfe_directory_index in if dir = 0 then None else Some (Byte_sequence.string_of_byte_sequence - (List.nth lnh.lnh_include_directories (dir - 1)))), - Byte_sequence.string_of_byte_sequence lnfe.lnfe_path )) + (Dwarf_byte_sequence.sym_bs_expect_const (List.nth lnh.lnh_include_directories (dir - 1))))), + Byte_sequence.string_of_byte_sequence (Dwarf_byte_sequence.sym_bs_expect_const lnfe.lnfe_path) )) lnh.lnh_file_entries in diff --git a/src/bin/dune b/src/bin/dune index f4c90590..02b51b85 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -4,7 +4,7 @@ (modules main) (flags (:standard -open Utils)) - (libraries config run utils sig_aarch64 other_cmds branchTable)) + (libraries config run utils sig_aarch64 other_cmds relsim)) (executable (name main_riscv64) @@ -12,7 +12,7 @@ (modules main_riscv64) (flags (:standard -open Utils)) - (libraries config run utils sig_riscv64 other_cmds branchTable)) + (libraries config run utils sig_riscv64 other_cmds)) (library (name other_cmds) @@ -20,4 +20,4 @@ (flags (:standard -open Utils)) (modules copySourcesCmd copySources dumpDwarf dumpSym readDwarf) - (libraries run utils config state trace)) + (libraries run utils config state trace relsim)) diff --git a/src/bin/main.ml b/src/bin/main.ml index fc17e98a..132b8f4a 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -71,9 +71,10 @@ let commands = Run.Func.command; Run.Instr.command; Run.Block.command; - Run.FuncRD.command; + (* Run.FuncRD.command; *) Other_cmds.CopySourcesCmd.command; - BranchTable.command; + (* BranchTable.command; *) + Z3.Test.command; ] let _ = Printexc.record_backtrace Config.enable_backtrace diff --git a/src/bin/main_riscv64.ml b/src/bin/main_riscv64.ml index 92a20d0f..50622cb7 100644 --- a/src/bin/main_riscv64.ml +++ b/src/bin/main_riscv64.ml @@ -71,9 +71,9 @@ let commands = Run.Func.command; Run.Instr.command; Run.Block.command; - Run.FuncRD.command; + (* Run.FuncRD.command; *) Other_cmds.CopySourcesCmd.command; - BranchTable.command; + (* BranchTable.command; *) ] let _ = Printexc.record_backtrace Config.enable_backtrace diff --git a/src/bin/readDwarf.ml b/src/bin/readDwarf.ml index 16d38882..9fe1ac33 100644 --- a/src/bin/readDwarf.ml +++ b/src/bin/readDwarf.ml @@ -72,7 +72,11 @@ let commands = Run.Instr.command; Run.Block.command; Run.FuncRD.command; + Run.RelProg.command; + Run.TestRelProg.command; CopySourcesCmd.command; + Z3.Test.command; + Relsim.command; ] let _ = Printexc.record_backtrace Config.enable_backtrace diff --git a/src/config/config.toml b/src/config/config.toml index 2497ed77..9c968490 100644 --- a/src/config/config.toml +++ b/src/config/config.toml @@ -66,7 +66,7 @@ toolchain = "aarch64-linux-gnu" arch-file = "../../aarch64.ir" # relative to the toml file arch-toml = "isla_aarch64.toml" # relative to the toml file linearize = ["ConditionHolds", "integer_conditional_select", "InterruptPending"] - other-opts = [] + other-opts = ["-R", "_PC=undefined:%bv64"] [archs.riscv64] toolchain = "riscv64-linux-gnu" diff --git a/src/config/isla_aarch64.toml b/src/config/isla_aarch64.toml index cf209041..f762a682 100644 --- a/src/config/isla_aarch64.toml +++ b/src/config/isla_aarch64.toml @@ -1,61 +1,24 @@ -#==================================================================================# -# BSD 2-Clause License # -# # -# Copyright (c) 2020-2021 Thibaut Pérami # -# Copyright (c) 2020-2021 Dhruv Makwana # -# Copyright (c) 2019-2021 Peter Sewell # -# All rights reserved. # -# # -# This software was developed by the University of Cambridge Computer # -# Laboratory as part of the Rigorous Engineering of Mainstream Systems # -# (REMS) project. # -# # -# This project has been partly funded by EPSRC grant EP/K008528/1. # -# This project has received funding from the European Research Council # -# (ERC) under the European Union's Horizon 2020 research and innovation # -# programme (grant agreement No 789108, ERC Advanced Grant ELVER). # -# This project has been partly funded by an EPSRC Doctoral Training studentship. # -# This project has been partly funded by Google. # -# # -# Redistribution and use in source and binary forms, with or without # -# modification, are permitted provided that the following conditions # -# are met: # -# 1. Redistributions of source code must retain the above copyright # -# notice, this list of conditions and the following disclaimer. # -# 2. Redistributions in binary form must reproduce the above copyright # -# notice, this list of conditions and the following disclaimer in # -# the documentation and/or other materials provided with the # -# distribution. # -# # -# THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' # -# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED # -# TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A # -# PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR # -# CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, # -# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT # -# LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF # -# USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND # -# ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, # -# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT # -# OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF # -# SUCH DAMAGE. # -# # -#==================================================================================# - # This is a config file for the Sail generated from ARM-ASL -# It is copied from the Isla repo and should be synced periodically. -# It probably contains a lot of stuff that's not needed for read-dwarf. pc = "_PC" ifetch = "Read_ifetch" -read_exclusives = ["Read_exclusive", "Read_exclusive_acquire"] -write_exclusives = ["Write_exclusive", "Write_exclusive_release"] +in_program_order = ["sail_barrier"] # The assembler is used for assembling the code in litmus tests. We # assume it takes arguments like GNU as. -assembler = "aarch64-linux-gnu-as -march=armv8.3-a" # read-dwarf +[[toolchain]] +name = "macos-aarch64" +os = "macos" +arch = "aarch64" +assembler = "as --target=aarch64-unknown-linux-gnu" +objdump = "/opt/homebrew/opt/llvm/bin/llvm-objdump" +linker = "/opt/homebrew/opt/llvm/bin/ld.lld" + +[[toolchain]] +name = "default" +assembler = "aarch64-linux-gnu-as -march=armv8.1-a" objdump = "aarch64-linux-gnu-objdump" linker = "aarch64-linux-gnu-ld" @@ -84,6 +47,8 @@ stride = "0x10" [registers] ignore = [ + "_PC", + "__PC_changed", "SEE", "__unconditional", "__trickbox_enabled", @@ -91,25 +56,15 @@ ignore = [ "__v82_implemented", "__v83_implemented", "__v84_implemented", - "__v85_implemented", - "_GTEExtObsAccess", - "_GTEExtObsActive", - "_GTEExtObsAddress", - "_GTEExtObsCount", - "_GTEExtObsData", - "_GTEExtObsIndex", - "_GTEExtObsResult", - "_GTEExtObsResultIndex", - "_GTEExtObsResultIsAddress", - "_GTE_PPU_Access", - "_GTE_PPU_Address", - "_GTE_PPU_SizeEn" + "__v85_implemented" ] # These registers are set before any symbolic execution occurs [registers.defaults] -"__isla_monomorphize_reads" = false -"__isla_monomorphize_writes" = false +"__isla_vector_gpr" = false +"__isla_continue_on_see" = true +"__monomorphize_reads" = false +"__monomorphize_writes" = false "VBAR_EL1" = "0x0000000000000000" "VBAR_EL2" = "0x0000000000000000" # Causes CNTCV to be incremented every cycle if bit 0 is 1 @@ -117,6 +72,7 @@ ignore = [ # SSAdvance? "MDSCR_EL1" = "0x00000000" "InGuardedPage" = false +"__highest_el_aarch32" = false "__currentInstrLength" = 4 "_PendingPhysicalSE" = false "__CNTControlBase" = "0x0000000000000" @@ -129,19 +85,18 @@ ignore = [ "CFG_RMR_AA64" = "0b1" "CFG_RVBAR" = "0x0000000010300000" "CFG_ID_AA64PFR0_EL1_MPAM" = "0x1" -"CFG_ID_AA64PFR0_EL1_EL3" = "0x2" -"CFG_ID_AA64PFR0_EL1_EL2" = "0x2" -"CFG_ID_AA64PFR0_EL1_EL1" = "0x2" -"CFG_ID_AA64PFR0_EL1_EL0" = "0x2" +"CFG_ID_AA64PFR0_EL1_EL3" = "0x1" +"CFG_ID_AA64PFR0_EL1_EL2" = "0x1" +"CFG_ID_AA64PFR0_EL1_EL1" = "0x1" +"CFG_ID_AA64PFR0_EL1_EL0" = "0x1" # Need to investigate BTI extension. Guard pages cause problems with # memory accesses. "__v81_implemented" = true -"__v82_implemented" = true # read-dwarf -"__v83_implemented" = true # read-dwarf +"__v82_implemented" = false +"__v83_implemented" = false "__v84_implemented" = false "__v85_implemented" = false "__unpred_tsize_aborts" = true -"exclusive_never_fails" = true # read-dwarf # Trickbox has various features for debugging spec and running tests "__trickbox_enabled" = false "__tlb_enabled" = false @@ -173,12 +128,20 @@ ignore = [ "__crypto_sm3_implemented" = false "__crypto_sha512_implemented" = false "__crypto_sha3_implemented" = false +"_GTEExtObsAccess" = "[0x0000; 256]" +"_GTEExtObsAddress" = "[0x0000000000000000; 256]" +"_GTEExtObsData" = "[0x0000000000000000; 256]" +"_GTEExtObsResult" = "[0x0000000000000000; 256]" +"_GTE_PPU_SizeEn" = "[0x00000000; 6]" +"_GTE_PPU_Address" = "[0x0000000000000000; 6]" +"_GTE_PPU_Access" = "[0x00000000; 6]" # These registers are set during symbolic execution by the special builtin "reset_registers" [registers.reset] -# Bit 1 being set causes us to abort on unaligned accesses +# Bit 1 being unset allows unaligned accesses # Bit 26 being set allows cache-maintenance ops in EL0 -"SCTLR_EL1" = "0x0000000004000002" +"SCTLR_EL1" = "0x0000000004000000" +"SCTLR_EL2" = "0x0000000004000000" # A map from register names that may appear in litmus files to Sail # register names @@ -245,45 +208,3 @@ ignore = [ "W28" = "R28" "W29" = "R29" "W30" = "R30" - -[reads] -Read_acquire = "A" -Read_exclusive_acquire = "A" - -[writes] -Write_release = "L" -Write_exclusive_release = "L" - -[cache_ops] -Cache_op_D_CVAU = "DC" -Cache_op_I_IVAU = "IC" -Cache_op_I_IALLU = "IC" - -# A mapping from Sail barrier_kinds for the spec to the names in cat -# memory models. -[barriers] -Barrier_DMB_SY = "DMB.SY" -Barrier_DMB_ST = "DMB.ST" -Barrier_DMB_LD = "DMB.LD" -Barrier_DMB_ISH = "DMB.ISH" -Barrier_DMB_ISHST = "DMB.ISHST" -Barrier_DMB_ISHLD = "DMB.ISHLD" -Barrier_DMB_NSH = "DMB.NSH" -Barrier_DMB_NSHST = "DMB.NSHST" -Barrier_DMB_NSHLD = "DMB.NSHLD" -Barrier_DMB_OSH = "DMB.OSH" -Barrier_DMB_OSHST = "DMB.OSHST" -Barrier_DMB_OSHLD = "DMB.OSHLD" -Barrier_DSB_SY = "DSB.SY" -Barrier_DSB_ST = "DSB.ST" -Barrier_DSB_LD = "DSB.LD" -Barrier_DSB_ISH = "DSB.ISH" -Barrier_DSB_ISHST = "DSB.ISHST" -Barrier_DSB_ISHLD = "DSB.ISHLD" -Barrier_DSB_NSH = "DSB.NSH" -Barrier_DSB_NSHST = "DSB.NSHST" -Barrier_DSB_NSHLD = "DSB.NSHLD" -Barrier_DSB_OSH = "DSB.OSH" -Barrier_DSB_OSHST = "DSB.OSHST" -Barrier_DSB_OSHLD = "DSB.OSHLD" -Barrier_ISB = "ISB" diff --git a/src/ctype/ctype.ml b/src/ctype/ctype.ml index daa31632..dbbe61f8 100644 --- a/src/ctype/ctype.ml +++ b/src/ctype/ctype.ml @@ -81,17 +81,17 @@ end) (*****************************************************************************) (** {1 DWARF constants } *) -let vDW_ATE_address = "DW_ATE_address" |> Dwarf.base_type_attribute_encode |> Z.to_int +let vDW_ATE_address = "DW_ATE_address" |> Dwarf.base_type_attribute_encode |> Sym.to_int -let vDW_ATE_boolean = "DW_ATE_boolean" |> Dwarf.base_type_attribute_encode |> Z.to_int +let vDW_ATE_boolean = "DW_ATE_boolean" |> Dwarf.base_type_attribute_encode |> Sym.to_int -let vDW_ATE_signed = "DW_ATE_signed" |> Dwarf.base_type_attribute_encode |> Z.to_int +let vDW_ATE_signed = "DW_ATE_signed" |> Dwarf.base_type_attribute_encode |> Sym.to_int -let vDW_ATE_signed_char = "DW_ATE_signed_char" |> Dwarf.base_type_attribute_encode |> Z.to_int +let vDW_ATE_signed_char = "DW_ATE_signed_char" |> Dwarf.base_type_attribute_encode |> Sym.to_int -let vDW_ATE_unsigned = "DW_ATE_unsigned" |> Dwarf.base_type_attribute_encode |> Z.to_int +let vDW_ATE_unsigned = "DW_ATE_unsigned" |> Dwarf.base_type_attribute_encode |> Sym.to_int -let vDW_ATE_unsigned_char = "DW_ATE_unsigned_char" |> Dwarf.base_type_attribute_encode |> Z.to_int +let vDW_ATE_unsigned_char = "DW_ATE_unsigned_char" |> Dwarf.base_type_attribute_encode |> Sym.to_int (*****************************************************************************) (*****************************************************************************) @@ -120,6 +120,7 @@ type unqualified = | Enum of { name : string; id : int } (** See {!env} for what the id refers to *) | FuncPtr (** Hack to accommodate PKVM *) | Missing (** Hack to accommodate PKVM *) + | Bits (** Hack to prevent losing type information when processing bitvectors with non-whole-byte sizes *) (** The internal representation of generalized C types *) and t = { @@ -136,7 +137,7 @@ and fragment = | Single of t (** Single object: Only when accessing of a global variable *) | DynArray of t (** Generic C pointer, may point to multiple element of that type *) | DynFragment of int (** Writable fragment for memory whose type is changing dynamically *) - | Global + | Global of string (** The Global fragment that contains all the fixed ELF section .text, .data, .rodata, ... *) @@ -337,6 +338,7 @@ let rec sizeof_unqualified = function | Array { elem; dims } -> let num = dims |> List.map (Option.value ~default:0) |> List.fold_left ( * ) 1 in num * sizeof elem + | Bits -> 0 (* Shouldn't use this value *) (** Give the size of an type. Need the environement. *) and sizeof t = sizeof_unqualified t.unqualified @@ -372,7 +374,7 @@ type conversion_context = { env : env; potential_link_name : string option } (** Get the id of a linksem [cupdie] *) let ids_of_cupdie ((cu, _, die) : Dwarf.cupdie) : cupdie_id = - (Z.to_int cu.cu_header.cuh_offset, Z.to_int die.die_offset) + (Sym.to_int cu.cu_header.cuh_offset, Sym.to_int die.die_offset) (** Pretty print the dwarf decl type @@ -380,7 +382,7 @@ let ids_of_cupdie ((cu, _, die) : Dwarf.cupdie) : cupdie_id = let pp_decl (d : Dwarf.decl) = Pp.dprintf "File %s, line %d" (Option.value d.decl_file ~default:"?") - (d.decl_line |> Option.map Z.to_int |> Option.value ~default:0) + (d.decl_line |> Option.map Sym.to_int |> Option.value ~default:0) (** This exception is raised when the type we are trying to reach must came from another translation unit or later in the current one. @@ -402,14 +404,14 @@ let expect_some_link = Option.value_fun ~default:(fun _ -> raise LinkError) Only integers, chars and bools supported. No floating points *) let base_type_of_linksem ?size ~encoding name = - let encoding = Z.to_int encoding in + let encoding = Sym.to_int encoding in if encoding = vDW_ATE_boolean then Cbool else if encoding = vDW_ATE_signed || encoding = vDW_ATE_unsigned then let size = Option.value_fail size "In Ctype.base_type_of_linksem: integer type %s do not have a size" name in - Cint { name; signed = encoding = vDW_ATE_signed; size = Z.to_int size; ischar = false } + Cint { name; signed = encoding = vDW_ATE_signed; size = Sym.to_int size; ischar = false } else if encoding = vDW_ATE_signed_char || encoding = vDW_ATE_unsigned_char then Cint { name; signed = encoding = vDW_ATE_signed_char; size = 1; ischar = true } else Raise.fail "In Ctype.base_of_linksem: encoding %x unknown" encoding @@ -428,7 +430,7 @@ let rec field_of_linksem ~cc ((_, fname, ltyp, offseto) : linksem_field) : field debug "Processed field %t" Pp.(top (opt string) fname); let offset = match offseto with - | Some offset -> Z.to_int offset + | Some offset -> Sym.to_int offset (* assume missing offsets are zero - perhaps should only occur for union members*) | None -> 0 in @@ -469,7 +471,7 @@ and[@warning "-16"] struct_type_of_linksem ?(force_complete = false) ~cc ~cupdie match Hashtbl.find cc.env.lenv (ids_of_cupdie cupdie) with | CT (CT_struct_union (_, Atk_structure, _, msize, _, Some members)) -> let lsize = expect_some_link msize in - let size = Z.to_int lsize in + let size = Sym.to_int lsize in let cc = { cc with potential_link_name = Some name } in let struc : struc = struc_of_linksem ~cc name size members in IdMap.seti cc.env.structs id struc; @@ -485,7 +487,7 @@ and[@warning "-16"] struct_type_of_linksem ?(force_complete = false) ~cc ~cupdie | CT (CT_struct_union (_, Atk_structure, _, msize, _, Some members)) -> let size = match msize with - | Some x -> Z.to_int x + | Some x -> Sym.to_int x | None -> warn "Struct %s doesn't have size" name; 0 @@ -503,7 +505,7 @@ and[@warning "-16"] struct_type_of_linksem ?(force_complete = false) ~cc ~cupdie and enum_of_linksem ~cc:_ name llabels : enum = let labels = Hashtbl.create 5 in - List.iter (fun (_, name, value) -> Hashtbl.add labels (Z.to_int value) name) llabels; + List.iter (fun (_, name, value) -> Hashtbl.add labels (Sym.to_int value) name) llabels; { name; labels } and enum_type_of_linksem ~cc ~cupdie ~mname ~decl : unqualified = @@ -529,13 +531,13 @@ and unqualified_of_linksem ?(force_complete = false) ~cc : linksem_t -> unqualif | CT (CT_pointer (_, Some t)) -> ptr @@ of_linksem_cc ~cc t | CT (CT_pointer (_, None)) -> voidstar | CT (CT_array (_, elem, l)) -> - Array { elem = of_linksem_cc ~cc elem; dims = List.map Fun.(fst %> Option.map Z.to_int) l } + Array { elem = of_linksem_cc ~cc elem; dims = List.map Fun.(fst %> Option.map Sym.to_int) l } | CT (CT_struct_union (cupdie, Atk_structure, mname, _, decl, _)) -> struct_type_of_linksem ~force_complete ~cc ~cupdie ~mname ~decl | CT (CT_struct_union (_, Atk_union, _, size, decl, _)) -> let size = match size with - | Some s -> Z.to_int s + | Some s -> Sym.to_int s | None -> warn "%t: Sizeless union defaulting to 8 for now" Pp.(top pp_decl decl); 8 @@ -619,7 +621,7 @@ let env_of_linksem (lenv : linksem_env) : env = Option.( let+! name = mname and+ size = msize in if not @@ IdMap.mem env.structs name then - IdMap.add env.structs name @@ incomplete_struct name (Z.to_int size) |> ignore) + IdMap.add env.structs name @@ incomplete_struct name (Sym.to_int size) |> ignore) | _ -> ()) lenv; (* Third phase: Add all the type to the result environement *) @@ -660,6 +662,7 @@ and pp_unqualified = function | Enum { name; _ } -> dprintf "Enum %s" name | FuncPtr -> dprintf "FuncPtr" | Missing -> dprintf "Missing" + | Bits -> dprintf "Bits" and pp_fragment frag = group @@ -669,7 +672,7 @@ and pp_fragment frag = | DynArray t -> pp t ^^ !^"[]" | Unknown -> !^"unknown" | DynFragment i -> dprintf "frag %d" i - | Global -> !^"global" + | Global s -> !^"global " ^^ !^s and pp_offset = function | Const off when off = 0 -> empty diff --git a/src/dune b/src/dune index cdaa4d1c..b474cb2a 100644 --- a/src/dune +++ b/src/dune @@ -2,3 +2,5 @@ (release (flags (:standard -short-paths)))) + +(dirs :standard \ branchTable) \ No newline at end of file diff --git a/src/dw/addr.ml b/src/dw/addr.ml new file mode 100644 index 00000000..201906bf --- /dev/null +++ b/src/dw/addr.ml @@ -0,0 +1,6 @@ +include Elf.Address + +let of_sym : Sym.t -> t = function +| Sym_ocaml.Num.Offset (section, offset) -> { section; offset = Z.to_int offset } +| _ -> Raise.fail "expected section+offset" + diff --git a/src/dw/dw.ml b/src/dw/dw.ml index 270c3576..af505b53 100644 --- a/src/dw/dw.ml +++ b/src/dw/dw.ml @@ -85,7 +85,7 @@ let of_elf (elf : Elf.File.t) = Arch.load_elf_arch elf; info "Extracting dwarf of %s" elf.filename; let ldwarf = - match Dwarf.extract_dwarf elf.linksem with + match Dwarf.extract_dwarf elf.linksem Abi_aarch64_symbolic_relocation.aarch64_data_relocation_interpreter with | Some d -> d | None -> dwarferror "Linksem extract_dwarf failed" in diff --git a/src/dw/func.ml b/src/dw/func.ml index 32f64174..a4d5894f 100644 --- a/src/dw/func.ml +++ b/src/dw/func.ml @@ -140,7 +140,8 @@ let of_linksem (elf : Elf.File.t) (tenv : Ctype.env) (lfun : linksem_t) = | None -> ( match lfun.ss_entry_address with | Some a -> ( - match Elf.SymTable.of_addr_opt elf.symbols (Nat_big_num.to_int a) with + let addr = Addr.of_sym a in + match Elf.SymTable.of_addr_opt elf.symbols addr with | Some sym -> Some sym | None -> None ) diff --git a/src/dw/loc.ml b/src/dw/loc.ml index 7b194e3e..a63fcc53 100644 --- a/src/dw/loc.ml +++ b/src/dw/loc.ml @@ -72,6 +72,7 @@ type t = | RegisterOffset of State.Reg.t * int (** At register + offset address *) | StackFrame of int (** On the stackFrame with offset *) | Global of Elf.SymTable.sym_offset (** Global variable with an offset *) + | Const of Sym.t | Dwarf of dwop list (** Uninterpreted dwarf location *) (** The type of a location in linksem format *) @@ -83,49 +84,54 @@ type linksem_t = dwop list let vDW_OP_addr : int = 0x03 (** The integer value of the DW_OP_reg0 constant in DWARF standard *) -let vDW_OP_reg0 : int = Z.to_int Dwarf.vDW_OP_reg0 +let vDW_OP_reg0 : int = Sym.to_int Dwarf.vDW_OP_reg0 (** The integer value of the DW_OP_breg0 constant in DWARF standard *) -let vDW_OP_breg0 : int = Z.to_int Dwarf.vDW_OP_breg0 +let vDW_OP_breg0 : int = Sym.to_int Dwarf.vDW_OP_breg0 (** Convert a linksem location description into a {!Loc.t} Very naive for now : If the list has a single element that we can translate directly, we do. Otherwise, we dump it into the {!t.Dwarf} constructor *) let of_linksem ?(amap = Arch.dwarf_reg_map ()) (elf : Elf.File.t) : linksem_t -> t = - let int_of_oav : Dwarf.operation_argument_value -> int = function - | OAV_natural n -> Z.to_int n - | OAV_integer i -> Z.to_int i - | _ -> failwith "Expected integer argument" + let sym_of_oav : Dwarf.operation_argument_value -> Sym.t = function + | OAV_natural n -> n + | OAV_integer i -> i + | _ -> failwith "Expected integer argument" in + let int_of_oav oav = oav |> sym_of_oav |> Sym.to_int in function (* Register *) | [({ op_semantics = OpSem_reg; _ } as op)] -> - let reg_num = Z.to_int op.op_code - vDW_OP_reg0 in + let reg_num = Sym.to_int op.op_code - vDW_OP_reg0 in if reg_num >= Array.length amap then failwith (Printf.sprintf "Loc.of_linksem: register number %d unknown, code %x, name %s" reg_num - (Z.to_int op.op_code) op.op_string) + (Sym.to_int op.op_code) op.op_string) else Register amap.(reg_num) (* RegisterOffset *) | [({ op_semantics = OpSem_breg; op_argument_values = [arg]; _ } as op)] -> - let reg_num = Z.to_int op.op_code - vDW_OP_breg0 in + let reg_num = Sym.to_int op.op_code - vDW_OP_breg0 in if reg_num >= Array.length amap then failwith (Printf.sprintf "Loc.of_linksem: register number %d unknown, code %x, name %s" reg_num - (Z.to_int op.op_code) op.op_string) + (Sym.to_int op.op_code) op.op_string) else RegisterOffset (amap.(reg_num), int_of_oav arg) (* StackFrame *) | [{ op_semantics = OpSem_fbreg; op_argument_values = [arg]; _ }] -> StackFrame (int_of_oav arg) (* Global *) | [{ op_semantics = OpSem_lit; op_code = code; op_argument_values = [arg]; _ }] as ops - when Z.to_int code = vDW_OP_addr -> ( - try Global (Elf.SymTable.of_addr_with_offset elf.symbols @@ int_of_oav arg) + when Sym.to_int code = vDW_OP_addr -> ( + let addr = Addr.of_sym @@ sym_of_oav arg in + try Global (Elf.SymTable.of_addr_with_offset elf.symbols @@ addr) with Not_found -> - warn "Symbol at 0x%x not found in Loc.of_linksem" (int_of_oav arg); + warn "Symbol at %t not found in Loc.of_linksem" (Pp.top Sym.pp (sym_of_oav arg)); Dwarf ops ) (* Other *) + | [{ op_semantics = OpSem_lit; op_argument_values = [arg]; _ }; { op_semantics = OpSem_stack_value; _ }] -> + let value = sym_of_oav arg in + Const value | ops -> Dwarf ops (** Convert the location to a string. This is not reversible *) @@ -134,6 +140,7 @@ let to_string = function | RegisterOffset (reg, off) -> Printf.sprintf "[%s+%x]" (State.Reg.to_string reg) off | StackFrame off -> Printf.sprintf "[frame+%x]" off | Global symoff -> Elf.SymTable.string_of_sym_offset symoff + | Const x -> Sym.to_string x | Dwarf ops -> Dwarf.pp_operations ops (** Compare two location. Loc.t is not compatible with polymorphic compare *) @@ -152,6 +159,12 @@ let compare l1 l2 = Pair.compare ~fst:Elf.Symbol.compare (sym1, off1) (sym2, off2) | (Global (_, _), _) -> -1 | (_, Global (_, _)) -> 1 + | (Const (Absolute x), Const (Absolute y)) -> Z.compare x y + | (Const (Offset(s,x)), Const (Offset(t,y))) -> Pair.compare ~snd:Z.compare (s,x) (t,y) + | (Const (Absolute _), Const (Offset _)) -> -1 + | (Const (Offset _), Const (Absolute _)) -> 1 + | (Const _, _) -> -1 + | (_, Const _) -> 1 | (Dwarf ops1, Dwarf ops2) -> compare ops1 ops2 (** Pretty-print the location *) diff --git a/src/dw/var.ml b/src/dw/var.ml index 0e6d86d5..a6a28c6c 100644 --- a/src/dw/var.ml +++ b/src/dw/var.ml @@ -45,21 +45,30 @@ (** This module contain all the definition to handle local and global variables as defined in the DWARF information of the target file *) +type range = Addr.t * Addr.t option + (** Type of a DWARF variable *) -type t = { name : string; param : bool; ctype : Ctype.t; locs : ((int * int) * Loc.t) list } +type t = { + name : string; + param : bool; + ctype : Ctype.t; + locs : (range * Loc.t) list; + locs_frame_base : (range * Loc.t) list; +} (** Type of a DWARF variable in linksem *) type linksem_t = Dwarf.sdt_variable_or_formal_parameter (** Merge contiguous location lists *) let rec loc_merge = function - | ((a1, b1), d1) :: ((a2, b2), d2) :: l when b1 = a2 && Loc.compare d1 d2 = 0 -> + | ((a1, b1), d1) :: ((a2, b2), d2) :: l when b1 = Some a2 && Loc.compare d1 d2 = 0 -> loc_merge (((a1, b2), d1) :: l) | a :: l -> a :: loc_merge l | [] -> [] -(** Convert from Z.t to int, if there is an overflow, returns Int.max_int instead of throwing *) -let clamp_z z = try Z.to_int z with Z.Overflow when Z.compare z Z.zero > 0 -> Int.max_int +let end_addr_of_sym = function +| Sym_ocaml.Num.Absolute z when Z.compare z (Z.of_int Int.max_int) > 0 -> None +| x -> Some (Addr.of_sym x) (** Create a DWARF variable from its linksem counterpart *) let of_linksem (elf : Elf.File.t) (env : Ctype.env) (lvar : linksem_t) : t = @@ -72,10 +81,15 @@ let of_linksem (elf : Elf.File.t) (env : Ctype.env) (lvar : linksem_t) : t = in let locs = lvar.svfp_locations |> Option.value ~default:[] - |> List.map (fun (a, b, l) -> ((Z.to_int a, clamp_z b), Loc.of_linksem elf l)) + |> List.map (fun (a, b, l) -> ((Addr.of_sym a, end_addr_of_sym b), Loc.of_linksem elf l)) + |> loc_merge + in + let locs_frame_base = + lvar.svfp_locations_frame_base |> Option.value ~default:[] + |> List.map (fun (a, b, l) -> ((Addr.of_sym a, end_addr_of_sym b), Loc.of_linksem elf l)) |> loc_merge in - { name; param; ctype; locs } + { name; param; ctype; locs; locs_frame_base } (** Pretty print a variable *) let pp_raw v = @@ -85,5 +99,5 @@ let pp_raw v = [ ("name", string v.name); ("ctype", Ctype.pp v.ctype); - ("locs", list (pair (pair ptr ptr) Loc.pp) v.locs); + ("locs", list (pair (pair Addr.pp (opt Addr.pp)) Loc.pp) v.locs); ]) diff --git a/src/elf/address.ml b/src/elf/address.ml new file mode 100644 index 00000000..33da9cd8 --- /dev/null +++ b/src/elf/address.ml @@ -0,0 +1,26 @@ +type t = { + section : string; + offset: int; +} + +let pp addr = Pp.(!^(addr.section) ^^ !^"+" ^^ ptr addr.offset) + +let of_linksem (section, offset) = { section; offset = Z.to_int offset } + +let (+) addr offset = { section = addr.section; offset = addr.offset + offset } + +let compare f {section=s1; offset=o1} {section=s2; offset=o2} = + if s1 = s2 then + Some (f o1 o2) + else + None + +let (<) = compare (<) + +let (>) = compare (>) + +let (<=) = compare (<=) + +let (>=) = compare (>=) + +let to_sym {section; offset} = Sym_ocaml.Num.Offset (section, Z.of_int offset) \ No newline at end of file diff --git a/src/elf/file.ml b/src/elf/file.ml index 4b49c026..095ad835 100644 --- a/src/elf/file.ml +++ b/src/elf/file.ml @@ -75,6 +75,14 @@ let machine_to_string = function (** Pretty prints a {!machine} *) let pp_machine mach = mach |> machine_to_string |> Pp.string +module SMap = Map.Make(String) + +type section = { + name : string; + size : int; + align : int; +} + (** The type containing all the information about an ELF file *) type t = { filename : string; (** The name on the file system. Useful for error messages *) @@ -84,7 +92,8 @@ type t = { (** The target architecture of the file; only used in [arch.ml, dumpSym.ml, dw.ml] *) linksem : Elf_file.elf_file; (** The original linksem structure for the file; only used in [dw.ml] *) - rodata : Segment.t; (** The read-only data section *) + rodata : Segment.t SMap.t; (** The read-only data sections *) + sections : section list; } (** Error on Elf parsing *) @@ -105,61 +114,78 @@ let elferror fmt = Printf.ksprintf (fun s -> raise (ElfError s)) fmt let of_file (filename : string) = info "Loading ELF file %s" filename; (* parse the ELF file using linksem *) - let ( (elf_file : Elf_file.elf_file), + let bs = match Byte_sequence.acquire filename with + | Error.Fail s -> elferror "Linksem: Byte_sequence.acquire: %s" s + | Error.Success x -> x + in + let elf64_file = match Elf_file.read_elf64_file bs with + | Error.Fail s -> elferror "Linksem: read_elf64_file: %s" s + | Error.Success x -> x + in + let symbol_map = match LinksemRelocatable.get_elf64_file_global_symbol_init elf64_file with + | Error.Fail s -> elferror "LinksemRelocatable: get_elf64_file_global_symbol_init: %s" s + | Error.Success x -> x + in + (* let ( (elf_file : Elf_file.elf_file), (elf_epi : Sail_interface.executable_process_image), (symbol_map : Elf_file.global_symbol_init_info) ) = match Sail_interface.populate_and_obtain_global_symbol_init_info filename with | Error.Fail s -> elferror "Linksem: populate_and_obtain_global_symbol_init_info: %s" s | Error.Success x -> x - in + in *) (* Check this is a 64 bits ELF file *) - begin - match elf_file with - | Elf_file.ELF_File_32 _ -> elferror "32 bits elf files unsupported" - | _ -> () - end; - let (segments, entry, machine) = - match elf_epi with - | ELF_Class_32 _ -> elferror "32 bits elf file class unsupported" - | ELF_Class_64 (s, e, m) -> (s, e, m) - in - - (* Extract all the segments *) - let segments = - List.filter_map - (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None) - segments - in - let entry = Z.to_int entry in - let machine = machine_of_linksem machine in - debug "Loading ELF segments of %s" filename; - let segments = List.map Segment.of_linksem segments in - debug "Loaded ELF segments %t" - @@ Pp.top (Pp.list Pp.hex) - @@ List.map (fun x -> x.Segment.addr) segments; + let entry = Z.to_int elf64_file.elf64_file_header.elf64_entry in + let machine = machine_of_linksem elf64_file.elf64_file_header.elf64_machine in debug "Loading ELF symbols of %s" filename; - let symbols = SymTbl.of_linksem segments symbol_map in + let symbols = SymTbl.of_linksem symbol_map in debug "Adding .rodata section of %s" filename; (* We add the .rodata section seperately from the symbols because - it can contain non-symbol information such as string literals and constants used in branch-register target calculations - the range of the section is guaranteed to overlap with any symbols within it, and so not suitable to be stored in the [RngMap] *) - let rodata = - let (_, addr, data) = - Dwarf.extract_section_body elf_file ".rodata" false - (* `false' argument is for returning an empty byte-sequence if - section is not found, instead of throwing an exception *) - in - Segment. - { - data; - addr = Nat_big_num.to_int addr; - size = BytesSeq.length data; - read = true; - write = false; - execute = false; + let elf_file = Elf_file.ELF_File_64 elf64_file in + let sections = List.filter_map (fun (s:Elf_interpreted_section.elf64_interpreted_section) -> + if Z.equal Z.zero (Z.logand s.elf64_section_flags Elf_section_header_table.shf_alloc) then + None + else + Some { + name=s.elf64_section_name_as_string; + size=Z.to_int s.elf64_section_size; + align=Z.to_int s.elf64_section_align; } + ) elf64_file.elf64_file_interpreted_sections + in + let rodata = + SMap.of_list @@ List.filter_map Option.(fun (section:Elf_interpreted_section.elf64_interpreted_section) -> + let+ sname = if String.starts_with ~prefix:".rodata" section.elf64_section_name_as_string then + Some section.elf64_section_name_as_string + else + None + in + let data = section.elf64_section_body in + let relocations = match LinksemRelocatable.get_relocations_for_section elf64_file sname with + | Error.Fail s -> elferror "LinksemRelocatable: get_relocations_for_section: %s" s + | Error.Success x -> Relocations.of_linksem x + in + (* let (_, addr, data) = + Dwarf.extract_section_body elf_file Abi_aarch64_symbolic_relocation.aarch64_data_relocation_interpreter sname false + (* `false' argument is for returning an empty byte-sequence if + section is not found, instead of throwing an exception *) + in *) + ( + sname, + Segment. + { + data = (data, relocations); + addr = 0; (* Meaningless for relocatable files *) + size = BytesSeq.length data; + read = true; + write = false; + execute = false; + } + ) + ) elf64_file.elf64_file_interpreted_sections in info "ELF file %s has been loaded" filename; - { filename; symbols; entry; machine; linksem = elf_file; rodata } + { filename; symbols; entry; machine; linksem = elf_file; rodata; sections } diff --git a/src/elf/linksemRelocatable.ml b/src/elf/linksemRelocatable.ml new file mode 100644 index 00000000..5f92e2e0 --- /dev/null +++ b/src/elf/linksemRelocatable.ml @@ -0,0 +1,75 @@ +(* TODO header *) + +module SMap = Map.Make (String) + +type sym_addr = string * Z.t + +type rels = + | AArch64 of (Z.t, Abi_aarch64_symbolic_relocation.aarch64_relocation_target Elf_symbolic.universal_relocation) Pmap.map + +type sym_data = +Byte_sequence_wrapper.byte_sequence * rels + + +(* Like in linksem, but address is section+offset, data has relocations and with a writable flag *) +type symbol = string * (Z.t * Z.t * sym_addr * sym_data * Z.t) * bool + +type global_symbol_init_info = symbol list + +open Elf_symbol_table +open Elf_interpreted_section + +let get_relocations_for_section (f:Elf_file.elf64_file) section = + let machine = f.elf64_file_header.elf64_machine in + if machine = Elf_header.elf_ma_aarch64 then + Error.bind + (Elf_symbolic.extract_elf64_relocations_for_section f Abi_aarch64_symbolic_relocation.aarch64_relocation_interpreter section) + @@ fun relocs -> Error.return (AArch64 relocs) + else + Error.fail @@ "machine not supported " ^ (Elf_header.string_of_elf_machine_architecture machine) + +let get_elf64_file_global_symbol_init (f: Elf_file.elf64_file) : global_symbol_init_info Error.error = + let secs = f.elf64_file_interpreted_sections in + Error.bind (Elf_file.get_elf64_file_symbol_table f) @@ fun (symtab, strtab) -> + let rel_cache = ref SMap.empty in + let get_relocs section = + match SMap.find_opt section !rel_cache with + | Some rels -> rels + | None -> get_relocations_for_section f section + in + List.filter_map ( + fun entry -> + let name = Uint32_wrapper.to_bigint entry.elf64_st_name in + let addr_offset = Uint64_wrapper.to_bigint entry.elf64_st_value in + let size = Uint64_wrapper.to_bigint entry.elf64_st_size in + let shndx = Uint32_wrapper.to_int entry.elf64_st_shndx in + let typ = Elf_symbol_table.extract_symbol_type entry.elf64_st_info in + let bnd = Elf_symbol_table.extract_symbol_binding entry.elf64_st_info in + Option.map ( + fun section -> + let addr = (section.elf64_section_name_as_string, addr_offset) in + let data = if Byte_sequence.length0 section.elf64_section_body = Z.zero then + Error.return (Byte_sequence.zeros size) + else + Byte_sequence.offset_and_cut addr_offset size section.elf64_section_body + in + Error.bind (get_relocs section.elf64_section_name_as_string) @@ fun (AArch64 relocs) -> + let relocs = relocs + |> Pmap.bindings_list + |> List.fold_left (fun m (pos, r) -> + let sz = size in + let open Z in + let open Compare in + if pos >= addr_offset && pos < addr_offset + sz then + Pmap.add (pos - addr_offset) r m + else + m + ) (Pmap.empty Z.compare) + |> fun x -> AArch64 x + in + Error.bind data @@ fun data -> + Error.bind (String_table.get_string_at name strtab) @@ fun str -> + let write = Elf_file.flag_is_set Elf_section_header_table.shf_write section.elf64_section_flags in + Error.return (str, (typ, size, addr, (data, relocs), bnd), write) + ) (List.nth_opt secs shndx) + ) symtab |> Error.mapM Fun.id \ No newline at end of file diff --git a/src/elf/relocations.ml b/src/elf/relocations.ml new file mode 100644 index 00000000..04117864 --- /dev/null +++ b/src/elf/relocations.ml @@ -0,0 +1,92 @@ +module IMap = Map.Make (Int) + +type target = + AArch64 of Abi_aarch64_symbolic_relocation.aarch64_relocation_target + +type binary_operation = Elf_symbolic.binary_operation + +type unary_operation = Elf_symbolic.unary_operation + +type exp = +| Section of string +| Const of int +| BinOp of (exp * binary_operation * exp) +| UnOp of (unary_operation * exp) + +type assertion = +| Range of int64 * int64 +| Alignment of int + +type rel = { + target : target; + value : exp; + checks: assertion list; + mask : int * int; +} + +type t = rel IMap.t + +type linksem_t = LinksemRelocatable.rels + +let rel_of_aarch64_linksem Elf_symbolic.{rel_desc_value; rel_desc_checks; rel_desc_mask; rel_desc_target } = + let rec value_of_linksem = function + | Elf_symbolic.Section s -> Section s + | Elf_symbolic.Const x -> Const (Z.to_int x) + | Elf_symbolic.BinOp (x, op, y) -> BinOp (value_of_linksem x, op, value_of_linksem y) + | Elf_symbolic.UnOp (op, x) -> UnOp (op, value_of_linksem x) + in + let checks = List.map (function + | Elf_symbolic.Overflow (min, max) -> Range (Z.to_int64 min, Z.to_int64 max) + | Elf_symbolic.Alignment (bits) -> Alignment (Z.to_int bits) + ) rel_desc_checks in + let hi, lo = rel_desc_mask in + { + target=AArch64 rel_desc_target; + checks; + mask = (Z.to_int hi, Z.to_int lo); + value = value_of_linksem rel_desc_value + } + + +let of_linksem: linksem_t -> t = function +| LinksemRelocatable.AArch64 relocs -> + let add k rel m = + IMap.add (Z.to_int k) (rel_of_aarch64_linksem rel) m + in + Pmap.fold add relocs IMap.empty + +let sub rels off len = + rels + |> IMap.to_list + |> List.filter_map (fun (pos, rel) -> if off <= pos && pos < off + len then Some (pos-off, rel) else None) + |> IMap.of_list + +let rec pp_exp = Pp.( + function + | Section s -> !^s + | Const x -> int x + | BinOp (a, Add, b) -> !^"(" ^^ pp_exp a ^^ !^"+" ^^ pp_exp b ^^ !^")" + | BinOp (a, Sub, b) -> !^"(" ^^ pp_exp a ^^ !^"-" ^^ pp_exp b ^^ !^")" + | BinOp (a, And, b) -> !^"(" ^^ pp_exp a ^^ !^"&" ^^ pp_exp b ^^ !^")" + | UnOp (Not, b) -> !^"(" ^^ !^"~" ^^ pp_exp b ^^ !^")" +) + +let pp_target = Pp.(function +| AArch64 Abi_aarch64_symbolic_relocation.Data640 -> !^"Data64" +| AArch64 Abi_aarch64_symbolic_relocation.Data320 -> !^"Data32" +| AArch64 Abi_aarch64_symbolic_relocation.ADD -> !^"ADD" +| AArch64 Abi_aarch64_symbolic_relocation.ADRP -> !^"ADRP" +| AArch64 Abi_aarch64_symbolic_relocation.CALL -> !^"CALL" +| AArch64 Abi_aarch64_symbolic_relocation.LDST b -> !^"LDST" ^^ int (1 lsl b) +| AArch64 Abi_aarch64_symbolic_relocation.CONDBR -> !^"CONDBR" +| AArch64 Abi_aarch64_symbolic_relocation.B -> !^"B") + +let pp_rel rel = + let hi, lo = rel.mask in + Pp.(pp_target rel.target ^^ !^": " ^^ pp_exp rel.value ^^ !^"[" ^^ int hi ^^ !^":" ^^ int lo ^^ !^"]") + +let pp rels = + if IMap.is_empty rels then + Pp.empty + else + Pp.(mapping "relocations" @@ List.map (fun (i, r) -> (hex i, pp_rel r)) (IMap.to_list rels)) \ No newline at end of file diff --git a/src/elf/segment.ml b/src/elf/segment.ml index faacf802..51b82009 100644 --- a/src/elf/segment.ml +++ b/src/elf/segment.ml @@ -51,7 +51,7 @@ (** The type of a segment *) type t = { - data : BytesSeq.t; + data : BytesSeq.t * Relocations.t; addr : int; (** The actual start address of the BytesSeq *) size : int; (** redundant with {!Utils.BytesSeq.length} data *) read : bool; @@ -66,7 +66,7 @@ let of_linksem (lseg : Elf_interpreted_segment.elf64_interpreted_segment) : t = BytesSeq.blit lseg.elf64_segment_body 0 bytes 0 (Z.to_int lseg.elf64_segment_size); let (read, write, execute) = lseg.elf64_segment_flags in { - data = BytesSeq.of_bytes bytes; + data = BytesSeq.of_bytes bytes, Relocations.IMap.empty; addr = Z.to_int lseg.elf64_segment_base; size; read; diff --git a/src/elf/symTable.ml b/src/elf/symTable.ml index d1b2ecd7..f0ac45a1 100644 --- a/src/elf/symTable.ml +++ b/src/elf/symTable.ml @@ -59,19 +59,57 @@ type sym_offset = sym * int module RMap = RngMap.Make (Symbol) module SMap = Map.Make (String) -type linksem_t = Elf_file.global_symbol_init_info - -type t = { by_name : sym SMap.t; by_addr : RMap.t } - -let empty = { by_name = SMap.empty; by_addr = RMap.empty } +module AddrMap = struct + type t = RMap.t SMap.t + + let add t (addr: Address.t) sym = + SMap.update addr.section (fun old -> + let old = match old with + | None -> RMap.empty + | Some x -> x + in + Some (RMap.add old addr.offset sym) + ) t + + let update f t (addr: Address.t) = + SMap.update addr.section (Option.map (fun x -> RMap.update f x addr.offset)) t + + let empty = SMap.empty + + let at t (addr: Address.t) = + SMap.find addr.section t |> Fun.flip RMap.at addr.offset + + let at_opt t (addr: Address.t) = + Option.bind (SMap.find_opt addr.section t) @@ Fun.flip RMap.at_opt addr.offset + + let at_off t (addr: Address.t) = + SMap.find addr.section t |> Fun.flip RMap.at_off addr.offset + + let at_off_opt t (addr: Address.t) = + Option.bind (SMap.find_opt addr.section t) @@ Fun.flip RMap.at_off_opt addr.offset + + let bindings t = + let sections = SMap.bindings t in + List.bind sections @@ fun (section, rmap) -> + let inner_bindings = RMap.bindings rmap in + List.map (fun (offset, sym) -> (Address.{section; offset}, sym)) inner_bindings + + +end + +type linksem_t = LinksemRelocatable.global_symbol_init_info + +type t = { by_name : sym SMap.t; by_addr : AddrMap.t } + +let empty = { by_name = SMap.empty; by_addr = AddrMap.empty } let add t sym = let by_name = SMap.add sym.name sym t.by_name in - try { by_name; by_addr = RMap.add t.by_addr sym.addr sym } + try { by_name; by_addr = AddrMap.add t.by_addr sym.addr sym } with Invalid_argument _ -> let updated = ref false in let by_addr = - RMap.update + AddrMap.update (fun usym -> if usym.addr = sym.addr && usym.size = sym.size then begin updated := true; @@ -88,15 +126,15 @@ let of_name t name = let of_name_opt t name = SMap.find_opt name t.by_name -let of_addr t addr = RMap.at t.by_addr addr +let of_addr t addr = AddrMap.at t.by_addr addr -let of_addr_opt t addr = RMap.at_opt t.by_addr addr +let of_addr_opt t addr = AddrMap.at_opt t.by_addr addr -let of_addr_with_offset t addr = RMap.at_off t.by_addr addr +let of_addr_with_offset t addr = AddrMap.at_off t.by_addr addr -let of_addr_with_offset_opt t addr = RMap.at_off_opt t.by_addr addr +let of_addr_with_offset_opt t addr = AddrMap.at_off_opt t.by_addr addr -let to_addr_offset (sym, offset) = sym.addr + offset +let to_addr_offset (sym, offset) = Address.(sym.addr + offset) let string_of_sym_offset ((sym, off) : sym_offset) = sym.name ^ "+" ^ string_of_int off @@ -109,15 +147,16 @@ let sym_offset_of_string t s : sym_offset = let of_position_string t s : sym_offset = let s = String.trim s in if s = "" then raise Not_found; - if s.[0] = '0' then of_addr_with_offset t (int_of_string s) else sym_offset_of_string t s + if s.[0] = '0' then raise Not_found (* no absolute addresses *) + else sym_offset_of_string t s -let of_linksem segments linksem_map = +let of_linksem linksem_map = let add_linksem_sym_to_map (map : t) (lsym : linksem_sym) = - if is_interesting_linksem lsym then add map (Symbol.of_linksem segments lsym) else map + if is_interesting_linksem lsym then add map (Symbol.of_linksem lsym) else map in List.fold_left add_linksem_sym_to_map empty linksem_map -let pp_raw st = RMap.bindings st.by_addr |> List.map (Pair.map Pp.ptr pp_raw) |> Pp.mapping "syms" +let pp_raw st = AddrMap.bindings st.by_addr |> List.map (Pair.map Address.pp pp_raw) |> Pp.mapping "syms" let iter t f = SMap.iter (fun _ value -> f value) t.by_name diff --git a/src/elf/symTable.mli b/src/elf/symTable.mli index bcd57ca5..18e7de50 100644 --- a/src/elf/symTable.mli +++ b/src/elf/symTable.mli @@ -57,7 +57,7 @@ type linksem_sym = Symbol.linksem_t (** The type of a symbol with offset *) type sym_offset = sym * int -type linksem_t = Elf_file.global_symbol_init_info +type linksem_t = LinksemRelocatable.global_symbol_init_info (** The type of a symbol table. *) type t @@ -78,19 +78,19 @@ val of_name_opt : t -> string -> sym option (** Get the symbol owning that address. Not_found is raised if no symbol own that address.data See {!of_addr_opt} *) -val of_addr : t -> int -> sym +val of_addr : t -> Address.t -> sym (** Get the symbol owning that address. None if no symbol own that address. See {!of_addr} *) -val of_addr_opt : t -> int -> sym option +val of_addr_opt : t -> Address.t -> sym option (** Get a symbol with the offset that correspond to that address *) -val of_addr_with_offset : t -> int -> sym_offset +val of_addr_with_offset : t -> Address.t -> sym_offset (** Get a symbol with the offset that correspond to that address *) -val of_addr_with_offset_opt : t -> int -> sym_offset option +val of_addr_with_offset_opt : t -> Address.t -> sym_offset option (** Get back the raw address from a symbol+offset value *) -val to_addr_offset : sym_offset -> int +val to_addr_offset : sym_offset -> Address.t (** Transform a symbol + offset into the corresponding string *) val string_of_sym_offset : sym_offset -> string @@ -110,7 +110,7 @@ val of_position_string : t -> string -> sym_offset (** Extract the symbol from the linksem symbol representation. Need the segments for filling the missing symbol data *) -val of_linksem : Segment.t list -> linksem_t -> t +val of_linksem : linksem_t -> t (** Pretty print the table as a raw ocaml value *) val pp_raw : t -> Pp.document diff --git a/src/elf/symbol.ml b/src/elf/symbol.ml index 439dc0ec..263c184b 100644 --- a/src/elf/symbol.ml +++ b/src/elf/symbol.ml @@ -42,27 +42,37 @@ (* *) (*==================================================================================*) +open Logs.Logger (struct + let str = __MODULE__ +end) + (* The documentation is in the mli file *) type typ = NOTYPE | OBJECT | FUNC | SECTION | FILE | UNKNOWN type linksem_typ = Z.t +type data = { + data: BytesSeq.t; + relocations: Relocations.t +} + type t = { name : string; other_names : string list; typ : typ; - addr : int; + addr : Address.t; + (* addr : int; *) size : int; writable : bool; - data : BytesSeq.t; + data : data; } -type linksem_t = string * (Z.t * Z.t * Z.t * BytesSeq.t option * Z.t) +type linksem_t = LinksemRelocatable.symbol let push_name s t = { t with other_names = s :: t.other_names } -let is_in t addr = t.addr <= addr && addr < t.addr + t.size +(* let is_in t addr = t.addr <= addr && addr < t.addr + t.size *) let len t = t.size @@ -75,7 +85,7 @@ let typ_of_linksem ltyp = | 4 -> FILE | _ -> UNKNOWN -let linksem_typ (_name, (typ, _size, _addr, _data, _)) = typ +let linksem_typ (_name, (typ, _size, _addr, _data, _), _) = typ (** [LoadingError(name,addr)] means that symbol [name] at [addr] could not be loaded *) exception LoadingError of string * int @@ -86,26 +96,26 @@ let _ = Some (Printf.sprintf "Symbol %s at 0x%x could not be loaded" name addr) | _ -> None) -let of_linksem segs (name, (typ, size, addr, data, _)) = +(* for debugging TODO remove *) +(* module SMap = Map.Make (String) +let locs = SMap.empty |> SMap.add ".text" 0 |> SMap.add ".data" 1000000 |> SMap.add ".eh_frame" 2000000 *) + +let of_linksem (name, (typ, size, addr, (data, rels), _), writable) = let typ = typ_of_linksem typ in let size = Z.to_int size in - let addr = Z.to_int addr in - let segment = - Option.value_fail (Segment.get_containing segs addr) "No segment contains symbol %s" name - in - let writable = segment.write in - let data = - data - |> Option.value_fun ~default:(fun () -> - Segment.get_addr (BytesSeq.getbs ~len:size) segment addr) - in + let addr = Address.of_linksem addr in + let data = { data; relocations = Relocations.of_linksem rels } in + (* let addr = SMap.find section locs + Z.to_int offset in *) { name; other_names = []; typ; size; addr; data; writable } let is_interesting = function OBJECT | FUNC -> true | _ -> false let is_interesting_linksem lsym = lsym |> linksem_typ |> typ_of_linksem |> is_interesting -let sub sym off len = BytesSeq.sub sym.data off len +let sub sym off len = { + data = BytesSeq.sub sym.data.data off len; + relocations = Relocations.sub sym.data.relocations off len; +} let compare s1 s2 = compare s1.addr s2.addr @@ -128,8 +138,9 @@ let pp_raw sym = ("name", !^(sym.name)); ("other names", separate nbspace (List.map string sym.other_names)); ("typ", pp_typ sym.typ); - ("addr", ptr sym.addr); + ("addr", Address.pp sym.addr); + (* ("addr", ptr sym.addr); *) ("size", ptr sym.size); ("writable", bool sym.writable); - ("data", BytesSeq.ppby ~by:4 sym.data); + ("data", pair (BytesSeq.ppby ~by:4) Relocations.pp (sym.data.data, sym.data.relocations)); ]) diff --git a/src/elf/symbol.mli b/src/elf/symbol.mli index e557439f..3bc5803f 100644 --- a/src/elf/symbol.mli +++ b/src/elf/symbol.mli @@ -55,26 +55,32 @@ type typ = NOTYPE | OBJECT | FUNC | SECTION | FILE | UNKNOWN type linksem_typ = Z.t +type data = { + data: BytesSeq.t; + relocations: Relocations.t +} + (** The ELF symbol. This type guarantee the data exists contrary to linksem symbols (it may be all zeros though) *) type t = { name : string; other_names : string list; typ : typ; - addr : int; + addr : Address.t; + (* addr : int; *) size : int; writable : bool; - data : BytesSeq.t; + data : data; } (** The type of an ELF symbol in linksem. See {!of_linksem}*) -type linksem_t = string * (Z.t * Z.t * Z.t * BytesSeq.t option * Z.t) +type linksem_t = LinksemRelocatable.symbol (** Add a name to the other names list *) val push_name : string -> t -> t (** Check if an address is in a symbol *) -val is_in : t -> int -> bool +(* val is_in : t -> int -> bool *) (** For conformance with the {!Utils.RngMap.LenObject} module type *) val len : t -> int @@ -93,7 +99,7 @@ exception LoadingError of string * int May raise {!LoadingError} when the symbol has no data and the data cannot be found in the segments *) -val of_linksem : Segment.t list -> linksem_t -> t +val of_linksem : linksem_t -> t (** Tell if a symbol type is interesting for readDwarf purposes *) val is_interesting : typ -> bool @@ -102,7 +108,7 @@ val is_interesting : typ -> bool val is_interesting_linksem : linksem_t -> bool (** Take the BytesSeq.t corresponding to the offset and length *) -val sub : t -> int -> int -> BytesSeq.t +val sub : t -> int -> int -> data (** Starting address comparison *) val compare : t -> t -> int diff --git a/src/exp/sums.ml b/src/exp/sums.ml index 4d945032..287f4936 100644 --- a/src/exp/sums.ml +++ b/src/exp/sums.ml @@ -42,13 +42,17 @@ (* *) (*==================================================================================*) +open Logs.Logger (struct + let str = __MODULE__ +end) + (* The documentation is in the mli file *) let rec split = let open Ast in function | Manyop (Bvmanyarith Bvadd, l, _) -> List.concat_map split l - | Unop (Extract (last, first), e, _) -> + | Unop (Extract (last, (0 as first)), e, _) -> let l = split e in List.map (Typed.extract ~first ~last) l | Unop (Bvneg, e, _) -> @@ -88,6 +92,8 @@ let smart_substract ~equal ~term exp = let split_concrete exp = let size = Typed.expect_bv (Typed.get_type exp) in let terms = split exp in + debug "Split:"; + List.iter (fun t -> debug "\t%t" Pp.(top (PpExp.pp_exp (fun _ -> !^"var")) t)) terms; let (symterms, concvals) = List.partition_map ConcreteEval.eval_if_concrete terms in let concbvs = List.map Value.expect_bv concvals in let concbv = List.fold_left BitVec.( + ) (BitVec.zero ~size) concbvs in diff --git a/src/isla/base.ml b/src/isla/base.ml index 4cb88d85..94f4788b 100644 --- a/src/isla/base.ml +++ b/src/isla/base.ml @@ -97,6 +97,8 @@ type rsmt = lrng smt (** The type of raw expressions out of the parser *) type rexp = lrng exp +type rtrcs = lrng trcs + (*****************************************************************************) (*****************************************************************************) (*****************************************************************************) @@ -173,6 +175,24 @@ let parse_trc_string ?(filename = "default") (s : string) : rtrc = let parse_trc_channel ?(filename = "default") (c : in_channel) : rtrc = parse_trc ~filename @@ Lexing.from_channel ~with_positions:true c +let parse_trcs = parse Parser.trcs_start + +let parse_trcs_string ?filename (s : string) : rtrcs = + parse_trcs ?filename @@ Lexing.from_string ~with_positions:true s + +let parse_trcs_channel ?filename (c : in_channel) : rtrcs = + parse_trcs ?filename @@ Lexing.from_channel ~with_positions:true c + +let parse_segments ?filename l = match parse_trcs ?filename l with +| TracesWithSegments (s, []) -> s +| _ -> raise (ParseError (l.lex_start_p, "Data is not SEGMENTS")) + +let parse_segments_string ?filename (s : string) : instruction_segments = + parse_segments ?filename @@ Lexing.from_string ~with_positions:true s + +let parse_segments_channel ?filename (c : in_channel) : instruction_segments = + parse_segments ?filename @@ Lexing.from_channel ~with_positions:true c + (*$R try let exp = parse_exp_string ~filename:"test" "v42" in diff --git a/src/isla/cache.ml b/src/isla/cache.ml index 038bbdd6..1cf72492 100644 --- a/src/isla/cache.ml +++ b/src/isla/cache.ml @@ -77,68 +77,87 @@ type config = Server.config bit 0 to back -1 : The start of the data bit back -1: set *) module Opcode (*: Cache.Key *) = struct - type t = BytesSeq.t option + type t = Server.opcode option + + let reloc_id: Relocation.t option -> int = function + | None -> 0 + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.Data640) -> 1 + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.Data320) -> 2 + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.ADRP) -> 3 + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.ADD) -> 4 + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.CALL) -> 5 + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.LDST b) -> assert (b < 5); 6 + b + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.CONDBR) -> 11 + | Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.B) -> 12 + + let reloc_of_id: int -> Relocation.t option = function + | 0 -> None + | 1 -> Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.Data640) + | 2 -> Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.Data320) + | 3 -> Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.ADRP) + | 4 -> Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.ADD) + | 5 -> Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.CALL) + | x when x < 11 -> Some (Elf.Relocations.AArch64 (Abi_aarch64_symbolic_relocation.LDST (x-6))) + | 11 -> Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.CONDBR) + | 12 -> Some (Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.B) + | x -> fail "Invalid relocation id %d" x let equal a b = match (a, b) with | (None, None) -> true - | (Some bs, Some bs2) -> BytesSeq.equal bs bs2 + | (Some (bs, r1), Some (bs2, r2)) -> BytesSeq.equal bs bs2 && r1 = r2 | _ -> false + let small_enough bs rel_id = + BytesSeq.length bs < (BytesSeq.int_bytes-1) && rel_id < (8*256) + let hash = function | None -> 0 - | Some bs -> + | Some (bs, rel) -> let i = BytesSeq.getintle_ze bs 0 in let l = BytesSeq.length bs in - if l < BytesSeq.int_bytes then begin + let rel_id = reloc_id rel in + if small_enough bs rel_id then begin assert (not @@ IntBits.get i IntBits.back); let res = IntBits.blit l 0 i (IntBits.back - 3) 3 in + let res = IntBits.blit rel_id 0 res (IntBits.back - 14) 11 in res end else IntBits.set i IntBits.back - let to_file file = function + let to_file _file = function | None -> () - | Some bs -> - if BytesSeq.length bs < BytesSeq.int_bytes then () + | Some (bs, rel) -> + let rel_id = reloc_id rel in + if small_enough bs rel_id then () else - let keyfile = Utils.Cache.to_keyfile file in - Files.write_bin BytesSeq.output keyfile bs + Raise.todo() - let of_file hash file = + let of_file hash _file = if hash = 0 then None else if IntBits.get hash IntBits.back then - let keyfile = Utils.Cache.to_keyfile file in - Some (Files.read BytesSeq.input keyfile) + Raise.todo() else - let data = IntBits.sub hash 0 (IntBits.back - 3) in + let data = IntBits.sub hash 0 (IntBits.back - 14) in + let reloc_id = IntBits.sub hash (IntBits.back - 14) 11 in let size = IntBits.sub hash (IntBits.back - 3) 3 in let b = Bytes.create size in Bits.unsafe_blit_of_int data 0 b 0 (size * 8); - Some (BytesSeq.of_bytes b) + Some (BytesSeq.of_bytes b, reloc_of_id reloc_id) end (** Representation of trace lists on disk. It is just a list of traces separated by new lines *) module TraceList (*: Cache.Value *) = struct - type t = Base.rtrc list + type t = Base.rtrcs let to_file file (trcs : t) = - let output_trc ochannel trc = Pp.fprintln ochannel @@ Base.pp_trc trc in - let output_trcs = Files.output_list output_trc in - Files.write output_trcs file trcs + Files.write Pp.fprintln file (Base.pp_trcs trcs) let of_file file : t = - let num = ref 0 in - let input_trc ichannel = - let trc = Files.input_sexp ichannel in - let filename = Printf.sprintf "Trace %i of %s" !num file in - incr num; - Base.parse_trc_string ~filename trc - in - let input_trcs = Files.input_list input_trc in - Files.read input_trcs file + let filename = Printf.sprintf "Traces of %s" file in + Files.read Files.input_string file |> Base.parse_trcs_string ~filename end (** An epoch independant of the isla version, bump if you change the representation @@ -216,7 +235,7 @@ let get_cache () = match !cache with Some cache -> cache | None -> failwith "Isla cache was not started" (** Get the traces of the opcode given. Use {!Server} if the value is not in the cache *) -let get_traces (opcode : BytesSeq.t) : Base.rtrc list = +let get_traces (opcode : Server.opcode) : Base.rtrcs = let (cache, config) = get_cache () in match IC.get_opt cache (Some opcode) with | Some trcs -> trcs @@ -232,11 +251,13 @@ let get_traces (opcode : BytesSeq.t) : Base.rtrc list = let get_nop () : Base.rtrc = let (cache, _) = get_cache () in match IC.get_opt cache None with - | Some [trc] -> trc + | Some (Traces [trc]) -> trc + | Some (TracesWithSegments _) -> fatal "Corrupted cache, nop has segments" | Some _ -> fatal "Corrupted cache, nop hasn't exactly one trace" | None -> ensure_started (); - let trcs = Server.request_bin_parsed @@ Arch.nop () in + let (segs, trcs) = Server.request_bin_parsed @@ (Arch.nop (), None) in + assert (Option.is_none segs); let trc = List.assoc true trcs in - IC.add cache None [trc]; + IC.add cache None (Traces [trc]); trc diff --git a/src/isla/isla.ml b/src/isla/isla.ml index 5ed4bdf5..e61981e1 100644 --- a/src/isla/isla.ml +++ b/src/isla/isla.ml @@ -50,6 +50,7 @@ module Cache = Cache module Conv = Conv module Manip = Manip module Preprocess = Preprocess +module Relocation = Relocation module Run = Run module Server = Server module Test = Test diff --git a/src/isla/preprocess.ml b/src/isla/preprocess.ml index 0f187384..7aa0abd1 100644 --- a/src/isla/preprocess.ml +++ b/src/isla/preprocess.ml @@ -68,7 +68,7 @@ let expect_processed = function | _ -> Raise.fail "Variables should be processed at this point" (** Preprocess a single trace *) -let simplify_trc (Trace events : rtrc) : rtrc = +let simplify_trc ?(num_segments = 0) (Trace events : rtrc) : rtrc = (* Phase 1: Discover which variable are actually used *) let used = HashVector.empty () in let process_used event = @@ -90,7 +90,8 @@ let simplify_trc (Trace events : rtrc) : rtrc = not yet commited are inlined. Variables are also renumbered at the same time. *) let simplify_context = HashVector.empty () in - let new_variables = Counter.make 0 in + (* Segment variables should not be renamed (we assume that those are v0-v(num_segments-1)) *) + let new_variables = Counter.make num_segments in let res = ref [] in let push_event (d : revent) = res := d :: !res in let push_smt loc (d : rsmt) = push_event (Smt (d, loc)) in @@ -100,13 +101,13 @@ let simplify_trc (Trace events : rtrc) : rtrc = match HashVector.get simplify_context i with | Declared { ty; loc } -> debug "Commiting declared variable %d" i; - let new_val = Counter.get new_variables in + let new_val = if i < num_segments then i else Counter.get new_variables in HashVector.set simplify_context i (Processed new_val); push_smt loc (DeclareConst (new_val, ty)); new_val | Defined { exp; loc } -> debug "Commiting defined variable %d" i; - let new_val = Counter.get new_variables in + let new_val = if i < num_segments then i else Counter.get new_variables in HashVector.set simplify_context i (Processed new_val); debug "New id is %d" new_val; let new_exp = simplify_exp exp in @@ -157,12 +158,24 @@ let simplify_trc (Trace events : rtrc) : rtrc = (1 + Counter.read new_variables); Trace (List.rev !res) -let preprocess (config : Server.config) (trcs : (bool * rtrc) list) : rtrc list = +let preprocess (config : Server.config) ((segs, trcs) : Server.trcs) : rtrcs = + let num_segments = + segs + |> Option.map (fun (Segments s) -> + let x = List.length s in + assert (List.for_all (fun (Segment (_,_,v)) -> v < x) s); + x + ) + |> Option.value ~default:0 + in let preprocess_one (b, trc) = if not b then None else let trc = trc |> Manip.remove_init |> Manip.remove_ignored config.ignored_regs in - let trc = simplify_trc trc in + let trc = simplify_trc ~num_segments trc in Some trc in - List.filter_map preprocess_one trcs + let trcs = List.filter_map preprocess_one trcs in + match segs with + | None -> Traces (trcs) + | Some segs -> TracesWithSegments (segs, trcs) diff --git a/src/isla/preprocess.mli b/src/isla/preprocess.mli index b78fc41d..73c8a70f 100644 --- a/src/isla/preprocess.mli +++ b/src/isla/preprocess.mli @@ -67,9 +67,9 @@ *) (** Simplify a simple trace by removing all useless variables *) -val simplify_trc : Base.rtrc -> Base.rtrc +val simplify_trc : ?num_segments:int -> Base.rtrc -> Base.rtrc (** Preprocess a group of traces, by removing useless registers (according to the config), removing initialisation code and simplifying with {!simplify_trc} *) -val preprocess : Server.config -> Server.trcs -> Base.rtrc list +val preprocess : Server.config -> Server.trcs -> Base.rtrcs diff --git a/src/isla/relocation.ml b/src/isla/relocation.ml new file mode 100644 index 00000000..c73e231b --- /dev/null +++ b/src/isla/relocation.ml @@ -0,0 +1,53 @@ +open Logs.Logger (struct + let str = __MODULE__ +end) + +type t = Elf.Relocations.target + +type segment = string * (int * int) (* mapping the name of a segment to the range of the relocation value *) + +let pp_opcode_with_segments (b, r) = + match r with + | None -> Pp.(!^"#x" ^^ BytesSeq.ppint b) + | Some (Elf.Relocations.AArch64 rtype) -> + let bits = BytesSeq.getbvle ~size:32 b 0 in + Pp.( + match rtype with + | Abi_aarch64_symbolic_relocation.Data640 -> fatal "Data64 relocation not allowed for instruction" + | Abi_aarch64_symbolic_relocation.Data320 -> fatal "Data32 relocation not allowed for instruction" + | Abi_aarch64_symbolic_relocation.ADRP -> + BitVec.pp_smt (BitVec.extract 31 31 bits) + ^^ !^" x0:2 " ^^ + BitVec.pp_smt (BitVec.extract 24 28 bits) + ^^ !^" x1:19 " ^^ + BitVec.pp_smt (BitVec.extract 0 4 bits) + | Abi_aarch64_symbolic_relocation.ADD -> + BitVec.pp_smt (BitVec.extract 22 31 bits) + ^^ !^" x0:12 " ^^ + BitVec.pp_smt (BitVec.extract 0 9 bits) + | Abi_aarch64_symbolic_relocation.LDST b -> + BitVec.pp_smt (BitVec.extract (22-b) 31 bits) + ^^ !^" x0:" ^^ int (12-b) ^^ !^" " ^^ + BitVec.pp_smt (BitVec.extract 0 9 bits) + | Abi_aarch64_symbolic_relocation.CALL -> + BitVec.pp_smt (BitVec.extract 26 31 bits) + ^^ !^" x0:26 " + | Abi_aarch64_symbolic_relocation.CONDBR -> + BitVec.pp_smt (BitVec.extract 24 31 bits) + ^^ !^" x0:19 " + ^^ BitVec.pp_smt (BitVec.extract 0 4 bits) + | Abi_aarch64_symbolic_relocation.B -> + BitVec.pp_smt (BitVec.extract 26 31 bits) + ^^ !^" x0:26 " + ) + +(* for interpreting the segments *) +let segments_of_reloc: t -> segment list = function +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.Data640 -> fatal "invalid relocation for instructions (Data64)" +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.Data320 -> fatal "invalid relocation for instructions (Data32)" +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.ADRP -> ["x0", (0, 1); "x1", (2, 20)] +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.ADD -> ["x0", (0, 11)] +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.LDST b -> ["x0", (0, 11-b)] +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.CALL -> ["x0", (0, 25)] +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.CONDBR -> ["x0", (0, 18)] +| Elf.Relocations.AArch64 Abi_aarch64_symbolic_relocation.B -> ["x0", (0, 25)] diff --git a/src/isla/server.ml b/src/isla/server.ml index 0fff247d..e6f247ff 100644 --- a/src/isla/server.ml +++ b/src/isla/server.ml @@ -66,7 +66,10 @@ type config = Config.t It is a list of traces, each with a flag telling if they are normal traces (no processor exception/fault) or not *) -type trcs = (bool * Base.rtrc) list +type trcs = Base.instruction_segments option * (bool * Base.rtrc) list + +type opcode = BytesSeq.t * Relocation.t option + (** Bump when updating isla. TODO: move the version checking to allow a range of version. @@ -121,7 +124,7 @@ let raw_stop () = | None -> () (** This should match exactly with the Answer type in isla-client code *) -type basic_answer = Error | Version of string | StartTraces | Trace of bool * string | EndTraces +type basic_answer = Error | Version of string | StartTraces | Trace of bool * string | EndTraces | Segments of string (** Read an answer from isla-client. This must match exactly [write_answer] in [client.rs] in [isla] *) @@ -136,11 +139,12 @@ let read_basic_answer () = let s = Server.read_string serv in Trace (b, s) | 4 -> EndTraces + | 5 -> Segments (Server.read_string serv) | _ -> failwith "Unknown isla anwser" (** The interpreted answer. If the protocol is followed, then one request lead to exactly one answer of that type *) -type answer = Version of string | Traces of (bool * string) list +type answer = Version of string | Traces of (string option * (bool * string) list) (** Expect a version answer and fails if it is not the case *) let expect_version = function Version s -> s | _ -> failwith "expected version number from isla" @@ -150,11 +154,15 @@ let expect_traces = function Traces tl -> tl | _ -> failwith "expected traces fr (** Expect isla traces and fails if it is not the case, additionally parse them *) let expect_parsed_traces a : trcs = - a |> expect_traces - |> List.mapi (fun i (b, t) -> + let rsegs, rtrcs = expect_traces a in + let filename = Printf.sprintf "Isla call %d" !req_num in + let trcs = List.mapi (fun i (b, t) -> ( b, - let filename = Printf.sprintf "Isla call %d, trace %d" !req_num i in - Base.parse_trc_string ~filename t )) + let filename = filename ^ Printf.sprintf ", trace %d" i in + Base.parse_trc_string ~filename t )) rtrcs + in + let segs = Option.map (Base.parse_segments_string ~filename) rsegs in + segs, trcs (** When isla encounter a non fatal error with that specific request. This error is recoverable and the sever can accept other requests *) @@ -162,39 +170,47 @@ exception IslaError (** Read the answer from isla, block until full answer *) let read_answer () : answer = + let rec traces_seq () = + match read_basic_answer () with + | EndTraces -> Seq.Nil + | Trace (bool, s) -> Seq.Cons ((bool, s), traces_seq) + | Error -> raise IslaError + | _ -> failwith "isla protocol error: no EndTraces" + in match read_basic_answer () with | Error -> raise IslaError | Version s -> Version s + | Segments s -> ( + match read_basic_answer () with + | StartTraces -> Traces (Some s, List.of_seq traces_seq) + | _ -> failwith "segments not followed by traces" + ) | StartTraces -> - let rec seq () = - match read_basic_answer () with - | EndTraces -> Seq.Nil - | Trace (bool, s) -> Seq.Cons ((bool, s), seq) - | Error -> raise IslaError - | _ -> failwith "isla protocol error: no EndTraces" - in - Traces (List.of_seq seq) + Traces (None, List.of_seq traces_seq) | _ -> failwith "isla protocol error: Traces element before StartTraces" (** Answer pretty printer *) let pp_answer = function | Version s -> Pp.(prefix 2 1 !^"isla-client version:" !^s) - | Traces l -> - l - |> List.map (fun (b, t) -> - Pp.( - let bdoc = if b then !^"norm:" else !^"ex:" in - prefix 2 1 bdoc (string t))) - |> Pp.(separate (hardline ^^ hardline)) + | Traces (s, l) -> + Pp.( + optional string s + ^^ hardline + ^^ hardline + ^^ (l + |> List.map (fun (b, t) -> + let bdoc = if b then !^"norm:" else !^"ex:" in + prefix 2 1 bdoc (string t)) + |> separate (hardline ^^ hardline))) (** The type of a request to isla *) -type request = TEXT_ASM of string | ASM of BytesSeq.t | VERSION | STOP +type request = TEXT_ASM of string | ASM of opcode | VERSION | STOP (** Convert a request into the string message expected by isla-client This should match the protocol *) let string_of_request = function | TEXT_ASM s -> Printf.sprintf "execute_asm %s" s - | ASM b -> Pp.(sprintc @@ !^"execute " ^^ BytesSeq.ppint b) + | ASM b -> Pp.(sprintc @@ !^"execute " ^^ Relocation.pp_opcode_with_segments b) | VERSION -> "version" | STOP -> "stop" @@ -217,7 +233,7 @@ let request (req : request) : answer = req |> string_of_request |> string_reques This is the main entry point of this module. *) -let request_bin_parsed (bin : BytesSeq.t) : trcs = ASM bin |> request |> expect_parsed_traces +let request_bin_parsed (opcode : opcode) : trcs = ASM opcode |> request |> expect_parsed_traces (** Send a request without expecting any answer *) let send_request req = req |> string_of_request |> send_string_request diff --git a/src/isla/test.ml b/src/isla/test.ml index 29b011de..b7a06ad7 100644 --- a/src/isla/test.ml +++ b/src/isla/test.ml @@ -166,7 +166,7 @@ let input imode (arg : string) : (string * string) Term.ret = try Elf.SymTable.of_position_string elf.symbols s with Not_found -> fail "The position %s could not be found in %s" s arg in - `Ok (filename, BytesSeq.to_string (BytesSeq.sub sym.data off 4)) + `Ok (filename, BytesSeq.to_string (BytesSeq.sub sym.data.data off 4)) (* TODO relocations *) let input_term = Term.(ret (const input $ imode_term $ arg)) @@ -186,8 +186,8 @@ let isla_mode_term = let isla_mode_to_request imode input = match imode with | ASM -> Server.TEXT_ASM input - | HEX -> Server.ASM (BytesSeq.of_hex input) - | BIN -> Server.ASM (BytesSeq.of_string input) + | HEX -> Server.ASM (BytesSeq.of_hex input, None) (* TODO? *) + | BIN -> Server.ASM (BytesSeq.of_string input, None) | _ -> assert false (** Run isla and return a text trace with a filename @@ -204,7 +204,7 @@ let isla_run isla_mode arch (filename, input) : string * string * Server.config start config; let msg : string = match request (isla_mode_to_request isla_mode input) with - | Traces l -> List.assoc true l + | Traces (_, l) -> List.assoc true l (* TODO segments *) | _ -> failwith "isla did not send back traces" in stop (); diff --git a/src/relsim/dune b/src/relsim/dune new file mode 100644 index 00000000..2f6abe26 --- /dev/null +++ b/src/relsim/dune @@ -0,0 +1,6 @@ +(library + (name relsim) + (public_name read-dwarf.relsim) + (flags + (:standard -open Utils)) + (libraries utils ast state run z3)) \ No newline at end of file diff --git a/src/relsim/relsim.ml b/src/relsim/relsim.ml new file mode 100644 index 00000000..3146a1b4 --- /dev/null +++ b/src/relsim/relsim.ml @@ -0,0 +1,447 @@ +open Logs.Logger (struct + let str = __MODULE__ +end) + +open Cmdliner +open Config.CommonOpt + +module Sums = Exp.Sums +module Typed = Exp.Typed + +module Var = struct + type t = Left of State.var | Right of State.var + + let equal a b = match (a,b) with + | Left a, Left b -> State.Var.equal a b + | Right a, Right b -> State.Var.equal a b + | _ -> false + + let pp = function + | Left v -> Pp.(!^"L:" ^^ State.Var.pp v) + | Right v -> Pp.(!^"R:" ^^ State.Var.pp v) + + let ty = function Left v | Right v -> State.Var.ty v + + let hash = Hashtbl.hash + + let of_string s = + let v = State.Var.of_string @@ String.sub s 2 (String.length s - 2) in + match String.sub s 0 2 with + | "L:" -> Left v + | "R:" -> Right v + | _ -> Raise.inv_arg "Invalid variable: %s" s +end + +module Exp = struct + include Exp.Make (Var) + + let left : State.Exp.t -> t = Ast.Manip.exp_map_var (fun v -> Var.Left v) + + let right : State.Exp.t -> t = Ast.Manip.exp_map_var (fun v -> Var.Right v) +end + +module Z3sim = Z3.Make (Var) + +type sem_type = +| Value of int +| Ptr of sem_type + +type value_relation = +| Eq +| EqSection of string +| EqPage of string +| Indirect of sem_type + +let rec pp_sem_type = Pp.(function +| Value w -> !^"Val"^^(int w) +| Ptr typ -> (pp_sem_type typ)^^(!^"*") +) + +let pp_rel = Pp.(function +| Eq -> !^"Eq" +| EqSection s -> !^"EqSection " ^^ !^s +| EqPage s -> !^"EqPage " ^^ !^s +| Indirect typ -> !^"Indirect " ^^ (pp_sem_type typ) +) + +let rec sem_type_of_type (typ: Ctype.t) : sem_type = + match typ.unqualified with + | Ctype.Machine _ | Ctype.Cint _ | Ctype.Cbool | Ctype.Enum _ -> Value (Ctype.sizeof typ) + | Ptr { fragment=Ctype.DynArray typ'; _ } -> Ptr (sem_type_of_type typ') + | _ -> Raise.todo() + +let value_rel_for_type: Ctype.unqualified -> value_relation = function +| Ctype.Machine _ | Ctype.Cint _ | Ctype.Cbool | Ctype.Enum _ -> Eq +| Ptr { fragment=Ctype.Global s; _ } -> EqSection s +| Ptr { fragment=Ctype.DynFragment i; _ } -> EqSection ("Dyn_"^string_of_int i) +| Ptr { fragment=Ctype.DynArray typ'; _ } -> Indirect (sem_type_of_type typ') +| _ -> Raise.todo() + +exception SimulationFailure of string + +let fail_sim fmt = + let fail msg = raise(SimulationFailure msg) in + Printf.ksprintf fail fmt + +let pp_diff pre pp l r = + let open Pp in + surround 2 2 + pre + (!^"L: "^^pp l ^^ space ^^ !^"R: "^^pp r) + empty + +module ExpRel = struct + type t = State.exp * value_relation * State.exp + + let to_exp ((exp1, rel, exp2):t) = + let open Option in + let modify e = + match rel with + | Eq -> e |> some + | EqSection s -> Typed.(e - State.Exp.of_var (State.Var.Section s)) |> some + (* TODO this is probably wrong: *) + | EqPage s -> Typed.(e - concat [extract ~first:12 ~last:63 (State.Exp.of_var (State.Var.Section s)); bits_int ~size:12 0]) |> some + | Indirect _ -> None + in + let+ e1, e2 = lift_pair (modify exp1, modify exp2) in + Typed.((Exp.left e1) = (Exp.right e2)) + + let pp ((a, r, b):t) = + let open Pp in + pp_diff + (pp_rel r ^^ !^" between") + Exp.pp (Exp.left a) (Exp.right b) +end + +module RegRel = struct + type t = value_relation State.Reg.Map.t + + let special_regs = ["OSDLR_EL1"; "OSLSR_EL1"; "EDSCR"; "SCR_EL3"] + + let infer_from_types (s:State.t) = + State.Reg.Map.mapi (fun reg (r:State.Tval.t) -> + if List.exists ((=) (State.Reg.to_string reg)) special_regs then + Some Eq + else + Option.map (fun (r:Ctype.t) -> + value_rel_for_type r.unqualified + ) r.ctyp + ) s.regs + + let to_exp_rel (s1:State.t) (s2:State.t) reg_rel : ExpRel.t list = + let bindings = State.Reg.Map.bindings reg_rel in + List.filter_map (fun (reg, rel) -> + Option.map (fun rel -> + State.get_reg_exp s1 reg, rel, State.get_reg_exp s2 reg + ) rel + ) bindings +end + +module StackRel = struct + module RelMap = RngMap.Make (struct + type t = value_relation * int + let len (_, sz: t) = sz + end) + type t = RelMap.t + + type loc = { offset:int; size:int } + + module Event = State.Mem.Fragment.Event + + let loc_of_blocks (blk1:State.Mem.Fragment.Block.t) (blk2:State.Mem.Fragment.Block.t) = + if Option.is_some blk1.base || Option.is_some blk2.base then + Raise.todo(); + if blk1.offset != blk2.offset || blk1.size != blk2.size then + fail_sim "blocks don't match (%d, %t bytes) (%d, %t bytes)" + blk1.offset (Pp.tos Ast.Size.pp_bytes blk1.size) + blk2.offset (Pp.tos Ast.Size.pp_bytes blk2.size); + { offset=blk1.offset; size=Ast.Size.to_bytes blk1.size } + + let rel_at_loc stack loc = + let open Option in + let* ((rel, relsz), reloff) = RelMap.at_off_opt stack loc.offset in + if loc.size != relsz || reloff != 0 then + (warn "Size not matching"; None) + else + Some rel + + let clear_loc stack loc = + RelMap.clear stack ~pos:loc.offset ~len:loc.size + + let infer_from_types ~stack_frag (st1:State.t) = + let frag = Vec.get st1.fenv.frags stack_frag in + let stack = ref RelMap.empty in + State.Fragment.iteri (fun off ctype -> + stack := RelMap.add !stack off (value_rel_for_type ctype.unqualified, Ctype.len ctype) + ) frag; + !stack +end + +module GlobalRel = struct + type eq_pair = State.exp * State.exp * sem_type + + type t = eq_pair list + + let find ~hyps (rel:t) a1 a2 = + let check_one a1 a2 (a1', a2', typ) = + debug "%t %t %t %t" (Pp.top State.Exp.pp a1) (Pp.top State.Exp.pp a2) (Pp.top State.Exp.pp a1') (Pp.top State.Exp.pp a2'); + let equal = Z3sim.check_full ~hyps Typed.(manyop Ast.And [Exp.left a1= Exp.left a1'; Exp.right a2= Exp.right a2']) in + match equal with + | Some true -> Some typ + | _ -> None + in + List.find_map (check_one a1 a2) rel + + let add (rel:t) ((a1, a2, typ): eq_pair) = + (a1, a2, typ)::rel + + let check ~hyps (rel:t) ((a1, a2, typ): eq_pair) = + Option.map ((=) typ) (find ~hyps rel a1 a2) + + let rel_of_sem_type = function + | Ptr t -> Indirect t + | Value _ -> Eq +end + +let block_addr (blk : State.Mem.Fragment.Block.t) = + let ext = 64-Arch.address_size in + match blk.base with + | None -> Typed.bits_int ~size:64 blk.offset + | Some b -> Typed.(unop (Ast.ZeroExtend ext) b + bits_int ~size:64 blk.offset) + +let ptr_safety_asserts typ v = + let sz = match typ with + | Value x -> x + | Ptr _ -> 8 (*assume 64 bit pointers*) + in + let topbits = (64 - Arch.address_size) in + let small_enough = Typed.(extract ~first:Arch.address_size ~last:63 v = zero ~size:topbits) in + + let last = sz - 1 in + let aligned = Typed.(extract ~first:0 ~last v = zero ~size:sz) in + + [small_enough; aligned] + +module Context = struct + type t = { + asserts: Exp.t list; + stack: StackRel.t; + global: GlobalRel.t; + } + + module Event = State.Mem.Fragment.Event + + let add_expr_rel (ctxt:t) rel = + match rel with + | (v1, Indirect t, v2) -> + let safety1 = ptr_safety_asserts t v1 |> List.map Exp.left in + let safety2 = ptr_safety_asserts t v2 |> List.map Exp.right in + let nullptrs = Typed.((Exp.left v1 = zero ~size:64) = (Exp.right v2 = zero ~size:64)) in + { + asserts = safety1 @ safety2 @ nullptrs::ctxt.asserts; + global = GlobalRel.add ctxt.global (v1, v2, t); + stack = ctxt.stack; + } + | rel -> + let exp = Option.value_fail (ExpRel.to_exp rel) "Failed to convert relation to expression" in + { ctxt with asserts = exp::ctxt.asserts } + + let check_expr_rel (ctxt:t) rel = + match rel with + | (v1, Indirect t, v2) -> + GlobalRel.check ~hyps:ctxt.asserts ctxt.global (v1, v2, t) + | rel -> + let exp = Option.value_fail (ExpRel.to_exp rel) "Failed to convert relation to expression" in + Z3sim.check_full ~hyps:ctxt.asserts exp + + let process_stack_operation event1 event2 (ctxt: t) = + match event1, event2 with + | Event.Read (blk1, v1), Event.Read (blk2, v2) -> + let loc = StackRel.loc_of_blocks blk1 blk2 in + let rel = StackRel.rel_at_loc ctxt.stack loc in + ( match rel with + | Some rel -> add_expr_rel ctxt (State.Exp.of_var v1, rel, State.Exp.of_var v2) + | None -> (debug "No relation for stack read %t %t" (Pp.top Event.pp event1) (Pp.top Event.pp event2); ctxt) + ) + | Event.Write (blk1, _exp1), Event.Write (blk2, _exp2) -> + let loc = StackRel.loc_of_blocks blk1 blk2 in + { ctxt with stack = StackRel.clear_loc ctxt.stack loc} + | _ -> fail_sim "traces don't match %t %t" (Pp.tos Event.pp event1) (Pp.tos Event.pp event2) + + let process_global_operation event1 event2 (ctxt: t) = + match event1, event2 with + | Event.Read (blk1, v1), Event.Read (blk2, v2) -> + let addr1 = block_addr blk1 in + let addr2 = block_addr blk2 in + let typ = GlobalRel.find ~hyps:ctxt.asserts ctxt.global addr1 addr2 in + ( match typ with + | Some typ -> + let rel = GlobalRel.rel_of_sem_type typ in + add_expr_rel ctxt (State.Exp.of_var v1, rel, State.Exp.of_var v2) + | None -> (warn "No relation for global read %t %t" (Pp.top Event.pp event1) (Pp.top Event.pp event2); ctxt) + ) + | Event.Write (blk1, exp1), Event.Write (blk2, exp2) -> + let addr1 = block_addr blk1 in + let addr2 = block_addr blk2 in + let typ = GlobalRel.find ~hyps:ctxt.asserts ctxt.global addr1 addr2 in + ( match typ with + | Some typ -> + let rel = GlobalRel.rel_of_sem_type typ in + if check_expr_rel ctxt (exp1, rel, exp2) <> Some true then + fail_sim "Unable to verify %t" (Pp.tos ExpRel.pp (exp1, rel, exp2)) + | None -> fail_sim "Unable to determine target type for global write %t %t" (Pp.tos Event.pp event1) (Pp.tos Event.pp event2) + ); + ctxt + | _ -> fail_sim "traces don't match %t %t" (Pp.tos Event.pp event1) (Pp.tos Event.pp event2) + + let infer_from_types ~stack_frag ~(dwarf:Dw.t) (state: State.t) = + let stack = StackRel.infer_from_types state ~stack_frag in + + let regs = RegRel.infer_from_types state in + let register_rels = RegRel.to_exp_rel state state regs in + + let global_variable_rels = + Hashtbl.to_seq_values dwarf.vars + |> Seq.map (fun (v:Dw.Var.t) -> + let typ = sem_type_of_type v.ctype in + match v.locs with + | [_, Global addr] -> + let addr = Elf.SymTable.to_addr_offset addr in + let exp = State.Exp.of_address ~size:64 addr in + (exp, Indirect typ, exp) + | _ -> + Raise.fail "Weird location description for global variable: %t" (Pp.tos Dw.Var.pp_raw v); + ) + |> List.of_seq + in + + let ctxt = { stack; asserts=[]; global=[] } in + List.fold_left add_expr_rel ctxt (register_rels @ global_variable_rels) +end + +type simrel = (State.Id.t*State.Id.t, Context.t) Hashtbl.t + +let stack_prov = 0(* TODO determine stack_frag automatically *) +let stack_frag = 0(* TODO determine stack_frag automatically *) + +exception SimulationFailureWithContext of { + msg:string; + states: State.t * State.t; + ctxt: Context.t; +} + +let rec checksim ~(rel:simrel) (s1:State.t) (s2:State.t) = + Hashtbl.find_opt rel (s1.id, s2.id) + |> Option.value_fun ~default:(fun() -> + let bs1 = Option.value_fail s1.base_state "no base state" in + let bs2 = Option.value_fail s2.base_state "no base state" in + let prev_ctxt = checksim ~rel bs1 bs2 in + try + + (* Process stack trace *) + let ((_,mem1), (_,mem2)) = State.Mem.(get_frag s1.mem stack_prov, get_frag s2.mem stack_prov) in + let (trc1, trc2) = State.Mem.Fragment.(get_trace mem1, get_trace mem2) in + + let ctxt = List.fold_right2 Context.process_stack_operation trc1 trc2 prev_ctxt in + + (* Process global trace *) + let (mem1, mem2) = State.Mem.(get_main s1.mem, get_main s2.mem) in + let (trc1, trc2) = State.Mem.Fragment.(get_trace mem1, get_trace mem2) in + + let ctxt = List.fold_right2 Context.process_global_operation trc1 trc2 ctxt in + + + let asst1 = List.map Exp.left s1.asserts in + let asst2 = List.map Exp.right s2.asserts in + let impl1 = List.find_all Fun.(Z3sim.check_full ~hyps:(asst1@ctxt.asserts) %> flip Option.value_fail "TODO: Z3 failed" %> not) asst2 in + let impl2 = List.find_all Fun.(Z3sim.check_full ~hyps:(asst2@ctxt.asserts) %> flip Option.value_fail "TODO: Z3 failed" %> not) asst1 in + if not (List.is_empty impl1 && List.is_empty impl2) then + fail_sim "%t" Pp.(Fun.const @@ sprint @@ pp_diff + !^"States not equivalent on path conditions" + (list Exp.pp) + impl2 + impl1 + ); + + Hashtbl.add rel (s1.id, s2.id) ctxt; + ctxt + with + | SimulationFailure s -> raise @@ SimulationFailureWithContext { + msg=s; + states=(s1,s2); + ctxt=prev_ctxt; + } + ) + +let check_return_values ~(ret_reg) ~(ret_type:Ctype.t) ~(rel:simrel) (s1:State.t) (s2:State.t) = + let ctxt = Hashtbl.find rel (s1.id, s2.id) in + + let ret_val1 = State.get_reg_exp s1 ret_reg in + let ret_val2 = State.get_reg_exp s2 ret_reg in + let rel = value_rel_for_type ret_type.unqualified in + + if Context.check_expr_rel ctxt (ret_val1, rel, ret_val2) <> Some true then + raise @@ SimulationFailureWithContext { + msg=Printf.sprintf "Return values not equivalent +Condition: %t\n" (Pp.tos ExpRel.pp (ret_val1, rel, ret_val2)); + states=(s1,s2); + ctxt=ctxt; + } + + +let run elf name = + let dwarf = Dw.of_file elf in + let tree = Run.Func.get_state_tree ~elf ~name () in + let initial_state = tree.state in + + let initial_ctxt = Context.infer_from_types ~stack_frag ~dwarf initial_state in + + let simrel:simrel = Hashtbl.create 10 in + Hashtbl.add simrel (initial_state.id, initial_state.id) initial_ctxt; + + debug "%t" (Pp.top (State.Tree.pp_all Run.Block_lib.pp_label) tree); + + let ret = Option.( + let* func =Dw.get_func_opt ~name dwarf in + let+ typ = func.func.ret in + if Ctype.sizeof typ > 8 then + Raise.fail "unsupported return type %t" (Pp.tos Ctype.pp typ) + else + ((Arch.dwarf_reg_map()).(0), typ) + ) in + + try + State.Tree.prefix_iter (fun _ s -> + checksim ~rel:simrel s s |> ignore; + if State.get_reg_exp s (Arch.pc()) = State.Exp.of_var State.Var.RetAddr then + Option.iter (fun (ret_reg, ret_type) -> + check_return_values ~ret_reg ~ret_type ~rel:simrel s s; + ) ret + ) tree; + base "Simulation successful" + with + | SimulationFailureWithContext e -> + let st, _ = e.states in + debug "Failing state: %t" (Pp.top State.pp st); + base "Simulation failed:\n\n%s" e.msg + +let elf = + let doc = "ELF file from which to pull the code" in + Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"ELF_FILE" ~doc) + +let func = + let doc = "Symbol name of the function to run" in + Arg.(value & pos 1 string "main" & info [] ~docv:"FUNCTION" ~doc) + +let term = + Term.( + CmdlinerHelper.func_options comopts run + $ elf $ func) + +let info = + let doc = + "Simulation relation on relocatable binary" + in + Cmd.(info "relsim" ~doc ~exits) + +let command = (term, info) diff --git a/src/run/BB.ml b/src/run/BB.ml index 0e3cab82..cdddee56 100644 --- a/src/run/BB.ml +++ b/src/run/BB.ml @@ -101,7 +101,7 @@ let get_code elfname symname len : BytesSeq.t = with Not_found -> fail "The symbol %s cannot found in %s" symname elfname in let len = match len with Some i -> i | None -> sym.size - off in - Elf.Symbol.sub sym off len + (Elf.Symbol.sub sym off len).data (*TODO relocations*) let code_term = Term.(CmdlinerHelper.func_options comopts get_code $ elf $ sym $ len) diff --git a/src/run/bb_lib.ml b/src/run/bb_lib.ml index 083d07eb..6790fe1a 100644 --- a/src/run/bb_lib.ml +++ b/src/run/bb_lib.ml @@ -64,8 +64,9 @@ type t = { main : trc array } Also does the typing of traces for register discovery. TODO Support variable length instructions *) -let from_binary (code : BytesSeq.t) : t = - let num = BytesSeq.length code / 4 in +let from_binary (_code : BytesSeq.t) : t = + Raise.todo() + (* let num = BytesSeq.length code / 4 in (* TODO fix fixed size instructions *) if BytesSeq.length code != num * 4 then failwith "BB.from_binary: The specified range cuts an instruction"; @@ -80,10 +81,10 @@ let from_binary (code : BytesSeq.t) : t = "BB.from_binary: Multiple path instruction.\n\ If this is not a branching instruction, try `run-block --linear'." in - code |> Isla.Cache.get_traces |> get_normal + (code, None) |> Isla.Cache.get_traces |> get_normal (*TODO relocs *) in let main = code |> BytesSeq.to_listbs ~len:4 |> List.map process |> Array.of_list in - { main } + { main } *) (* Sequence of the second test: mpool.c:116.6 (mpool_fini) 40012240: 37000049 tbnz diff --git a/src/run/block.ml b/src/run/block.ml index 89d0c0e0..ed9f8ddb 100644 --- a/src/run/block.ml +++ b/src/run/block.ml @@ -109,7 +109,7 @@ let gen_block ((elf : Elf.File.t), (symoffset : Elf.SymTable.sym_offset)) len br let open Option in unlift_pair @@ let+ l = len in - (start, start + l) + (start, Elf.Address.(start + l)) in let endpred = Block_lib.gen_endpred ?min ?max ~brks () in Trace.Cache.start @@ Arch.get_isla_config (); diff --git a/src/run/block_lib.ml b/src/run/block_lib.ml index 25e5c528..3b62215f 100644 --- a/src/run/block_lib.ml +++ b/src/run/block_lib.ml @@ -56,7 +56,7 @@ open Logs.Logger (struct end) (** [endpred pc_exp] gives when to stop *) -type t = { runner : Runner.t; start : int; endpred : State.exp -> string option } +type t = { runner : Runner.t; start : Elf.Address.t; endpred : State.exp -> string option } (** Build a complex block starting from [start] in [sym] and ending when [endpred] says so. [endpred] is a predicate on the symbolic PC expression *) @@ -67,14 +67,14 @@ type label = | Start (** Root node of the tree *) | End of string (** Lead node of the tree, the string describe which end condition has be triggered *) - | BranchAt of int (** A Branching node at a given PC *) - | NormalAt of int (** A normal instruction at PC. Exists only if [every_instruction] is true *) + | BranchAt of Elf.Address.t (** A Branching node at a given PC *) + | NormalAt of Elf.Address.t (** A normal instruction at PC. Exists only if [every_instruction] is true *) let label_to_string = function | Start -> "Start" | End s -> Printf.sprintf "End (%s)" s - | BranchAt pc -> Printf.sprintf "Branch at 0x%x" pc - | NormalAt pc -> Printf.sprintf "Normal at 0x%x" pc + | BranchAt pc -> Printf.sprintf "Branch at %t" Pp.(tos Elf.Address.pp pc) + | NormalAt pc -> Printf.sprintf "Normal at %t" Pp.(tos Elf.Address.pp pc) let pp_label label = label |> label_to_string |> Pp.string @@ -93,24 +93,25 @@ let run ?(every_instruction = false) ?relevant (b : t) (start : State.t) : label assert (State.is_locked start); let rec run_from state = let pc_exp = State.get_reg_exp state pcreg in + State.Simplify.ctxfull state; if State.is_possible state then match b.endpred pc_exp with | Some endmsg -> info "Stopped at pc %t because %s" (Pp.top State.Exp.pp pc_exp) endmsg; - State.Simplify.ctxfull state; + (* State.Simplify.ctxfull state; *) State.lock state; State.Tree.{ state; data = End endmsg; rest = [] } | None -> ( - let prelock state = State.Simplify.ctxfull state in + (* let prelock state = State.Simplify.ctxfull state in *) if every_instruction then begin - prelock state; + (* prelock state; *) State.lock state end; let states = - let pc = pc_exp |> Ast.expect_bits |> BitVec.to_int in + let pc = State.Exp.expect_sym_address pc_exp in if Option.fold ~none:true ~some:(Fun.flip Hashtbl.mem pc) relevant then ( info "Running pc %t" (Pp.top State.Exp.pp pc_exp); - Runner.run ~prelock b.runner state + Runner.run ~prelock:ignore b.runner state ) else ( info "Skipping pc %t" (Pp.top State.Exp.pp pc_exp); @@ -123,21 +124,21 @@ let run ?(every_instruction = false) ?relevant (b : t) (start : State.t) : label | [state] when not every_instruction -> run_from state | [nstate] when every_instruction -> let rest = [run_from nstate] in - { state; data = NormalAt (pc_exp |> Ast.expect_bits |> BitVec.to_int); rest } + { state; data = NormalAt (State.Exp.expect_sym_address pc_exp); rest } | states -> let rest = List.map run_from states in State.Tree. - { state; data = BranchAt (pc_exp |> Ast.expect_bits |> BitVec.to_int); rest } + { state; data = BranchAt (State.Exp.expect_sym_address pc_exp); rest } ) else begin info "Reached dead code at %t" (Pp.top State.Exp.pp pc_exp); - State.Simplify.ctxfull state; + (* State.Simplify.ctxfull state; *) State.lock state; State.Tree.{ state; data = End "Reached dead code"; rest = [] } end in let state = State.copy start in - State.set_pc ~pc:pcreg state b.start; + State.set_pc_sym ~pc:pcreg state b.start; let rest = [run_from state] in State.Tree.{ state = start; data = Start; rest } @@ -158,21 +159,23 @@ let gen_endpred ?min ?max ?loop ?(brks = []) () : State.exp -> string option = | Some n -> Printf.sprintf "%d times" n | None -> "" in - function - | Ast.Bits (bv, _) -> ( - let pc = BitVec.to_int bv in - debug "enpred: Evaluating PC 0x%x" pc; + fun pc_exp -> + ( try + Some (State.Exp.expect_sym_address pc_exp) + with + _ -> None + ) |> Option.map (fun pc -> + debug "enpred: Evaluating PC %t" (Pp.top Elf.Address.pp pc); match (min, max, loop) with - | (Some min, _, _) when pc < min -> endnow "PC 0x%x was below min 0x%x" pc min - | (_, Some max, _) when pc >= max -> endnow "PC 0x%x was above max 0x%x" pc max - | _ when List.exists (( = ) pc) brks -> endnow "PC 0x%x hit a breakpoint" pc + | (Some min, _, _) when Elf.Address.(pc < min) <> Some false -> endnow "PC %t was below min %t" Pp.(tos Elf.Address.pp pc) Pp.(tos Elf.Address.pp min) + | (_, Some max, _) when Elf.Address.(pc >= max) <> Some false -> endnow "PC %t was above max %t" Pp.(tos Elf.Address.pp pc) Pp.(tos Elf.Address.pp max) + | _ when List.exists (( = ) pc) brks -> endnow "PC %t hit a breakpoint" Pp.(tos Elf.Address.pp pc) | (_, _, Some loop) -> let current_num = Hashtbl.find_opt pchtbl pc |> Option.value ~default:0 in - if current_num >= loop then endnow "PC 0x%x had been seen more than %s" pc loop_str + if current_num >= loop then endnow "PC %t had been seen more than %s" Pp.(tos Elf.Address.pp pc) loop_str else begin Hashtbl.replace pchtbl pc (current_num + 1); None end | _ -> None - ) - | exp -> endnow "PC %t is symbolic" Pp.(tos State.Exp.pp exp) + ) |> Option.value_fun ~default:(fun () -> endnow "PC %t is symbolic" Pp.(tos State.Exp.pp pc_exp)) diff --git a/src/run/func.ml b/src/run/func.ml index 3afdb1d5..08ac6c2b 100644 --- a/src/run/func.ml +++ b/src/run/func.ml @@ -46,13 +46,13 @@ open Cmdliner open Config.CommonOpt -open Fun +(* open Fun *) open Logs.Logger (struct let str = __MODULE__ end) -let no_run_prep ~elf:elfname ~name ~entry = +let no_run_prep ~elf:elfname ~name ~entry ?(init = State.init_sections_symbolic ~sp:Arch.sp ~addr_size:Arch.address_size) () = base "Running %s in %s" name elfname; let dwarf = Dw.of_file elfname in let elf = dwarf.elf in @@ -66,26 +66,31 @@ let no_run_prep ~elf:elfname ~name ~entry = let abi = Arch.get_abi api in Trace.Cache.start @@ Arch.get_isla_config (); base "Computing entry state"; - let start = Init.state () |> State.copy ~elf |> abi.init in + let start = Init.state () |> State.copy ~elf |> abi.init |> init in if entry then base "Entry state:\n%t" (Pp.topi State.pp start); (dwarf, elf, func, start) let get_state_tree ~elf:elfname ~name ?(dump = false) ?(entry = false) ?len ?(breakpoints = []) - ?loop ?tree_to_file () = - let (dwarf, elf, func, start) = no_run_prep ~elf:elfname ~name ~entry in + ?loop ?tree_to_file ?init ?every_instruction () = + let (dwarf, elf, func, start) = no_run_prep ~elf:elfname ~name ~entry ?init () in match func.sym with | None -> fail "Function %s exists in DWARF data but does not have any code" name | Some sym -> let brks = List.map - (Elf.SymTable.of_position_string elf.symbols %> Elf.SymTable.to_addr_offset) + (fun x -> + if String.starts_with ~prefix:"UND" x then (*HACK for undefined symbol*) + Elf.Address.{ section=x; offset=0 } + else + x |> Elf.SymTable.of_position_string elf.symbols |> Elf.SymTable.to_addr_offset + ) breakpoints in let (min, max) = let open Option in unlift_pair @@ let+ l = len in - (sym.addr, sym.addr + l) + (sym.addr, Elf.Address.(sym.addr + l)) in let endpred = Block_lib.gen_endpred ?min ?max ?loop ~brks () in let runner = Runner.of_dwarf dwarf in @@ -96,7 +101,7 @@ let get_state_tree ~elf:elfname ~name ?(dump = false) ?(entry = false) ?len ?(br base "Instructions:\n%t\n" (Pp.topi Runner.pp_instr runner) end; base "Start running"; - let tree = Block_lib.run block start in + let tree = Block_lib.run block start ?every_instruction in tree_to_file |> Option.iter (fun x -> Files.write_string x @@ Pp.tos (State.Tree.pp_all Block_lib.pp_label) tree ()); @@ -104,7 +109,7 @@ let get_state_tree ~elf:elfname ~name ?(dump = false) ?(entry = false) ?len ?(br tree let cmd_func elfname name dump no_run entry len breakpoints loop tree_to_file = - if no_run then ignore @@ no_run_prep ~elf:elfname ~name ~entry + if no_run then ignore @@ no_run_prep ~elf:elfname ~name ~entry () else ignore @@ get_state_tree ~elf:elfname ~name ~dump ~entry ?len ~breakpoints ?loop ?tree_to_file () diff --git a/src/run/func.mli b/src/run/func.mli index 7f72d3f5..eac27b23 100644 --- a/src/run/func.mli +++ b/src/run/func.mli @@ -7,6 +7,8 @@ val get_state_tree : ?breakpoints:string list -> ?loop:int -> ?tree_to_file:string -> + ?init:(State.t -> State.t) -> + ?every_instruction:bool -> unit -> Block_lib.label State.Tree.t diff --git a/src/run/funcRD.ml b/src/run/funcRD.ml index 9e1dc449..052b50b9 100644 --- a/src/run/funcRD.ml +++ b/src/run/funcRD.ml @@ -56,6 +56,10 @@ open Logs.Logger (struct end) let run_func_rd elfname name objdump_d branchtables breakpoints = + match Analyse.Utils.read_file_lines "src/analyse/html-preamble-insts.html" with + | Error _ -> () + | Ok lines -> Array.iter (function s -> Printf.printf "%s\n" s) lines + ; base "Running with rd %s in %s" name elfname; base "Loading %s" elfname; let dwarf = Dw.of_file elfname in @@ -70,13 +74,13 @@ let run_func_rd elfname name objdump_d branchtables breakpoints = let abi = Arch.get_abi api in Trace.Cache.start @@ Arch.get_isla_config (); base "Computing entry state"; - let start = Init.state () |> State.copy ~elf |> abi.init in + let start = Init.state () |> State.copy ~elf |> abi.init |> State.init_sections ~sp:Arch.sp ~addr_size:Arch.address_size in base "Loading %s for Analyse" elfname; let analyse_test = Analyse.Elf.parse_elf_file elfname in base "Analysing %s for Analyse" elfname; let analyse_analysis = Analyse.Collected.mk_analysis analyse_test objdump_d branchtables in let print_analyse_instruction pc = - let pc = Z.of_int pc in + let pc = Elf.Address.to_sym pc in let index = analyse_analysis.index_of_address pc in let instr = analyse_analysis.instructions.(index) in Analyse.Pp.pp_instruction Analyse.Types.Html (*Ascii*) analyse_test analyse_analysis 0 index @@ -98,7 +102,7 @@ let run_func_rd elfname name objdump_d branchtables breakpoints = let tree = Block_lib.run ~every_instruction:true block start in base "Ended running, start pretty printing"; (* This table will contain the state diff to print at each pc with a message *) - let instr_data : (int, string * State.t * State.Reg.t list) Hashtbl.t = + let instr_data : (Elf.Address.t, string * State.t * State.Reg.t list) Hashtbl.t = Hashtbl.create 100 in let get_footprint pc = @@ -113,7 +117,7 @@ let run_func_rd elfname name objdump_d branchtables breakpoints = let last_pc = st.last_pc in let last_instr_f = get_footprint last_pc in let s = - if last_pc <> pc - 4 then Printf.sprintf "Coming from 0x%x: " last_pc else "" + if Elf.Address.(last_pc + 4 <> pc) then Printf.sprintf "Coming from %t: " Pp.(tos Elf.Address.pp last_pc) else "" in let regs = List.merge_uniq Stdlib.compare cur_instr_f last_instr_f in Hashtbl.add instr_data pc (Printf.sprintf "%sBefore branch" s, st, regs) @@ -122,27 +126,31 @@ let run_func_rd elfname name objdump_d branchtables breakpoints = let last_pc = st.last_pc in let last_instr_f = get_footprint last_pc in let s = - if last_pc <> pc - 4 then Printf.sprintf "Coming from 0x%x: " last_pc else "" + if Elf.Address.(last_pc + 4 <> pc) then Printf.sprintf "Coming from %t: " Pp.(tos Elf.Address.pp last_pc) else "" in let regs = List.merge_uniq Stdlib.compare cur_instr_f last_instr_f in Hashtbl.add instr_data pc (Printf.sprintf "%sNormal instruction" s, st, regs) | Block_lib.End s -> let last_pc = st.last_pc in let last_instr = Runner.expect_normal runner last_pc in - Hashtbl.add instr_data (st.last_pc + 4) + Hashtbl.add instr_data Elf.Address.(st.last_pc + 4) (Printf.sprintf "End because: %s" s, st, Trace.Instr.footprint last_instr)) tree; Vec.iter (fun funcaddr -> let sym = Elf.SymTable.of_addr elf.symbols funcaddr in Analyse.Pp.pp_instruction_init (); - Seq.iota_step_up ~start:funcaddr ~step:4 ~endi:(funcaddr + sym.size) - |> Seq.iter (fun pc -> + Seq.iota_step_up ~start:0 ~step:4 ~endi:sym.size + |> Seq.iter (fun pc_diff -> + let pc = Elf.Address.(funcaddr + pc_diff) in Hashtbl.find_all instr_data pc |> List.iter (fun (msg, st, regs) -> - base "At 0x%x, %s:\n%t" pc msg Pp.(topi (State.pp_partial ~regs) st)); + base "At %t, %s:\n%t" Pp.(top Elf.Address.pp pc) msg Pp.(topi (State.pp_partial ~regs) st)); print_string (print_analyse_instruction pc))) - runner.funcs + runner.funcs; + match Analyse.Utils.read_file_lines "src/analyse/html-postamble.html" with + | Error _ -> () + | Ok lines -> Array.iter (function s -> Printf.printf "%s\n" s) lines let elf = let doc = "ELF file from which to pull the code" in diff --git a/src/run/instr.ml b/src/run/instr.ml index 07a8dab8..0098d35b 100644 --- a/src/run/instr.ml +++ b/src/run/instr.ml @@ -140,7 +140,7 @@ let get_instr arch instr elfopt : BytesSeq.t = in debug "Got symbol:\n%t\n" (Pp.topi Elf.Symbol.pp_raw sym); let len = 4 (* TODO proper Instruction length system *) in - BytesSeq.sub sym.data off len + BytesSeq.sub sym.data.data off len (*TODO relocations*) let instr_term = Term.(CmdlinerHelper.func_options comopts get_instr $ arch $ instr $ elf) @@ -148,14 +148,15 @@ let simp_trace_term = Term.(const ( || ) $ simp_trace $ simp) let simp_state_term = Term.(const ( || ) $ simp_state $ simp) -let get_traces instr isla_run dump_types : traces = - Isla.Cache.start @@ Arch.get_isla_config (); +let get_traces _instr _isla_run _dump_types : traces = + Raise.todo() + (* Isla.Cache.start @@ Arch.get_isla_config (); (* I call Init.init manually to print the register types *) Init.init () |> ignore; - let rtraces = Isla.Cache.get_traces instr in + let rtraces = Isla.Cache.get_traces (instr, None) in (* TODO relocs *) List.iter (fun t -> Isla.Type.type_trc t |> ignore) rtraces; if dump_types then base "Register types:\n%t\n" (Pp.topi State.Reg.pp_index ()); - if isla_run then IslaTraces rtraces else Traces (List.map Trace.of_isla rtraces) + if isla_run then IslaTraces rtraces else Traces (List.map Trace.of_isla rtraces) *) let pre_traces_term = Term.(const get_traces $ instr_term $ isla_run $ reg_types) diff --git a/src/run/relProg.ml b/src/run/relProg.ml new file mode 100644 index 00000000..f4a0f354 --- /dev/null +++ b/src/run/relProg.ml @@ -0,0 +1,229 @@ +open Cmdliner +open Config.CommonOpt + +open Logs.Logger (struct + let str = __MODULE__ +end) + +let rec pp_array pp sz dims value = + match dims with + | [] -> pp value + | None::_ -> pp value + | Some d :: dims -> + let sz = sz / d in + Seq.iota d + |> Seq.map (fun x -> Exp.Typed.extract ~first:(8*x*sz) ~last:(8*(x+1)*sz-1) value) + |> List.of_seq + |> Pp.list (pp_array pp sz dims) + +let pp_typed ~(tenv: Ctype.env) ~(ctype: Ctype.t) ~(pp : ?hex:bool -> _ -> _) (value: State.Exp.t) = + match ctype.unqualified with + | Machine _ -> pp value + | Cint _ -> pp value + | Cbool -> pp value + | Ptr _ -> pp ~hex:true value + | Struct { id; _ } -> + let s = IdMap.geti tenv.structs id in + Pp.( + Ctype.FieldMap.to_seq s.layout + |> Seq.map (fun (offset, (field:Ctype.field)) -> ( + Option.value ~default:"?" field.fname, + pp (Exp.Typed.extract ~first:(8*offset) ~last:(8*(offset + field.size)-1) value) + )) + |> List.of_seq + |> record s.name + ) + | Array { dims; _ } -> + let sz = Ctype.sizeof ctype in + pp_array pp sz dims value + | Enum _ -> pp value + | FuncPtr -> pp value + | Missing -> pp value + | Bits -> pp value + +let read_big ~prov st addr sz = + let addr = Exp.Typed.extract ~last:(Arch.address_size-1) ~first:0 addr in + Seq.iota_step_up ~step:16 ~endi:sz + |> Seq.map (fun off -> + let addr = Exp.Typed.(addr + bits_int ~size:Arch.address_size off) in + let len = min 16 (sz - off) in + match prov with + | None -> State.read_noprov st ~addr ~size:(Ast.Size.of_bytes len) + | Some p -> State.read ~provenance:p st ~addr:addr ~size:(Ast.Size.of_bytes len) + ) + |> List.of_seq + |> Exp.Typed.concat + +let eval_loc ?frame_value sz st (loc: Dw.Loc.t) : State.Exp.t option = + match loc with + | Register reg -> Some (State.get_reg_exp st reg) + | RegisterOffset (reg, off) -> + let r = State.get_reg st reg in + let open Ctype in + let prov = Option.bind r.ctyp (fun ctype -> + match ctype.unqualified with + | Ptr { provenance; _ } -> Some provenance + | _ -> None + ) in + Some (read_big ~prov st Exp.Typed.(r.exp + bits_int ~size:64 off) sz) + | StackFrame off -> + (* This is a bit hacky, should instead extract the provenance from frame_value *) + let stack_provenance = Option.bind (State.get_reg st (Arch.sp())).ctyp (fun ctype -> + match ctype.unqualified with + | Ptr { provenance; _ } -> Some provenance + | _ -> None + ) in + + let open Option in + let+ frame_value = frame_value in + debug "Reading from %t" Pp.(top State.Exp.pp Exp.Typed.(frame_value + bits_int ~size:64 off)); + read_big ~prov:stack_provenance st Exp.Typed.(frame_value + bits_int ~size:64 off) sz + | Global symoff -> + let addr = Elf.SymTable.to_addr_offset symoff in + let addr = State.Exp.of_address ~size:Arch.address_size addr in + Some (read_big ~prov:None st addr sz) + | Const x -> + Some (match x with + | Absolute x -> x |> BitVec.of_z ~size:(8*sz) |> Exp.Typed.bits + | Offset (s, o) -> State.Exp.of_address ~size:(8*sz) Elf.Address.{section=s; offset=Z.to_int o} + ) + | Dwarf _ops -> None + +let eval_loc_from_list ?frame_value sz st pc locs= + let open Option in + let+ loc = List.find_map (fun ((lo,hi), loc) -> ( + let open Elf.Address in + let* hi = hi in + let* over = lo <= pc in + let* under = pc < hi in + if over && under then + Some loc + else + None + )) locs in + eval_loc ?frame_value sz st loc + +let pp_variable_value ~(tenv: Ctype.env) ~(ctype: Ctype.t) value = + let pp ?(hex=false) = fun value -> + match Exp.ConcreteEval.eval_if_concrete value with + | Some(Exp.Value.Bv bv) when not hex -> Pp.int @@ BitVec.to_int bv + | Some(value) -> Exp.Value.pp value + | None -> State.Exp.pp value + in + Pp.optional (pp_typed ~tenv ~ctype ~pp) value + +let printvars ~st ~(dwarf: Dw.t) pc = + let out = ref "" in + + let st = State.copy_if_locked st in + let pv vars = + Seq.iter (fun (v: Dw.Var.t) -> + let sz = Ctype.sizeof v.ctype in + let frame_value = eval_loc_from_list sz st pc v.locs_frame_base |> Option.join in + debug "Frame value %t" Pp.(top (optional State.Exp.pp) frame_value); + let value = eval_loc_from_list ?frame_value sz st pc v.locs in + match value with + | None -> () + | Some var_val -> out := !out ^ Printf.sprintf "%s = %t\n" v.name Pp.(tos (pp_variable_value ~ctype:v.ctype ~tenv:dwarf.tenv) var_val); + ) + vars + in + pv (Hashtbl.to_seq_values dwarf.vars); + Hashtbl.iter (fun _ (fn:Dw.Func.t) -> + let rec pscope (scope:Dw.Func.scope) = + pv (List.to_seq scope.vars); + List.iter pscope scope.scopes + in + pscope fn.func.scope + ) dwarf.funcs; + !out + + +let run_prog elfname name objdump_d branchtables = + match Analyse.Utils.read_file_lines "src/analyse/html-preamble-insts.html" with + | Error _ -> () + | Ok lines -> Array.iter (function s -> Printf.printf "%s\n" s) lines + ; + base "Running with rd %s in %s" name elfname; + base "Loading %s" elfname; + let dwarf = Dw.of_file elfname in + base "Loading %s for Analyse" elfname; + let analyse_test = Analyse.Elf.parse_elf_file elfname in + base "Analysing %s for Analyse" elfname; + let analyse_analysis = Analyse.Collected.mk_analysis analyse_test objdump_d branchtables in + let print_analyse_instruction pc = + let pc = Elf.Address.to_sym pc in + let index = analyse_analysis.index_of_address pc in + let instr = analyse_analysis.instructions.(index) in + Analyse.Pp.pp_instruction Analyse.Types.Html (*Ascii*) analyse_test analyse_analysis 0 index + instr + in + base "Start running"; + let tree = Func.get_state_tree ~elf:elfname ~name ~init:(State.init_sections ~sp:Arch.sp ~addr_size:Arch.address_size) ~every_instruction:true () + ~breakpoints:["UND.abort"; "UND.exit"] + in + base "Ended running, start pretty printing"; + (* This table will contain the state diff to print at each pc with a message *) + (* let instr_data : (Elf.Address.t, string * State.t * State.Reg.t list) Hashtbl.t = + Hashtbl.create 100 + in + let get_footprint pc = + Runner.get_normal_opt runner pc |> Option.fold ~none:[] ~some:Trace.Instr.footprint + in *) + let rec iter (f:Block_lib.label State.Tree.t) = + let st = f.state in + let last_pc = st.last_pc in + (match f.data with + | Block_lib.Start -> () + | Block_lib.BranchAt pc | Block_lib.NormalAt pc -> + if Elf.Address.(last_pc + 4 <> pc) then + Printf.printf "\nJUMP from %t:\n\n" Pp.(top Elf.Address.pp last_pc); + print_string @@ Analyse.Pp.css Analyse.Types.Html Render_vars @@ printvars ~st ~dwarf pc; + print_string (print_analyse_instruction pc); + | Block_lib.End _ -> + print_string "END"; + ); + let succ = List.filter (fun (s:Block_lib.label State.Tree.t) -> + State.is_possible s.state + ) f.rest in + if List.length succ > 1 then + print_string "BRANCH!"; + List.iter iter succ + in + iter tree; + match Analyse.Utils.read_file_lines "src/analyse/html-postamble.html" with + | Error _ -> () + | Ok lines -> Array.iter (function s -> Printf.printf "%s\n" s) lines + + +let elf = + let doc = "ELF file from which to pull the code" in + Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"ELF_FILE" ~doc) + +let func = + let doc = "Symbol name of the function to run" in + Arg.(value & pos 1 string "main" & info [] ~docv:"FUNCTION" ~doc) + +let objdump_d = + let doc = "File containing result of objdump -d" in + Arg.(required & opt (some non_dir_file) None & info ["objdump-d"] ~docv:"OBJDUMP_FILE" ~doc) + +let branch_table = + let doc = "File containing branch table base addresses and sizes" in + Arg.( + (* required *) + value & opt (some non_dir_file) None & info ["branch-tables"] ~docv:"BRANCH_TABLES_FILE" ~doc) + +let term = + Term.( + CmdlinerHelper.func_options comopts run_prog + $ elf $ func $ objdump_d $ branch_table) + +let info = + let doc = + "Run main of relocatable file" + in + Cmd.(info "run-rel-prog" ~doc ~exits) + +let command = (term, info) + \ No newline at end of file diff --git a/src/run/runner.ml b/src/run/runner.ml index 864dba24..7ae5ff59 100644 --- a/src/run/runner.ml +++ b/src/run/runner.ml @@ -75,9 +75,9 @@ type slot = type t = { elf : Elf.File.t; dwarf : Dw.t option; - instrs : (int, slot) Hashtbl.t; (** Instruction cache *) + instrs : (Elf.Address.t, slot) Hashtbl.t; (** Instruction cache *) pc : Reg.t; - funcs : int Vec.t; (** Loaded functions by loading order *) + funcs : Elf.Address.t Vec.t; (** Loaded functions by loading order *) } let of_elf ?dwarf elf = @@ -94,42 +94,45 @@ let of_dwarf dwarf = of_elf ~dwarf dwarf.elf let load_sym runner (sym : Elf.Symbol.t) = info "Loading symbol %s in %s" sym.name runner.elf.filename; Vec.add_one runner.funcs sym.addr; + debug "Loding symbol %t" (Pp.top Elf.Symbol.pp_raw sym); let opcode_list = Arch.split_into_instrs sym.data in let addr = ref sym.addr in List.iter - (fun code -> + (fun Elf.Symbol.{ data = code; relocations } -> let (addr, instr_len) = let result = !addr and len = BytesSeq.length code in - addr := !addr + len; + addr := Elf.Address.(!addr + len); (result, len) in + debug "Relocation at address %t: %t" (Pp.top Elf.Address.pp addr) (Pp.top Elf.Relocations.pp relocations); try - let instr = Trace.Cache.get_instr code in + let reloc = Elf.Relocations.IMap.find_opt 0 relocations in + let instr = Trace.Cache.get_instr (code, reloc) in if instr.traces = [] then begin - debug "Instruction at 0x%x in %s is loaded as special" addr sym.name; + debug "Instruction at %t in %s is loaded as special" (Pp.top Elf.Address.pp addr) sym.name; Hashtbl.add runner.instrs addr (Special instr_len) end else begin - debug "Instruction at 0x%x in %s is loaded as normal. Traces are:\n%t" addr sym.name + debug "Instruction at %t in %s is loaded as normal. Traces are:\n%t" (Pp.top Elf.Address.pp addr) sym.name Pp.(topi Trace.Instr.pp instr); Hashtbl.add runner.instrs addr (Normal instr) end with exn -> - warn "Could not convert isla trace of instruction at 0x%x in %s to Trace.t: %s\n%s" addr + warn "Could not convert isla trace of instruction at %t in %s to Trace.t: %s\n%s" (Pp.top Elf.Address.pp addr) runner.elf.filename (Printexc.to_string exn) (Printexc.get_backtrace ()); Hashtbl.add runner.instrs addr (IslaFail instr_len)) opcode_list (** Fetch an instruction, and return corresponding slot. *) -let fetch (runner : t) (pc : int) : slot = - debug "Fetching PC 0x%x" pc; +let fetch (runner : t) (pc : Elf.Address.t) : slot = + debug "Fetching PC %t" (Pp.top Elf.Address.pp pc); match Hashtbl.find_opt runner.instrs pc with | Some v -> v | None -> ( match Elf.SymTable.of_addr_opt runner.elf.symbols pc with | Some sym when sym.typ = Elf.Symbol.FUNC -> if Hashtbl.mem runner.instrs sym.addr then begin - warn "Tried to fetch in middle of instructions in %s at 0x%x" runner.elf.filename pc; + warn "Tried to fetch in middle of instructions in %s at %t" runner.elf.filename (Pp.top Elf.Address.pp pc); Hashtbl.add runner.instrs pc Nocode; Nocode end @@ -138,13 +141,13 @@ let fetch (runner : t) (pc : int) : slot = match Hashtbl.find_opt runner.instrs pc with | Some v -> v | None -> - warn "Tried to fetch in middle of instructions in %s at 0x%x" runner.elf.filename - pc; + warn "Tried to fetch in middle of instructions in %s at %t" runner.elf.filename + (Pp.top Elf.Address.pp pc); Hashtbl.add runner.instrs pc Nocode; Nocode end | _ -> - warn "Tried to fetch outside of normal code in %s at 0x%x" runner.elf.filename pc; + warn "Tried to fetch outside of normal code in %s at %t" runner.elf.filename (Pp.top Elf.Address.pp pc); Hashtbl.add runner.instrs pc Nocode; Nocode ) @@ -162,12 +165,13 @@ let fetch (runner : t) (pc : int) : slot = let execute_normal ?(prelock = ignore) ~pc runner (instr : Trace.Instr.t) state = let dwarf = runner.dwarf in let next = instr.length in + let relocation = instr.relocation in let run_pure () = List.map (fun (trc : Trace.Instr.trace_meta) -> let nstate = State.copy state in State.set_last_pc nstate pc; - Trace.Run.trace_pc_mut ?dwarf ~next nstate trc.trace; + Trace.Run.trace_pc_mut ?dwarf ?relocation ~next nstate trc.trace; nstate) instr.traces in @@ -175,7 +179,7 @@ let execute_normal ?(prelock = ignore) ~pc runner (instr : Trace.Instr.t) state match instr.traces with | [trc] -> State.set_last_pc state pc; - Trace.Run.trace_pc_mut ?dwarf ~next state trc.trace; + Trace.Run.trace_pc_mut ?dwarf ?relocation ~next state trc.trace; [state] | _ -> prelock state; @@ -187,15 +191,15 @@ let execute_normal ?(prelock = ignore) ~pc runner (instr : Trace.Instr.t) state let skip runner state : State.t list = let pc_exp = State.get_reg_exp state runner.pc in try - let pc = pc_exp |> Ast.expect_bits |> BitVec.to_int in + let pc = State.Exp.expect_sym_address pc_exp in match fetch runner pc with - | Normal { traces = _; read = _; written = _; length; opcode = _ } + | Normal { traces = _; read = _; written = _; length; opcode = _; relocation = _ } |Special length |IslaFail length -> let state = State.copy_if_locked state in State.bump_pc ~pc:runner.pc state length; [state] - | Nocode -> Raise.fail "Trying to skip 0x%x in %s: no code there" pc runner.elf.filename + | Nocode -> Raise.fail "Trying to skip %t in %s: no code there" (Pp.tos Elf.Address.pp pc) runner.elf.filename with exn -> err "Trying to skip instruction at %t in %s: Unexpected error" Pp.(top State.Exp.pp pc_exp) @@ -219,14 +223,14 @@ let skip runner state : State.t list = let run ?prelock runner state : State.t list = let pc_exp = State.get_reg_exp state runner.pc in try - let pc = pc_exp |> Ast.expect_bits |> BitVec.to_int in + let pc = State.Exp.expect_sym_address pc_exp in match fetch runner pc with | Normal instr -> execute_normal ?prelock ~pc runner instr state | Special _ -> - Raise.fail "Special instruction at 0x%x in %s. unsupported for now" pc runner.elf.filename - | Nocode -> Raise.fail "Trying to run 0x%x in %s: no code there" pc runner.elf.filename + Raise.fail "Special instruction at %t in %s. unsupported for now" (Pp.tos Elf.Address.pp pc) runner.elf.filename + | Nocode -> Raise.fail "Trying to run %t in %s: no code there" (Pp.tos Elf.Address.pp pc) runner.elf.filename | IslaFail _ -> - Raise.fail "Trying to run 0x%x in %s: Isla pipeline failed on that instruction" pc + Raise.fail "Trying to run %t in %s: Isla pipeline failed on that instruction" (Pp.tos Elf.Address.pp pc) runner.elf.filename with exn -> err "Trying to run instruction at %t in %s: Unexpected error" @@ -257,4 +261,4 @@ let pp_slot = (** Dump instruction table *) let pp_instr (runner : t) = let open Pp in - hashtbl_sorted ~name:"Instructions" ~compare ptr pp_slot runner.instrs + hashtbl_sorted ~name:"Instructions" ~compare Elf.Address.pp pp_slot runner.instrs diff --git a/src/run/testRelProg.ml b/src/run/testRelProg.ml new file mode 100644 index 00000000..e9f15408 --- /dev/null +++ b/src/run/testRelProg.ml @@ -0,0 +1,120 @@ +open Cmdliner +open Config.CommonOpt + +open Logs.Logger (struct + let str = __MODULE__ +end) + +type err = { msg: string; asserts: State.Exp.t list } +type node_result = { all_fail: bool; errors: err list } +let node_result_of_result = function +| Ok () -> { all_fail=false; errors=[] } +| Error e -> { all_fail=true; errors=[e] } + +let rec process_tree ~pc ~ret ~ext (node:Block_lib.label State.Tree.t) = + let l = node.data in + let st = node.state in + + let found_symread = ref false in + st.read_vars |> Vec.iter Fun.(State.Tval.exp %> Ast.Manip.exp_iter_var (fun v -> + match v with + | State.Var.ReadVar _ -> found_symread := true; warn "State contains symbolic read variable:\n %t" (Pp.top State.Var.pp v) + | _ -> () + )); + if !found_symread then + warn "State:\n%t" (Pp.top State.pp st); + + if not (State.is_possible st) then + { all_fail=true; errors=[] } + else match l with + | Block_lib.End _ -> let result = ( + let pc_exp = State.get_reg_exp st pc in + let pc_addr = try + Some (State.Exp.expect_sym_address pc_exp) + with + _ -> None + in + let ret_exp = match pc_addr with + | Some pc_addr -> + if pc_addr = Elf.Address.{ section="UND.abort"; offset=0 } then + Result.error { + msg=Printf.sprintf "abort called from %t" (Pp.tos Elf.Address.pp st.last_pc); + asserts=st.asserts; + } + else if pc_addr <> Elf.Address.{ section="UND.exit"; offset=0 } then + Result.error { + msg=Printf.sprintf "finished at weird address %t" (Pp.tos Elf.Address.pp pc_addr); + asserts=st.asserts; + } + else + Result.ok (State.get_reg_exp st ext) + | None -> + Result.ok (State.get_reg_exp st ret) (* Symbolic pc = returned from main *) + in + Result.bind ret_exp @@ fun ret_exp -> + let ret_val = ret_exp |> Exp.ConcreteEval.eval |> Exp.Value.expect_bv |> BitVec.to_int in + if ret_val <> 0 then + Result.error { + msg=Printf.sprintf "non-zero return code %d" ret_val; + asserts=st.asserts + } + else + Result.ok () + ) in + node_result_of_result result + | _ -> + let results = List.map (process_tree ~pc ~ret ~ext) node.rest in + let all_errors = List.bind results (fun x -> x.errors) in + if List.for_all (fun x -> x.all_fail) results then { + all_fail=true; + errors=List.map (fun x -> {x with asserts=st.asserts}) all_errors; + } + else { + all_fail=false; + errors=all_errors; + } + +let test return_register exit_register name = + let tree = Func.get_state_tree ~elf:name ~name:"main" ~init:(State.init_sections ~sp:Arch.sp ~addr_size:Arch.address_size) ~every_instruction:false () + ~breakpoints:["UND.abort"; "UND.exit"] + in + debug "%t" (Pp.top (State.Tree.pp_all Block_lib.pp_label) tree); + let pc = Arch.pc () in + let ret = State.Reg.of_string return_register in + let ext = State.Reg.of_string exit_register in + let results = process_tree ~pc ~ret ~ext tree in + if List.is_empty results.errors then + base "Success" + else + fail "Some paths fail: %t" Pp.( + top (list (fun (e:err) -> !^(e.msg) ^^ !^" when " ^^ list State.Exp.pp e.asserts)) results.errors + ) + +let elf = + let doc = "ELF file from which to pull the code" in + Arg.(required & pos 0 (some non_dir_file) None & info [] ~docv:"ELF_FILE" ~doc) + +let return_register = + let doc = "The name of the register containing the return value of main function" in + Arg.(value & opt string "R0" & info ["r"] ~docv:"RETURN_REGISTER" ~doc) + +let exit_register = + let doc = "The name of the register containing the argument to exit function" in + Arg.(value & opt string "R0" & info ["e"] ~docv:"EXIT_REGISTER" ~doc) + + +let term = + Term.( + CmdlinerHelper.func_options comopts test + $ return_register $ exit_register $ elf) + +let info = + let doc = + "Test run relocatable file\ + + Test succeeds if all possble outcomes result in the program exiting with\ + with code 0" + in + Cmd.(info "test-rel-prog" ~doc ~exits) + +let command = (term, info) diff --git a/src/state/base.ml b/src/state/base.ml index 52cad8a8..17659776 100644 --- a/src/state/base.ml +++ b/src/state/base.ml @@ -62,6 +62,8 @@ end type id = Id.t module Var = struct + let next_nondet = ref 0 + type t = | Register of Id.t * Reg.t (** The value of this register in this state *) | ReadVar of Id.t * int * Ast.Size.t @@ -76,6 +78,8 @@ module Var = struct | NonDet of int * Ast.Size.t (** Variable representing non-determinism in the spec. Can only be bit-vectors of size {8, 16, 32, 64} for now. *) + | Section of string + (** Symbolic base address of ELF section. Assume 64bit for now. *) let to_string = function | Register (state, reg) -> @@ -90,6 +94,7 @@ module Var = struct | NonDet (num, size) -> if size = Ast.Size.B64 then Printf.sprintf "nondet:%i" num else Printf.sprintf "nondet:%i:%dbits" num (Ast.Size.to_bits size) + | Section s -> "section:"^s let expect_register = function | Register (_, reg) -> reg @@ -125,6 +130,7 @@ module Var = struct | ["arg"; num] -> Arg (int_of_string num) | ["retarg"; ""] -> RetArg | ["retaddr"; ""] -> RetAddr + | ["section"; s] -> Section s | _ -> Raise.inv_arg "Invalid state variable: %s" s let of_reg id reg = Register (id, reg) @@ -138,6 +144,7 @@ module Var = struct | (RetArg, RetArg) -> true | (RetAddr, RetAddr) -> true | (NonDet (num, size), NonDet (num', size')) -> num = num' && size = size' + | (Section s, Section s') -> s = s' | _ -> false let hash = Hashtbl.hash @@ -153,10 +160,18 @@ module Var = struct | RetArg -> Ast.Ty_BitVec 64 | RetAddr -> Ast.Ty_BitVec 64 | NonDet (_, size) -> Ast.Ty_BitVec (Ast.Size.to_bits size) + | Section _ -> Ast.Ty_BitVec 64 + + let new_nondet sz = + let v = NonDet (!next_nondet, sz) in + next_nondet := !next_nondet + 1; + v end type var = Var.t +module Z3St = Z3.Make (Var) + module Sums = Exp.Sums module Typed = Exp.Typed module ConcreteEval = Exp.ConcreteEval @@ -166,6 +181,27 @@ module Exp = struct include Exp.Make (Var) let of_reg id reg = Var.of_reg id reg |> of_var + + let expect_sym_address exp = + let sym, conc = Exp.Sums.split_concrete exp in + let section = match sym with + | Some(Ast.Var (Var.Section s, _)) -> s + | _ -> Raise.fail "Expected symbolic Section base" + in + let offset = BitVec.to_int conc in + Elf.Address.{ section; offset } + + let of_section ~(size : int) (section : string) = + Typed.extract ~last:(size-1) ~first:0 + (of_var @@ Var.Section section) + + + let of_address ~(size : int) (addr : Elf.Address.t) = + Typed.( + of_section ~size addr.section + + + bits_int ~size addr.offset + ) end type exp = Exp.t @@ -199,6 +235,74 @@ end type tval = Tval.t +module Relocation = struct + type t = { + value: Exp.t; + asserts: Exp.t list; + target: Elf.Relocations.target; + } + + let rec exp_of_relocation_exp: Elf.Relocations.exp -> exp = + let f = exp_of_relocation_exp in function + | Section s -> Exp.of_var (Var.Section s) (* TODO size? *) + | Const x -> Typed.bits (BitVec.of_int x ~size:64) (* TODO size? *) + | BinOp (a, Add, b) -> Typed.(f a + f b) + | BinOp (a, Sub, b) -> Typed.(f a - f b) + | BinOp (a, And, b) -> Typed.manyop (AstGen.Ott.Bvmanyarith AstGen.Ott.Bvand) [f a; f b] + | UnOp (Not, b) -> Typed.unop AstGen.Ott.Bvnot (f b) + + let of_elf (relocation: Elf.Relocations.rel) = + let open Elf.Relocations in + let value = exp_of_relocation_exp relocation.value in + let asserts = List.map (function + | Range (min, max) -> + let min = Typed.bits @@ BitVec.of_z ~size:64 @@ Z.of_int64 min in + let max = Typed.bits @@ BitVec.of_z ~size:64 @@ Z.of_int64 max in + let cond1 = Typed.(binop (Bvcomp Bvsle) min value) in + let cond2 = Typed.(binop (Bvcomp Bvslt) value max) in + Typed.(manyop And [cond1; cond2]) + | Alignment b -> + let last = b-1 in + Typed.(extract ~first:0 ~last value = bits_int ~size:b 0) + ) relocation.checks in + let (last, first) = relocation.mask in + let value = Typed.extract ~first ~last value in + { value; asserts; target = relocation.target } + + module IMap = Map.Make (Int) + + let exp_of_data (data : Elf.Symbol.data) = + let size = 8 * (BytesSeq.length data.data) in + (* Assume little endian here *) + let bv = BytesSeq.getbvle ~size data.data 0 in + let exp = Typed.bits bv in + IMap.fold (fun offset rel (exp, asserts) -> + let relocation = of_elf rel in + let pos = 8 * offset in + let width = match relocation.target with + | AArch64 Abi_aarch64_symbolic_relocation.Data640 -> 64 + | AArch64 Abi_aarch64_symbolic_relocation.Data320 -> 32 + | _ -> Raise.fail "Unsopported relocation" + in + let before = if pos > 0 then + [Typed.extract ~first:0 ~last:(pos-1) exp] + else + [] + in + let after = if pos + width < size then + [Typed.extract ~first:(pos+width) ~last:(size-1) exp] + else + [] + in + let v, a = + ( + Typed.concat (after @ relocation.value :: before), + relocation.asserts @ asserts + ) in + v,a + ) data.relocations (exp, []) +end + module Mem = struct module Size = Ast.Size @@ -214,20 +318,34 @@ module Mem = struct In general the stack will be the fragment 0 but this is not guaranteed. Some execution contexts may even not have any stacks.*) - type t = { mutable main : Fragment.t; frags : (Exp.t * Fragment.t) Vec.t } + type t = { + mutable main : Fragment.t; + frags : (Exp.t * Fragment.t) Vec.t; + sections : (string, provenance) Hashtbl.t; (* mapping sections to their fragments *) + mutable allow_main : bool; (* HACK to prvent incorrectly assuming Main provenance when using section fragments *) + } (** Get the main fragment of memory *) - let get_main { main; frags = _ } = main + let get_main { main; _ } = main + + (** Get fragment *) + let get_frag mem i = + Vec.get mem.frags i (** Empty memory, every address is unbound *) - let empty () = { main = Fragment.empty; frags = Vec.empty () } + let empty () = { main = Fragment.empty; frags = Vec.empty (); sections = Hashtbl.create 10; allow_main = true } (** Build a new memory from the old one by keeping the old one as a base *) let from mem = - { main = Fragment.from mem.main; frags = Vec.map (Pair.map Fun.id Fragment.from) mem.frags } + { + main = Fragment.from mem.main; + frags = Vec.map (Pair.map Fun.id Fragment.from) mem.frags; + sections = Hashtbl.copy mem.sections; + allow_main = mem.allow_main; + } (** Copy the memory so that it can be mutated separately *) - let copy mem = { main = mem.main; frags = Vec.copy mem.frags } + let copy mem = { main = mem.main; frags = Vec.copy mem.frags; sections = Hashtbl.copy mem.sections; allow_main = mem.allow_main } (** Add a new fragment with the specified base *) let new_frag mem base = @@ -295,11 +413,28 @@ module Mem = struct Vec.ppi (fun (base, frag) -> Pp.infix 2 1 colon (Exp.pp base) (Fragment.pp_raw frag)) mem.frags ); + ("sections", hashtbl string Ctype.pp_provenance mem.sections) ] (** Check is this memory is empty which means all addresses are undefined *) let is_empty mem = Fragment.is_empty mem.main && Vec.for_all (Pair.for_all Fun.ctrue Fragment.is_empty) mem.frags + + + let create_section_frag ~addr_size mem section = + match Hashtbl.find_opt mem.sections section with + | Some prov -> + info "Fragment for section %s already exists" section; + prov + | None -> + let base = Exp.of_section ~size:addr_size section in + let prov = new_frag mem base in + Hashtbl.replace mem.sections section prov; + prov + + let get_section_provenance mem section = + Hashtbl.find_opt mem.sections section + |> Option.value ~default:Ctype.Main end type t = { @@ -309,6 +444,7 @@ type t = { mutable regs : Tval.t Reg.Map.t; (** The values and types of registers *) read_vars : Tval.t Vec.t; (** The results of reads made since base state *) mutable asserts : exp list; (** Only asserts since base_state *) + mutable relocation_asserts : exp list; (** Only asserts since base_state *) mem : Mem.t; elf : Elf.File.t option; (** Optionally an ELF file, this may be used when running instructions on @@ -317,7 +453,7 @@ type t = { However the symbolic execution should always be more concrete with it than without it *) fenv : Fragment.env; (** The memory type environment. See {!Fragment.env} *) - mutable last_pc : int; + mutable last_pc : Elf.Address.t; (** The PC of the instruction that lead into this state. The state should be right after that instruction. This has no semantic meaning as part of the state. It's just for helping knowing what comes from where *) @@ -351,10 +487,11 @@ let make ?elf () = regs = Reg.Map.init @@ Tval.of_reg id; read_vars = Vec.empty (); asserts = []; + relocation_asserts = []; mem = Mem.empty (); elf; fenv = Fragment.Env.make (); - last_pc = 0; + last_pc = Elf.Address.{ section = ".text"; offset = 0 }; (* TODO is this right? *) } in next_id := id + 1; @@ -372,6 +509,7 @@ let copy ?elf state = regs = Reg.Map.copy state.regs; read_vars = Vec.empty (); asserts = (if locked then [] else state.asserts); + relocation_asserts = (if locked then [] else state.relocation_asserts); mem = (if locked then Mem.from state.mem else Mem.copy state.mem); elf = Option.(elf ||| state.elf); fenv = Fragment.Env.copy state.fenv; @@ -388,6 +526,13 @@ let push_assert (s : t) (e : exp) = assert (not @@ is_locked s); s.asserts <- e :: s.asserts +let push_relocation_assert (s : t) (e : exp) = + assert (not @@ is_locked s); + s.relocation_asserts <- e :: s.relocation_asserts + +let rec load_relocation_asserts (s : t) = + s.relocation_asserts @ (s.base_state |> Option.map load_relocation_asserts |> Option.value ~default:[]) + let set_asserts state asserts = assert (not @@ is_locked state); state.asserts <- asserts @@ -422,54 +567,120 @@ let set_read (s : t) (read_num : int) (exp : Exp.t) = assert (Typed.get_type exp = Typed.get_type (Vec.get s.read_vars read_num |> Tval.exp)); Vec.update s.read_vars read_num @@ Tval.map_exp (Fun.const exp) +let eval_address (s : t) (addr: Exp.t) : Elf.Address.t option = + let ctxt0 = function Var.Section _ -> Value.bv @@ BitVec.of_int ~size:64 0 | _ -> raise ConcreteEval.Symbolic in + let open Option in + let* offset_exp = try + Some (ConcreteEval.eval ~ctxt:ctxt0 addr) + with + ConcreteEval.Symbolic -> None + in + let offset = offset_exp |> Value.expect_bv |> BitVec.to_int in + let sections = Hashtbl.create 10 in + Ast.Manip.exp_iter_var (function Var.Section s -> Hashtbl.add sections s () | _ -> ()) addr; + + let hyps = load_relocation_asserts s in + let size = addr |> Typed.get_type |> Typed.expect_bv in + sections |> Hashtbl.to_seq_keys |> Seq.find_map (fun section -> + let address = Elf.Address.{ section; offset } in + let expression = Exp.of_address ~size address in + if Z3St.check_full ~hyps Typed.(expression = addr) = Some true then + Some address + else + None + ) + let read_from_rodata (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) : Exp.t option = + debug "reading from rodata at address: %t" (Pp.top Exp.pp addr); match s.elf with | None -> None | Some elf -> ( - if not @@ ConcreteEval.is_concrete addr then None - else - let int_addr = ConcreteEval.eval addr |> Value.expect_bv |> BitVec.to_int in - let size = size |> Ast.Size.to_bits in - try - let (sym, offset) = Elf.SymTable.of_addr_with_offset elf.symbols int_addr in - if sym.writable then None - else - (* Assume little endian here *) - let bv = BytesSeq.getbvle ~size sym.data offset in - Some (Typed.bits bv) - with Not_found -> - let rodata = elf.rodata in - if rodata.addr <= int_addr && int_addr + size < rodata.addr + rodata.size then - let bv = BytesSeq.getbvle ~size rodata.data (int_addr - rodata.addr) in - (* Assume little endian here *) - Some (Typed.bits bv) - else ( - warn "Failed to find symbol or rodata at 0x%x" int_addr; - None - ) + Option.bind (eval_address s addr) @@ fun sym_addr -> + let size = size |> Ast.Size.to_bytes in + try + let (sym, offset) = Elf.SymTable.of_addr_with_offset elf.symbols sym_addr in + if sym.writable then None + else ( + let data = Elf.Symbol.sub sym offset size in + let value, asserts = Relocation.exp_of_data data in + + if not @@ List.is_empty asserts then + warn "Relocaiton assserts in .rodata ignored: %t" Pp.(top (list Exp.pp) asserts); + + Some value + ) + with Not_found -> + let int_addr = sym_addr.offset in + let open Option in + let* rodata = Elf.File.SMap.find_opt sym_addr.section elf.rodata in + if rodata.addr <= int_addr && int_addr + size <= rodata.addr + rodata.size then + let data, relocations = rodata.data in + let data = BytesSeq.sub data (int_addr - rodata.addr) size in + let relocations = Elf.Relocations.sub relocations (int_addr - rodata.addr) size in + let value, asserts = Relocation.exp_of_data {data; relocations} in + + if not @@ List.is_empty asserts then + warn "Relocaiton assserts in .rodata ignored: %t" Pp.(top (list Exp.pp) asserts); + + Some value + else ( + warn "Failed to find symbol or rodata at %t" (Pp.top Elf.Address.pp sym_addr); + None + ) ) -let read ~provenance ?ctyp (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) : Exp.t = +let rec read ~provenance ?ctyp (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) : Exp.t = assert (not @@ is_locked s); - let var = make_read ?ctyp s size in - let exp = Mem.read s.mem ~provenance ~var ~addr ~size in - let exp = if provenance = Main && exp = None then read_from_rodata ~addr ~size s else exp in - Option.iter (set_read s (Var.expect_readvar var)) exp; - Option.value exp ~default:(Exp.of_var var) - -let read_noprov ?ctyp (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) : Exp.t = - if ConcreteEval.is_concrete addr || Vec.length s.mem.frags = 0 then - read ~provenance:Ctype.Main ?ctyp s ~addr ~size - else Raise.fail "Trying to access %t in state %d: No provenance info" Pp.(tos Exp.pp addr) s.id - -let write ~provenance (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) (value : Exp.t) : unit = + if provenance = Ctype.Main && not s.mem.allow_main then + read_noprov ?ctyp s ~addr ~size + else + let var = make_read ?ctyp s size in + let exp = Mem.read s.mem ~provenance ~var ~addr ~size in + let exp = if exp = None then read_from_rodata ~addr ~size s else exp in + Option.iter (set_read s (Var.expect_readvar var)) exp; + Option.value exp ~default:(Exp.of_var var) + +and read_noprov ?ctyp (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) : Exp.t = + debug "Addr: %t" Pp.(top Exp.pp addr); + let elf_addr = eval_address s addr in + debug "Address: %t" Pp.(top (optional Elf.Address.pp) elf_addr); + match elf_addr with + | Some elf_addr -> + let addr_size = addr |> Typed.get_type |> Typed.expect_bv in + let addr = Exp.of_address ~size:addr_size elf_addr in + let provenance = Mem.get_section_provenance s.mem elf_addr.section in + if provenance = Ctype.Main && not s.mem.allow_main then + Raise.fail "Main fragment should not be used here"; + read ~provenance ?ctyp s ~addr ~size + | None when Vec.length s.mem.frags = 0 -> + if not s.mem.allow_main then + Raise.fail "Main fragment should not be used here"; + read ~provenance:Ctype.Main ?ctyp s ~addr ~size + | None -> Raise.fail "Trying to access %t in state %d: No provenance info" Pp.(tos Exp.pp addr) s.id + +let rec write ~provenance (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) (value : Exp.t) : unit = assert (not @@ is_locked s); - Mem.write ~provenance s.mem ~addr ~size ~exp:value - -let write_noprov (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) (value : Exp.t) : unit = - if ConcreteEval.is_concrete addr || Vec.length s.mem.frags = 0 then - write ~provenance:Ctype.Main s ~addr ~size value - else Raise.fail "Trying to access %t in state %d: No provenance info" Pp.(tos Exp.pp addr) s.id + if provenance = Ctype.Main && not s.mem.allow_main then + write_noprov s ~addr ~size value + else + Mem.write ~provenance s.mem ~addr ~size ~exp:value + +and write_noprov (s : t) ~(addr : Exp.t) ~(size : Mem.Size.t) (value : Exp.t) : unit = + let elf_addr = eval_address s addr in + debug "Address: %t" Pp.(top (optional Elf.Address.pp) elf_addr); + match elf_addr with + | Some elf_addr -> + let addr_size = addr |> Typed.get_type |> Typed.expect_bv in + let addr = Exp.of_address ~size:addr_size elf_addr in + let provenance = Mem.get_section_provenance s.mem elf_addr.section in + if provenance = Ctype.Main && not s.mem.allow_main then + Raise.fail "Main fragment should not be used here"; + write ~provenance s ~addr ~size value + | None when Vec.length s.mem.frags = 0 -> + if not s.mem.allow_main then + Raise.fail "Main fragment should not be used here"; + write ~provenance:Ctype.Main s ~addr ~size value + | None -> Raise.fail "Trying to access %t in state %d: No provenance info" Pp.(tos Exp.pp addr) s.id let reset_reg (s : t) ?(ctyp : Ctype.t option) (reg : Reg.t) : unit = assert (not @@ is_locked s); @@ -492,34 +703,120 @@ let get_reg_exp s reg = get_reg s reg |> Tval.exp let update_reg_exp (s : t) (reg : Reg.t) (f : exp -> exp) = Reg.Map.get s.regs reg |> Tval.map_exp f |> Reg.Map.set s.regs reg +(* TODO *) let set_pc ~(pc : Reg.t) (s : t) (pcval : int) = let exp = Typed.bits_int ~size:64 pcval in - let ctyp = Ctype.of_frag Ctype.Global ~offset:pcval ~constexpr:true in + let ctyp = Ctype.of_frag (Ctype.Global ".text") ~offset:pcval ~constexpr:true in + set_reg s pc @@ Tval.make ~ctyp exp + +let set_pc_sym ~(pc : Reg.t) (s : t) (pcval : Elf.Address.t) = + let exp = Typed.(var ~typ:(Ty_BitVec 64) (Var.Section pcval.section) + bits_int ~size:64 pcval.offset) in + let ctyp = Ctype.of_frag (Ctype.Global ".text") ~offset:pcval.offset ~constexpr:true in set_reg s pc @@ Tval.make ~ctyp exp + let bump_pc ~(pc : Reg.t) (s : t) (bump : int) = let pc_exp = get_reg_exp s pc in - assert (ConcreteEval.is_concrete pc_exp); - let old_pc = ConcreteEval.eval pc_exp |> Value.expect_bv |> BitVec.to_int in - let new_pc = old_pc + bump in - set_pc ~pc s new_pc + let old_pc = Exp.expect_sym_address pc_exp in + let new_pc = Elf.Address.(old_pc + bump) in + set_pc_sym ~pc s new_pc let concretize_pc ~(pc : Reg.t) (s : t) = - let pc_exp = get_reg_exp s pc in - try ConcreteEval.eval pc_exp |> Value.expect_bv |> BitVec.to_int |> set_pc ~pc s - with ConcreteEval.Symbolic -> () + pc |> get_reg_exp s |> eval_address s |> Option.iter (set_pc_sym ~pc s) let set_last_pc state pc = assert (not @@ is_locked state); state.last_pc <- pc + +let push_section_constraints ~sp ~addr_size state sections = + let sp = sp () in + let rec f : Elf.File.section list -> unit = function + | [] -> () + | s::rest -> ( + let max_section_addr = Int.shift_left 1 addr_size - s.size in + let s_exp = (Exp.of_var (Var.Section s.name)) in + (* The whole section fits in memory *) + push_assert state Typed.(comp Ast.Bvule s_exp (bits_int ~size:64 max_section_addr)); + (* The load address cannot be 0 *) + push_assert state Typed.(not (s_exp = (bits_int ~size:64 0))); + if s.align > 1 then ( + let (align_pow, _) = Seq.ints 0 + |> Seq.drop_while (fun x -> Int.shift_left 1 x < s.align) + |> Seq.uncons + |> Option.get + in + if s.align = Int.shift_left 1 align_pow then + let last = align_pow - 1 in + (* Section address is aligned *) + push_assert state Typed.(extract ~first:0 ~last s_exp = zero ~size:align_pow) + else + warn "Section alignment is not a power of two: %d" s.align + ); + (* Sections don't overlap *) + let s_end = Typed.(s_exp + bits_int ~size:64 s.size) in (* we know this doesn't overflow thanks to the other constraints *) + List.iter (fun (s2:Elf.File.section) -> + let s2_exp = (Exp.of_var (Var.Section s2.name)) in + let s2_end = Typed.(s2_exp + bits_int ~size:64 s2.size) in + let order1 = Typed.(comp Ast.Bvule s_end s2_exp) in + let order2 = Typed.(comp Ast.Bvule s2_end s_exp) in + push_assert state Typed.(manyop Or [order1; order2]) + ) rest; + (* Doesn't overlap with stack *) + let stack_end = get_reg_exp state sp in + let stack_start = Typed.(stack_end - bits_int ~size:64 0x1000) in + let order1 = Typed.(comp Ast.Bvule s_end stack_start) in + let order2 = Typed.(comp Ast.Bvule stack_end s_exp) in + push_assert state Typed.(manyop Or [order1; order2]); + + f rest + ) + in + f sections + +let init_sections ~sp ~addr_size state = + let state = copy_if_locked state in + let _ = Option.( + let+ elf = state.elf in + state.mem.allow_main <- false; + push_section_constraints ~sp ~addr_size state elf.sections; + List.iter (fun (x:Elf.File.section) -> Mem.create_section_frag ~addr_size state.mem x.name |> ignore) elf.sections; + Elf.SymTable.iter elf.symbols @@ fun sym -> + let len = List.find (fun x -> sym.size mod x = 0) [16;8;4;2;1] in + if sym.typ = Elf.Symbol.OBJECT then + let provenance = Mem.get_section_provenance state.mem sym.addr.section in + Seq.iota_step_up ~step:len ~endi:sym.size + |> Seq.iter (fun off -> + let data = Elf.Symbol.sub sym off len in + let addr = Exp.of_address ~size:addr_size Elf.Address.(sym.addr + off) in + let size = Ast.Size.of_bytes len in + let (exp, asserts) = Relocation.exp_of_data data in + Mem.write ~provenance state.mem ~addr ~size ~exp; + List.iter (push_relocation_assert state) asserts; + ) + ) in + lock state; + state + +let init_sections_symbolic ~sp ~addr_size state = + let state = copy_if_locked state in + let _ = Option.( + let+ elf = state.elf in + push_section_constraints ~sp ~addr_size state elf.sections; + Elf.SymTable.iter elf.symbols @@ fun sym -> + if sym.typ = Elf.Symbol.OBJECT then + Hashtbl.replace state.mem.sections sym.addr.section Main + ) in + lock state; + state + let pp s = let open Pp in record "state" [ ("id", Id.pp s.id); ("base_state", Option.fold ~none:!^"none" ~some:(fun s -> Id.pp s.id) s.base_state); - ("last_pc", ptr s.last_pc); + ("last_pc", Elf.Address.pp s.last_pc); ("regs", Reg.Map.pp Tval.pp s.regs); ("fenv", Fragment.Env.pp s.fenv); ("read_vars", Vec.ppi Tval.pp s.read_vars); @@ -536,7 +833,7 @@ let pp_partial ~regs s = [ ("id", Id.pp s.id |> some); ("base_state", Option.map (fun s -> Id.pp s.id) s.base_state); - ("last_pc", ptr s.last_pc |> some); + ("last_pc", Elf.Address.pp s.last_pc |> some); ( "regs", List.map (fun reg -> (Reg.pp reg, Reg.Map.get s.regs reg |> Tval.pp)) regs |> Pp.mapping "" |> some ); diff --git a/src/state/base.mli b/src/state/base.mli index 455943b0..73d6c370 100644 --- a/src/state/base.mli +++ b/src/state/base.mli @@ -113,6 +113,8 @@ module Var : sig | RetAddr (** The return address: The address to which a "return" instruction would jump. *) | NonDet of int * Ast.Size.t (** Variable representing non-determinism in the spec. Can only be a bit-vector for now. *) + | Section of string + (** Symbolic base address of ELF section. Assume 64bit for now. *) (** Convert the variable to the string encoding. For parsing infrastructure reason, the encoding must always contain at least one [:]. *) @@ -143,6 +145,9 @@ module Var : sig (** Get the type of a variable *) val ty : t -> Reg.ty + + (** Get a fresh NonDet variable *) + val new_nondet : Ast.Size.t -> t end (** The type of variables *) @@ -156,6 +161,12 @@ module Exp : sig (** Create an expression from an register and a state id *) val of_reg : id -> Reg.t -> t + + val expect_sym_address : t -> Elf.Address.t + + val of_section : size:int -> string -> t + + val of_address : size:int -> Elf.Address.t -> t end type exp = Exp.t @@ -189,6 +200,18 @@ end type tval = Tval.t +module Relocation : sig + type t = { + value: Exp.t; + asserts: Exp.t list; + target: Elf.Relocations.target; + } + + val of_elf : Elf.Relocations.rel -> t + + val exp_of_data : Elf.Symbol.data -> (exp * exp list) +end + (** {1 State memory management } *) (** This module manages the memory part of the state. @@ -236,6 +259,9 @@ module Mem : sig (** Get the main fragment of memory *) val get_main : t -> Fragment.t + + (** Get fragment *) + val get_frag : t -> int -> Exp.t * Fragment.t end (** {1 State type } *) @@ -284,6 +310,7 @@ type t = private { mutable regs : Tval.t Reg.Map.t; (** The values and types of registers *) read_vars : Tval.t Vec.t; (** The results of reads made since base state *) mutable asserts : exp list; (** Only asserts since base_state *) + mutable relocation_asserts : exp list; (** Only asserts since base_state *) mem : Mem.t; elf : Elf.File.t option; (** Optionally an ELF file, this may be used when running instructions on @@ -292,7 +319,7 @@ type t = private { However the symbolic execution should always be more concrete with it than without it *) fenv : Fragment.env; (** The memory type environment. See {!Fragment.env} *) - mutable last_pc : int; + mutable last_pc : Elf.Address.t; (** The PC of the instruction that lead into this state. The state should be right after that instruction. This has no semantic meaning as part of the state. It's just for helping knowing what comes from where *) @@ -381,11 +408,20 @@ val copy : ?elf:Elf.File.t -> t -> t The returned state is always unlocked *) val copy_if_locked : ?elf:Elf.File.t -> t -> t +val init_sections : sp:(unit -> Reg.t) -> addr_size:int -> t -> t + +(** Assigns all sections with global objects to Main fragment *) +val init_sections_symbolic : sp:(unit -> Reg.t) -> addr_size:int -> t -> t + + (** {1 State convenience manipulation } *) (** Add an assertion to a state *) val push_assert : t -> exp -> unit +(** Add an assertion to a state *) +val push_relocation_assert : t -> exp -> unit + (** Set a state to be impossible (single [false] assert). *) val set_impossible : t -> unit @@ -464,6 +500,8 @@ val update_reg_exp : t -> Reg.t -> (exp -> exp) -> unit (** Set the PC to a concrete value and keep its type appropriate *) val set_pc : pc:Reg.t -> t -> int -> unit +val set_pc_sym : pc:Reg.t -> t -> Elf.Address.t -> unit + (** Bump a concrete PC by a concrete bump (generally the size of a non-branching instruction *) val bump_pc : pc:Reg.t -> t -> int -> unit @@ -471,7 +509,7 @@ val bump_pc : pc:Reg.t -> t -> int -> unit val concretize_pc : pc:Reg.t -> t -> unit (** Set the [last_pc] of the state *) -val set_last_pc : t -> int -> unit +val set_last_pc : t -> Elf.Address.t -> unit (** {1 Pretty printing } *) diff --git a/src/state/reg.mli b/src/state/reg.mli index fd67c573..b9692051 100644 --- a/src/state/reg.mli +++ b/src/state/reg.mli @@ -216,6 +216,9 @@ module Map : sig (** Map the function all the registers (including future, not yet added ones) *) val map : ('a -> 'b) -> 'a t -> 'b t + (** Same as {!map} but with the index *) + val mapi : (reg -> 'a -> 'b) -> 'a t -> 'b t + (** Map the function on all the register by mutation (including future ones) *) val map_mut : ('a -> 'a) -> 'a t -> unit diff --git a/src/state/simplify.ml b/src/state/simplify.ml index 3fee6e92..14088110 100644 --- a/src/state/simplify.ml +++ b/src/state/simplify.ml @@ -90,11 +90,18 @@ let ctxfull state = (fun e -> declare e; match Z3St.check_both serv e with - | Some true -> None + | Some true -> + debug "%t is redundant" (Pp.top Exp.pp e); + None | Some false -> found_false := true; + debug "%t is impossible" (Pp.top Exp.pp e); None - | None -> Some e) + | None -> + debug "%t is possible" (Pp.top Exp.pp e); + Z3St.send_assert serv e; + Some e + ) state.asserts in (* If state is impossible then it has a single assertion: false *) diff --git a/src/state/symbolicBytes.ml b/src/state/symbolicBytes.ml index e9bf6836..07a43622 100644 --- a/src/state/symbolicBytes.ml +++ b/src/state/symbolicBytes.ml @@ -126,6 +126,7 @@ module Make (Var : Exp.Var) : S with type var = Var.t = struct assert (pos + len <= elen); (Typed.extract ~last:((8 * (pos + len)) - 1) ~first:(8 * pos) e, len) + (* TODO should we care about endianness? *) (* Warning: This code is complicated because of all the indices. I tried to make diagrams to explain *) let sub ~pos ~len sb = @@ -148,7 +149,7 @@ module Make (Var : Exp.Var) : S with type var = Var.t = struct || *) let next = pos + off_len in - let* rest = sub_list ~pos:next ~len:(len - next) sb in + let* rest = sub_list ~pos:next ~len:(len - off_len) sb in let nexp = Typed.extract ~last:((8 * elen) - 1) ~first:(8 * off) e in Some (nexp :: rest) else @@ -166,7 +167,7 @@ module Make (Var : Exp.Var) : S with type var = Var.t = struct Some [Typed.extract ~last:((8 * taken_len) - 1) ~first:(8 * off) e] in let+ list = sub_list ~pos ~len sb in - Typed.concat list + Typed.concat @@ List.rev list let blit_exp exp ~pos ~len sb = assert (len > 0); diff --git a/src/state/symbolicFragment.ml b/src/state/symbolicFragment.ml index dbc941fa..40ef78f2 100644 --- a/src/state/symbolicFragment.ml +++ b/src/state/symbolicFragment.ml @@ -98,6 +98,8 @@ module type S = sig type t = | Read of Block.t * var (** From [Block.t], read [var] *) | Write of Block.t * exp (** To [Block.t], write [exp] *) + + val pp : t -> Pp.document end (** The type of a memory fragment *) diff --git a/src/trace/base.ml b/src/trace/base.ml index eb0a88b0..2419e7b7 100644 --- a/src/trace/base.ml +++ b/src/trace/base.ml @@ -93,6 +93,7 @@ module Var = struct | Register of Reg.t (** The value of the register at the beginning of the trace *) | Read of int * Ast.Size.t (** The result of that memory reading operation *) | NonDet of int * Ast.Size.t (** Variable representing non-determinism in the spec *) + | Segment of string * int (** Variable representing symbolic segment in the opcode *) (** Convert the variable to the string encoding. For parsing infractructure reason, the encoding must always contain at least one [:]. *) @@ -104,6 +105,8 @@ module Var = struct | NonDet (num, size) -> if size = Ast.Size.B64 then Printf.sprintf "nondet:%i" num else Printf.sprintf "nondet:%i:%dbits" num (Ast.Size.to_bits size) + | Segment (name, bits) -> + Printf.sprintf "segment:%s:%dbits" name bits (** Inverse of {!to_string} *) let of_string s = @@ -117,6 +120,9 @@ module Var = struct | ["nondet"; num; size] -> let size = Scanf.sscanf size "%dbits" Ast.Size.of_bits in NonDet (int_of_string num, size) + | ["segment"; name; bits] -> + let bits = Scanf.sscanf bits "%dbits" Fun.id in + Segment (name, bits) | _ -> Raise.inv_arg "%s is not a Base.Var.t" s (** Pretty prints the variable *) @@ -130,6 +136,7 @@ module Var = struct | Register reg -> Reg.reg_type reg | Read (_, size) -> Ast.Ty_BitVec (Ast.Size.to_bits size) | NonDet (_, size) -> Ast.Ty_BitVec (Ast.Size.to_bits size) + | Segment (_, bits) -> Ast.Ty_BitVec bits let of_reg reg = Register reg end @@ -248,17 +255,27 @@ let write_to_valu vc valu exp = match valu with Isla.(RegVal_Base (Val_Symbolic i)) -> HashVector.set vc i exp | _ -> () (** Convert an isla event to Trace events, most events are deleted *) -let events_of_isla ~written_registers ~read_counter ~(vc : value_context) : +let events_of_isla ~segments_map ~written_registers ~read_counter ~(vc : value_context) : Isla.revent -> event list = function | Smt (DeclareConst (i, ty), _) -> - ( try - match ty with - | Ty_BitVec ((8 | 16 | 32 | 64 | 128) as size) -> - HashVector.set vc i (Exp.of_var (Var.NonDet (i, Ast.Size.of_bits size))) - | Ty_BitVec _ | Ty_Bool | Ty_Enum _ | Ty_Array (_, _) -> - debug "Unimplemented: ignoring non-det variable %i of type %t" i - (Pp.top Isla.pp_ty ty) - with OfIslaError -> warn "not setting nondet:%d" i + ( match HashVector.get_opt segments_map i with + | Some (name, size) -> + let ty_match = match ty with + | Ty_BitVec sz -> size = sz + | _ -> false + in + if not ty_match then fatal "Variable type doesn't match instruction segment %t and %d" (Pp.top Isla.pp_ty ty) size + else + HashVector.set vc i (Exp.of_var (Var.Segment (name, size))) + | None -> + try + match ty with + | Ty_BitVec ((8 | 16 | 32 | 64 | 128) as size) -> + HashVector.set vc i (Exp.of_var (Var.NonDet (i, Ast.Size.of_bits size))) + | Ty_BitVec _ | Ty_Bool | Ty_Enum _ | Ty_Array (_, _) -> + debug "Unimplemented: ignoring non-det variable %i of type %t" i + (Pp.top Isla.pp_ty ty) + with OfIslaError -> warn "not setting nondet:%d" i ); [] | Smt (DefineConst (i, e), _) -> @@ -321,11 +338,15 @@ let events_of_isla ~written_registers ~read_counter ~(vc : value_context) : | AbstractPrimop _ -> [] (** Top level function to convert an isla trace to one of this module *) -let of_isla (Trace events : Isla.rtrc) : t = +let of_isla (segments: Isla.segment list) (Trace events : Isla.rtrc) : t = let written_registers = Hashtbl.create 10 in let read_counter = Counter.make 0 in let vc = HashVector.empty () in - List.concat_map (events_of_isla ~written_registers ~read_counter ~vc) events + let segments_map = HashVector.empty () in + List.iter (fun (Isla.Segment (name, size, var)) -> + HashVector.set segments_map var (name, size) + ) segments; + List.concat_map (events_of_isla ~segments_map ~written_registers ~read_counter ~vc) events (*****************************************************************************) (*****************************************************************************) @@ -345,7 +366,7 @@ let declare_non_det serv events = iter_var (function | Register _ | Read _ -> () - | NonDet _ as var -> + | NonDet _ | Segment _ as var -> if not @@ VarTbl.mem declared @@ var then begin Z3Tr.declare_var_always serv var; VarTbl.add declared var () diff --git a/src/trace/cache.ml b/src/trace/cache.ml index 366f7bea..7cb5625d 100644 --- a/src/trace/cache.ml +++ b/src/trace/cache.ml @@ -155,17 +155,23 @@ let get_cache () = match !cache with Some cache -> cache | None -> failwith "Trace cache was not started" (** Get the traces of the opcode given. Use {!Isla.Server} if the value is not in the cache *) -let get_traces (opcode : BytesSeq.t) : Base.t list = +let get_traces (opcode : Isla.Server.opcode) : Base.t list = let cache = get_cache () in match TC.get_opt cache (Some opcode) with | Some trcs -> trcs | None -> - let isla_traces = Isla.Cache.get_traces opcode in - let traces = List.map (tee (Isla.Type.type_trc %> ignore) %> Base.of_isla) isla_traces in + let segments, isla_traces = match Isla.Cache.get_traces opcode with + | Traces t -> [], t + | TracesWithSegments (Segments s, t) -> s, t + in + let traces = List.map (tee (Isla.Type.type_trc %> ignore) %> Base.of_isla segments) isla_traces in let straces = List.map Base.simplify traces in TC.add cache (Some opcode) straces; straces (** Get a full blown {!Instr} from the opcode, going through the whole Isla pipeline if necessary.*) -let get_instr (opcode : BytesSeq.t) : Instr.t = Instr.of_traces opcode @@ get_traces opcode +let get_instr (opcode : BytesSeq.t * Elf.Relocations.rel option) : Instr.t = + let raw_opcode, reloc = opcode in + let reloc_target = Option.map (fun (x : Elf.Relocations.rel) -> x.target) reloc in + Instr.of_traces opcode @@ get_traces (raw_opcode, reloc_target) diff --git a/src/trace/context.ml b/src/trace/context.ml index cd8b46be..59950dc2 100644 --- a/src/trace/context.ml +++ b/src/trace/context.ml @@ -48,33 +48,67 @@ should be added here *) +open Logs.Logger (struct + let str = __MODULE__ +end) + +module SMap = Map.Make (String) + (** The context to run a trace *) type t = { reg_writes : (State.Reg.t * State.tval) Vec.t; (** Stores the delayed register writes *) mem_reads : State.tval HashVector.t; (** Stores the result of memory reads *) + nondets : State.var HashVector.t; (** Stores the mapping of nondet variables *) state : State.t; + segments : State.exp SMap.t; + asserts: State.exp list; dwarf : Dw.t option; (** Optionally DWARF information. If present, typing is enabled *) } (** Build a {!context} from a state *) -let make_context ?dwarf state = +let make_context ?dwarf ?relocation state = let reg_writes = Vec.empty () in let mem_reads = HashVector.empty () in - { state; reg_writes; mem_reads; dwarf } + let nondets = HashVector.empty () in + + let segments, asserts = relocation + |> Option.map (fun relocation -> + let State.Relocation.{value;asserts;target} = State.Relocation.of_elf relocation in + List.iter (State.push_relocation_assert state) asserts; + + (target + |> Isla.Relocation.segments_of_reloc + |> SMap.of_list + |> SMap.map (fun (first, last) -> Exp.Typed.extract ~first ~last value), + asserts) + ) + |> Option.value ~default:(SMap.empty, []) + in + { state; reg_writes; mem_reads; nondets; dwarf; segments; asserts } (** Expand a Trace variable to a State expression, using the context *) let expand_var ~(ctxt : t) (v : Base.Var.t) (a : Ast.no Ast.ty) : State.exp = assert (Base.Var.ty v = a); match v with | Register reg -> State.get_reg_exp ctxt.state reg - | NonDet (i, _) | Read (i, _) -> (HashVector.get ctxt.mem_reads i).exp - -let map_var ~(ctxt : t) (v : Base.Var.t) (a : Ast.no Ast.ty) : State.var = - assert (Base.Var.ty v = a); - match v with - | Register reg -> State.Var.Register (ctxt.state.id, reg) - | NonDet (i, size) -> State.Var.NonDet (i, size) - | Read (i, size) -> State.Var.ReadVar (ctxt.state.id, i, size) + | NonDet (i, sz) -> HashVector.get_opt ctxt.nondets i + |> Option.value_fun ~default:(fun () -> + Fun.tee (HashVector.add ctxt.nondets i) (State.Var.new_nondet sz) + ) + |> State.Exp.of_var + | Read (i, _) -> (HashVector.get ctxt.mem_reads i).exp (* TODO is the NonDet case correct *) + | Segment (name, _) -> SMap.find name ctxt.segments (*TODO put the actual value there*) + (* | Segment (name, sz) -> Exp.Typed.extract ~first:0 ~last:(sz-1) (State.Exp.of_var (State.Var.Section name)) TODO put the actual value there *) (** Tell if typing should enabled with this context *) let typing_enabled ~(ctxt : t) = ctxt.dwarf <> None + +module Z3St = State.Simplify.Z3St + +let simplify ~(ctxt : t) (exp : State.exp) : State.exp = + debug "Before simplification: %t" (Pp.top State.Exp.pp exp); + debug "Before simplification: %t" (Pp.top State.Exp.pp (Z3St.simplify_full exp)); + exp + |> Z3St.simplify_subterms_full ~hyps:ctxt.asserts + |> Z3St.simplify_full + |> Fun.tee (fun e -> debug "After simplification: %t" (Pp.top State.Exp.pp e)) \ No newline at end of file diff --git a/src/trace/instr.ml b/src/trace/instr.ml index 3dd01196..e53848b1 100644 --- a/src/trace/instr.ml +++ b/src/trace/instr.ml @@ -60,6 +60,8 @@ type trace_meta = { written : Reg.t list; } +module SMap = Map.Make (String) + (** A full instruction representation *) type t = { traces : trace_meta list; @@ -67,6 +69,7 @@ type t = { read : Reg.t list; written : Reg.t list; opcode : BytesSeq.t; + relocation : Elf.Relocations.rel option; } let dedup_regs = List.sort_uniq State.Reg.compare @@ -81,7 +84,7 @@ let trace_meta_of_trace trace = let jump = ref None in let process_var = function | Base.Var.Register reg -> read := reg :: !read - | Base.Var.(Read _ | NonDet _) -> () + | Base.Var.(Read _ | NonDet _ | Segment _) -> () in let process_exp : Base.exp -> unit = Ast.Manip.exp_iter_var process_var in let process_event : Base.event -> unit = function @@ -99,16 +102,18 @@ let trace_meta_of_trace trace = { trace; jump_target = !jump; read = dedup_regs !read; written = dedup_regs !written } (** Generate full instruction data from a list of traces *) -let of_traces opcode traces = +let of_traces ((opcode: BytesSeq.t), (relocation: Elf.Relocations.rel option)) traces = let traces = List.map trace_meta_of_trace traces in let length = BytesSeq.length opcode in let read = dedup_regs @@ List.concat_map (fun (tr : trace_meta) -> tr.read) traces in let written = dedup_regs @@ List.concat_map (fun (tr : trace_meta) -> tr.written) traces in - { traces; length; read; written; opcode } + + { traces; length; read; written; opcode; relocation } (** Pretty print the representation of an instruction *) let pp instr = let open Pp in + !^"Relocation" ^^ optional Elf.Relocations.pp_rel instr.relocation ^^ hardline ^^ separate_mapi hardline (fun i trc -> prefix 4 1 (dprintf "Trace %d:" i) (Base.pp trc.trace)) instr.traces diff --git a/src/trace/run.ml b/src/trace/run.ml index bd8eb38d..5298484f 100644 --- a/src/trace/run.ml +++ b/src/trace/run.ml @@ -64,16 +64,20 @@ type ctxt = Ctxt.t let expand ~(ctxt : ctxt) (exp : Base.exp) : State.exp = Ast.Manip.exp_var_subst (Ctxt.expand_var ~ctxt) exp +let expand_simplify ~(ctxt : ctxt) (exp : Base.exp) : State.exp = + exp |> expand ~ctxt |> Context.simplify ~ctxt + (** Expand a Trace expression to a typed State expression, using the context. If the context enables typing, the expression will actually be typed, otherwise the type will be [None] *) let expand_tval ~(ctxt : ctxt) (exp : Base.exp) : State.tval = - let sexp = expand ~ctxt exp in + let sexp = expand_simplify ~ctxt exp in if Ctxt.typing_enabled ~ctxt then let ctyp = Typer.expr ~ctxt exp in { ctyp; exp = sexp } - else { ctyp = None; exp = sexp } + else + { ctyp = None; exp = sexp } (** Run the event. The modified state is the one inside [ctxt]. *) @@ -83,41 +87,49 @@ let event_mut ~(ctxt : ctxt) (event : Base.event) = match event with | WriteReg { reg; value } -> Vec.add_one ctxt.reg_writes (reg, expand_tval ~ctxt value) | ReadMem { addr; value; size } -> - let naddr = expand ~ctxt addr in + let naddr = expand_simplify ~ctxt addr in + debug "naddr: %t" (Pp.top State.Exp.pp naddr); + let ptrtype = Typer.expr ~ctxt addr in + debug "ptrtype: %t" Pp.(top (optional Ctype.pp) ptrtype); let tval = match ctxt.dwarf with | Some dwarf -> - let ptrtype = Typer.expr ~ctxt addr in Typer.read ~dwarf ctxt.state ?ptrtype ~addr:naddr ~size - | None -> State.read_noprov ctxt.state ~addr:naddr ~size |> State.Tval.of_exp + | None -> + State.read_noprov ctxt.state ~addr:naddr ~size |> State.Tval.of_exp in + debug "read value: %t" Pp.(top State.Tval.pp tval); HashVector.set ctxt.mem_reads value tval | WriteMem { addr; value; size } -> ( - let naddr = expand ~ctxt addr in + let naddr = expand_simplify ~ctxt addr in + debug "naddr: %t" (Pp.top State.Exp.pp naddr); + let ptrtype = Typer.expr ~ctxt addr in + debug "ptrtype: %t" Pp.(top (optional Ctype.pp) ptrtype); match ctxt.dwarf with | Some dwarf -> let ptrtype = Typer.expr ~ctxt addr in debug "Typed write mem with ptr:%t" (Pp.top (Pp.opt Ctype.pp) ptrtype); let value = expand_tval ~ctxt value in + debug "written value: %t" Pp.(top State.Tval.pp value); Typer.write ~dwarf ctxt.state ?ptrtype ~addr:naddr ~size value | None -> - let value = expand ~ctxt value in + let value = expand_simplify ~ctxt value in State.write_noprov ctxt.state ~addr:naddr ~size value ) - | Assert exp -> State.push_assert ctxt.state (expand ~ctxt exp) + | Assert exp -> State.push_assert ctxt.state (expand_simplify ~ctxt exp) (** Run a trace on the provided state by mutation. Enable typing if [dwarf] is provided *) -let trace_mut ?dwarf (state : State.t) (events : Base.t) : unit = +let trace_mut ?dwarf ?relocation (state : State.t) (events : Base.t) : unit = assert (not @@ State.is_locked state); info "Running trace with typing %s" (if dwarf <> None then "on" else "off"); - let ctxt = Context.make_context ?dwarf state in + let ctxt = Context.make_context ?dwarf ?relocation state in List.iter (event_mut ~ctxt) events; Vec.iter (fun (reg, tval) -> State.Reg.Map.set state.regs reg tval) ctxt.reg_writes (** Run a trace on the provided state by returning an updated copy.*) -let trace ?dwarf (start : State.t) (events : Base.t) : State.t = +let trace ?dwarf ?relocation (start : State.t) (events : Base.t) : State.t = let state = State.copy start in - trace_mut ?dwarf state events; + trace_mut ?dwarf ?relocation state events; State.lock state; state @@ -126,12 +138,12 @@ let trace ?dwarf (start : State.t) (events : Base.t) : State.t = Thus this function automatically handle moving the PC for fall-through instruction *) -let trace_pc_mut ?dwarf ~(next : int) (state : State.t) (events : Base.t) : unit = +let trace_pc_mut ?dwarf ?relocation ~(next : int) (state : State.t) (events : Base.t) : unit = let pc = Arch.pc () in let rec is_touching_pc : Base.t -> bool = function | [] -> false | WriteReg { reg; _ } :: _ when reg = pc -> true | _ :: l -> is_touching_pc l in - trace_mut ?dwarf state events; + trace_mut ?dwarf ?relocation state events; if is_touching_pc events then State.concretize_pc ~pc state else State.bump_pc ~pc state next diff --git a/src/trace/typer.ml b/src/trace/typer.ml index e83f3284..2dd8e1a2 100644 --- a/src/trace/typer.ml +++ b/src/trace/typer.ml @@ -1,4 +1,4 @@ -(*==================================================================================*) +(* ================================================================================== *) (* BSD 2-Clause License *) (* *) (* Copyright (c) 2020-2021 Thibaut Pérami *) @@ -98,6 +98,24 @@ let machine_of_size ?(update = 0) (typ : Ctype.t) : Ctype.t = let constexpr = typ.constexpr in Ctype.machine ~constexpr (size + update) +let is_const tval = + tval.ctyp + |> Option.map Ctype.is_constexpr + |> Option.value_fun ~default:(fun () -> Exp.ConcreteEval.is_concrete tval.exp) + +let constexpr_of_exp e = + let ty = Exp.Typed.get_type e in + if Exp.Typed.is_bv ty then + let bitsize = Exp.Typed.expect_bv ty in + Option.some @@ + if bitsize mod 8 = 0 || bitsize = Arch.address_size then + Ctype.machine ~constexpr:true (bitsize / 8) + else + Ctype.Bits |> Ctype.qual ~constexpr:true + else + None + + let unop (u : Ast.unop) tval : Ctype.t option = let open Option in let* typ = tval.ctyp in @@ -106,7 +124,8 @@ let unop (u : Ast.unop) tval : Ctype.t option = | Bvneg | Bvnot -> machine_of_size typ |> some | Extract (b, a) -> debug "Extracting from type %t" Pp.(top (opt Ctype.pp) tval.ctyp); - if (* HACK for adrp: a = 0 && b = Arch.address_size - 1 &&*) Ctype.is_ptr typ then tval.ctyp + if (* HACK for adrp: a = 0 && b = Arch.address_size - 1 &&*) Ctype.is_ptr typ then + tval.ctyp else let bitsize = b - a + 1 in let constexpr = typ.constexpr in @@ -178,7 +197,7 @@ let manyop ~ctxt (m : Ast.manyop) (tvals : tval list) : Ctype.t option = match List.hd tvals with | { exp = Unop (Extract (_, _), _, _); - ctyp = Some ({ unqualified = Ptr { fragment = Global; offset; _ }; _ } as ctyp); + ctyp = Some ({ unqualified = Ptr { fragment = Global _; offset; _ }; _ } as ctyp); } -> ( match offset with | Somewhere -> Some ctyp @@ -203,6 +222,7 @@ let rec expr ~ctxt (exp : Base.exp) : Ctype.t option = | Var (Register reg, _) -> State.get_reg ctxt.state reg |> State.Tval.ctyp | Var (Read (r, _), _) -> HashVector.get ctxt.mem_reads r |> State.Tval.ctyp | Var (NonDet _, _) -> None + | Var (Segment _, _) -> None (* TODO? *) | Bits (bv, _) -> let size = BitVec.size bv in if size mod 8 = 0 || size = Arch.address_size then @@ -211,12 +231,37 @@ let rec expr ~ctxt (exp : Base.exp) : Ctype.t option = | Bool _ -> None | Enum _ -> None | Vec _ -> None - | Unop (u, e, _) -> expr_tval ~ctxt e |> unop u + | Unop (u, e, _) -> + let tval = expr_tval ~ctxt e in + Option.( + unop u tval + ||| + if is_const tval then + constexpr_of_exp exp + else + None + ) | Binop (b, e, e', _) -> let te = expr_tval ~ctxt e in let te' = expr_tval ~ctxt e' in - binop ~ctxt b te te' - | Manyop (m, el, _) -> List.map (expr_tval ~ctxt) el |> manyop ~ctxt m + Option.( + binop ~ctxt b te te' + ||| + if is_const te && is_const te' then + constexpr_of_exp exp + else + None + ) + | Manyop (m, el, _) -> + let tvals = List.map (expr_tval ~ctxt) el in + Option.( + manyop ~ctxt m tvals + ||| + if List.for_all is_const tvals then + constexpr_of_exp exp + else + None + ) | Ite _ -> None | Bound _ -> . | Let _ -> . @@ -254,8 +299,8 @@ let fragment_at ~(dwarf : Dw.t) ~fenv ~size (frag : Ctype.fragment) at : Ctype.t let frag = Fragment.Env.get fenv i in let* (typ, off) = Fragment.at_off_opt frag at in Ctype.type_at ~env ~size typ off - | Global -> ( - match Elf.SymTable.of_addr_with_offset_opt dwarf.elf.symbols at with + | Global s -> ( + match Elf.SymTable.of_addr_with_offset_opt dwarf.elf.symbols Elf.Address.{ section = s; offset = at } with | Some (sym, offset) -> ( match Hashtbl.find_opt dwarf.vars sym.name with | Some v -> Ctype.type_at ~env ~size v.ctype offset diff --git a/src/utils/fullVec.ml b/src/utils/fullVec.ml index f6bea2c1..998e2232 100644 --- a/src/utils/fullVec.ml +++ b/src/utils/fullVec.ml @@ -107,6 +107,11 @@ let map f fv = let gen = fv.gen %> f in { vec; gen } +let mapi f fv = + let vec = Vec.mapi f fv.vec in + let gen = (fun i -> fv.gen i |> f i) in + { vec; gen } + let map_mut f fv = Vec.map_mut f fv.vec; fv.gen <- fv.gen %> f diff --git a/src/utils/fullVec.mli b/src/utils/fullVec.mli index 51d9f079..9a67676f 100644 --- a/src/utils/fullVec.mli +++ b/src/utils/fullVec.mli @@ -89,6 +89,9 @@ val get_vec_until : 'a t -> int -> 'a Vec.t (** Map the function over the fullvec. Postcompose the map on the generator *) val map : ('a -> 'b) -> 'a t -> 'b t +(** Same as {!map} but with the index *) +val mapi : (int -> 'a -> 'b) -> 'a t -> 'b t + (** Map the function over the fullvector by mutation. Postcompose the map on the generator.contents Warning, a lot of {!map_mut} may make the generator big and slow. Maybe try to use {!set_after} to reset it when required.*) diff --git a/src/utils/list.ml b/src/utils/list.ml index 5eae6c30..6eb978ca 100644 --- a/src/utils/list.ml +++ b/src/utils/list.ml @@ -298,3 +298,17 @@ let prod l1 l2 = (** Monadic merge. [let* x = xl and* y = yl in ... = let* x= xl in let* y = yl in ...] *) let ( and* ) = prod + +let hd_opt = function +| [] -> None +| h :: _ -> Some h + +let rec transpose ~defaults l = + let first = map hd_opt l in + let rest = map (drop 1) l in + if for_all Stdlib.Option.is_none first then + [] + else + let t = transpose ~defaults rest in + let h = combine first defaults |> map (fun (value, default) -> Stdlib.Option.value ~default value) in + h :: t diff --git a/src/utils/rngMap.ml b/src/utils/rngMap.ml index 1e81ad21..42f872cb 100644 --- a/src/utils/rngMap.ml +++ b/src/utils/rngMap.ml @@ -303,14 +303,20 @@ module Make (Obj : LenObject) : S with type obj = Obj.t = struct let clear_crop t ~pos ~len ~crop = assert (len >= 0); (* Crop an possible object starting before the start but ending after the start. *) + let endp = pos + len in let t = match prev t (pos - 1) with | Some (addr, obj) when addr + Obj.len obj > pos -> + let objend = addr + Obj.len obj in + let t = if endp < objend then + IMap.add (pos + len) (crop ~pos:(endp - addr) ~len:(objend - endp) obj) t + else + t + in IMap.update addr (Option.map (crop ~pos:0 ~len:(pos - addr))) t | _ -> t in let seq = IMap.to_seq_from pos t in - let endp = pos + len in (* Remove all objects of the sequence from t until endp *) let rec remove_until t seq endp = match seq () with diff --git a/src/utils/sym.ml b/src/utils/sym.ml new file mode 100644 index 00000000..83421beb --- /dev/null +++ b/src/utils/sym.ml @@ -0,0 +1,62 @@ +type t = Sym_ocaml.Num.t + +let pp x = x |> Dwarf.pphex_sym |> Pp.string + +let to_z x = Sym_ocaml.Num.to_num x + +let to_int x = Z.to_int @@ to_z x + +let of_int x = Sym_ocaml.Num.Absolute (Z.of_int x) +let of_int64 x = Sym_ocaml.Num.Absolute (Z.of_int64 x) + +let equal = Sym_ocaml.Num.equal + +let max_addr = Z.(shift_left (of_int 1) 64 - (of_int 1)) + +let min_addr = Z.of_int 0 + +(* TODO very hacky *) +let compare x y = match (x, y) with +| (Sym_ocaml.Num.Absolute x, Sym_ocaml.Num.Offset (_, y)) when Nat_big_num.less x y -> -1 +| (Sym_ocaml.Num.Absolute x, Sym_ocaml.Num.Offset (_, _)) when Nat_big_num.greater_equal x max_addr -> 1 +| (Sym_ocaml.Num.Offset (_, x), Sym_ocaml.Num.Absolute y) when Nat_big_num.less y x -> 1 +| (Sym_ocaml.Num.Offset (_, _), Sym_ocaml.Num.Absolute y) when Nat_big_num.greater_equal y max_addr -> -1 +| (x, y) -> Sym_ocaml.Num.compare x y + +let less x y = compare x y < 0 +let less_equal x y = compare x y <= 0 +(* let equal x y = compare x y = 0 *) +let greater x y = compare x y > 0 +let greater_equal x y = compare x y >= 0 + +let to_string = Sym_ocaml.Num.ppf Z.to_string + +let sub = Sym_ocaml.Num.sub + +let add = Sym_ocaml.Num.add + +let mul = Sym_ocaml.Num.mul + +let pow_int_positive x y = Sym_ocaml.Num.Absolute (Nat_big_num.pow_int_positive x y) + +let shift_left x s = Sym_ocaml.Num.map (fun x -> Nat_big_num.shift_left x s) x +let shift_right x s = Sym_ocaml.Num.map (fun x -> Nat_big_num.shift_right x s) x +let modulus = Sym_ocaml.Num.map2 Nat_big_num.modulus + +let in_range first last x = match (first, last, x) with +| (Sym_ocaml.Num.Absolute f, Sym_ocaml.Num.Absolute l, Sym_ocaml.Num.Absolute x) -> Nat_big_num.less_equal f x && Nat_big_num.less_equal x l +| (Sym_ocaml.Num.Offset (s1, f), Sym_ocaml.Num.Offset (s2, l), Sym_ocaml.Num.Offset (s, x)) when s1 = s2 -> + s1 = s && Nat_big_num.less_equal f x && Nat_big_num.less_equal x l (* TODO kinda hacky *) +| _ -> Raise.fail "Can't determine if %t is in range [%t,%t]" (Pp.tos pp x) (Pp.tos pp first) (Pp.tos pp last) + +module Ordered = struct + let compare x y = match (x, y) with + | (Sym_ocaml.Num.Offset (s1, _x), Sym_ocaml.Num.Offset (s2, _y)) when s1 <> s2 -> String.compare s1 s2 + | (x, y) -> compare x y + + let less_equal x y = compare x y <= 0 + let less x y = compare x y < 0 + let greater x y = compare x y > 0 + let greater_equal x y = compare x y >= 0 + let equal x y = compare x y = 0 +end \ No newline at end of file diff --git a/src/z3/z3.ml b/src/z3/z3.ml index 45321719..52c31a95 100644 --- a/src/z3/z3.ml +++ b/src/z3/z3.ml @@ -395,6 +395,10 @@ module type S = sig This results in two calls to the SMT solver. one with {!check} and one with {!check_sat} *) val check_both : server -> exp -> bool option + val simplify_subterms : server -> exp -> exp + + val simplify_subterms_decl : server -> declared:unit Htbl.t -> exp -> exp + (*****************************************************************************) (*****************************************************************************) (*****************************************************************************) @@ -415,6 +419,8 @@ module type S = sig (** Do a standalone check of whether the set of assertion is sat *) val check_sat_full : exp list -> bool option + + val simplify_subterms_full : ?hyps:exp list -> exp -> exp end module SimpContext = ContextCounter (struct @@ -516,4 +522,70 @@ module Make (Var : Var) : S with type var = Var.t = struct | _ -> ( match check_sat serv e with Some false as f -> f | _ -> None ) + + + let rec simplify_subterms serv (e : Exp.t) : Exp.t = + e |> Ast.Manip.all_subterms + |> List.find_opt (fun t -> + Typed.get_type e = Typed.get_type t && + let result = check serv Typed.(e = t) in + result = Some true + ) + |> Option.map (simplify_subterms serv) + |> Option.value_fun ~default:(fun () -> + Ast.Manip.direct_exp_map_exp (simplify_subterms serv) e + ) + + let simplify_subterms_decl serv ~declared (e : Exp.t) : Exp.t = + declare_vars serv ~declared e; + simplify_subterms serv e + + let simplify_subterms_full ?(hyps = []) e = + let serv = ensure_started_get () in + SimpContext.openc (); + let declared = Htbl.create 10 in + List.iter (send_assert_decl ~declared serv) hyps; + let res = simplify_subterms_decl ~declared serv e in + SimpContext.closec (); + res +end + +module Test = struct + module Var = struct + include String + + let pp = Pp.string + + let ty _ = Ast.Ty_BitVec 64 + + let of_string = Fun.id + end + + module Typed = Exp.Typed + module Exp = Exp.Make (Var) + + module Z3Test = Make (Var) + + let test () = + let x = Typed.var ~typ:(Ast.Ty_BitVec 64) "x" in + let bvint64 = Typed.bits_int ~size:64 in + let constr = Typed.(binop (Ast.Bvcomp Ast.Bvult) x (bvint64 16)) in + let exp = Typed.(concat [bits_int ~size:60 0; extract x ~first:0 ~last:3]) in + let simplified = Z3Test.simplify_subterms_full ~hyps:[constr] exp in + Printf.printf "original: %t\n" (Pp.top Exp.pp exp); + Printf.printf "simplified: %t\n" (Pp.top Exp.pp simplified); + + + open Cmdliner + open Config.CommonOpt + + + let term = Term.(CmdlinerHelper.func_options (config :: z3 :: comopts) test $ const ()) + + let info = + let doc = "" + in + Cmd.(info "z3-test" ~doc ~exits) + + let command = (term, info) end