Merge pull request #3717 from mtzguido/misc

Misc cleanups
FStarLang · Feb 5, 2025 · 5eb0d44 · 5eb0d44
2 parents 3f87f61 + 2ce5b4f
commit 5eb0d44
Show file tree

Hide file tree

Showing 6 changed files with 29 additions and 20 deletions.
diff --git a/mk/generic.mk b/mk/generic.mk
@@ -41,11 +41,11 @@ ocaml: all-ml
 .PHONY: verify
 verify: all-checked
 
-FSTAR_OPTIONS += $(OTHERFLAGS)
 FSTAR_OPTIONS += --odir "$(OUTPUT_DIR)"
 FSTAR_OPTIONS += --cache_dir "$(CACHE_DIR)"
 FSTAR_OPTIONS += --include "$(SRC)"
 FSTAR_OPTIONS += --cache_checked_modules
+FSTAR_OPTIONS += $(OTHERFLAGS)
 
 ifeq ($(ADMIT),1)
 FSTAR_OPTIONS += --admit_smt_queries true

diff --git a/mk/test.mk b/mk/test.mk
@@ -27,14 +27,16 @@ FSTAR_EXE ?= $(FSTAR_ROOT)/out/bin/fstar.exe
 FSTAR_EXE := $(abspath $(FSTAR_EXE))
 export FSTAR_EXE
 
-# This warning is really useless.
-OTHERFLAGS += --warn_error -321
-OTHERFLAGS += --ext context_pruning
-OTHERFLAGS += --z3version 4.13.3
+FSTAR_ARGS += --odir $(OUTPUT_DIR)
+FSTAR_ARGS += --cache_dir $(CACHE_DIR)
+FSTAR_ARGS += --already_cached Prims,FStar,LowStar
+FSTAR_ARGS += --warn_error -321 # This warning is really useless.
+FSTAR_ARGS += --ext context_pruning
+FSTAR_ARGS += --z3version 4.13.3
+FSTAR_ARGS += $(OTHERFLAGS)
 
 # Set ADMIT=1 to admit queries
-ADMIT ?=
-MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
+FSTAR_ARGS += $(if $(ADMIT),--admit_smt_queries true)
 
 # Almost everything goes into the OUTPUT_DIR, except for .checked files
 # which go in the CACHE_DIR. The .depend goes in the current directory.
@@ -43,12 +45,9 @@ MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
 OUTPUT_DIR ?= _output
 CACHE_DIR ?= _cache
 
-FSTAR = $(FSTAR_EXE) $(SIL) 				\
+FSTAR = $(FSTAR_EXE) $(SIL) 						\
 	$(if $(NO_WRITE_CHECKED),,--cache_checked_modules)		\
-	--odir $(OUTPUT_DIR)				\
-	--cache_dir $(CACHE_DIR)			\
-	--already_cached Prims,FStar,LowStar		\
-	 $(OTHERFLAGS) $(MAYBE_ADMIT)
+	$(FSTAR_ARGS)
 
 ifneq ($(MAKECMDGOALS),clean)
 ifeq ($(NODEPEND),) # Set NODEPEND=1 to not dependency analysis

diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst
@@ -233,6 +233,7 @@ type query_settings = {
     query_hash:option string;
     query_can_be_split_and_retried:bool;
     query_term: FStarC.Syntax.Syntax.term;
+    query_record_hints: bool;
 }
 
 (* Translation from F* rlimit units to Z3 rlimit units.
@@ -267,8 +268,10 @@ let with_fuel_and_diagnostics settings label_assumptions =
         Term.CheckSat; //go Z3!
         Term.SetOption ("rlimit", "0"); //back to using infinite rlimit
         Term.GetReasonUnknown; //explain why it failed
-        Term.GetUnsatCore; //for proof profiling, recording hints etc
-    ]
+    ]@
+    (if settings.query_record_hints
+     then [ Term.GetUnsatCore ]
+     else [])
     @(if (Options.print_z3_statistics() ||
           Options.query_stats ()) then [Term.GetStatistics] else []) //stats
     @settings.query_suffix //recover error labels and a final "Done!" message
@@ -846,6 +849,7 @@ let make_solver_configs
                         | Some {hash=h} -> h);
             query_can_be_split_and_retried=can_split;
             query_term=query_term;
+            query_record_hints=Options.record_hints();
         } in
         default_settings, next_hint
     in
@@ -1269,6 +1273,7 @@ type solver_cfg = {
   valid_elim       : bool;
   z3version        : string;
   context_pruning  : bool;
+  record_hints     : bool;
 }
 
 let _last_cfg : ref (option solver_cfg) = BU.mk_ref None
@@ -1282,6 +1287,7 @@ let get_cfg env : solver_cfg =
     ; valid_elim       = Options.smtencoding_valid_elim ()
     ; z3version        = Options.z3_version ()
     ; context_pruning  = Options.Ext.enabled "context_pruning"
+    ; record_hints     = Options.record_hints ()
     }
 
 let save_cfg env =
@@ -1527,7 +1533,7 @@ let solver = {
 
     solve=solve;
     solve_sync=solve_sync_bool;
-    finish=(fun () -> ());
+    finish=Z3.stop;
     refresh=Z3.refresh;
 }
 

diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst
@@ -409,6 +409,8 @@ let giveZ3 decls = with_solver_state_unit (SolverState.give decls)
 let refresh using_facts_from =
     (!bg_z3_proc).refresh();
     with_solver_state_unit (SolverState.reset using_facts_from)
+let stop () =
+    (!bg_z3_proc).refresh()
 
 let doZ3Exe (log_file:_) (r:Range.range) (fresh:bool) (input:string) (label_messages:error_labels) (queryid:string) : z3status & z3statistics =
   let parse (z3out:string) =

diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fsti b/src/smtencoding/FStarC.SMTEncoding.Z3.fsti
@@ -75,6 +75,9 @@ killing the current process. A new process will *not* be started
 until we actually need to perform a query. *)
 val refresh: option SolverState.using_facts_from_setting -> unit
 
+(* Kill the current background Z3 process. *)
+val stop : unit -> unit
+
 val push : msg:string -> unit
 val pop : msg:string -> unit
 val snapshot : string -> int

diff --git a/tests/micro-benchmarks/Makefile b/tests/micro-benchmarks/Makefile
@@ -1,8 +1,7 @@
-SUBDIRS += ns_resolution
-
-OTHERFLAGS+=--warn_error +240
-
 FSTAR_ROOT ?= ../..
 include $(FSTAR_ROOT)/mk/test.mk
 
-$(CACHE_DIR)/MustEraseForExtraction.fst.checked: OTHERFLAGS += --warn_error @318
+SUBDIRS += ns_resolution
+
+$(CACHE_DIR)/MustEraseForExtraction.fst.checked: FSTAR_ARGS += --warn_error @318
+FSTAR_ARGS += --warn_error +240