extended NormalSubstituter so that it can take in a forold substitution

optimized the FailurePreservationChecker to eliminate some quantifiers

2 files changed, 95 insertions, 31 deletions

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 4f538c52..61e3bf02 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -462,7 +462,7 @@ namespace Microsoft.Boogie
             this.decls.Add(proc);

         }

 

-        private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

+        private void CreateFailurePreservationCheckerForall(Program program, ActionInfo first, ActionInfo second)

         {

             Debug.Assert(second.isNonBlocking);

             if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0)

@@ -505,7 +505,7 @@ namespace Microsoft.Boogie
             this.decls.Add(proc);

         }

 

-        private void CreateFailurePreservationCheckerOld(Program program, ActionInfo first, ActionInfo second)

+        private void CreateFailurePreservationChecker(Program program, ActionInfo first, ActionInfo second)

         {

             if (first.gateUsedGlobalVars.Intersect(second.modifiedGlobalVars).Count() == 0 && second.isNonBlocking)

                 return;

@@ -519,54 +519,50 @@ namespace Microsoft.Boogie
             inputs.AddRange(first.thatInParams);

             inputs.AddRange(second.thisInParams);

 

-            Expr transitionRelation = (new TransitionRelationComputation(program, second)).Compute();

-            Expr expr = Expr.True;

+            Expr requiresExpr = Expr.True;

             foreach (AssertCmd assertCmd in first.thatGate)

             {

-                expr = Expr.And(assertCmd.Expr, expr);

+                requiresExpr = Expr.And(assertCmd.Expr, requiresExpr);

             }

+            requiresExpr = Expr.Not(requiresExpr);

             List<Requires> requires = DisjointnessRequires(program, first, second);

-            requires.Add(new Requires(false, Expr.Not(expr)));

+            requires.Add(new Requires(false, requiresExpr));

             foreach (AssertCmd assertCmd in second.thisGate)

             {

                 requires.Add(new Requires(false, assertCmd.Expr));

             }

-            

+

             Dictionary<Variable, Expr> map = new Dictionary<Variable, Expr>();

             Dictionary<Variable, Expr> oldMap = new Dictionary<Variable, Expr>();

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

             foreach (Variable v in program.GlobalVariables())

             {

-                BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));

-                boundVars.Add(bv);

-                map[v] = new IdentifierExpr(Token.NoToken, bv);

-            }

-            foreach (Variable v in second.thisOutParams)

-            {

+                if (second.modifiedGlobalVars.Contains(v))

                 {

                     BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));

                     boundVars.Add(bv);

                     map[v] = new IdentifierExpr(Token.NoToken, bv);

                 }

+                else

                 {

-                    BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));

-                    boundVars.Add(bv);

-                    oldMap[v] = new IdentifierExpr(Token.NoToken, bv);

+                    map[v] = new OldExpr(Token.NoToken, Expr.Ident(v));

                 }

+                oldMap[v] = Expr.Ident(v);

             }

-            foreach (Variable v in second.thisAction.LocVars)

+            foreach (Variable v in second.thisOutParams)

             {

-                BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "pre_" + v.Name, v.TypedIdent.Type));

+                BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "post_" + v.Name, v.TypedIdent.Type));

                 boundVars.Add(bv);

-                oldMap[v] = new IdentifierExpr(Token.NoToken, bv);

+                map[v] = new IdentifierExpr(Token.NoToken, bv);

             }

 

-            Expr ensuresExpr = Expr.And(transitionRelation, Expr.Not(expr));

+            Expr ensuresExpr = Expr.And((new TransitionRelationComputation(program, second)).Compute(), requiresExpr);

+            Substitution subst = Substituter.SubstitutionFromHashtable(map);

+            Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);

+            ensuresExpr = Substituter.Apply(subst, oldSubst, ensuresExpr);

             if (boundVars.Count > 0)

             {

-                Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                Substitution oldSubst = Substituter.SubstitutionFromHashtable(oldMap);

-                ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, (Expr)new MySubstituter(subst, oldSubst).Visit(ensuresExpr));

+                ensuresExpr = new ExistsExpr(Token.NoToken, boundVars, ensuresExpr);

             }

             List<Ensures> ensures = new List<Ensures>();

             ensures.Add(new Ensures(false, ensuresExpr));

diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index 07ccba77..a11c93ec 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -424,6 +424,22 @@ namespace Microsoft.Boogie {
     }

 

     /// <summary>

+    /// Apply a substitution to an expression. 

+    /// Outside "old" expressions, the substitution "always" is applied; any variable not in

+    /// domain(always) is not changed.  Inside "old" expressions, apply map "forOld" to

+    /// variables in domain(forOld), apply map "always" to variables in

+    /// domain(always)-domain(forOld), and leave variable unchanged otherwise.

+    /// </summary>

+    public static Expr Apply(Substitution always, Substitution forold, Expr expr)

+    {

+        Contract.Requires(expr != null);

+        Contract.Requires(always != null);

+        Contract.Requires(forold != null);

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

+        return (Expr)new NormalSubstituter(always, forold).Visit(expr);

+    }

+

+    /// <summary>

     /// Apply a substitution to a command.  Any variables not in domain(subst)

     /// is not changed.  The substitutions applies within the "old", but the "old"

     /// expression remains.

@@ -436,6 +452,22 @@ namespace Microsoft.Boogie {
     }

 

     /// <summary>

+    /// Apply a substitution to a command.  

+    /// Outside "old" expressions, the substitution "always" is applied; any variable not in

+    /// domain(always) is not changed.  Inside "old" expressions, apply map "forOld" to

+    /// variables in domain(forOld), apply map "always" to variables in

+    /// domain(always)-domain(forOld), and leave variable unchanged otherwise.

+    /// </summary>

+    public static Cmd Apply(Substitution always, Substitution forold, Cmd cmd)

+    {

+        Contract.Requires(cmd != null);

+        Contract.Requires(always != null);

+        Contract.Requires(forold != null);

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

+        return (Cmd)new NormalSubstituter(always, forold).Visit(cmd);

+    }

+

+    /// <summary>

     /// Apply a substitution to an expression replacing "old" expressions.

     /// Outside "old" expressions, the substitution "always" is applied; any variable not in

     /// domain(always) is not changed.  Inside "old" expressions, apply map "forOld" to

@@ -466,23 +498,59 @@ namespace Microsoft.Boogie {
     }

 

     private sealed class NormalSubstituter : Duplicator {

-      private readonly Substitution/*!*/ subst;

+      private readonly Substitution/*!*/ always;

+      private readonly Substitution/*!*/ forold;

       [ContractInvariantMethod]

       void ObjectInvariant() {

-        Contract.Invariant(subst != null);

+        Contract.Invariant(always != null);

+        Contract.Invariant(forold != null);

       }

 

       public NormalSubstituter(Substitution subst)

         : base() {

         Contract.Requires(subst != null);

-        this.subst = subst;

+        this.always = subst;

+        this.forold = Substituter.SubstitutionFromHashtable(new Dictionary<Variable, Expr>());

       }

 

-      public override Expr VisitIdentifierExpr(IdentifierExpr node) {

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

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

-        Expr/*?*/ e = subst(cce.NonNull(node.Decl));

-        return e == null ? base.VisitIdentifierExpr(node) : e;

+      public NormalSubstituter(Substitution subst, Substitution forold)

+          : base()

+      {

+          Contract.Requires(subst != null);

+          this.always = subst;

+          this.forold = forold;

+      }

+

+      private bool insideOldExpr = false;

+

+      public override Expr VisitIdentifierExpr(IdentifierExpr node)

+      {

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

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

+          Expr/*?*/ e = null;

+

+          if (insideOldExpr)

+          {

+              e = forold(cce.NonNull(node.Decl));

+          }

+

+          if (e == null)

+          {

+              e = always(cce.NonNull(node.Decl));

+          }

+

+          return e == null ? base.VisitIdentifierExpr(node) : e;

+      }

+

+      public override Expr VisitOldExpr(OldExpr node)

+      {

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

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

+          bool previouslyInOld = insideOldExpr;

+          insideOldExpr = true;

+          Expr/*!*/ e = (Expr/*!*/)cce.NonNull(this.Visit(node.Expr));

+          insideOldExpr = previouslyInOld;

+          return new OldExpr(node.tok, e);

       }

     }