Better error reports for checklink

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

2 files changed, 98 insertions, 77 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 54de487..4de9721 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -36,6 +36,9 @@ let exhaustivity = ref true
 (** CompCert Asm *)
 type ccode = Asm.instruction list
 
+let print_debug s =
+  if !debug then print_endline (string_of_log_entry true (DEBUG(s)))
+
 (** 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 true entry);
@@ -91,10 +94,10 @@ let name_of_section:
     section_name -> string
   =
   begin match Configuration.system with
-  | "macosx" -> failwith "Unsupported CompCert configuration: macosx"
+  | "macosx" -> fatal "Unsupported CompCert configuration: macosx"
   | "linux"  -> name_of_section_Linux
   | "diab"   -> name_of_section_Diab
-  | _        -> failwith "Unsupported CompCert configuration"
+  | _        -> fatal "Unsupported CompCert configuration"
   end
 
 (** Compares a CompCert section name with an ELF section name. *)
@@ -409,7 +412,7 @@ let match_csts (cc: constant) (ec: int32) (ffw: f_framework): f_framework =
       end
   | Csymbol_sda (ident, i) ->
       (* sda should be handled separately in places it occurs *)
-      failwith "Unhandled Csymbol_sda, please report."
+      fatal "Unhandled Csymbol_sda, please report."
 
 let match_z_int32 (cz: coq_Z) (ei: int32) =
   check_eq "match_z_int32" (z_int32 cz) ei
@@ -534,7 +537,6 @@ let rec match_jmptbl lbllist vaddr size ffw =
           >>> lblmap_unify lbl vaddr
           >>= match_jmptbl_aux lbls rest
       | { _ } ->
-          print_endline "Ill-formed jump table";
           ERR("Ill-formed jump table")
     )
   in
@@ -789,7 +791,7 @@ let check_sda ident ofs r addr ffw: f_framework or_err =
   | [] -> ERR("No satisfying SDA mapping, errors were: " ^
                  string_of_list id ", " (filter_err res))
   | [ffw] -> OK(ffw)
-  | _ -> failwith "Multiple possible SDA mappings, please report."
+  | _ -> fatal "Multiple possible SDA mappings, please report."
 
 (** Compares a whole CompCert function code against an ELF code, starting at
     program counter [pc].
@@ -1346,7 +1348,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
                   fw
                   >>> check_builtin_vload_common
                     cs ecode pc chunk addr (Cint Integers.Int.zero) res
-              | _ -> failwith "Unexpected args in EF_vload, please report."
+              | _ -> fatal "Unexpected args in EF_vload, please report."
               end
           | EF_vstore(chunk) ->
               begin match args with
@@ -1354,7 +1356,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
                   fw
                   >>> check_builtin_vstore_common
                     cs ecode pc chunk addr (Cint Integers.Int.zero) src
-              | _ -> failwith "Unexpected args in EF_vstore, please report."
+              | _ -> fatal "Unexpected args in EF_vstore, please report."
               end
           | EF_vload_global(chunk, ident, ofs) ->
               begin match ecode with
@@ -1389,7 +1391,7 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
                         (Csymbol_low(ident, ofs)) src
                   | _ -> error
                   end
-              | _ -> failwith "Unexpected args in EF_vstore_global, please report."
+              | _ -> fatal "Unexpected args in EF_vstore_global, please report."
               end
           | EF_memcpy(sz, al) ->
               let sz = z_int sz in
@@ -1440,10 +1442,10 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
                   else compare_code cs ecode pc fw
               | _ -> error
               end
-          | EF_annot(_, _)    -> failwith "Unexpected EF_annot, please report."
-          | EF_external(_, _) -> failwith "Unexpected EF_external, please report."
-          | EF_free           -> failwith "Unexpected EF_free, please report."
-          | EF_malloc         -> failwith "Unexpected EF_malloc, please report."
+          | EF_annot(_, _)    -> fatal "Unexpected EF_annot, please report."
+          | EF_external(_, _) -> fatal "Unexpected EF_external, please report."
+          | EF_free           -> fatal "Unexpected EF_free, please report."
+          | EF_malloc         -> fatal "Unexpected EF_malloc, please report."
           end
       | Pcmplw(r1, r2) ->
           begin match ecode with
@@ -2851,7 +2853,7 @@ let check_stubs sfw =
               sfw
               >>> (sf_ef ^%= add_log (ERROR("Couldn't match stub")))
           end
-    | _ -> failwith "Unexpected fundef in check_stubs, please report."
+    | _ -> fatal "Unexpected fundef in check_stubs, please report."
     end
   in
   PosMap.fold check_stub sfw.stub_ident_to_vaddr sfw
@@ -2865,7 +2867,7 @@ let read_sdump file =
   try
     let magic = String.create (String.length sdump_magic_number) in
     really_input ic magic 0 (String.length sdump_magic_number);
-    if magic <> sdump_magic_number then failwith "bad magic number";
+    if magic <> sdump_magic_number then fatal "Bad magic number";
     let prog = (input_value ic: Asm.program) in
     let names = (input_value ic: (ident, string) Hashtbl.t) in
     let atoms = (input_value ic: (ident, C2C.atom_info) Hashtbl.t) in
@@ -2880,9 +2882,9 @@ let read_sdump file =
 (** Processes a .sdump file.
 *)
 let process_sdump efw sdump: e_framework =
-  if !debug then print_endline ("Beginning reading " ^ sdump);
+  print_debug ("Beginning reading " ^ sdump);
   let (prog, names, atoms) = read_sdump sdump in
-  if !debug then print_endline "Constructing mapping from idents to symbol indices";
+  print_debug ("Constructing mapping from idents to symbol indices");
   let ident_to_sym_ndx =
     Hashtbl.fold
       (fun ident name m ->
@@ -2893,7 +2895,7 @@ let process_sdump efw sdump: e_framework =
       names
       PosMap.empty
   in
-  if !debug then print_endline "Constructing worklist";
+  print_debug("Constructing worklist");
   let worklist_fundefs =
     List.filter
       (fun f ->
@@ -2908,11 +2910,11 @@ let process_sdump efw sdump: e_framework =
       (fun f ->
         match f with
         | ident, Internal ccode -> (ident, Hashtbl.find names ident, ccode)
-        | _,     External _     -> failwith "IMPOSSIBRU!"
+        | _,     External _     -> fatal "IMPOSSIBRU!"
       )
       worklist_fundefs
   in
-  if !debug then print_endline "Beginning processing of the worklist";
+  print_debug("Beginning processing of the worklist");
   efw
   >>> (fun efw ->
     {
@@ -2926,12 +2928,12 @@ let process_sdump efw sdump: e_framework =
   )
   >>> worklist_process wl
   >>> (fun sfw ->
-    if !debug then print_endline "Checking stubs";
+    print_debug "Checking stubs";
     sfw
   )
   >>> check_stubs
   >>> (fun sfw ->
-    if !debug then print_endline "Checking data";
+    print_debug "Checking data";
     sfw
   )
   >>> check_data prog.prog_vars
@@ -3237,7 +3239,7 @@ let check_elf_nodump elf sdumps =
       ELF_symbol_strtab
     >>> check_sym_tab_zero
   in
-  if !debug then print_endline "Done checking header, beginning processing of .sdumps";
+  print_debug "Done checking header, beginning processing of .sdumps";
   (* Thread the framework through the processing of all .sdump files *)
   List.fold_left process_sdump efw sdumps
   (* check the padding in between identified byte chunks *)
@@ -3252,26 +3254,30 @@ let check_elf_nodump elf sdumps =
     If requested, dump the calculated bytes mapping, so that it can be
     reused by the fuzzer. *)
 let check_elf_dump elffilename sdumps =
-  if !debug then print_endline "Beginning ELF parsing";
+  print_debug "Beginning ELF parsing";
   let elf = read_elf elffilename in
-  if !debug then print_endline "Beginning ELF checking";
+  print_debug "Beginning ELF checking";
   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;
+  if !print_elfmap
+  then
+    begin
+      Printf.printf "\n\n%s\n\n\n"
+        (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;
+  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
@@ -3293,12 +3299,11 @@ let check_elf_dump elffilename sdumps =
     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
-        );
-        print_newline ()
+        Printf.printf "%s\n%s\n\n"
+          (string_of_log_entry false
+             (WARNING("the following function symbols do not appear in .sdump files."))
+          )
+          (string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_fun)
     end
   ;
   (* indicate data symbols that have not been checked *)
@@ -3322,20 +3327,20 @@ let check_elf_dump elffilename sdumps =
     begin match miss_data with
     | [] -> ()
     | _  ->
-        print_endline
-          "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 ()
+        Printf.printf "%s\n%s\n\n"
+          (string_of_log_entry false
+             (WARNING("the following data symbols do not appear in .sdump files."))
+          )
+          (string_of_list (fun ndx -> efw.elf.e_symtab.(ndx).st_name) " " miss_data)
     end
   ;
   (* print diagnosis *)
   let worrysome = List.filter
     (function
-    | ERROR(_) -> true
+    | DEBUG(_)   -> false
+    | ERROR(_)   -> true
+    | INFO(_)    -> false
     | WARNING(_) -> true
-    | DEBUG(_) -> false
     )
     efw.log
   in
@@ -3346,21 +3351,30 @@ let check_elf_dump elffilename sdumps =
   in
   begin match worrysome with
   | [] ->
-      print_endline "\nEverything seems fine with this ELF.";
+      Printf.printf "%s\n\n"
+        (string_of_log_entry false
+           (INFO("Everything 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
+      then
+        begin
+          Printf.printf "%s\n\n"
+            (string_of_log_entry false
+               (INFO("However, some parts of the ELF could not be identified." ^
+                        if !print_elfmap
+                        then ""
+                        else " Use -printelfmap to see what was covered."
+                ))
+            )
+        end
   | _ ->
       if !debug
-      then print_endline (
-        "DEBUG MODE: The following messages are actual problems."
-      );
+      then
+        begin
+          Printf.printf "%s\n\n"
+            (string_of_log_entry false
+               (DEBUG("Final error log:")))
+        end;
       List.(iter
               (fun e ->
                 match string_of_log_entry false e with
diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml
index 46778e2..405d3be 100644
--- a/checklink/Frameworks.ml
+++ b/checklink/Frameworks.ml
@@ -6,8 +6,9 @@ open Lens
 open Library
 
 type log_entry =
-  | DEBUG of string
-  | ERROR of string
+  | DEBUG   of string
+  | ERROR   of string
+  | INFO    of string
   | WARNING of string
 
 type byte_chunk_desc =
@@ -16,16 +17,16 @@ type byte_chunk_desc =
   | ELF_shtab
   | ELF_section_strtab
   | ELF_symbol_strtab
-  | Symtab_data of elf32_sym
-  | Symtab_function of elf32_sym
-  | Data_symbol of elf32_sym
-  | Function_symbol of elf32_sym
+  | Symtab_data        of elf32_sym
+  | Symtab_function    of elf32_sym
+  | Data_symbol        of elf32_sym
+  | Function_symbol    of elf32_sym
   | Zero_symbol
-  | Stub of string
+  | Stub               of string
   | Jumptable
-  | Float_literal of float
+  | Float_literal      of float
   | Padding
-  | Unknown of string
+  | Unknown            of string
 
 (** This framework is carried along while analyzing the whole ELF file.
 *)
@@ -175,10 +176,16 @@ let ( ^%=? ) (lens: ('a, 'b) Lens.t) (transf: 'b -> 'b or_err)
 (** Finally, some printers.
 *)
 
-let string_of_log_entry show_debug = function
-| DEBUG(s)   -> if show_debug then s else ""
-| ERROR(s)   -> "ERROR: " ^ s
-| WARNING(s) -> "WARNING: " ^ s
+let format_logtype = Printf.sprintf "%10s"
+
+let string_of_log_entry show_debug entry =
+  match entry with
+  | DEBUG(s)   -> if show_debug then (format_logtype "DEBUG: ") ^ s else ""
+  | ERROR(s)   -> (format_logtype "ERROR: ") ^ s
+  | INFO(s)    -> (format_logtype "INFO: ") ^ s
+  | WARNING(s) -> (format_logtype "WARNING: ") ^ s
+
+let fatal s = failwith ((format_logtype "FATAL: ") ^ s)
 
 let string_of_byte_chunk_desc = function
 | ELF_header -> "ELF header"