summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--checklink/Check.ml267
-rw-r--r--checklink/ELF_parsers.ml107
-rw-r--r--checklink/ELF_types.ml123
-rw-r--r--checklink/ELF_utils.ml90
-rw-r--r--checklink/Frameworks.ml4
-rw-r--r--checklink/Library.ml14
-rw-r--r--checklink/PPC_utils.ml25
-rw-r--r--checklink/Validator.ml9
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