fixed the linear type checking related to globals

fixed the modset analysis so that it infers the stable predicate also
added more information to type error messages

4 files changed, 86 insertions, 66 deletions

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index 11927293..900546e6 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -42,6 +42,7 @@ namespace Microsoft.Boogie {
     static Procedure enclosingProc;

     static Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>/*!*/ modSets;

     static HashSet<Procedure> yieldingProcs;

+    static HashSet<Procedure> asyncAndParallelCallTargetProcs;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullDictionaryAndValues(modSets));

@@ -69,6 +70,7 @@ namespace Microsoft.Boogie {
 

       modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

       yieldingProcs = new HashSet<Procedure>();

+      asyncAndParallelCallTargetProcs = new HashSet<Procedure>();

 

       HashSet<Procedure/*!*/> implementedProcs = new HashSet<Procedure/*!*/>();

       foreach (Declaration/*!*/ decl in program.TopLevelDeclarations) {

@@ -118,6 +120,10 @@ namespace Microsoft.Boogie {
           {

               x.AddAttribute("yields");

           }

+          if (asyncAndParallelCallTargetProcs.Contains(x) && !QKeyValue.FindBoolAttribute(x.Attributes, "stable"))

+          {

+              x.AddAttribute("stable");

+          }

       }

 

       if (false /*CommandLineOptions.Clo.Trace*/)      {

@@ -209,6 +215,7 @@ namespace Microsoft.Boogie {
           var curr = callCmd;

           while (curr != null)

           {

+              asyncAndParallelCallTargetProcs.Add(curr.Proc);

               if (!yieldingProcs.Contains(curr.Proc)) 

               {

                   yieldingProcs.Add(curr.Proc);

diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs
index ca2aaedf..3a9de5fb 100644
--- a/Source/Core/LinearSets.cs
+++ b/Source/Core/LinearSets.cs
@@ -29,9 +29,10 @@ namespace Microsoft.Boogie
         public int errorCount;

         public CheckingContext checkingContext;

         public Dictionary<string, Type> domainNameToType;

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

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

         public Dictionary<Variable, string> inoutParamToDomainName;

         public Dictionary<Variable, string> varToDomainName;

+        public Dictionary<Variable, string> globalVarToDomainName;

         public Dictionary<string, LinearDomain> linearDomains;

 

         public LinearTypechecker(Program program)

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

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

             this.parallelCallInvars = new HashSet<Variable>();

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

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

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

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

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

@@ -59,9 +60,22 @@ namespace Microsoft.Boogie
             checkingContext.Error(node, message);

             errorCount++;

         }

+        public override Program VisitProgram(Program node)

+        {

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

+            foreach (GlobalVariable g in program.GlobalVariables())

+            {

+                string domainName = FindDomainName(g);

+                if (domainName != null)

+                {

+                    globalVarToDomainName[g] = domainName;

+                }

+            }

+            return base.VisitProgram(node);

+        }

         public override Implementation VisitImplementation(Implementation node)

         {

-            HashSet<Variable> start = new HashSet<Variable>();

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

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

             {

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

@@ -87,7 +101,7 @@ namespace Microsoft.Boogie
 

             Stack<Block> dfsStack = new Stack<Block>();

             HashSet<Block> dfsStackAsSet = new HashSet<Block>();

-            availableLocalLinearVars[node.Blocks[0]] = start;

+            availableLinearVars[node.Blocks[0]] = start;

             dfsStack.Push(node.Blocks[0]);

             dfsStackAsSet.Add(node.Blocks[0]);

             while (dfsStack.Count > 0)

@@ -97,27 +111,31 @@ namespace Microsoft.Boogie
                 HashSet<Variable> end = PropagateAvailableLinearVarsAcrossBlock(b);

                 if (b.TransferCmd is ReturnCmd)

                 {

+                    foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(end))

+                    {

+                        Error(b, string.Format("Global variable {0} must be available at a return", g.Name));

+                    } 

                     foreach (Variable v in node.OutParams)

                     {

                         if (FindDomainName(v) == null || end.Contains(v)) continue;

-                        Error(b, "output variable must be available at a return");

+                        Error(b, string.Format("Output variable {0} must be available at a return", v.Name));

                     }

+                    continue;

                 }

-                if (b.TransferCmd is ReturnCmd) continue;

                 GotoCmd gotoCmd = b.TransferCmd as GotoCmd;

                 foreach (Block target in gotoCmd.labelTargets)

                 {

-                    if (!availableLocalLinearVars.ContainsKey(target))

+                    if (!availableLinearVars.ContainsKey(target))

                     {

-                        availableLocalLinearVars[target] = new HashSet<Variable>(end);

+                        availableLinearVars[target] = new HashSet<Variable>(end);

                         dfsStack.Push(target);

                         dfsStackAsSet.Add(target);

                     }

                     else

                     {

-                        var savedAvailableVars = new HashSet<Variable>(availableLocalLinearVars[target]);

-                        availableLocalLinearVars[target].IntersectWith(end);

-                        if (savedAvailableVars.IsProperSupersetOf(availableLocalLinearVars[target]) && !dfsStackAsSet.Contains(target))

+                        var savedAvailableVars = new HashSet<Variable>(availableLinearVars[target]);

+                        availableLinearVars[target].IntersectWith(end);

+                        if (savedAvailableVars.IsProperSupersetOf(availableLinearVars[target]) && !dfsStackAsSet.Contains(target))

                         {

                             dfsStack.Push(target);

                             dfsStackAsSet.Add(target);

@@ -128,7 +146,7 @@ namespace Microsoft.Boogie
             return impl;

         }

         private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b) {

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

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

             foreach (Cmd cmd in b.Cmds)

             {

                 if (cmd is AssignCmd)

@@ -155,6 +173,10 @@ namespace Microsoft.Boogie
                 }

                 else if (cmd is CallCmd)

                 {

+                    foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))

+                    {

+                        Error(b, string.Format("Global variable {0} must be available at a call", g.Name));

+                    } 

                     CallCmd callCmd = (CallCmd)cmd;

                     while (callCmd != null)

                     {

@@ -174,7 +196,7 @@ namespace Microsoft.Boogie
                         callCmd = callCmd.InParallelWith;

                     }

                     callCmd = (CallCmd)cmd;

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

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

                     while (callCmd != null)

                     {

                         foreach (IdentifierExpr ie in callCmd.Outs)

@@ -196,13 +218,19 @@ namespace Microsoft.Boogie
                 }

                 else if (cmd is YieldCmd)

                 {

-                    availableLocalLinearVars[cmd] = new HashSet<Variable>(start);

+                    foreach (GlobalVariable g in globalVarToDomainName.Keys.Except(start))

+                    {

+                        Error(b, string.Format("Global variable {0} must be available at a yield", g.Name));

+                    }

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

                 }

             }

             return start;

         }

         public string FindDomainName(Variable v)

         {

+            if (globalVarToDomainName.ContainsKey(v))

+                return globalVarToDomainName[v];

             if (inoutParamToDomainName.ContainsKey(v))

                 return inoutParamToDomainName[v];

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

@@ -233,7 +261,7 @@ namespace Microsoft.Boogie
                 }

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

                 {

-                    Error(node, "a linear domain must be consistently attached to variables of a particular type");

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

                 }

                 else

                 {

@@ -248,44 +276,35 @@ namespace Microsoft.Boogie
             for (int i = 0; i < node.Lhss.Count; i++)

             {

                 AssignLhs lhs = node.Lhss[i];

-                string domainName = FindDomainName(lhs.DeepAssignedVariable);

+                Variable lhsVar = lhs.DeepAssignedVariable;

+                string domainName = FindDomainName(lhsVar);

                 if (domainName == null) continue;

                 SimpleAssignLhs salhs = lhs as SimpleAssignLhs;

                 if (salhs == null)

                 {

-                    Error(node, "Only simple assignment allowed on linear sets");

-                    continue;

-                }

-                if (salhs.DeepAssignedVariable is GlobalVariable)

-                {

-                    Error(node, "Linear global variable cannot be written to");

+                    Error(node, string.Format("Only simple assignment allowed on linear variable {0}", lhsVar.Name));

                     continue;

                 }

                 IdentifierExpr rhs = node.Rhss[i] as IdentifierExpr;

                 if (rhs == null)

                 {

-                    Error(node, "Only variable can be assigned to a linear variable");

+                    Error(node, string.Format("Only variable can be assigned to linear variable {0}", lhsVar.Name));

                     continue; 

                 }

                 string rhsDomainName = FindDomainName(rhs.Decl);

                 if (rhsDomainName == null)

                 {

-                    Error(node, "Only linear variable can be assigned to another linear variable");

+                    Error(node, string.Format("Only linear variable can be assigned to linear variable {0}", lhsVar.Name));

                     continue;

                 }

                 if (domainName != rhsDomainName)

                 {

-                    Error(node, "Variable of one domain being assigned to a variable of another domain");

+                    Error(node, string.Format("Linear variable of domain {0} cannot be assigned to linear variable of domain {1}", rhsDomainName, domainName));

                     continue;

                 }

                 if (rhsVars.Contains(rhs.Decl))

                 {

-                    Error(node, "A linear variable can occur only once in the rhs");

-                    continue;

-                }

-                if (rhs.Decl is GlobalVariable)

-                {

-                    Error(node, "Linear global variable cannot be read from");

+                    Error(node, string.Format("Linear variable {0} can occur only once in the right-hand-side of an assignment", rhs.Decl.Name));

                     continue;

                 }

                 rhsVars.Add(rhs.Decl);

@@ -304,13 +323,13 @@ namespace Microsoft.Boogie
                 IdentifierExpr actual = node.Ins[i] as IdentifierExpr;

                 if (actual == null)

                 {

-                    Error(node, "Only variable can be assigned to a linear variable");

+                    Error(node, string.Format("Only variable can be passed to linear parameter {0}", formal.Name));

                     continue;

                 }

                 string actualDomainName = FindDomainName(actual.Decl);

                 if (actualDomainName == null)

                 {

-                    Error(node, "Only a linear argument can be passed to a linear parameter");

+                    Error(node, string.Format("Only a linear argument can be passed to linear parameter {0}", formal.Name));

                     continue;

                 }

                 if (domainName != actualDomainName)

@@ -320,7 +339,7 @@ namespace Microsoft.Boogie
                 }

                 if (parallelCallInvars.Contains(actual.Decl))

                 {

-                    Error(node, "A linear set can occur only once as an in parameter");

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

                     continue;

                 }

                 if (actual.Decl is GlobalVariable)

@@ -373,13 +392,7 @@ namespace Microsoft.Boogie
                 domainNameToScope[domainName] = new HashSet<Variable>();

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

             }

-            foreach (Variable v in program.GlobalVariables())

-            {

-                var domainName = FindDomainName(v);

-                if (domainName == null) continue;

-                domainNameToScope[domainName].Add(v);

-            }

-            foreach (Variable v in availableLocalLinearVars[absy])

+            foreach (Variable v in availableLinearVars[absy])

             {

                 var domainName = FindDomainName(v);

                 domainNameToScope[domainName].Add(v);

@@ -453,7 +466,7 @@ namespace Microsoft.Boogie
                                 {

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

                                 }

-                                foreach (Variable v in availableLocalLinearVars[callCmd])

+                                foreach (Variable v in availableLinearVars[callCmd])

                                 {

                                     var domainName = FindDomainName(v);

                                     var domain = linearDomains[domainName];

@@ -510,10 +523,9 @@ namespace Microsoft.Boogie
                     domainNameToOutputScope[domainName] = new HashSet<Variable>();

                     

                 }

-                foreach (Variable v in program.GlobalVariables())

+                foreach (Variable v in globalVarToDomainName.Keys)

                 {

-                    var domainName = FindDomainName(v);

-                    if (domainName == null) continue;

+                    var domainName = globalVarToDomainName[v];

                     domainNameToInputScope[domainName].Add(v);

                     domainNameToOutputScope[domainName].Add(v);

                 }

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 56b327cd..dd6276c2 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -67,7 +67,7 @@ namespace Microsoft.Boogie
             newCmds.Add(yieldCallCmd);

         }

 

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

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

         {

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

             foreach (var domainName in linearTypechecker.linearDomains.Keys)

@@ -77,7 +77,7 @@ namespace Microsoft.Boogie
                 expr.Typecheck(new TypecheckingContext(null));

                 domainNameToExpr[domainName] = expr;

             }

-            foreach (Variable v in availableLocalLinearVars)

+            foreach (Variable v in availableLinearVars)

             {

                 var domainName = linearTypechecker.FindDomainName(v);

                 var domain = linearTypechecker.linearDomains[domainName];

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

                 newCmds.Add(new HavocCmd(Token.NoToken, globalMods));

             }

-            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[yieldCmd], domainNameToInputVar);

+            Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[yieldCmd], domainNameToInputVar);

             AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

 

             for (int j = 0; j < cmds.Count; j++)

@@ -440,13 +440,13 @@ namespace Microsoft.Boogie
                         if (callCmd.InParallelWith != null || callCmd.IsAsync ||

                             QKeyValue.FindBoolAttribute(callCmd.Proc.Attributes, "yields"))

                         {

-                            HashSet<Variable> availableLocalLinearVars = new HashSet<Variable>(linearTypechecker.availableLocalLinearVars[callCmd]);

+                            HashSet<Variable> availableLinearVars = new HashSet<Variable>(linearTypechecker.availableLinearVars[callCmd]);

                             foreach (IdentifierExpr ie in callCmd.Outs)

                             {

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

-                                availableLocalLinearVars.Add(ie.Decl);

+                                availableLinearVars.Add(ie.Decl);

                             }

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

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

                             AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);

                         }

                     }

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

             foreach (Block header in yieldingHeaders)

             {

-                Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[header], domainNameToInputVar);

+                Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLinearVars[header], domainNameToInputVar);

                 foreach (Block pred in header.Predecessors)

                 {

                     AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);

diff --git a/Test/linear/Answer b/Test/linear/Answer
index e6df2e87..9ba244e5 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -1,22 +1,23 @@
 

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

-typecheck.bpl(6,22): Error: a linear domain must be consistently attached to variables of a particular type

+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 sets

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

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

-typecheck.bpl(39,6): Error: Variable of one domain being assigned to a variable of another domain

-typecheck.bpl(45,9): Error: A linear variable can occur only once in the rhs

-typecheck.bpl(49,4): Error: A linear set can occur only once as an in parameter

-typecheck.bpl(51,4): Error: Only variable can be assigned to a linear variable

+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

+typecheck.bpl(39,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D

+typecheck.bpl(45,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment

+typecheck.bpl(49,4): Error: Linear variable a can occur only once as an input parameter

+typecheck.bpl(51,4): Error: Only variable can be passed to linear parameter b

 typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same

 typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same

-typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter

-typecheck.bpl(61,4): Error: A linear set can occur only once as an in parameter

-typecheck.bpl(66,6): Error: output variable must be available at a return

-typecheck.bpl(75,4): Error: Linear global variable cannot be read from

-typecheck.bpl(81,4): Error: Linear global variable cannot be written to

-16 type checking errors detected in typecheck.bpl

+typecheck.bpl(57,4): Error: Only a linear argument can be passed to linear parameter a

+typecheck.bpl(61,4): Error: Linear variable a can occur only once as an input parameter

+typecheck.bpl(66,6): Error: Output variable d must be available at a return

+typecheck.bpl(75,4): Error: Global variable g must be available at a return

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

+typecheck.bpl(81,4): Error: Output variable r must be available at a return

+17 type checking errors detected in typecheck.bpl

 

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