diff options
| -rw-r--r-- | checklink/Check.ml | 267 | ||||
| -rw-r--r-- | checklink/ELF_parsers.ml | 107 | ||||
| -rw-r--r-- | checklink/ELF_types.ml | 123 | ||||
| -rw-r--r-- | checklink/ELF_utils.ml | 90 | ||||
| -rw-r--r-- | checklink/Frameworks.ml | 4 | ||||
| -rw-r--r-- | checklink/Library.ml | 14 | ||||
| -rw-r--r-- | checklink/PPC_utils.ml | 25 | ||||
| -rw-r--r-- | checklink/Validator.ml | 9 |
8 files changed, 354 insertions, 285 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml index 9282f5e..0483a89 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -538,21 +538,19 @@ let rec match_jmptbl lbllist vaddr size ffw = ) in let elf = ffw.sf.ef.elf in - let cur_sym_ndx = elf.e_symtab.(ffw.this_sym_ndx).st_shndx in - begin match bitstring_at_vaddr elf cur_sym_ndx vaddr size with - | None -> ERR("Symbol out of its parent section") - | Some(bs) -> - begin match section_at_vaddr elf vaddr with - | None -> ERR("Jumptable's virtual address is out of any section") - | Some(sndx) -> - let ofs = physical_offset_of_vaddr elf sndx vaddr in + begin match section_at_vaddr elf vaddr with + | None -> ERR("No section for the jumptable") + | Some(sndx) -> + begin match bitstring_at_vaddr elf vaddr size with + | None -> ERR("") + | Some(bs, pofs, psize) -> ffw >>> (ff_sf ^%= match_sections_name jmptbl_section elf.e_shdra.(sndx).sh_name ) >>> match_jmptbl_aux lbllist bs >>? (ff_ef ^%= - add_range ofs (Safe32.of_int (size / 8)) 0 Jumptable) + add_range pofs psize 0 Jumptable) end end @@ -798,8 +796,15 @@ let check_sda ident ofs r addr ffw: f_framework or_err = let rec compare_code ccode ecode pc fw: f_framework or_err = let error = ERR("Non-matching instructions") in match ccode, ecode with - | [], [] -> OK(fw) - | [], _ | _, [] -> ERR("Codes have different lengths") + | [], [] -> OK(fw) + | [], e_rest -> + let rest_str = String.concat "\n" (List.map string_of_instr e_rest) in + ERR("CompCert code exhausted before the end of ELF code, remaining:\n" + ^ rest_str) + | c_rest, [] -> + let rest_str = String.concat "\n" (List.map string_of_instruction c_rest) in + ERR("ELF code exhausted before the end of CompCert code, remaining:\n" + ^ rest_str) | c::cs, e::es -> let recur_simpl = compare_code cs es (Int32.add 4l pc) in let fw = @@ -1087,7 +1092,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = let tblvaddr = Int32.( add (shift_left (Safe32.of_int simm0) 16) (exts d1) ) in - let tblsize = (32 * List.length table) in + let tblsize = Safe32.of_int (32 * List.length table) in fw >>> match_iregs GPR12 rD0 >>> match_iregs reg rA0 @@ -1777,33 +1782,28 @@ let rec compare_code ccode ecode pc fw: f_framework or_err = | _ -> Section_literal end in - begin match section_at_vaddr elf vaddr with - | None -> - ERR("Float literal's virtual address out of any section") - | Some(sndx) -> - let section_bitstring = bitstring_at_vaddr elf sndx in - let f = ( - let bs = - begin match section_bitstring vaddr 64 with - | None -> assert false - | Some(bs) -> bs - end - in + begin match bitstring_at_vaddr elf vaddr 64l with + | None -> assert false + | Some(bs, pofs, psize) -> + let f = bitmatch bs with | { f : 64 : int } -> Int64.float_of_bits f - ) in - let ofs = physical_offset_of_vaddr elf sndx vaddr in + in fw >>> (ff_sf ^%= - match_sections_name - literal_section - elf.e_shdra.(sndx).sh_name + begin match section_at_vaddr elf vaddr with + | None -> sf_ef ^%= add_log (ERROR("No section at that virtual address")) + | Some(sndx) -> + match_sections_name + literal_section + elf.e_shdra.(sndx).sh_name + end ) >>> match_iregs GPR12 rD0 >>> match_iregs GPR0 rA0 >>> match_fregs r1 frD1 >>> match_floats c f - >>> (ff_ef ^%= add_range ofs 8l 8 (Float_literal(f))) + >>> (ff_ef ^%= add_range pofs psize 8 (Float_literal(f))) >>> match_iregs GPR12 rA1 >>> compare_code cs es (Int32.add 8l pc) end @@ -2551,18 +2551,10 @@ let rec worklist_process (wl: worklist) sfw: s_framework = end end -(** This variant helps representing big empty bitstrings without allocating - memory. It is useful to create a bitstring for an STT_NOBITS symbol, for - instance. -*) -type maybe_bitstring = - | Empty of int - | NonEmpty of bitstring - (** Compares a data symbol with its expected contents. Returns the updated framework as well as the size of the data matched. **) -let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framework) +let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework) : (s_framework * int) or_err = let error = ERR("Reached end of data bitstring too soon") in let rec compare_data_aux l bs s (sfw: s_framework): @@ -2639,19 +2631,7 @@ let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framewor ) end in - let rec compare_data_empty l s (sfw: s_framework): - (s_framework * int) or_err = - match l with - | [] -> OK(sfw, s) - | d::l -> - begin match d with - | Init_space(z) -> compare_data_empty l (s + z_int z) sfw - | _ -> ERR("Expected empty data") - end - in - match maybebs with - | Empty(_) -> compare_data_empty l 0 sfw - | NonEmpty(bs) -> compare_data_aux l bs 0 sfw + compare_data_aux l bs 0 sfw (** Checks the data symbol table. *) @@ -2710,104 +2690,84 @@ let check_data_symtab ident sym_ndx size sfw = let check_data (pv: (ident * unit globvar) list) (sfw: s_framework) : s_framework = let process_ndx ident ldata sfw ndx = - let elf = (sfw |. sf_ef).elf in + let elf = sfw.ef.elf in let sym = elf.e_symtab.(ndx) in let sym_vaddr = sym.st_value in - let sym_size = sym.st_size in - let sym_sndx = sym.st_shndx in - let sym_bs_opt = - begin match elf.e_shdra.(sym_sndx).sh_type with - | SHT_NOBITS -> - Some(Empty(Safe.(of_int32 sym.st_size * 8))) - | SHT_PROGBITS -> - begin match bitstring_at_vaddr_nosize elf sym_sndx sym_vaddr with - | None -> None - | Some(bs) -> Some(NonEmpty(bs)) - end - | _ -> assert false - end - in - let res = - begin match sym_bs_opt with - | None -> ERR("Could not find symbol data for data symbol " ^ sym.st_name) - | Some(sym_bs) -> + begin match bitstring_at_vaddr_nosize elf sym_vaddr with + | None -> ERR("Could not find symbol data for data symbol " ^ sym.st_name) + | Some(sym_bs, pofs, psize) -> + let res = sfw >>> (sf_ef ^%= add_log (DEBUG("Processing data: " ^ sym.st_name))) >>> compare_data ldata sym_bs - end - in - match res with - | ERR(s) -> ERR(s) - | OK(sfw, size) -> - let sym_shdr = (sfw |. sf_ef).elf.e_shdra.(sym_sndx) in - let sym_ofs_local = Int32.sub sym_vaddr sym_shdr.sh_addr in - let sxn_ofs = sym_shdr.sh_offset in - let sym_begin = Int32.add sxn_ofs sym_ofs_local in - let align = - begin match (Hashtbl.find sfw.atoms ident).a_alignment with - | None -> 0 - | Some(a) -> a - end in - sfw.ef.chkd_data_syms.(ndx) <- true; - sfw - >>> ( - begin match sym_shdr.sh_type with - | SHT_NOBITS -> - id (* These occupy no space, for now we just forget them *) - | _ -> - sf_ef ^%= - add_range sym_begin sym_size align (Data_symbol(sym)) - end - ) - >>> ( - if not (is_well_aligned sym_ofs_local align) - then ( - sf_ef ^%= add_log (ERROR( - "Symbol not correctly aligned in the ELF file" - )) - ) - else id - ) - >>> check_data_symtab ident ndx size - >>> (fun sfw -> OK(sfw)) - in - let check_data_aux sfw ig = - let (ident, gv) = ig in - let init_data = gv.gvar_init in - let ident_ndxes = PosMap.find ident sfw.ident_to_sym_ndx in + begin match res with + | ERR(s) -> ERR(s) + | OK(sfw, size) -> + let align = + begin match (Hashtbl.find sfw.atoms ident).a_alignment with + | None -> 0 + | Some(a) -> a + end + in + sfw.ef.chkd_data_syms.(ndx) <- true; + sfw + >>> ( + if size = 0 + then id (* These occupy no space, for now we just forget them *) + else sf_ef ^%= + add_range pofs (Safe32.of_int size) align (Data_symbol(sym)) + ) + >>> ( + if not (is_well_aligned sym_vaddr align) + then ( + sf_ef ^%= add_log (ERROR( + "Symbol not correctly aligned in the ELF file" + )) + ) + else id + ) + >>> check_data_symtab ident ndx size + >>> (fun sfw -> OK(sfw)) + end + end + in + let check_data_aux sfw ig = + let (ident, gv) = ig in + let init_data = gv.gvar_init in + let ident_ndxes = PosMap.find ident sfw.ident_to_sym_ndx in (*print_endline ("Candidates: " ^ string_of_list id ", " (List.map (fun ndx -> fw.elf.e_symtab.(ndx).st_name) ident_ndxes));*) - let results = List.map (process_ndx ident init_data sfw) ident_ndxes in - let successes = filter_ok results in - match successes with - | [] -> - sfw - >>> sf_ef ^%= - add_log (ERROR( - "No matching data segment among candidates [" ^ - (string_of_list - (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_name) - ", " - ident_ndxes - ) ^ - "], Errors: [" ^ - string_of_list - (function OK(_) -> "" | ERR(s) -> s) - ", " - (List.filter (function ERR(_) -> true | _ -> false) results) - ^ "]" - )) - | [sfw] -> sfw - | fws -> - sfw - >>> sf_ef ^%= add_log (ERROR("Multiple matching data segments!")) - in - List.fold_left check_data_aux sfw + let results = List.map (process_ndx ident init_data sfw) ident_ndxes in + let successes = filter_ok results in + match successes with + | [] -> + sfw + >>> sf_ef ^%= + add_log (ERROR( + "No matching data segment among candidates [" ^ + (string_of_list + (fun ndx -> sfw.ef.elf.e_symtab.(ndx).st_name) + ", " + ident_ndxes + ) ^ + "], Errors: [" ^ + string_of_list + (function OK(_) -> "" | ERR(s) -> s) + ", " + (List.filter (function ERR(_) -> true | _ -> false) results) + ^ "]" + )) + | [sfw] -> sfw + | fws -> + sfw + >>> sf_ef ^%= add_log (ERROR("Multiple matching data segments!")) + in + List.fold_left check_data_aux sfw (* Empty lists mean the symbol is external, no need for check *) - (List.filter (fun (_, gv) -> gv.gvar_init <> []) pv) + (List.filter (fun (_, gv) -> gv.gvar_init <> []) pv) (** Checks that everything that has been assimiled as a stub during checks indeed looks like a stub. @@ -2825,8 +2785,7 @@ let check_stubs sfw = in let elf = sfw.ef.elf in let stub_ecode = from_some (code_at_vaddr elf vaddr 2) in - let stub_sndx = from_some (section_at_vaddr elf vaddr) in - let stub_offset = physical_offset_of_vaddr elf stub_sndx vaddr in + let stub_offset = from_some (physical_offset_of_vaddr elf vaddr) in begin match fundef with | (_, External(EF_external(dest_ident, _) as ef)) -> let args = (ef_sig ef).sig_args in @@ -3037,10 +2996,9 @@ let check_padding efw = if sym.st_shndx >= Array.length elf.e_shdra then false (* special section *) else - let offset = - physical_offset_of_vaddr elf sym.st_shndx sym.st_value - in - intersect (x, y) offset sym.st_size + match physical_offset_of_vaddr elf sym.st_value with + | None -> false + | Some(ofs) -> intersect (x, y) ofs sym.st_size ) (Array.to_list elf.e_symtab) ) @@ -3074,17 +3032,18 @@ let check_padding efw = | ((b1, e1, a1, n1) as h1) :: ((b2, e2, a2, n2) as h2) :: rest -> let pad_start = Int32.add e1 1l in let pad_stop = Int32.sub b2 1l in - if - pad_start = b2 (* if they are directly consecutive *) - || Safe.(of_int32 b2 - of_int32 e1) > a2 (* or if they are too far away *) - || not (is_padding efw.elf.e_bitstring - (Safe32.to_int pad_start) (Safe32.to_int pad_stop)) + if pad_start = b2 (* if they are directly consecutive *) + || Safe.(of_int32 b2 - of_int32 e1) > a2 (* or if they are too far away *) + || not (is_padding efw.elf.e_bitstring + (Safe32.to_int pad_start) (Safe32.to_int pad_stop)) then (* not padding *) if pad_start <= pad_stop - then check_padding_aux efw - ((pad_start, pad_stop, 0, unknown pad_start pad_stop) :: h1 :: accu) - (h2 :: rest) - else check_padding_aux efw (h1 :: accu) (h2 :: rest) + then + check_padding_aux efw + ((pad_start, pad_stop, 0, unknown pad_start pad_stop) :: h1 :: accu) + (h2 :: rest) + else + check_padding_aux efw (h1 :: accu) (h2 :: rest) else ( (* this is padding! *) check_padding_aux efw ((pad_start, pad_stop, 0, Padding) :: h1 :: accu) diff --git a/checklink/ELF_parsers.ml b/checklink/ELF_parsers.ml index de72d39..776b7d9 100644 --- a/checklink/ELF_parsers.ml +++ b/checklink/ELF_parsers.ml @@ -5,6 +5,16 @@ open ELF_utils open Library open PPC_parsers +(** Allows relaxations of the parser: + + 1. Any segment that has the same p_offset and p_memsz as another segment, + and a null p_filesz, will be considered as having a p_filesz equal to the + other segment. This allow symbol's contents resolution to succeed even in + the presence of a bootstrapping copy mechanism from one segment to the + other. +*) +let relaxed = ref false + exception Unknown_endianness (** Converts an elf endian into a bitstring endian *) @@ -305,30 +315,83 @@ let read_elf_bs (bs: bitstring): elf = check_overlaps e_shdra e_hdr; let symtab_sndx = section_ndx_by_name_noelf e_shdra ".symtab" in let e_symtab = ( - let symtab_shdr = e_shdra.(symtab_sndx) in - let symtab_strtab_sndx = symtab_shdr.sh_link in - let symtab_nb_ent = (Safe32.to_int symtab_shdr.sh_size / 16) in - Array.init symtab_nb_ent - (read_elf32_sym e_hdr - (section_bitstring_noelf bs e_shdra symtab_sndx) - (section_bitstring_noelf bs e_shdra (Safe32.to_int symtab_strtab_sndx))) + let symtab_shdr = e_shdra.(symtab_sndx) in + let symtab_strtab_sndx = symtab_shdr.sh_link in + let symtab_nb_ent = (Safe32.to_int symtab_shdr.sh_size / 16) in + Array.init symtab_nb_ent + (read_elf32_sym e_hdr + (section_bitstring_noelf bs e_shdra symtab_sndx) + (section_bitstring_noelf bs e_shdra (Safe32.to_int symtab_strtab_sndx))) ) in + let e_phdra = + let untweaked = Array.init e_hdr.e_phnum (read_elf32_phdr e_hdr bs) in + if !relaxed + then + Array.mapi + (fun ndx curr -> + if ndx < 1 + then curr + else + let prev = untweaked.(ndx - 1) in + if (curr.p_offset = prev.p_offset) + && (curr.p_memsz = prev.p_memsz) + then { curr with p_filesz = prev.p_filesz } + else curr + ) + untweaked + else untweaked + in + let e_sym_phdr = + let intervals = + Array.mapi + (fun ndx phdr -> (* (ndx, (start, stop), type) *) + (ndx, + (phdr.p_vaddr, Safe32.(phdr.p_vaddr + phdr.p_memsz - 1l)), + phdr.p_type + ) + ) + e_phdra + in + let intervals = Array.of_list ( + List.filter + (function (_, _, PT_LOAD) -> true | _ -> false) + (Array.to_list intervals) + ) in + Array.fast_sort (fun (_, (x, _), _) (_, (y, _), _) -> compare x y) intervals; + let lookup = + sorted_lookup + ( + fun (_, (a, b), _) v -> + if a <= v && v <= b + then 0 + else compare a v + ) + intervals + in + fun vaddr -> + begin match lookup vaddr with + | None -> None + | Some(ndx, (_, _), _) -> Some(ndx) + end + in + let e_syms_by_name = + let m = ref StringMap.empty in + for i = 0 to Array.length e_symtab - 1 do + let name = strip_versioning e_symtab.(i).st_name in + let list = try StringMap.find name !m with Not_found -> [] in + m := StringMap.add name (i :: list) !m + done; + !m + in { - e_bitstring = bs; - e_hdr = e_hdr; - e_shdra = e_shdra; - e_phdra = Array.init e_hdr.e_phnum (read_elf32_phdr e_hdr bs); - e_symtab = e_symtab; - e_symtab_sndx = symtab_sndx; - e_syms_by_name = ( - let m = ref StringMap.empty in - for i = 0 to Array.length e_symtab - 1 do - let name = strip_versioning e_symtab.(i).st_name in - let list = try StringMap.find name !m with Not_found -> [] in - m := StringMap.add name (i :: list) !m - done; - !m - ); + e_bitstring = bs; + e_hdr = e_hdr; + e_shdra = e_shdra; + e_phdra = e_phdra; + e_symtab = e_symtab; + e_symtab_sndx = symtab_sndx; + e_sym_phdr = e_sym_phdr; + e_syms_by_name = e_syms_by_name; } (** Reads a whole ELF file from a file name *) diff --git a/checklink/ELF_types.ml b/checklink/ELF_types.ml index a6568ed..f67b91d 100644 --- a/checklink/ELF_types.ml +++ b/checklink/ELF_types.ml @@ -26,11 +26,11 @@ type ev = | EV_CURRENT | EV_UNKNOWN -type elf_identification = { - ei_class: elfclass; (* 32/64 bit *) - ei_data: elfdata; (* endianness *) - ei_version: ev; (* ELF header version *) -} +type elf_identification = + { ei_class : elfclass (* 32/64 bit *) + ; ei_data : elfdata (* endianness *) + ; ei_version : ev (* ELF header version *) + } (** ELF header *) @@ -59,22 +59,22 @@ let shn_UNDEF = 0 let shn_ABS = 0xFFF1 let shn_COMMON = 0xFFF2 -type elf32_ehdr = { - e_ident: elf_identification; (* Machine-independent data *) - e_type: et; (* Object file type *) - e_machine: em; (* Required architecture *) - e_version: ev; (* Object file version *) - e_entry: elf32_addr; (* Entry point virtual address *) - e_phoff: elf32_off; (* Program header table's offset *) - e_shoff: elf32_off; (* Section header table's offset *) - e_flags: Bitstring.bitstring; (* Processor-specific flags *) - e_ehsize: elf32_half; (* ELF header size *) - e_phentsize: elf32_half; (* Size of a program header's entry *) - e_phnum: elf32_half; (* Number of program header entries *) - e_shentsize: elf32_half; (* Size of a section header's entry *) - e_shnum: elf32_half; (* Number of section header entries *) - e_shstrndx: elf32_half; (* Section name string table index *) -} +type elf32_ehdr = + { e_ident : elf_identification (* Machine-independent data *) + ; e_type : et (* Object file type *) + ; e_machine : em (* Required architecture *) + ; e_version : ev (* Object file version *) + ; e_entry : elf32_addr (* Entry point virtual address *) + ; e_phoff : elf32_off (* Program header table's offset *) + ; e_shoff : elf32_off (* Section header table's offset *) + ; e_flags : Bitstring.bitstring (* Processor-specific flags *) + ; e_ehsize : elf32_half (* ELF header size *) + ; e_phentsize : elf32_half (* Size of a program header's entry *) + ; e_phnum : elf32_half (* Number of program header entries *) + ; e_shentsize : elf32_half (* Size of a section header's entry *) + ; e_shnum : elf32_half (* Number of section header entries *) + ; e_shstrndx : elf32_half (* Section name string table index *) + } (** ELF section header *) @@ -93,18 +93,18 @@ type sht = | SHT_DYNSYM | SHT_UNKNOWN -type elf32_shdr = { - sh_name: string; - sh_type: sht; - sh_flags: elf32_word; - sh_addr: elf32_addr; - sh_offset: elf32_off; - sh_size: elf32_word; - sh_link: elf32_word; - sh_info: elf32_word; - sh_addralign: elf32_word; - sh_entsize: elf32_word; -} +type elf32_shdr = + { sh_name : string + ; sh_type : sht + ; sh_flags : elf32_word + ; sh_addr : elf32_addr + ; sh_offset : elf32_off + ; sh_size : elf32_word + ; sh_link : elf32_word + ; sh_info : elf32_word + ; sh_addralign : elf32_word + ; sh_entsize : elf32_word + } let shf_WRITE = 0x1l let shf_ALLOC = 0x2l @@ -124,15 +124,15 @@ type elf32_st_type = | STT_FILE | STT_UNKNOWN -type elf32_sym = { - st_name: string; - st_value: elf32_addr; - st_size: elf32_word; - st_bind: elf32_st_bind; - st_type: elf32_st_type; - st_other: byte; - st_shndx: elf32_half; -} +type elf32_sym = + { st_name : string + ; st_value : elf32_addr + ; st_size : elf32_word + ; st_bind : elf32_st_bind + ; st_type : elf32_st_type + ; st_other : byte + ; st_shndx : elf32_half + } (** ELF program header *) @@ -146,24 +146,25 @@ type p_type = | PT_PHDR | PT_UNKNOWN -type elf32_phdr = { - p_type: p_type ; - p_offset: elf32_off ; - p_vaddr: elf32_addr ; - p_paddr: elf32_addr ; - p_filesz: elf32_word ; - p_memsz: elf32_word ; - p_flags: bitstring ; - p_align: elf32_word ; -} +type elf32_phdr = + { p_type : p_type + ; p_offset : elf32_off + ; p_vaddr : elf32_addr + ; p_paddr : elf32_addr + ; p_filesz : elf32_word + ; p_memsz : elf32_word + ; p_flags : bitstring + ; p_align : elf32_word + } (** ELF *) -type elf = { - e_bitstring: bitstring; - e_hdr: elf32_ehdr; - e_shdra: elf32_shdr array; - e_phdra: elf32_phdr array; - e_symtab: elf32_sym array; - e_symtab_sndx: int; (* to avoid having to find it again when needed *) - e_syms_by_name: int list StringMap.t; (* faster lookup *) -} +type elf = + { e_bitstring : bitstring + ; e_hdr : elf32_ehdr + ; e_shdra : elf32_shdr array + ; e_phdra : elf32_phdr array + ; e_symtab : elf32_sym array + ; e_symtab_sndx : int (* section index of the symbol table *) + ; e_sym_phdr : int32 -> int option (* fast sym -> phdr lookup *) + ; e_syms_by_name : int list StringMap.t (* fast name -> sym lookup *) + } diff --git a/checklink/ELF_utils.ml b/checklink/ELF_utils.ml index 4d90160..898c778 100644 --- a/checklink/ELF_utils.ml +++ b/checklink/ELF_utils.ml @@ -18,10 +18,16 @@ let section_bitstring_noelf let section_bitstring (e: elf): int -> bitstring = section_bitstring_noelf e.e_bitstring e.e_shdra -let physical_offset_of_vaddr (e: elf)(sndx: int)(vaddr: int32): int32 = - let shdr = e.e_shdra.(sndx) in - Int32.(add shdr.sh_offset (sub vaddr shdr.sh_addr)) +let physical_offset_of_vaddr (e: elf)(vaddr: int32): int32 option = + begin match e.e_sym_phdr vaddr with + | None -> None + | Some(pndx) -> + let phdr = e.e_phdra.(pndx) in + let vaddr_ofs = Safe32.(vaddr - phdr.p_vaddr) in + Some(Safe32.(phdr.p_offset + vaddr_ofs)) + end +(* TODO: could make this more efficient, but it's not often called *) let section_at_vaddr (e: elf)(vaddr: int32): int option = array_exists (fun shdr -> @@ -30,31 +36,67 @@ let section_at_vaddr (e: elf)(vaddr: int32): int option = e.e_shdra (** - Returns the bitstring of the specified size beginning at the specified - virtual address within the specified section. + Returns the bitstring of the specified byte size beginning at the specified + virtual address, along with its physical byte offset and physical byte size, + that is, the space it occupies in the file. *) -let bitstring_at_vaddr e sndx vaddr size = - let shdr = e.e_shdra.(sndx) in - if vaddr < shdr.sh_addr || Safe32.(shdr.sh_addr + shdr.sh_size) <= vaddr - then None - else - let bs = section_bitstring e sndx in - let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in - Some(Bitstring.subbitstring bs bit_ofs size) +let bitstring_at_vaddr (e: elf)(vaddr: int32)(size:int32): + (bitstring * int32 * int32) option = + match e.e_sym_phdr vaddr with + | None -> None + | Some(pndx) -> + let phdr = e.e_phdra.(pndx) in + let phdr_mem_first = phdr.p_vaddr in + let phdr_mem_last = Safe32.(phdr.p_vaddr + phdr.p_memsz - 1l) in + let vaddr_mem_first = vaddr in + let vaddr_mem_last = Safe32.(vaddr + size - 1l) in + if not (phdr_mem_first <= vaddr_mem_first && vaddr_mem_last <= phdr_mem_last) + then None (* we're overlapping segments *) + else + let vaddr_relative_ofs = Safe32.(vaddr_mem_first - phdr_mem_first) in + let vaddr_file_ofs = Safe32.(phdr.p_offset + vaddr_relative_ofs) in + if phdr.p_filesz = 0l || vaddr_relative_ofs > phdr.p_filesz + then + Some( + Bitstring.create_bitstring Safe32.(to_int (8l * size)), + phdr.p_offset, (* whatever? *) + 0l + ) + else if Safe32.(vaddr_relative_ofs + size) > phdr.p_filesz + then + let bit_start = Safe32.(to_int (8l * vaddr_file_ofs)) in + let vaddr_file_len = Safe32.(phdr.p_filesz - vaddr_relative_ofs) in + let bit_len = Safe32.(to_int (8l * vaddr_file_len)) in + let first = Bitstring.subbitstring e.e_bitstring bit_start bit_len in + let rest = Bitstring.create_bitstring (8 * Safe32.to_int size - bit_len) in + Some( + Bitstring.concat [first; rest], + vaddr_file_ofs, + vaddr_file_len + ) + else + let bit_start = Safe32.(to_int (8l * (phdr.p_offset + vaddr_relative_ofs))) in + let bit_len = Safe.(8 * Safe32.to_int size) in + Some( + Bitstring.subbitstring e.e_bitstring bit_start bit_len, + vaddr_file_ofs, + size + ) (** - Returns the entire bitstring that begins at the specified virtual address - within the specified section and ends at the end of the file. This is useful - when you don't know the sections size yet. + Returns the entire bitstring that begins at the specified virtual address and + ends at the end of the segment. *) -let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring option = - let shdr = e.e_shdra.(sndx) in - if vaddr < shdr.sh_addr || Safe32.(shdr.sh_addr + shdr.sh_size) <= vaddr - then None - else - let bs = section_bitstring e sndx in - let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in - Some(Bitstring.dropbits bit_ofs bs) +let bitstring_at_vaddr_nosize (e: elf)(vaddr: int32): + (bitstring * int32 * int32) option = + match e.e_sym_phdr vaddr with + | None -> None + | Some(pndx) -> + let phdr = e.e_phdra.(pndx) in + let first_byte_vaddr = vaddr in + let last_byte_vaddr = Safe32.(phdr.p_vaddr + phdr.p_memsz - 1l) in + let size = Safe32.(last_byte_vaddr - first_byte_vaddr + 1l) in + bitstring_at_vaddr e vaddr size (** Removes symbol version for GCC's symbols. diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index 4e98735..46778e2 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -136,7 +136,7 @@ let stub_ident_to_vaddr = { let add_range (start: int32) (length: int32) (align: int) (bcd: byte_chunk_desc) (efw: e_framework): e_framework = assert (0l <= start && 0l < length); - let stop = Int32.(sub (add start length) 1l) in + let stop = Safe32.(start + length - 1l) in { efw with chkd_bytes_list = @@ -196,5 +196,3 @@ let string_of_byte_chunk_desc = function | Float_literal(f) -> "Float literal: " ^ string_of_float f | Padding -> "Padding" | Unknown(s) -> " ??? " ^ s - - diff --git a/checklink/Library.ml b/checklink/Library.ml index 0259039..f55d9de 100644 --- a/checklink/Library.ml +++ b/checklink/Library.ml @@ -134,3 +134,17 @@ let string_of_int32i = Int32.to_string let string_of_positive p = string_of_int32i (positive_int32 p) let string_of_z z = string_of_int32 (z_int32 z) + +let sorted_lookup (compare: 'a -> 'b -> int) (arr: 'a array) (v: 'b): 'a option = + let rec sorted_lookup_aux (i_from: int) (i_to: int): 'a option = + if i_from > i_to + then None + else + let i_mid = (i_from + i_to) / 2 in + let comp = compare arr.(i_mid) v in + if comp < 0 (* v_mid < v *) + then sorted_lookup_aux (i_mid + 1) i_to + else if comp > 0 + then sorted_lookup_aux i_from (i_mid - 1) + else Some(arr.(i_mid)) + in sorted_lookup_aux 0 (Array.length arr - 1) diff --git a/checklink/PPC_utils.ml b/checklink/PPC_utils.ml index 338c4c5..44d49d3 100644 --- a/checklink/PPC_utils.ml +++ b/checklink/PPC_utils.ml @@ -4,28 +4,17 @@ open Library open PPC_parsers open PPC_types -let code_at_vaddr (e: elf) (vaddr: int32) (nb_instr: int): ecode option = - begin match section_at_vaddr e vaddr with +let code_at_vaddr (e: elf)(vaddr: int32)(nb_instr: int): ecode option = + begin match bitstring_at_vaddr e vaddr (Safe32.of_int (4 * nb_instr)) with | None -> None - | Some(sndx) -> - begin match bitstring_at_vaddr e sndx vaddr (32 * nb_instr) with - | None -> None - | Some(code_bs) -> Some (parse_code_as_list code_bs) - end + | Some(code_bs, _, _) -> Some (parse_code_as_list code_bs) end let code_of_sym_ndx (e: elf) (ndx: int): ecode option = let sym = e.e_symtab.(ndx) in - begin match sym.st_type with - | STT_FUNC -> - let sym_vaddr = sym.st_value in - let sym_size = Safe.(of_int32 sym.st_size * 8) in - let sym_sndx = sym.st_shndx in - begin match bitstring_at_vaddr e sym_sndx sym_vaddr sym_size with - | None -> None - | Some(code_bs) -> Some (parse_code_as_list code_bs) - end - | _ -> None + begin match bitstring_at_vaddr e sym.st_value sym.st_size with + | None -> None + | Some(bs, _, _) -> Some(parse_code_as_list bs) end let code_of_sym_name (e: elf) (name: string): ecode option = @@ -33,5 +22,3 @@ let code_of_sym_name (e: elf) (name: string): ecode option = | Some ndx -> code_of_sym_ndx e ndx | None -> None end - - diff --git a/checklink/Validator.ml b/checklink/Validator.ml index c413c75..55e4da1 100644 --- a/checklink/Validator.ml +++ b/checklink/Validator.ml @@ -10,9 +10,10 @@ let option_bytefuzz = ref false let option_printelf = ref false let set_elf_file s = - match !elf_file with + begin match !elf_file with | None -> elf_file := Some s | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line") + end let options = [ "-exe <filename>", Arg.String set_elf_file, @@ -33,6 +34,9 @@ let options = [ "Random fuzz testing byte per byte"; "-debugfuzz", Arg.Set Fuzz.fuzz_debug, "Print a detailed trace of ongoing fuzz testing"; + "-relaxed", Arg.Set ELF_parsers.relaxed, + "Allows the following behaviors in the ELF parser: +\t* Use of a fallback heuristic to resolve symbols bootstrapped at load time"; ] let anonymous arg = @@ -49,7 +53,7 @@ Options are:" let _ = Arg.parse options anonymous usage; - match !elf_file with + begin match !elf_file with | None -> Arg.usage options usage; exit 2 @@ -67,3 +71,4 @@ let _ = end else begin check_elf_dump elffilename sdumps end + end |