cchecklink now reads segments instead of sections

cchecklink is now using program header information to figure out the
initial address space of the program, rather than the information in the
parent section of each symbol. This decouples the resolution of symbols
from inaccurate section information, reflecting more the actual program
loading. Additionally, a -relaxed option has been added to deal with
some strange ELFs, for instance when symbols data is dynamically
bootstrapped from another place by boot code different than the program
loader.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1893 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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