Adding background model to fixedpoint counterexamples and small code contracts fixes

4 files changed, 44 insertions, 8 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index be98eb5b..d91ca010 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -510,6 +510,19 @@ namespace Microsoft.Boogie.SMTLib
         return topnode;

     }

 

+    private Model SExprToModel(SExpr resp, ErrorHandler handler)

+    {

+        // Concatenate all the arguments

+        string modelString = resp[0].Name;

+        // modelString = modelString.Substring(7, modelString.Length - 8); // remove "(model " and final ")"

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

+        if (models == null || models.Count == 0)

+        {

+            HandleProverError("no model from prover: " + resp.ToString());

+        }

+        return models[0];

+    }

+

     private string QuantifiedVCExpr2String(VCExpr x)

     {

         return VCExpr2String(x, 1); 

@@ -634,6 +647,14 @@ namespace Microsoft.Boogie.SMTLib
                         }

                         else

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

+                        resp = Process.GetProverResponse();

+                        if (resp.Name == "model")

+                        {

+                            var model = SExprToModel(resp, handler);

+                            cex.owner.SetBackgroundModel(model);

+                        }

+                        else

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

                         break;

                     }

                 default:

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 092d12d2..cabc9d9e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -188,12 +188,14 @@ namespace Microsoft.Boogie {
 

     public static bool firstModelFile = true;

 

+    public bool ModelHasStatesAlready = false;

+

     public void PrintModel()

     {

       var filename = CommandLineOptions.Clo.ModelViewFile;

       if (Model == null || filename == null || CommandLineOptions.Clo.StratifiedInlining > 0) return;

 

-      var m = this.GetModelWithStates();

+      var m = ModelHasStatesAlready ? Model : this.GetModelWithStates();

 

       if (filename == "-") {

         m.Write(Console.Out);

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index bc6a7ce0..e96499fe 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -52,7 +52,7 @@ namespace Microsoft.Boogie
 

         Context ctx;

         RPFP rpfp;

-        Program program;

+        // Program program;

         Microsoft.Boogie.ProverContext boogieContext;

         Microsoft.Boogie.VCExpressionGenerator gen;

         public readonly static string recordProcName = "boogie_si_record"; // TODO: this really needed?

@@ -515,7 +515,7 @@ namespace Microsoft.Boogie
 

 

             public List<VCExprVar> interfaceExprVars; 

-            public List<VCExprVar> privateVars;

+            // public List<VCExprVar> privateVars;

             public VCExpr funcExpr;

             public VCExpr falseExpr;

             public RPFP.Transformer F;

@@ -1004,7 +1004,7 @@ namespace Microsoft.Boogie
             Contract.Assert(gen != null);

             VCExpr vcexpr;

             if(NoLabels){

-                int assertionCount = 0;

+                // int assertionCount = 0;

                 VCExpr startCorrect = null; /* VC.VCGen.LetVC(cce.NonNull(impl.Blocks[0]), null, null, info.blockVariables, info.bindings,

                     info.ctxt, out assertionCount); */

                 vcexpr = gen.Let(info.bindings, startCorrect);

@@ -1017,7 +1017,7 @@ namespace Microsoft.Boogie
             info.mvInfo = mvInfo;

             List<VCExpr> interfaceExprs = new List<VCExpr>();

 

-            if (true || !info.isMain)

+            if (true /* was:  !info.isMain */)

             {

                 Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;

                 Contract.Assert(translator != null);

@@ -1129,7 +1129,7 @@ namespace Microsoft.Boogie
 

         public class CyclicLiveVariableAnalysis : Microsoft.Boogie.LiveVariableAnalysis

         {

-            public static void ComputeLiveVariables(Implementation impl)

+            public new static void ComputeLiveVariables(Implementation impl)

             {

 

                 bool some_change = true;

@@ -1538,6 +1538,7 @@ namespace Microsoft.Boogie
             }

         }

 

+

         public Counterexample CreateBoogieCounterExample(RPFP rpfp, RPFP.Node root, Implementation mainImpl)

         {

             FindLabels();

@@ -1546,10 +1547,11 @@ namespace Microsoft.Boogie
               GenerateTrace(rpfp, root, orderedStateIds, mainImpl,true);

             if (CommandLineOptions.Clo.ModelViewFile != null)

             {

-                Model m = new Model();

+                Model m = root.owner.GetBackgroundModel();

                 GetModelWithStates(m, root, implName2StratifiedInliningInfo[mainImpl.Name],

                                    orderedStateIds, varSubst);

                 newCounterexample.Model = m;

+                newCounterexample.ModelHasStatesAlready = true;

             }

             return newCounterexample;

         }

diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index 9048f0f5..f6a42a43 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -566,10 +566,21 @@ namespace Microsoft.Boogie
             public List<Node> nodes = new List<Node>();

         };

 

+        /** Set the model of the background theory used in a counterexample. */

+        public void SetBackgroundModel(Model m)

+        {

+            dualModel = m;

+        }

+

+        /** Set the model of the background theory used in a counterexample. */

+        public Model GetBackgroundModel()

+        {

+            return dualModel;

+        }

 

         private int nodeCount = 0;

         private int edgeCount = 0;

-        // private Model dualModel;

+        private Model dualModel;

         // private LabeledLiterals dualLabels;

         private Stack<stack_entry> stack;

         public List<Node> nodes = new List<Node>();