checklink: first import of Valentin Robert's validator for asm and link

cparser: renamed Errors to Cerrors; removed packing into Cparser.


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

1 files changed, 56 insertions, 0 deletions

diff --git a/checklink/Validator.ml b/checklink/Validator.ml
new file mode 100644
index 0000000..b27bc4c
--- /dev/null
+++ b/checklink/Validator.ml
@@ -0,0 +1,56 @@
+open Check
+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_dumpelf = ref false
+
+let set_elf_file s =
+  match !elf_file with
+  | None -> elf_file := Some s
+  | Some _ -> raise (Arg.Bad "multiple ELF executables given on command line")
+
+let options = [
+  "-dumpelf", Arg.Set option_dumpelf,
+    "Print the contents of the ELF executable";
+  "-debug", Arg.Set Check.debug,
+    "Print a detailed trace of verification";
+  "-elfmap", Arg.Set Check.dump_elfmap,
+    "Dump an ELF map to <exename>.elfmap>, for use with random fuzzing";
+  "-exe <filename>", Arg.String set_elf_file,
+    "Specify the ELF executable file to analyze";
+  "-fuzz", Arg.Set option_fuzz,
+    "Random fuzzing test"
+]
+
+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 " ^ Configuration.version ^ "
+Usage: valink [options] <.sdump files> <ELF executable>
+Options are:"
+
+let _ =
+  Arg.parse options anonymous usage;
+  match !elf_file with
+  | None ->
+      Arg.usage options usage;
+      exit 2
+  | Some elffilename ->
+      let sdumps = List.rev !sdump_files in
+      if !option_fuzz then begin
+        Random.self_init();
+        fuzz_loop elffilename sdumps
+      end else if !option_dumpelf then begin
+        let elf = read_elf elffilename in
+        print_endline (string_of_elf elf)
+      end else begin
+        check_and_dump elffilename sdumps
+      end