New section mapping checks and symbol data lookup

Section mapping is now discovered on-the-fly, and linker script remappings
are reported as warnings at the end. Symbol data lookup is now able to
gracefully fail if the symbol's virtual address is not within the range of
its parent section's virtual address space.

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

4 files changed, 118 insertions, 57 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index c2bade7..20ecb6e 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -104,17 +104,22 @@ let match_sections_name
     s_framework
     =
   let c_name = name_of_section c_section in
-  if e_name = c_name ||
-    (c_name = ".bss" && e_name = ".sbss") (* this is complicated! *)
-  then sfw
-  else (
+  try
+    let expected = StringMap.find c_name sfw.ef.section_map in
+    if e_name = expected
+    then sfw
+    else (
+      sfw
+      >>> sf_ef ^%=
+        add_log (ERROR(
+          Printf.sprintf
+            "CompCert section %s was mapped to both %s and %s"
+            c_name expected e_name
+        ))
+    )
+  with Not_found -> (
     sfw
-    >>> sf_ef ^%=
-      (add_log
-         (ERROR
-            ("Section should be " ^ c_name ^ " instead of " ^ e_name)
-         )
-      )
+    >>> (sf_ef |-- section_map) ^%= StringMap.add c_name e_name
   )
 
 (** Checks the symbol table entry of the function symbol number [sym_ndx],
@@ -533,18 +538,22 @@ 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
-  let bs = bitstring_at_vaddr elf cur_sym_ndx vaddr size in
-  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
-      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)
+  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
+          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)
+      end
+  end
 
 (** Matches [ecode] agains the expected code for a small memory copy
     pseudo-instruction. Returns a triple containing the updated framework,
@@ -722,19 +731,19 @@ let match_memcpy_big ecode pc sz al src dst fw
 
 let match_bo_bt_bool bo =
   bitmatch bo with
-    | { false:1; true:1; true:1; false:1; false:1 } -> true
-    | { _ } -> false
+  | { false:1; true:1; true:1; false:1; false:1 } -> true
+  | { _ } -> false
 
 let match_bo_bf_bool bo =
   bitmatch bo with
-    | { false:1; false:1; true:1; false:1; false:1 } -> true
-    | { _ } -> false
+  | { false:1; false:1; true:1; false:1; false:1 } -> true
+  | { _ } -> false
 
 let match_bo_bt bo ffw =
   ffw >>> (ff_ef ^%=
       bitmatch bo with
-        | { false:1; true:1; true:1; false:1; false:1 } -> id
-        | { _ } -> add_log (ERROR("match_bo_bt"))
+      | { false:1; true:1; true:1; false:1; false:1 } -> id
+      | { _ } -> add_log (ERROR("match_bo_bt"))
   )
 
 let match_bo_bf bo ffw =
@@ -748,8 +757,8 @@ let match_bo_ctr bo ffw =
   ffw
   >>> (ff_ef ^%=
       bitmatch bo with
-        | { true:1; false:1; true:1; false:1; false:1 } -> id
-        | { _ } -> add_log (ERROR("bitmatch"))
+      | { true:1; false:1; true:1; false:1; false:1 } -> id
+      | { _ } -> add_log (ERROR("bitmatch"))
   )
 
 (** Compares a whole CompCert function code against an ELF code, starting at
@@ -1766,7 +1775,13 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
                 | Some(sndx) ->
                     let section_bitstring = bitstring_at_vaddr elf sndx in
                     let f = (
-                      bitmatch (section_bitstring vaddr 64) with
+                      let bs =
+                        begin match section_bitstring vaddr 64 with
+                        | None -> assert false
+                        | Some(bs) -> bs
+                        end
+                      in
+                      bitmatch bs with
                       | { f : 64 : int } -> Int64.float_of_bits f
                     ) in
                     let ofs = physical_offset_of_vaddr elf sndx vaddr in
@@ -2381,11 +2396,11 @@ let rec worklist_process (wl: worklist) sfw: s_framework =
         let elf = (sfw |. sf_ef).elf in
         let pc = elf.e_symtab.(ndx).st_value in
         match code_of_sym_ndx elf ndx with
-        | None -> assert false
+        | None -> ERR("Could not find symbol data for function symbol " ^ name)
         | Some ecode ->
             sfw
             >>> sf_ef ^%=
-            add_log (DEBUG("  Processing function: " ^ name))
+            add_log (DEBUG("Processing function: " ^ name))
             >>> (fun sfw ->
               {
                 sf = sfw;
@@ -2606,18 +2621,27 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
     let sym_vaddr = sym.st_value in
     let sym_size = sym.st_size in
     let sym_sndx = sym.st_shndx in
-    let sym_bs =
-      match elf.e_shdra.(sym_sndx).sh_type with
+    let sym_bs_opt =
+      begin match elf.e_shdra.(sym_sndx).sh_type with
       | SHT_NOBITS ->
-          Empty(Safe.(of_int32 sym.st_size * 8))
+          Some(Empty(Safe.(of_int32 sym.st_size * 8)))
       | SHT_PROGBITS ->
-          NonEmpty(bitstring_at_vaddr_nosize elf sym_sndx sym_vaddr)
+          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 =
-      sfw
-      >>> (sf_ef ^%= add_log (DEBUG("  Processing data: " ^ sym.st_name)))
-      >>> compare_data ldata sym_bs in
+      begin match sym_bs_opt with
+      | None -> ERR("Could not find symbol data for data symbol " ^ sym.st_name)
+      | Some(sym_bs) ->
+          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) ->
@@ -2680,6 +2704,7 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
             (function OK(_) -> "" | ERR(s) -> s)
             ", "
             (List.filter (function ERR(_) -> true | _ -> false) results)
+                        ^ "]"
         ))
     | [sfw] -> sfw
     | fws ->
@@ -3043,6 +3068,22 @@ let check_sym_tab_zero efw =
   )
   >>> add_range elf.e_shdra.(elf.e_symtab_sndx).sh_offset 16l 4 Zero_symbol
 
+let warn_sections_remapping efw =
+  StringMap.fold
+    (fun c_name e_name efw ->
+      if c_name = e_name
+      then efw
+      else (
+        efw >>> add_log (WARNING(
+          Printf.sprintf
+            "Section %s has been re-mapped to %s by your linker script"
+            c_name e_name
+        ))
+      )
+    )
+    efw.section_map
+    efw
+
 (** Checks a whole ELF file according to a list of .sdump files. This never
     dumps anything, so it can be safely used when fuzz-testing even if the
     user accidentally enabled dumping options. *)
@@ -3059,6 +3100,7 @@ let check_elf_nodump elf sdumps =
       chkd_bytes_list = [];
       chkd_fun_syms = Array.make nb_syms false;
       chkd_data_syms = Array.make nb_syms false;
+      section_map = StringMap.empty;
     }
     >>> check_elf_header
     >>> add_range
@@ -3086,8 +3128,10 @@ let check_elf_nodump elf sdumps =
   if !debug then print_endline "Done checking header, beginning processing of .sdumps";
   (* Thread the framework through the processing of all .sdump files *)
   List.fold_left process_sdump efw sdumps
-  (* then finally, check the padding in between identified byte chunks *)
+  (* check the padding in between identified byte chunks *)
   >>> check_padding
+  (* warn if some CompCert sections have been remapped by the linker script *)
+  >>> warn_sections_remapping
 
 (** Checks a whole ELF file according to .sdump files.
     If requested, dump the calculated bytes mapping, so that it can be
diff --git a/checklink/ELF_utils.ml b/checklink/ELF_utils.ml
index 5244dc8..4d90160 100644
--- a/checklink/ELF_utils.ml
+++ b/checklink/ELF_utils.ml
@@ -35,20 +35,26 @@ let section_at_vaddr (e: elf)(vaddr: int32): int option =
 *)
 let bitstring_at_vaddr e sndx vaddr size =
   let shdr = e.e_shdra.(sndx) in
-  let bs = section_bitstring e sndx in
-  let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in
-  Bitstring.subbitstring bs bit_ofs size
+  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)
 
 (**
    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.
 *)
-let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring =
+let bitstring_at_vaddr_nosize (e: elf)(sndx: int)(vaddr: int32): bitstring option =
   let shdr = e.e_shdra.(sndx) in
-  let bs = section_bitstring e sndx in
-  let bit_ofs = Safe.(8 * Safe32.(to_int (vaddr - shdr.sh_addr))) in
-  Bitstring.dropbits bit_ofs bs
+  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)
 
 (**
    Removes symbol version for GCC's symbols.
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index f35672d..4054b68 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -38,6 +38,7 @@ type e_framework = {
   chkd_bytes_list: (int32 * int32 * int * byte_chunk_desc) list;
   chkd_fun_syms: bool array;
   chkd_data_syms: bool array;
+  section_map: string StringMap.t;
 }
 
 module PosOT = struct
@@ -104,6 +105,11 @@ let log = {
   set = (fun l ef -> { ef with log = l });
 }
 
+let section_map = {
+  get = (fun ef -> ef.section_map);
+  set = (fun m ef -> { ef with section_map = m });
+}
+
 let ident_to_sym_ndx = {
   get = (fun sf -> sf.ident_to_sym_ndx);
   set = (fun i sf -> { sf with ident_to_sym_ndx = i });
diff --git a/checklink/PPC_utils.ml b/checklink/PPC_utils.ml
index d027649..338c4c5 100644
--- a/checklink/PPC_utils.ml
+++ b/checklink/PPC_utils.ml
@@ -5,28 +5,33 @@ open PPC_parsers
 open PPC_types
 
 let code_at_vaddr (e: elf) (vaddr: int32) (nb_instr: int): ecode option =
-  match section_at_vaddr e vaddr with
+  begin match section_at_vaddr e vaddr with
   | None -> None
   | Some(sndx) ->
-      let code_bs =
-        bitstring_at_vaddr e sndx vaddr (32 * nb_instr) in
-      Some (parse_code_as_list code_bs)
+      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
+  end
 
 let code_of_sym_ndx (e: elf) (ndx: int): ecode option =
   let sym = e.e_symtab.(ndx) in
-  match sym.st_type with
+  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
-      let code_bs =
-        bitstring_at_vaddr e sym_sndx sym_vaddr sym_size in
-      Some (parse_code_as_list code_bs)
+      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
+  end
 
 let code_of_sym_name (e: elf) (name: string): ecode option =
-  match ndx_of_sym_name e name with
+  begin match ndx_of_sym_name e name with
   | Some ndx -> code_of_sym_ndx e ndx
   | None     -> None
+  end