3d: allow timeout-limited breadth-first search

src/3d/HashingOptions.fst

@@ -36,3 +36,8 @@ let input_stream_include = function
   | InputStreamBuffer -> ""
   | InputStreamStatic s
   | InputStreamExtern s -> s
+
+type timeout_options =
+  | TimeoutUnspecified
+  | TimeoutUnlimited
+  | Timeout of pos

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_branch_depth ()) (Options.get_z3_pos_test ()) (Options.get_z3_neg_test ())
+    Z3TestGen.do_test out_dir out_file z3 prog name nbwitnesses (Options.get_z3_timeout ()) (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 (Options.get_z3_branch_depth ())
+    Z3TestGen.do_diff_test out_dir out_file z3 prog name1 name2 nbwitnesses (Options.get_z3_timeout ()) (Options.get_z3_branch_depth ())
   )
 
 let produce_test_checker_exe

src/3d/OS.fsti

@@ -29,6 +29,10 @@ val file_contents: string -> FStar.All.ML string
 
 val write_witness_to_file: list int -> string -> FStar.All.ML unit
 
+(* Timestamp, to implement the --z3_timeout option *)
+
+val timestamp : unit -> FStar.All.ML nat
+
 (* Moved here to break dependency cycle *)
 
-val int_of_string (x:string) : FStar.All.ML int
+val int_of_string (x:string) : FStar.All.ML int

src/3d/Options.fst

@@ -140,6 +140,8 @@ let z3_branch_depth : ref (option vstring) = alloc None
 
 let z3_options : ref (option vstring) = alloc None
 
+let z3_timeout : ref (option vstring) = alloc None
+
 noeq
 type cmd_option_kind =
   | OptBool:
@@ -385,6 +387,7 @@ let (display_usage_2, compute_options_2, fstar_options) =
     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_global_timeout" (OptStringOption "seconds|unlimited" always_valid z3_timeout) "global approximate timeout for z3 test case generation, or unlimited. Required unless --z3_branch_depth is given" [];
     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)" [];
@@ -601,17 +604,30 @@ let get_test_checker () = !test_checker
 
 let get_z3_branch_depth () =
   match !z3_branch_depth with
-  | None -> 0
+  | None -> None
   | Some s ->
   try
     let n = OS.int_of_string s in
-    if n < 0 then (0 <: nat) else begin
+    if n < 0 then None else begin
       assert (n >= 0);
-      (n <: nat)
+      Some (n <: nat)
     end
-  with _ -> 0
+  with _ -> None
 
 let get_z3_options () : ML string = 
   match !z3_options with
   | None -> ""
   | Some s -> s
+
+let get_z3_timeout () : ML timeout_options =
+  match !z3_timeout with
+  | None -> TimeoutUnspecified
+  | Some "unlimited" -> TimeoutUnlimited
+  | Some s ->
+    try
+      let n = OS.int_of_string s in
+      if n <= 0 then TimeoutUnspecified else begin
+        assert (n > 0);
+        Timeout n
+      end
+    with _ -> TimeoutUnspecified

src/3d/Options.fsti

@@ -80,4 +80,6 @@ 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
+val get_z3_branch_depth: unit -> ML (option nat)
+
+val get_z3_timeout: unit -> ML timeout_options