Added small data area support to checklink

Accesses to small data areas are dynamically resolved by constructing a
mapping from registers to virtual addresses they are supposed to point
to. This mapping is reported.

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

3 files changed, 201 insertions, 58 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 20ecb6e..7dcdc83 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -68,8 +68,7 @@ let name_of_section_Linux:
   | Section_const -> ".rodata"
   | Section_small_const -> ".sdata2"
   | Section_string -> ".rodata"
-  | Section_literal -> ".rodata" (* should have been .rodata.cst8, but ld script
-                                    merges it with .rodata *)
+  | Section_literal -> ".rodata.cst8"
   | Section_jumptable -> ".text"
   | Section_user(s, wr, ex) -> s
 
@@ -406,8 +405,7 @@ let match_csts (cc: constant) (ec: int32) (ffw: f_framework): f_framework =
           else ((ff_sf |-- ident_to_sym_ndx) ^%= (PosMap.add ident vaddrs)) ffw
       end
   | Csymbol_sda (ident, i) ->
-      ffw
-      >>> ff_ef ^%= (add_log (ERROR("TODO")))
+      assert false (* sda should be handled separately in places it occurs *)
 
 let match_z_int32 (cz: coq_Z) (ei: int32) =
   check_eq "match_z_int32" (z_int32 cz) ei
@@ -761,6 +759,36 @@ let match_bo_ctr bo ffw =
       | { _ } -> add_log (ERROR("bitmatch"))
   )
 
+let check_sda ident ofs r addr ffw: f_framework or_err =
+  let ofs = z_int32 ofs in
+  let check_sda_aux ndx: f_framework or_err =
+    let elf = ffw.sf.ef.elf in
+    let sym = elf.e_symtab.(ndx) in
+    let sxn = elf.e_shdra.(sym.st_shndx) in
+    try
+      let r_addr = IntMap.find r ffw.sf.ef.sda_map in
+      if r_addr < sxn.sh_offset || r_addr >= Safe32.(sxn.sh_offset + sxn.sh_size)
+      then ERR("SDA register out of the address range of its symbol's section")
+      else if Safe32.(r_addr + ofs) = sym.st_value
+      then OK(ffw)
+      else ERR(
+        Printf.sprintf
+          "SDA register %d is expected to point both at 0x%lx and 0x%lx"
+          r r_addr Safe32.(sym.st_value - ofs)
+      )
+    with Not_found ->
+      OK(
+        ffw >>> (ff_ef |-- sda_map) ^%= IntMap.add r Safe32.(sym.st_value - ofs)
+      )
+  in
+  let sym_list = PosMap.find ident ffw.sf.ident_to_sym_ndx in
+  let res = List.map check_sda_aux sym_list in
+  match filter_ok res with
+  | [] -> ERR("No satisfying SDA mapping, errors were: " ^
+                 string_of_list id ", " (filter_err res))
+  | [ffw] -> OK(ffw)
+  | _ -> assert false (* This should not happen... *)
+
 (** Compares a whole CompCert function code against an ELF code, starting at
     program counter [pc].
 *)
@@ -805,6 +833,15 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
               >>> recur_simpl
           | _ -> error
           end
+      | Paddi(rd, r1, Csymbol_sda(ident, ofs)) ->
+          begin match ecode with
+          | ADDI(rD, rA, simm) :: es ->
+              fw
+              >>> match_iregs rd  rD
+              >>> check_sda ident ofs rA (exts simm)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Paddi(rd, r1, cst) ->
           begin match ecode with
           | ADDI(rD, rA, simm) :: es ->
@@ -1661,6 +1698,15 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
           >>> lblmap_unify lbl pc
           >>? (fun fw -> {fw with label_list = lbl :: fw.label_list})
           >>= compare_code cs ecode pc
+      | Plbz(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | LBZ(rD, rA, d) :: es ->
+              fw
+              >>> match_iregs rd  rD
+              >>> check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Plbz(rd, cst, r1) ->
           begin match ecode with
           | LBZ(rD, rA, d) :: es ->
@@ -1681,29 +1727,18 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
               >>> recur_simpl
           | _ -> error
           end
-      | Plfd(rd, cst, r1) ->
+      | Plfd(rd, Csymbol_sda(ident, ofs), r1) ->
           begin match ecode with
           | LFD(frD, rA, d) :: es ->
               fw
               >>> match_fregs rd  frD
-              >>> match_csts  cst (exts d)
-              >>> match_iregs r1  rA
-              >>> recur_simpl
-          | _ -> error
-          end
-      | Plfdx(rd, r1, r2) ->
-          begin match ecode with
-          | LFDX(frD, rA, rB) :: es ->
-              fw
-              >>> match_fregs rd frD
-              >>> match_iregs r1 rA
-              >>> match_iregs r2 rB
-              >>> recur_simpl
+              >>> check_sda ident ofs rA (exts d)
+              >>= recur_simpl
           | _ -> error
           end
-      | Plfs(rd, cst, r1) ->
+      | Plfd(rd, cst, r1) ->
           begin match ecode with
-          | LFS(frD, rA, d) :: es ->
+          | LFD(frD, rA, d) :: es ->
               fw
               >>> match_fregs rd  frD
               >>> match_csts  cst (exts d)
@@ -1711,9 +1746,9 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
               >>> recur_simpl
           | _ -> error
           end
-      | Plfsx(rd, r1, r2) ->
+      | Plfdx(rd, r1, r2) ->
           begin match ecode with
-          | LFSX(frD, rA, rB) :: es ->
+          | LFDX(frD, rA, rB) :: es ->
               fw
               >>> match_fregs rd frD
               >>> match_iregs r1 rA
@@ -1721,36 +1756,6 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
               >>> recur_simpl
           | _ -> error
           end
-      | Plha(rd, cst, r1) ->
-          begin match ecode with
-          | LHA(rD, rA, d) :: es ->
-              fw
-              >>> match_iregs rd  rD
-              >>> match_csts  cst (exts d)
-              >>> match_iregs r1  rA
-              >>> recur_simpl
-          | _ -> error
-          end
-      | Plhax(rd, r1, r2) ->
-          begin match ecode with
-          | LHAX(rD, rA, rB) :: es ->
-              fw
-              >>> match_iregs rd rD
-              >>> match_iregs r1 rA
-              >>> match_iregs r2 rB
-              >>> recur_simpl
-          | _ -> error
-          end
-      | Plhzx(rd, r1, r2) ->
-          begin match ecode with
-          | LHZX(rD, rA, rB) :: es ->
-              fw
-              >>> match_iregs rd rD
-              >>> match_iregs r1 rA
-              >>> match_iregs r2 rB
-              >>> recur_simpl
-          | _ -> error
-          end
       | Plfi(r1, c) ->
           begin match ecode with
           |   ADDIS(rD0, rA0, simm0) ::
@@ -1801,6 +1806,73 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
                 end
           | _ -> error
           end
+      | Plfs(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | LFS(frD, rA, d) :: es ->
+              fw
+              >>> match_fregs rd  frD
+              >>> check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
+      | Plfs(rd, cst, r1) ->
+          begin match ecode with
+          | LFS(frD, rA, d) :: es ->
+              fw
+              >>> match_fregs rd  frD
+              >>> match_csts  cst (exts d)
+              >>> match_iregs r1  rA
+              >>> recur_simpl
+          | _ -> error
+          end
+      | Plfsx(rd, r1, r2) ->
+          begin match ecode with
+          | LFSX(frD, rA, rB) :: es ->
+              fw
+              >>> match_fregs rd frD
+              >>> match_iregs r1 rA
+              >>> match_iregs r2 rB
+              >>> recur_simpl
+          | _ -> error
+          end
+      | Plha(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | LHA(rD, rA, d) :: es ->
+              fw
+              >>> match_iregs rd  rD
+              >>> check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
+      | Plha(rd, cst, r1) ->
+          begin match ecode with
+          | LHA(rD, rA, d) :: es ->
+              fw
+              >>> match_iregs rd  rD
+              >>> match_csts  cst (exts d)
+              >>> match_iregs r1  rA
+              >>> recur_simpl
+          | _ -> error
+          end
+      | Plhax(rd, r1, r2) ->
+          begin match ecode with
+          | LHAX(rD, rA, rB) :: es ->
+              fw
+              >>> match_iregs rd rD
+              >>> match_iregs r1 rA
+              >>> match_iregs r2 rB
+              >>> recur_simpl
+          | _ -> error
+          end
+      | Plhz(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | LHZ(rD, rA, d) :: es ->
+              fw
+              >>> match_iregs rd  rD
+              >>> check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Plhz(rd, cst, r1) ->
           begin match ecode with
           | LHZ(rD, rA, d) :: es ->
@@ -1811,6 +1883,25 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
               >>> recur_simpl
           | _ -> error
           end
+      | Plhzx(rd, r1, r2) ->
+          begin match ecode with
+          | LHZX(rD, rA, rB) :: es ->
+              fw
+              >>> match_iregs rd rD
+              >>> match_iregs r1 rA
+              >>> match_iregs r2 rB
+              >>> recur_simpl
+          | _ -> error
+          end
+      | Plwz(rd, Csymbol_sda(ident, ofs), r1) ->
+          begin match ecode with
+          | LWZ(rD, rA, d) :: es ->
+              fw
+              >>> match_iregs rd  rD
+              >>> check_sda ident ofs rA (exts d)
+              >>= recur_simpl
+          | _ -> error
+          end
       | Plwz(rd, cst, r1) ->
           begin match ecode with
           | LWZ(rD, rA, d) :: es ->
@@ -2479,7 +2570,7 @@ let compare_data (l: init_data list) (maybebs: maybe_bitstring) (sfw: s_framewor
         let sfw =
           if !debug
           then (
-            (sf_ef ^%= add_log (DEBUG(string_of_init_data d))) sfw
+            (sf_ef ^%= add_log (DEBUG("  " ^ string_of_init_data d))) sfw
           )
           else sfw
         in
@@ -3068,6 +3159,9 @@ let check_sym_tab_zero efw =
   )
   >>> add_range elf.e_shdra.(elf.e_symtab_sndx).sh_offset 16l 4 Zero_symbol
 
+(** If CompCert sections have been mapped to an ELF section whose name is
+    not the same, we warn the user.
+*)
 let warn_sections_remapping efw =
   StringMap.fold
     (fun c_name e_name efw ->
@@ -3084,6 +3178,22 @@ let warn_sections_remapping efw =
     efw.section_map
     efw
 
+let warn_sda_mapping efw =
+  if IntMap.is_empty efw.sda_map
+  then efw
+  else (
+    IntMap.fold
+      (fun r vaddr efw ->
+        efw >>> add_log (WARNING(
+          Printf.sprintf
+            "SDA register %d has been mapped to virtual address 0x%lx by your linker script"
+            r vaddr
+        ))
+      )
+      efw.sda_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. *)
@@ -3101,6 +3211,7 @@ let check_elf_nodump elf sdumps =
       chkd_fun_syms = Array.make nb_syms false;
       chkd_data_syms = Array.make nb_syms false;
       section_map = StringMap.empty;
+      sda_map = IntMap.empty;
     }
     >>> check_elf_header
     >>> add_range
@@ -3132,6 +3243,7 @@ let check_elf_nodump elf sdumps =
   >>> check_padding
   (* warn if some CompCert sections have been remapped by the linker script *)
   >>> warn_sections_remapping
+  >>> warn_sda_mapping
 
 (** Checks a whole ELF file according to .sdump files.
     If requested, dump the calculated bytes mapping, so that it can be
@@ -3182,7 +3294,8 @@ let check_elf_dump elffilename sdumps =
           "\nWARNING: the following function symbols do not appear in .sdump files.";
         print_endline (
           string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_fun
-        )
+        );
+        print_newline ()
     end
   ;
   (* indicate data symbols that have not been checked *)
@@ -3207,15 +3320,20 @@ let check_elf_dump elffilename sdumps =
     | [] -> ()
     | _  ->
         print_endline
-          "\nWARNING: the following data symbols do not appear in .sdump files.";
+          "WARNING: the following data symbols do not appear in .sdump files.";
         print_endline (
           string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_data
-        )
+        );
+        print_newline ()
     end
   ;
   (* print diagnosis *)
   let worrysome = List.filter
-    (function ERROR(_) -> true | WARNING(_) -> true | DEBUG(_) -> false)
+    (function
+    | ERROR(_) -> true
+    | WARNING(_) -> true
+    | DEBUG(_) -> false
+    )
     efw.log
   in
   let exists_unknown_chunk =
@@ -3236,6 +3354,10 @@ let check_elf_dump elffilename sdumps =
         )
       end
   | _ ->
+      if !debug
+      then print_endline (
+        "DEBUG MODE: The following messages are actual problems."
+      );
       List.(iter
               (fun e ->
                 match string_of_log_entry false e with
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 4054b68..4e98735 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -38,7 +38,13 @@ type e_framework = {
   chkd_bytes_list: (int32 * int32 * int * byte_chunk_desc) list;
   chkd_fun_syms: bool array;
   chkd_data_syms: bool array;
+  (** The mapping from CompCert sections to ELF sections will be inferred along
+      the way. This way, we can check things without prior knowledge of the
+      linker script. *)
   section_map: string StringMap.t;
+  (** We will assign a virtual address to each register that can act as an SDA
+      base register. *)
+  sda_map: int32 IntMap.t;
 }
 
 module PosOT = struct
@@ -110,6 +116,11 @@ let section_map = {
   set = (fun m ef -> { ef with section_map = m });
 }
 
+let sda_map = {
+  get = (fun ef -> ef.sda_map);
+  set = (fun m ef -> { ef with sda_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/Library.ml b/checklink/Library.ml
index bb0d217..0259039 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -3,6 +3,7 @@ open BinPos
 
 type bitstring = Bitstring.bitstring
 
+module IntMap = Map.Make(struct type t = int let compare = compare end)
 module StringMap = Map.Make (String)
 
 let is_some: 'a option -> bool = function
@@ -24,13 +25,22 @@ let is_ok: 'a or_err -> bool = function
 | OK(_) -> true
 | ERR(_) -> false
 
+let is_err x = not (is_ok x)
+
 let from_ok: 'a or_err -> 'a = function
 | OK(x) -> x
-| ERR(_) -> raise Not_found
+| ERR(_) -> assert false
+
+let from_err: 'a or_err -> string = function
+| OK(_) -> assert false
+| ERR(s) -> s
 
 let filter_ok (l: 'a or_err list): 'a list =
   List.(map from_ok (filter is_ok l))
 
+let filter_err (l: 'a or_err list): string list =
+  List.(map from_err (filter is_err l))
+
 external id : 'a -> 'a = "%identity"
 
 (** Checks for existence of an array element satisfying a condition, and returns