From 6873de1e22575d6d227b26ead84621d0fe4cab04 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Thu, 17 Feb 2011 18:59:50 +0000 Subject: Make it possible to run Z3 on pipe; use generic PROVER_LOG options --- Binaries/UnivBackPred2.smt2 | 1 - Source/Provers/SMTLib/ProverInterface.cs | 166 +++++++++++++++++++++++-------- Source/Provers/SMTLib/SMTLib.csproj | 1 + Source/Provers/SMTLib/SMTLibProcess.cs | 28 +++++- Source/Provers/SMTLib/Z3.cs | 104 +++++++++++++++++++ 5 files changed, 255 insertions(+), 45 deletions(-) create mode 100644 Source/Provers/SMTLib/Z3.cs diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2 index 33c82099..4490d2cb 100644 --- a/Binaries/UnivBackPred2.smt2 +++ b/Binaries/UnivBackPred2.smt2 @@ -1,4 +1,3 @@ -; ------------------------------------------------------------------------- ; Boogie universal background predicate ; Copyright (c) 2004-2010, Microsoft Corp. diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 16801a65..8f1542ce 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -17,12 +17,12 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.Clustering; using Microsoft.Boogie.TypeErasure; using Microsoft.Boogie.Simplify; +using System.Text; namespace Microsoft.Boogie.SMTLib { public class SMTLibProverOptions : ProverOptions { - public string Output = "boogie-vc-@PROC@.smt2"; public bool UseWeights = true; public bool UseLabels { get { return UseZ3; } } public bool UseZ3 = true; @@ -30,7 +30,6 @@ namespace Microsoft.Boogie.SMTLib protected override bool Parse(string opt) { return - ParseString(opt, "OUTPUT", ref Output) || ParseBool(opt, "USE_WEIGHTS", ref UseWeights) || ParseBool(opt, "USE_Z3", ref UseZ3) || base.Parse(opt); @@ -44,11 +43,10 @@ namespace Microsoft.Boogie.SMTLib @" SMT-specific options: ~~~~~~~~~~~~~~~~~~~~~ -OUTPUT= Store VC in named file (default: boogie-vc-@PROC@.smt2) -USE_WEIGHTS= Pass :weight annotations on quantified formulas (default: true) USE_Z3= Use z3.exe as the prover, and use Z3 extensions (default: true) +USE_WEIGHTS= Pass :weight annotations on quantified formulas (default: true) +VERBOSITY= 1 - print prover output (default: 0) " + base.Help; - // DIST requires non-public binaries } } } @@ -105,6 +103,11 @@ USE_Z3= Use z3.exe as the prover, and use Z3 extensions (defau Namer = new SMTLibNamer(); this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer); + if (this.options.UseZ3) { + var psi = SMTLibProcess.ComputerProcessStartInfo(Z3.Z3ExecutablePath(), "AUTO_CONFIG=false -smt2 -in"); + Process = new SMTLibProcess(psi, this.options); + Process.ErrorHandler += this.HandleProverError; + } } public override ProverContext Context @@ -117,10 +120,14 @@ USE_Z3= Use z3.exe as the prover, and use Z3 extensions (defau } } - private readonly TypeAxiomBuilder AxBuilder; - private readonly UniqueNamer Namer; - private readonly TypeDeclCollector DeclCollector; - private readonly SMTLibProcess Process; + readonly TypeAxiomBuilder AxBuilder; + readonly UniqueNamer Namer; + readonly TypeDeclCollector DeclCollector; + readonly SMTLibProcess Process; + readonly List proverErrors = new List(); + readonly StringBuilder common = new StringBuilder(); + TextWriter currentLogFile; + ErrorHandler currentErrorHandler; private void FeedTypeDeclsToProver() { @@ -130,17 +137,41 @@ USE_Z3= Use z3.exe as the prover, and use Z3 extensions (defau } } - public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) + private string Sanitize(string msg) { - //Contract.Requires(descriptiveName != null); - //Contract.Requires(vc != null); - //Contract.Requires(handler != null); - TextWriter output = OpenOutputFile(descriptiveName); - Contract.Assert(output != null); + var idx = msg.IndexOf('\n'); + if (idx > 0) + msg = msg.Replace("\r", "").Replace("\n", "\r\n"); + return msg; + } - WriteLineAndLog(output, _backgroundPredicates); - string name = SMTLibNamer.QuoteId(descriptiveName); - WriteLineAndLog(output, "(set-info :boogie-vc-id " + name + ")"); + private void SendCommon(string s) + { + Send(s, true); + } + + private void SendThisVC(string s) + { + Send(s, false); + } + + private void Send(string s, bool isCommon) + { + s = Sanitize(s); + + if (isCommon) + common.Append(s).Append("\r\n"); + + if (Process != null) + Process.Send(s); + if (currentLogFile != null) + currentLogFile.WriteLine(s); + } + + private void PrepareCommon() + { + if (common.Length == 0) + SendCommon(_backgroundPredicates); if (!AxiomsAreSetup) { var axioms = ctx.Axioms; @@ -154,26 +185,56 @@ USE_Z3= Use z3.exe as the prover, and use Z3 extensions (defau AddAxiom(VCExpr2String(axioms, -1)); AxiomsAreSetup = true; } + } - string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; - string prelude = ctx.GetProverCommands(true); - Contract.Assert(prelude != null); - WriteLineAndLog(output, prelude); - - foreach (string s in TypeDecls) { - Contract.Assert(s != null); - WriteLineAndLog(output, s); - } + private void FlushAxioms() + { + TypeDecls.Iter(SendCommon); + TypeDecls.Clear(); foreach (string s in Axioms) { Contract.Assert(s != null); if (s != "true") - WriteLineAndLog(output, "(assert " + s + ")"); + SendCommon("(assert " + s + ")"); } + Axioms.Clear(); + } - WriteLineAndLog(output, vcString); - WriteLineAndLog(output, "(check-sat)"); + private void CloseLogFile() + { + if (currentLogFile != null) { + currentLogFile.Close(); + currentLogFile = null; + } + } + + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) + { + //Contract.Requires(descriptiveName != null); + //Contract.Requires(vc != null); + //Contract.Requires(handler != null); + + currentErrorHandler = handler; + + if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen + + if (options.LogFilename != null && currentLogFile == null) { + currentLogFile = OpenOutputFile(descriptiveName); + currentLogFile.Write(common.ToString()); + } + + PrepareCommon(); + string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))"; + FlushAxioms(); + + SendThisVC("(push)"); + SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")"); + SendThisVC(vcString); - output.Close(); + if (Process != null) + Process.PingPong(); // flush any errors + + SendThisVC("(check-sat)"); + SendThisVC("(pop 1)"); } private TextWriter OpenOutputFile(string descriptiveName) @@ -181,27 +242,52 @@ USE_Z3= Use z3.exe as the prover, and use Z3 extensions (defau Contract.Requires(descriptiveName != null); Contract.Ensures(Contract.Result() != null); - string filename = ((SMTLibProverOptions)options).Output; + string filename = options.LogFilename; filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename)); return new StreamWriter(filename, false); } - private void WriteLineAndLog(TextWriter output, string msg) + private void HandleProverError(string s) { - Contract.Requires(output != null); - Contract.Requires(msg != null); - var idx = msg.IndexOf('\n'); - if (idx > 0) { - msg = msg.Replace("\r", "").Replace("\n", "\r\n"); + lock (proverErrors) { + proverErrors.Add(s); + Console.Error.WriteLine("Prover error: " + s); } - output.WriteLine(msg); } [NoDefaultContract] public override Outcome CheckOutcome(ErrorHandler handler) { //Contract.Requires(handler != null); Contract.EnsuresOnThrow(true); - return Outcome.Undetermined; + + var result = Outcome.Undetermined; + + if (Process == null) + return result; + + Process.Ping(); + + + while (true) { + var resp = Process.GetProverResponse(); + if (resp == null || Process.IsPong(resp)) + break; + + switch (resp.Name) { + case "unsat": + result = Outcome.Valid; + break; + case "sat": + case "unknown": + result = Outcome.Invalid; + break; + default: + HandleProverError("Unexpected prover response: " + resp.ToString()); + break; + } + } + + return result; } protected string VCExpr2String(VCExpr expr, int polarity) diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj index c0ade351..536fd43e 100644 --- a/Source/Provers/SMTLib/SMTLib.csproj +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -114,6 +114,7 @@ + diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index da058ab6..4a631960 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -18,6 +18,7 @@ namespace Microsoft.Boogie.SMTLib public class SMTLibProcess { readonly Process prover; + readonly SMTLibProverOptions options; readonly Queue proverOutput = new Queue(); readonly Queue proverErrors = new Queue(); readonly TextWriter toProver; @@ -34,12 +35,14 @@ namespace Microsoft.Boogie.SMTLib }; } - public SMTLibProcess(ProcessStartInfo psi) + public SMTLibProcess(ProcessStartInfo psi, SMTLibProverOptions options) { + this.options = options; + try { - prover.ErrorDataReceived += prover_ErrorDataReceived; - prover.OutputDataReceived += prover_OutputDataReceived; prover = Process.Start(psi); + prover.ErrorDataReceived += prover_ErrorDataReceived; + prover.OutputDataReceived += prover_OutputDataReceived; prover.BeginErrorReadLine(); prover.BeginOutputReadLine(); toProver = prover.StandardInput; @@ -50,6 +53,13 @@ namespace Microsoft.Boogie.SMTLib public void Send(string cmd) { + if (options.Verbosity >= 2) { + var log = cmd; + if (log.Length > 50) + log = log.Substring(0, 50) + "..."; + log = log.Replace("\r", "").Replace("\n", " "); + Console.WriteLine("[SMT-INP] {0}", log); + } toProver.WriteLine(cmd); } @@ -78,6 +88,8 @@ namespace Microsoft.Boogie.SMTLib public SExpr GetProverResponse() { + toProver.Flush(); + while (true) { var exprs = ParseSExprs(true).ToArray(); Contract.Assert(exprs.Length <= 1); @@ -114,8 +126,10 @@ namespace Microsoft.Boogie.SMTLib if (linePos < currLine.Length) return currLine[linePos]; - else + else { currLine = null; + linePos = 0; + } } } @@ -138,6 +152,7 @@ namespace Microsoft.Boogie.SMTLib if (quoted) { sb.Append("\n"); currLine = ReadProver(); + linePos = 0; if (currLine == null) break; } else break; @@ -176,6 +191,7 @@ namespace Microsoft.Boogie.SMTLib if (c == ')') { if (top) ParseError("stray ')'"); + break; } string id; @@ -245,6 +261,8 @@ namespace Microsoft.Boogie.SMTLib void prover_OutputDataReceived(object sender, DataReceivedEventArgs e) { lock (this) { + if (options.Verbosity >= 1) + Console.WriteLine("[SMT-OUT] {0}", e.Data); proverOutput.Enqueue(e.Data); Monitor.Pulse(this); } @@ -253,6 +271,8 @@ namespace Microsoft.Boogie.SMTLib void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e) { lock (this) { + if (options.Verbosity >= 1) + Console.WriteLine("[SMT-ERR] {0}", e.Data); proverErrors.Enqueue(e.Data); Monitor.Pulse(this); } diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs new file mode 100644 index 00000000..3867a55b --- /dev/null +++ b/Source/Provers/SMTLib/Z3.cs @@ -0,0 +1,104 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics.Contracts; +using System.IO; +using System.Text.RegularExpressions; + +namespace Microsoft.Boogie.SMTLib +{ + class Z3 + { + static string _proverPath; + + static string CodebaseString() + { + Contract.Ensures(Contract.Result() != null); + return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)); + } + + public static string Z3ExecutablePath() + { + if (_proverPath == null) + FindZ3Executable(); + return _proverPath; + } + + static void FindZ3Executable() + // throws ProverException, System.IO.FileNotFoundException; + { + Contract.Ensures(_proverPath != null); + + var proverExe = "z3.exe"; + + if (_proverPath == null) { + // Initialize '_proverPath' + _proverPath = Path.Combine(CodebaseString(), proverExe); + string firstTry = _proverPath; + + if (File.Exists(firstTry)) + return; + + string programFiles = Environment.GetEnvironmentVariable("ProgramFiles"); + Contract.Assert(programFiles != null); + string programFilesX86 = Environment.GetEnvironmentVariable("ProgramFiles(x86)"); + if (programFiles.Equals(programFilesX86)) { + // If both %ProgramFiles% and %ProgramFiles(x86)% point to "ProgramFiles (x86)", use %ProgramW6432% instead. + programFiles = Environment.GetEnvironmentVariable("ProgramW6432"); + } + + + List z3Dirs = new List(); + if (Directory.Exists(programFiles + @"\Microsoft Research\")) { + string msrDir = programFiles + @"\Microsoft Research\"; + z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*")); + } + if (Directory.Exists(programFilesX86 + @"\Microsoft Research\")) { + string msrDir = programFilesX86 + @"\Microsoft Research\"; + z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*")); + } + + // Look for the most recent version of Z3. + int minor = 0, major = 0; + string winner = null; + Regex r = new Regex(@"^Z3-(\d+)\.(\d+)$"); + foreach (string d in z3Dirs) { + string name = new DirectoryInfo(d).Name; + foreach (Match m in r.Matches(name)) { + int ma, mi; + ma = int.Parse(m.Groups[1].ToString()); + mi = int.Parse(m.Groups[2].ToString()); + if (major < ma || (major == ma && minor < mi)) { + major = ma; + minor = mi; + winner = d; + } + } + } + + if (major == 0 && minor == 0) { + throw new ProverException("Cannot find executable: " + firstTry); + } + Contract.Assert(winner != null); + + _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe); + if (!File.Exists(_proverPath)) { + throw new ProverException("Cannot find prover: " + _proverPath); + } + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("[TRACE] Using prover: " + _proverPath); + } + } + } + + + } +} -- cgit v1.2.3