various bug fixes

added "cnst" feature

4 files changed, 252 insertions, 128 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 0b6cf232..f7b14836 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -4,6 +4,7 @@ using System.Linq;
 using System.Text;

 using System.Threading.Tasks;

 using Microsoft.Boogie;

+using System.Diagnostics;

 

 namespace Microsoft.Boogie

 {

@@ -13,7 +14,9 @@ namespace Microsoft.Boogie
         {

             if (iter == null) return null;

             iter.Next = RemoveLinearAttribute(iter.Next);

-            return (QKeyValue.FindStringAttribute(iter, "linear") == null) ? iter : iter.Next;

+            bool iterIsNonLinear = QKeyValue.FindStringAttribute(iter, "linear") == null && 

+                                   QKeyValue.FindStringAttribute(iter, "cnst") == null;

+            return iterIsNonLinear ? iter : iter.Next;

         }

 

         public override Variable VisitVariable(Variable node)

@@ -23,14 +26,20 @@ namespace Microsoft.Boogie
         }

     }

 

+    public enum LinearKind {

+        LINEAR,

+        CONST

+    }

+

     public class LinearTypeChecker : StandardVisitor

     {

         public Program program;

         public int errorCount;

         public CheckingContext checkingContext;

         public Dictionary<string, Type> domainNameToType;

-        public Dictionary<Absy, HashSet<Variable>> availableLinearVars;

-        public Dictionary<Variable, string> inoutParamToDomainName;

+        private Dictionary<Absy, HashSet<Variable>> availableLinearVars;

+        public Dictionary<Variable, LinearQualifier> inParamToLinearQualifier;

+        public Dictionary<Variable, string> outParamToDomainName;

         public Dictionary<Variable, string> varToDomainName;

         public Dictionary<Variable, string> globalVarToDomainName;

         public Dictionary<string, LinearDomain> linearDomains;

@@ -42,7 +51,8 @@ namespace Microsoft.Boogie
             this.checkingContext = new CheckingContext(null);

             this.domainNameToType = new Dictionary<string, Type>();

             this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();

-            this.inoutParamToDomainName = new Dictionary<Variable, string>();

+            this.inParamToLinearQualifier = new Dictionary<Variable, LinearQualifier>();

+            this.outParamToDomainName = new Dictionary<Variable, string>();

             this.varToDomainName = new Dictionary<Variable, string>();

             this.linearDomains = new Dictionary<string, LinearDomain>();

         }

@@ -77,10 +87,11 @@ namespace Microsoft.Boogie
             HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);

             for (int i = 0; i < node.InParams.Count; i++)

             {

-                string domainName = FindDomainName(node.Proc.InParams[i]);

+                Variable v = node.Proc.InParams[i];

+                string domainName = FindDomainName(v);

                 if (domainName != null)

                 {

-                    inoutParamToDomainName[node.InParams[i]] = domainName;

+                    inParamToLinearQualifier[node.InParams[i]] = new LinearQualifier(domainName, FindLinearKind(v));

                     start.Add(node.InParams[i]);

                 }

             }

@@ -89,7 +100,7 @@ namespace Microsoft.Boogie
                 string domainName = FindDomainName(node.Proc.OutParams[i]);

                 if (domainName != null)

                 {

-                    inoutParamToDomainName[node.OutParams[i]] = domainName;

+                    outParamToDomainName[node.OutParams[i]] = domainName;

                 }

             }

             

@@ -144,6 +155,29 @@ namespace Microsoft.Boogie
             }

             return impl;

         }

+        public void AddAvailableVars(CallCmd callCmd, HashSet<Variable> start)

+        {

+            foreach (IdentifierExpr ie in callCmd.Outs)

+            {

+                if (FindDomainName(ie.Decl) == null) continue;

+                start.Add(ie.Decl);

+            }

+            for (int i = 0; i < callCmd.Proc.InParams.Count; i++)

+            {

+                IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;

+                if (ie == null) continue;

+                Variable v = callCmd.Proc.InParams[i];

+                if (FindDomainName(v) == null || FindLinearKind(v) == LinearKind.LINEAR) continue;

+                start.Add(ie.Decl);

+            }

+        }

+        public void AddAvailableVars(ParCallCmd parCallCmd, HashSet<Variable> start)

+        {

+            foreach (CallCmd callCmd in parCallCmd.CallCmds)

+            {

+                AddAvailableVars(callCmd, start);

+            }

+        }

         private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {

             HashSet<Variable> start = new HashSet<Variable>(availableLinearVars[b]);

             foreach (Cmd cmd in b.Cmds)

@@ -155,13 +189,17 @@ namespace Microsoft.Boogie
                     {

                         if (FindDomainName(assignCmd.Lhss[i].DeepAssignedVariable) == null) continue;

                         IdentifierExpr ie = assignCmd.Rhss[i] as IdentifierExpr;

-                        if (start.Contains(ie.Decl))

+                        if (!start.Contains(ie.Decl))

                         {

-                            start.Remove(ie.Decl);

+                            Error(ie, "unavailable source for a linear read"); 

                         }

-                        else

+                        else if (FindLinearKind(ie.Decl) == LinearKind.CONST)

                         {

-                            Error(ie, "unavailable source for a linear read");

+                            Error(ie, "const linear vars cannot occur on the right side of a linear assignment");

+                        }

+                        else 

+                        {

+                            start.Remove(ie.Decl);

                         }

                     }

                     foreach (AssignLhs assignLhs in assignCmd.Lhss)

@@ -183,19 +221,15 @@ namespace Microsoft.Boogie
                         IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;

                         if (start.Contains(ie.Decl))

                         {

-                            start.Remove(ie.Decl);

+                            start.Remove(ie.Decl); 

                         }

                         else

                         {

-                            Error(ie, "unavailable source for a linear read");

+                            Error(ie, "unavailable source for a linear read"); 

                         }

                     }

                     availableLinearVars[callCmd] = new HashSet<Variable>(start);

-                    foreach (IdentifierExpr ie in callCmd.Outs)

-                    {

-                        if (FindDomainName(ie.Decl) == null) continue;

-                        start.Add(ie.Decl);

-                    }

+                    AddAvailableVars(callCmd, start);

                 }

                 else if (cmd is ParCallCmd)

                 {

@@ -221,14 +255,7 @@ namespace Microsoft.Boogie
                         }

                     }

                     availableLinearVars[parCallCmd] = new HashSet<Variable>(start);

-                    foreach (CallCmd callCmd in parCallCmd.CallCmds)

-                    {

-                        foreach (IdentifierExpr ie in callCmd.Outs)

-                        {

-                            if (FindDomainName(ie.Decl) == null) continue;

-                            start.Add(ie.Decl);

-                        }

-                    }

+                    AddAvailableVars(parCallCmd, start);

                 }

                 else if (cmd is HavocCmd)

                 {

@@ -254,9 +281,37 @@ namespace Microsoft.Boogie
         {

             if (globalVarToDomainName.ContainsKey(v))

                 return globalVarToDomainName[v];

-            if (inoutParamToDomainName.ContainsKey(v))

-                return inoutParamToDomainName[v];

-            return QKeyValue.FindStringAttribute(v.Attributes, "linear");

+            if (inParamToLinearQualifier.ContainsKey(v))

+                return inParamToLinearQualifier[v].domainName;

+            if (outParamToDomainName.ContainsKey(v))

+                return outParamToDomainName[v];

+            string domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");

+            if (domainName != null)

+                return domainName;

+            return QKeyValue.FindStringAttribute(v.Attributes, "cnst");

+        }

+        public LinearKind FindLinearKind(Variable v)

+        {

+            if (globalVarToDomainName.ContainsKey(v))

+                return LinearKind.LINEAR;

+            if (inParamToLinearQualifier.ContainsKey(v))

+                return inParamToLinearQualifier[v].kind;

+            if (outParamToDomainName.ContainsKey(v))

+                return LinearKind.LINEAR;

+

+            if (QKeyValue.FindStringAttribute(v.Attributes, "cnst") != null)

+            {

+                return LinearKind.CONST;

+            }

+            else if (QKeyValue.FindStringAttribute(v.Attributes, "linear") != null)

+            { 

+                return LinearKind.LINEAR; 

+            }

+            else

+            {

+                Debug.Assert(false);

+                return LinearKind.CONST;

+            }

         }

         public override Variable VisitVariable(Variable node)

         {

@@ -364,6 +419,11 @@ namespace Microsoft.Boogie
                     Error(node, "Only local linear variable can be an actual input parameter of a procedure call");

                     continue;

                 }

+                if (FindLinearKind(formal) == LinearKind.LINEAR && FindLinearKind(actual.Decl) == LinearKind.CONST)

+                {

+                    Error(node, "Only non-const linear variable can be an actual parameter to a non-const input parameter of a procedure call");

+                    continue;

+                }

                 if (inVars.Contains(actual.Decl))

                 {

                     Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name));

@@ -420,7 +480,7 @@ namespace Microsoft.Boogie
             return base.VisitParCallCmd(node);

         }

 

-        private IEnumerable<Variable> AvailableLinearVars(Absy absy)

+        public IEnumerable<Variable> AvailableLinearVars(Absy absy)

         {

             if (availableLinearVars.ContainsKey(absy))

                 return availableLinearVars[absy];

@@ -493,13 +553,13 @@ namespace Microsoft.Boogie
                                 Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

                                 foreach (var domainName in linearDomains.Keys)

                                 {

-                                    domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);

+                                    domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);

                                 }

                                 foreach (Variable v in AvailableLinearVars(callCmd))

                                 {

                                     var domainName = FindDomainName(v);

                                     var domain = linearDomains[domainName];

-                                    IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

+                                    IdentifierExpr ie = Expr.Ident(v);

                                     var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), 

                                                             new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), domainNameToExpr[domainName] });

                                     expr.Resolve(new ResolutionContext(null));

@@ -634,9 +694,9 @@ namespace Microsoft.Boogie
             int count = 0;

             foreach (Variable v in scope)

             {

-                IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

+                IdentifierExpr ie = Expr.Ident(v);

                 Expr e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstInt), new List<Expr>{ new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(count++)) } );

-                e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List<Expr> { new IdentifierExpr(Token.NoToken, partition), e } );

+                e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapEqInt), new List<Expr> { Expr.Ident(partition), e } );

                 e = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapImpBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : Singleton(ie, domainName), e } );

                 e = Expr.Binary(BinaryOperator.Opcode.Eq, e, new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.True }));

                 disjointExpr = Expr.Binary(BinaryOperator.Opcode.And, e, disjointExpr);

@@ -648,6 +708,17 @@ namespace Microsoft.Boogie
         }

     }

 

+    public class LinearQualifier

+    {

+        public string domainName;

+        public LinearKind kind;

+        public LinearQualifier(string domainName, LinearKind kind)

+        {

+            this.domainName = domainName;

+            this.kind = kind;

+        }

+    }

+

     public class LinearDomain

     {

         public Microsoft.Boogie.Type elementType;

@@ -676,11 +747,11 @@ namespace Microsoft.Boogie
             else

             {

                 BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));

-                IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);

+                IdentifierExpr aie = Expr.Ident(a);

                 BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));

-                IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);

+                IdentifierExpr bie = Expr.Ident(b);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

-                IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

+                IdentifierExpr xie = Expr.Ident(x);

                 var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapOrBool), new List<Expr> { aie, bie } );

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie } );

                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Or,

@@ -704,11 +775,11 @@ namespace Microsoft.Boogie
             else

             {

                 BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeBool));

-                IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);

+                IdentifierExpr aie = Expr.Ident(a);

                 BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeBool));

-                IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);

+                IdentifierExpr bie = Expr.Ident(b);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

-                IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

+                IdentifierExpr xie = Expr.Ident(x);

                 var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapImpBool), new List<Expr> { aie, bie });

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });

                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Imp,

@@ -731,7 +802,7 @@ namespace Microsoft.Boogie
             else

             {

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

-                IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

+                IdentifierExpr xie = Expr.Ident(x);

                 var trueTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), 

                                            new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstBool), new List<Expr> { Expr.True }), xie });

                 var trueAxiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { x }, trueTerm);

@@ -755,11 +826,11 @@ namespace Microsoft.Boogie
             else

             {

                 BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", mapTypeInt));

-                IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);

+                IdentifierExpr aie = Expr.Ident(a);

                 BoundVariable b = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "b", mapTypeInt));

-                IdentifierExpr bie = new IdentifierExpr(Token.NoToken, b);

+                IdentifierExpr bie = Expr.Ident(b);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

-                IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

+                IdentifierExpr xie = Expr.Ident(x);

                 var mapApplTerm = new NAryExpr(Token.NoToken, new FunctionCall(mapEqInt), new List<Expr> { aie, bie });

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { mapApplTerm, xie });

                 var rhsTerm = Expr.Binary(BinaryOperator.Opcode.Eq,

@@ -782,9 +853,9 @@ namespace Microsoft.Boogie
             else

             {

                 BoundVariable a = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "a", Type.Int));

-                IdentifierExpr aie = new IdentifierExpr(Token.NoToken, a);

+                IdentifierExpr aie = Expr.Ident(a);

                 BoundVariable x = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "x", elementType));

-                IdentifierExpr xie = new IdentifierExpr(Token.NoToken, x);

+                IdentifierExpr xie = Expr.Ident(x);

                 var lhsTerm = new NAryExpr(Token.NoToken, new MapSelect(Token.NoToken, 1), new List<Expr> { new NAryExpr(Token.NoToken, new FunctionCall(mapConstInt), new List<Expr> { aie }), xie });

                 var axiomExpr = new ForallExpr(Token.NoToken, new List<Variable> { a, x }, Expr.Binary(BinaryOperator.Opcode.Eq, lhsTerm, aie));

                 axiomExpr.Typecheck(new TypecheckingContext(null));

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 78943c1b..ce6a3cdf 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -114,15 +114,10 @@ namespace Microsoft.Boogie
             private ActionInfo first;  // corresponds to that*

             private ActionInfo second; // corresponds to this*

             private Stack<Cmd> path;

-            private Expr transitionRelation;

+            private List<PathInfo> paths;

 

-            public TransitionRelationComputation(Program program, ActionInfo second)

+            public TransitionRelationComputation(Program program, ActionInfo second) : this(program, null, second)

             {

-                this.program = program;

-                this.first = null;

-                this.second = second;

-                this.path = new Stack<Cmd>();

-                this.transitionRelation = Expr.False;

             }

 

             public TransitionRelationComputation(Program program, ActionInfo first, ActionInfo second)

@@ -131,27 +126,27 @@ namespace Microsoft.Boogie
                 this.first = first;

                 this.second = second;

                 this.path = new Stack<Cmd>();

-                this.transitionRelation = Expr.False;

-            }

-

-            public Expr Compute()

-            {

+                this.paths = new List<PathInfo>();

                 List<IdentifierExpr> havocVars = new List<IdentifierExpr>();

-                second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v)));

-                second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v)));

+                this.second.thisOutParams.ForEach(v => havocVars.Add(Expr.Ident(v)));

+                this.second.thisAction.LocVars.ForEach(v => havocVars.Add(Expr.Ident(v)));

                 if (havocVars.Count > 0)

                 {

                     HavocCmd havocCmd = new HavocCmd(Token.NoToken, havocVars);

                     path.Push(havocCmd);

                 }

-                Search(second.thisAction.Blocks[0], false);

-                return transitionRelation;

+                Search(this.second.thisAction.Blocks[0], false);

             }

 

-            private void Substitute(Dictionary<Variable, Expr> map, ref Expr returnExpr, ref Dictionary<Variable, Expr> varToExpr)

+            private void Substitute(Dictionary<Variable, Expr> map, ref List<Expr> pathExprs, ref Dictionary<Variable, Expr> varToExpr)

             {

                 Substitution subst = Substituter.SubstitutionFromHashtable(map);

-                returnExpr = Substituter.Apply(subst, returnExpr);

+                List<Expr> oldPathExprs = pathExprs;

+                pathExprs = new List<Expr>();

+                foreach (Expr pathExpr in oldPathExprs)

+                {

+                    pathExprs.Add(Substituter.Apply(subst, pathExpr));

+                }

                 Dictionary<Variable, Expr> oldVarToExpr = varToExpr;

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

                 foreach (Variable v in oldVarToExpr.Keys)

@@ -164,18 +159,17 @@ namespace Microsoft.Boogie
             {

                 public HashSet<Variable> existsVars;

                 public Dictionary<Variable, Expr> varToExpr;

-                public Expr pathExpr;

+                public List<Expr> pathExprs;

 

-                public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, Expr pathExpr)

+                public PathInfo(HashSet<Variable> existsVars, Dictionary<Variable, Expr> varToExpr, List<Expr> pathExprs)

                 {

                     this.existsVars = existsVars;

                     this.varToExpr = varToExpr;

-                    this.pathExpr = pathExpr;

+                    this.pathExprs = pathExprs;

                 }

             }

 

-            private List<PathInfo> paths = new List<PathInfo>();

-            private Expr CalculatePathCondition()

+            private void AddPath()

             {

                 HashSet<Variable> existsVars = new HashSet<Variable>();

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

@@ -194,14 +188,14 @@ namespace Microsoft.Boogie
                 {

                     varToExpr[v] = Expr.Ident(v);

                 }

-                Expr pathExpr = Expr.True;

+                List<Expr> pathExprs = new List<Expr>();

                 int boundVariableCount = 0;

                 foreach (Cmd cmd in path)

                 {

                     if (cmd is AssumeCmd)

                     {

                         AssumeCmd assumeCmd = cmd as AssumeCmd;

-                        pathExpr = Expr.And(assumeCmd.Expr, pathExpr);

+                        pathExprs.Add(assumeCmd.Expr);

                     }

                     else if (cmd is AssignCmd)

                     {

@@ -211,7 +205,7 @@ namespace Microsoft.Boogie
                         {

                             map[assignCmd.Lhss[k].DeepAssignedVariable] = assignCmd.Rhss[k];

                         }

-                        Substitute(map, ref pathExpr, ref varToExpr);

+                        Substitute(map, ref pathExprs, ref varToExpr);

                     }

                     else if (cmd is HavocCmd)

                     {

@@ -220,19 +214,25 @@ namespace Microsoft.Boogie
                         foreach (IdentifierExpr ie in havocCmd.Vars)

                         {

                             BoundVariable bv = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, "#tmp_" + boundVariableCount++, ie.Decl.TypedIdent.Type));

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

+                            map[ie.Decl] = Expr.Ident(bv);

                             existsVars.Add(bv);

                         }

-                        Substitute(map, ref pathExpr, ref varToExpr);

+                        Substitute(map, ref pathExprs, ref varToExpr);

                     }

                     else

                     {

                         Debug.Assert(false);

                     }

                 }

-                paths.Add(new PathInfo(existsVars, varToExpr, pathExpr));

+                paths.Add(new PathInfo(new HashSet<Variable>(existsVars), varToExpr, pathExprs));

+            }

 

+            private Expr CalculatePathCondition(PathInfo path)

+            {

+                HashSet<Variable> existsVars = path.existsVars;

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

+

+                Dictionary<Variable, Expr> varToExpr = path.varToExpr;

                 foreach (Variable v in varToExpr.Keys)

                 {

                     IdentifierExpr ie = varToExpr[v] as IdentifierExpr;

@@ -242,17 +242,58 @@ namespace Microsoft.Boogie
                         existsVars.Remove(ie.Decl);

                     }

                 }

-                pathExpr = (new MyDuplicator()).VisitExpr(pathExpr);

+

+                List<Expr> pathExprs = new List<Expr>();

+                path.pathExprs.ForEach(x => pathExprs.Add((new MyDuplicator()).VisitExpr(x)));

+                foreach (Expr x in pathExprs)

+                {

+                    Variable boundVar;

+                    Expr boundVarExpr;

+                    if (InferSubstitution(x, out boundVar, out boundVarExpr) && existsVars.Contains(boundVar))

+                    {

+                        existsMap[boundVar] = boundVarExpr;

+                        existsVars.Remove(boundVar);

+                    }

+                }

+

+                Expr returnExpr = Expr.True;

+                pathExprs.ForEach(x => Expr.And(returnExpr, x)); 

                 foreach (Variable v in varToExpr.Keys)

                 {

-                    pathExpr = Expr.And(pathExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));

+                    returnExpr = Expr.And(returnExpr, Expr.Eq(Expr.Ident(v), (new MyDuplicator()).VisitExpr(varToExpr[v])));

                 }

-                pathExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), pathExpr);

+                returnExpr = Substituter.Apply(Substituter.SubstitutionFromHashtable(existsMap), returnExpr);

                 if (existsVars.Count > 0)

                 {

-                    pathExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), pathExpr);

+                    returnExpr = new ExistsExpr(Token.NoToken, new List<Variable>(existsVars), returnExpr);

                 }

-                return pathExpr;

+                return returnExpr;

+            }

+

+            bool InferSubstitution(Expr x, out Variable var, out Expr expr)

+            {

+                var = null;

+                expr = null;

+                NAryExpr naryExpr = x as NAryExpr;

+                if (naryExpr == null || naryExpr.Fun.FunctionName != "==")

+                {

+                    return false;

+                }

+                IdentifierExpr arg0 = naryExpr.Args[0] as IdentifierExpr;

+                if (arg0 != null && arg0.Decl is BoundVariable)

+                {

+                    var = arg0.Decl;

+                    expr = naryExpr.Args[1];

+                    return true;

+                }

+                IdentifierExpr arg1 = naryExpr.Args[1] as IdentifierExpr;

+                if (arg1 != null && arg1.Decl is BoundVariable)

+                {

+                    var = arg1.Decl;

+                    expr = naryExpr.Args[0];

+                    return true;

+                }

+                return false;

             }

 

             public Expr LeftMoverCompute(Expr failureExpr)

@@ -261,7 +302,22 @@ namespace Microsoft.Boogie
                 foreach (PathInfo path in paths)

                 {

                     Expr expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(path.varToExpr), failureExpr);

-                    expr = Expr.And(path.pathExpr, expr);

+                    Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

+                    foreach (Expr x in path.pathExprs)

+                    {

+                        Variable boundVar;

+                        Expr boundVarExpr;

+                        if (InferSubstitution(x, out boundVar, out boundVarExpr) && path.existsVars.Contains(boundVar))

+                        {

+                            subst[boundVar] = boundVarExpr;

+                            path.existsVars.Remove(boundVar);

+                        }

+                        else

+                        {

+                            expr = Expr.And(expr, x);

+                        }

+                    }

+                    expr = Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), expr);

                     expr = new OldExpr(Token.NoToken, expr);

                     if (path.existsVars.Count > 0)

                     {

@@ -272,6 +328,16 @@ namespace Microsoft.Boogie
                 return returnExpr;

             }

 

+            public Expr TransitionRelationCompute()

+            {

+                Expr transitionRelation = Expr.False;

+                foreach (PathInfo path in paths)

+                {

+                    transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition(path));

+                }

+                return transitionRelation;

+            }

+

             private void Search(Block b, bool inFirst)

             {

                 int pathSizeAtEntry = path.Count;

@@ -283,7 +349,7 @@ namespace Microsoft.Boogie
                 {

                     if (first == null || inFirst)

                     {

-                        transitionRelation = Expr.Or(transitionRelation, CalculatePathCondition());

+                        AddPath();

                     }

                     else

                     {

@@ -418,13 +484,13 @@ namespace Microsoft.Boogie
             blocks.AddRange(secondBlocks);

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

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

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

+            Expr transitionRelation = (new TransitionRelationComputation(program, first, second)).TransitionRelationCompute();

             Ensures ensureCheck = new Ensures(false, transitionRelation);

             ensureCheck.ErrorData = string.Format("Commutativity check between {0} and {1} failed", first.proc.Name, second.proc.Name);

             ensures.Add(ensureCheck);

             string checkerName = string.Format("CommutativityChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

+            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, blocks);

             impl.Proc = proc;

@@ -461,7 +527,7 @@ namespace Microsoft.Boogie
             }

             string checkerName = string.Format("GatePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

+            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, outputs, locals, secondBlocks);

             impl.Proc = proc;

@@ -496,9 +562,7 @@ namespace Microsoft.Boogie
                 requires.Add(new Requires(false, assertCmd.Expr));

             }

 

-            TransitionRelationComputation transitionRelationComputation = new TransitionRelationComputation(program, second);

-            transitionRelationComputation.Compute();

-            Expr ensuresExpr = transitionRelationComputation.LeftMoverCompute(failureExpr);

+            Expr ensuresExpr = (new TransitionRelationComputation(program, second)).LeftMoverCompute(failureExpr);

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

             Ensures ensureCheck = new Ensures(false, ensuresExpr);

             ensureCheck.ErrorData = string.Format("Gate failure of {0} not preserved by {1}", first.proc.Name, second.proc.Name);

@@ -508,7 +572,7 @@ namespace Microsoft.Boogie
             blocks.Add(new Block(Token.NoToken, "L", new List<Cmd>(), new ReturnCmd(Token.NoToken)));

             string checkerName = string.Format("FailurePreservationChecker_{0}_{1}", first.proc.Name, second.proc.Name);

             List<IdentifierExpr> globalVars = new List<IdentifierExpr>();

-            program.GlobalVariables().Iter(x => globalVars.Add(new IdentifierExpr(Token.NoToken, x)));

+            program.GlobalVariables().Iter(x => globalVars.Add(Expr.Ident(x)));

             Procedure proc = new Procedure(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), requires, globalVars, ensures);

             Implementation impl = new Implementation(Token.NoToken, checkerName, new List<TypeVariable>(), inputs, new List<Variable>(), new List<Variable>(), blocks);

             impl.Proc = proc;

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index 435e72bf..d9f23cb3 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -253,7 +253,7 @@ namespace Microsoft.Boogie
             globalMods = new List<IdentifierExpr>();

             foreach (Variable g in program.GlobalVariables())

             {

-                globalMods.Add(new IdentifierExpr(Token.NoToken, g));

+                globalMods.Add(Expr.Ident(g));

             }

             asyncAndParallelCallDesugarings = new Dictionary<string, Procedure>();

             yieldCheckerProcs = new List<Procedure>();

@@ -261,9 +261,9 @@ namespace Microsoft.Boogie
             yieldProc = null;

         }

 

-        private HashSet<Variable> AvailableLinearVars(Absy absy)

+        private IEnumerable<Variable> AvailableLinearVars(Absy absy)

         {

-            return linearTypeChecker.availableLinearVars[absyMap[absy]];

+            return linearTypeChecker.AvailableLinearVars(absyMap[absy]);

         }

 

         private void AddCallToYieldProc(IToken tok, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)

@@ -328,12 +328,12 @@ namespace Microsoft.Boogie
             }

         }

 

-        private Dictionary<string, Expr> ComputeAvailableExprs(HashSet<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)

+        private Dictionary<string, Expr> ComputeAvailableExprs(IEnumerable<Variable> availableLinearVars, Dictionary<string, Variable> domainNameToInputVar)

         {

             Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

             foreach (var domainName in linearTypeChecker.linearDomains.Keys)

             {

-                var expr = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);

+                var expr = Expr.Ident(domainNameToInputVar[domainName]);

                 expr.Resolve(new ResolutionContext(null));

                 expr.Typecheck(new TypecheckingContext(null));

                 domainNameToExpr[domainName] = expr;

@@ -342,7 +342,7 @@ namespace Microsoft.Boogie
             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 var domain = linearTypeChecker.linearDomains[domainName];

-                IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

+                IdentifierExpr ie = Expr.Ident(v);

                 var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] });

                 expr.Resolve(new ResolutionContext(null));

                 expr.Typecheck(new TypecheckingContext(null));

@@ -357,13 +357,13 @@ namespace Microsoft.Boogie
             List<Expr> rhss = new List<Expr>();

             foreach (var domainName in linearTypeChecker.linearDomains.Keys)

             {

-                lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName])));

+                lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));

                 rhss.Add(domainNameToExpr[domainName]);

             }

             foreach (Variable g in ogOldGlobalMap.Keys)

             {

                 lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ogOldGlobalMap[g])));

-                rhss.Add(new IdentifierExpr(Token.NoToken, g));

+                rhss.Add(Expr.Ident(g));

             }

             if (lhss.Count > 0)

             {

@@ -446,13 +446,13 @@ namespace Microsoft.Boogie
                     {

                         Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), true);

                         inParams.Add(y);

-                        map[x] = new IdentifierExpr(Token.NoToken, y);

+                        map[x] = Expr.Ident(y);

                     }

                     foreach (Variable x in callCmd.Proc.OutParams)

                     {

                         Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_{0}_{1}", count, x.Name), x.TypedIdent.Type), false);

                         outParams.Add(y);

-                        map[x] = new IdentifierExpr(Token.NoToken, y);

+                        map[x] = Expr.Ident(y);

                     }

                     Contract.Assume(callCmd.Proc.TypeParameters.Count == 0);

                     Substitution subst = Substituter.SubstitutionFromHashtable(map);

@@ -488,7 +488,7 @@ namespace Microsoft.Boogie
                 Variable inParam = proc.InParams[i];

                 Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

                 locals.Add(copy);

-                map[proc.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);

+                map[proc.InParams[i]] = Expr.Ident(copy);

             }

             {

                 int i = proc.InParams.Count - linearTypeChecker.linearDomains.Count;

@@ -497,7 +497,7 @@ namespace Microsoft.Boogie
                     Variable inParam = proc.InParams[i];

                     Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);

                     inputs.Add(copy);

-                    map[proc.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);

+                    map[proc.InParams[i]] = Expr.Ident(copy);

                     i++;

                 }

             }

@@ -507,7 +507,7 @@ namespace Microsoft.Boogie
                 Variable outParam = proc.OutParams[i];

                 var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));

                 locals.Add(copy);

-                map[proc.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);

+                map[proc.OutParams[i]] = Expr.Ident(copy);

             }

             foreach (IdentifierExpr ie in globalMods)

             {

@@ -594,7 +594,7 @@ namespace Microsoft.Boogie
                 Variable inParam = decl.InParams[i];

                 Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));

                 locals.Add(copy);

-                map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);

+                map[decl.InParams[i]] = Expr.Ident(copy);

             }

             {

                 int i = decl.InParams.Count - linearTypeChecker.linearDomains.Count;

@@ -603,7 +603,7 @@ namespace Microsoft.Boogie
                     Variable inParam = decl.InParams[i];

                     Variable copy = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type), true);

                     inputs.Add(copy);

-                    map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);

+                    map[decl.InParams[i]] = Expr.Ident(copy);

                     i++;

                 }

             }

@@ -612,7 +612,7 @@ namespace Microsoft.Boogie
                 Variable outParam = decl.OutParams[i];

                 var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));

                 locals.Add(copy);

-                map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy);

+                map[decl.OutParams[i]] = Expr.Ident(copy);

             }

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

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

@@ -740,7 +740,7 @@ namespace Microsoft.Boogie
             foreach (Variable local in impl.LocVars)

             {

                 var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type));

-                map[local] = new IdentifierExpr(Token.NoToken, copy);

+                map[local] = Expr.Ident(copy);

             }

             Dictionary<Variable, Variable> ogOldGlobalMap = new Dictionary<Variable, Variable>();

             foreach (IdentifierExpr ie in globalMods)

@@ -777,7 +777,7 @@ namespace Microsoft.Boogie
                         foroldMap[ie.Decl] = Expr.Ident(ogOldGlobalMap[ie.Decl]);

                     }

                     Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap);

-                    Expr betaExpr = new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo).Compute();

+                    Expr betaExpr = (new MoverCheck.TransitionRelationComputation(moverTypeChecker.program, actionInfo)).TransitionRelationCompute();

                     beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr);

                     Expr alphaExpr = Expr.True;

                     foreach (AssertCmd assertCmd in actionInfo.thisGate)

@@ -868,11 +868,7 @@ namespace Microsoft.Boogie
                         if (callCmd.IsAsync || QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

                         {

                             HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(callCmd));

-                            foreach (IdentifierExpr ie in callCmd.Outs)

-                            {

-                                if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue;

-                                availableLinearVars.Add(ie.Decl);

-                            }

+                            linearTypeChecker.AddAvailableVars(callCmd, availableLinearVars);

                             Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);

                             AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

                         }

@@ -888,14 +884,7 @@ namespace Microsoft.Boogie
                             newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Or(Expr.Ident(pc), alpha)));

                         }

                         HashSet<Variable> availableLinearVars = new HashSet<Variable>(AvailableLinearVars(parCallCmd));

-                        foreach (CallCmd callCmd in parCallCmd.CallCmds)

-                        {

-                            foreach (IdentifierExpr ie in callCmd.Outs)

-                            {

-                                if (linearTypeChecker.FindDomainName(ie.Decl) == null) continue;

-                                availableLinearVars.Add(ie.Decl);

-                            }

-                        }

+                        linearTypeChecker.AddAvailableVars(parCallCmd, availableLinearVars);

                         Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(availableLinearVars, domainNameToInputVar);

                         AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

                     }

@@ -966,7 +955,7 @@ namespace Microsoft.Boogie
                 }

                 foreach (Variable v in ogOldGlobalMap.Keys)

                 {

-                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, new IdentifierExpr(Token.NoToken, v), Expr.Ident(ogOldGlobalMap[v]))));

+                    newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(v), Expr.Ident(ogOldGlobalMap[v]))));

                 }

                 newCmds.AddRange(header.Cmds);

                 header.Cmds = newCmds;

@@ -986,7 +975,7 @@ namespace Microsoft.Boogie
                 Dictionary<string, Expr> domainNameToExpr = new Dictionary<string, Expr>();

                 foreach (var domainName in linearTypeChecker.linearDomains.Keys)

                 {

-                    domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);

+                    domainNameToExpr[domainName] = Expr.Ident(domainNameToInputVar[domainName]);

                 }

                 for (int i = 0; i < impl.InParams.Count - linearTypeChecker.linearDomains.Count; i++)

                 {

@@ -994,12 +983,12 @@ namespace Microsoft.Boogie
                     var domainName = linearTypeChecker.FindDomainName(v);

                     if (domainName == null) continue;

                     var domain = linearTypeChecker.linearDomains[domainName];

-                    IdentifierExpr ie = new IdentifierExpr(Token.NoToken, v);

+                    IdentifierExpr ie = Expr.Ident(v);

                     domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { v.TypedIdent.Type is MapType ? ie : linearTypeChecker.Singleton(ie, domainName), domainNameToExpr[domainName] });

                 }

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

-                    lhss.Add(new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, domainNameToLocalVar[domainName])));

+                    lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(domainNameToLocalVar[domainName])));

                     rhss.Add(domainNameToExpr[domainName]);

                 }

                 foreach (Variable g in ogOldGlobalMap.Keys)

@@ -1151,7 +1140,7 @@ namespace Microsoft.Boogie
                     List<Expr> exprSeq = new List<Expr>();

                     foreach (Variable v in inputs)

                     {

-                        exprSeq.Add(new IdentifierExpr(Token.NoToken, v));

+                        exprSeq.Add(Expr.Ident(v));

                     }

                     CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());

                     callCmd.Proc = proc;

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 2e7881f6..a3e35a70 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -90,20 +90,20 @@ namespace Microsoft.Boogie
                 this.thisInParams.Add(x);

                 Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), true, x.Attributes);

                 this.thatInParams.Add(y);

-                map[x] = new IdentifierExpr(Token.NoToken, y);

+                map[x] = Expr.Ident(y);

             }

             foreach (Variable x in proc.OutParams)

             {

                 this.thisOutParams.Add(x);

                 Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false, x.Attributes);

                 this.thatOutParams.Add(y);

-                map[x] = new IdentifierExpr(Token.NoToken, y);

+                map[x] = Expr.Ident(y);

             }

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

             foreach (Variable x in thisAction.LocVars)

             {

                 Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "that_" + x.Name, x.TypedIdent.Type), false);

-                map[x] = new IdentifierExpr(Token.NoToken, y);

+                map[x] = Expr.Ident(y);

                 thatLocVars.Add(y);

             }

             Contract.Assume(proc.TypeParameters.Count == 0);