added syntax for par call and ParCallCmd

1 files changed, 55 insertions, 11 deletions

diff --git a/Source/Concurrency/TypeCheck.cs b/Source/Concurrency/TypeCheck.cs
index d4df34b8..41fb9480 100644
--- a/Source/Concurrency/TypeCheck.cs
+++ b/Source/Concurrency/TypeCheck.cs
@@ -21,7 +21,7 @@ namespace Microsoft.Boogie
         HashSet<Variable> globalVariables;

         bool globalVarAccessAllowed;

         bool visitingAssertion;

-        int phaseNumEnclosingProc;

+        int enclosingProcPhaseNum;

         public Dictionary<Procedure, ActionInfo> procToActionInfo;

         public Program program;

 

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

             this.program = program;

             this.visitingAssertion = false;

-            this.phaseNumEnclosingProc = int.MaxValue;

+            this.enclosingProcPhaseNum = int.MaxValue;

         }

         public override Block VisitBlock(Block node)

         {

@@ -83,27 +83,71 @@ namespace Microsoft.Boogie
         }

         public override Implementation VisitImplementation(Implementation node)

         {

-            phaseNumEnclosingProc = FindPhaseNumber(node.Proc);

+            enclosingProcPhaseNum = FindPhaseNumber(node.Proc);

             return base.VisitImplementation(node);

         }

         public override Procedure VisitProcedure(Procedure node)

         {

-            phaseNumEnclosingProc = FindPhaseNumber(node);

+            enclosingProcPhaseNum = FindPhaseNumber(node);

             return base.VisitProcedure(node);

         } 

         public override Cmd VisitCallCmd(CallCmd node)

         {

             globalVarAccessAllowed = false;

-            if (!node.IsAsync && node.InParallelWith == null) {

+            if (enclosingProcPhaseNum == int.MaxValue)

+                return base.VisitCallCmd(node);

 

+            if (!node.IsAsync)

+            {

                 int calleePhaseNum = FindPhaseNumber(node.Proc);

-                if (!(calleePhaseNum == int.MaxValue || phaseNumEnclosingProc > calleePhaseNum))

+                if (enclosingProcPhaseNum > calleePhaseNum)

+                {

+                    procToActionInfo[node.Proc].callerPhaseNums.Add(enclosingProcPhaseNum);

+                }

+                else

                 {

-                    Error(node, "The phase of the caller procedure must be greater than the phase of the callee");    

+                    Error(node, "The phase of the caller procedure must be greater than the phase of the callee");

                 }

             }

             return base.VisitCallCmd(node);

         }

+        public override Cmd VisitParCallCmd(ParCallCmd node)

+        {

+            globalVarAccessAllowed = false;

+            foreach (CallCmd callCmd in node.CallCmds)

+            {

+                base.VisitCallCmd(callCmd);

+            }

+

+            if (enclosingProcPhaseNum == int.MaxValue)

+                return node;

+

+            int maxCalleePhaseNum = 0;

+            foreach (CallCmd iter in node.CallCmds)

+            {

+                int calleePhaseNum = FindPhaseNumber(iter.Proc);

+                if (calleePhaseNum < maxCalleePhaseNum)

+                    maxCalleePhaseNum = calleePhaseNum;

+            }

+

+            if (enclosingProcPhaseNum > maxCalleePhaseNum)

+            {

+                bool isLeftMover = true;

+                bool isRightMover = true;

+                foreach (CallCmd iter in node.CallCmds)

+                {

+                    ActionInfo actionInfo = procToActionInfo[iter.Proc];

+                    isLeftMover = isLeftMover && actionInfo.IsLeftMover;

+                    isRightMover = isRightMover && actionInfo.IsRightMover;

+                    actionInfo.callerPhaseNums.Add(enclosingProcPhaseNum);

+                }

+                if (!isLeftMover && !isRightMover)

+                {

+                    Error(node, "The procedures in the parallel call must be all right mover or all left mover");

+                }

+            }

+            return node;

+        }

         public override YieldCmd VisitYieldCmd(YieldCmd node)

         {

             globalVarAccessAllowed = true;

@@ -120,7 +164,7 @@ namespace Microsoft.Boogie
         public override Ensures VisitEnsures(Ensures ensures)

         {

             int phaseNum = QKeyValue.FindIntAttribute(ensures.Attributes, "phase", 0);

-            if (phaseNum > phaseNumEnclosingProc)

+            if (phaseNum > enclosingProcPhaseNum)

             {

                 Error(ensures, "The phase of ensures clause cannot be greater than the phase of enclosing procedure");

             }

@@ -132,7 +176,7 @@ namespace Microsoft.Boogie
         public override Requires VisitRequires(Requires requires)

         {

             int phaseNum = QKeyValue.FindIntAttribute(requires.Attributes, "phase", 0);

-            if (phaseNum > phaseNumEnclosingProc)

+            if (phaseNum > enclosingProcPhaseNum)

             {

                 Error(requires, "The phase of requires clause cannot be greater than the phase of enclosing procedure");

             }

@@ -144,7 +188,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssertCmd(AssertCmd node)

         {

             int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", 0);

-            if (phaseNum > phaseNumEnclosingProc)

+            if (phaseNum > enclosingProcPhaseNum)

             {

                 Error(node, "The phase of assert cannot be greater than the phase of enclosing procedure");

             }

@@ -156,7 +200,7 @@ namespace Microsoft.Boogie
         public override Cmd VisitAssumeCmd(AssumeCmd node)

         {

             int phaseNum = QKeyValue.FindIntAttribute(node.Attributes, "phase", 0);

-            if (phaseNum > phaseNumEnclosingProc)

+            if (phaseNum > enclosingProcPhaseNum)

             {

                 Error(node, "The phase of assume cannot be greater than the phase of enclosing procedure");

             }