various fixes related to new error traces

4 files changed, 193 insertions, 100 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 4c0597f9..342a2b1b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -380,9 +380,72 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    public override ProverInterface.Outcome CheckOutcome(ProverInterface.ErrorHandler handler, IEnumerable<int> controlFlowConstants) {

+      var result = Outcome.Undetermined;

+      if (Process == null)

+        return result;

+

+      Contract.Assume(controlFlowConstants == null);

+      try {

+        currentErrorHandler = handler;

+        FlushProverWarnings();

+

+        var errorsLeft = CommandLineOptions.Clo.ProverCCLimit;

+        if (errorsLeft < 1)

+          errorsLeft = 1;

+

+        var globalResult = Outcome.Undetermined;

+

+        while (true) {

+          errorsLeft--;

+          Dictionary<int, string[]> paths = null;

+

+          result = GetResponse();

+          if (globalResult == Outcome.Undetermined)

+            globalResult = result;

+

+          if (result == Outcome.Invalid) {

+            paths = CalculatePath(controlFlowConstants);

+            ErrorModel errorModel = GetErrorModel();

+            Dictionary<int, IList<string>> paths1 = new Dictionary<int, IList<string>>();

+            foreach (int x in paths.Keys) {

+              paths1[x] = paths[x].ToList();

+            }

+            handler.OnModel(paths1, errorModel);

+          }

+

+          if (paths == null || errorsLeft == 0) break;

+

+          string[] path = paths[0];

+          string source = path[path.Length - 2];

+          string target = path[path.Length - 1];

+          SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + ")))");

+          SendThisVC("(check-sat)");

+        }

+

+        if (CommandLineOptions.Clo.StratifiedInlining == 0) {

+          SendThisVC("(pop 1)");

+        }

+        else if (CommandLineOptions.Clo.StratifiedInlining > 0 && pendingPop) {

+          pendingPop = false;

+          SendThisVC("(pop 1)");

+        }

+

+        FlushLogFile();

+

+        if (CommandLineOptions.Clo.RestartProverPerVC && Process != null)

+          Process.NeedsRestart = true;

+

+        return globalResult;

+      }

+      finally {

+        currentErrorHandler = null;

+      }

+    }

+

     [NoDefaultContract]

     public override Outcome CheckOutcome(ErrorHandler handler)

-    {  //Contract.Requires(handler != null);

+    {  

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

       

       var result = Outcome.Undetermined;

@@ -400,30 +463,47 @@ namespace Microsoft.Boogie.SMTLib
 

         var globalResult = Outcome.Undetermined;

 

-        while (errorsLeft-- > 0) {

+        while (true) {

+          errorsLeft--;

           string[] labels = null;

 

           result = GetResponse();

           if (globalResult == Outcome.Undetermined)

             globalResult = result;

 

-          if (result == Outcome.Invalid && options.UseZ3) {

-            labels = GetLabelsInfo(handler);

+          if (result == Outcome.Invalid) {

+            IList<string> xlabels;

+            if (CommandLineOptions.Clo.UseLabels) {

+              labels = GetLabelsInfo();

+              xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

+            }

+            else {

+              labels = CalculatePath();

+              xlabels = labels;

+            }

+            ErrorModel errorModel = GetErrorModel();

+            handler.OnModel(xlabels, errorModel);

           }

 

-          if (labels == null) break;

+          if (labels == null || errorsLeft == 0) break;

 

-          var negLabels = labels.Where(l => l.StartsWith("@")).ToArray();

-          var posLabels = labels.Where(l => !l.StartsWith("@"));

-          Func<string, string> lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s));

-          if (!options.MultiTraces)

-            posLabels = Enumerable.Empty<string>();

-          var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();

-          var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");

-          if (errorsLeft > 0) {

+          if (CommandLineOptions.Clo.UseLabels) {

+            var negLabels = labels.Where(l => l.StartsWith("@")).ToArray();

+            var posLabels = labels.Where(l => !l.StartsWith("@"));

+            Func<string, string> lbl = (s) => SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(s));

+            if (!options.MultiTraces)

+              posLabels = Enumerable.Empty<string>();

+            var conjuncts = posLabels.Select(s => "(not " + lbl(s) + ")").Concat(negLabels.Select(lbl)).ToArray();

+            var expr = conjuncts.Length == 1 ? conjuncts[0] : ("(or " + conjuncts.Concat(" ") + ")");

             SendThisVC("(assert " + expr + ")");

             SendThisVC("(check-sat)");

           }

+          else {

+            string source = labels[labels.Length - 2];

+            string target = labels[labels.Length - 1];

+            SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") " + target + ")))");

+            SendThisVC("(check-sat)");

+          }

         }

 

         if (CommandLineOptions.Clo.StratifiedInlining == 0)

@@ -449,99 +529,99 @@ namespace Microsoft.Boogie.SMTLib
     }

 

     private string[] CalculatePath() {

-      SendThisVC("(get-value ((ControlFlow 0 0)))");

-      var path = new List<string>();

+      Dictionary<int, string[]> dict = CalculatePath(new int[] { 0 });

+      return dict[0];

+    }

+

+    private Dictionary<int, string[]> CalculatePath(IEnumerable<int> controlFlowConstants) {

+      Dictionary<int, string[]> ret = new Dictionary<int, string[]>();

+      foreach (var controlFlowConstant in controlFlowConstants) {

+        SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " 0)))");

+        var path = new List<string>();

+        while (true) {

+          var resp = Process.GetProverResponse();

+          if (resp == null) break;

+          if (!(resp.Name == "" && resp.ArgCount == 1)) break;

+          resp = resp.Arguments[0];

+          if (!(resp.Name == "" && resp.ArgCount == 2)) break;

+          resp = resp.Arguments[1];

+          var v = resp.Name;

+          if (v == "-" && resp.ArgCount == 1) {

+            v = resp.Arguments[0].Name;

+            path.Add(v);

+            break;

+          }

+          else if (resp.ArgCount != 0)

+            break;

+          path.Add(v);

+          SendThisVC("(get-value ((ControlFlow " + controlFlowConstant + " " + v + ")))");

+        }

+        ret[controlFlowConstant] = path.ToArray();

+      }

+      return ret;

+    }

+

+    private ErrorModel GetErrorModel() {

+      if (!options.ExpectingModel())

+        return null;

+      SendThisVC("(get-model)");

+      Process.Ping();

+      Model theModel = null;

       while (true) {

         var resp = Process.GetProverResponse();

-        if (resp == null)

-          break;

-        if (!(resp.Name == "" && resp.ArgCount == 1)) break;

-        resp = resp.Arguments[0];

-        if (!(resp.Name == "" && resp.ArgCount == 2)) break;

-        resp = resp.Arguments[1];

-        var v = resp.Name;

-        if (v == "-" && resp.ArgCount == 1) 

-          v += resp.Arguments[0].Name;

-        else if (resp.ArgCount != 0) 

-          break;

-        if (v.StartsWith("-")) {

-          path.Add("@" + v.Substring(1));

+        if (resp == null || Process.IsPong(resp))

           break;

+        if (theModel != null)

+          HandleProverError("Expecting only one model but got many");

+        

+        string modelStr = null;

+        if (resp.Name == "model" && resp.ArgCount >= 1) {

+          modelStr = resp[0].Name;

+        }

+        else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {

+          modelStr = resp.Name;

         }

         else {

-          path.Add("+" + v);

+          HandleProverError("Unexpected prover response getting model: " + resp.ToString());

+        }

+        List<Model> models = null;

+        try {

+          models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));

+        }

+        catch (ArgumentException exn) {

+          HandleProverError("Model parsing error: " + exn.Message);

         }

-        SendThisVC("(get-value ((ControlFlow 0 " + v + ")))");

+        if (models == null)

+          HandleProverError("Could not parse any models");

+        else if (models.Count == 0)

+          HandleProverError("Could not parse any models");

+        else if (models.Count > 1)

+          HandleProverError("Expecting only one model but got many");

+        else

+          theModel = models[0];

       }

-      return path.ToArray();

+      return new ErrorModel(theModel);

     }

 

-    private string[] GetLabelsInfo(ErrorHandler handler)

+    private string[] GetLabelsInfo()

     {

-      if (CommandLineOptions.Clo.UseLabels)

-        SendThisVC("(labels)");

-      if (options.ExpectingModel())

-        SendThisVC("(get-model)");

+      SendThisVC("(labels)");

       Process.Ping();

 

-      List<string> labelNums = null;

-      Model theModel = null;

       string[] res = null;

-

       while (true) {

         var resp = Process.GetProverResponse();

         if (resp == null || Process.IsPong(resp))

           break;

+        if (res != null)

+          HandleProverError("Expecting only one sequence of labels but got many");

         if (resp.Name == "labels" && resp.ArgCount >= 1) {

-          var labels = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray();

-          res = labels;

-          if (labelNums != null) HandleProverError("Got multiple :labels responses");

-          labelNums = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

-        } else {

-          string modelStr = null;

-          if (resp.Name == "model" && resp.ArgCount >= 1) {

-            modelStr = resp[0].Name;

-          } else if (resp.ArgCount == 0 && resp.Name.Contains("->")) {

-            modelStr = resp.Name;

-          }

-

-          if (modelStr != null) {

-            List<Model> models = null;

-            try {

-              models = Model.ParseModels(new StringReader("Z3 error model: \n" + modelStr));

-            } catch (ArgumentException exn) {

-              HandleProverError("Model parsing error: " + exn.Message);

-            }

-

-            if (models != null) {

-              if (models.Count == 0) HandleProverError("Could not parse any models");

-              else {

-                if (models.Count > 1) HandleProverError("Expecting only one model, got multiple");

-                if (theModel != null) HandleProverError("Got multiple :model responses");

-                theModel = models[0];

-              }

-            }

-          } else {

-            HandleProverError("Unexpected prover response (getting labels/model): " + resp.ToString());

-          }

+          res = resp.Arguments.Select(a => a.Name.Replace("|", "")).ToArray();

+        }

+        else {

+          HandleProverError("Unexpected prover response getting labels: " + resp.ToString());

         }

       }

-

-      if (!CommandLineOptions.Clo.UseLabels) {

-        res = CalculatePath();

-        if (res.Length == 0) 

-          res = null;

-        else

-          labelNums = res.Select(a => a.Replace("@", "").Replace("+", "")).ToList();

-      }

-

-      if (labelNums != null) {

-        ErrorModel m = null;

-        if (theModel != null)

-          m = new ErrorModel(theModel);

-        handler.OnModel(labelNums, m);

-      }

-

       return res;

     }

 

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 9b7b6e36..73ca71b2 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -734,7 +734,11 @@ namespace Microsoft.Boogie {
       Undetermined

     }

     public class ErrorHandler {

-      public virtual void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {

+      public virtual void OnModel(Dictionary<int, IList<string>> labels, ErrorModel errModel) {

+

+      }

+

+      public virtual void OnModel(IList<string> labels, ErrorModel errModel) {

         Contract.Requires(cce.NonNullElements(labels));

       }

 

@@ -743,7 +747,6 @@ namespace Microsoft.Boogie {
       }

 

       public virtual void OnProverWarning(string message)

-        //modifies Console.Out.*, Console.Error.*;

       {

         Contract.Requires(message != null);

         switch (CommandLineOptions.Clo.PrintProverWarnings) {

@@ -761,7 +764,6 @@ namespace Microsoft.Boogie {
         }

       }

 

-

       public virtual Absy Label2Absy(string label) {

         Contract.Requires(label != null);

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

@@ -772,6 +774,9 @@ namespace Microsoft.Boogie {
     public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);

     [NoDefaultContract]

     public abstract Outcome CheckOutcome(ErrorHandler handler);

+    public virtual Outcome CheckOutcome(ErrorHandler handler, IEnumerable<int> controlFlowConstants) {

+      throw new System.NotImplementedException();

+    }

     public virtual void LogComment(string comment) {

       Contract.Requires(comment != null);

     }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index e0d7b4a7..0bdb17a4 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -87,7 +87,6 @@ namespace VC
             {

                 Contract.Invariant(cce.NonNullElements(privateVars));

                 Contract.Invariant(cce.NonNullElements(interfaceExprVars));

-                Contract.Invariant(cce.NonNullElements(interfaceExprVars));

             }

 

             public bool initialized;

@@ -127,9 +126,6 @@ namespace VC
                 {

                     StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, checker.TheoremProver.Context, QuantifierExpr.GetNextSkolemId());

                     implName2StratifiedInliningInfo[impl.Name] = info;

-                    // We don't need controlFlowVariable for stratified Inlining

-                    //impl.LocVars.Add(info.controlFlowVariable);

-                    

 

                     ExprSeq exprs = new ExprSeq();

                     foreach (Variable v in program.GlobalVariables())

@@ -209,10 +205,16 @@ namespace VC
             VCExpressionGenerator gen = checker.VCExprGen;

             Contract.Assert(gen != null);

 

-

-            VCExpr vcexpr = gen.Not(GenerateVC(impl, null, out label2absy, checker));

+            VCExpr vcexpr = gen.Not(GenerateVC(impl, info.controlFlowVariable, out label2absy, checker));

             Contract.Assert(vcexpr != null);

-          

+            if (!CommandLineOptions.Clo.UseLabels) {

+              var ctx = checker.TheoremProver.Context;

+              var bet = ctx.BoogieExprTranslator;

+              VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);

+              VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));

+              VCExpr eqExpr = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));

+              vcexpr = ctx.ExprGen.And(eqExpr, vcexpr);

+            }

           

             info.label2absy = label2absy;

             info.mvInfo = mvInfo;

@@ -2460,6 +2462,14 @@ namespace VC
                 }

                 //Console.WriteLine("Inlining {0}", procName);

                 VCExpr expansion = cce.NonNull(info.vcexpr);

+                

+                if (!CommandLineOptions.Clo.UseLabels) {

+                  var ctx = checker.TheoremProver.Context;

+                  var bet = ctx.BoogieExprTranslator;

+                  VCExpr controlFlowVariableExpr = bet.LookupVariable(info.controlFlowVariable);

+                  VCExpr eqExpr = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.FromInt(id)));

+                  expansion = ctx.ExprGen.And(eqExpr, expansion);

+                }

 

                 // Instantiate the "forall" variables

                 Dictionary<VCExprVar, VCExpr> substForallDict = new Dictionary<VCExprVar, VCExpr>();

@@ -3591,9 +3601,7 @@ namespace VC
                           NAryExpr mvStateExpr = expr as NAryExpr;

                           if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) {

                             LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;

-                            Debug.Assert(x != null);

-                            int foo = x.asBigNum.ToInt;

-                            orderedStateIds.Add(new Tuple<int, int>(candidateId, foo));

+                            orderedStateIds.Add(new Tuple<int, int>(candidateId, x.asBigNum.ToInt));

                           }

                         }

 

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 1c0aeee8..a1693650 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -102,7 +102,7 @@ namespace VC {
 

         this.impl = impl;

         this.uniqueId = uniqueId;

-        this.controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "cfc", Microsoft.Boogie.Type.Int));

+        this.controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));

         impl.LocVars.Add(controlFlowVariable);

 

         List<Variable> interfaceVars = new List<Variable>();