From e8a4d17623b4b2c0755c2b28595df7732fe806f4 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 20 Dec 2022 14:11:40 -0800 Subject: [PATCH] Improve Z3 detection * Be more explicit about the path of the executable to invoke. * Identify the version and set different Z3 options accordingly. Fixes #2370 Enables a fix for #1477 Interacts with #1914 (which may already be fixed) --- Source/DafnyCore/DafnyOptions.cs | 91 ++++++++++++++++--- .../DafnyLanguageServer.cs | 28 ++---- 2 files changed, 83 insertions(+), 36 deletions(-) diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 189be194719..46fcb91eb61 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -7,6 +7,7 @@ using System.CommandLine; using System.CommandLine.Binding; using System.CommandLine.Parsing; +using System.Diagnostics; using System.Linq; using System.Diagnostics.Contracts; using System.IO; @@ -816,8 +817,10 @@ public void ApplyDefaultOptionsWithoutSettingsDefault() { // expand macros in filenames, now that LogPrefix is fully determined - SetZ3ExecutablePath(); - SetZ3Options(); + if (!ProverOptions.Any(x => x.StartsWith("SOLVER=") && !x.EndsWith("=z3"))) { + var z3Version = SetZ3ExecutablePath(); + SetZ3Options(z3Version); + } // Ask Boogie to perform abstract interpretation UseAbstractInterpretation = true; @@ -1060,35 +1063,89 @@ in such cases in the verifier being faster. /// /// Dafny releases come with their own copy of Z3, to save users the trouble of having to install extra dependencies. - /// For this to work, Dafny looks for Z3 at the location where it is put by our release script (i.e., z3/bin/z3[.exe]). - /// If Z3 is not found there, Dafny relies on Boogie to locate Z3 (which also supports setting a path explicitly on the command line). - /// Developers (and people getting Dafny from source) need to install an appropriate version of Z3 themselves. + /// For this to work, Dafny first tries any prover path explicitly provided by the user, then looks for for the copy + /// distributed with Dafny, and finally looks in any directory in the system PATH environment variable. /// - private void SetZ3ExecutablePath() { + private Version SetZ3ExecutablePath() { + string confirmedProverPath = null; + + // Try an explicitly provided prover path, if there is one. var pp = "PROVER_PATH="; var proverPathOption = ProverOptions.Find(o => o.StartsWith(pp)); if (proverPathOption != null) { var proverPath = proverPathOption.Substring(pp.Length); // Boogie will perform the ultimate test to see if "proverPath" is real--it will attempt to run it. // However, by at least checking if the file exists, we can produce a better error message in common scenarios. + // Unfortunately, there doesn't seem to be a portable way of checking whether it's executable. if (!File.Exists(proverPath)) { throw new Bpl.ProverException($"Requested prover not found: '{proverPath}'"); } - } else { - var platform = (int)System.Environment.OSVersion.Platform; - var isUnix = platform == 4 || platform == 6 || platform == 128; + confirmedProverPath = proverPath; + } - var z3binName = isUnix ? "z3" : "z3.exe"; + var platform = System.Environment.OSVersion.Platform; + var isUnix = platform == PlatformID.Unix || platform == PlatformID.MacOSX || (int)platform == 128; + var z3binName = isUnix ? "z3" : "z3.exe"; + + // Next, try looking in a directory relative to Dafny itself. + if (confirmedProverPath is null) { var dafnyBinDir = Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location); var z3BinDir = Path.Combine(dafnyBinDir, "z3", "bin"); var z3BinPath = Path.Combine(z3BinDir, z3binName); if (File.Exists(z3BinPath)) { - // Let's use z3BinPath - ProverOptions.Add($"{pp}{z3BinPath}"); + confirmedProverPath = z3BinPath; } } + + // Finally, try looking in the system PATH variable. + if (confirmedProverPath is null) { + var z3InPATH = System.Environment + .GetEnvironmentVariable("PATH")! + .Split(isUnix ? ':' : ';') + .Select(s => Path.Combine(s, z3binName)) + .FirstOrDefault(File.Exists); + if (z3InPATH is not null) { + confirmedProverPath = z3InPATH; + } + } + + if (confirmedProverPath is not null) { + ProverOptions.Add($"{pp}{confirmedProverPath}"); + return GetZ3Version(confirmedProverPath); + } + + throw new Bpl.ProverException("Z3 not found in Dafny distribution or PATH environment variable."); + } + + private static readonly Regex Z3VersionRegex = new Regex(@"Z3 version (?\d+)\.(?\d+)\.(?\d+)"); + + [CanBeNull] + public static Version GetZ3Version(string proverPath) { + var z3Process = new ProcessStartInfo(proverPath, "-version") { + CreateNoWindow = true, + RedirectStandardError = true, + RedirectStandardOutput = true, + RedirectStandardInput = true + }; + var run = Process.Start(z3Process); + if (run == null) { + return null; + } + + var actualOutput = run.StandardOutput.ReadToEnd(); + run.WaitForExit(); + var versionMatch = Z3VersionRegex.Match(actualOutput); + if (!versionMatch.Success) { + // Might be another solver. + return null; + } + + var major = int.Parse(versionMatch.Groups["major"].Value); + var minor = int.Parse(versionMatch.Groups["minor"].Value); + var patch = int.Parse(versionMatch.Groups["patch"].Value); + return new Version(major, minor, patch); } // Set a Z3 option, but only if it is not overwriting an existing option. @@ -1098,7 +1155,7 @@ private void SetZ3Option(string name, string value) { } } - private void SetZ3Options() { + private void SetZ3Options(Version z3Version) { // Boogie sets the following Z3 options by default: // smt.mbqi = false // model.compact = false @@ -1108,10 +1165,14 @@ private void SetZ3Options() { // Boogie also used to set the following options, but does not anymore. SetZ3Option("auto_config", "false"); SetZ3Option("type_check", "true"); - SetZ3Option("smt.case_split", "3"); // TODO: try removing SetZ3Option("smt.qi.eager_threshold", "100"); // TODO: try lowering SetZ3Option("smt.delay_units", "true"); - SetZ3Option("smt.arith.solver", "2"); + + if (z3Version is not null && z3Version.Major == 4 && z3Version.Minor == 8 && z3Version.Build == 5) { + // These options tend to help with Z3 4.8.5 but hurt with newer versions of Z3. + SetZ3Option("smt.case_split", "3"); + SetZ3Option("smt.arith.solver", "2"); + } if (DisableNLarith || 3 <= ArithMode) { SetZ3Option("smt.arith.nl", "false"); diff --git a/Source/DafnyLanguageServer/DafnyLanguageServer.cs b/Source/DafnyLanguageServer/DafnyLanguageServer.cs index 5debac48260..62aa59cf5b2 100644 --- a/Source/DafnyLanguageServer/DafnyLanguageServer.cs +++ b/Source/DafnyLanguageServer/DafnyLanguageServer.cs @@ -70,33 +70,19 @@ private static void PublishSolverPath(ILanguageServer server) { } private static void HandleZ3Version(ITelemetryPublisher telemetryPublisher, SMTLibSolverOptions proverOptions) { - var z3Process = new ProcessStartInfo(proverOptions.ProverPath, "-version") { - CreateNoWindow = true, - RedirectStandardError = true, - RedirectStandardOutput = true, - RedirectStandardInput = true - }; - var run = Process.Start(z3Process); - if (run == null) { - return; - } - - var actualOutput = run.StandardOutput.ReadToEnd(); - run.WaitForExit(); - var versionMatch = Z3VersionRegex.Match(actualOutput); - if (!versionMatch.Success) { - // Might be another solver. + var z3Version = DafnyOptions.GetZ3Version(proverOptions.ProverPath); + if (z3Version is null) { return; } - - telemetryPublisher.PublishZ3Version(versionMatch.Value); - var major = int.Parse(versionMatch.Groups["major"].Value); - var minor = int.Parse(versionMatch.Groups["minor"].Value); - var patch = int.Parse(versionMatch.Groups["patch"].Value); + var major = z3Version.Major; + var minor = z3Version.Minor; + var patch = z3Version.Build; if (major <= 4 && (major < 4 || minor <= 8) && (minor < 8 || patch <= 6)) { return; } + telemetryPublisher.PublishZ3Version("Z3 version {major}.{minor}.{patch}"); + var toReplace = "O:model_compress=false"; var i = DafnyOptions.O.ProverOptions.IndexOf(toReplace); if (i == -1) {