Add PROVER_PATH prover option (to base options, but currently only used by SMTLib)

Add support for Inspector with latest Z3/SMT2 frontend

1 files changed, 158 insertions, 0 deletions

diff --git a/Source/Provers/SMTLib/Inspector.cs b/Source/Provers/SMTLib/Inspector.cs
new file mode 100644
index 00000000..4126c169
--- /dev/null
+++ b/Source/Provers/SMTLib/Inspector.cs
@@ -0,0 +1,158 @@
+//-----------------------------------------------------------------------------

+//

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

+//

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

+using System;

+using System.IO;

+using System.Diagnostics;

+using System.Collections;

+using System.Collections.Generic;

+using System.Diagnostics.Contracts;

+//using util;

+using Microsoft.Boogie;

+using Microsoft.Boogie.Simplify;

+using Microsoft.Basetypes;

+using Microsoft.Boogie.VCExprAST;

+

+namespace Microsoft.Boogie.SMTLib

+{

+  internal class FindLabelsVisitor : TraversingVCExprVisitor<bool, bool> {

+    public HashSet<string/*!*/>/*!*/ Labels = new HashSet<string/*!*/>();

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(cce.NonNull(Labels));

+    }

+

+

+    public static HashSet<string/*!*/>/*!*/ FindLabels(VCExpr/*!*/ expr) {

+      Contract.Requires(expr != null);

+      Contract.Ensures(cce.NonNull(Contract.Result<HashSet<string/*!*/>/*!*/>()));

+

+      FindLabelsVisitor visitor = new FindLabelsVisitor();

+      visitor.Traverse(expr, true);

+      return visitor.Labels;

+    }

+    

+    protected override bool StandardResult(VCExpr node, bool arg) {

+      //Contract.Requires(node!=null);

+      VCExprNAry nary = node as VCExprNAry;

+      if (nary != null) {

+        VCExprLabelOp lab = nary.Op as VCExprLabelOp;

+        if (lab != null) {

+          Labels.Add(lab.label);

+        }

+      }

+      return true;

+    }

+  }

+

+  internal class Inspector {

+    [Rep] protected readonly Process inspector;

+    [Rep] readonly TextReader fromInspector;

+    [Rep] readonly TextWriter toInspector;

+    [ContractInvariantMethod]

+    void ObjectInvariant() 

+    {

+      Contract.Invariant(inspector!=null);

+      Contract.Invariant(fromInspector!=null);

+      Contract.Invariant(toInspector != null);

+    }

+

+

+    public Inspector(SMTLibProverOptions opts)

+    {

+      Contract.Requires(opts != null);

+      ProcessStartInfo psi = new ProcessStartInfo(opts.Inspector);

+      Contract.Assert(psi!=null);

+      psi.CreateNoWindow = true;

+      psi.UseShellExecute = false;

+      psi.RedirectStandardInput = true;

+      psi.RedirectStandardOutput = true;

+      psi.RedirectStandardError = false;

+

+      try 

+      {

+        Process inspector = Process.Start(psi);

+        this.inspector = inspector;

+        fromInspector = inspector.StandardOutput;

+        toInspector = inspector.StandardInput;

+      } 

+      catch (System.ComponentModel.Win32Exception e)

+      {

+        throw new Exception(string.Format("Unable to start the inspector process {0}: {1}", opts.Inspector, e.Message));

+      }

+    }

+

+    public void NewProblem(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler)

+    {

+      Contract.Requires(descriptiveName != null);

+      Contract.Requires(vc != null);

+      Contract.Requires(handler != null);

+      HashSet<string/*!*/>/*!*/ labels = FindLabelsVisitor.FindLabels(vc);

+      Contract.Assert(labels!=null);

+      toInspector.WriteLine("PROBLEM " + descriptiveName);

+      toInspector.WriteLine("TOKEN BEGIN");

+      foreach (string lab in labels) {

+        Contract.Assert(lab!=null);

+        string no = lab.Substring(1);

+        Absy absy = handler.Label2Absy(no);

+        

+        IToken tok = absy.tok;

+        AssertCmd assrt = absy as AssertCmd;

+        Block blk = absy as Block;

+        string val = tok.val; // might require computation, so cache it

+        if (val == "foo" || tok.filename == null) continue; // no token

+

+        toInspector.Write("TOKEN ");

+        toInspector.Write(lab);

+        toInspector.Write(" ");

+

+        if (assrt != null) {

+          toInspector.Write("ASSERT");

+          string errData = assrt.ErrorData as string;

+          if (errData != null) {

+            val = errData;

+          } else if (assrt.ErrorMessage != null) {

+            val = assrt.ErrorMessage;

+          }

+        } else if (blk != null) {

+          toInspector.Write("BLOCK ");

+          toInspector.Write(blk.Label);

+        } else {

+          Contract.Assume( false);

+        }

+        if (val == null || val == "assert" || val == "ensures") { val = ""; }

+

+        if (absy is LoopInitAssertCmd) {

+          val += " (loop entry)";

+        } else if (absy is LoopInvMaintainedAssertCmd) {

+          val += " (loop body)";

+        } else if (val.IndexOf("#VCCERR") >= 0) { 

+          // skip further transformations

+        } else if (absy is AssertRequiresCmd) {

+          AssertRequiresCmd req = (AssertRequiresCmd)absy;

+          IToken t2 = req.Requires.tok;

+          string tval = t2.val;

+          if (tval == "requires")

+            tval = string.Format("{0}({1},{2}))", t2.filename, t2.line, t2.col);

+          string call = "";

+          if (val != "call") call = " in call to " + val;

+          val = string.Format("precondition {0}{1}", tval, call);

+        }

+

+        val = val.Replace("\r", "").Replace("\n", " ");

+

+        toInspector.WriteLine(string.Format(" {0} {1} :@:{2}:@:{3}", tok.line, tok.col, tok.filename, val));

+      }

+      toInspector.WriteLine("TOKEN END");

+    }

+

+    public void StatsLine(string line)

+    {

+      Contract.Requires(line != null);

+      toInspector.WriteLine(line);

+      toInspector.Flush();

+    }

+  }

+}