Start implementation of pipe communication in SMTLIB backend

4 files changed, 380 insertions, 11 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 7a38a95b..7ad1ac0c 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -22,16 +22,17 @@ namespace Microsoft.Boogie.SMTLib
 {

   public class SMTLibProverOptions : ProverOptions

   {

-    public string Output = "boogie-vc-@PROC@.smt";

-    public bool UsePredicates = false;

+    public string Output = "boogie-vc-@PROC@.smt2";

     public bool UseWeights = true;

-    public bool UseLabels = false;

+    public bool UseLabels { get { return UseZ3; } }

+    public bool UseZ3 = true;

 

     protected override bool Parse(string opt)

     {

       return

         ParseString(opt, "OUTPUT", ref Output) ||

-        ParseBool(opt, "USE_PREDICATES", ref UsePredicates) ||

+        ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||

+        ParseBool(opt, "USE_Z3", ref UseZ3) ||

         base.Parse(opt);

     }

 

@@ -43,9 +44,9 @@ namespace Microsoft.Boogie.SMTLib
 @"

 SMT-specific options:

 ~~~~~~~~~~~~~~~~~~~~~

-OUTPUT=<string>           Store VC in named file. Defaults to boogie-vc-@PROC@.smt.

-USE_PREDICATES=<bool>     Try to use SMT predicates for functions returning bool.

-

+OUTPUT=<string>           Store VC in named file (default: boogie-vc-@PROC@.smt2)

+USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (default: true)

+USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (default: true)

 " + base.Help;

         // DIST requires non-public binaries

       }

@@ -111,6 +112,7 @@ void ObjectInvariant()
     private readonly TypeAxiomBuilder AxBuilder;

     private readonly UniqueNamer Namer;

     private readonly TypeDeclCollector DeclCollector;

+    private readonly SMTLibProcess Process;

 

     private void FeedTypeDeclsToProver() {

       foreach (string s in DeclCollector.GetNewDeclarations())

@@ -314,10 +316,6 @@ void ObjectInvariant()
       //Contract.Requires(options != null);

       Contract.Ensures(Contract.Result<object>() != null);

 

-      if (CommandLineOptions.Clo.BracketIdsInVC < 0) {

-        CommandLineOptions.Clo.BracketIdsInVC = 0;

-      }

-

       VCExpressionGenerator gen = new VCExpressionGenerator ();

       List<string>/*!>!*/ proverCommands = new List<string/*!*/> ();

 // TODO: what is supported?

diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs
new file mode 100644
index 00000000..2d143830
--- /dev/null
+++ b/Source/Provers/SMTLib/SExpr.cs
@@ -0,0 +1,105 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System;

+using System.Linq;

+using System.Collections.Generic;

+using System.Collections.ObjectModel;

+using System.Text;

+using System.Diagnostics.Contracts;

+using System.Globalization;

+

+namespace Microsoft.Boogie

+{

+  public class SExpr

+  {

+    static readonly SExpr[] EmptyArgs = new SExpr[0];

+    public readonly string Name;

+    public SExpr[] Arguments

+    {

+      get

+      {

+        Contract.Ensures(Contract.Result<SExpr[]>() != null);

+        Contract.Ensures(Contract.ForAll(Contract.Result<SExpr[]>(), expr => expr != null));

+

+        return this.arguments;

+      }

+    }

+

+    public SExpr this[int idx]

+    {

+      get

+      {

+        return Arguments[idx];

+      }

+    }

+

+    public bool IsId

+    {

+      get { return Arguments.Length == 0; }

+    }

+

+    private readonly SExpr[] arguments;

+

+    [ContractInvariantMethod]

+    void ObjectInvariant()

+    {

+      Contract.Invariant(this.Name != null);

+      Contract.Invariant(this.arguments != null);

+      Contract.Invariant(Contract.ForAll(this.arguments, arg => arg != null));

+    }

+

+    public SExpr(string name, params SExpr[] args)

+      : this(name, (IEnumerable<SExpr>)args)

+    {

+      Contract.Requires(name != null);

+      Contract.Requires(args != null);

+      Contract.Requires(Contract.ForAll(args, x => x != null));

+    }

+

+    public SExpr(string name, IEnumerable<SExpr> args)

+    {

+      Contract.Requires(name != null);

+      Contract.Requires(args != null);

+      // We don't want to evaluate args twice!

+      // Contract.Requires(Contract.ForAll(args, x => x != null));

+      Name = name;

+      arguments = args.ToArray();

+    }

+

+    public SExpr(string name)

+      : this(name, EmptyArgs)

+    {

+      Contract.Requires(name != null);

+    }

+

+    #region pretty-printing

+    void WriteTo(StringBuilder sb)

+    {

+      Contract.Requires(sb != null);

+

+      if (Arguments.Length > 0) sb.Append('(');

+      if (Name.Any(Char.IsWhiteSpace))

+        sb.Append("\"").Append(Name).Append("\"");

+      else

+        sb.Append(Name);

+      foreach (var a in Arguments) {

+        sb.Append(' ');

+        a.WriteTo(sb);

+      }

+      if (Arguments.Length > 0) sb.Append(')');

+    }

+

+    public override string ToString()

+    {

+      var sb = new StringBuilder();

+      this.WriteTo(sb);

+      return sb.ToString();

+    }

+    #endregion

+

+  }

+}

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 7e0ed5e7..c0ade351 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -108,8 +108,10 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="ProverInterface.cs" />

+    <Compile Include="SExpr.cs" />

     <Compile Include="SMTLibLineariser.cs" />

     <Compile Include="SMTLibNamer.cs" />

+    <Compile Include="SMTLibProcess.cs" />

     <Compile Include="TypeDeclCollector.cs" />

     <Compile Include="..\..\version.cs" />

   </ItemGroup>

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
new file mode 100644
index 00000000..da058ab6
--- /dev/null
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -0,0 +1,264 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using System.IO;

+using System.Threading;

+using System.Diagnostics.Contracts;

+

+namespace Microsoft.Boogie.SMTLib

+{

+  public class SMTLibProcess

+  {

+    readonly Process prover;

+    readonly Queue<string> proverOutput = new Queue<string>();

+    readonly Queue<string> proverErrors = new Queue<string>();

+    readonly TextWriter toProver;    

+

+    public static ProcessStartInfo ComputerProcessStartInfo(string executable, string options)

+    {

+      return new ProcessStartInfo(executable, options)

+      {

+        CreateNoWindow = true,

+        UseShellExecute = false,

+        RedirectStandardInput = true,

+        RedirectStandardOutput = true,

+        RedirectStandardError = true

+      };

+    }

+

+    public SMTLibProcess(ProcessStartInfo psi)

+    {

+      try {

+        prover.ErrorDataReceived += prover_ErrorDataReceived;

+        prover.OutputDataReceived += prover_OutputDataReceived;

+        prover = Process.Start(psi);

+        prover.BeginErrorReadLine();

+        prover.BeginOutputReadLine();

+        toProver = prover.StandardInput;

+      } catch (System.ComponentModel.Win32Exception e) {

+        throw new ProverException(string.Format("Unable to start the process {0}: {1}", psi.FileName, e.Message));

+      }

+    }

+

+    public void Send(string cmd)

+    {

+      toProver.WriteLine(cmd);

+    }

+

+    // this is less than perfect; (echo ...) would be better

+    public void Ping()

+    {

+      Send("(get-info :name)");

+    }

+

+    public bool IsPong(SExpr sx)

+    {

+      return sx.Name == "" && sx.Arguments.Length == 1 && sx.Arguments[0].Name.Contains("name");

+    }

+

+    public void PingPong()

+    {

+      Ping();

+      while (true) {

+        var sx = GetProverResponse();

+        if (IsPong(sx))

+          return;

+        else

+          ErrorHandler("Invalid PING response from the prover: " + sx.ToString());

+      }

+    }

+

+    public SExpr GetProverResponse()

+    {

+      while (true) {

+        var exprs = ParseSExprs(true).ToArray();

+        Contract.Assert(exprs.Length <= 1);

+        if (exprs.Length == 0)

+          return null;

+        var resp = exprs[0];

+        if (resp.Name == "error") {

+          if (resp.Arguments.Length == 1 && resp.Arguments[0].IsId)

+            ErrorHandler(resp.Arguments[0].Name);

+          else

+            ErrorHandler(resp.ToString());

+        } else

+          return resp;

+      }

+    }

+

+    public event Action<string> ErrorHandler;

+    int errorCnt;

+

+    #region SExpr parsing

+    int linePos;

+    string currLine;

+    char SkipWs()

+    {

+      while (true) {

+        if (currLine == null) {

+          currLine = ReadProver();

+          if (currLine == null)

+            return '\0';

+        }

+

+        while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos]))

+          linePos++;

+

+        if (linePos < currLine.Length)

+          return currLine[linePos];

+        else

+          currLine = null;

+      }

+    }

+

+    void Shift()

+    {

+      linePos++;

+    }

+

+    string ParseId()

+    {

+      var sb = new StringBuilder();

+

+      var beg = SkipWs();

+      

+      var quoted = beg == '"' || beg == '|';

+      if (quoted)

+        Shift();

+      while (true) {

+        if (linePos >= currLine.Length) {

+          if (quoted) {

+            sb.Append("\n");

+            currLine = ReadProver();

+            if (currLine == null)

+              break;

+          } else break;

+        }

+

+        var c = currLine[linePos++];

+        if (quoted && c == beg)

+          break;

+        if (!quoted && char.IsWhiteSpace(c)) {

+          linePos--;

+          break;

+        }

+        if (quoted && c == '\\' && linePos < currLine.Length && currLine[linePos] == '"') {

+          sb.Append('"');

+          linePos++;

+          continue;

+        }

+        sb.Append(c);

+      }

+

+      return sb.ToString();

+    }

+

+    void ParseError(string msg)

+    {

+      ErrorHandler("Error parsing prover output: " + msg);

+    }

+

+    IEnumerable<SExpr> ParseSExprs(bool top)

+    {

+      while (true) {

+        var c = SkipWs();

+        if (c == '\0')

+          break;

+

+        if (c == ')') {

+          if (top)

+            ParseError("stray ')'");

+        }

+

+        string id;

+

+        if (c == '(') {

+          Shift();

+          c = SkipWs();          

+          if (c == '\0') {

+            ParseError("expecting something after '('");

+            break;

+          } else if (c == '(') {

+            id = "";

+          } else {

+            id = ParseId();

+          }

+

+          var args = ParseSExprs(false).ToArray();

+

+          c = SkipWs();

+          if (c == ')') {

+            Shift();

+          } else {

+            ParseError("unclosed '(" + id + "'");

+          }

+          yield return new SExpr(id, args);

+        } else {

+          id = ParseId();

+          yield return new SExpr(id);

+        }

+

+        if (top) break;

+      }

+    }

+    #endregion

+

+    #region handling input from the prover

+    string ReadProver()

+    {

+      string error = null;

+      while (true) {

+        if (error != null) {

+          ErrorHandler(error);

+          errorCnt++;

+          error = null;

+        }

+

+        lock (this) {

+          while (proverOutput.Count == 0 && proverErrors.Count == 0 && !prover.HasExited) {

+            Monitor.Wait(this, 100);

+          }

+

+          if (proverErrors.Count > 0) {

+            error = proverErrors.Dequeue();

+            continue;

+          }

+

+          if (proverOutput.Count > 0) {

+            return proverOutput.Dequeue();

+          }

+

+          if (prover.HasExited)

+            return null;

+        }

+      }

+    }

+

+    void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)

+    {

+      lock (this) {

+        proverOutput.Enqueue(e.Data);

+        Monitor.Pulse(this);

+      }

+    }

+

+    void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e)

+    {

+      lock (this) {

+        proverErrors.Enqueue(e.Data);

+        Monitor.Pulse(this);

+      }

+    }

+    #endregion

+

+  }

+}

+