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 +++++++++++--------- checklink/ELF_printers.ml | 211 +++++++++++++++++++++++----------------------- checklink/Frameworks.ml | 4 +- checklink/Library.ml | 3 + checklink/Validator.ml | 34 +++++--- 5 files changed, 184 insertions(+), 161 deletions(-) (limited to 'checklink') 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) ) diff --git a/checklink/ELF_printers.ml b/checklink/ELF_printers.ml index f0f154e..ffdc414 100644 --- a/checklink/ELF_printers.ml +++ b/checklink/ELF_printers.ml @@ -7,145 +7,142 @@ let string_of_elf32_off = string_of_int32 let string_of_elf32_word = string_of_int32 let string_of_elfclass = function -| ELFCLASSNONE -> "ELFCLASSNONE" -| ELFCLASS32 -> "ELFCLASS32" -| ELFCLASS64 -> "ELFCLASS64" -| ELFCLASSUNKNOWN -> "ELFCLASSUNKNOWN" +| ELFCLASSNONE -> "ELFCLASSNONE" +| ELFCLASS32 -> "ELFCLASS32" +| ELFCLASS64 -> "ELFCLASS64" +| ELFCLASSUNKNOWN -> "ELFCLASSUNKNOWN" let string_of_elfdata = function -| ELFDATANONE -> "ELFDATANONE" -| ELFDATA2LSB -> "ELFDATA2LSB" -| ELFDATA2MSB -> "ELFDATA2MSB" -| ELFDATAUNKNOWN -> "ELFDATAUNKNOWN" +| ELFDATANONE -> "ELFDATANONE" +| ELFDATA2LSB -> "ELFDATA2LSB" +| ELFDATA2MSB -> "ELFDATA2MSB" +| ELFDATAUNKNOWN -> "ELFDATAUNKNOWN" let string_of_ev = function -| EV_NONE -> "EV_NONE" -| EV_CURRENT -> "EV_CURRENT" -| EV_UNKNOWN -> "EV_UNKNOWN" +| EV_NONE -> "EV_NONE" +| EV_CURRENT -> "EV_CURRENT" +| EV_UNKNOWN -> "EV_UNKNOWN" let string_of_elf_identification ei = - "{\nei_class = " ^ string_of_elfclass ei.ei_class ^ - ";\nei_data = " ^ string_of_elfdata ei.ei_data ^ + "{\nei_class = " ^ string_of_elfclass ei.ei_class ^ + ";\nei_data = " ^ string_of_elfdata ei.ei_data ^ ";\nei_version = " ^ string_of_ev ei.ei_version ^ ";\n}" let string_of_et = function -| ET_NONE -> "ET_NONE" -| ET_REL -> "ET_REL" -| ET_EXEC -> "ET_EXEC" -| ET_DYN -> "ET_DYN" -| ET_CORE -> "ET_CORE" -| ET_UNKNOWN -> "ET_UNKNOWN" +| ET_NONE -> "ET_NONE" +| ET_REL -> "ET_REL" +| ET_EXEC -> "ET_EXEC" +| ET_DYN -> "ET_DYN" +| ET_CORE -> "ET_CORE" +| ET_UNKNOWN -> "ET_UNKNOWN" let string_of_em = function -| EM_NONE -> "EM_NONE" -| EM_M32 -> "EM_M32" -| EM_SPARC -> "EM_SPARC" -| EM_386 -> "EM_386" -| EM_68K -> "EM_68K" -| EM_88K -> "EM_88K" -| EM_860 -> "EM_860" -| EM_MIPS -> "EM_MIPS" -| EM_MIPS_RS4_BE -> "EM_MIPS_RS4_BE" -| EM_PPC -> "EM_PPC" -| EM_UNKNOWN -> "EM_UNKNOWN" +| EM_NONE -> "EM_NONE" +| EM_M32 -> "EM_M32" +| EM_SPARC -> "EM_SPARC" +| EM_386 -> "EM_386" +| EM_68K -> "EM_68K" +| EM_88K -> "EM_88K" +| EM_860 -> "EM_860" +| EM_MIPS -> "EM_MIPS" +| EM_MIPS_RS4_BE -> "EM_MIPS_RS4_BE" +| EM_PPC -> "EM_PPC" +| EM_UNKNOWN -> "EM_UNKNOWN" let string_of_elf32_ehdr eh = - "{\ne_ident = " ^ string_of_elf_identification eh.e_ident ^ - ";\ne_type = " ^ string_of_et eh.e_type ^ - ";\ne_machine = " ^ string_of_em eh.e_machine ^ - ";\ne_version = " ^ string_of_ev eh.e_version ^ - ";\ne_entry = " ^ string_of_elf32_addr eh.e_entry ^ - ";\ne_phoff = " ^ string_of_elf32_off eh.e_phoff ^ - ";\ne_shoff = " ^ string_of_elf32_off eh.e_shoff ^ - ";\ne_flags = " ^ string_of_bitstring eh.e_flags ^ - ";\ne_ehsize = " ^ string_of_elf32_half eh.e_ehsize ^ - ";\ne_phentsize = " ^ string_of_elf32_half eh.e_phentsize ^ - ";\ne_phnum = " ^ string_of_elf32_half eh.e_phnum ^ - ";\ne_shentsize = " ^ string_of_elf32_half eh.e_shentsize ^ - ";\ne_shnum = " ^ string_of_elf32_half eh.e_shnum ^ - ";\ne_shstrndx = " ^ string_of_elf32_half eh.e_shstrndx ^ + "{\ne_ident = " ^ string_of_elf_identification eh.e_ident ^ + ";\ne_type = " ^ string_of_et eh.e_type ^ + ";\ne_machine = " ^ string_of_em eh.e_machine ^ + ";\ne_version = " ^ string_of_ev eh.e_version ^ + ";\ne_entry = " ^ string_of_elf32_addr eh.e_entry ^ + ";\ne_phoff = " ^ string_of_elf32_off eh.e_phoff ^ + ";\ne_shoff = " ^ string_of_elf32_off eh.e_shoff ^ + ";\ne_flags = " ^ string_of_bitstring eh.e_flags ^ + ";\ne_ehsize = " ^ string_of_elf32_half eh.e_ehsize ^ + ";\ne_phentsize = " ^ string_of_elf32_half eh.e_phentsize ^ + ";\ne_phnum = " ^ string_of_elf32_half eh.e_phnum ^ + ";\ne_shentsize = " ^ string_of_elf32_half eh.e_shentsize ^ + ";\ne_shnum = " ^ string_of_elf32_half eh.e_shnum ^ + ";\ne_shstrndx = " ^ string_of_elf32_half eh.e_shstrndx ^ ";\n}" let string_of_sht = function -| SHT_NULL -> "SHT_NULL" -| SHT_PROGBITS -> "SHT_PROGBITS" -| SHT_SYMTAB -> "SHT_SYMTAB" -| SHT_STRTAB -> "SHT_STRTAB" -| SHT_RELA -> "SHT_RELA" -| SHT_HASH -> "SHT_HASH" -| SHT_DYNAMIC -> "SHT_DYNAMIC" -| SHT_NOTE -> "SHT_NOTE" -| SHT_NOBITS -> "SHT_NOBITS" -| SHT_REL -> "SHT_REL" -| SHT_SHLIB -> "SHT_SHLIB" -| SHT_DYNSYM -> "SHT_DYNSYM" -| SHT_UNKNOWN -> "SHT_UNKNOWN" +| SHT_NULL -> "SHT_NULL" +| SHT_PROGBITS -> "SHT_PROGBITS" +| SHT_SYMTAB -> "SHT_SYMTAB" +| SHT_STRTAB -> "SHT_STRTAB" +| SHT_RELA -> "SHT_RELA" +| SHT_HASH -> "SHT_HASH" +| SHT_DYNAMIC -> "SHT_DYNAMIC" +| SHT_NOTE -> "SHT_NOTE" +| SHT_NOBITS -> "SHT_NOBITS" +| SHT_REL -> "SHT_REL" +| SHT_SHLIB -> "SHT_SHLIB" +| SHT_DYNSYM -> "SHT_DYNSYM" +| SHT_UNKNOWN -> "SHT_UNKNOWN" let string_of_elf32_shdr sh = - "{\nsh_name = " ^ sh.sh_name ^ - ";\nsh_type = " ^ string_of_sht sh.sh_type ^ - ";\nsh_flags = " ^ string_of_elf32_word sh.sh_flags ^ - ";\nsh_addr = " ^ string_of_elf32_addr sh.sh_addr ^ - ";\nsh_offset = " ^ string_of_elf32_off sh.sh_offset ^ - ";\nsh_size = " ^ string_of_elf32_word sh.sh_size ^ - ";\nsh_link = " ^ string_of_elf32_word sh.sh_link ^ - ";\nsh_info = " ^ string_of_elf32_word sh.sh_info ^ - ";\nsh_addralign = " ^ string_of_elf32_word sh.sh_addralign ^ - ";\nsh_entsize = " ^ string_of_elf32_word sh.sh_entsize ^ + "{\nsh_name = " ^ sh.sh_name ^ + ";\nsh_type = " ^ string_of_sht sh.sh_type ^ + ";\nsh_flags = " ^ string_of_elf32_word sh.sh_flags ^ + ";\nsh_addr = " ^ string_of_elf32_addr sh.sh_addr ^ + ";\nsh_offset = " ^ string_of_elf32_off sh.sh_offset ^ + ";\nsh_size = " ^ string_of_elf32_word sh.sh_size ^ + ";\nsh_link = " ^ string_of_elf32_word sh.sh_link ^ + ";\nsh_info = " ^ string_of_elf32_word sh.sh_info ^ + ";\nsh_addralign = " ^ string_of_elf32_word sh.sh_addralign ^ + ";\nsh_entsize = " ^ string_of_elf32_word sh.sh_entsize ^ ";\n}" let string_of_p_type = function -| PT_NULL -> "PT_NULL" -| PT_LOAD -> "PT_LOAD" -| PT_DYNAMIC -> "PT_DYNAMIC" -| PT_INTERP -> "PT_INTERP" -| PT_NOTE -> "PT_NOTE" -| PT_SHLIB -> "PT_SHLIB" -| PT_PHDR -> "PT_PHDR" -| PT_UNKNOWN -> "PT_UNKNOWN" +| PT_NULL -> "PT_NULL" +| PT_LOAD -> "PT_LOAD" +| PT_DYNAMIC -> "PT_DYNAMIC" +| PT_INTERP -> "PT_INTERP" +| PT_NOTE -> "PT_NOTE" +| PT_SHLIB -> "PT_SHLIB" +| PT_PHDR -> "PT_PHDR" +| PT_UNKNOWN -> "PT_UNKNOWN" let string_of_elf32_phdr ph = - "{\np_type = " ^ string_of_p_type ph.p_type ^ - ";\np_offset = " ^ string_of_elf32_off ph.p_offset ^ - ";\np_vaddr = " ^ string_of_elf32_addr ph.p_vaddr ^ - ";\np_paddr = " ^ string_of_elf32_addr ph.p_paddr ^ - ";\np_filesz = " ^ string_of_elf32_word ph.p_filesz ^ - ";\np_memsz = " ^ string_of_elf32_word ph.p_memsz ^ - ";\np_flags = " ^ string_of_bitstring ph.p_flags ^ - ";\np_align = " ^ string_of_elf32_word ph.p_align ^ + "{\np_type = " ^ string_of_p_type ph.p_type ^ + ";\np_offset = " ^ string_of_elf32_off ph.p_offset ^ + ";\np_vaddr = " ^ string_of_elf32_addr ph.p_vaddr ^ + ";\np_paddr = " ^ string_of_elf32_addr ph.p_paddr ^ + ";\np_filesz = " ^ string_of_elf32_word ph.p_filesz ^ + ";\np_memsz = " ^ string_of_elf32_word ph.p_memsz ^ + ";\np_flags = " ^ string_of_bitstring ph.p_flags ^ + ";\np_align = " ^ string_of_elf32_word ph.p_align ^ ";\n}" let string_of_elf32_st_bind = function -| STB_LOCAL -> "STB_LOCAL" -| STB_GLOBAL -> "STB_GLOBAL" -| STB_WEAK -> "STB_WEAK" -| STB_UNKNOWN -> "STB_UNKNOWN" +| STB_LOCAL -> "STB_LOCAL" +| STB_GLOBAL -> "STB_GLOBAL" +| STB_WEAK -> "STB_WEAK" +| STB_UNKNOWN -> "STB_UNKNOWN" let string_of_elf32_st_type = function -| STT_NOTYPE -> "STT_NOTYPE" -| STT_OBJECT -> "STT_OBJECT" -| STT_FUNC -> "STT_FUNC" -| STT_SECTION -> "STT_SECTION" -| STT_FILE -> "STT_FILE" -| STT_UNKNOWN -> "STT_UNKNOWN" +| STT_NOTYPE -> "STT_NOTYPE" +| STT_OBJECT -> "STT_OBJECT" +| STT_FUNC -> "STT_FUNC" +| STT_SECTION -> "STT_SECTION" +| STT_FILE -> "STT_FILE" +| STT_UNKNOWN -> "STT_UNKNOWN" let string_of_elf32_sym s = - "{\nst_name = " ^ s.st_name ^ - ";\nst_value = " ^ string_of_elf32_addr s.st_value ^ - ";\nst_size = " ^ string_of_elf32_word s.st_size ^ - ";\nst_bind = " ^ string_of_elf32_st_bind s.st_bind ^ - ";\nst_type = " ^ string_of_elf32_st_type s.st_type ^ - ";\nst_other = " ^ string_of_int s.st_other ^ - ";\nst_shndx = " ^ string_of_elf32_half s.st_shndx ^ + "{\nst_name = " ^ s.st_name ^ + ";\nst_value = " ^ string_of_elf32_addr s.st_value ^ + ";\nst_size = " ^ string_of_elf32_word s.st_size ^ + ";\nst_bind = " ^ string_of_elf32_st_bind s.st_bind ^ + ";\nst_type = " ^ string_of_elf32_st_type s.st_type ^ + ";\nst_other = " ^ string_of_int s.st_other ^ + ";\nst_shndx = " ^ string_of_elf32_half s.st_shndx ^ ";\n}" let string_of_elf e = - "{\ne_header = " ^ string_of_elf32_ehdr e.e_hdr ^ - ";\ne_sections = " ^ - string_of_array string_of_elf32_shdr ",\n" e.e_shdra ^ - ";\ne_programs = " ^ - string_of_array string_of_elf32_phdr ",\n" e.e_phdra ^ - ";\ne_symtab = " ^ - string_of_array string_of_elf32_sym ",\n" e.e_symtab ^ + "{\ne_header = " ^ string_of_elf32_ehdr e.e_hdr ^ + ";\ne_sections = " ^ string_of_array string_of_elf32_shdr ",\n" e.e_shdra ^ + ";\ne_programs = " ^ string_of_array string_of_elf32_phdr ",\n" e.e_phdra ^ + ";\ne_symtab = " ^ string_of_array string_of_elf32_sym ",\n" e.e_symtab ^ ";\n}" diff --git a/checklink/Frameworks.ml b/checklink/Frameworks.ml index 828299e..72b00b4 100644 --- a/checklink/Frameworks.ml +++ b/checklink/Frameworks.ml @@ -187,6 +187,8 @@ let string_of_log_entry show_debug entry = let fatal s = failwith ((format_logtype "FATAL: ") ^ s) +let verbose_elfmap = ref false + let string_of_byte_chunk_desc = function | ELF_header -> "ELF header" | ELF_progtab -> "ELF program header table" @@ -202,4 +204,4 @@ let string_of_byte_chunk_desc = function | Jumptable -> "Jump table" | Float_literal(f) -> "Float literal: " ^ string_of_float f | Padding -> "Padding" -| Unknown(s) -> " ??? " ^ s +| Unknown(s) -> "???" ^ (if !verbose_elfmap then s else "") diff --git a/checklink/Library.ml b/checklink/Library.ml index ebcbac8..f6b1883 100644 --- a/checklink/Library.ml +++ b/checklink/Library.ml @@ -161,3 +161,6 @@ let sorted_lookup (compare: 'a -> 'b -> int) (arr: 'a array) (v: 'b): 'a option then sorted_lookup_aux i_from (i_mid - 1) else Some(arr.(i_mid)) in sorted_lookup_aux 0 (Array.length arr - 1) + +let list_false_indices a = + filter_some (Array.(to_list (mapi (fun ndx b -> if b then None else Some(ndx)) a))) diff --git a/checklink/Validator.ml b/checklink/Validator.ml index 34c9cbc..1edcdb4 100644 --- a/checklink/Validator.ml +++ b/checklink/Validator.ml @@ -23,29 +23,39 @@ let add_disassemble s = option_disassemble := true let options = [ + (* Main options *) "-exe", Arg.String set_elf_file, " Specify the ELF executable file to analyze"; - "-disass", Arg.String add_disassemble, - " Disassemble the symbol with specified name (can be repeated)"; + (* Parsing behavior *) + "-relaxed", Arg.Set ELF_parsers.relaxed, + "Allows the following behaviors in the ELF parser: +\t* Use of a fallback heuristic to resolve symbols bootstrapped at load time"; + (* Printing behavior *) + "-no-exhaustive", Arg.Clear Check.exhaustivity, + "Disable the exhaustivity check of ELF function and data symbols"; + "-list-missing", Arg.Set Check.list_missing, + "List function and data symbols that were missing in the exhaustivity check"; + (* Alternative outputs *) "-debug", Arg.Set Check.debug, "Print a detailed trace of verification"; - "-noexhaust", Arg.Clear Check.exhaustivity, - "Disable the exhaustivity check of ELF function and data symbols"; - "-printelf", Arg.Set option_printelf, + "-disass", Arg.String add_disassemble, + " Disassemble the symbol with specified name (can be repeated)"; + "-print-elf", Arg.Set option_printelf, "Print the contents of the unanalyzed ELF executable"; - "-printelfmap", Arg.Set Check.print_elfmap, + (* ELF map related *) + "-print-elfmap", Arg.Set Check.print_elfmap, "Print a map of the analyzed ELF executable"; - "-dumpelfmap", Arg.Set Check.dump_elfmap, + "-verbose-elfmap", Arg.Set Frameworks.verbose_elfmap, + "Show sections and symbols contained in the unknown parts of the elf map"; + (* Fuzz testing related *) + "-dump-elfmap", Arg.Set Check.dump_elfmap, "Dump an ELF map to .elfmap, for use with random fuzzing"; "-fuzz", Arg.Set option_fuzz, "Random fuzz testing"; - "-bytefuzz", Arg.Set option_bytefuzz, + "-fuzz-byte", Arg.Set option_bytefuzz, "Random fuzz testing byte per byte"; - "-debugfuzz", Arg.Set Fuzz.fuzz_debug, + "-fuzz-debug", Arg.Set Fuzz.fuzz_debug, "Print a detailed trace of ongoing fuzz testing"; - "-relaxed", Arg.Set ELF_parsers.relaxed, - "Allows the following behaviors in the ELF parser: -\t* Use of a fallback heuristic to resolve symbols bootstrapped at load time"; ] let anonymous arg = -- cgit v1.2.3