Merge branch 'master' into nik_3d_probe

src/3d/FStar.Getopt.fsti

@@ -25,7 +25,7 @@ type opt_variant 'a =
   | ZeroArgs of (unit -> ML 'a)
   | OneArg of (string -> ML 'a) * string
 
-type opt' 'a = char * string * opt_variant 'a * string
+type opt' 'a = char * string * opt_variant 'a
 type opt = opt' unit
 
 type parse_cmdline_res =

src/3d/Main.fst

@@ -527,7 +527,7 @@ let produce_z3_and_test
   (name: string)
 : Tot process_files_t
 = produce_z3_and_test_gen batch out_dir (fun out_file nbwitnesses prog z3 ->
-    Z3TestGen.do_test out_dir out_file z3 prog name nbwitnesses (Options.get_z3_pos_test ()) (Options.get_z3_neg_test ())
+    Z3TestGen.do_test out_dir out_file z3 prog name nbwitnesses (Options.get_z3_branch_depth ()) (Options.get_z3_pos_test ()) (Options.get_z3_neg_test ())
   )
 
 let produce_z3_and_diff_test
@@ -538,7 +538,7 @@ let produce_z3_and_diff_test
 =
   let (name1, name2) = names in
   produce_z3_and_test_gen batch out_dir (fun out_file nbwitnesses prog z3 ->
-    Z3TestGen.do_diff_test out_dir out_file z3 prog name1 name2 nbwitnesses
+    Z3TestGen.do_diff_test out_dir out_file z3 prog name1 name2 nbwitnesses (Options.get_z3_branch_depth ())
   )
 
 let produce_test_checker_exe

src/3d/Options.fst

@@ -135,6 +135,10 @@ let z3_executable : ref (option vstring) = alloc None
 
 let test_checker : ref (option vstring) = alloc None
 
+let z3_branch_depth : ref (option vstring) = alloc None
+
+let z3_options : ref (option vstring) = alloc None
+
 noeq
 type cmd_option_kind =
   | OptBool:
@@ -151,6 +155,8 @@ type cmd_option_kind =
       (v: ref (list (valid_string valid))) ->
       cmd_option_kind
 
+let fstar_opt = FStar.Getopt.opt & string
+
 noeq
 type cmd_option
 = | CmdOption:
@@ -159,11 +165,11 @@ type cmd_option
     (desc: string) ->
     (implies: list string) (* name of OptBool to set to true *) ->
     cmd_option
-  | CmdFStarOption of FStar.Getopt.opt
+  | CmdFStarOption of fstar_opt
 
 let cmd_option_name (a: cmd_option) : Tot string =
   match a with
-  | CmdFStarOption (_, name', _, _)
+  | CmdFStarOption ((_, name', _), _)
   | CmdOption name' _ _ _
     -> name'
 
@@ -175,12 +181,12 @@ let rec find_cmd_option (name: string) (l: list cmd_option): Tot (option cmd_opt
 let cmd_option_description (a: cmd_option) : Tot string =
   match a with
   | CmdOption _ _ desc _
-  | CmdFStarOption (_, _, _, desc) ->
+  | CmdFStarOption (_, desc) ->
     desc
 
 let cmd_option_arg_desc (a: cmd_option) : Tot string =
   match a with
-  | CmdFStarOption (_, _, arg, _) ->
+  | CmdFStarOption ((_, _, arg), _) ->
     begin match arg with
     | FStar.Getopt.OneArg (_, argdesc) -> argdesc
     | _ -> ""
@@ -220,55 +226,61 @@ let negate_description (s: string) : Tot string = negate_string_gen s "Do not"
 let fstar_options_of_cmd_option
   (options: ref (list cmd_option))
   (o: cmd_option)
-: Tot (list FStar.Getopt.opt)
+: Tot (list fstar_opt)
 = match o with
   | CmdFStarOption f -> [f]
   | CmdOption name kind desc implies ->
     begin match kind with
     | OptBool v ->
       [
-        (FStar.Getopt.noshort, name, FStar.Getopt.ZeroArgs (fun _ -> set_implies options implies; v := true), desc);
-        (FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := false), negate_description desc);
+        ((FStar.Getopt.noshort, name, FStar.Getopt.ZeroArgs (fun _ -> set_implies options implies; v := true)), desc);
+        ((FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := false)), negate_description desc);
       ]
     | OptStringOption arg_desc valid v ->
       [
         (
-          FStar.Getopt.noshort, name,
-          FStar.Getopt.OneArg (
-            (fun (x: string) ->
-              if valid x
-              then begin
-                set_implies options implies;
-                v := Some x
-              end else
-                failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)
-            ),
-            arg_desc
+          (
+            FStar.Getopt.noshort, name,
+            FStar.Getopt.OneArg (
+              (fun (x: string) ->
+                if valid x
+                then begin
+                  set_implies options implies;
+                  v := Some x
+                end else
+                  failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)
+              ),
+              arg_desc
+            )
           ),
           desc
         );
-        (FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := None), negate_description desc)
+        ((FStar.Getopt.noshort, negate_name name, FStar.Getopt.ZeroArgs (fun _ -> v := None)), negate_description desc)
       ]
     | OptList arg_desc valid v ->
       [
         (
-          FStar.Getopt.noshort, name,
-          FStar.Getopt.OneArg (
-            (fun (x: string) ->
-              if valid x
-              then begin
-                set_implies options implies;
-                v := x :: !v
-              end else
-                failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)
-            ),
-            arg_desc
+          (
+            FStar.Getopt.noshort, name,
+            FStar.Getopt.OneArg (
+              (fun (x: string) ->
+                if valid x
+                then begin
+                  set_implies options implies;
+                  v := x :: !v
+                end else
+                  failwith (Printf.sprintf "Bad argument to %s: got %s, expected %s" name x arg_desc)
+              ),
+              arg_desc
+            )
           ),
           desc
         );
         (
-          FStar.Getopt.noshort, negate_name name,
-          FStar.Getopt.ZeroArgs (fun _ -> v := []),
+          (
+            FStar.Getopt.noshort, negate_name name,
+            FStar.Getopt.ZeroArgs (fun _ -> v := [])
+          ),
           desc
         );
       ]
@@ -357,7 +369,7 @@ let (display_usage_2, compute_options_2, fstar_options) =
     CmdOption "input_stream_include" (OptStringOption ".h file" always_valid input_stream_include) "Include file defining the EverParseInputStreamBase type (only for --input_stream extern or static)" [];
     CmdOption "no_copy_everparse_h" (OptBool no_copy_everparse_h) "Do not Copy EverParse.h (--batch only)" [];
     CmdOption "debug" (OptBool debug) "Emit a lot of debugging output" [];
-    CmdFStarOption ('h', "help", FStar.Getopt.ZeroArgs (fun _ -> display_usage (); exit 0), "Show this help message");
+    CmdFStarOption (('h', "help", FStar.Getopt.ZeroArgs (fun _ -> display_usage (); exit 0)), "Show this help message");
     CmdOption "json" (OptBool json) "Dump the AST in JSON format" [];
     CmdOption "makefile" (OptStringOption "gmake|nmake" valid_makefile makefile) "Do not produce anything, other than a Makefile to produce everything" [];
     CmdOption "makefile_name" (OptStringOption "some file name" always_valid makefile_name) "Name of the Makefile to produce (with --makefile, default <output directory>/EverParse.Makefile" [];
@@ -367,13 +379,15 @@ let (display_usage_2, compute_options_2, fstar_options) =
     CmdOption "skip_c_makefiles" (OptBool skip_c_makefiles) "Do not Generate Makefile.basic, Makefile.include" [];
     CmdOption "skip_o_rules" (OptBool skip_o_rules) "With --makefile, do not generate rules for .o files" [];
     CmdOption "test_checker" (OptStringOption "parser name" always_valid test_checker) "produce a test checker executable" [];
-    CmdFStarOption (let open FStar.Getopt in noshort, "version", ZeroArgs (fun _ -> FStar.IO.print_string (Printf.sprintf "EverParse/3d %s\nCopyright 2018, 2019, 2020 Microsoft Corporation\n" Version.everparse_version); exit 0), "Show this version of EverParse");
+    CmdFStarOption ((let open FStar.Getopt in noshort, "version", ZeroArgs (fun _ -> FStar.IO.print_string (Printf.sprintf "EverParse/3d %s\nCopyright 2018, 2019, 2020 Microsoft Corporation\n" Version.everparse_version); exit 0)), "Show this version of EverParse");
     CmdOption "equate_types" (OptList "an argument of the form A,B, to generate asserts of the form (A.t == B.t)" valid_equate_types equate_types_list) "Takes an argument of the form A,B and then for each entrypoint definition in B, it generates an assert (A.t == B.t) in the B.Types file, useful when refactoring specs, you can provide multiple equate_types on the command line" [];
+    CmdOption "z3_branch_depth" (OptStringOption "nb" always_valid z3_branch_depth) "enumerate branch choices up to depth nb (default 0)" [];
     CmdOption "z3_diff_test" (OptStringOption "parser1,parser2" valid_equate_types z3_diff_test) "produce differential tests for two parsers" [];
     CmdOption "z3_executable" (OptStringOption "path/to/z3" always_valid z3_executable) "z3 executable for test case generation (default `z3`; does not affect verification of generated F* code)" [];
+    CmdOption "z3_options" (OptStringOption "'options to z3'" always_valid z3_options) "command-line options to pass to z3 for test case generation (does not affect verification of generated F* code)" [];
     CmdOption "z3_test" (OptStringOption "parser name" always_valid z3_test) "produce positive and/or negative test cases for a given parser" [];
     CmdOption "z3_test_mode" (OptStringOption "pos|neg|all" valid_z3_test_mode z3_test_mode) "produce positive, negative, or all kinds of test cases (default all)" [];
-    CmdOption "z3_witnesses" (OptStringOption "nb" always_valid z3_witnesses) "ask for nb distinct test witnesses" [];
+    CmdOption "z3_witnesses" (OptStringOption "nb" always_valid z3_witnesses) "ask for nb distinct test witnesses per branch case (default 1)" [];
     CmdOption "__arg0" (OptStringOption "executable name" always_valid arg0) "executable name to use for the help message" [];
     CmdOption "__micro_step" (OptStringOption "verify|extract|copy_clang_format|emit_config" valid_micro_step micro_step) "micro step" [];
     CmdOption "__produce_c_from_existing_krml" (OptBool produce_c_from_existing_krml) "produce C from .krml files" [];
@@ -390,7 +404,7 @@ let compute_options = compute_options_2
 
 let parse_cmd_line () : ML (list string) =
   let open FStar.Getopt in
-  let res = FStar.Getopt.parse_cmdline fstar_options (fun file -> input_file := file :: !input_file; Success) in
+  let res = FStar.Getopt.parse_cmdline (List.Tot.map fst fstar_options) (fun file -> input_file := file :: !input_file; Success) in
   match res with
   | Success -> !input_file
   | Help -> display_usage(); exit 0
@@ -561,7 +575,10 @@ let get_z3_witnesses () =
   | Some s ->
   try
     let n = OS.int_of_string s in
-    if n < 1 then 1 else n
+    if n < 1 then (1 <: pos) else begin
+      assert (n >= 1);
+      (n <: pos)
+    end
   with _ -> 1
 
 let get_debug _ = !debug
@@ -579,3 +596,20 @@ let get_z3_executable () =
 let get_save_z3_transcript () = !save_z3_transcript
 
 let get_test_checker () = !test_checker
+
+let get_z3_branch_depth () =
+  match !z3_branch_depth with
+  | None -> 0
+  | Some s ->
+  try
+    let n = OS.int_of_string s in
+    if n < 0 then (0 <: nat) else begin
+      assert (n >= 0);
+      (n <: nat)
+    end
+  with _ -> 0
+
+let get_z3_options () : ML string = 
+  match !z3_options with
+  | None -> ""
+  | Some s -> s

src/3d/Options.fsti

@@ -70,7 +70,7 @@ val get_z3_pos_test: unit -> ML bool
 
 val get_z3_neg_test: unit -> ML bool
 
-val get_z3_witnesses: unit -> ML int
+val get_z3_witnesses: unit -> ML pos
 
 val get_debug: unit -> ML bool
 
@@ -79,3 +79,5 @@ val get_z3_diff_test: unit -> ML (option (string & string))
 val get_save_z3_transcript: unit -> ML (option string)
 
 val get_test_checker: unit -> ML (option string)
+
+val get_z3_branch_depth: unit -> ML nat