Skip to content

Commit

Permalink
Improve Z3 detection
Browse files Browse the repository at this point in the history 
* Be more explicit about the path of the executable to invoke.
* Identify the version and set different Z3 options accordingly.

Fixes dafny-lang#2370
Enables a fix for dafny-lang#1477
Interacts with dafny-lang#1914 (which may already be fixed)
  • Loading branch information
@atomb
atomb committed Dec 20, 2022
1 parent b6a0117 commit e8a4d17
Show file tree
Hide file tree
Showing 2 changed files with 83 additions and 36 deletions.
91 changes: 76 additions & 15 deletions Source/DafnyCore/DafnyOptions.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -1060,35 +1063,89 @@ in such cases in the verifier being faster.

/// <summary>
/// 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.
/// </summary>
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 (?<major>\d+)\.(?<minor>\d+)\.(?<patch>\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.
Expand All @@ -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
Expand All @@ -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");
Expand Down
28 changes: 7 additions & 21 deletions Source/DafnyLanguageServer/DafnyLanguageServer.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down

0 comments on commit e8a4d17

Please sign in to comment.