added {:aux} attribute to local variables

2 files changed, 52 insertions, 31 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 8241d42b..ec00a6e4 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -209,10 +209,12 @@ namespace Microsoft.Boogie
         Implementation enclosingImpl;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

-        bool inSpecification;

+        bool canAccessSharedVars;

+        bool canAccessAuxVars;

         int minPhaseNum;

         int maxPhaseNum;

         public Dictionary<Absy, HashSet<int>> absyToPhaseNums;

+        HashSet<Variable> auxVars;

 

         private static List<int> FindIntAttributes(QKeyValue kv, string name)

         {

@@ -321,6 +323,7 @@ namespace Microsoft.Boogie
 

         public MoverTypeChecker(Program program)

         {

+            this.auxVars = new HashSet<Variable>();

             this.absyToPhaseNums = new Dictionary<Absy, HashSet<int>>();

             this.introducePhaseNums = new Dictionary<Variable, int>();

             this.hidePhaseNums = new Dictionary<Variable, int>();

@@ -330,7 +333,8 @@ namespace Microsoft.Boogie
             this.program = program;

             this.enclosingProc = null;

             this.enclosingImpl = null;

-            this.inSpecification = false;

+            this.canAccessSharedVars = false;

+            this.canAccessAuxVars = false;

             this.minPhaseNum = int.MaxValue;

             this.maxPhaseNum = -1;

             foreach (var g in program.GlobalVariables())

@@ -365,6 +369,14 @@ namespace Microsoft.Boogie
                 return node;

             }

             this.enclosingImpl = node;

+            auxVars = new HashSet<Variable>();

+            foreach (Variable v in node.LocVars)

+            {

+                if (QKeyValue.FindBoolAttribute(v.Attributes, "aux"))

+                {

+                    auxVars.Add(v);

+                }

+            }

             return base.VisitImplementation(node);

         }

         

@@ -448,14 +460,35 @@ namespace Microsoft.Boogie
             }

             return base.VisitParCallCmd(node);

         }

-        

+

+        public override Cmd VisitAssignCmd(AssignCmd node)

+        {

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

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

+            {

+                bool savedCanAccessSharedVars = canAccessSharedVars;

+                bool savedCanAccessAuxVars = canAccessAuxVars;

+                Variable v = node.Lhss[i].DeepAssignedVariable;

+                if (v is LocalVariable && auxVars.Contains(v))

+                {

+                    canAccessSharedVars = true;

+                    canAccessAuxVars = true;

+                }

+                this.Visit(node.Lhss[i]);

+                this.Visit(node.Rhss[i]);

+                canAccessSharedVars = savedCanAccessSharedVars;

+                canAccessAuxVars = savedCanAccessAuxVars;

+            }

+            return node;

+        }

+

         public override Expr VisitIdentifierExpr(IdentifierExpr node)

         {

             if (node.Decl is GlobalVariable)

             {

-                if (!inSpecification)

+                if (!canAccessSharedVars)

                 {

-                    Error(node, "Global variable can be accessed only in atomic actions or specifications");

+                    Error(node, "Shared variable can be accessed only in atomic actions or specifications");

                 }

                 else

                 {

@@ -469,6 +502,11 @@ namespace Microsoft.Boogie
                     }

                 }

             }

+            else if (node.Decl is LocalVariable && auxVars.Contains(node.Decl) && !canAccessAuxVars)

+            {

+                Error(node, "Auxiliary variable can be accessed only in assertions");

+            }

+

             return base.VisitIdentifierExpr(node);

         }

         

@@ -476,9 +514,9 @@ namespace Microsoft.Boogie
         {

             minPhaseNum = int.MaxValue;

             maxPhaseNum = -1;

-            inSpecification = true;

+            canAccessSharedVars = true;

             Ensures ret = base.VisitEnsures(ensures);

-            inSpecification = false;

+            canAccessSharedVars = false;

             ActionInfo actionInfo = procToActionInfo[enclosingProc];

             AtomicActionInfo atomicActionInfo = actionInfo as AtomicActionInfo;

             if (atomicActionInfo != null && atomicActionInfo.ensures == ensures)

@@ -503,20 +541,22 @@ namespace Microsoft.Boogie
         {

             minPhaseNum = int.MaxValue;

             maxPhaseNum = -1;

-            inSpecification = true;

+            canAccessSharedVars = true;

             Requires ret = base.VisitRequires(requires);

-            inSpecification = false;

+            canAccessSharedVars = false;

             CheckAndAddPhases(requires, requires.Attributes, procToActionInfo[enclosingProc].phaseNum);

             return ret;

         }

-        

+

         public override Cmd VisitAssertCmd(AssertCmd node)

         {

             minPhaseNum = int.MaxValue;

             maxPhaseNum = -1;

-            inSpecification = true;

+            canAccessSharedVars = true;

+            canAccessAuxVars = true;

             Cmd ret = base.VisitAssertCmd(node);

-            inSpecification = false;

+            canAccessAuxVars = false;

+            canAccessSharedVars = false;

             CheckAndAddPhases(node, node.Attributes, procToActionInfo[enclosingImpl.Proc].phaseNum);

             return ret;

         }

diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs
index 6f356626..92ec7e1c 100644
--- a/Source/Concurrency/YieldTypeChecker.cs
+++ b/Source/Concurrency/YieldTypeChecker.cs
@@ -371,18 +371,6 @@ namespace Microsoft.Boogie
                     {

                         edgeLabels[edge] = 'Y';

                     }

-                    else if (cmd is AssumeCmd || cmd is AssignCmd || cmd is HavocCmd)

-                    {

-                        if (AccessesGlobals(cmd))

-                        {

-                            finalStates.Add(curr);

-                            initialStates.Add(next);

-                        }

-                        else

-                        {

-                            edgeLabels[edge] = 'P';

-                        }

-                    }

                     else

                     {

                         edgeLabels[edge] = 'P';

@@ -391,13 +379,6 @@ namespace Microsoft.Boogie
             }

         }

 

-        private static bool AccessesGlobals(Cmd cmd)

-        {

-            VariableCollector collector = new VariableCollector();

-            collector.Visit(cmd);

-            return collector.usedVars.Any(x => x is GlobalVariable);

-        }

-        

         private static string PrintGraph(Implementation yTypeChecked, Graph<int> graph, Dictionary<Tuple<int, int>, string> edgeLabels)

         {

             var s = new StringBuilder();