Worked on the verification result caching.

4 files changed, 28 insertions, 10 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 61d8cdc4..27c3594a 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1796,13 +1796,19 @@ namespace Microsoft.Boogie {
     }

     protected abstract Cmd/*!*/ ComputeDesugaring();

 

-    public void ExtendDesugaring(IEnumerable<Cmd> before, IEnumerable<Cmd> after)

+    public void ExtendDesugaring(IEnumerable<Cmd> before, IEnumerable<Cmd> beforePreconditionCheck, IEnumerable<Cmd> after)

     {

       var desug = Desugaring;

       var stCmd = desug as StateCmd;

       if (stCmd != null)

       {

         stCmd.Cmds.InsertRange(0, before);

+        var idx = stCmd.Cmds.FindIndex(c => c is AssertCmd || c is HavocCmd || c is AssumeCmd);

+        if (idx < 0)

+        {

+          idx = 0;

+        }

+        stCmd.Cmds.InsertRange(idx, beforePreconditionCheck);

         stCmd.Cmds.AddRange(after);

       }

       else if (desug != null)

@@ -2473,8 +2479,8 @@ namespace Microsoft.Boogie {
       #endregion

 

       #region assume Post[ins, outs, old(frame) := cins, couts, cframe]

-      calleeSubstitution = Substituter.SubstitutionFromHashtable(substMap);

-      calleeSubstitutionOld = Substituter.SubstitutionFromHashtable(substMapOld);

+      calleeSubstitution = Substituter.SubstitutionFromHashtable(substMap, true);

+      calleeSubstitutionOld = Substituter.SubstitutionFromHashtable(substMapOld, true);

       foreach (Ensures/*!*/ e in this.Proc.Ensures) {

         Contract.Assert(e != null);

         Expr copy = Substituter.ApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, e.Condition);

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 565b2f06..d9a35174 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -479,29 +479,40 @@ namespace Microsoft.Boogie {
   public delegate Expr/*?*/ Substitution(Variable/*!*/ v);

 

   public static class Substituter {

-    public static Substitution SubstitutionFromHashtable(Dictionary<Variable, Expr> map) {

+    public static Substitution SubstitutionFromHashtable(Dictionary<Variable, Expr> map, bool fallBackOnName = false)

+    {

       Contract.Requires(map != null);

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

       // TODO: With Whidbey, could use anonymous functions.

-      return new Substitution(new CreateSubstitutionClosure(map).Method);

+      return new Substitution(new CreateSubstitutionClosure(map, fallBackOnName).Method);

     }

     private sealed class CreateSubstitutionClosure {

       Dictionary<Variable /*!*/, Expr /*!*/>/*!*/ map;

+      Dictionary<string /*!*/, Expr /*!*/>/*!*/ nameMap;

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(map != null);

       }

 

-      public CreateSubstitutionClosure(Dictionary<Variable, Expr> map)

+      public CreateSubstitutionClosure(Dictionary<Variable, Expr> map, bool fallBackOnName = false)

         : base() {

         Contract.Requires(map != null);

         this.map = map;

+        if (fallBackOnName)

+        {

+          this.nameMap = map.ToDictionary(kv => kv.Key.Name, kv => kv.Value);

+        }

       }

       public Expr/*?*/ Method(Variable v) {

         Contract.Requires(v != null);

         if(map.ContainsKey(v)) {

           return map[v];

         }

+        Expr e;

+        if (nameMap != null && nameMap.TryGetValue(v.Name, out e))

+        {

+          return e;

+        }

         return null;

       }

     }

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index f8b29a69..ba995cba 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -223,6 +223,7 @@ namespace Microsoft.Boogie
           && node.AssignedAssumptionVariable == null)

       {

         var before = new List<Cmd>();

+        var beforePrecondtionCheck = new List<Cmd>();

         var after = new List<Cmd>();

         Expr assumedExpr = new LiteralExpr(Token.NoToken, false);

         var canUseSpecs = DependencyCollector.AllFunctionDependenciesAreDefinedAndUnchanged(oldProc, Program);

@@ -232,7 +233,7 @@ namespace Microsoft.Boogie
           if (precond != null)

           {

             var assume = new AssumeCmd(Token.NoToken, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

-            before.Add(assume);

+            beforePrecondtionCheck.Add(assume);

           }

 

           assumedExpr = node.Postcondition(oldProc, Program);

@@ -268,7 +269,7 @@ namespace Microsoft.Boogie
           var assumed = new AssignCmd(Token.NoToken, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

           after.Add(assumed);

         }

-        node.ExtendDesugaring(before, after);

+        node.ExtendDesugaring(before, beforePrecondtionCheck, after);

       }

 

       return result;

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index db470ef3..56e0aa7f 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -76,8 +76,8 @@ Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not ho
 Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.

 

 Boogie program verifier finished with 0 verified, 1 error

-Snapshots11.v1.bpl(7,5): Error BP5002: A precondition for this call might not hold.

-Snapshots11.v1.bpl(13,3): Related location: This is the precondition that might not hold.

+Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.

+Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.

 

 Boogie program verifier finished with 0 verified, 1 error