Merge

7 files changed, 234 insertions, 6 deletions

diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 5b7fc946..f6a976e5 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -31,6 +31,7 @@ namespace Microsoft.Boogie {
     public int MemoryLimit = 0;

     public CommandLineOptions.BvHandling BitVectors = CommandLineOptions.BvHandling.None;

     public int Verbosity = 0;

+    public string ProverPath;

 

     private string/*!*/ stringRepr = "";

     [ContractInvariantMethod]

@@ -53,7 +54,8 @@ namespace Microsoft.Boogie {
              ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) ||

              ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) ||

              ParseInt(opt, "VERBOSITY", ref Verbosity) ||

-             ParseInt(opt, "TIME_LIMIT", ref TimeLimit);

+             ParseInt(opt, "TIME_LIMIT", ref TimeLimit) || 

+             ParseString(opt, "PROVER_PATH", ref ProverPath);

       // || base.Parse(opt)

     }

 

@@ -73,6 +75,7 @@ APPEND_LOG_FILE=<bool>    Append, rather than overwrite the log file.
 MEMORY_LIMIT=<int>        Memory limit of the prover in megabytes.

 VERBOSITY=<int>           The higher, the more verbose.

 TIME_LIMIT=<int>          Time limit per verification condition in miliseconds.

+PROVER_PATH=<string>      Path to the prover to use.

 

 The generic options may or may not be used by the prover plugin.

 ";

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();

+    }

+  }

+}

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index bc137492..9b4429f9 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -76,7 +76,10 @@ namespace Microsoft.Boogie.SMTLib
       this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);

 

       if (this.options.UseZ3) {

-        var psi = SMTLibProcess.ComputerProcessStartInfo(Z3.ExecutablePath(), "AUTO_CONFIG=false -smt2 -in");

+        var path = this.options.ProverPath;

+        if (path == null)

+          path = Z3.ExecutablePath();

+        var psi = SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");

         Process = new SMTLibProcess(psi, this.options);

         Process.ErrorHandler += this.HandleProverError;

       }

@@ -238,9 +241,13 @@ namespace Microsoft.Boogie.SMTLib
       SendThisVC(vcString);

       FlushLogFile();

 

-      if (Process != null)

+      if (Process != null) {

         Process.PingPong(); // flush any errors

 

+        if (Process.Inspector != null)

+          Process.Inspector.NewProblem(descriptiveName, vc, handler);

+      }

+

       SendThisVC("(check-sat)");

       FlushLogFile();

     }

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 3bec2e62..f4cdbb14 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -147,6 +147,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="SMTLibProverOptions.cs" />

     <Compile Include="ProverInterface.cs" />

     <Compile Include="SExpr.cs" />

@@ -178,6 +179,10 @@
       <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

       <Name>Model</Name>

     </ProjectReference>

+    <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

     <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">

       <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index a5fd1502..cea598b0 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 Inspector inspector;

     readonly SMTLibProverOptions options;

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

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

@@ -40,6 +41,10 @@ namespace Microsoft.Boogie.SMTLib
     {

       this.options = options;

 

+      if (options.Inspector != null) {

+        this.inspector = new Inspector(options);

+      }

+

       foreach (var arg in options.SolverArguments)

         psi.Arguments += " " + arg;

 

@@ -108,6 +113,11 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    internal Inspector Inspector

+    {

+      get { return inspector; }

+    }

+

     public SExpr GetProverResponse()

     {

       toProver.Flush();

@@ -123,8 +133,28 @@ namespace Microsoft.Boogie.SMTLib
             ErrorHandler(resp.Arguments[0].Name);

           else

             ErrorHandler(resp.ToString());

-        } else

+        } else if (resp.Name == "progress") {

+          if (inspector != null) {

+            var sb = new StringBuilder();

+            foreach (var a in resp.Arguments) {

+              if (a.Name == "labels") {

+                sb.Append("STATS LABELS");

+                foreach (var x in a.Arguments)

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

+              } else if (a.Name.StartsWith(":")) {

+                sb.Append("STATS NAMED_VALUES ").Append(a.Name);

+                foreach (var x in a.Arguments)

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

+              } else {

+                continue;

+              }

+              inspector.StatsLine(sb.ToString());

+              sb.Clear();

+            }

+          }

+        } else {

           return resp;

+        }

       }

     }

 

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 9b90b12a..847822c1 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -157,6 +157,9 @@ namespace Microsoft.Boogie.SMTLib
         options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

       }

 

+      if (options.Inspector != null)

+        options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

+

       // legacy option handling

       if (!CommandLineOptions.Clo.z3AtFlag)

         options.MultiTraces = true;

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index a7c01ff1..3d9ac7aa 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -239,6 +239,8 @@ namespace VC
         public static Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;

         // proc name -> k -> VCExpr

         Dictionary<string, List<VCExpr>> procVcCopies;

+        // proc name -> k -> CallSite Boolean constant

+        Dictionary<string, List<VCExprVar>> callSiteConstant;

         // VC for ProcCopyBounding

         VCExpr procBoundedVC;

 

@@ -246,6 +248,7 @@ namespace VC
         {

             interfaceVarCopies = new Dictionary<string, List<List<VCExprVar>>>();

             procVcCopies = new Dictionary<string, List<VCExpr>>();

+            callSiteConstant = new Dictionary<string, List<VCExprVar>>();

             procBoundedVC = VCExpressionGenerator.True;

 

             // Duplicate VCs of each procedure K times 

@@ -277,7 +280,7 @@ namespace VC
                     var id = calls.procCopy2Id[Tuple.Create(kvp.Key, i)];

                     calls.setCurrProc(kvp.Key);

                     calls.currInlineCount = id;

-                    var bm = new BoundingVCMutator(checker.underlyingChecker.VCExprGen, interfaceVarCopies, calls, id);

+                    var bm = new BoundingVCMutator(checker.underlyingChecker.VCExprGen, interfaceVarCopies, callSiteConstant, calls, id);

                     kvp.Value[i] = bm.Mutate(kvp.Value[i], true);

                     //checker.AddAxiom(kvp.Value[i]);

                     procBoundedVC = checker.underlyingChecker.VCExprGen.And(procBoundedVC, kvp.Value[i]);

@@ -303,15 +306,21 @@ namespace VC
         {

             // proc name -> k -> interface variables

             Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies;

+            // proc name -> k -> CallSite Boolean constant

+            Dictionary<string, List<VCExprVar>> callSiteConstant;

+

             FCallHandler calls;

             int currId;

 

-            public BoundingVCMutator(VCExpressionGenerator gen, Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies,

+            public BoundingVCMutator(VCExpressionGenerator gen, 

+                Dictionary<string, List<List<VCExprVar>>> interfaceVarCopies,

+                Dictionary<string, List<VCExprVar>> callSiteConstant,

                 FCallHandler calls, int currId)

                 : base(gen)

             {

                 Contract.Requires(gen != null);

                 this.interfaceVarCopies = interfaceVarCopies;

+                this.callSiteConstant = callSiteConstant;

                 this.calls = calls;

                 this.currId = currId;

             }

@@ -387,6 +396,9 @@ namespace VC
                                 var c = Gen.Eq(callExpr[i], iv[i]);

                                 conj = Gen.And(conj, c);

                             }

+                            // Add the call-site constant

+                            conj = Gen.And(conj, callSiteConstant[op.Func.Name][k]);

+

                             // label the conjunct

                             conj = Gen.LabelPos(string.Format("PCB_{0}_{1}", uid, k), conj);

                             ret = Gen.Or(conj, ret);

@@ -432,6 +444,7 @@ namespace VC
 

             interfaceVarCopies.Add(info.impl.Name, new List<List<VCExprVar>>());

             procVcCopies.Add(info.impl.Name, new List<VCExpr>());

+            callSiteConstant.Add(info.impl.Name, new List<VCExprVar>());

 

             for (int k = 0; k < K; k++)

             {

@@ -470,6 +483,14 @@ namespace VC
                 subst = new SubstitutingVCExprVisitor(Gen);

                 expr = subst.Mutate(expr, substExists);

 

+                // create a constant for call sites

+                string cscName = "pcb_csc_" + k.ToString() + "_" + newVarCnt.ToString();

+                newVarCnt++;

+                checker.underlyingChecker.TheoremProver.Context.DeclareConstant(new Constant(Token.NoToken, new TypedIdent(Token.NoToken, cscName, Microsoft.Boogie.Type.Bool)), false, null);

+                var csc = Gen.Variable(cscName, Microsoft.Boogie.Type.Bool);

+                callSiteConstant[info.impl.Name].Add(csc);

+

+                expr = Gen.Implies(csc, expr);

                 procVcCopies[info.impl.Name].Add(expr);

             }

         }

@@ -1816,6 +1837,7 @@ namespace VC
                             Contract.Assert(v1 != null && v2 != null);

                             conj = Gen.And(conj, Gen.Eq(v1, v2));

                         }

+                        conj = Gen.And(conj, callSiteConstant[bop.Func.Name][k]);

                         // label the conjunct

                         conj = Gen.LabelPos(string.Format("PCB_CONNECT_{0}_{1}", id, k), conj);

                         disj = Gen.Or(disj, conj);