diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 14:45:56 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 14:45:56 +0200 |
commit | ed6043fe910f7a320f7af6d3f9d35f39f5cf7ee1 (patch) | |
tree | 3fab134f5444f0472a1ff8c06e5b7686a40648dc /checklink/Validator.ml | |
parent | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (diff) | |
parent | 8a95c3e07fd02eaa87f8cca447bc7d7c2642eb22 (diff) | |
download | compcert-ed6043fe910f7a320f7af6d3f9d35f39f5cf7ee1.tar.gz compcert-ed6043fe910f7a320f7af6d3f9d35f39f5cf7ee1.zip |
Merge remote-tracking branch 'origin/master' into named-externals
Conflicts:
arm/TargetPrinter.ml
backend/CMparser.mly
backend/SelectLongproof.v
backend/Selectionproof.v
cfrontend/C2C.ml
checklink/Asm_printers.ml
checklink/Check.ml
checklink/Fuzz.ml
common/AST.v
debug/DebugInformation.ml
debug/DebugInit.ml
debug/DwarfPrinter.ml
debug/DwarfTypes.mli
debug/Dwarfgen.ml
exportclight/ExportClight.ml
ia32/TargetPrinter.ml
powerpc/Asm.v
powerpc/SelectOpproof.v
powerpc/TargetPrinter.ml
Diffstat (limited to 'checklink/Validator.ml')
-rw-r--r-- | checklink/Validator.ml | 132 |
1 files changed, 0 insertions, 132 deletions
diff --git a/checklink/Validator.ml b/checklink/Validator.ml deleted file mode 100644 index f9ca0edb..00000000 --- a/checklink/Validator.ml +++ /dev/null @@ -1,132 +0,0 @@ -open Check -open Disassembler -open ELF_parsers -open ELF_printers -open Fuzz - -let elf_file = ref (None: string option) -let sdump_files = ref ([] : string list) -let option_fuzz = ref false -let option_bytefuzz = ref false -let option_printelf = ref false - -let set_elf_file s = - begin match !elf_file with - | None -> elf_file := Some s - | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line") - end - -let set_conf_file s = - begin match !conf_file with - | None -> conf_file := Some s - | Some _ -> raise (Arg.Bad "multiple configuration files given on command line") - end - -let read_sdumps_from_channel ic = - try - while true do - let l = input_line ic in - if l <> "" then sdump_files := l :: !sdump_files - done - with End_of_file -> - () - -let read_sdumps_from_file f = - if f = "-" then - read_sdumps_from_channel stdin - else begin - try - let ic = open_in f in - read_sdumps_from_channel ic; - close_in ic - with Sys_error msg -> - Printf.eprintf "Error reading file: %s\n" msg; exit 2 - end - -let option_disassemble = ref false -let disassemble_list = ref ([]: string list) -let add_disassemble s = - disassemble_list := s :: !disassemble_list; - option_disassemble := true - -let options = [ - (* Main options *) - "-exe", Arg.String set_elf_file, - "<filename> Specify the ELF executable file to analyze"; - "-conf", Arg.String set_conf_file, - "<filename> Specify a configuration file"; - "-files-from", Arg.String read_sdumps_from_file, - "<filename> Read names of .sdump files from the given file\n\ - \t(or from standard input if <filename> is '-')"; - (* Parsing behavior *) - "-relaxed", Arg.Set ELF_parsers.relaxed, - "Allows the following behaviors in the ELF parser:\n\ -\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"; - "-disass", Arg.String add_disassemble, - "<symname> Disassemble the symbol with specified name (can be repeated)"; - "-print-elf", Arg.Set option_printelf, - "Print the contents of the unanalyzed ELF executable"; - (* ELF map related *) - "-print-elfmap", Arg.Set Check.print_elfmap, - "Print a map of the analyzed ELF executable"; - "-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 <exename>.elfmap, for use with random fuzzing"; - "-fuzz", Arg.Set option_fuzz, - "Random fuzz testing"; - "-fuzz-byte", Arg.Set option_bytefuzz, - "Random fuzz testing byte per byte"; - "-fuzz-debug", Arg.Set Fuzz.fuzz_debug, - "Print a detailed trace of ongoing fuzz testing"; -] - -let anonymous arg = - if Filename.check_suffix arg ".sdump" then - sdump_files := arg :: !sdump_files - else - set_elf_file arg - -let usage = - "The CompCert C post-linking validator, version " ^ Version.version ^ " -Usage: cchecklink [options] <.sdump files> <ELF executable> -In the absence of options, checks are performed and a short result is displayed. -Options are:" - -let _ = - Arg.parse options anonymous usage; - begin match !elf_file with - | None -> - Arg.usage options usage; - exit 2 - | Some elffilename -> - let sdumps = List.rev !sdump_files in - if !option_disassemble then begin - let elf = read_elf elffilename in - List.iter - (fun s -> - Printf.printf "Disassembling %s:\n%s\n\n" s (disassemble elf s) - ) - !disassemble_list - end else if !option_bytefuzz then begin - Random.self_init(); - fuzz_every_byte_loop elffilename sdumps - end else if !option_fuzz then begin - Random.self_init(); - fuzz_loop elffilename sdumps - end else if !option_printelf then begin - let elf = read_elf elffilename in - print_endline (string_of_elf elf) - end else begin - check_elf_dump elffilename sdumps - end - end |