From 6256626f743bfcdd488fa1ec9d086d14f11109b4 Mon Sep 17 00:00:00 2001 From: varobert Date: Mon, 4 Jun 2012 08:53:56 +0000 Subject: checklink: improved user-friendliness Command-line options have been renamed and reordered. Error messages verbosity is more fine-grained. Possibly spurious debug messages are more clearly separated from the actual conclusions of the process. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1913 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 93 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 52 insertions(+), 41 deletions(-) (limited to 'checklink/Check.ml') diff --git a/checklink/Check.ml b/checklink/Check.ml index 3b146b0..6b3653b 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -23,16 +23,20 @@ open Sections *) let debug = ref false -(** Whether to print the ELF map *) +(** Whether to print the ELF map. *) let print_elfmap = ref false -(** Whether to dump the ELF map *) +(** 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 *) + against CompCert idents. *) let exhaustivity = ref true +(** Whether to print the list of all symbols (function and data) that were not + found in .sdump files. *) +let list_missing = ref false + (** CompCert Asm *) type ccode = Asm.instruction list @@ -41,7 +45,7 @@ let print_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); + if !debug then print_endline ("--DEBUG-- " ^ string_of_log_entry true entry); {efw with log = entry :: efw.log} (** [flag] should have only one bit set. *) @@ -380,12 +384,13 @@ let match_csts (cc: constant) (ec: int32): checker = fun ffw -> let efw = ffw |. ff_ef in match cc with | Cint (i) -> + let i = z_int32_lax i in let msg = Printf.sprintf "match_csts Cint %s %s" - (string_of_z i) + (string_of_int32 i) (string_of_int32 ec) in - check_eq msg ec (z_int32_lax i) ffw + check_eq msg ec i ffw | Csymbol_low (ident, i) -> let candidates = try PosMap.find ident sfw.ident_to_sym_ndx @@ -3315,25 +3320,30 @@ let check_elf_dump elffilename sdumps = 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 - ) - ) - ) + (list_false_indices efw.chkd_fun_syms) in if !exhaustivity then begin match miss_fun with | [] -> () | _ -> - 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) + if !list_missing + then + Printf.printf "%s\n%s\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) + else + print_endline + (string_of_log_entry false + (WARNING( + Printf.sprintf + "%d function symbols do not appear in .sdump files. Add -list-missing to list them." + (List.length miss_fun) + ) + ) + ) end ; (* indicate data symbols that have not been checked *) @@ -3343,25 +3353,30 @@ let check_elf_dump elffilename sdumps = 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 - ) - ) - ) + (list_false_indices efw.chkd_data_syms) in if !exhaustivity then begin match miss_data with | [] -> () | _ -> - 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) + if !list_missing + then + Printf.printf "%s\n%s\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) + else + print_endline + (string_of_log_entry false + (WARNING( + Printf.sprintf + "%d data symbols do not appear in .sdump files. Add -list-missing to list them." + (List.length miss_data) + ) + ) + ) end ; (* print diagnosis *) @@ -3381,14 +3396,14 @@ let check_elf_dump elffilename sdumps = in begin match worrysome with | [] -> - Printf.printf "%s\n\n" + Printf.printf "%s\n" (string_of_log_entry false (INFO("Everything seems fine with this ELF.")) ); if exists_unknown_chunk then begin - Printf.printf "%s\n\n" + Printf.printf "%s\n" (string_of_log_entry false (INFO("However, some parts of the ELF could not be identified." ^ if !print_elfmap @@ -3399,17 +3414,13 @@ let check_elf_dump elffilename sdumps = end | _ -> if !debug - then - begin - Printf.printf "%s\n\n" - (string_of_log_entry false - (DEBUG("Final error log:"))) - end; + then Printf.printf "%s\n" + (string_of_log_entry true (DEBUG("Final error log:"))); List.(iter (fun e -> match string_of_log_entry false e with | "" -> () - | s -> print_endline s + | s -> print_endline (s ^ "scoubidou") ) (rev efw.log) ) -- cgit v1.2.3