From e0de63933d24240b43f652f2f5cfaacc5922df7e Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Tue, 31 Dec 2013 21:00:35 -0800
Subject: made some fixes to type checking of atomic actions

---
 Source/Concurrency/TypeCheck.cs | 80 ++++++++++++++++++++++++-----------------
 1 file changed, 48 insertions(+), 32 deletions(-)

(limited to 'Source/Concurrency')

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index 42c06462..ed64162a 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -141,14 +141,6 @@ namespace Microsoft.Boogie
 
     public class MoverTypeChecker : StandardVisitor
     {
-        public int FindPhaseNumber(Procedure proc)
-        {
-            if (procToActionInfo.ContainsKey(proc))
-                return procToActionInfo[proc].phaseNum;
-            else
-                return int.MaxValue;
-        }
-
         CheckingContext checkingContext;
         public int errorCount;
         HashSet<Variable> qedGlobalVariables;
@@ -157,6 +149,36 @@ namespace Microsoft.Boogie
         public Program program;
         public HashSet<int> assertionPhaseNums;
         bool inAtomicSpecification;
+        CallCmd callCmd;
+
+        public MoverTypeChecker(Program program)
+        {
+            this.qedGlobalVariables = new HashSet<Variable>();
+            foreach (var g in program.GlobalVariables())
+            {
+                if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))
+                {
+                    this.qedGlobalVariables.Add(g);
+                    g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);
+                }
+            }
+            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
+            this.assertionPhaseNums = new HashSet<int>();
+            this.errorCount = 0;
+            this.checkingContext = new CheckingContext(null);
+            this.program = program;
+            this.enclosingProcPhaseNum = int.MaxValue;
+            this.inAtomicSpecification = false;
+            this.callCmd = null;
+        }
+
+        public int FindPhaseNumber(Procedure proc)
+        {
+            if (procToActionInfo.ContainsKey(proc))
+                return procToActionInfo[proc].phaseNum;
+            else
+                return int.MaxValue;
+        }
 
         public void TypeCheck()
         {
@@ -189,25 +211,6 @@ namespace Microsoft.Boogie
 #endif
         }
 
-        public MoverTypeChecker(Program program)
-        {
-            this.qedGlobalVariables = new HashSet<Variable>();
-            foreach (var g in program.GlobalVariables())
-            {
-                if (QKeyValue.FindBoolAttribute(g.Attributes, "qed"))
-                {
-                    this.qedGlobalVariables.Add(g);
-                    g.Attributes = OwickiGries.RemoveQedAttribute(g.Attributes);
-                }
-            }
-            this.procToActionInfo = new Dictionary<Procedure, ActionInfo>();
-            this.assertionPhaseNums = new HashSet<int>();
-            this.errorCount = 0;
-            this.checkingContext = new CheckingContext(null);
-            this.program = program;
-            this.enclosingProcPhaseNum = int.MaxValue;
-            this.inAtomicSpecification = false;
-        }
         public override Implementation VisitImplementation(Implementation node)
         {
             enclosingProcPhaseNum = FindPhaseNumber(node.Proc);
@@ -232,7 +235,10 @@ namespace Microsoft.Boogie
                     Error(node, "The phase of the caller procedure must be greater than the phase of the callee");
                 }
             }
-            return base.VisitCallCmd(node);
+            callCmd = node;
+            Cmd ret = base.VisitCallCmd(node);
+            callCmd = null;
+            return ret;
         }
         public override Cmd VisitParCallCmd(ParCallCmd node)
         {
@@ -242,6 +248,9 @@ namespace Microsoft.Boogie
                 int calleePhaseNum = FindPhaseNumber(iter.Proc);
                 if (calleePhaseNum > maxCalleePhaseNum)
                     maxCalleePhaseNum = calleePhaseNum;
+                callCmd = iter;
+                base.VisitCallCmd(iter);
+                callCmd = null;
             }
 
             if (enclosingProcPhaseNum > maxCalleePhaseNum)
@@ -266,13 +275,20 @@ namespace Microsoft.Boogie
         {
             if (node.Decl is GlobalVariable)
             {
-                if (inAtomicSpecification && !qedGlobalVariables.Contains(node.Decl))
+                if (callCmd != null && procToActionInfo.ContainsKey(callCmd.Proc))
                 {
-                    Error(node, "Cannot access non-qed global variable in atomic action");
+                    Error(node, "Cannot access global variable in call to atomic action");
                 }
-                else if (!inAtomicSpecification && qedGlobalVariables.Contains(node.Decl))
+                else
                 {
-                    Error(node, "Cannot access qed global variable in ordinary code");
+                    if (inAtomicSpecification && !qedGlobalVariables.Contains(node.Decl))
+                    {
+                        Error(node, "Cannot access non-qed global variable in atomic action");
+                    }
+                    else if (!inAtomicSpecification && qedGlobalVariables.Contains(node.Decl))
+                    {
+                        Error(node, "Cannot access qed global variable in ordinary code");
+                    }
                 }
             }
             return base.VisitIdentifierExpr(node);
-- 
cgit v1.2.3