summaryrefslogtreecommitdiff
path: root/checklink
diff options
context:
space:
mode:
Diffstat (limited to 'checklink')
-rw-r--r--checklink/Check.ml142
-rw-r--r--checklink/Frameworks.ml33
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"