From 36eaa99fd16e159d807785540c2f0ee8d226f023 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 23 Jul 2023 20:00:30 -0700 Subject: [PATCH 1/9] Compiler.Util: keep program name in process Useful to later display messages about it. --- ocaml/fstar-lib/FStar_Compiler_Util.ml | 7 ++++++- src/basic/FStar.Compiler.Util.fsti | 1 + 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/ocaml/fstar-lib/FStar_Compiler_Util.ml b/ocaml/fstar-lib/FStar_Compiler_Util.ml index 0b4ec5b777e..e5ae389b938 100644 --- a/ocaml/fstar-lib/FStar_Compiler_Util.ml +++ b/ocaml/fstar-lib/FStar_Compiler_Util.ml @@ -93,6 +93,7 @@ type proc = mutable killed : bool; stop_marker: (string -> bool) option; id : string; + prog : string; start_time : time} let all_procs : (proc list) ref = ref [] @@ -142,7 +143,9 @@ let start_process' Unix.close stdin_r; Unix.close stdout_w; Unix.close stderr_w; - let proc = { pid = pid; id = prog ^ ":" ^ id; + let proc = { pid = pid; + id = prog ^ ":" ^ id; + prog = prog; inc = Unix.in_channel_of_descr stdout_r; errc = Unix.in_channel_of_descr stderr_r; outc = Unix.out_channel_of_descr stdin_w; @@ -186,6 +189,8 @@ let kill_process (p: proc) = let kill_all () = BatList.iter kill_process !all_procs +let proc_prog (p:proc) : string = p.prog + let process_read_all_output (p: proc) = (* Pass cleanup:false because kill_process closes both fds already. *) BatIO.read_all (BatIO.input_channel ~autoclose:true ~cleanup:false p.inc) diff --git a/src/basic/FStar.Compiler.Util.fsti b/src/basic/FStar.Compiler.Util.fsti index d2631f5d409..d60f3eb5b48 100644 --- a/src/basic/FStar.Compiler.Util.fsti +++ b/src/basic/FStar.Compiler.Util.fsti @@ -205,6 +205,7 @@ val start_process: string -> string -> list string -> (string -> bool) -> proc val ask_process: proc -> string -> (*err_handler:*)(unit -> string) -> (*stderr_handler:*)(string -> unit) -> string val kill_process: proc -> unit val kill_all: unit -> unit +val proc_prog : proc -> string val get_file_extension: string -> string val is_path_absolute: string -> bool From 612da98fe2c38a63e212edab5df47cb484ed0bce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 23 Jul 2023 20:01:17 -0700 Subject: [PATCH 2/9] Compiler.Misc: new module, introduce version comparison --- src/basic/FStar.Compiler.Misc.fst | 16 ++++++++++++++++ src/basic/FStar.Compiler.Misc.fsti | 10 ++++++++++ 2 files changed, 26 insertions(+) create mode 100644 src/basic/FStar.Compiler.Misc.fst create mode 100644 src/basic/FStar.Compiler.Misc.fsti diff --git a/src/basic/FStar.Compiler.Misc.fst b/src/basic/FStar.Compiler.Misc.fst new file mode 100644 index 00000000000..82f8e9f2856 --- /dev/null +++ b/src/basic/FStar.Compiler.Misc.fst @@ -0,0 +1,16 @@ +module FStar.Compiler.Misc + +open FStar.Compiler +open FStar.Compiler.Effect +open FStar.Compiler.Util + +open FStar.Order +open FStar.String + +let compare_version (v1 v2 : string) : order = + let cs1 = String.split ['.'] v1 |> List.map int_of_string in + let cs2 = String.split ['.'] v2 |> List.map int_of_string in + compare_list cs1 cs2 compare_int + +let version_gt v1 v2 = compare_version v1 v2 = Gt +let version_ge v1 v2 = compare_version v1 v2 <> Lt diff --git a/src/basic/FStar.Compiler.Misc.fsti b/src/basic/FStar.Compiler.Misc.fsti new file mode 100644 index 00000000000..5d61e8c999e --- /dev/null +++ b/src/basic/FStar.Compiler.Misc.fsti @@ -0,0 +1,10 @@ +module FStar.Compiler.Misc + +open FStar.Compiler.Effect + +(* This functions compare version numbers. E.g. "4.8.5" and "4.12.3". +NOTE: the versions cannot contain any alphabetic character, only numbers +are allowed for now. *) + +val version_gt : string -> string -> bool +val version_ge : string -> string -> bool From 655cf97bec484cdb28457cc96a5990e136f1955f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 23 Jul 2023 20:01:57 -0700 Subject: [PATCH 3/9] SMTEncoding: remove some unused functions --- src/smtencoding/FStar.SMTEncoding.Encode.fst | 1 - src/smtencoding/FStar.SMTEncoding.Solver.fst | 2 +- src/smtencoding/FStar.SMTEncoding.Z3.fsti | 3 --- 3 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/smtencoding/FStar.SMTEncoding.Encode.fst b/src/smtencoding/FStar.SMTEncoding.Encode.fst index 315f481385c..baffd898490 100644 --- a/src/smtencoding/FStar.SMTEncoding.Encode.fst +++ b/src/smtencoding/FStar.SMTEncoding.Encode.fst @@ -1787,7 +1787,6 @@ let rollback_env depth = FStar.Common.rollback pop_env last_env depth let init tcenv = init_env tcenv; - Z3.init (); Z3.giveZ3 [DefPrelude] let snapshot msg = BU.atomically (fun () -> let env_depth, () = snapshot_env () in diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst index c216581ae0f..9ef06d979da 100644 --- a/src/smtencoding/FStar.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst @@ -1286,7 +1286,7 @@ let solver = { solve=solve; solve_sync=solve_sync_bool; - finish=Z3.finish; + finish=(fun () -> ()); refresh=Z3.refresh; } diff --git a/src/smtencoding/FStar.SMTEncoding.Z3.fsti b/src/smtencoding/FStar.SMTEncoding.Z3.fsti index 46fffaa6ac5..2435f44e0cd 100644 --- a/src/smtencoding/FStar.SMTEncoding.Z3.fsti +++ b/src/smtencoding/FStar.SMTEncoding.Z3.fsti @@ -49,7 +49,6 @@ type query_log = { } val status_string_and_errors : z3status -> string * error_labels -val set_z3_options : string -> unit val giveZ3 : list decl -> unit val ask: r:Range.range @@ -63,9 +62,7 @@ val ask: r:Range.range -> z3result val refresh: unit -> unit -val finish: unit -> unit val mk_fresh_scope: unit -> scope_t -val init : unit -> unit val push : msg:string -> unit val pop : msg:string -> unit val snapshot : msg:string -> (int * unit) From c0058e665bbd14ea9dacceb687619ac57d2e93da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 31 Mar 2023 13:21:21 -0700 Subject: [PATCH 4/9] SMTEncoding: introduce Z3 version switch --- src/basic/FStar.Errors.Codes.fst | 2 + src/basic/FStar.Errors.Codes.fsti | 2 + src/basic/FStar.Options.fst | 14 +- src/basic/FStar.Options.fsti | 3 +- src/smtencoding/FStar.SMTEncoding.Solver.fst | 2 + src/smtencoding/FStar.SMTEncoding.Z3.fst | 225 +++++++++++-------- 6 files changed, 154 insertions(+), 94 deletions(-) diff --git a/src/basic/FStar.Errors.Codes.fst b/src/basic/FStar.Errors.Codes.fst index 8ba0f50c395..28377042ed2 100644 --- a/src/basic/FStar.Errors.Codes.fst +++ b/src/basic/FStar.Errors.Codes.fst @@ -372,4 +372,6 @@ let default_settings : list error_setting = Error_InternalQualifier , CAlwaysError, 354; Warning_NameEscape , CWarning, 355; Warning_UnexpectedZ3Stderr , CWarning, 356; + Warning_SolverMismatch , CError, 357; + Warning_SolverVersionMismatch , CError, 358; ] diff --git a/src/basic/FStar.Errors.Codes.fsti b/src/basic/FStar.Errors.Codes.fsti index 612580d5a64..354177f07ba 100644 --- a/src/basic/FStar.Errors.Codes.fsti +++ b/src/basic/FStar.Errors.Codes.fsti @@ -384,6 +384,8 @@ type raw_error = | Error_InternalQualifier | Warning_NameEscape | Warning_UnexpectedZ3Stderr + | Warning_SolverMismatch + | Warning_SolverVersionMismatch type error_setting = raw_error * error_flag * int diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst index ef4e5803709..f746588c8d2 100644 --- a/src/basic/FStar.Options.fst +++ b/src/basic/FStar.Options.fst @@ -258,6 +258,7 @@ let defaults = ("z3seed" , Int 0); ("z3cliopt" , List []); ("z3smtopt" , List []); + ("z3version" , String "4.8.5"); ("__no_positivity" , Bool false); ("__tactics_nbe" , Bool false); ("warn_error" , List []); @@ -319,6 +320,7 @@ let set_verification_options o = "z3rlimit"; "z3rlimit_factor"; "z3seed"; + "z3version"; "trivial_pre_for_unannotated_effectful_fns"; ] in List.iter (fun k -> set_option k (Util.smap_try_find o k |> Util.must)) verifopts @@ -441,6 +443,7 @@ let get_z3refresh () = lookup_opt "z3refresh" let get_z3rlimit () = lookup_opt "z3rlimit" as_int let get_z3rlimit_factor () = lookup_opt "z3rlimit_factor" as_int let get_z3seed () = lookup_opt "z3seed" as_int +let get_z3version () = lookup_opt "z3version" as_string let get_no_positivity () = lookup_opt "__no_positivity" as_bool let get_warn_error () = lookup_opt "warn_error" (as_list as_string) let get_use_nbe () = lookup_opt "use_nbe" as_bool @@ -1286,6 +1289,11 @@ let rec specs_with_types warn_unsafe : list (char * string * opt_type * string) IntStr "positive_integer", "Set the Z3 random seed (default 0)"); + ( noshort, + "z3version", + SimpleStr "version", + "Set the version of Z3 that is to be used. Default: 4.8.5"); + ( noshort, "__no_positivity", WithSideEffect ((fun _ -> if warn_unsafe then option_warning_callback "__no_positivity"), Const (Bool true)), @@ -1440,6 +1448,7 @@ let settable = function | "z3rlimit" | "z3rlimit_factor" | "z3seed" + | "z3version" | "trivial_pre_for_unannotated_effectful_fns" | "profile_group_by_decl" | "profile_component" @@ -1800,6 +1809,7 @@ let retry () = get_retry () let reuse_hint_for () = get_reuse_hint_for () let report_assumes () = get_report_assumes () let silent () = get_silent () +let smt () = get_smt () let smtencoding_elim_box () = get_smtencoding_elim_box () let smtencoding_nl_arith_native () = get_smtencoding_nl_arith_repr () = "native" let smtencoding_nl_arith_wrapped () = get_smtencoding_nl_arith_repr () = "wrapped" @@ -1839,15 +1849,13 @@ let using_facts_from () = | Some ns -> parse_settings ns let warn_default_effects () = get_warn_default_effects () let warn_error () = String.concat " " (get_warn_error()) -let z3_exe () = match get_smt () with - | None -> Platform.exe "z3" - | Some s -> s let z3_cliopt () = get_z3cliopt () let z3_smtopt () = get_z3smtopt () let z3_refresh () = get_z3refresh () let z3_rlimit () = get_z3rlimit () let z3_rlimit_factor () = get_z3rlimit_factor () let z3_seed () = get_z3seed () +let z3_version () = get_z3version () let no_positivity () = get_no_positivity () let use_nbe () = get_use_nbe () let use_nbe_for_extraction () = get_use_nbe_for_extraction () diff --git a/src/basic/FStar.Options.fsti b/src/basic/FStar.Options.fsti index eb9fb9c0043..31cdc4bed28 100644 --- a/src/basic/FStar.Options.fsti +++ b/src/basic/FStar.Options.fsti @@ -201,6 +201,7 @@ val should_check_file : string -> bool (* Should check this file, lax val should_verify : string -> bool (* Should check this module with verification enabled. *) val should_verify_file : string -> bool (* Should check this file with verification enabled. *) val silent : unit -> bool +val smt : unit -> option string val smtencoding_elim_box : unit -> bool val smtencoding_nl_arith_default: unit -> bool val smtencoding_nl_arith_wrapped: unit -> bool @@ -230,13 +231,13 @@ val use_tactics : unit -> bool val using_facts_from : unit -> list (list string * bool) val warn_default_effects : unit -> bool val with_saved_options : (unit -> 'a) -> 'a -val z3_exe : unit -> string val z3_cliopt : unit -> list string val z3_smtopt : unit -> list string val z3_refresh : unit -> bool val z3_rlimit : unit -> int val z3_rlimit_factor : unit -> int val z3_seed : unit -> int +val z3_version : unit -> string val no_positivity : unit -> bool val warn_error : unit -> string val set_error_flags_callback : ((unit -> parse_cmdline_res) -> unit) diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst index 9ef06d979da..3ca037b828b 100644 --- a/src/smtencoding/FStar.SMTEncoding.Solver.fst +++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst @@ -1084,6 +1084,7 @@ type solver_cfg = { facts : list (list string * bool); valid_intro : bool; valid_elim : bool; + z3version : string; } let _last_cfg : ref (option solver_cfg) = BU.mk_ref None @@ -1095,6 +1096,7 @@ let get_cfg env : solver_cfg = ; facts = env.proof_ns ; valid_intro = Options.smtencoding_valid_intro () ; valid_elim = Options.smtencoding_valid_elim () + ; z3version = Options.z3_version () } let save_cfg env = diff --git a/src/smtencoding/FStar.SMTEncoding.Z3.fst b/src/smtencoding/FStar.SMTEncoding.Z3.fst index 8abc72f7900..bd42bc8e992 100644 --- a/src/smtencoding/FStar.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStar.SMTEncoding.Z3.fst @@ -22,75 +22,63 @@ open FStar.SMTEncoding.Term open FStar.BaseTypes open FStar.Compiler.Util +module M = FStar.Compiler.Misc module BU = FStar.Compiler.Util (****************************************************************************) (* Z3 Specifics *) (****************************************************************************) -(* Check the Z3 commit hash once, and issue a warning if it is not - equal to the one that we are expecting from the Z3 url below -*) -let _z3version_checked : ref bool = BU.mk_ref false - -let _z3version_expected = "Z3 version 4.8.5" - -let _z3url = "https://github.com/FStarLang/binaries/tree/master/z3-tested" - -let parse_z3_version_lines out = - match splitlines out with - | version :: _ -> - if BU.starts_with version _z3version_expected - then begin - if Options.debug_any () - then - print_string - (BU.format1 - "Successfully found expected Z3 version %s\n" - version); - None - end - else - let msg = - BU.format2 - "Expected Z3 version \"%s\", got \"%s\"" - _z3version_expected - (BU.trim_string out) - in - Some msg - | _ -> Some "No Z3 version string found" +(* We only warn once about these things *) +let _already_warned_solver_mismatch : ref bool = BU.mk_ref false +let _already_warned_version_mismatch : ref bool = BU.mk_ref false -let z3version_warning_message () = - let run_proc_result = - try - Some (BU.run_process "z3_version" (Options.z3_exe()) ["-version"] None) - with _ -> None - in - match run_proc_result with - | None -> Some (FStar.Errors.Error_Z3InvocationError, "Could not run Z3") - | Some out -> - begin match parse_z3_version_lines out with - | None -> None - | Some msg -> Some (FStar.Errors.Warning_Z3InvocationWarning, msg) - end - -let check_z3version () = - if not !_z3version_checked - then begin - _z3version_checked := true; - match z3version_warning_message () with - | None -> () - | Some (e, msg) -> - let msg = - BU.format4 - "%s\n%s\n%s\n%s" - msg - "Please download the version of Z3 corresponding to your platform from:" - _z3url - "and add the bin/ subdirectory into your PATH" - in - FStar.Errors.log_issue Range.dummyRange (e, msg) - end +let z3url = "https://github.com/Z3Prover/z3/releases" + +(* Check if [path] is potentially a valid z3, by trying to run +it with -version and checking for non-empty output. Alternatively +we could call [which] on it (if it's not an absolute path), but +we shouldn't rely on the existence of a binary which. *) +let inpath (path:string) : bool = + try + let s = BU.run_process "z3_pathtest" path ["-version"] None in + s <> "" + with + | _ -> false + +(* Find the Z3 executable that we should invoke, according to the +needed version. The logic is as follows: + +- If the user provided the --smt option, use that binary unconditionally. +- If z3-VER (or z3-VER.exe) exists in the PATH (where VER is either + the default version or the user-provided --z3version) use it. +- Otherwise, default to "z3" in the PATH. + +We cache the chosen executable for every Z3 version we've ran. +*) +let z3_exe : unit -> string = + let cache : BU.smap string = BU.smap_create 5 in + let find_or (k:string) (f : string -> string) : string = + match smap_try_find cache k with + | Some v -> v + | None -> + let v = f k in + smap_add cache k v; + v + in + fun () -> + find_or (Options.z3_version()) (fun version -> + let path = + let z3_v = Platform.exe ("z3-" ^ version) in + let smto = Options.smt () in + if Some? smto then Some?.v smto + else if inpath z3_v then z3_v + else Platform.exe "z3" + in + if Options.debug_any () then + BU.print1 "Chosen Z3 executable: %s\n" path; + path + ) type label = string @@ -183,7 +171,7 @@ let query_logging = (* Z3 background process handling *) let z3_cmd_and_args () = - let cmd = Options.z3_exe () in + let cmd = z3_exe () in let cmd_args = List.append ["-smt2"; "-in"; @@ -191,21 +179,60 @@ let z3_cmd_and_args () = (Options.z3_cliopt ()) in (cmd, cmd_args) -let new_z3proc id cmd_and_args = - check_z3version(); - BU.start_process id (fst cmd_and_args) (snd cmd_and_args) (fun s -> s = "Done!") - let warn_handler (s:string) : unit = Errors.log_issue Range.dummyRange (Errors.Warning_UnexpectedZ3Output, "Unexpected output from Z3: \"" ^ s ^ "\"") +(* Talk to the process to see if it's the correct version of Z3 +(i.e. the one in the optionstate). Also check that it indeed is Z3. By +default, each of these generates an error, but they can be downgraded +into warnings. The warnings are anyway printed only once per F* +invocation. *) +let check_z3version (p:proc) : unit = + let getinfo (arg:string) : string = + let s = BU.ask_process p (Util.format1 "(get-info :%s)\n(echo \"Done!\")\n" arg) (fun _ -> "Killed") warn_handler in + if BU.starts_with s ("(:" ^ arg) then + let ss = String.split ['"'] s in + List.nth ss 1 + else ( + warn_handler s; + Errors.raise_err (Errors.Error_Z3InvocationError, BU.format1 "Could not run Z3 from `%s'" (proc_prog p)) + ) + in + let name = getinfo "name" in + if name <> "Z3" && not (!_already_warned_solver_mismatch) then ( + Errors.log_issue Range.dummyRange (Errors.Warning_SolverMismatch, + BU.format3 "Unexpected SMT solver: expected to be talking to Z3, got %s.\n\ + Please download the correct version of Z3 from %s\n\ + and install it into your $PATH as `%s'." + name + z3url (Platform.exe ("z3-" ^ Options.z3_version ())) + ); + _already_warned_solver_mismatch := true + ); + let ver = getinfo "version" in + if ver <> Options.z3_version () && not (!_already_warned_version_mismatch) then ( + Errors.log_issue Range.dummyRange (Errors.Warning_SolverMismatch, + BU.format5 "Unexpected Z3 version for `%s': expected %s, got %s.\n\ + Please download the correct version of Z3 from %s\n\ + and install it into your $PATH as `%s'." + (proc_prog p) + (Options.z3_version()) ver + z3url (Platform.exe ("z3-" ^ Options.z3_version ())) + ); + _already_warned_version_mismatch := true + ); + () + +let new_z3proc (id:string) (cmd_and_args : string & list string) : BU.proc = + let proc = BU.start_process id (fst cmd_and_args) (snd cmd_and_args) (fun s -> s = "Done!") in + check_z3version proc; + proc + let new_z3proc_with_id = let ctr = BU.mk_ref (-1) in (fun cmd_and_args -> - let p = new_z3proc (BU.format1 "bg-%s" (incr ctr; !ctr |> string_of_int)) cmd_and_args in - let reply = BU.ask_process p "(echo \"Test\")\n(echo \"Done!\")\n" (fun _ -> "Killed") warn_handler in - if reply = "Test\n" - then p - else failwith (BU.format1 "Failed to start and test Z3 process, expected output \"Test\" got \"%s\"" reply)) + let p = new_z3proc (BU.format1 "z3-bg-%s" (incr ctr; !ctr |> string_of_int)) cmd_and_args in + p) type bgproc = { ask: string -> string; @@ -229,10 +256,15 @@ let bg_z3_proc = let the_z3proc = BU.mk_ref None in let the_z3proc_params = BU.mk_ref (Some ("", [""])) in let the_z3proc_ask_count = BU.mk_ref 0 in + let the_z3proc_version = BU.mk_ref "" in + // NOTE: We keep track of the version and restart on changes + // just to be safe: the executable name in the_z3proc_params should + // be enough to distinguish between the different executables. let make_new_z3_proc cmd_and_args = the_z3proc := Some (new_z3proc_with_id cmd_and_args); the_z3proc_params := Some cmd_and_args; the_z3proc_ask_count := 0 in + the_z3proc_version := Options.z3_version (); let z3proc () = if !the_z3proc = None then make_new_z3_proc (z3_cmd_and_args ()); must (!the_z3proc) @@ -251,14 +283,25 @@ let bg_z3_proc = let refresh () = let next_params = z3_cmd_and_args () in let old_params = must (!the_z3proc_params) in + + let old_version = !the_z3proc_version in + let next_version = Options.z3_version () in + + (* We only refresh the solver if we have used it at all, or if the + parameters/version must be changed. We also force a refresh if log_queries is + on. I (GM 2023/07/23) think this might have been for making sure we get + a new file after checking a dependency, and that it might not be needed + now. However it's not a big performance hit, and it's only when logging + queries, so I'm maintaining this. *) if Options.log_queries() || (!the_z3proc_ask_count > 0) || - not (old_params = next_params) + old_params <> next_params || + old_version <> next_version then begin maybe_kill_z3proc(); if Options.query_stats() then begin - BU.print3 "Refreshing the z3proc (ask_count=%s old=[%s] new=[%s]) \n" + BU.print3 "Refreshing the z3proc (ask_count=%s old=[%s] new=[%s])\n" (BU.string_of_int !the_z3proc_ask_count) (cmd_and_args_to_string old_params) (cmd_and_args_to_string next_params) @@ -446,27 +489,30 @@ let doZ3Exe (log_file:_) (r:Range.range) (fresh:bool) (input:string) (label_mess log_result (fun _fname s -> ignore (query_logging.append_to_log s)) r; r -let z3_options = BU.mk_ref +let z3_options (ver:string) = + (* Common z3 prefix for all supported versions (at minimum 4.8.5). + Note: smt.arith.solver defaults to 2 in 4.8.5, but it doesn't hurt to + specify it. *) + let opts = "(set-option :global-decls false)\n\ (set-option :smt.mbqi false)\n\ (set-option :auto_config false)\n\ (set-option :produce-unsat-cores true)\n\ (set-option :model true)\n\ (set-option :smt.case_split 3)\n\ - (set-option :smt.relevancy 2)\n" - -// Use by F*.js -let set_z3_options opts = - z3_options := opts - -let init () = - (* A no-op now that there's no concurrency *) - () - -let finish () = - (* A no-op now that there's no concurrency *) - () + (set-option :smt.relevancy 2)\n\ + (set-option :smt.arith.solver 2)\n" + in + (* We need the following options for Z3 >= 4.12.3 *) + let opts = opts ^ begin + if M.version_ge ver "4.12.3" then + "(set-option :rewriter.enable_der false)\n\ + (set-option :rewriter.sort_disjunctions false)\n\ + (set-option :pi.decompose_patterns false)\n" + else "" end + in + opts // bg_scope is a global, mutable variable that keeps a list of the declarations // that we have given to z3 so far. In order to allow rollback of history, @@ -542,9 +588,8 @@ let context_profile (theory:list decl) = (string_of_int n)) modules - let mk_input fresh theory = - let options = !z3_options in + let options = z3_options (Options.z3_version()) in //fxime use bgproc let options = options ^ (Options.z3_smtopt() |> String.concat "\n") in if Options.print_z3_statistics() then context_profile theory; let r, hash = From 6273c5c8a7e339de355e499a94f9d9cb48ab1b09 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 23 Jul 2023 20:02:25 -0700 Subject: [PATCH 5/9] snap --- .../generated/FStar_Compiler_Misc.ml | 17 + .../fstar-lib/generated/FStar_Errors_Codes.ml | 14 +- ocaml/fstar-lib/generated/FStar_Options.ml | 28 +- .../generated/FStar_SMTEncoding_Encode.ml | 1 - .../generated/FStar_SMTEncoding_Solver.ml | 31 +- .../generated/FStar_SMTEncoding_Z3.ml | 369 ++++++++++-------- 6 files changed, 272 insertions(+), 188 deletions(-) create mode 100644 ocaml/fstar-lib/generated/FStar_Compiler_Misc.ml diff --git a/ocaml/fstar-lib/generated/FStar_Compiler_Misc.ml b/ocaml/fstar-lib/generated/FStar_Compiler_Misc.ml new file mode 100644 index 00000000000..cf346bed48d --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_Compiler_Misc.ml @@ -0,0 +1,17 @@ +open Prims +let (compare_version : Prims.string -> Prims.string -> FStar_Order.order) = + fun v1 -> + fun v2 -> + let cs1 = + FStar_Compiler_Effect.op_Bar_Greater (FStar_String.split [46] v1) + (FStar_Compiler_List.map FStar_Compiler_Util.int_of_string) in + let cs2 = + FStar_Compiler_Effect.op_Bar_Greater (FStar_String.split [46] v2) + (FStar_Compiler_List.map FStar_Compiler_Util.int_of_string) in + FStar_Order.compare_list cs1 cs2 FStar_Order.compare_int +let (version_gt : Prims.string -> Prims.string -> Prims.bool) = + fun v1 -> + fun v2 -> let uu___ = compare_version v1 v2 in uu___ = FStar_Order.Gt +let (version_ge : Prims.string -> Prims.string -> Prims.bool) = + fun v1 -> + fun v2 -> let uu___ = compare_version v1 v2 in uu___ <> FStar_Order.Lt \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml b/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml index 58df18ba2aa..38f42235998 100644 --- a/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml +++ b/ocaml/fstar-lib/generated/FStar_Errors_Codes.ml @@ -372,6 +372,8 @@ type raw_error = | Error_InternalQualifier | Warning_NameEscape | Warning_UnexpectedZ3Stderr + | Warning_SolverMismatch + | Warning_SolverVersionMismatch let (uu___is_Error_DependencyAnalysisFailed : raw_error -> Prims.bool) = fun projectee -> match projectee with @@ -1909,6 +1911,14 @@ let (uu___is_Warning_UnexpectedZ3Stderr : raw_error -> Prims.bool) = match projectee with | Warning_UnexpectedZ3Stderr -> true | uu___ -> false +let (uu___is_Warning_SolverMismatch : raw_error -> Prims.bool) = + fun projectee -> + match projectee with | Warning_SolverMismatch -> true | uu___ -> false +let (uu___is_Warning_SolverVersionMismatch : raw_error -> Prims.bool) = + fun projectee -> + match projectee with + | Warning_SolverVersionMismatch -> true + | uu___ -> false type error_setting = (raw_error * error_flag * Prims.int) let (default_settings : error_setting Prims.list) = [(Error_DependencyAnalysisFailed, CAlwaysError, Prims.int_zero); @@ -2272,4 +2282,6 @@ let (default_settings : error_setting Prims.list) = (Error_PluginDynlink, CError, (Prims.of_int (353))); (Error_InternalQualifier, CAlwaysError, (Prims.of_int (354))); (Warning_NameEscape, CWarning, (Prims.of_int (355))); - (Warning_UnexpectedZ3Stderr, CWarning, (Prims.of_int (356)))] \ No newline at end of file + (Warning_UnexpectedZ3Stderr, CWarning, (Prims.of_int (356))); + (Warning_SolverMismatch, CError, (Prims.of_int (357))); + (Warning_SolverVersionMismatch, CError, (Prims.of_int (358)))] \ 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 6d97e97455a..571e035aa9c 100644 --- a/ocaml/fstar-lib/generated/FStar_Options.ml +++ b/ocaml/fstar-lib/generated/FStar_Options.ml @@ -389,6 +389,7 @@ let (defaults : (Prims.string * option_val) Prims.list) = ("z3seed", (Int Prims.int_zero)); ("z3cliopt", (List [])); ("z3smtopt", (List [])); + ("z3version", (String "4.8.5")); ("__no_positivity", (Bool false)); ("__tactics_nbe", (Bool false)); ("warn_error", (List [])); @@ -447,6 +448,7 @@ let (set_verification_options : optionstate -> unit) = "z3rlimit"; "z3rlimit_factor"; "z3seed"; + "z3version"; "trivial_pre_for_unannotated_effectful_fns"] in FStar_Compiler_List.iter (fun k -> @@ -681,6 +683,8 @@ let (get_z3rlimit_factor : unit -> Prims.int) = fun uu___ -> lookup_opt "z3rlimit_factor" as_int let (get_z3seed : unit -> Prims.int) = fun uu___ -> lookup_opt "z3seed" as_int +let (get_z3version : unit -> Prims.string) = + fun uu___ -> lookup_opt "z3version" as_string let (get_no_positivity : unit -> Prims.bool) = fun uu___ -> lookup_opt "__no_positivity" as_bool let (get_warn_error : unit -> Prims.string Prims.list) = @@ -971,7 +975,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 failwith "unexpected value for --quake" | uu___ -> failwith "unexpected value for --quake" -let (uu___449 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) +let (uu___450 : (((Prims.string -> unit) -> unit) * (Prims.string -> unit))) = let cb = FStar_Compiler_Util.mk_ref FStar_Pervasives_Native.None in let set1 f = @@ -983,11 +987,11 @@ let (uu___449 : (((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___449 with + match uu___450 with | (set_option_warning_callback_aux1, option_warning_callback) -> set_option_warning_callback_aux1 let (option_warning_callback : Prims.string -> unit) = - match uu___449 with + match uu___450 with | (set_option_warning_callback_aux1, option_warning_callback1) -> option_warning_callback1 let (set_option_warning_callback : (Prims.string -> unit) -> unit) = @@ -1335,6 +1339,8 @@ let rec (specs_with_types : "Set the Z3 per-query resource limit multiplier. This is useful when, say, regenerating hints and you want to be more lax. (default 1)"); (FStar_Getopt.noshort, "z3seed", (IntStr "positive_integer"), "Set the Z3 random seed (default 0)"); + (FStar_Getopt.noshort, "z3version", (SimpleStr "version"), + "Set the version of Z3 that is to be used. Default: 4.8.5"); (FStar_Getopt.noshort, "__no_positivity", (WithSideEffect (((fun uu___ -> @@ -1475,6 +1481,7 @@ let (settable : Prims.string -> Prims.bool) = | "z3rlimit" -> true | "z3rlimit_factor" -> true | "z3seed" -> true + | "z3version" -> true | "trivial_pre_for_unannotated_effectful_fns" -> true | "profile_group_by_decl" -> true | "profile_component" -> true @@ -1492,7 +1499,7 @@ let (settable_specs : (FStar_Compiler_List.filter (fun uu___ -> match uu___ with | (uu___1, x, uu___2, uu___3) -> settable x)) -let (uu___640 : +let (uu___642 : (((unit -> FStar_Getopt.parse_cmdline_res) -> unit) * (unit -> FStar_Getopt.parse_cmdline_res))) = @@ -1509,11 +1516,11 @@ let (uu___640 : (set1, call) let (set_error_flags_callback_aux : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = - match uu___640 with + match uu___642 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___640 with + match uu___642 with | (set_error_flags_callback_aux1, set_error_flags1) -> set_error_flags1 let (set_error_flags_callback : (unit -> FStar_Getopt.parse_cmdline_res) -> unit) = @@ -2009,6 +2016,8 @@ let (reuse_hint_for : unit -> Prims.string FStar_Pervasives_Native.option) = let (report_assumes : unit -> Prims.string FStar_Pervasives_Native.option) = fun uu___ -> get_report_assumes () let (silent : unit -> Prims.bool) = fun uu___ -> get_silent () +let (smt : unit -> Prims.string FStar_Pervasives_Native.option) = + fun uu___ -> get_smt () let (smtencoding_elim_box : unit -> Prims.bool) = fun uu___ -> get_smtencoding_elim_box () let (smtencoding_nl_arith_native : unit -> Prims.bool) = @@ -2081,12 +2090,6 @@ let (warn_default_effects : unit -> Prims.bool) = let (warn_error : unit -> Prims.string) = fun uu___ -> let uu___1 = get_warn_error () in FStar_String.concat " " uu___1 -let (z3_exe : unit -> Prims.string) = - fun uu___ -> - let uu___1 = get_smt () in - match uu___1 with - | FStar_Pervasives_Native.None -> FStar_Platform.exe "z3" - | FStar_Pervasives_Native.Some s -> s let (z3_cliopt : unit -> Prims.string Prims.list) = fun uu___ -> get_z3cliopt () let (z3_smtopt : unit -> Prims.string Prims.list) = @@ -2096,6 +2099,7 @@ let (z3_rlimit : unit -> Prims.int) = fun uu___ -> get_z3rlimit () let (z3_rlimit_factor : unit -> Prims.int) = fun uu___ -> get_z3rlimit_factor () let (z3_seed : unit -> Prims.int) = fun uu___ -> get_z3seed () +let (z3_version : unit -> Prims.string) = fun uu___ -> get_z3version () let (no_positivity : unit -> Prims.bool) = fun uu___ -> get_no_positivity () let (use_nbe : unit -> Prims.bool) = fun uu___ -> get_use_nbe () let (use_nbe_for_extraction : unit -> Prims.bool) = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml index 1ee28465ab0..668af33f931 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Encode.ml @@ -7223,7 +7223,6 @@ let (rollback_env : Prims.int FStar_Pervasives_Native.option -> unit) = let (init : FStar_TypeChecker_Env.env -> unit) = fun tcenv -> init_env tcenv; - FStar_SMTEncoding_Z3.init (); FStar_SMTEncoding_Z3.giveZ3 [FStar_SMTEncoding_Term.DefPrelude] let (snapshot : Prims.string -> (FStar_TypeChecker_Env.solver_depth_t * unit)) = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml index a78ec1063af..1ee1658f0f7 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml @@ -1817,35 +1817,46 @@ type solver_cfg = smtopt: Prims.string Prims.list ; facts: (Prims.string Prims.list * Prims.bool) Prims.list ; valid_intro: Prims.bool ; - valid_elim: Prims.bool } + valid_elim: Prims.bool ; + z3version: Prims.string } let (__proj__Mksolver_cfg__item__seed : solver_cfg -> Prims.int) = fun projectee -> match projectee with - | { seed; cliopt; smtopt; facts; valid_intro; valid_elim;_} -> seed + | { seed; cliopt; smtopt; facts; valid_intro; valid_elim; z3version;_} -> + seed let (__proj__Mksolver_cfg__item__cliopt : solver_cfg -> Prims.string Prims.list) = fun projectee -> match projectee with - | { seed; cliopt; smtopt; facts; valid_intro; valid_elim;_} -> cliopt + | { seed; cliopt; smtopt; facts; valid_intro; valid_elim; z3version;_} -> + cliopt let (__proj__Mksolver_cfg__item__smtopt : solver_cfg -> Prims.string Prims.list) = fun projectee -> match projectee with - | { seed; cliopt; smtopt; facts; valid_intro; valid_elim;_} -> smtopt + | { seed; cliopt; smtopt; facts; valid_intro; valid_elim; z3version;_} -> + smtopt let (__proj__Mksolver_cfg__item__facts : solver_cfg -> (Prims.string Prims.list * Prims.bool) Prims.list) = fun projectee -> match projectee with - | { seed; cliopt; smtopt; facts; valid_intro; valid_elim;_} -> facts + | { seed; cliopt; smtopt; facts; valid_intro; valid_elim; z3version;_} -> + facts let (__proj__Mksolver_cfg__item__valid_intro : solver_cfg -> Prims.bool) = fun projectee -> match projectee with - | { seed; cliopt; smtopt; facts; valid_intro; valid_elim;_} -> + | { seed; cliopt; smtopt; facts; valid_intro; valid_elim; z3version;_} -> valid_intro let (__proj__Mksolver_cfg__item__valid_elim : solver_cfg -> Prims.bool) = fun projectee -> match projectee with - | { seed; cliopt; smtopt; facts; valid_intro; valid_elim;_} -> valid_elim + | { seed; cliopt; smtopt; facts; valid_intro; valid_elim; z3version;_} -> + valid_elim +let (__proj__Mksolver_cfg__item__z3version : solver_cfg -> Prims.string) = + fun projectee -> + match projectee with + | { seed; cliopt; smtopt; facts; valid_intro; valid_elim; z3version;_} -> + z3version let (_last_cfg : solver_cfg FStar_Pervasives_Native.option FStar_Compiler_Effect.ref) = FStar_Compiler_Util.mk_ref FStar_Pervasives_Native.None @@ -1856,13 +1867,15 @@ let (get_cfg : FStar_TypeChecker_Env.env -> solver_cfg) = let uu___2 = FStar_Options.z3_smtopt () in let uu___3 = FStar_Options.smtencoding_valid_intro () in let uu___4 = FStar_Options.smtencoding_valid_elim () in + let uu___5 = FStar_Options.z3_version () in { seed = uu___; cliopt = uu___1; smtopt = uu___2; facts = (env.FStar_TypeChecker_Env.proof_ns); valid_intro = uu___3; - valid_elim = uu___4 + valid_elim = uu___4; + z3version = uu___5 } let (save_cfg : FStar_TypeChecker_Env.env -> unit) = fun env -> @@ -2154,7 +2167,7 @@ let (solver : FStar_TypeChecker_Env.solver_t) = FStar_TypeChecker_Env.handle_smt_goal = (fun e -> fun g -> [(e, g)]); FStar_TypeChecker_Env.solve = solve; FStar_TypeChecker_Env.solve_sync = solve_sync_bool; - FStar_TypeChecker_Env.finish = FStar_SMTEncoding_Z3.finish; + FStar_TypeChecker_Env.finish = (fun uu___ -> ()); FStar_TypeChecker_Env.refresh = FStar_SMTEncoding_Z3.refresh } let (dummy : FStar_TypeChecker_Env.solver_t) = diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml index bbbb969c847..7316ca55f1f 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Z3.ml @@ -109,81 +109,47 @@ let (__proj__Mkquery_log__item__close_log : query_log -> unit -> unit) = match projectee with | { get_module_name; set_module_name; write_to_log; append_to_log; close_log;_} -> close_log -let (_z3version_checked : Prims.bool FStar_Compiler_Effect.ref) = - FStar_Compiler_Util.mk_ref false -let (_z3version_expected : Prims.string) = "Z3 version 4.8.5" -let (_z3url : Prims.string) = - "https://github.com/FStarLang/binaries/tree/master/z3-tested" -let (parse_z3_version_lines : - Prims.string -> Prims.string FStar_Pervasives_Native.option) = - fun out -> - match FStar_Compiler_Util.splitlines out with - | version::uu___ -> - if FStar_Compiler_Util.starts_with version _z3version_expected - then - ((let uu___2 = FStar_Options.debug_any () in - if uu___2 - then - let uu___3 = - FStar_Compiler_Util.format1 - "Successfully found expected Z3 version %s\n" version in - FStar_Compiler_Util.print_string uu___3 - else ()); - FStar_Pervasives_Native.None) - else - (let msg = - FStar_Compiler_Util.format2 - "Expected Z3 version \"%s\", got \"%s\"" _z3version_expected - (FStar_Compiler_Util.trim_string out) in - FStar_Pervasives_Native.Some msg) - | uu___ -> FStar_Pervasives_Native.Some "No Z3 version string found" -let (z3version_warning_message : - unit -> - (FStar_Errors_Codes.raw_error * Prims.string) - FStar_Pervasives_Native.option) - = - fun uu___ -> - let run_proc_result = - try - (fun uu___1 -> - match () with - | () -> - let uu___2 = - let uu___3 = FStar_Options.z3_exe () in - FStar_Compiler_Util.run_process "z3_version" uu___3 - ["-version"] FStar_Pervasives_Native.None in - FStar_Pervasives_Native.Some uu___2) () - with | uu___1 -> FStar_Pervasives_Native.None in - match run_proc_result with +let (_already_warned_solver_mismatch : Prims.bool FStar_Compiler_Effect.ref) + = FStar_Compiler_Util.mk_ref false +let (_already_warned_version_mismatch : Prims.bool FStar_Compiler_Effect.ref) + = FStar_Compiler_Util.mk_ref false +let (z3url : Prims.string) = "https://github.com/Z3Prover/z3/releases" +let (inpath : Prims.string -> Prims.bool) = + fun path -> + try + (fun uu___ -> + match () with + | () -> + let s = + FStar_Compiler_Util.run_process "z3_pathtest" path + ["-version"] FStar_Pervasives_Native.None in + s <> "") () + with | uu___ -> false +let (z3_exe : unit -> Prims.string) = + let cache = FStar_Compiler_Util.smap_create (Prims.of_int (5)) in + let find_or k f = + let uu___ = FStar_Compiler_Util.smap_try_find cache k in + match uu___ with + | FStar_Pervasives_Native.Some v -> v | FStar_Pervasives_Native.None -> - FStar_Pervasives_Native.Some - (FStar_Errors_Codes.Error_Z3InvocationError, "Could not run Z3") - | FStar_Pervasives_Native.Some out -> - let uu___1 = parse_z3_version_lines out in - (match uu___1 with - | FStar_Pervasives_Native.None -> FStar_Pervasives_Native.None - | FStar_Pervasives_Native.Some msg -> - FStar_Pervasives_Native.Some - (FStar_Errors_Codes.Warning_Z3InvocationWarning, msg)) -let (check_z3version : unit -> unit) = + let v = f k in (FStar_Compiler_Util.smap_add cache k v; v) in fun uu___ -> - let uu___1 = - let uu___2 = FStar_Compiler_Effect.op_Bang _z3version_checked in - Prims.op_Negation uu___2 in - if uu___1 - then - (FStar_Compiler_Effect.op_Colon_Equals _z3version_checked true; - (let uu___3 = z3version_warning_message () in - match uu___3 with - | FStar_Pervasives_Native.None -> () - | FStar_Pervasives_Native.Some (e, msg) -> - let msg1 = - FStar_Compiler_Util.format4 "%s\n%s\n%s\n%s" msg - "Please download the version of Z3 corresponding to your platform from:" - _z3url "and add the bin/ subdirectory into your PATH" in - FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange - (e, msg1))) - else () + let uu___1 = FStar_Options.z3_version () in + find_or uu___1 + (fun version -> + let path = + let z3_v = FStar_Platform.exe (Prims.op_Hat "z3-" version) in + let smto = FStar_Options.smt () in + if FStar_Pervasives_Native.uu___is_Some smto + then FStar_Pervasives_Native.__proj__Some__item__v smto + else + (let uu___3 = inpath z3_v in + if uu___3 then z3_v else FStar_Platform.exe "z3") in + (let uu___3 = FStar_Options.debug_any () in + if uu___3 + then FStar_Compiler_Util.print1 "Chosen Z3 executable: %s\n" path + else ()); + path) type label = Prims.string let (status_tag : z3status -> Prims.string) = fun uu___ -> @@ -301,7 +267,7 @@ let (query_logging : query_log) = } let (z3_cmd_and_args : unit -> (Prims.string * Prims.string Prims.list)) = fun uu___ -> - let cmd = FStar_Options.z3_exe () in + let cmd = z3_exe () in let cmd_args = let uu___1 = let uu___2 = @@ -317,21 +283,91 @@ let (z3_cmd_and_args : unit -> (Prims.string * Prims.string Prims.list)) = let uu___2 = FStar_Options.z3_cliopt () in FStar_Compiler_List.append uu___1 uu___2 in (cmd, cmd_args) +let (warn_handler : Prims.string -> unit) = + fun s -> + FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange + (FStar_Errors_Codes.Warning_UnexpectedZ3Output, + (Prims.op_Hat "Unexpected output from Z3: \"" (Prims.op_Hat s "\""))) +let (check_z3version : FStar_Compiler_Util.proc -> unit) = + fun p -> + let getinfo arg = + let s = + let uu___ = + FStar_Compiler_Util.format1 "(get-info :%s)\n(echo \"Done!\")\n" + arg in + FStar_Compiler_Util.ask_process p uu___ (fun uu___1 -> "Killed") + warn_handler in + if FStar_Compiler_Util.starts_with s (Prims.op_Hat "(:" arg) + then + let ss = FStar_String.split [34] s in + FStar_Compiler_List.nth ss Prims.int_one + else + (warn_handler s; + (let uu___2 = + let uu___3 = + let uu___4 = FStar_Compiler_Util.proc_prog p in + FStar_Compiler_Util.format1 "Could not run Z3 from `%s'" uu___4 in + (FStar_Errors_Codes.Error_Z3InvocationError, uu___3) in + FStar_Errors.raise_err uu___2)) in + let name = getinfo "name" in + (let uu___1 = + (name <> "Z3") && + (let uu___2 = + FStar_Compiler_Effect.op_Bang _already_warned_solver_mismatch in + Prims.op_Negation uu___2) in + if uu___1 + then + ((let uu___3 = + let uu___4 = + let uu___5 = + let uu___6 = + let uu___7 = FStar_Options.z3_version () in + Prims.op_Hat "z3-" uu___7 in + FStar_Platform.exe uu___6 in + FStar_Compiler_Util.format3 + "Unexpected SMT solver: expected to be talking to Z3, got %s.\nPlease download the correct version of Z3 from %s\nand install it into your $PATH as `%s'." + name z3url uu___5 in + (FStar_Errors_Codes.Warning_SolverMismatch, uu___4) in + FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange uu___3); + FStar_Compiler_Effect.op_Colon_Equals _already_warned_solver_mismatch + true) + else ()); + (let ver = getinfo "version" in + let uu___2 = + (let uu___3 = FStar_Options.z3_version () in ver <> uu___3) && + (let uu___3 = + FStar_Compiler_Effect.op_Bang _already_warned_version_mismatch in + Prims.op_Negation uu___3) in + if uu___2 + then + ((let uu___4 = + let uu___5 = + let uu___6 = FStar_Compiler_Util.proc_prog p in + let uu___7 = FStar_Options.z3_version () in + let uu___8 = + let uu___9 = + let uu___10 = FStar_Options.z3_version () in + Prims.op_Hat "z3-" uu___10 in + FStar_Platform.exe uu___9 in + FStar_Compiler_Util.format5 + "Unexpected Z3 version for `%s': expected %s, got %s.\nPlease download the correct version of Z3 from %s\nand install it into your $PATH as `%s'." + uu___6 uu___7 ver z3url uu___8 in + (FStar_Errors_Codes.Warning_SolverMismatch, uu___5) in + FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange uu___4); + FStar_Compiler_Effect.op_Colon_Equals + _already_warned_version_mismatch true) + else ()) let (new_z3proc : Prims.string -> (Prims.string * Prims.string Prims.list) -> FStar_Compiler_Util.proc) = fun id -> fun cmd_and_args -> - check_z3version (); - FStar_Compiler_Util.start_process id - (FStar_Pervasives_Native.fst cmd_and_args) - (FStar_Pervasives_Native.snd cmd_and_args) (fun s -> s = "Done!") -let (warn_handler : Prims.string -> unit) = - fun s -> - FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange - (FStar_Errors_Codes.Warning_UnexpectedZ3Output, - (Prims.op_Hat "Unexpected output from Z3: \"" (Prims.op_Hat s "\""))) + let proc = + FStar_Compiler_Util.start_process id + (FStar_Pervasives_Native.fst cmd_and_args) + (FStar_Pervasives_Native.snd cmd_and_args) (fun s -> s = "Done!") in + check_z3version proc; proc let (new_z3proc_with_id : (Prims.string * Prims.string Prims.list) -> FStar_Compiler_Util.proc) = let ctr = FStar_Compiler_Util.mk_ref (~- Prims.int_one) in @@ -343,19 +379,9 @@ let (new_z3proc_with_id : (let uu___3 = FStar_Compiler_Effect.op_Bang ctr in FStar_Compiler_Effect.op_Bar_Greater uu___3 FStar_Compiler_Util.string_of_int) in - FStar_Compiler_Util.format1 "bg-%s" uu___1 in + FStar_Compiler_Util.format1 "z3-bg-%s" uu___1 in new_z3proc uu___ cmd_and_args in - let reply = - FStar_Compiler_Util.ask_process p "(echo \"Test\")\n(echo \"Done!\")\n" - (fun uu___ -> "Killed") warn_handler in - if reply = "Test\n" - then p - else - (let uu___1 = - FStar_Compiler_Util.format1 - "Failed to start and test Z3 process, expected output \"Test\" got \"%s\"" - reply in - failwith uu___1) + p type bgproc = { ask: Prims.string -> Prims.string ; @@ -383,6 +409,7 @@ let (bg_z3_proc : bgproc FStar_Compiler_Effect.ref) = let the_z3proc_params = FStar_Compiler_Util.mk_ref (FStar_Pervasives_Native.Some ("", [""])) in let the_z3proc_ask_count = FStar_Compiler_Util.mk_ref Prims.int_zero in + let the_z3proc_version = FStar_Compiler_Util.mk_ref "" in let make_new_z3_proc cmd_and_args = (let uu___1 = let uu___2 = new_z3proc_with_id cmd_and_args in @@ -391,71 +418,76 @@ let (bg_z3_proc : bgproc FStar_Compiler_Effect.ref) = FStar_Compiler_Effect.op_Colon_Equals the_z3proc_params (FStar_Pervasives_Native.Some cmd_and_args); FStar_Compiler_Effect.op_Colon_Equals the_z3proc_ask_count Prims.int_zero in - let z3proc uu___ = - (let uu___2 = + (let uu___1 = FStar_Options.z3_version () in + FStar_Compiler_Effect.op_Colon_Equals the_z3proc_version uu___1); + (let z3proc uu___1 = + (let uu___3 = + let uu___4 = FStar_Compiler_Effect.op_Bang the_z3proc in + uu___4 = FStar_Pervasives_Native.None in + if uu___3 + then let uu___4 = z3_cmd_and_args () in make_new_z3_proc uu___4 + else ()); + (let uu___3 = FStar_Compiler_Effect.op_Bang the_z3proc in + FStar_Compiler_Util.must uu___3) in + let ask input = + FStar_Compiler_Util.incr the_z3proc_ask_count; + (let kill_handler uu___2 = "\nkilled\n" in + let uu___2 = z3proc () in + FStar_Compiler_Util.ask_process uu___2 input kill_handler warn_handler) in + let maybe_kill_z3proc uu___1 = + let uu___2 = let uu___3 = FStar_Compiler_Effect.op_Bang the_z3proc in - uu___3 = FStar_Pervasives_Native.None in - if uu___2 - then let uu___3 = z3_cmd_and_args () in make_new_z3_proc uu___3 - else ()); - (let uu___2 = FStar_Compiler_Effect.op_Bang the_z3proc in - FStar_Compiler_Util.must uu___2) in - let ask input = - FStar_Compiler_Util.incr the_z3proc_ask_count; - (let kill_handler uu___1 = "\nkilled\n" in - let uu___1 = z3proc () in - FStar_Compiler_Util.ask_process uu___1 input kill_handler warn_handler) in - let maybe_kill_z3proc uu___ = - let uu___1 = - let uu___2 = FStar_Compiler_Effect.op_Bang the_z3proc in - uu___2 <> FStar_Pervasives_Native.None in - if uu___1 - then - ((let uu___3 = - let uu___4 = FStar_Compiler_Effect.op_Bang the_z3proc in - FStar_Compiler_Util.must uu___4 in - FStar_Compiler_Util.kill_process uu___3); - FStar_Compiler_Effect.op_Colon_Equals the_z3proc - FStar_Pervasives_Native.None) - else () in - let refresh uu___ = - let next_params = z3_cmd_and_args () in - let old_params = - let uu___1 = FStar_Compiler_Effect.op_Bang the_z3proc_params in - FStar_Compiler_Util.must uu___1 in - (let uu___2 = - ((FStar_Options.log_queries ()) || - (let uu___3 = FStar_Compiler_Effect.op_Bang the_z3proc_ask_count in - uu___3 > Prims.int_zero)) - || (Prims.op_Negation (old_params = next_params)) in + uu___3 <> FStar_Pervasives_Native.None in if uu___2 then - (maybe_kill_z3proc (); - (let uu___5 = FStar_Options.query_stats () in - if uu___5 - then - let uu___6 = - let uu___7 = FStar_Compiler_Effect.op_Bang the_z3proc_ask_count in - FStar_Compiler_Util.string_of_int uu___7 in - FStar_Compiler_Util.print3 - "Refreshing the z3proc (ask_count=%s old=[%s] new=[%s]) \n" - uu___6 (cmd_and_args_to_string old_params) - (cmd_and_args_to_string next_params) - else ()); - make_new_z3_proc next_params) - else ()); - query_logging.close_log () in - let restart uu___ = - maybe_kill_z3proc (); - query_logging.close_log (); - (let next_params = z3_cmd_and_args () in make_new_z3_proc next_params) in - let x = [] in - FStar_Compiler_Util.mk_ref - { - ask = (FStar_Compiler_Util.with_monitor x ask); - refresh = (FStar_Compiler_Util.with_monitor x refresh); - restart = (FStar_Compiler_Util.with_monitor x restart) - } + ((let uu___4 = + let uu___5 = FStar_Compiler_Effect.op_Bang the_z3proc in + FStar_Compiler_Util.must uu___5 in + FStar_Compiler_Util.kill_process uu___4); + FStar_Compiler_Effect.op_Colon_Equals the_z3proc + FStar_Pervasives_Native.None) + else () in + let refresh uu___1 = + let next_params = z3_cmd_and_args () in + let old_params = + let uu___2 = FStar_Compiler_Effect.op_Bang the_z3proc_params in + FStar_Compiler_Util.must uu___2 in + let old_version = FStar_Compiler_Effect.op_Bang the_z3proc_version in + let next_version = FStar_Options.z3_version () in + (let uu___3 = + (((FStar_Options.log_queries ()) || + (let uu___4 = FStar_Compiler_Effect.op_Bang the_z3proc_ask_count in + uu___4 > Prims.int_zero)) + || (old_params <> next_params)) + || (old_version <> next_version) in + if uu___3 + then + (maybe_kill_z3proc (); + (let uu___6 = FStar_Options.query_stats () in + if uu___6 + then + let uu___7 = + let uu___8 = FStar_Compiler_Effect.op_Bang the_z3proc_ask_count in + FStar_Compiler_Util.string_of_int uu___8 in + FStar_Compiler_Util.print3 + "Refreshing the z3proc (ask_count=%s old=[%s] new=[%s])\n" + uu___7 (cmd_and_args_to_string old_params) + (cmd_and_args_to_string next_params) + else ()); + make_new_z3_proc next_params) + else ()); + query_logging.close_log () in + let restart uu___1 = + maybe_kill_z3proc (); + query_logging.close_log (); + (let next_params = z3_cmd_and_args () in make_new_z3_proc next_params) in + let x = [] in + FStar_Compiler_Util.mk_ref + { + ask = (FStar_Compiler_Util.with_monitor x ask); + refresh = (FStar_Compiler_Util.with_monitor x refresh); + restart = (FStar_Compiler_Util.with_monitor x restart) + }) type smt_output_section = Prims.string Prims.list type smt_output = { @@ -786,13 +818,19 @@ let (doZ3Exe : fun s -> let uu___2 = query_logging.append_to_log s in ()) r1; r1) -let (z3_options : Prims.string FStar_Compiler_Effect.ref) = - FStar_Compiler_Util.mk_ref - "(set-option :global-decls false)\n(set-option :smt.mbqi false)\n(set-option :auto_config false)\n(set-option :produce-unsat-cores true)\n(set-option :model true)\n(set-option :smt.case_split 3)\n(set-option :smt.relevancy 2)\n" -let (set_z3_options : Prims.string -> unit) = - fun opts -> FStar_Compiler_Effect.op_Colon_Equals z3_options opts -let (init : unit -> unit) = fun uu___ -> () -let (finish : unit -> unit) = fun uu___ -> () +let (z3_options : Prims.string -> Prims.string) = + fun ver -> + let opts = + "(set-option :global-decls false)\n(set-option :smt.mbqi false)\n(set-option :auto_config false)\n(set-option :produce-unsat-cores true)\n(set-option :model true)\n(set-option :smt.case_split 3)\n(set-option :smt.relevancy 2)\n(set-option :smt.arith.solver 2)\n" in + let opts1 = + let uu___ = + let uu___1 = FStar_Compiler_Misc.version_ge ver "4.12.3" in + if uu___1 + then + "(set-option :rewriter.enable_der false)\n(set-option :rewriter.sort_disjunctions false)\n(set-option :pi.decompose_patterns false)\n" + else "" in + Prims.op_Hat opts uu___ in + opts1 let (fresh_scope : scope_t FStar_Compiler_Effect.ref) = FStar_Compiler_Util.mk_ref [[]] let (mk_fresh_scope : unit -> scope_t) = @@ -918,7 +956,8 @@ let (mk_input : = fun fresh -> fun theory -> - let options = FStar_Compiler_Effect.op_Bang z3_options in + let options = + let uu___ = FStar_Options.z3_version () in z3_options uu___ in let options1 = let uu___ = let uu___1 = FStar_Options.z3_smtopt () in From 1bc4efff0f4170afdbfe50355daa869e60f6b600 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 24 Jul 2023 00:59:52 -0700 Subject: [PATCH 6/9] UInt128: use retry on flaky proof --- ulib/FStar.UInt128.fst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst index 205bb2eb286..f5880b68614 100644 --- a/ulib/FStar.UInt128.fst +++ b/ulib/FStar.UInt128.fst @@ -315,6 +315,8 @@ let u64_diff_wrap a b = () val sub_mod_wrap1_ok : a:t -> b:t -> Lemma (requires (v a - v b < 0 /\ U64.v a.low < U64.v b.low)) (ensures (v (sub_mod_impl a b) = v a - v b + pow2 128)) + +#push-options "--retry 10" let sub_mod_wrap1_ok a b = // carry == 1 and subtraction in low wraps let l = U64.sub_mod a.low b.low in @@ -327,6 +329,7 @@ let sub_mod_wrap1_ok a b = u64_diff_wrap a.high b.high; () end +#pop-options let sum_lt (a1 a2 b1 b2:nat) : Lemma (requires (a1 + a2 < b1 + b2 /\ a1 >= b1)) From d20c879d47e68b549a11a13f3a4d43eaf1134ea9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 24 Jul 2023 00:51:46 -0700 Subject: [PATCH 7/9] VConfig: add z3version --- src/basic/FStar.Options.fst | 1 + src/syntax/FStar.Syntax.Embeddings.fst | 6 +++++- ulib/FStar.VConfig.fsti | 1 + 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/basic/FStar.Options.fst b/src/basic/FStar.Options.fst index f746588c8d2..042fc126363 100644 --- a/src/basic/FStar.Options.fst +++ b/src/basic/FStar.Options.fst @@ -2120,6 +2120,7 @@ let get_vconfig () = z3rlimit = get_z3rlimit (); z3rlimit_factor = get_z3rlimit_factor (); z3seed = get_z3seed (); + z3version = get_z3version (); trivial_pre_for_unannotated_effectful_fns = get_trivial_pre_for_unannotated_effectful_fns (); reuse_hint_for = get_reuse_hint_for (); } diff --git a/src/syntax/FStar.Syntax.Embeddings.fst b/src/syntax/FStar.Syntax.Embeddings.fst index dd6e260e86b..702776e50be 100644 --- a/src/syntax/FStar.Syntax.Embeddings.fst +++ b/src/syntax/FStar.Syntax.Embeddings.fst @@ -783,6 +783,7 @@ let e_vconfig = S.as_arg (embed e_fsint vcfg.z3rlimit rng None norm); S.as_arg (embed e_fsint vcfg.z3rlimit_factor rng None norm); S.as_arg (embed e_fsint vcfg.z3seed rng None norm); + S.as_arg (embed e_string vcfg.z3version rng None norm); S.as_arg (embed e_bool vcfg.trivial_pre_for_unannotated_effectful_fns rng None norm); S.as_arg (embed (e_option e_string) vcfg.reuse_hint_for rng None norm); ] @@ -818,6 +819,7 @@ let e_vconfig = (z3rlimit, _); (z3rlimit_factor, _); (z3seed, _); + (z3version, _); (trivial_pre_for_unannotated_effectful_fns, _); (reuse_hint_for, _) ] when S.fv_eq_lid fv PC.mkvconfig_lid -> @@ -846,6 +848,7 @@ let e_vconfig = BU.bind_opt (try_unembed e_fsint z3rlimit norm) (fun z3rlimit -> BU.bind_opt (try_unembed e_fsint z3rlimit_factor norm) (fun z3rlimit_factor -> BU.bind_opt (try_unembed e_fsint z3seed norm) (fun z3seed -> + BU.bind_opt (try_unembed e_string z3version norm) (fun z3version -> BU.bind_opt (try_unembed e_bool trivial_pre_for_unannotated_effectful_fns norm) (fun trivial_pre_for_unannotated_effectful_fns -> BU.bind_opt (try_unembed (e_option e_string) reuse_hint_for norm) (fun reuse_hint_for -> Some ({ @@ -874,9 +877,10 @@ let e_vconfig = z3rlimit = z3rlimit; z3rlimit_factor = z3rlimit_factor; z3seed = z3seed; + z3version = z3version; trivial_pre_for_unannotated_effectful_fns = trivial_pre_for_unannotated_effectful_fns; reuse_hint_for = reuse_hint_for; - })))))))))))))))))))))))))))) + }))))))))))))))))))))))))))))) | _ -> None in diff --git a/ulib/FStar.VConfig.fsti b/ulib/FStar.VConfig.fsti index 657074a19c6..9807e31368a 100644 --- a/ulib/FStar.VConfig.fsti +++ b/ulib/FStar.VConfig.fsti @@ -47,6 +47,7 @@ type vconfig = { z3rlimit : int; z3rlimit_factor : int; z3seed : int; + z3version : string; trivial_pre_for_unannotated_effectful_fns : bool; reuse_hint_for : option string; } From 4d17e59a5c9e67b2543fa224f769447222f624a3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 24 Jul 2023 00:52:15 -0700 Subject: [PATCH 8/9] snap --- ocaml/fstar-lib/generated/FStar_Options.ml | 10 +- .../generated/FStar_Syntax_Embeddings.ml | 162 ++++++++++-------- .../fstar-lib/generated/FStar_Tactics_SMT.ml | 16 ++ .../generated/FStar_Tactics_V2_Derived.ml | 2 + ocaml/fstar-lib/generated/FStar_VConfig.ml | 66 ++++--- 5 files changed, 158 insertions(+), 98 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStar_Options.ml b/ocaml/fstar-lib/generated/FStar_Options.ml index 571e035aa9c..6aa565d95dd 100644 --- a/ocaml/fstar-lib/generated/FStar_Options.ml +++ b/ocaml/fstar-lib/generated/FStar_Options.ml @@ -2467,8 +2467,9 @@ let (get_vconfig : unit -> FStar_VConfig.vconfig) = let uu___23 = get_z3rlimit () in let uu___24 = get_z3rlimit_factor () in let uu___25 = get_z3seed () in - let uu___26 = get_trivial_pre_for_unannotated_effectful_fns () in - let uu___27 = get_reuse_hint_for () in + let uu___26 = get_z3version () in + let uu___27 = get_trivial_pre_for_unannotated_effectful_fns () in + let uu___28 = get_reuse_hint_for () in { FStar_VConfig.initial_fuel = uu___1; FStar_VConfig.max_fuel = uu___2; @@ -2495,8 +2496,9 @@ let (get_vconfig : unit -> FStar_VConfig.vconfig) = FStar_VConfig.z3rlimit = uu___23; FStar_VConfig.z3rlimit_factor = uu___24; FStar_VConfig.z3seed = uu___25; - FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = uu___26; - FStar_VConfig.reuse_hint_for = uu___27 + FStar_VConfig.z3version = uu___26; + FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = uu___27; + FStar_VConfig.reuse_hint_for = uu___28 } in vcfg let (set_vconfig : FStar_VConfig.vconfig -> unit) = diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml index 24903a55f04..de6080152ae 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml @@ -1579,8 +1579,8 @@ let (e_vconfig : let uu___53 = let uu___54 = FStar_Syntax_Embeddings_Base.embed - e_bool - vcfg.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns in + e_string + vcfg.FStar_VConfig.z3version in uu___54 rng FStar_Pervasives_Native.None norm in @@ -1590,18 +1590,32 @@ let (e_vconfig : let uu___54 = let uu___55 = let uu___56 = - let uu___57 = - e_option - e_string in FStar_Syntax_Embeddings_Base.embed - uu___57 - vcfg.FStar_VConfig.reuse_hint_for in + e_bool + vcfg.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns in uu___56 rng FStar_Pervasives_Native.None norm in FStar_Syntax_Syntax.as_arg uu___55 in - [uu___54] in + let uu___55 = + let uu___56 = + let uu___57 = + let uu___58 = + let uu___59 + = + e_option + e_string in + FStar_Syntax_Embeddings_Base.embed + uu___59 + vcfg.FStar_VConfig.reuse_hint_for in + uu___58 rng + FStar_Pervasives_Native.None + norm in + FStar_Syntax_Syntax.as_arg + uu___57 in + [uu___56] in + uu___54 :: uu___55 in uu___52 :: uu___53 in uu___50 :: uu___51 in uu___48 :: uu___49 in @@ -1655,254 +1669,265 @@ let (e_vconfig : (z3cliopt, uu___21)::(z3smtopt, uu___22)::(z3refresh, uu___23):: (z3rlimit, uu___24)::(z3rlimit_factor, uu___25)::(z3seed, uu___26):: - (trivial_pre_for_unannotated_effectful_fns, uu___27)::(reuse_hint_for, - uu___28)::[]) + (z3version, uu___27)::(trivial_pre_for_unannotated_effectful_fns, + uu___28)::(reuse_hint_for, uu___29)::[]) when FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.mkvconfig_lid -> - let uu___29 = + let uu___30 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint initial_fuel norm in - FStar_Compiler_Util.bind_opt uu___29 + FStar_Compiler_Util.bind_opt uu___30 (fun initial_fuel1 -> - let uu___30 = + let uu___31 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint max_fuel norm in - FStar_Compiler_Util.bind_opt uu___30 + FStar_Compiler_Util.bind_opt uu___31 (fun max_fuel1 -> - let uu___31 = + let uu___32 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint initial_ifuel norm in - FStar_Compiler_Util.bind_opt uu___31 + FStar_Compiler_Util.bind_opt uu___32 (fun initial_ifuel1 -> - let uu___32 = + let uu___33 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint max_ifuel norm in - FStar_Compiler_Util.bind_opt uu___32 + FStar_Compiler_Util.bind_opt uu___33 (fun max_ifuel1 -> - let uu___33 = + let uu___34 = FStar_Syntax_Embeddings_Base.try_unembed e_bool detail_errors norm in - FStar_Compiler_Util.bind_opt uu___33 + FStar_Compiler_Util.bind_opt uu___34 (fun detail_errors1 -> - let uu___34 = + let uu___35 = FStar_Syntax_Embeddings_Base.try_unembed e_bool detail_hint_replay norm in - FStar_Compiler_Util.bind_opt uu___34 + FStar_Compiler_Util.bind_opt uu___35 (fun detail_hint_replay1 -> - let uu___35 = + let uu___36 = FStar_Syntax_Embeddings_Base.try_unembed e_bool no_smt norm in FStar_Compiler_Util.bind_opt - uu___35 + uu___36 (fun no_smt1 -> - let uu___36 = + let uu___37 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint quake_lo norm in FStar_Compiler_Util.bind_opt - uu___36 + uu___37 (fun quake_lo1 -> - let uu___37 = + let uu___38 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint quake_hi norm in FStar_Compiler_Util.bind_opt - uu___37 + uu___38 (fun quake_hi1 -> - let uu___38 = + let uu___39 = FStar_Syntax_Embeddings_Base.try_unembed e_bool quake_keep norm in FStar_Compiler_Util.bind_opt - uu___38 + uu___39 (fun quake_keep1 -> - let uu___39 = + let uu___40 = FStar_Syntax_Embeddings_Base.try_unembed e_bool retry norm in FStar_Compiler_Util.bind_opt - uu___39 + uu___40 (fun retry1 -> - let uu___40 + let uu___41 = FStar_Syntax_Embeddings_Base.try_unembed e_bool smtencoding_elim_box norm in FStar_Compiler_Util.bind_opt - uu___40 + uu___41 (fun smtencoding_elim_box1 -> - let uu___41 + let uu___42 = FStar_Syntax_Embeddings_Base.try_unembed e_string smtencoding_nl_arith_repr norm in FStar_Compiler_Util.bind_opt - uu___41 + uu___42 (fun smtencoding_nl_arith_repr1 -> - let uu___42 + let uu___43 = FStar_Syntax_Embeddings_Base.try_unembed e_string smtencoding_l_arith_repr norm in FStar_Compiler_Util.bind_opt - uu___42 + uu___43 (fun smtencoding_l_arith_repr1 -> - let uu___43 + let uu___44 = FStar_Syntax_Embeddings_Base.try_unembed e_bool smtencoding_valid_intro norm in FStar_Compiler_Util.bind_opt - uu___43 + uu___44 (fun smtencoding_valid_intro1 -> - let uu___44 + let uu___45 = FStar_Syntax_Embeddings_Base.try_unembed e_bool smtencoding_valid_elim norm in FStar_Compiler_Util.bind_opt - uu___44 + uu___45 (fun smtencoding_valid_elim1 -> - let uu___45 + let uu___46 = FStar_Syntax_Embeddings_Base.try_unembed e_bool tcnorm norm in FStar_Compiler_Util.bind_opt - uu___45 + uu___46 (fun tcnorm1 -> - let uu___46 + let uu___47 = FStar_Syntax_Embeddings_Base.try_unembed e_bool no_plugins norm in FStar_Compiler_Util.bind_opt - uu___46 + uu___47 (fun no_plugins1 -> - let uu___47 + let uu___48 = FStar_Syntax_Embeddings_Base.try_unembed e_bool no_tactics norm in FStar_Compiler_Util.bind_opt - uu___47 + uu___48 (fun no_tactics1 -> - let uu___48 + let uu___49 = FStar_Syntax_Embeddings_Base.try_unembed e_string_list z3cliopt norm in FStar_Compiler_Util.bind_opt - uu___48 + uu___49 (fun z3cliopt1 -> - let uu___49 + let uu___50 = FStar_Syntax_Embeddings_Base.try_unembed e_string_list z3smtopt norm in FStar_Compiler_Util.bind_opt - uu___49 + uu___50 (fun z3smtopt1 -> - let uu___50 + let uu___51 = FStar_Syntax_Embeddings_Base.try_unembed e_bool z3refresh norm in FStar_Compiler_Util.bind_opt - uu___50 + uu___51 (fun z3refresh1 -> - let uu___51 + let uu___52 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint z3rlimit norm in FStar_Compiler_Util.bind_opt - uu___51 + uu___52 (fun z3rlimit1 -> - let uu___52 + let uu___53 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint z3rlimit_factor norm in FStar_Compiler_Util.bind_opt - uu___52 + uu___53 (fun z3rlimit_factor1 -> - let uu___53 + let uu___54 = FStar_Syntax_Embeddings_Base.try_unembed e_fsint z3seed norm in FStar_Compiler_Util.bind_opt - uu___53 + uu___54 (fun z3seed1 -> - let uu___54 + let uu___55 + = + FStar_Syntax_Embeddings_Base.try_unembed + e_string + z3version + norm in + FStar_Compiler_Util.bind_opt + uu___55 + (fun + z3version1 + -> + let uu___56 = FStar_Syntax_Embeddings_Base.try_unembed e_bool trivial_pre_for_unannotated_effectful_fns norm in FStar_Compiler_Util.bind_opt - uu___54 + uu___56 (fun trivial_pre_for_unannotated_effectful_fns1 -> - let uu___55 + let uu___57 = - let uu___56 + let uu___58 = e_option e_string in FStar_Syntax_Embeddings_Base.try_unembed - uu___56 + uu___58 reuse_hint_for norm in FStar_Compiler_Util.bind_opt - uu___55 + uu___57 (fun reuse_hint_for1 -> @@ -1979,13 +2004,16 @@ let (e_vconfig : z3rlimit_factor1; FStar_VConfig.z3seed = z3seed1; + FStar_VConfig.z3version + = + z3version1; FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = trivial_pre_for_unannotated_effectful_fns1; FStar_VConfig.reuse_hint_for = reuse_hint_for1 - }))))))))))))))))))))))))))) + })))))))))))))))))))))))))))) | uu___2 -> FStar_Pervasives_Native.None) in let uu___ = let uu___1 = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_SMT.ml b/ocaml/fstar-lib/generated/FStar_Tactics_SMT.ml index 4e9d25afdea..97e0efacb3c 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_SMT.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_SMT.ml @@ -89,6 +89,8 @@ let (smt_sync' : FStar_VConfig.z3rlimit_factor = (vcfg.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (vcfg.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (vcfg.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (vcfg.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); @@ -183,6 +185,8 @@ let (set_rlimit : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = FStar_VConfig.z3rlimit_factor = (uu___.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (uu___.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (uu___.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (uu___.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); @@ -324,6 +328,8 @@ let (set_initial_fuel : FStar_VConfig.z3rlimit_factor = (uu___.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (uu___.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (uu___.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (uu___.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); @@ -401,6 +407,8 @@ let (set_initial_ifuel : FStar_VConfig.z3rlimit_factor = (uu___.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (uu___.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (uu___.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (uu___.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); @@ -479,6 +487,8 @@ let (set_max_fuel : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) FStar_VConfig.z3rlimit_factor = (uu___.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (uu___.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (uu___.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (uu___.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); @@ -556,6 +566,8 @@ let (set_max_ifuel : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) FStar_VConfig.z3rlimit_factor = (uu___.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (uu___.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (uu___.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (uu___.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); @@ -632,6 +644,8 @@ let (set_fuel : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = FStar_VConfig.z3rlimit_factor = (uu___.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (uu___.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (uu___.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (uu___.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); @@ -707,6 +721,8 @@ let (set_ifuel : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = FStar_VConfig.z3rlimit_factor = (uu___.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (uu___.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (uu___.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (uu___.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml index 66a19686c78..c0e4d4eea6a 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml @@ -5316,6 +5316,8 @@ let (smt_sync' : FStar_VConfig.z3rlimit_factor = (vcfg.FStar_VConfig.z3rlimit_factor); FStar_VConfig.z3seed = (vcfg.FStar_VConfig.z3seed); + FStar_VConfig.z3version = + (vcfg.FStar_VConfig.z3version); FStar_VConfig.trivial_pre_for_unannotated_effectful_fns = (vcfg.FStar_VConfig.trivial_pre_for_unannotated_effectful_fns); diff --git a/ocaml/fstar-lib/generated/FStar_VConfig.ml b/ocaml/fstar-lib/generated/FStar_VConfig.ml index 5c3fb1dd54b..b6152e4af20 100644 --- a/ocaml/fstar-lib/generated/FStar_VConfig.ml +++ b/ocaml/fstar-lib/generated/FStar_VConfig.ml @@ -26,6 +26,7 @@ type vconfig = z3rlimit: Prims.int ; z3rlimit_factor: Prims.int ; z3seed: Prims.int ; + z3version: Prims.string ; trivial_pre_for_unannotated_effectful_fns: Prims.bool ; reuse_hint_for: Prims.string FStar_Pervasives_Native.option } let (__proj__Mkvconfig__item__initial_fuel : vconfig -> Prims.int) = @@ -36,7 +37,7 @@ let (__proj__Mkvconfig__item__initial_fuel : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> initial_fuel let (__proj__Mkvconfig__item__max_fuel : vconfig -> Prims.int) = @@ -47,7 +48,7 @@ let (__proj__Mkvconfig__item__max_fuel : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> max_fuel let (__proj__Mkvconfig__item__initial_ifuel : vconfig -> Prims.int) = @@ -58,7 +59,7 @@ let (__proj__Mkvconfig__item__initial_ifuel : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> initial_ifuel let (__proj__Mkvconfig__item__max_ifuel : vconfig -> Prims.int) = @@ -69,7 +70,7 @@ let (__proj__Mkvconfig__item__max_ifuel : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> max_ifuel let (__proj__Mkvconfig__item__detail_errors : vconfig -> Prims.bool) = @@ -80,7 +81,7 @@ let (__proj__Mkvconfig__item__detail_errors : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> detail_errors let (__proj__Mkvconfig__item__detail_hint_replay : vconfig -> Prims.bool) = @@ -91,7 +92,7 @@ let (__proj__Mkvconfig__item__detail_hint_replay : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> detail_hint_replay let (__proj__Mkvconfig__item__no_smt : vconfig -> Prims.bool) = @@ -102,7 +103,7 @@ let (__proj__Mkvconfig__item__no_smt : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> no_smt let (__proj__Mkvconfig__item__quake_lo : vconfig -> Prims.int) = @@ -113,7 +114,7 @@ let (__proj__Mkvconfig__item__quake_lo : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> quake_lo let (__proj__Mkvconfig__item__quake_hi : vconfig -> Prims.int) = @@ -124,7 +125,7 @@ let (__proj__Mkvconfig__item__quake_hi : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> quake_hi let (__proj__Mkvconfig__item__quake_keep : vconfig -> Prims.bool) = @@ -135,7 +136,7 @@ let (__proj__Mkvconfig__item__quake_keep : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> quake_keep let (__proj__Mkvconfig__item__retry : vconfig -> Prims.bool) = @@ -146,7 +147,7 @@ let (__proj__Mkvconfig__item__retry : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> retry let (__proj__Mkvconfig__item__smtencoding_elim_box : vconfig -> Prims.bool) = fun projectee -> @@ -156,7 +157,7 @@ let (__proj__Mkvconfig__item__smtencoding_elim_box : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> smtencoding_elim_box let (__proj__Mkvconfig__item__smtencoding_nl_arith_repr : @@ -168,7 +169,7 @@ let (__proj__Mkvconfig__item__smtencoding_nl_arith_repr : smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> smtencoding_nl_arith_repr let (__proj__Mkvconfig__item__smtencoding_l_arith_repr : @@ -180,7 +181,7 @@ let (__proj__Mkvconfig__item__smtencoding_l_arith_repr : smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> smtencoding_l_arith_repr let (__proj__Mkvconfig__item__smtencoding_valid_intro : @@ -192,7 +193,7 @@ let (__proj__Mkvconfig__item__smtencoding_valid_intro : smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> smtencoding_valid_intro let (__proj__Mkvconfig__item__smtencoding_valid_elim : vconfig -> Prims.bool) @@ -204,7 +205,7 @@ let (__proj__Mkvconfig__item__smtencoding_valid_elim : vconfig -> Prims.bool) smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> smtencoding_valid_elim let (__proj__Mkvconfig__item__tcnorm : vconfig -> Prims.bool) = @@ -215,7 +216,7 @@ let (__proj__Mkvconfig__item__tcnorm : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> tcnorm let (__proj__Mkvconfig__item__no_plugins : vconfig -> Prims.bool) = @@ -226,7 +227,7 @@ let (__proj__Mkvconfig__item__no_plugins : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> no_plugins let (__proj__Mkvconfig__item__no_tactics : vconfig -> Prims.bool) = @@ -237,7 +238,7 @@ let (__proj__Mkvconfig__item__no_tactics : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> no_tactics let (__proj__Mkvconfig__item__z3cliopt : vconfig -> Prims.string Prims.list) @@ -249,7 +250,7 @@ let (__proj__Mkvconfig__item__z3cliopt : vconfig -> Prims.string Prims.list) smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> z3cliopt let (__proj__Mkvconfig__item__z3smtopt : vconfig -> Prims.string Prims.list) @@ -261,7 +262,7 @@ let (__proj__Mkvconfig__item__z3smtopt : vconfig -> Prims.string Prims.list) smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> z3smtopt let (__proj__Mkvconfig__item__z3refresh : vconfig -> Prims.bool) = @@ -272,7 +273,7 @@ let (__proj__Mkvconfig__item__z3refresh : vconfig -> Prims.bool) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> z3refresh let (__proj__Mkvconfig__item__z3rlimit : vconfig -> Prims.int) = @@ -283,7 +284,7 @@ let (__proj__Mkvconfig__item__z3rlimit : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> z3rlimit let (__proj__Mkvconfig__item__z3rlimit_factor : vconfig -> Prims.int) = @@ -294,7 +295,7 @@ let (__proj__Mkvconfig__item__z3rlimit_factor : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> z3rlimit_factor let (__proj__Mkvconfig__item__z3seed : vconfig -> Prims.int) = @@ -305,9 +306,20 @@ let (__proj__Mkvconfig__item__z3seed : vconfig -> Prims.int) = smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> z3seed +let (__proj__Mkvconfig__item__z3version : vconfig -> Prims.string) = + fun projectee -> + match projectee with + | { initial_fuel; max_fuel; initial_ifuel; max_ifuel; detail_errors; + detail_hint_replay; no_smt; quake_lo; quake_hi; quake_keep; retry; + smtencoding_elim_box; smtencoding_nl_arith_repr; + smtencoding_l_arith_repr; smtencoding_valid_intro; + smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; + trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> + z3version let (__proj__Mkvconfig__item__trivial_pre_for_unannotated_effectful_fns : vconfig -> Prims.bool) = fun projectee -> @@ -317,7 +329,7 @@ let (__proj__Mkvconfig__item__trivial_pre_for_unannotated_effectful_fns : smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> trivial_pre_for_unannotated_effectful_fns let (__proj__Mkvconfig__item__reuse_hint_for : @@ -329,6 +341,6 @@ let (__proj__Mkvconfig__item__reuse_hint_for : smtencoding_elim_box; smtencoding_nl_arith_repr; smtencoding_l_arith_repr; smtencoding_valid_intro; smtencoding_valid_elim; tcnorm; no_plugins; no_tactics; z3cliopt; - z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; + z3smtopt; z3refresh; z3rlimit; z3rlimit_factor; z3seed; z3version; trivial_pre_for_unannotated_effectful_fns; reuse_hint_for;_} -> reuse_hint_for \ No newline at end of file From 9a574dbcc5ecfa6721ad08dde6c4616ae071a956 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 21 Jun 2023 23:42:17 -0700 Subject: [PATCH 9/9] UInt128: stabilize --- ulib/FStar.UInt128.fst | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst index f5880b68614..f34cddeec37 100644 --- a/ulib/FStar.UInt128.fst +++ b/ulib/FStar.UInt128.fst @@ -282,12 +282,14 @@ let add_mod (a b: t) : Pure t r #pop-options +#push-options "--retry 5" let sub (a b: t) : Pure t (requires (v a - v b >= 0)) (ensures (fun r -> v r = v a - v b)) = let l = U64.sub_mod a.low b.low in { low = l; high = U64.sub (U64.sub a.high b.high) (carry a.low l); } +#pop-options let sub_underspec (a b: t) = let l = U64.sub_mod a.low b.low in @@ -312,6 +314,7 @@ val u64_diff_wrap : a:U64.t -> b:U64.t -> (ensures (U64.v (U64.sub_mod a b) == U64.v a - U64.v b + pow2 64)) let u64_diff_wrap a b = () +#push-options "--z3rlimit 20" val sub_mod_wrap1_ok : a:t -> b:t -> Lemma (requires (v a - v b < 0 /\ U64.v a.low < U64.v b.low)) (ensures (v (sub_mod_impl a b) = v a - v b + pow2 128)) @@ -670,6 +673,7 @@ let shift_t_mod_val (a: t) (s: nat{s < 64}) : Math.paren_mul_right a_h (pow2 64) (pow2 s); () +#push-options "--z3rlimit 20" let shift_left_small (a: t) (s: U32.t) : Pure t (requires (U32.v s < 64)) (ensures (fun r -> v r = (v a * pow2 (U32.v s)) % pow2 128)) = @@ -683,6 +687,7 @@ let shift_left_small (a: t) (s: U32.t) : Pure t mod_spec_rew_n (a_l * pow2 s) (pow2 64); shift_t_mod_val a s; r +#pop-options val shift_left_large : a:t -> s:U32.t{U32.v s >= 64 /\ U32.v s < 128} -> r:t{v r = (v a * pow2 (U32.v s)) % pow2 128} @@ -908,10 +913,12 @@ let mul32_digits x y = () let u32_32 : x:U32.t{U32.v x == 32} = U32.uint_to_t 32 +#push-options "--z3rlimit 30" let u32_combine (hi lo: U64.t) : Pure U64.t (requires (U64.v lo < pow2 32)) (ensures (fun r -> U64.v r = U64.v hi % pow2 32 * pow2 32 + U64.v lo)) = U64.add lo (U64.shift_left hi u32_32) +#pop-options let product_bound (a b:nat) (k:pos) : Lemma (requires (a < k /\ b < k)) @@ -1049,6 +1056,7 @@ let product_sums (a b c d:nat) : val u64_32_product (xl xh yl yh:UInt.uint_t 32) : Lemma ((xl + xh * pow2 32) * (yl + yh * pow2 32) == xl * yl + (xl * yh) * pow2 32 + (xh * yl) * pow2 32 + (xh * yh) * pow2 64) +#push-options "--z3rlimit 25" let u64_32_product xl xh yl yh = assert (xh >= 0); //flakiness; without this, can't prove that (xh * pow2 32) >= 0 assert (pow2 32 >= 0); //flakiness; without this, can't prove that (xh * pow2 32) >= 0 @@ -1058,6 +1066,7 @@ let u64_32_product xl xh yl yh = assert (xl * (yh * pow2 32) == (xl * yh) * pow2 32); Math.pow2_plus 32 32; assert ((xh * pow2 32) * (yh * pow2 32) == (xh * yh) * pow2 64) +#pop-options let product_expand (x y: U64.t) : Lemma (U64.v x * U64.v y == phh x y * pow2 64 + @@ -1096,9 +1105,9 @@ let mul_wide_low_ok (x y: U64.t) : assert (mul_wide_low x y == ((plh x y + phl x y + pll_h x y) * pow2 32 + pll_l x y) % pow2 64); product_low_expand x y -#push-options "--z3rlimit 10" val product_high32 : x:U64.t -> y:U64.t -> Lemma ((U64.v x * U64.v y) / pow2 32 == phh x y * pow2 32 + plh x y + phl x y + pll_h x y) +#push-options "--z3rlimit 20" let product_high32 x y = Math.pow2_plus 32 32; product_expand x y; @@ -1155,6 +1164,7 @@ let sub_mod_gt_0 (n:nat) (k:pos) : val sum_rounded_mod_exact : n:nat -> m:nat -> k:pos -> Lemma (((n - n%k) + (m - m%k)) / k * k == (n - n%k) + (m - m%k)) +#push-options "--retry 5" // sporadically fails let sum_rounded_mod_exact n m k = n_minus_mod_exact n k; n_minus_mod_exact m k; @@ -1162,6 +1172,7 @@ let sum_rounded_mod_exact n m k = sub_mod_gt_0 m k; mod_add (n - n%k) (m - m%k) k; Math.div_exact_r ((n - n%k) + (m - m % k)) k +#pop-options val div_sum_combine : n:nat -> m:nat -> k:pos -> Lemma (n / k + m / k == (n + (m - n % k) - m % k) / k)