new design for linear types + VCgen

ported all the examples
added the QED examples to runtest.bat

21 files changed, 273 insertions, 77 deletions

diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index f7b14836..c8cb1844 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -36,7 +36,7 @@ namespace Microsoft.Boogie
         public Program program;

         public int errorCount;

         public CheckingContext checkingContext;

-        public Dictionary<string, Type> domainNameToType;

+        public Dictionary<string, Dictionary<Type, Function>> domainNameToCollectors;

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

         public Dictionary<Variable, LinearQualifier> inParamToLinearQualifier;

         public Dictionary<Variable, string> outParamToDomainName;

@@ -49,20 +49,59 @@ namespace Microsoft.Boogie
             this.program = program;

             this.errorCount = 0;

             this.checkingContext = new CheckingContext(null);

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

+            this.domainNameToCollectors = new Dictionary<string, Dictionary<Type, Function>>();

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

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

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

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

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

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

         }

         public void TypeCheck()

         {

             this.VisitProgram(program);

-            foreach (string domainName in domainNameToType.Keys)

+            foreach (string domainName in domainNameToCollectors.Keys)

             {

-                this.linearDomains[domainName] = new LinearDomain(program, domainName, domainNameToType[domainName]);

+                var collectors = domainNameToCollectors[domainName];

+                if (collectors.Count == 0) continue;

+                this.linearDomains[domainName] = new LinearDomain(program, domainName, collectors);

             }

+            Dictionary<Absy, HashSet<Variable>> newAvailableLinearVars = new Dictionary<Absy, HashSet<Variable>>();

+            foreach (Absy absy in this.availableLinearVars.Keys)

+            {

+                HashSet<Variable> vars = new HashSet<Variable>();

+                foreach (Variable var in this.availableLinearVars[absy])

+                {

+                    string domainName = FindDomainName(var);

+                    if (this.linearDomains.ContainsKey(domainName))

+                    {

+                        vars.Add(var);

+                    }

+                }

+                newAvailableLinearVars[absy] = vars;

+            }

+            this.availableLinearVars = newAvailableLinearVars;

+            var temp = new Dictionary<Variable, string>();

+            foreach (Variable v in outParamToDomainName.Keys)

+            {

+                if (linearDomains.ContainsKey(outParamToDomainName[v]))

+                    temp[v] = outParamToDomainName[v];

+            }

+            this.outParamToDomainName = temp;

+            temp = new Dictionary<Variable, string>();

+            foreach (Variable v in varToDomainName.Keys)

+            {

+                if (linearDomains.ContainsKey(varToDomainName[v]))

+                    temp[v] = varToDomainName[v];

+            }

+            this.varToDomainName = temp;

+            temp = new Dictionary<Variable, string>();

+            foreach (Variable v in globalVarToDomainName.Keys)

+            {

+                if (linearDomains.ContainsKey(globalVarToDomainName[v]))

+                    temp[v] = globalVarToDomainName[v];

+            }

+            this.globalVarToDomainName = temp;

         }

         private void Error(Absy node, string message)

         {

@@ -71,7 +110,6 @@ namespace Microsoft.Boogie
         }

         public override Program VisitProgram(Program node)

         {

-            globalVarToDomainName = new Dictionary<Variable, string>();

             foreach (GlobalVariable g in program.GlobalVariables())

             {

                 string domainName = FindDomainName(g);

@@ -82,6 +120,39 @@ namespace Microsoft.Boogie
             }

             return base.VisitProgram(node);

         }

+        public override Function VisitFunction(Function node)

+        {

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

+            if (domainName != null)

+            {

+                if (!domainNameToCollectors.ContainsKey(domainName)) 

+                {

+                    domainNameToCollectors[domainName] = new Dictionary<Type, Function>();

+                }

+                if (node.InParams.Count == 1 && node.OutParams.Count == 1)

+                {

+                    Type inType = node.InParams[0].TypedIdent.Type;

+                    MapType outType = node.OutParams[0].TypedIdent.Type as MapType;

+                    if (domainNameToCollectors[domainName].ContainsKey(inType))

+                    {

+                        Error(node, string.Format("A collector for domain for input type has already been defined"));

+                    }

+                    else if (outType == null || outType.Arguments.Count != 1 || !outType.Result.Equals(Type.Bool))

+                    {

+                        Error(node, "Output of a linear domain collector should be of set type");

+                    }

+                    else 

+                    {

+                        domainNameToCollectors[domainName][inType] = node;

+                    }

+                }

+                else

+                {

+                    Error(node, "Linear domain collector should have one input and one output parameter");

+                }

+            }

+            return base.VisitFunction(node);

+        }

         public override Implementation VisitImplementation(Implementation node)

         {

             HashSet<Variable> start = new HashSet<Variable>(globalVarToDomainName.Keys);

@@ -318,32 +389,9 @@ namespace Microsoft.Boogie
             string domainName = FindDomainName(node);

             if (domainName != null)

             {

-                Type type = node.TypedIdent.Type;

-                MapType mapType = type as MapType;

-                if (mapType != null)

-                {

-                    if (mapType.Arguments.Count == 1 && mapType.Result.Equals(Type.Bool))

-                    {

-                        type = mapType.Arguments[0];

-                        if (type is MapType)

-                        {

-                            Error(node, "the domain of a linear set must be a scalar type");

-                            return base.VisitVariable(node);

-                        }

-                    }

-                    else

-                    {

-                        Error(node, "a linear domain can be attached to either a set or a scalar type");

-                        return base.VisitVariable(node);

-                    }

-                }

-                if (domainNameToType.ContainsKey(domainName) && !domainNameToType[domainName].Equals(type))

-                {

-                    Error(node, string.Format("Linear domain {0} must be consistently attached to variables of one type", domainName));

-                }

-                else

+                if (!domainNameToCollectors.ContainsKey(domainName))

                 {

-                    domainNameToType[domainName] = type;

+                    domainNameToCollectors[domainName] = new Dictionary<Type,Function>();

                 }

             }

             return base.VisitVariable(node);

@@ -483,9 +531,13 @@ namespace Microsoft.Boogie
         public IEnumerable<Variable> AvailableLinearVars(Absy absy)

         {

             if (availableLinearVars.ContainsKey(absy))

+            {

                 return availableLinearVars[absy];

+            }

             else

+            {

                 return new HashSet<Variable>();

+            }

         }

 

         private void AddDisjointnessExpr(List<Cmd> newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)

@@ -494,7 +546,6 @@ namespace Microsoft.Boogie
             foreach (var domainName in linearDomains.Keys)

             {

                 domainNameToScope[domainName] = new HashSet<Variable>();

-                domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);

             }

             foreach (Variable v in AvailableLinearVars(absy))

             {

@@ -503,7 +554,7 @@ namespace Microsoft.Boogie
             }

             foreach (string domainName in linearDomains.Keys)

             {

-                newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToScope[domainName])));

+                newCmds.Add(new AssumeCmd(Token.NoToken, DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));

             }

         }

 

@@ -559,9 +610,9 @@ namespace Microsoft.Boogie
                                 {

                                     var domainName = FindDomainName(v);

                                     var domain = linearDomains[domainName];

-                                    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] });

+                                    if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

+                                    Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

+                                    var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });

                                     expr.Resolve(new ResolutionContext(null));

                                     expr.Typecheck(new TypecheckingContext(null));

                                     domainNameToExpr[domainName] = expr;

@@ -637,12 +688,14 @@ namespace Microsoft.Boogie
                 {

                     var domainName = FindDomainName(v);

                     if (domainName == null) continue;

+                    if (!this.linearDomains.ContainsKey(domainName)) continue;

                     domainNameToInputScope[domainName].Add(v);

                 }

                 foreach (Variable v in proc.OutParams)

                 {

                     var domainName = FindDomainName(v);

                     if (domainName == null) continue;

+                    if (!this.linearDomains.ContainsKey(domainName)) continue;

                     domainNameToOutputScope[domainName].Add(v);

                 }

                 foreach (var domainName in linearDomains.Keys)

@@ -651,8 +704,7 @@ namespace Microsoft.Boogie
                     var domain = linearDomains[domainName];

                     Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "linear_" + domainName + "_in", new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Type.Bool)), true);

                     proc.InParams.Add(f);

-                    domainNameToOutputScope[domainName].Add(f);

-                    proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, domainNameToOutputScope[domainName])));

+                    proc.Ensures.Add(new Ensures(true, DisjointnessExpr(domainName, f, domainNameToOutputScope[domainName])));

                 }

             }

             

@@ -675,37 +727,43 @@ namespace Microsoft.Boogie
             //CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

         }

 

-        public Expr Singleton(Expr e, string domainName)

-        {

-            var domain = linearDomains[domainName];

-            return Expr.Store(new NAryExpr(Token.NoToken, new FunctionCall(domain.mapConstBool), new List<Expr> { Expr.False }), e, Expr.True);

-        }

-

-        List<Expr> MkExprs(params Expr[] args)

+        private Expr SubsetExpr(LinearDomain domain, Expr ie, Variable partition, int partitionCount)

         {

-            return new List<Expr>(args);

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

+            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> { ie, e });

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

+            return e;

         }

 

-        public Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)

+        private Expr SubsetExprs(LinearDomain domain, HashSet<Variable> scope, Variable partition, int count, Expr expr)

         {

-            LinearDomain domain = linearDomains[domainName];

-            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));

-            Expr disjointExpr = Expr.True;

-            int count = 0;

             foreach (Variable v in scope)

             {

-                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> { 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);

+                if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

+                Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

+                expr = Expr.Binary(BinaryOperator.Opcode.And, SubsetExpr(domain, ie, partition, count), expr);

+                count++;

             }

-            var expr = new ExistsExpr(Token.NoToken, new List<Variable> { partition }, disjointExpr);

+            expr = new ExistsExpr(Token.NoToken, new List<Variable> { partition }, expr);

             expr.Resolve(new ResolutionContext(null));

             expr.Typecheck(new TypecheckingContext(null));

             return expr;

         }

+

+        public Expr DisjointnessExpr(string domainName, Variable inputVar, HashSet<Variable> scope)

+        {

+            LinearDomain domain = linearDomains[domainName];

+            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));

+            return SubsetExprs(domain, scope, partition, 1, SubsetExpr(domain, Expr.Ident(inputVar), partition, 0));

+        }

+

+        public Expr DisjointnessExpr(string domainName, HashSet<Variable> scope)

+        {

+            LinearDomain domain = linearDomains[domainName];

+            BoundVariable partition = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("partition_{0}", domainName), new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { domain.elementType }, Microsoft.Boogie.Type.Int)));

+            return SubsetExprs(domain, scope, partition, 0, Expr.True);

+        }

     }

 

     public class LinearQualifier

@@ -721,19 +779,21 @@ namespace Microsoft.Boogie
 

     public class LinearDomain

     {

-        public Microsoft.Boogie.Type elementType;

         public Function mapEqInt;

         public Function mapConstInt;

         public Function mapOrBool;

         public Function mapImpBool;

         public Function mapConstBool;

         public List<Axiom> axioms;

+        public Type elementType;

+        public Dictionary<Type, Function> collectors;

 

-        public LinearDomain(Program program, string domainName, Type elementType)

+        public LinearDomain(Program program, string domainName, Dictionary<Type, Function> collectors)

         {

-            this.elementType = elementType;

             this.axioms = new List<Axiom>();

-

+            this.collectors = collectors;

+            MapType setType = (MapType)collectors.First().Value.OutParams[0].TypedIdent.Type;

+            this.elementType = setType.Arguments[0];

             MapType mapTypeBool = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Bool);

             MapType mapTypeInt = new MapType(Token.NoToken, new List<TypeVariable>(), new List<Type> { this.elementType }, Type.Int);

             this.mapOrBool = new Function(Token.NoToken, "linear_" + domainName + "_MapOr",

diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index 10becb3b..f30213a0 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -443,18 +443,21 @@ namespace Microsoft.Boogie
             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

             foreach (Variable v in first.thatInParams)

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

             foreach (Variable v in second.thisInParams)

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

                 if (domainName == null) continue;

+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 domainNameToScope[domainName].Add(v);

             }

             foreach (string domainName in domainNameToScope.Keys)

diff --git a/Source/Concurrency/OwickiGries.cs b/Source/Concurrency/OwickiGries.cs
index d9f23cb3..d4ecab2e 100644
--- a/Source/Concurrency/OwickiGries.cs
+++ b/Source/Concurrency/OwickiGries.cs
@@ -341,9 +341,11 @@ namespace Microsoft.Boogie
             foreach (Variable v in availableLinearVars)

             {

                 var domainName = linearTypeChecker.FindDomainName(v);

+                if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                 var domain = linearTypeChecker.linearDomains[domainName];

-                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] });

+                if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

+                Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

+                var expr = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });

                 expr.Resolve(new ResolutionContext(null));

                 expr.Typecheck(new TypecheckingContext(null));

                 domainNameToExpr[domainName] = expr;

@@ -982,9 +984,11 @@ namespace Microsoft.Boogie
                     Variable v = impl.InParams[i];

                     var domainName = linearTypeChecker.FindDomainName(v);

                     if (domainName == null) continue;

+                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                     var domain = linearTypeChecker.linearDomains[domainName];

-                    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] });

+                    if (!domain.collectors.ContainsKey(v.TypedIdent.Type)) continue;

+                    Expr ie = new NAryExpr(Token.NoToken, new FunctionCall(domain.collectors[v.TypedIdent.Type]), new List<Expr> { Expr.Ident(v) });

+                    domainNameToExpr[domainName] = new NAryExpr(Token.NoToken, new FunctionCall(domain.mapOrBool), new List<Expr> { ie, domainNameToExpr[domainName] });

                 }

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

@@ -1031,12 +1035,12 @@ namespace Microsoft.Boogie
                 foreach (var domainName in linearTypeChecker.linearDomains.Keys)

                 {

                     domainNameToScope[domainName] = new HashSet<Variable>();

-                    domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);

                 }

                 foreach (Variable v in program.GlobalVariables())

                 {

                     var domainName = linearTypeChecker.FindDomainName(v);

                     if (domainName == null) continue;

+                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                     domainNameToScope[domainName].Add(v);

                 }

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

@@ -1044,11 +1048,12 @@ namespace Microsoft.Boogie
                     Variable v = proc.InParams[i];

                     var domainName = linearTypeChecker.FindDomainName(v);

                     if (domainName == null) continue;

+                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                     domainNameToScope[domainName].Add(v);

                 }

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

-                    cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));

+                    cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));

                 }

                 foreach (Requires r in proc.Requires)

                 {

@@ -1072,12 +1077,12 @@ namespace Microsoft.Boogie
                 foreach (var domainName in linearTypeChecker.linearDomains.Keys)

                 {

                     domainNameToScope[domainName] = new HashSet<Variable>();

-                    domainNameToScope[domainName].Add(domainNameToInputVar[domainName]);

                 }

                 foreach (Variable v in program.GlobalVariables())

                 {

                     var domainName = linearTypeChecker.FindDomainName(v);

                     if (domainName == null) continue;

+                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                     domainNameToScope[domainName].Add(v);

                 }

                 for (int i = 0; i < proc.OutParams.Count; i++)

@@ -1085,11 +1090,12 @@ namespace Microsoft.Boogie
                     Variable v = proc.OutParams[i];

                     var domainName = linearTypeChecker.FindDomainName(v);

                     if (domainName == null) continue;

+                    if (!linearTypeChecker.linearDomains.ContainsKey(domainName)) continue;

                     domainNameToScope[domainName].Add(v);

                 }

                 foreach (string domainName in linearTypeChecker.linearDomains.Keys)

                 {

-                    cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToScope[domainName])));

+                    cmds.Add(new AssumeCmd(Token.NoToken, linearTypeChecker.DisjointnessExpr(domainName, domainNameToInputVar[domainName], domainNameToScope[domainName])));

                 }

                 foreach (Ensures e in proc.Ensures)

                 {

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 2934d690..9219497b 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -1,7 +1,5 @@
 

 -------------------- typecheck.bpl --------------------

-typecheck.bpl(6,22): Error: Linear domain A must be consistently attached to variables of one type

-typecheck.bpl(18,22): Error: a linear domain can be attached to either a set or a scalar type

 typecheck.bpl(31,9): Error: Only simple assignment allowed on linear variable b

 typecheck.bpl(33,6): Error: Only variable can be assigned to linear variable a

 typecheck.bpl(35,6): Error: Only linear variable can be assigned to linear variable a

@@ -17,7 +15,7 @@ typecheck.bpl(67,0): Error: Output variable d must be available at a return
 typecheck.bpl(76,0): Error: Global variable g must be available at a return

 typecheck.bpl(81,7): Error: unavailable source for a linear read

 typecheck.bpl(82,0): Error: Output variable r must be available at a return

-17 type checking errors detected in typecheck.bpl

+15 type checking errors detected in typecheck.bpl

 

 -------------------- list.bpl --------------------

 

diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index f4badca9..b0caa9e1 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -2,6 +2,11 @@ type X;
 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

 

+function {:inline} {:linear "Mem"} MemCollector(xs: [X]bool) : [X]bool

+{

+  xs

+}

+

 var head: X;

 var tail: X;

 var {:linear "Mem"} D: [X]bool;

diff --git a/Test/og/Answer b/Test/og/Answer
index 067a6534..c9e349e1 100644
--- a/Test/og/Answer
+++ b/Test/og/Answer
@@ -56,10 +56,10 @@ Boogie program verifier finished with 5 verified, 0 errors
 Boogie program verifier finished with 4 verified, 0 errors

 

 -------------------- parallel4.bpl --------------------

-parallel4.bpl(18,3): Error BP5001: This assertion might not hold.

+parallel4.bpl(24,3): Error BP5001: This assertion might not hold.

 Execution trace:

     (0,0): og_init

-    parallel4.bpl(16,5): anon0$1

+    parallel4.bpl(22,5): anon0$1

 

 Boogie program verifier finished with 2 verified, 1 error

 

@@ -72,7 +72,7 @@ Boogie program verifier finished with 4 verified, 0 errors
 Boogie program verifier finished with 3 verified, 0 errors

 

 -------------------- t1.bpl --------------------

-t1.bpl(35,5): Error: Non-interference check failed

+t1.bpl(51,5): Error: Non-interference check failed

 Execution trace:

     (0,0): og_init

     (0,0): inline$Impl_YieldChecker_A_2147483647$0$L1

@@ -95,3 +95,19 @@ Execution trace:
     (0,0): inline$Proc_YieldChecker_P_2147483647$1$L0

 

 Boogie program verifier finished with 1 verified, 1 error

+

+-------------------- DeviceCache.bpl --------------------

+

+Boogie program verifier finished with 50 verified, 0 errors

+

+-------------------- ticket.bpl --------------------

+

+Boogie program verifier finished with 28 verified, 0 errors

+

+-------------------- lock.bpl --------------------

+

+Boogie program verifier finished with 6 verified, 0 errors

+

+-------------------- multiset.bpl --------------------

+

+Boogie program verifier finished with 102 verified, 0 errors

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index 730b1ce1..ec61e188 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -6,6 +6,16 @@ var {:qed} lock: X;
 var {:qed} currsize: int;

 var {:qed} newsize: int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool

+{

+  x

+}

+

 function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

 {

     0 <= currsize && currsize <= newsize && 

diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl
index 32fb25b7..28e8b662 100644
--- a/Test/og/DeviceCacheSimplified.bpl
+++ b/Test/og/DeviceCacheSimplified.bpl
@@ -1,5 +1,11 @@
 type X;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)

 {

     currsize <= newsize && (ghostLock == nil <==> currsize == newsize)

diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 5985b6d6..a263467c 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -1,9 +1,14 @@
 type X;

-

 const nil: X;

 var l: X;

 var x: int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: X);

 ensures xls != nil;

 

diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index eaa820b9..d31c20ee 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -1,5 +1,21 @@
 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

+function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool

+{

+  x

+}

+

+function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool

+{

+  x

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: int);

 ensures xls != 0;

 

diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 96aca741..ff3f5b1e 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -13,6 +13,11 @@ function {:inline} All() : [X]bool
     MapConstBool(true)

 }

 

+function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool

+{

+  xs

+}

+

 var x: int;

 var l: [X]bool;

 

diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 565cc82b..04406609 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -13,6 +13,11 @@ function {:inline} All() : [X]bool
     MapConstBool(true)

 }

 

+function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool

+{

+  xs

+}

+

 var x: int;

 var l: X;

 const nil: X;

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 047d25a6..161171bf 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -10,6 +10,12 @@ var {:qed} lock : [int]X;
 var {:qed} owner : [int]X;

 const max : int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 axiom (max > 0);

 

 procedure {:yields} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);

diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 6ebb9cf1..64144ae9 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -2,6 +2,12 @@ function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
 

 var g:int;

 

+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

+{

+  x

+}

+

+

 var {:linear "Perm"} Permissions: [int]bool;

 

 procedure Allocate_Perm() returns ({:linear "Perm"} xls: [int]bool);

diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 6cc85131..07864511 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,5 +1,11 @@
 var a:[int]int;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

 procedure {:entrypoint} {:yields} main() 

diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 22e7173f..1069399f 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -2,6 +2,12 @@ var a:int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure {:entrypoint} {:yields} main() 

 {

   var {:linear "tid"} i: int;

diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 34bb82a9..01bbe74d 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -2,6 +2,12 @@ var a:[int]int;
 

 procedure Allocate() returns ({:linear "tid"} xls: int);

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

 procedure {:entrypoint} {:yields} main() 

 {

     var {:linear "tid"} i: int;

diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index ad4123f9..8b77ce1b 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -3,6 +3,11 @@ function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
 

 function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;

 

+function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool

+{

+  x

+}

+

 procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);

   ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);

 

diff --git a/Test/og/runtest.bat b/Test/og/runtest.bat
index 068f361f..30bd66cc 100644
--- a/Test/og/runtest.bat
+++ b/Test/og/runtest.bat
@@ -9,7 +9,7 @@ for %%f in (foo.bpl bar.bpl one.bpl parallel1.bpl) do (
   %BGEXE% %* /nologo /noinfer %%f

 )

 

-for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl) do (

+for %%f in (linear-set.bpl linear-set2.bpl FlanaganQadeer.bpl DeviceCacheSimplified.bpl parallel2.bpl parallel4.bpl parallel5.bpl akash.bpl t1.bpl new1.bpl perm.bpl async.bpl DeviceCache.bpl ticket.bpl lock.bpl multiset.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f

diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 84ed3a35..43758a91 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -1,5 +1,21 @@
 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

+function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool

+{

+  MapConstBool(false)[x := true]

+}

+

+function {:inline} {:linear "1"} SetCollector1(x: [int]bool) : [int]bool

+{

+  x

+}

+

+function {:inline} {:linear "2"} SetCollector2(x: [int]bool) : [int]bool

+{

+  x

+}

+

 procedure Allocate() returns ({:linear "tid"} xls: int);

 ensures xls != 0;

 

diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index fe56fb27..3404f8e0 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -11,6 +11,16 @@ var {:qed} s: int;
 var {:qed} cs: X;

 var {:qed} T: [int]bool;

 

+function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

+function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool

+{

+  MapConstBool(false)[x := true]

+}

+function {:inline} {:linear "tid"} TidSetCollector(x: [X]bool) : [X]bool

+{

+  x

+}

+

 function {:inline} Inv1(tickets: [int]bool, ticket: int): (bool)

 {

     tickets == RightOpen(ticket)