Adjustments to cchecklink's options and verbosity

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

5 files changed, 217 insertions, 108 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 7adfc50..34e6efd 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -19,19 +19,26 @@ open PPC_utils
 open Sections
 
 (** Enables immediate printing of log information to stdout.
-    Warning: will print out everything before backtracking.
+    Warning: will print out everything even when backtracking.
 *)
 let debug = ref false
 
+(** Whether to print the ELF map *)
+let print_elfmap = ref false
+
 (** Whether to dump the ELF map *)
 let dump_elfmap = ref false
 
+(** Whether to check that all ELF function/data symbols have been matched
+    against CompCert idents *)
+let exhaustivity = ref true
+
 (** CompCert Asm *)
 type ccode = Asm.instruction list
 
 (** Adds a log entry into the framework. *)
 let add_log (entry: log_entry) (efw: e_framework): e_framework =
-  if !debug then print_endline (string_of_log_entry entry);
+  if !debug then print_endline (string_of_log_entry true entry);
   {efw with log = entry :: efw.log}
 
 (** [flag] should have only one bit set. *)
@@ -102,10 +109,12 @@ let match_sections_name
   then sfw
   else (
     sfw
-    >>> (sf_ef ^%=
-        (add_log (ERROR(
-          "Section should be " ^ c_name ^ " instead of " ^ e_name)))
-    )
+    >>> sf_ef ^%=
+      (add_log
+         (ERROR
+            ("Section should be " ^ c_name ^ " instead of " ^ e_name)
+         )
+      )
   )
 
 (** Checks the symbol table entry of the function symbol number [sym_ndx],
@@ -145,9 +154,8 @@ let check_fun_symtab
     )
   )
   >>> match_sections_name section elf.e_shdra.(sym.st_shndx).sh_name
-  >>> (sf_ef ^%=
+  >>> sf_ef ^%=
       add_range symtab_ent_start 16l 4 (Symtab_function(sym))
-  )
 
 (** Checks that the offset [ofs] is well aligned with regards to [al], expressed
     in bytes. *)
@@ -171,10 +179,10 @@ let mark_covered_fun_sym_ndx (ndx: int) ffw: f_framework =
     | Some(a) -> a
     | None -> 0
   in
+  ffw.sf.ef.chkd_fun_syms.(ndx) <- true;
   ffw
-  >>> (ff_ef ^%=
-      (add_range sym_begin sym_size align (Function_symbol(sym)))
-  )
+  >>> ff_ef ^%=
+      add_range sym_begin sym_size align (Function_symbol(sym))
   >>> (ff_sf ^%=
       if not (is_well_aligned sym_ofs_local align)
       then (
@@ -463,7 +471,7 @@ let rec bitmask mb me =
     0 0 0 0 1 1 1 0 0 0 0    bitmask (me + 1) (mb - 1)
   *)
   else if mb = me + 1
-  then (-1l)
+  then (-1l) (* this needs special handling *)
   else Int32.(sub (-1l) (bitmask (me + 1) (mb - 1)))
 
 (** Checks that a label did not occur twice in the same function. *)
@@ -725,9 +733,15 @@ let rec compare_code ccode ecode pc fw: f_framework on_success =
   | [], _ | _, [] -> ERR("Codes have different lengths")
   | c::cs, e::es  ->
       let recur_simpl = compare_code cs es (Int32.add 4l pc) in
-      (*let curr_instr = "  [" ^ string_of_int32 pc ^ "] " ^
-        string_of_instruction c ^ " - " ^ string_of_instr e in
-        let fw = (ff_ef ^%= add_log (LOG(curr_instr))) fw in*)
+      let fw =
+        if !debug
+        then (
+          let curr_instr = "  [" ^ string_of_int32 pc ^ "] " ^
+            string_of_instruction c ^ " - " ^ string_of_instr e in
+          (ff_ef ^%= add_log (DEBUG(curr_instr))) fw
+        )
+        else fw
+      in
       match c with
       | Padd(rd, r1, r2) ->
           begin match ecode with
@@ -2326,7 +2340,7 @@ let rec worklist_process (wl: worklist) sfw: s_framework =
         | Some ecode ->
             sfw
             >>> sf_ef ^%=
-            add_log (LOG("  Processing function: " ^ name))
+            add_log (DEBUG("  Processing function: " ^ name))
             >>> (fun sfw ->
               {
                 sf = sfw;
@@ -2342,8 +2356,9 @@ let rec worklist_process (wl: worklist) sfw: s_framework =
       begin match candidates with
       | []    ->
           sfw
-          >>> sf_ef ^%= add_log (ERROR("Skipping missing symbol " ^ name))
-                        >>> worklist_process wl
+          >>> sf_ef ^%=
+          add_log (ERROR("Skipping missing symbol " ^ name))
+          >>> worklist_process wl
       | [ndx] ->
           begin match process_ndx ndx with
           | OK(ffw) ->
@@ -2511,7 +2526,7 @@ let check_data_symtab ident sym_ndx size sfw =
     match sym.st_type with
     | STT_OBJECT -> id
     | STT_NOTYPE -> (sf_ef ^%=
-        add_log (WARNING("Missing type for symbol"))
+        add_log (WARNING("Missing type for symbol " ^ sym.st_name))
     )
     | _ -> (sf_ef ^%=
         add_log (ERROR("Symbol should have type STT_OBJECT"))
@@ -2549,7 +2564,7 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
     in
     let res =
       sfw
-      >>> (sf_ef ^%= add_log (LOG("  Processing data: " ^ sym.st_name)))
+      >>> (sf_ef ^%= add_log (DEBUG("  Processing data: " ^ sym.st_name)))
       >>> compare_data ldata sym_bs in
     match res with
     | ERR(s) -> ERR(s)
@@ -2564,11 +2579,12 @@ let check_data (pv: (ident * unit globvar) list) (sfw: s_framework)
           | Some(a) -> a
           end
         in
+        sfw.ef.chkd_data_syms.(ndx) <- true;
         sfw
         >>> (
           begin match sym_shdr.sh_type with
           | SHT_NOBITS ->
-              id
+              id (* These occupy no space, for now we just forget them *)
           | _ ->
               sf_ef ^%=
               add_range sym_begin sym_size align (Data_symbol(sym))
@@ -2813,46 +2829,45 @@ let is_padding bs start stop =
     Returns a framework where [chkd_bytes_list] is sorted and full.
 *)
 let check_padding efw =
-  (*let elf = efw.elf in
-    let sndxes = list_n elf.e_hdr.e_shnum in
-    let matching_sections x y =
+  let elf = efw.elf in
+  let sndxes = list_n elf.e_hdr.e_shnum in
+  let matching_sections x y =
     string_of_list
-    id
-    ", "
-    List.(map
-    (fun ndx -> elf.e_shdra.(ndx).sh_name)
-    (List.filter
-    (fun ndx ->
-    let shdr = elf.e_shdra.(ndx) in
-    intersect (x, y) shdr.sh_offset shdr.sh_size
-    )
-    sndxes
-    )
-    )
-    in*)
-  (*let matching_symbols x y =
+      id
+      ", "
+      (List.map
+         (fun ndx -> elf.e_shdra.(ndx).sh_name)
+         (List.filter
+            (fun ndx ->
+              let shdr = elf.e_shdra.(ndx) in
+              intersect (x, y) shdr.sh_offset shdr.sh_size
+            )
+            sndxes
+         )
+      )
+  in
+  let matching_symbols x y =
     string_of_list
-    id
-    ", "
-    List.(map
-    (fun sym -> sym.st_name)
-    (List.filter
-    (fun sym ->
-    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
-    )
-    (Array.to_list elf.e_symtab)
-    )
-    )
-    in*)
-  let unknown x y = Unknown(""
-  (*^ "Sections: " ^ matching_sections x y*)
-  (*^ "\nSymbols: " ^ matching_symbols x y*)
+      id
+      ", "
+      (List.map
+         (fun sym -> sym.st_name)
+         (List.filter
+            (fun sym ->
+              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
+            )
+            (Array.to_list elf.e_symtab)
+         )
+      )
+  in
+  let unknown x y = Unknown(
+    "\nSections: " ^ matching_sections x y ^ "\nSymbols: " ^ matching_symbols x y
   )
   in
   (* check_padding_aux assumes a sorted list *)
@@ -2967,9 +2982,12 @@ let check_sym_tab_zero efw =
   )
   >>> add_range elf.e_shdra.(elf.e_symtab_sndx).sh_offset 16l 4 Zero_symbol
 
-(** Checks a whole ELF file according to a list of .sdump files. *)
-let check_elf elf sdumps =
+(** 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. *)
+let check_elf_nodump elf sdumps =
   let eh = elf.e_hdr in
+  let nb_syms = Array.length elf.e_symtab in
   let section_strtab = elf.e_shdra.(eh.e_shstrndx) in
   let symtab_shdr = elf.e_shdra.(elf.e_symtab_sndx) in
   let symbol_strtab = elf.e_shdra.(int32_int symtab_shdr.sh_link) in
@@ -2978,6 +2996,8 @@ let check_elf elf sdumps =
       elf = elf;
       log = [];
       chkd_bytes_list = [];
+      chkd_fun_syms = Array.make nb_syms false;
+      chkd_data_syms = Array.make nb_syms false;
     }
     >>> check_elf_header
     >>> add_range
@@ -3002,43 +3022,118 @@ let check_elf elf sdumps =
       ELF_symbol_strtab
     >>> check_sym_tab_zero
   in
+  (* 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_padding
-  >>> add_log (LOG("ELF map:"))
-  >>> (fun efw ->
-    efw
-    >>> add_log (LOG(
-      string_of_list
-        (fun (a, b, align, r) -> string_of_range a b ^ " (" ^
-          string_of_int align ^ ") " ^ string_of_byte_chunk_desc r)
-        "\n"
-        efw.chkd_bytes_list
-    ))
-  )
 
 (** Checks a whole ELF file according to .sdump files.
     If requested, dump the calculated bytes mapping, so that it can be
     reused by the fuzzer. *)
-let check_and_dump elffilename sdumps =
+let check_elf_dump elffilename sdumps =
   let elf = read_elf elffilename in
-  check_elf elf sdumps
-  >>> (fun efw ->
-    if !dump_elfmap then begin
-      (* dump the elf map for fuzz-testing *)
-      let oc = open_out (elffilename ^ ".elfmap") in
-      output_value oc efw.chkd_bytes_list;
-      close_out oc
-    end;
-    efw
-  )
-  >>> (fun efw ->
-    if not !debug
-    then List.(
-      iter
-        (fun e ->
-          print_endline (string_of_log_entry e)
-        )
-        (rev efw.log)
+  let efw = check_elf_nodump elf sdumps in
+  (* print the elfmap if requested *)
+  if !print_elfmap then begin
+    print_endline (
+      string_of_list
+        (fun (a, b, align, r) -> string_of_range a b ^ " (" ^
+          string_of_int align ^ ") " ^ string_of_byte_chunk_desc r)
+        "\n"
+        efw.chkd_bytes_list
     )
-  )
-
+  end;
+  (* dump the elfmap if requested *)
+  if !dump_elfmap then begin
+    let oc = open_out (elffilename ^ ".elfmap") in
+    output_value oc efw.chkd_bytes_list;
+    close_out oc
+  end;
+  (* indicate function symbols that have not been checked *)
+  let miss_fun =
+    List.filter
+      (fun ndx ->
+        let symtype = efw.elf.e_symtab.(ndx).st_type in
+        symtype = STT_FUNC || symtype = STT_NOTYPE
+      )
+      (filter_some
+         (Array.to_list
+            (Array.mapi
+               (fun ndx b -> if b then None else Some(ndx))
+               efw.chkd_fun_syms
+            )
+         )
+      )
+  in
+  if !exhaustivity
+  then
+    begin match miss_fun with
+    | [] -> ()
+    | _  ->
+        print_endline
+          "\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
+        )
+    end
+  ;
+  (* indicate data symbols that have not been checked *)
+  let miss_data =
+    List.filter
+      (fun ndx ->
+        let symtype = efw.elf.e_symtab.(ndx).st_type in
+        symtype = STT_OBJECT || symtype = STT_NOTYPE
+      )
+      (filter_some
+         (Array.to_list
+            (Array.mapi
+               (fun ndx b -> if b then None else Some(ndx))
+               efw.chkd_data_syms
+            )
+         )
+      )
+  in
+  if !exhaustivity
+  then
+    begin match miss_data with
+    | [] -> ()
+    | _  ->
+        print_endline
+          "\nWARNING: 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
+        )
+    end
+  ;
+  (* print diagnosis *)
+  let worrysome = List.filter
+    (function ERROR(_) -> true | WARNING(_) -> true | DEBUG(_) -> false)
+    efw.log
+  in
+  let exists_unknown_chunk =
+    List.exists
+      (function (_, _, _, Unknown(_)) -> true | _ -> false)
+      efw.chkd_bytes_list
+  in
+  begin match worrysome with
+  | [] ->
+      print_endline "\nEverything seems fine with this ELF.";
+      if exists_unknown_chunk
+      then begin
+        print_endline (
+          "However, some parts of the ELF could not be identified." ^
+            if !print_elfmap
+            then ""
+            else " Use -printelfmap to see what was covered."
+        )
+      end
+  | _ ->
+      List.(iter
+              (fun e ->
+                match string_of_log_entry false e with
+                | "" -> ()
+                | s -> print_endline s
+              )
+              (rev efw.log)
+      )
+  end;
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index e8f75ba..f63eb9a 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -6,10 +6,9 @@ open Lens
 open Library
 
 type log_entry =
-  | LOG of string
+  | DEBUG of string
   | ERROR of string
   | WARNING of string
-  | DEBUG of string
 
 type byte_chunk_desc =
   | ELF_header
@@ -37,6 +36,8 @@ type e_framework = {
       The first two fields are the start and stop offsets, the third is an
       alignment constraint, the last is a description. *)
   chkd_bytes_list: (int32 * int32 * int * byte_chunk_desc) list;
+  chkd_fun_syms: bool array;
+  chkd_data_syms: bool array;
 }
 
 module PosOT = struct
@@ -164,11 +165,10 @@ let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b on_success)
 (** Finally, some printers.
 *)
 
-let string_of_log_entry = function
-| LOG(s)     -> s
+let string_of_log_entry show_debug = function
+| DEBUG(s)   -> if show_debug then s else ""
 | ERROR(s)   -> "ERROR: " ^ s
 | WARNING(s) -> "WARNING: " ^ s
-| DEBUG(s)   -> "DEBUG: " ^ s
 
 let string_of_byte_chunk_desc = function
 | ELF_header -> "ELF header"
diff --git a/checklink/Fuzz.ml b/checklink/Fuzz.ml
index 538c2d8..56b665a 100644
--- a/checklink/Fuzz.ml
+++ b/checklink/Fuzz.ml
@@ -14,6 +14,9 @@ let range_of_byte elfmap byte =
   let (_, _, _, r) = full_range_of_byte elfmap byte in
   r
 
+(** [fuzz_check] will print what happened on stderr, and report errors (that is,
+    when the check went fine) to stdout.
+*)
 let fuzz_check elfmap bs byte old sdumps =
   try
     (* The point here is to go all the way through the checks, and see whether
@@ -21,7 +24,7 @@ let fuzz_check elfmap bs byte old sdumps =
        might be missing a bug!
     *)
     let elf = read_elf_bs bs in
-    let efw = check_elf elf sdumps in
+    let efw = check_elf_nodump elf sdumps in
     if List.exists (function ERROR(s) -> true | _ -> false) efw.log
     then () (* finding an ERROR is expected *)
     else (* not finding an ERROR is bad! This is reported. *)
diff --git a/checklink/Library.ml b/checklink/Library.ml
index dbe7b46..0014025 100644
--- a/checklink/Library.ml
+++ b/checklink/Library.ml
@@ -3,10 +3,16 @@ open BinPos
 
 type bitstring = Bitstring.bitstring
 
+let is_some = function
+| Some(_) -> true
+| None    -> false
+
 let from_some = function
 | Some(x) -> x
 | None    -> raise Not_found
 
+let filter_some l = List.(map from_some (filter is_some l))
+
 type 'a on_success =
   | OK of 'a
   | ERR of string
diff --git a/checklink/Validator.ml b/checklink/Validator.ml
index b27bc4c..f91a131 100644
--- a/checklink/Validator.ml
+++ b/checklink/Validator.ml
@@ -6,7 +6,7 @@ open Fuzz
 let elf_file = ref (None: string option)
 let sdump_files = ref ([] : string list)
 let option_fuzz = ref false
-let option_dumpelf = ref false
+let option_printelf = ref false
 
 let set_elf_file s =
   match !elf_file with
@@ -14,16 +14,20 @@ let set_elf_file s =
   | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line")
 
 let options = [
-  "-dumpelf", Arg.Set option_dumpelf,
-    "Print the contents of the ELF executable";
+  "-printelf", Arg.Set option_printelf,
+    "Print the contents of the unanalyzed ELF executable";
+  "-printelfmap", Arg.Set Check.print_elfmap,
+    "Print a map of the analyzed ELF executable";
   "-debug", Arg.Set Check.debug,
     "Print a detailed trace of verification";
-  "-elfmap", Arg.Set Check.dump_elfmap,
-    "Dump an ELF map to <exename>.elfmap>, for use with random fuzzing";
+  "-dumpelfmap", Arg.Set Check.dump_elfmap,
+    "Dump an ELF map to <exename>.elfmap, for use with random fuzzing";
   "-exe <filename>", Arg.String set_elf_file,
     "Specify the ELF executable file to analyze";
   "-fuzz", Arg.Set option_fuzz,
-    "Random fuzzing test"
+    "Random fuzzing test";
+  "-noexhaust", Arg.Clear Check.exhaustivity,
+    "Disable the exhaustivity check of ELF function and data symbols"
 ]
 
 let anonymous arg =
@@ -34,7 +38,8 @@ let anonymous arg =
 
 let usage =
 "The CompCert C post-linking validator, version " ^ Configuration.version ^ "
-Usage: valink [options] <.sdump files> <ELF executable>
+Usage: cchecklink [options] <.sdump files> <ELF executable>
+In the absence of options, checks are performed and a short result is displayed.
 Options are:"
 
 let _ =
@@ -48,9 +53,9 @@ let _ =
       if !option_fuzz then begin
         Random.self_init();
         fuzz_loop elffilename sdumps
-      end else if !option_dumpelf then begin
+      end else if !option_printelf then begin
         let elf = read_elf elffilename in
         print_endline (string_of_elf elf)
       end else begin
-        check_and_dump elffilename sdumps
+        check_elf_dump elffilename sdumps
       end