diff --git a/ocaml/fstar-lib/FStar_Hash.ml b/ocaml/fstar-lib/FStar_Hash.ml index 46fae6ea79f..dc2652b5339 100644 --- a/ocaml/fstar-lib/FStar_Hash.ml +++ b/ocaml/fstar-lib/FStar_Hash.ml @@ -1,5 +1,10 @@ module BU = FStar_Compiler_Util +module Z = FStar_BigInt + type hash_code = int + +let cmp_hash (x:hash_code) (y:hash_code) : Z.t = Z.of_int (x-y) + let of_int (i:Z.t) = Z.to_int i let of_string (s:string) = BatHashtbl.hash s diff --git a/ocaml/fstar-lib/generated/FStar_Class_Hashable.ml b/ocaml/fstar-lib/generated/FStar_Class_Hashable.ml new file mode 100644 index 00000000000..a8dd25810d3 --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_Class_Hashable.ml @@ -0,0 +1,194 @@ +open Prims +type 'a hashable = { + hash: 'a -> FStar_Hash.hash_code } +let __proj__Mkhashable__item__hash : + 'a . 'a hashable -> 'a -> FStar_Hash.hash_code = + fun projectee -> match projectee with | { hash;_} -> hash +let hash : 'a . 'a hashable -> 'a -> FStar_Hash.hash_code = + fun projectee -> match projectee with | { hash = hash1;_} -> hash1 +let (showable_hash_code : FStar_Hash.hash_code FStar_Class_Show.showable) = + { FStar_Class_Show.show = FStar_Hash.string_of_hash_code } +let (eq_hash_code : FStar_Hash.hash_code FStar_Class_Deq.deq) = + { FStar_Class_Deq.op_Equals_Question = (=) } +let (ord_hash_code : FStar_Hash.hash_code FStar_Class_Ord.ord) = + { + FStar_Class_Ord.super = eq_hash_code; + FStar_Class_Ord.cmp = + (fun x -> + fun y -> + let uu___ = FStar_Hash.cmp_hash x y in + FStar_Compiler_Order.order_from_int uu___) + } +let (hashable_int : Prims.int hashable) = { hash = FStar_Hash.of_int } +let (hashable_string : Prims.string hashable) = + { hash = FStar_Hash.of_string } +let (hashable_bool : Prims.bool hashable) = + { + hash = + (fun b -> + if b + then FStar_Hash.of_int Prims.int_one + else FStar_Hash.of_int (Prims.of_int (2))) + } +let hashable_list : 'a . 'a hashable -> 'a Prims.list hashable = + fun uu___ -> + { + hash = + (fun xs -> + let uu___1 = FStar_Hash.of_int Prims.int_zero in + FStar_Compiler_List.fold_left + (fun h -> + fun x -> let uu___2 = hash uu___ x in FStar_Hash.mix h uu___2) + uu___1 xs) + } +let hashable_option : + 'a . 'a hashable -> 'a FStar_Pervasives_Native.option hashable = + fun uu___ -> + { + hash = + (fun x -> + match x with + | FStar_Pervasives_Native.None -> FStar_Hash.of_int Prims.int_zero + | FStar_Pervasives_Native.Some x1 -> + let uu___1 = FStar_Hash.of_int Prims.int_one in + let uu___2 = hash uu___ x1 in FStar_Hash.mix uu___1 uu___2) + } +let hashable_either : + 'a 'b . + 'a hashable -> 'b hashable -> ('a, 'b) FStar_Pervasives.either hashable + = + fun uu___ -> + fun uu___1 -> + { + hash = + (fun x -> + match x with + | FStar_Pervasives.Inl a1 -> + let uu___2 = FStar_Hash.of_int Prims.int_zero in + let uu___3 = hash uu___ a1 in FStar_Hash.mix uu___2 uu___3 + | FStar_Pervasives.Inr b1 -> + let uu___2 = FStar_Hash.of_int Prims.int_one in + let uu___3 = hash uu___1 b1 in FStar_Hash.mix uu___2 uu___3) + } +let hashable_tuple2 : + 'a 'b . 'a hashable -> 'b hashable -> ('a * 'b) hashable = + fun uu___ -> + fun uu___1 -> + { + hash = + (fun uu___2 -> + match uu___2 with + | (a1, b1) -> + let uu___3 = hash uu___ a1 in + let uu___4 = hash uu___1 b1 in FStar_Hash.mix uu___3 uu___4) + } +let hashable_tuple3 : + 'a 'b 'c . + 'a hashable -> 'b hashable -> 'c hashable -> ('a * 'b * 'c) hashable + = + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + { + hash = + (fun uu___3 -> + match uu___3 with + | (a1, b1, c1) -> + let uu___4 = + let uu___5 = hash uu___ a1 in + let uu___6 = hash uu___1 b1 in + FStar_Hash.mix uu___5 uu___6 in + let uu___5 = hash uu___2 c1 in + FStar_Hash.mix uu___4 uu___5) + } +let hashable_tuple4 : + 'a 'b 'c 'd . + 'a hashable -> + 'b hashable -> + 'c hashable -> 'd hashable -> ('a * 'b * 'c * 'd) hashable + = + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + fun uu___3 -> + { + hash = + (fun uu___4 -> + match uu___4 with + | (a1, b1, c1, d1) -> + let uu___5 = + let uu___6 = + let uu___7 = hash uu___ a1 in + let uu___8 = hash uu___1 b1 in + FStar_Hash.mix uu___7 uu___8 in + let uu___7 = hash uu___2 c1 in + FStar_Hash.mix uu___6 uu___7 in + let uu___6 = hash uu___3 d1 in + FStar_Hash.mix uu___5 uu___6) + } +let hashable_tuple5 : + 'a 'b 'c 'd 'e . + 'a hashable -> + 'b hashable -> + 'c hashable -> + 'd hashable -> 'e hashable -> ('a * 'b * 'c * 'd * 'e) hashable + = + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + fun uu___3 -> + fun uu___4 -> + { + hash = + (fun uu___5 -> + match uu___5 with + | (a1, b1, c1, d1, e1) -> + let uu___6 = + let uu___7 = + let uu___8 = + let uu___9 = hash uu___ a1 in + let uu___10 = hash uu___1 b1 in + FStar_Hash.mix uu___9 uu___10 in + let uu___9 = hash uu___2 c1 in + FStar_Hash.mix uu___8 uu___9 in + let uu___8 = hash uu___3 d1 in + FStar_Hash.mix uu___7 uu___8 in + let uu___7 = hash uu___4 e1 in + FStar_Hash.mix uu___6 uu___7) + } +let hashable_tuple6 : + 'a 'b 'c 'd 'e 'f . + 'a hashable -> + 'b hashable -> + 'c hashable -> + 'd hashable -> + 'e hashable -> + 'f hashable -> ('a * 'b * 'c * 'd * 'e * 'f) hashable + = + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + fun uu___3 -> + fun uu___4 -> + fun uu___5 -> + { + hash = + (fun uu___6 -> + match uu___6 with + | (a1, b1, c1, d1, e1, f1) -> + let uu___7 = + let uu___8 = + let uu___9 = + let uu___10 = + let uu___11 = hash uu___ a1 in + let uu___12 = hash uu___1 b1 in + FStar_Hash.mix uu___11 uu___12 in + let uu___11 = hash uu___2 c1 in + FStar_Hash.mix uu___10 uu___11 in + let uu___10 = hash uu___3 d1 in + FStar_Hash.mix uu___9 uu___10 in + let uu___9 = hash uu___4 e1 in + FStar_Hash.mix uu___8 uu___9 in + let uu___8 = hash uu___5 f1 in + FStar_Hash.mix uu___7 uu___8) + } \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml index 893a4080ab5..be20d936f9b 100644 --- a/ocaml/fstar-lib/generated/FStar_Options.ml +++ b/ocaml/fstar-lib/generated/FStar_Options.ml @@ -356,6 +356,7 @@ let (defaults : (Prims.string * option_val) Prims.list) = ("quake_lo", (Int Prims.int_one)); ("quake_hi", (Int Prims.int_one)); ("quake_keep", (Bool false)); + ("query_cache", (Bool false)); ("query_stats", (Bool false)); ("record_hints", (Bool false)); ("record_options", (Bool false)); @@ -612,6 +613,8 @@ let (get_quake_hi : unit -> Prims.int) = fun uu___ -> lookup_opt "quake_hi" as_int let (get_quake_keep : unit -> Prims.bool) = fun uu___ -> lookup_opt "quake_keep" as_bool +let (get_query_cache : unit -> Prims.bool) = + fun uu___ -> lookup_opt "query_cache" as_bool let (get_query_stats : unit -> Prims.bool) = fun uu___ -> lookup_opt "query_stats" as_bool let (get_record_hints : unit -> Prims.bool) = @@ -1005,7 +1008,7 @@ let (interp_quake_arg : Prims.string -> (Prims.int * Prims.int * Prims.bool)) let uu___ = ios f1 in let uu___1 = ios f2 in (uu___, uu___1, true) else FStar_Compiler_Effect.failwith "unexpected value for --quake" | uu___ -> FStar_Compiler_Effect.failwith "unexpected value for --quake" -let (uu___450 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) +let (uu___451 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) = let cb = FStar_Compiler_Util.mk_ref FStar_Pervasives_Native.None in let set1 f = @@ -1017,11 +1020,11 @@ let (uu___450 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) | FStar_Pervasives_Native.Some f -> f msg in (set1, call) let (set_option_warning_callback_aux : (Prims.string -> unit) -> unit) = - match uu___450 with + match uu___451 with | (set_option_warning_callback_aux1, option_warning_callback) -> set_option_warning_callback_aux1 let (option_warning_callback : Prims.string -> unit) = - match uu___450 with + match uu___451 with | (set_option_warning_callback_aux1, option_warning_callback1) -> option_warning_callback1 let (set_option_warning_callback : (Prims.string -> unit) -> unit) = @@ -2199,9 +2202,9 @@ let rec (specs_with_types : let uu___149 = text - "Print SMT query statistics" in + "Keep a running cache of SMT queries to make verification faster. Only available in the interactive mode. NOTE: This feature is experimental and potentially unsound! Hence why\n it is not allowed in batch mode (where it is also less useful). If you\n find a query that is mistakenly accepted with the cache, please\n report a bug to the F* issue tracker on GitHub." in (FStar_Getopt.noshort, - "query_stats", + "query_cache", (Const (Bool true)), @@ -2213,9 +2216,9 @@ let rec (specs_with_types : let uu___151 = text - "Record a database of hints for efficient proof replay" in + "Print SMT query statistics" in (FStar_Getopt.noshort, - "record_hints", + "query_stats", (Const (Bool true)), @@ -2227,9 +2230,9 @@ let rec (specs_with_types : let uu___153 = text - "Record the state of options used to check each sigelt, useful for the `check_with` attribute and metaprogramming. Note that this implies a performance hit and increases the size of checked files." in + "Record a database of hints for efficient proof replay" in (FStar_Getopt.noshort, - "record_options", + "record_hints", (Const (Bool true)), @@ -2241,14 +2244,28 @@ let rec (specs_with_types : let uu___155 = text + "Record the state of options used to check each sigelt, useful for the `check_with` attribute and metaprogramming. Note that this implies a performance hit and increases the size of checked files." in + (FStar_Getopt.noshort, + "record_options", + (Const + (Bool + true)), + uu___155) in + let uu___155 + = + let uu___156 + = + let uu___157 + = + text "Retry each SMT query N times and succeed on the first try. Using --retry disables --quake." in (FStar_Getopt.noshort, "retry", (PostProcessed ((fun - uu___156 + uu___158 -> - match uu___156 + match uu___158 with | Int i -> @@ -2269,18 +2286,18 @@ let rec (specs_with_types : true); Bool true) | - uu___157 + uu___159 -> FStar_Compiler_Effect.failwith "impos"), (IntStr "positive integer"))), - uu___155) in - let uu___155 + uu___157) in + let uu___157 = - let uu___156 + let uu___158 = - let uu___157 + let uu___159 = text "Optimistically, attempt using the recorded hint for toplevel_name (a top-level name in the current module) when trying to verify some other term 'g'" in @@ -2288,12 +2305,12 @@ let rec (specs_with_types : "reuse_hint_for", (SimpleStr "toplevel_name"), - uu___157) in - let uu___157 + uu___159) in + let uu___159 = - let uu___158 + let uu___160 = - let uu___159 + let uu___161 = text "Report every use of an escape hatch, include assume, admit, etc." in @@ -2302,12 +2319,12 @@ let rec (specs_with_types : (EnumStr ["warn"; "error"]), - uu___159) in - let uu___159 + uu___161) in + let uu___161 = - let uu___160 + let uu___162 = - let uu___161 + let uu___163 = text "Disable all non-critical output" in @@ -2316,12 +2333,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___161) in - let uu___161 + uu___163) in + let uu___163 = - let uu___162 + let uu___164 = - let uu___163 + let uu___165 = text "Path to the Z3 SMT solver (we could eventually support other solvers)" in @@ -2329,211 +2346,197 @@ let rec (specs_with_types : "smt", (PathStr "path"), - uu___163) in - let uu___163 + uu___165) in + let uu___165 = - let uu___164 + let uu___166 = - let uu___165 + let uu___167 = text "Toggle a peephole optimization that eliminates redundant uses of boxing/unboxing in the SMT encoding (default 'false')" in (FStar_Getopt.noshort, "smtencoding.elim_box", BoolStr, - uu___165) in - let uu___165 - = - let uu___166 - = + uu___167) in let uu___167 = let uu___168 = - text - "Control the representation of non-linear arithmetic functions in the SMT encoding:" in let uu___169 = let uu___170 = + text + "Control the representation of non-linear arithmetic functions in the SMT encoding:" in let uu___171 = let uu___172 = - text - "if 'boxwrap' use 'Prims.op_Multiply, Prims.op_Division, Prims.op_Modulus'" in let uu___173 = let uu___174 = text - "if 'native' use '*, div, mod'" in + "if 'boxwrap' use 'Prims.op_Multiply, Prims.op_Division, Prims.op_Modulus'" in let uu___175 = let uu___176 = text + "if 'native' use '*, div, mod'" in + let uu___177 + = + let uu___178 + = + text "if 'wrapped' use '_mul, _div, _mod : Int*Int -> Int'" in - [uu___176] in + [uu___178] in + uu___176 + :: + uu___177 in uu___174 :: uu___175 in - uu___172 - :: - uu___173 in FStar_Errors_Msg.bulleted - uu___171 in - let uu___171 + uu___173 in + let uu___173 = text "(default 'boxwrap')" in FStar_Pprint.op_Hat_Hat + uu___172 + uu___173 in + FStar_Pprint.op_Hat_Hat uu___170 uu___171 in - FStar_Pprint.op_Hat_Hat - uu___168 - uu___169 in (FStar_Getopt.noshort, "smtencoding.nl_arith_repr", (EnumStr ["native"; "wrapped"; "boxwrap"]), - uu___167) in - let uu___167 - = - let uu___168 - = + uu___169) in let uu___169 = let uu___170 = - text - "Toggle the representation of linear arithmetic functions in the SMT encoding:" in let uu___171 = let uu___172 = + text + "Toggle the representation of linear arithmetic functions in the SMT encoding:" in let uu___173 = let uu___174 = - text - "if 'boxwrap', use 'Prims.op_Addition, Prims.op_Subtraction, Prims.op_Minus'" in let uu___175 = let uu___176 = text + "if 'boxwrap', use 'Prims.op_Addition, Prims.op_Subtraction, Prims.op_Minus'" in + let uu___177 + = + let uu___178 + = + text "if 'native', use '+, -, -'" in - [uu___176] in - uu___174 + [uu___178] in + uu___176 :: - uu___175 in + uu___177 in FStar_Errors_Msg.bulleted - uu___173 in - let uu___173 + uu___175 in + let uu___175 = text "(default 'boxwrap')" in FStar_Pprint.op_Hat_Hat + uu___174 + uu___175 in + FStar_Pprint.op_Hat_Hat uu___172 uu___173 in - FStar_Pprint.op_Hat_Hat - uu___170 - uu___171 in (FStar_Getopt.noshort, "smtencoding.l_arith_repr", (EnumStr ["native"; "boxwrap"]), - uu___169) in - let uu___169 + uu___171) in + let uu___171 = - let uu___170 + let uu___172 = - let uu___171 + let uu___173 = text "Include an axiom in the SMT encoding to introduce proof-irrelevance from a constructive proof" in (FStar_Getopt.noshort, "smtencoding.valid_intro", BoolStr, - uu___171) in - let uu___171 + uu___173) in + let uu___173 = - let uu___172 + let uu___174 = - let uu___173 + let uu___175 = text "Include an axiom in the SMT encoding to eliminate proof-irrelevance into the existence of a proof witness" in (FStar_Getopt.noshort, "smtencoding.valid_elim", BoolStr, - uu___173) in - let uu___173 - = - let uu___174 - = + uu___175) in let uu___175 = let uu___176 = - text - "Split SMT verification conditions into several separate queries, one per goal. Helps with localizing errors." in let uu___177 = let uu___178 = + text + "Split SMT verification conditions into several separate queries, one per goal. Helps with localizing errors." in let uu___179 = - text - "Use 'no' to disable (this may reduce the quality of error messages)." in let uu___180 = let uu___181 = text - "Use 'on_failure' to split queries and retry when discharging fails (the default)" in + "Use 'no' to disable (this may reduce the quality of error messages)." in let uu___182 = let uu___183 = text + "Use 'on_failure' to split queries and retry when discharging fails (the default)" in + let uu___184 + = + let uu___185 + = + text "Use 'yes' to always split." in - [uu___183] in + [uu___185] in + uu___183 + :: + uu___184 in uu___181 :: uu___182 in - uu___179 - :: - uu___180 in FStar_Errors_Msg.bulleted - uu___178 in + uu___180 in FStar_Pprint.op_Hat_Hat - uu___176 - uu___177 in + uu___178 + uu___179 in (FStar_Getopt.noshort, "split_queries", (EnumStr ["no"; "on_failure"; "always"]), - uu___175) in - let uu___175 - = - let uu___176 - = - let uu___177 - = - text - "Do not use the lexical scope of tactics to improve binder names" in - (FStar_Getopt.noshort, - "tactic_raw_binders", - (Const - (Bool - true)), uu___177) in let uu___177 = @@ -2542,9 +2545,9 @@ let rec (specs_with_types : let uu___179 = text - "Do not recover from metaprogramming errors, and abort if one occurs" in + "Do not use the lexical scope of tactics to improve binder names" in (FStar_Getopt.noshort, - "tactics_failhard", + "tactic_raw_binders", (Const (Bool true)), @@ -2556,9 +2559,9 @@ let rec (specs_with_types : let uu___181 = text - "Print some rough information on tactics, such as the time they take to run" in + "Do not recover from metaprogramming errors, and abort if one occurs" in (FStar_Getopt.noshort, - "tactics_info", + "tactics_failhard", (Const (Bool true)), @@ -2570,9 +2573,9 @@ let rec (specs_with_types : let uu___183 = text - "Print a depth-indexed trace of tactic execution (Warning: very verbose)" in + "Print some rough information on tactics, such as the time they take to run" in (FStar_Getopt.noshort, - "tactic_trace", + "tactics_info", (Const (Bool true)), @@ -2584,11 +2587,12 @@ let rec (specs_with_types : let uu___185 = text - "Trace tactics up to a certain binding depth" in + "Print a depth-indexed trace of tactic execution (Warning: very verbose)" in (FStar_Getopt.noshort, - "tactic_trace_d", - (IntStr - "positive_integer"), + "tactic_trace", + (Const + (Bool + true)), uu___185) in let uu___185 = @@ -2597,12 +2601,11 @@ let rec (specs_with_types : let uu___187 = text - "Use NBE to evaluate metaprograms (experimental)" in + "Trace tactics up to a certain binding depth" in (FStar_Getopt.noshort, - "__tactics_nbe", - (Const - (Bool - true)), + "tactic_trace_d", + (IntStr + "positive_integer"), uu___187) in let uu___187 = @@ -2611,10 +2614,12 @@ let rec (specs_with_types : let uu___189 = text - "Attempt to normalize definitions marked as tcnorm (default 'true')" in + "Use NBE to evaluate metaprograms (experimental)" in (FStar_Getopt.noshort, - "tcnorm", - BoolStr, + "__tactics_nbe", + (Const + (Bool + true)), uu___189) in let uu___189 = @@ -2623,12 +2628,10 @@ let rec (specs_with_types : let uu___191 = text - "Print the time it takes to verify each top-level definition. This is just an alias for an invocation of the profiler, so it may not work well if combined with --profile. In particular, it implies --profile_group_by_decl." in + "Attempt to normalize definitions marked as tcnorm (default 'true')" in (FStar_Getopt.noshort, - "timing", - (Const - (Bool - true)), + "tcnorm", + BoolStr, uu___191) in let uu___191 = @@ -2637,9 +2640,9 @@ let rec (specs_with_types : let uu___193 = text - "Attach stack traces on errors" in + "Print the time it takes to verify each top-level definition. This is just an alias for an invocation of the profiler, so it may not work well if combined with --profile. In particular, it implies --profile_group_by_decl." in (FStar_Getopt.noshort, - "trace_error", + "timing", (Const (Bool true)), @@ -2651,9 +2654,9 @@ let rec (specs_with_types : let uu___195 = text - "Emit output formatted for debugging" in + "Attach stack traces on errors" in (FStar_Getopt.noshort, - "ugly", + "trace_error", (Const (Bool true)), @@ -2665,9 +2668,9 @@ let rec (specs_with_types : let uu___197 = text - "Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)" in + "Emit output formatted for debugging" in (FStar_Getopt.noshort, - "unthrottle_inductives", + "ugly", (Const (Bool true)), @@ -2679,9 +2682,9 @@ let rec (specs_with_types : let uu___199 = text - "Allow tactics to run external processes. WARNING: checking an untrusted F* file while using this option can have disastrous effects." in + "Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)" in (FStar_Getopt.noshort, - "unsafe_tactic_exec", + "unthrottle_inductives", (Const (Bool true)), @@ -2693,9 +2696,9 @@ let rec (specs_with_types : let uu___201 = text - "Use equality constraints when comparing higher-order types (Temporary)" in + "Allow tactics to run external processes. WARNING: checking an untrusted F* file while using this option can have disastrous effects." in (FStar_Getopt.noshort, - "use_eq_at_higher_order", + "unsafe_tactic_exec", (Const (Bool true)), @@ -2707,9 +2710,9 @@ let rec (specs_with_types : let uu___203 = text - "Use a previously recorded hints database for proof replay" in + "Use equality constraints when comparing higher-order types (Temporary)" in (FStar_Getopt.noshort, - "use_hints", + "use_eq_at_higher_order", (Const (Bool true)), @@ -2721,9 +2724,9 @@ let rec (specs_with_types : let uu___205 = text - "Admit queries if their hash matches the hash recorded in the hints database" in + "Use a previously recorded hints database for proof replay" in (FStar_Getopt.noshort, - "use_hint_hashes", + "use_hints", (Const (Bool true)), @@ -2735,11 +2738,12 @@ let rec (specs_with_types : let uu___207 = text - "Use compiled tactics from path" in + "Admit queries if their hash matches the hash recorded in the hints database" in (FStar_Getopt.noshort, - "use_native_tactics", - (PathStr - "path"), + "use_hint_hashes", + (Const + (Bool + true)), uu___207) in let uu___207 = @@ -2748,12 +2752,11 @@ let rec (specs_with_types : let uu___209 = text - "Do not run plugins natively and interpret them as usual instead" in + "Use compiled tactics from path" in (FStar_Getopt.noshort, - "no_plugins", - (Const - (Bool - true)), + "use_native_tactics", + (PathStr + "path"), uu___209) in let uu___209 = @@ -2762,9 +2765,9 @@ let rec (specs_with_types : let uu___211 = text - "Do not run the tactic engine before discharging a VC" in + "Do not run plugins natively and interpret them as usual instead" in (FStar_Getopt.noshort, - "no_tactics", + "no_plugins", (Const (Bool true)), @@ -2776,18 +2779,32 @@ let rec (specs_with_types : let uu___213 = text + "Do not run the tactic engine before discharging a VC" in + (FStar_Getopt.noshort, + "no_tactics", + (Const + (Bool + true)), + uu___213) in + let uu___213 + = + let uu___214 + = + let uu___215 + = + text "Prunes the context to include only the facts from the given namespace or fact id. Facts can be include or excluded using the [+|-] qualifier. For example --using_facts_from '* -FStar.Reflection +FStar.Compiler.List -FStar.Compiler.List.Tot' will remove all facts from FStar.Compiler.List.Tot.*, retain all remaining facts from FStar.Compiler.List.*, remove all facts from FStar.Reflection.*, and retain all the rest. Note, the '+' is optional: --using_facts_from 'FStar.Compiler.List' is equivalent to --using_facts_from '+FStar.Compiler.List'. Multiple uses of this option accumulate, e.g., --using_facts_from A --using_facts_from B is interpreted as --using_facts_from A^B." in (FStar_Getopt.noshort, "using_facts_from", (ReverseAccumulated (SimpleStr "One or more space-separated occurrences of '[+|-]( * | namespace | fact id)'")), - uu___213) in - let uu___213 + uu___215) in + let uu___215 = - let uu___214 + let uu___216 = - let uu___215 + let uu___217 = text "This does nothing and will be removed" in @@ -2796,12 +2813,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___215) in - let uu___215 + uu___217) in + let uu___217 = - let uu___216 + let uu___218 = - let uu___217 + let uu___219 = text "Display version number" in @@ -2809,7 +2826,7 @@ let rec (specs_with_types : "version", (WithSideEffect ((fun - uu___218 + uu___220 -> display_version (); @@ -2818,12 +2835,12 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___217) in - let uu___217 + uu___219) in + let uu___219 = - let uu___218 + let uu___220 = - let uu___219 + let uu___221 = text "Warn when (a -> b) is desugared to (a -> Tot b)" in @@ -2832,12 +2849,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___219) in - let uu___219 + uu___221) in + let uu___221 = - let uu___220 + let uu___222 = - let uu___221 + let uu___223 = text "Z3 command line options" in @@ -2846,12 +2863,12 @@ let rec (specs_with_types : (ReverseAccumulated (SimpleStr "option")), - uu___221) in - let uu___221 + uu___223) in + let uu___223 = - let uu___222 + let uu___224 = - let uu___223 + let uu___225 = text "Z3 options in smt2 format" in @@ -2860,12 +2877,12 @@ let rec (specs_with_types : (ReverseAccumulated (SimpleStr "option")), - uu___223) in - let uu___223 + uu___225) in + let uu___225 = - let uu___224 + let uu___226 = - let uu___225 + let uu___227 = text "Restart Z3 after each query; useful for ensuring proof robustness" in @@ -2874,12 +2891,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___225) in - let uu___225 + uu___227) in + let uu___227 = - let uu___226 + let uu___228 = - let uu___227 + let uu___229 = text "Set the Z3 per-query resource limit (default 5 units, taking roughtly 5s)" in @@ -2887,12 +2904,12 @@ let rec (specs_with_types : "z3rlimit", (IntStr "positive_integer"), - uu___227) in - let uu___227 + uu___229) in + let uu___229 = - let uu___228 + let uu___230 = - let uu___229 + let uu___231 = text "Set the Z3 per-query resource limit multiplier. This is useful when, say, regenerating hints and you want to be more lax. (default 1)" in @@ -2900,12 +2917,12 @@ let rec (specs_with_types : "z3rlimit_factor", (IntStr "positive_integer"), - uu___229) in - let uu___229 + uu___231) in + let uu___231 = - let uu___230 + let uu___232 = - let uu___231 + let uu___233 = text "Set the Z3 random seed (default 0)" in @@ -2913,12 +2930,12 @@ let rec (specs_with_types : "z3seed", (IntStr "positive_integer"), - uu___231) in - let uu___231 + uu___233) in + let uu___233 = - let uu___232 + let uu___234 = - let uu___233 + let uu___235 = text "Set the version of Z3 that is to be used. Default: 4.8.5" in @@ -2926,12 +2943,12 @@ let rec (specs_with_types : "z3version", (SimpleStr "version"), - uu___233) in - let uu___233 + uu___235) in + let uu___235 = - let uu___234 + let uu___236 = - let uu___235 + let uu___237 = text "Don't check positivity of inductive types" in @@ -2939,7 +2956,7 @@ let rec (specs_with_types : "__no_positivity", (WithSideEffect ((fun - uu___236 + uu___238 -> if warn_unsafe @@ -2950,75 +2967,63 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___235) in - let uu___235 - = - let uu___236 - = + uu___237) in let uu___237 = let uu___238 = - text - "The [-warn_error] option follows the OCaml syntax, namely:" in let uu___239 = let uu___240 = + text + "The [-warn_error] option follows the OCaml syntax, namely:" in let uu___241 = - text - "[r] is a range of warnings (either a number [n], or a range [n..n])" in let uu___242 = let uu___243 = text - "[-r] silences range [r]" in + "[r] is a range of warnings (either a number [n], or a range [n..n])" in let uu___244 = let uu___245 = text - "[+r] enables range [r] as warnings (NOTE: \"enabling\" an error will downgrade it to a warning)" in + "[-r] silences range [r]" in let uu___246 = let uu___247 = text + "[+r] enables range [r] as warnings (NOTE: \"enabling\" an error will downgrade it to a warning)" in + let uu___248 + = + let uu___249 + = + text "[@r] makes range [r] fatal." in - [uu___247] in + [uu___249] in + uu___247 + :: + uu___248 in uu___245 :: uu___246 in uu___243 :: uu___244 in - uu___241 - :: - uu___242 in FStar_Errors_Msg.bulleted - uu___240 in + uu___242 in FStar_Pprint.op_Hat_Hat - uu___238 - uu___239 in + uu___240 + uu___241 in (FStar_Getopt.noshort, "warn_error", (ReverseAccumulated (SimpleStr "")), - uu___237) in - let uu___237 - = - let uu___238 - = - let uu___239 - = - text - "Use normalization by evaluation as the default normalization strategy (default 'false')" in - (FStar_Getopt.noshort, - "use_nbe", - BoolStr, uu___239) in let uu___239 = @@ -3027,9 +3032,9 @@ let rec (specs_with_types : let uu___241 = text - "Use normalization by evaluation for normalizing terms before extraction (default 'false')" in + "Use normalization by evaluation as the default normalization strategy (default 'false')" in (FStar_Getopt.noshort, - "use_nbe_for_extraction", + "use_nbe", BoolStr, uu___241) in let uu___241 @@ -3039,9 +3044,9 @@ let rec (specs_with_types : let uu___243 = text - "Enforce trivial preconditions for unannotated effectful functions (default 'true')" in + "Use normalization by evaluation for normalizing terms before extraction (default 'false')" in (FStar_Getopt.noshort, - "trivial_pre_for_unannotated_effectful_fns", + "use_nbe_for_extraction", BoolStr, uu___243) in let uu___243 @@ -3051,12 +3056,24 @@ let rec (specs_with_types : let uu___245 = text + "Enforce trivial preconditions for unannotated effectful functions (default 'true')" in + (FStar_Getopt.noshort, + "trivial_pre_for_unannotated_effectful_fns", + BoolStr, + uu___245) in + let uu___245 + = + let uu___246 + = + let uu___247 + = + text "Debug messages for embeddings/unembeddings of natively compiled terms" in (FStar_Getopt.noshort, "__debug_embedding", (WithSideEffect ((fun - uu___246 + uu___248 -> FStar_Compiler_Effect.op_Colon_Equals debug_embedding @@ -3064,12 +3081,12 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___245) in - let uu___245 + uu___247) in + let uu___247 = - let uu___246 + let uu___248 = - let uu___247 + let uu___249 = text "Eagerly embed and unembed terms to primitive operations and plugins: not recommended except for benchmarking" in @@ -3077,7 +3094,7 @@ let rec (specs_with_types : "eager_embedding", (WithSideEffect ((fun - uu___248 + uu___250 -> FStar_Compiler_Effect.op_Colon_Equals eager_embedding @@ -3085,12 +3102,12 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___247) in - let uu___247 + uu___249) in + let uu___249 = - let uu___248 + let uu___250 = - let uu___249 + let uu___251 = text "Emit profiles grouped by declaration rather than by module" in @@ -3099,12 +3116,12 @@ let rec (specs_with_types : (Const (Bool true)), - uu___249) in - let uu___249 + uu___251) in + let uu___251 = - let uu___250 + let uu___252 = - let uu___251 + let uu___253 = text "Specific source locations in the compiler are instrumented with profiling counters. Pass `--profile_component FStar.TypeChecker` to enable all counters in the FStar.TypeChecker namespace. This option is a module or namespace selector, like many other options (e.g., `--extract`)" in @@ -3113,12 +3130,12 @@ let rec (specs_with_types : (Accumulated (SimpleStr "One or more space-separated occurrences of '[+|-]( * | namespace | module | identifier)'")), - uu___251) in - let uu___251 + uu___253) in + let uu___253 = - let uu___252 + let uu___254 = - let uu___253 + let uu___255 = text "Profiling can be enabled when the compiler is processing a given set of source modules. Pass `--profile FStar.Pervasives` to enable profiling when the compiler is processing any module in FStar.Pervasives. This option is a module or namespace selector, like many other options (e.g., `--extract`)" in @@ -3127,12 +3144,12 @@ let rec (specs_with_types : (Accumulated (SimpleStr "One or more space-separated occurrences of '[+|-]( * | namespace | module)'")), - uu___253) in - let uu___253 + uu___255) in + let uu___255 = - let uu___254 + let uu___256 = - let uu___255 + let uu___257 = text "Display this information" in @@ -3140,26 +3157,26 @@ let rec (specs_with_types : "help", (WithSideEffect ((fun - uu___256 + uu___258 -> ( - let uu___258 + let uu___260 = specs warn_unsafe in display_usage_aux - uu___258); + uu___260); FStar_Compiler_Effect.exit Prims.int_zero), (Const (Bool true)))), - uu___255) in - let uu___255 + uu___257) in + let uu___257 = - let uu___256 + let uu___258 = - let uu___257 + let uu___259 = text "List all debug keys and exit" in @@ -3167,7 +3184,7 @@ let rec (specs_with_types : "list_debug_keys", (WithSideEffect ((fun - uu___258 + uu___260 -> display_debug_keys (); @@ -3176,8 +3193,11 @@ let rec (specs_with_types : (Const (Bool true)))), - uu___257) in - [uu___256] in + uu___259) in + [uu___258] in + uu___256 + :: + uu___257 in uu___254 :: uu___255 in @@ -3570,6 +3590,7 @@ let (settable : Prims.string -> Prims.bool) = | "quake_hi" -> true | "quake_keep" -> true | "quake" -> true + | "query_cache" -> true | "query_stats" -> true | "record_options" -> true | "retry" -> true @@ -3624,7 +3645,7 @@ let (settable_specs : (fun uu___ -> match uu___ with | ((uu___1, x, uu___2), uu___3) -> settable x) all_specs -let (uu___658 : +let (uu___660 : (((unit -> FStar_Getopt.parse_cmdline_res) -> unit) * (unit -> FStar_Getopt.parse_cmdline_res))) = @@ -3641,11 +3662,11 @@ let (uu___658 : (set1, call) let (set_error_flags_callback_aux : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = - match uu___658 with + match uu___660 with | (set_error_flags_callback_aux1, set_error_flags) -> set_error_flags_callback_aux1 let (set_error_flags : unit -> FStar_Getopt.parse_cmdline_res) = - match uu___658 with + match uu___660 with | (set_error_flags_callback_aux1, set_error_flags1) -> set_error_flags1 let (set_error_flags_callback : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = @@ -4124,6 +4145,7 @@ let (proof_recovery : unit -> Prims.bool) = let (quake_lo : unit -> Prims.int) = fun uu___ -> get_quake_lo () let (quake_hi : unit -> Prims.int) = fun uu___ -> get_quake_hi () let (quake_keep : unit -> Prims.bool) = fun uu___ -> get_quake_keep () +let (query_cache : unit -> Prims.bool) = fun uu___ -> get_query_cache () let (query_stats : unit -> Prims.bool) = fun uu___ -> get_query_stats () let (record_hints : unit -> Prims.bool) = fun uu___ -> get_record_hints () let (record_options : unit -> Prims.bool) = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml index 63d6b0b01d9..81f6b4ec233 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml @@ -1243,7 +1243,7 @@ let (full_query_id : query_settings -> Prims.string) = Prims.strcat ", " uu___2 in Prims.strcat settings.query_name uu___1 in Prims.strcat "(" uu___ -let collect : 'a . 'a Prims.list -> ('a * Prims.int) Prims.list = +let collect_dups : 'a . 'a Prims.list -> ('a * Prims.int) Prims.list = fun l -> let acc = [] in let rec add_one acc1 x = @@ -1257,84 +1257,92 @@ let collect : 'a . 'a Prims.list -> ('a * Prims.int) Prims.list = type answer = { ok: Prims.bool ; - nsuccess: Prims.int ; - lo: Prims.int ; - hi: Prims.int ; - errs: errors Prims.list Prims.list ; + cache_hit: Prims.bool ; quaking: Prims.bool ; quaking_or_retrying: Prims.bool ; + lo: Prims.int ; + hi: Prims.int ; + nsuccess: Prims.int ; total_ran: Prims.int ; - tried_recovery: Prims.bool } + tried_recovery: Prims.bool ; + errs: errors Prims.list Prims.list } let (__proj__Mkanswer__item__ok : answer -> Prims.bool) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> ok -let (__proj__Mkanswer__item__nsuccess : answer -> Prims.int) = + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> ok +let (__proj__Mkanswer__item__cache_hit : answer -> Prims.bool) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> nsuccess -let (__proj__Mkanswer__item__lo : answer -> Prims.int) = + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> cache_hit +let (__proj__Mkanswer__item__quaking : answer -> Prims.bool) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> lo -let (__proj__Mkanswer__item__hi : answer -> Prims.int) = + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> quaking +let (__proj__Mkanswer__item__quaking_or_retrying : answer -> Prims.bool) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> hi -let (__proj__Mkanswer__item__errs : answer -> errors Prims.list Prims.list) = + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> quaking_or_retrying +let (__proj__Mkanswer__item__lo : answer -> Prims.int) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> errs -let (__proj__Mkanswer__item__quaking : answer -> Prims.bool) = + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> lo +let (__proj__Mkanswer__item__hi : answer -> Prims.int) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> quaking -let (__proj__Mkanswer__item__quaking_or_retrying : answer -> Prims.bool) = + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> hi +let (__proj__Mkanswer__item__nsuccess : answer -> Prims.int) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> quaking_or_retrying + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> nsuccess let (__proj__Mkanswer__item__total_ran : answer -> Prims.int) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> total_ran + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> total_ran let (__proj__Mkanswer__item__tried_recovery : answer -> Prims.bool) = fun projectee -> match projectee with - | { ok; nsuccess; lo; hi; errs; quaking; quaking_or_retrying; total_ran; - tried_recovery;_} -> tried_recovery + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> tried_recovery +let (__proj__Mkanswer__item__errs : answer -> errors Prims.list Prims.list) = + fun projectee -> + match projectee with + | { ok; cache_hit; quaking; quaking_or_retrying; lo; hi; nsuccess; + total_ran; tried_recovery; errs;_} -> errs let (ans_ok : answer) = { ok = true; - nsuccess = Prims.int_one; - lo = Prims.int_one; - hi = Prims.int_one; - errs = []; + cache_hit = false; quaking = false; quaking_or_retrying = false; + lo = Prims.int_one; + hi = Prims.int_one; + nsuccess = Prims.int_one; total_ran = Prims.int_one; - tried_recovery = false + tried_recovery = false; + errs = [] } let (ans_fail : answer) = { ok = false; - nsuccess = Prims.int_zero; - lo = (ans_ok.lo); - hi = (ans_ok.hi); - errs = (ans_ok.errs); + cache_hit = (ans_ok.cache_hit); quaking = (ans_ok.quaking); quaking_or_retrying = (ans_ok.quaking_or_retrying); + lo = (ans_ok.lo); + hi = (ans_ok.hi); + nsuccess = Prims.int_zero; total_ran = (ans_ok.total_ran); - tried_recovery = (ans_ok.tried_recovery) + tried_recovery = (ans_ok.tried_recovery); + errs = (ans_ok.errs) } -let (uu___548 : answer FStar_Class_Show.showable) = +let (uu___552 : answer FStar_Class_Show.showable) = { FStar_Class_Show.show = (fun ans -> @@ -1741,14 +1749,15 @@ let (ask_solver_quake : query_settings Prims.list -> answer) = | FStar_Pervasives.Inl es -> [es]) rs in { ok = (nsuccess >= lo1); - nsuccess; - lo = lo1; - hi = hi1; - errs = all_errs; + cache_hit = false; quaking; quaking_or_retrying; + lo = lo1; + hi = hi1; + nsuccess; total_ran; - tried_recovery = false + tried_recovery = false; + errs = all_errs })) type recovery_hammer = | IncreaseRLimit of Prims.int @@ -1840,14 +1849,15 @@ let (ask_solver_recover : query_settings Prims.list -> answer) = | [] -> { ok = (r.ok); - nsuccess = (r.nsuccess); - lo = (r.lo); - hi = (r.hi); - errs = (r.errs); + cache_hit = (r.cache_hit); quaking = (r.quaking); quaking_or_retrying = (r.quaking_or_retrying); + lo = (r.lo); + hi = (r.hi); + nsuccess = (r.nsuccess); total_ran = (r.total_ran); - tried_recovery = true + tried_recovery = true; + errs = (r.errs) } | h::hs -> let r1 = try_hammer h in @@ -2030,7 +2040,7 @@ let (report : FStar_TypeChecker_Env.env -> query_settings -> answer -> unit) query_term = (default_settings.query_term) } in let errs = FStar_Compiler_List.map errors_to_report1 all_errs in - let errs1 = collect (FStar_Compiler_List.flatten errs) in + let errs1 = collect_dups (FStar_Compiler_List.flatten errs) in let errs2 = FStar_Compiler_List.map (fun uu___1 -> @@ -2204,77 +2214,107 @@ let (encode_and_ask : fun use_env_msg -> fun tcenv -> fun q -> - maybe_refresh_solver tcenv; - (let uu___2 = - let uu___3 = - let uu___4 = FStar_TypeChecker_Env.get_range tcenv in - FStar_Compiler_Range_Ops.string_of_range uu___4 in - FStar_Compiler_Util.format1 "Starting query at %s" uu___3 in - FStar_SMTEncoding_Encode.push uu___2); - (let pop uu___2 = - let uu___3 = + let do1 uu___ = + maybe_refresh_solver tcenv; + (let uu___3 = let uu___4 = let uu___5 = FStar_TypeChecker_Env.get_range tcenv in FStar_Compiler_Range_Ops.string_of_range uu___5 in - FStar_Compiler_Util.format1 "Ending query at %s" uu___4 in - FStar_SMTEncoding_Encode.pop uu___3 in - finally pop - (fun uu___2 -> - let uu___3 = - FStar_SMTEncoding_Encode.encode_query use_env_msg tcenv q in - match uu___3 with - | (prefix, labels, qry, suffix) -> - let tcenv1 = - FStar_TypeChecker_Env.incr_query_index tcenv in - (match qry with - | FStar_SMTEncoding_Term.Assume - { - FStar_SMTEncoding_Term.assumption_term = - { - FStar_SMTEncoding_Term.tm = - FStar_SMTEncoding_Term.App - (FStar_SMTEncoding_Term.FalseOp, uu___4); - FStar_SMTEncoding_Term.freevars = uu___5; - FStar_SMTEncoding_Term.rng = uu___6;_}; - FStar_SMTEncoding_Term.assumption_caption = - uu___7; - FStar_SMTEncoding_Term.assumption_name = uu___8; - FStar_SMTEncoding_Term.assumption_fact_ids = - uu___9;_} - -> ([], ans_ok) - | uu___4 when tcenv1.FStar_TypeChecker_Env.admit -> - ([], ans_ok) - | FStar_SMTEncoding_Term.Assume uu___4 -> - ((let uu___6 = - (is_retry || - (let uu___7 = - FStar_Options.split_queries () in - uu___7 = FStar_Options.Always)) - && (FStar_Compiler_Debug.any ()) in - if uu___6 - then - let n = FStar_Compiler_List.length labels in - (if n <> Prims.int_one - then - let uu___7 = - FStar_TypeChecker_Env.get_range tcenv1 in - let uu___8 = + FStar_Compiler_Util.format1 "Starting query at %s" uu___4 in + FStar_SMTEncoding_Encode.push uu___3); + (let pop uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = FStar_TypeChecker_Env.get_range tcenv in + FStar_Compiler_Range_Ops.string_of_range uu___6 in + FStar_Compiler_Util.format1 "Ending query at %s" uu___5 in + FStar_SMTEncoding_Encode.pop uu___4 in + finally pop + (fun uu___3 -> + let uu___4 = + FStar_SMTEncoding_Encode.encode_query use_env_msg tcenv + q in + match uu___4 with + | (prefix, labels, qry, suffix) -> + let tcenv1 = + FStar_TypeChecker_Env.incr_query_index tcenv in + (match qry with + | FStar_SMTEncoding_Term.Assume + { + FStar_SMTEncoding_Term.assumption_term = + { + FStar_SMTEncoding_Term.tm = + FStar_SMTEncoding_Term.App + (FStar_SMTEncoding_Term.FalseOp, uu___5); + FStar_SMTEncoding_Term.freevars = uu___6; + FStar_SMTEncoding_Term.rng = uu___7;_}; + FStar_SMTEncoding_Term.assumption_caption = + uu___8; + FStar_SMTEncoding_Term.assumption_name = + uu___9; + FStar_SMTEncoding_Term.assumption_fact_ids = + uu___10;_} + -> ([], ans_ok) + | uu___5 when tcenv1.FStar_TypeChecker_Env.admit -> + ([], ans_ok) + | FStar_SMTEncoding_Term.Assume uu___5 -> + ((let uu___7 = + (is_retry || + (let uu___8 = + FStar_Options.split_queries () in + uu___8 = FStar_Options.Always)) + && (FStar_Compiler_Debug.any ()) in + if uu___7 + then + let n = FStar_Compiler_List.length labels in + (if n <> Prims.int_one + then + let uu___8 = + FStar_TypeChecker_Env.get_range tcenv1 in let uu___9 = - FStar_Syntax_Print.term_to_string q in - let uu___10 = - FStar_SMTEncoding_Term.declToSmt "" qry in - let uu___11 = - FStar_Compiler_Util.string_of_int n in - FStar_Compiler_Util.format3 - "Encoded split query %s\nto %s\nwith %s labels" - uu___9 uu___10 uu___11 in - FStar_Errors.diag uu___7 uu___8 - else ()) - else ()); - ask_solver can_split is_retry tcenv1 labels - prefix qry q suffix) - | uu___4 -> - FStar_Compiler_Effect.failwith "Impossible"))) + let uu___10 = + FStar_Syntax_Print.term_to_string q in + let uu___11 = + FStar_SMTEncoding_Term.declToSmt "" + qry in + let uu___12 = + FStar_Compiler_Util.string_of_int n in + FStar_Compiler_Util.format3 + "Encoded split query %s\nto %s\nwith %s labels" + uu___10 uu___11 uu___12 in + FStar_Errors.diag uu___8 uu___9 + else ()) + else ()); + ask_solver can_split is_retry tcenv1 labels + prefix qry q suffix) + | uu___5 -> + FStar_Compiler_Effect.failwith "Impossible"))) in + let uu___ = + FStar_SMTEncoding_Solver_Cache.try_find_query_cache tcenv q in + if uu___ + then + ([], + { + ok = (ans_ok.ok); + cache_hit = true; + quaking = (ans_ok.quaking); + quaking_or_retrying = (ans_ok.quaking_or_retrying); + lo = (ans_ok.lo); + hi = (ans_ok.hi); + nsuccess = (ans_ok.nsuccess); + total_ran = (ans_ok.total_ran); + tried_recovery = (ans_ok.tried_recovery); + errs = (ans_ok.errs) + }) + else + (let uu___2 = do1 () in + match uu___2 with + | (cfgs, ans) -> + (if ans.ok + then + FStar_SMTEncoding_Solver_Cache.query_cache_add tcenv q + else (); + (cfgs, ans))) let (do_solve : Prims.bool -> Prims.bool -> diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver_Cache.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver_Cache.ml new file mode 100644 index 00000000000..adfdce1ae3e --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver_Cache.ml @@ -0,0 +1,384 @@ +open Prims +let (hashable_lident : FStar_Ident.lident FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun l -> + let uu___ = FStar_Class_Show.show FStar_Ident.showable_lident l in + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_string uu___) + } +let (hashable_ident : FStar_Ident.ident FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun i -> + let uu___ = FStar_Class_Show.show FStar_Ident.showable_ident i in + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_string uu___) + } +let (hashable_binding : + FStar_Syntax_Syntax.binding FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun uu___ -> + match uu___ with + | FStar_Syntax_Syntax.Binding_var bv -> + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term + bv.FStar_Syntax_Syntax.sort + | FStar_Syntax_Syntax.Binding_lid (l, (us, t)) -> + let uu___1 = + let uu___2 = FStar_Class_Hashable.hash hashable_lident l in + let uu___3 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_ident) us in + FStar_Hash.mix uu___2 uu___3 in + let uu___2 = + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term t in + FStar_Hash.mix uu___1 uu___2 + | FStar_Syntax_Syntax.Binding_univ u -> + FStar_Class_Hashable.hash hashable_ident u) + } +let (hashable_bv : FStar_Syntax_Syntax.bv FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun b -> + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term + b.FStar_Syntax_Syntax.sort) + } +let (hashable_fv : FStar_Syntax_Syntax.fv FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun f -> + FStar_Class_Hashable.hash hashable_lident + (f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v) + } +let (hashable_binder : + FStar_Syntax_Syntax.binder FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun b -> + FStar_Class_Hashable.hash hashable_bv + b.FStar_Syntax_Syntax.binder_bv) + } +let (hashable_letbinding : + FStar_Syntax_Syntax.letbinding FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun lb -> + let uu___ = + let uu___1 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_either hashable_bv hashable_fv) + lb.FStar_Syntax_Syntax.lbname in + let uu___2 = + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term + lb.FStar_Syntax_Syntax.lbtyp in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term + lb.FStar_Syntax_Syntax.lbdef in + FStar_Hash.mix uu___ uu___1) + } +let (hashable_pragma : + FStar_Syntax_Syntax.pragma FStar_Class_Hashable.hashable) = + { + FStar_Class_Hashable.hash = + (fun uu___ -> + match uu___ with + | FStar_Syntax_Syntax.SetOptions s -> + let uu___1 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + Prims.int_one in + let uu___2 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_string + s in + FStar_Hash.mix uu___1 uu___2 + | FStar_Syntax_Syntax.ResetOptions s -> + let uu___1 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (2)) in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_option + FStar_Class_Hashable.hashable_string) s in + FStar_Hash.mix uu___1 uu___2 + | FStar_Syntax_Syntax.PushOptions s -> + let uu___1 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (3)) in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_option + FStar_Class_Hashable.hashable_string) s in + FStar_Hash.mix uu___1 uu___2 + | FStar_Syntax_Syntax.PopOptions -> + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (4)) + | FStar_Syntax_Syntax.RestartSolver -> + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (5)) + | FStar_Syntax_Syntax.PrintEffectsGraph -> + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (6))) + } +let rec (hash_sigelt : FStar_Syntax_Syntax.sigelt -> FStar_Hash.hash_code) = + fun se -> hash_sigelt' se.FStar_Syntax_Syntax.sigel +and (hash_sigelt' : FStar_Syntax_Syntax.sigelt' -> FStar_Hash.hash_code) = + fun se -> + match se with + | FStar_Syntax_Syntax.Sig_inductive_typ + { FStar_Syntax_Syntax.lid = lid; FStar_Syntax_Syntax.us = us; + FStar_Syntax_Syntax.params = params; + FStar_Syntax_Syntax.num_uniform_params = num_uniform_params; + FStar_Syntax_Syntax.t = t; FStar_Syntax_Syntax.mutuals = mutuals; + FStar_Syntax_Syntax.ds = ds; + FStar_Syntax_Syntax.injective_type_params = injective_type_params;_} + -> + let uu___ = + let uu___1 = + let uu___2 = + let uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = + FStar_Class_Hashable.hash + FStar_Class_Hashable.hashable_int Prims.int_zero in + let uu___8 = + FStar_Class_Hashable.hash hashable_lident lid in + FStar_Hash.mix uu___7 uu___8 in + let uu___7 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_ident) + us in + FStar_Hash.mix uu___6 uu___7 in + let uu___6 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_binder) + params in + FStar_Hash.mix uu___5 uu___6 in + let uu___5 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_option + FStar_Class_Hashable.hashable_int) num_uniform_params in + FStar_Hash.mix uu___4 uu___5 in + let uu___4 = + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term t in + FStar_Hash.mix uu___3 uu___4 in + let uu___3 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_lident) mutuals in + FStar_Hash.mix uu___2 uu___3 in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_lident) ds in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_bool + injective_type_params in + FStar_Hash.mix uu___ uu___1 + | FStar_Syntax_Syntax.Sig_bundle + { FStar_Syntax_Syntax.ses = ses; FStar_Syntax_Syntax.lids = lids;_} + -> + let uu___ = + let uu___1 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + Prims.int_one in + let uu___2 = + (FStar_Class_Hashable.hashable_list + { FStar_Class_Hashable.hash = hash_sigelt }).FStar_Class_Hashable.hash + ses in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_lident) lids in + FStar_Hash.mix uu___ uu___1 + | FStar_Syntax_Syntax.Sig_datacon + { FStar_Syntax_Syntax.lid1 = lid; FStar_Syntax_Syntax.us1 = us; + FStar_Syntax_Syntax.t1 = t; FStar_Syntax_Syntax.ty_lid = ty_lid; + FStar_Syntax_Syntax.num_ty_params = num_ty_params; + FStar_Syntax_Syntax.mutuals1 = mutuals; + FStar_Syntax_Syntax.injective_type_params1 = injective_type_params;_} + -> + let uu___ = + let uu___1 = + let uu___2 = + let uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = + FStar_Class_Hashable.hash + FStar_Class_Hashable.hashable_int (Prims.of_int (2)) in + let uu___7 = + FStar_Class_Hashable.hash hashable_lident lid in + FStar_Hash.mix uu___6 uu___7 in + let uu___6 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_ident) us in + FStar_Hash.mix uu___5 uu___6 in + let uu___5 = + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term t in + FStar_Hash.mix uu___4 uu___5 in + let uu___4 = FStar_Class_Hashable.hash hashable_lident ty_lid in + FStar_Hash.mix uu___3 uu___4 in + let uu___3 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + num_ty_params in + FStar_Hash.mix uu___2 uu___3 in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_lident) mutuals in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_bool + injective_type_params in + FStar_Hash.mix uu___ uu___1 + | FStar_Syntax_Syntax.Sig_declare_typ + { FStar_Syntax_Syntax.lid2 = lid; FStar_Syntax_Syntax.us2 = us; + FStar_Syntax_Syntax.t2 = t;_} + -> + let uu___ = + let uu___1 = + let uu___2 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (3)) in + let uu___3 = FStar_Class_Hashable.hash hashable_lident lid in + FStar_Hash.mix uu___2 uu___3 in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_ident) us in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term t in + FStar_Hash.mix uu___ uu___1 + | FStar_Syntax_Syntax.Sig_let + { FStar_Syntax_Syntax.lbs1 = lbs; FStar_Syntax_Syntax.lids1 = lids;_} + -> + let uu___ = + let uu___1 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (4)) in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_tuple2 + FStar_Class_Hashable.hashable_bool + (FStar_Class_Hashable.hashable_list hashable_letbinding)) + lbs in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_lident) lids in + FStar_Hash.mix uu___ uu___1 + | FStar_Syntax_Syntax.Sig_assume + { FStar_Syntax_Syntax.lid3 = lid; FStar_Syntax_Syntax.us3 = us; + FStar_Syntax_Syntax.phi1 = phi;_} + -> + let uu___ = + let uu___1 = + let uu___2 = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (5)) in + let uu___3 = FStar_Class_Hashable.hash hashable_lident lid in + FStar_Hash.mix uu___2 uu___3 in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_ident) us in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash FStar_Syntax_Hash.hashable_term phi in + FStar_Hash.mix uu___ uu___1 + | FStar_Syntax_Syntax.Sig_pragma p -> + let uu___ = + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + (Prims.of_int (6)) in + let uu___1 = FStar_Class_Hashable.hash hashable_pragma p in + FStar_Hash.mix uu___ uu___1 + | uu___ -> + FStar_Class_Hashable.hash FStar_Class_Hashable.hashable_int + Prims.int_zero +let (hashable_sigelt : + FStar_Syntax_Syntax.sigelt FStar_Class_Hashable.hashable) = + { FStar_Class_Hashable.hash = hash_sigelt } +let (hashable_env : FStar_TypeChecker_Env.env FStar_Class_Hashable.hashable) + = + { + FStar_Class_Hashable.hash = + (fun e -> + let uu___ = + let uu___1 = + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list hashable_binding) + e.FStar_TypeChecker_Env.gamma in + let uu___3 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list + (FStar_Class_Hashable.hashable_tuple2 + (FStar_Class_Hashable.hashable_list hashable_lident) + hashable_sigelt)) e.FStar_TypeChecker_Env.gamma_sig in + FStar_Hash.mix uu___2 uu___3 in + let uu___2 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_list + (FStar_Class_Hashable.hashable_tuple2 + (FStar_Class_Hashable.hashable_list + FStar_Class_Hashable.hashable_string) + FStar_Class_Hashable.hashable_bool)) + e.FStar_TypeChecker_Env.proof_ns in + FStar_Hash.mix uu___1 uu___2 in + let uu___1 = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_tuple2 + FStar_Class_Hashable.hashable_bool + FStar_Class_Hashable.hashable_bool) + ((e.FStar_TypeChecker_Env.admit), (e.FStar_TypeChecker_Env.lax)) in + FStar_Hash.mix uu___ uu___1) + } +let (query_cache_ref : + FStar_Hash.hash_code FStar_Compiler_RBSet.t FStar_Compiler_Effect.ref) = + let uu___ = + Obj.magic + (FStar_Class_Setlike.empty () + (Obj.magic + (FStar_Compiler_RBSet.setlike_rbset + FStar_Class_Hashable.ord_hash_code)) ()) in + FStar_Compiler_Util.mk_ref uu___ +let (on : unit -> Prims.bool) = + fun uu___ -> (FStar_Options.query_cache ()) && (FStar_Options.ide ()) +let (query_cache_add : + FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> unit) = + fun g -> + fun q -> + let uu___ = on () in + if uu___ + then + let h = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_tuple2 hashable_env + FStar_Syntax_Hash.hashable_term) (g, q) in + let uu___1 = + let uu___2 = FStar_Compiler_Effect.op_Bang query_cache_ref in + Obj.magic + (FStar_Class_Setlike.add () + (Obj.magic + (FStar_Compiler_RBSet.setlike_rbset + FStar_Class_Hashable.ord_hash_code)) h + (Obj.magic uu___2)) in + FStar_Compiler_Effect.op_Colon_Equals query_cache_ref uu___1 + else () +let (try_find_query_cache : + FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> Prims.bool) = + fun g -> + fun q -> + let uu___ = on () in + if uu___ + then + let h = + FStar_Class_Hashable.hash + (FStar_Class_Hashable.hashable_tuple2 hashable_env + FStar_Syntax_Hash.hashable_term) (g, q) in + let r = + let uu___1 = FStar_Compiler_Effect.op_Bang query_cache_ref in + FStar_Class_Setlike.mem () + (Obj.magic + (FStar_Compiler_RBSet.setlike_rbset + FStar_Class_Hashable.ord_hash_code)) h (Obj.magic uu___1) in + r + else false \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Hash.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Hash.ml index 70fca371d54..5218ed71979 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Hash.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Hash.ml @@ -1247,4 +1247,6 @@ and (equal_subst_elt : | (FStar_Syntax_Syntax.UN (i1, u1), FStar_Syntax_Syntax.UN (i2, u2)) -> (i1 = i2) && (equal_universe u1 u2) | (FStar_Syntax_Syntax.UD (un1, i1), FStar_Syntax_Syntax.UD (un2, i2)) - -> (i1 = i2) && (FStar_Ident.ident_equals un1 un2) \ No newline at end of file + -> (i1 = i2) && (FStar_Ident.ident_equals un1 un2) +let (hashable_term : FStar_Syntax_Syntax.term FStar_Class_Hashable.hashable) + = { FStar_Class_Hashable.hash = ext_hash_term } \ No newline at end of file diff --git a/src/basic/FStar.Hash.fsti b/src/basic/FStar.Hash.fsti index 2971ee485c1..fc019906319 100644 --- a/src/basic/FStar.Hash.fsti +++ b/src/basic/FStar.Hash.fsti @@ -3,6 +3,8 @@ open FStar.Compiler.Effect type hash_code +val cmp_hash (_ _ : hash_code) : int + val of_int : int -> hash_code val of_string : string -> hash_code val mix : hash_code -> hash_code -> hash_code diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst index 611b444d666..2dca9b858d6 100644 --- a/src/basic/FStar.Options.fst +++ b/src/basic/FStar.Options.fst @@ -235,6 +235,7 @@ let defaults = ("quake_lo" , Int 1); ("quake_hi" , Int 1); ("quake_keep" , Bool false); + ("query_cache" , Bool false); ("query_stats" , Bool false); ("record_hints" , Bool false); ("record_options" , Bool false); @@ -420,6 +421,7 @@ let get_proof_recovery () = lookup_opt "proof_recovery" let get_quake_lo () = lookup_opt "quake_lo" as_int let get_quake_hi () = lookup_opt "quake_hi" as_int let get_quake_keep () = lookup_opt "quake_keep" as_bool +let get_query_cache () = lookup_opt "query_cache" as_bool let get_query_stats () = lookup_opt "query_stats" as_bool let get_record_hints () = lookup_opt "record_hints" as_bool let get_record_options () = lookup_opt "record_options" as_bool @@ -1127,6 +1129,16 @@ let rec specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.d text "Using --quake disables --retry. When quake testing, queries are not splitted for error reporting unless \ '--split_queries always' is given. Queries from the smt_sync tactic are not quake-tested."); + ( noshort, + "query_cache", + Const (Bool true), + text "Keep a running cache of SMT queries to make verification faster. \ + Only available in the interactive mode. \ + NOTE: This feature is experimental and potentially unsound! Hence why + it is not allowed in batch mode (where it is also less useful). If you + find a query that is mistakenly accepted with the cache, please + report a bug to the F* issue tracker on GitHub."); + ( noshort, "query_stats", Const (Bool true), @@ -1516,6 +1528,7 @@ let settable = function | "quake_hi" | "quake_keep" | "quake" + | "query_cache" | "query_stats" | "record_options" | "retry" @@ -1904,6 +1917,7 @@ let proof_recovery () = get_proof_recovery () let quake_lo () = get_quake_lo () let quake_hi () = get_quake_hi () let quake_keep () = get_quake_keep () +let query_cache () = get_query_cache () let query_stats () = get_query_stats () let record_hints () = get_record_hints () let record_options () = get_record_options () diff --git a/src/basic/FStar.Options.fsti b/src/basic/FStar.Options.fsti index 84a0cce7415..0ed2c7ce92c 100644 --- a/src/basic/FStar.Options.fsti +++ b/src/basic/FStar.Options.fsti @@ -180,6 +180,7 @@ val proof_recovery : unit -> bool val quake_lo : unit -> int val quake_hi : unit -> int val quake_keep : unit -> bool +val query_cache : unit -> bool val query_stats : unit -> bool val record_hints : unit -> bool val record_options : unit -> bool diff --git a/src/class/FStar.Class.Hashable.fst b/src/class/FStar.Class.Hashable.fst index a0f2039a3da..6a14d2509d8 100644 --- a/src/class/FStar.Class.Hashable.fst +++ b/src/class/FStar.Class.Hashable.fst @@ -1,3 +1,91 @@ module FStar.Class.Hashable -(* empty *) +open FStar +open FStar.Compiler +open FStar.Hash +open FStar.Class.Show +open FStar.Class.Deq +open FStar.Class.Ord + +instance showable_hash_code : showable hash_code = { + show = string_of_hash_code; +} + +instance eq_hash_code : deq hash_code = { + ( =? ) = (=); +} + +instance ord_hash_code : ord hash_code = { + super = FStar.Tactics.Typeclasses.solve; + cmp = (fun x y -> Order.order_from_int (cmp_hash x y)); +} + +instance hashable_int : hashable int = { hash = of_int; } +instance hashable_string : hashable string = { hash = of_string; } +instance hashable_bool : hashable bool = { + hash = (fun b -> if b then of_int 1 else of_int 2); +} + +instance hashable_list + (_ : hashable 'a) +: Tot (hashable (list 'a)) = { + hash = (fun xs -> List.fold_left (fun h x -> mix h (hash x)) (of_int 0) xs); +} + +instance hashable_option + (_ : hashable 'a) +: Tot (hashable (option 'a)) = { + hash = (fun x -> match x with None -> of_int 0 | Some x -> mix (of_int 1) (hash x)); +} + +instance hashable_either + (_ : hashable 'a) + (_ : hashable 'b) +: Tot (hashable (either 'a 'b)) = { + hash = (fun x -> match x with Inl a -> mix (of_int 0) (hash a) | Inr b -> mix (of_int 1) (hash b)); +} + +instance hashable_tuple2 + (_ : hashable 'a) + (_ : hashable 'b) +: Tot (hashable ('a & 'b)) = { + hash = (fun (a, b) -> hash a `mix` hash b); +} + +instance hashable_tuple3 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) +: Tot (hashable ('a & 'b & 'c)) = { + hash = (fun (a, b, c) -> hash a `mix` hash b `mix` hash c); +} + +instance hashable_tuple4 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) + (_ : hashable 'd) +: Tot (hashable ('a & 'b & 'c & 'd)) = { + hash = (fun (a, b, c, d) -> hash a `mix` hash b `mix` hash c `mix` hash d); +} + +instance hashable_tuple5 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) + (_ : hashable 'd) + (_ : hashable 'e) +: Tot (hashable ('a & 'b & 'c & 'd & 'e)) = { + hash = (fun (a, b, c, d, e) -> hash a `mix` hash b `mix` hash c `mix` hash d `mix` hash e); +} + +instance hashable_tuple6 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) + (_ : hashable 'd) + (_ : hashable 'e) + (_ : hashable 'f) +: Tot (hashable ('a & 'b & 'c & 'd & 'e & 'f)) = { + hash = (fun (a, b, c, d, e, f) -> hash a `mix` hash b `mix` hash c `mix` hash d `mix` hash e `mix` hash f); +} diff --git a/src/class/FStar.Class.Hashable.fsti b/src/class/FStar.Class.Hashable.fsti index de34f4f7475..56200545f22 100644 --- a/src/class/FStar.Class.Hashable.fsti +++ b/src/class/FStar.Class.Hashable.fsti @@ -1,12 +1,68 @@ module FStar.Class.Hashable +open FStar.Hash include FStar.Hash +open FStar.Class.Show +open FStar.Class.Deq +open FStar.Class.Ord class hashable (a:Type) = { hash : a -> hash_code; } -instance hashable_int : hashable int = { hash = of_int; } -instance hashable_string : hashable string = { hash = of_string; } +(* Properties about hash_code, better moved elsewhere. *) +instance val showable_hash_code : showable hash_code +instance val eq_hash_code : deq hash_code +instance val ord_hash_code : ord hash_code -instance showable_hash_code : showable hash_code = { show = string_of_hash_code; } +instance val hashable_int : hashable int +instance val hashable_string : hashable string +instance val hashable_bool : hashable bool + +instance val hashable_list + (_ : hashable 'a) +: Tot (hashable (list 'a)) + +instance val hashable_option + (_ : hashable 'a) +: Tot (hashable (option 'a)) + +instance val hashable_either + (_ : hashable 'a) + (_ : hashable 'b) +: Tot (hashable (either 'a 'b)) + +instance val hashable_tuple2 + (_ : hashable 'a) + (_ : hashable 'b) +: Tot (hashable ('a & 'b)) + +instance val hashable_tuple3 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) +: Tot (hashable ('a & 'b & 'c)) + +instance val hashable_tuple4 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) + (_ : hashable 'd) +: Tot (hashable ('a & 'b & 'c & 'd)) + +instance val hashable_tuple5 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) + (_ : hashable 'd) + (_ : hashable 'e) +: Tot (hashable ('a & 'b & 'c & 'd & 'e)) + +instance val hashable_tuple6 + (_ : hashable 'a) + (_ : hashable 'b) + (_ : hashable 'c) + (_ : hashable 'd) + (_ : hashable 'e) + (_ : hashable 'f) +: Tot (hashable ('a & 'b & 'c & 'd & 'e & 'f)) diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.Cache.fst b/src/smtencoding/FStar.SMTEncoding.Solver.Cache.fst new file mode 100644 index 00000000000..514bfdb3bcf --- /dev/null +++ b/src/smtencoding/FStar.SMTEncoding.Solver.Cache.fst @@ -0,0 +1,160 @@ +(* + Copyright 2008-2014 Nikhil Swamy and Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + +module FStar.SMTEncoding.Solver.Cache + +open FStar +open FStar.Compiler +open FStar.Compiler.Effect +open FStar.TypeChecker.Env +open FStar.Syntax.Syntax + +module BU = FStar.Compiler.Util +open FStar.Compiler.RBSet + +open FStar.Class.Show +open FStar.Class.Hashable + +(* import instances *) +module XXX0 = FStar.Syntax.Hash + +instance hashable_lident : hashable Ident.lident = { + hash = (fun l -> hash (show l)); +} + +instance hashable_ident : hashable Ident.ident = { + hash = (fun i -> hash (show i)); +} + +instance hashable_binding : hashable binding = { + hash = (function + | Binding_var bv -> hash bv.sort + | Binding_lid (l, (us, t)) -> hash l `mix` hash us `mix` hash t + | Binding_univ u -> hash u); +} + +instance hashable_bv : hashable bv = { + // hash name? + hash = (fun b -> hash b.sort); +} + +instance hashable_fv : hashable fv = { + hash = (fun f -> hash f.fv_name.v); +} + +instance hashable_binder : hashable binder = { + hash = (fun b -> hash b.binder_bv); +} + +instance hashable_letbinding : hashable letbinding = { + hash = (fun lb -> hash lb.lbname `mix` hash lb.lbtyp `mix` hash lb.lbdef); +} + +instance hashable_pragma : hashable pragma = { + hash = (function + | SetOptions s -> hash 1 `mix` hash s + | ResetOptions s -> hash 2 `mix` hash s + | PushOptions s -> hash 3 `mix` hash s + | PopOptions -> hash 4 + | RestartSolver -> hash 5 + | PrintEffectsGraph -> hash 6); +} + +let rec hash_sigelt (se:sigelt) : hash_code = + hash_sigelt' se.sigel + +and hash_sigelt' (se:sigelt') : hash_code = + match se with + | Sig_inductive_typ {lid; us; params; num_uniform_params; t; mutuals; ds; injective_type_params} -> + hash 0 `mix` + hash lid `mix` + hash us `mix` + hash params `mix` + hash num_uniform_params `mix` + hash t `mix` + hash mutuals `mix` + hash ds `mix` + hash injective_type_params + | Sig_bundle {ses; lids} -> + hash 1 `mix` + (hashable_list #_ {hash=hash_sigelt}).hash ses // sigh, reusing hashable instance when we don't have an instance + `mix` hash lids + | Sig_datacon {lid; us; t; ty_lid; num_ty_params; mutuals; injective_type_params} -> + hash 2 `mix` + hash lid `mix` + hash us `mix` + hash t `mix` + hash ty_lid `mix` + hash num_ty_params `mix` + hash mutuals `mix` + hash injective_type_params + | Sig_declare_typ {lid; us; t} -> + hash 3 `mix` + hash lid `mix` + hash us `mix` + hash t + | Sig_let {lbs; lids} -> + hash 4 `mix` + hash lbs `mix` + hash lids + | Sig_assume {lid; us; phi} -> + hash 5 `mix` + hash lid `mix` + hash us `mix` + hash phi + | Sig_pragma p -> + hash 6 `mix` + hash p + | _ -> + (* FIXME: hash is not completely faithful. In particular + it ignores effect decls and hashes them the same. *) + hash 0 + +instance hashable_sigelt : hashable sigelt = { + hash = hash_sigelt; +} + +(* All that matters for the query cache. *) +instance hashable_env : hashable env = { + hash = (fun e -> + hash e.gamma `mix` + hash e.gamma_sig `mix` + hash e.proof_ns `mix` + hash (e.admit, e.lax) + ); +} + +let query_cache_ref : ref (RBSet.t hash_code) = + BU.mk_ref (empty ()) + +let on () = + Options.query_cache () && Options.ide () + +let query_cache_add (g:env) (q:term) : unit = + if on () then ( + let h = hash (g, q) in +// BU.print1 "Adding query cache for %s\n" (show h); + query_cache_ref := add h !query_cache_ref + ) + +let try_find_query_cache (g:env) (q:term) : bool = + if on () then ( + let h = hash (g, q) in + let r = mem h !query_cache_ref in +// BU.print2 "Looked up query cache for %s, r = %s\n" (show h) (show r); + r + ) else + false diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.Cache.fsti b/src/smtencoding/FStar.SMTEncoding.Solver.Cache.fsti new file mode 100644 index 00000000000..bbf309847e9 --- /dev/null +++ b/src/smtencoding/FStar.SMTEncoding.Solver.Cache.fsti @@ -0,0 +1,26 @@ +(* + Copyright 2008-2014 Nikhil Swamy and Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) + +module FStar.SMTEncoding.Solver.Cache + +open FStar +open FStar.Compiler +open FStar.Compiler.Effect +open FStar.TypeChecker.Env +open FStar.Syntax.Syntax + +val query_cache_add (g:env) (q:term) : unit +val try_find_query_cache (g:env) (q:term) : bool diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst index 57ff49a56cf..829c22a3974 100644 --- a/src/smtencoding/FStar.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst @@ -31,6 +31,8 @@ open FStar.SMTEncoding.ErrorReporting open FStar.SMTEncoding.Util open FStar.Class.Show open FStar.Class.PP +open FStar.Class.Hashable +open FStar.Compiler.RBSet module BU = FStar.Compiler.Util module Env = FStar.TypeChecker.Env @@ -746,7 +748,7 @@ let fold_queries (qs:list query_settings) let full_query_id settings = "(" ^ settings.query_name ^ ", " ^ (BU.string_of_int settings.query_index) ^ ")" -let collect (l : list 'a) : list ('a & int) = +let collect_dups (l : list 'a) : list ('a & int) = let acc : list ('a & int) = [] in let rec add_one acc x = match acc with @@ -763,18 +765,34 @@ let collect (l : list 'a) : list ('a & int) = it succeeded or not. The rest is only used for error reporting. *) type answer = { ok : bool; - nsuccess : int; - lo : int; - hi : int; - errs : list (list errors); // mmm... list list? + (* ^ Query was proven *) + cache_hit : bool; + (* ^ Got result from cache. Currently, this also implies + ok=true (we don't cache failed queries), but don't count + on it. *) + quaking : bool; + (* ^ Were we quake testing? *) quaking_or_retrying : bool; + (* ^ Were we quake testing *or* retrying? *) + lo : int; + (* ^ Lower quake bound. *) + hi : int; + (* ^ Higher quake bound. *) + nsuccess : int; + (* ^ Number of successful attempts. Can be >1 when quaking. *) total_ran : int; + (* ^ Total number of queries made. *) tried_recovery : bool; + (* ^ Did we try using --proof_recovery for this? *) + + errs : list (list errors); // mmm... list list? + (* ^ Errors from SMT solver. *) } let ans_ok : answer = { ok = true; + cache_hit = false; nsuccess = 1; lo = 1; hi = 1; @@ -1020,6 +1038,7 @@ let ask_solver_quake in (* Return answer *) { ok = nsuccess >= lo + ; cache_hit = false ; nsuccess = nsuccess ; lo = lo ; hi = hi @@ -1208,7 +1227,7 @@ let report (env:Env.env) (default_settings : query_settings) (a : answer) : unit (* Obtain all errors that would have been reported *) let errs = List.map errors_to_report all_errs in (* Summarize them *) - let errs = errs |> List.flatten |> collect in + let errs = errs |> List.flatten |> collect_dups in (* Show the amount on each error *) let errs = errs |> List.map (fun ((e, m, r, ctx), n) -> let m = @@ -1300,6 +1319,7 @@ let finally (h : unit -> unit) (f : unit -> 'a) : 'a = (* The query_settings list is non-empty unless the query was trivial. *) let encode_and_ask (can_split:bool) (is_retry:bool) use_env_msg tcenv q : (list query_settings & answer) = + let do () : list query_settings & answer = maybe_refresh_solver tcenv; Encode.push (BU.format1 "Starting query at %s" (Range.string_of_range <| Env.get_range tcenv)); let pop () = Encode.pop (BU.format1 "Ending query at %s" (Range.string_of_range <| Env.get_range tcenv)) in @@ -1329,6 +1349,15 @@ let encode_and_ask (can_split:bool) (is_retry:bool) use_env_msg tcenv q : (list | _ -> failwith "Impossible" ) + in + if Solver.Cache.try_find_query_cache tcenv q then ( + ([], { ans_ok with cache_hit = true }) + ) else ( + let (cfgs, ans) = do () in + if ans.ok then + Solver.Cache.query_cache_add tcenv q; + (cfgs, ans) + ) (* Asks the solver and reports errors. Does quake if needed. *) let do_solve (can_split:bool) (is_retry:bool) use_env_msg tcenv q : unit = diff --git a/src/syntax/FStar.Syntax.Hash.fst b/src/syntax/FStar.Syntax.Hash.fst index 76dceef79c2..d382285d1bf 100644 --- a/src/syntax/FStar.Syntax.Hash.fst +++ b/src/syntax/FStar.Syntax.Hash.fst @@ -608,3 +608,7 @@ and equal_subst_elt s1 s2 = | UD (un1, i1), UD (un2, i2) -> i1 = i2 && Ident.ident_equals un1 un2 + +instance hashable_term : hashable term = { + hash = ext_hash_term; +} diff --git a/src/syntax/FStar.Syntax.Hash.fsti b/src/syntax/FStar.Syntax.Hash.fsti index bc6ba90db37..8d4bb8c35e0 100644 --- a/src/syntax/FStar.Syntax.Hash.fsti +++ b/src/syntax/FStar.Syntax.Hash.fsti @@ -23,7 +23,11 @@ open FStar.Compiler.Util open FStar.Syntax.Syntax open FStar.Const module H = FStar.Hash +open FStar.Class.Hashable val ext_hash_term (t:term) : H.hash_code val ext_hash_term_no_memo (t:term) : H.hash_code val equal_term (t0 t1:term) : bool + +(* uses ext_hash_term (with memo) *) +instance val hashable_term : hashable term