[Civl] Remove ISR code (#1007)

Author: shazqadeer

Source/Concurrency/InductiveSequentialization.cs

@@ -81,7 +81,7 @@ where first.IsRightMover || second.IsLeftMover
        * obviates the need to generate it.
        */
 
-      foreach (var sequentialization in civlTypeChecker.Sequentializations.Where(x => x.rule == InductiveSequentializationRule.ISL))
+      foreach (var sequentialization in civlTypeChecker.Sequentializations)
       {
         foreach (var leftMover in sequentialization.EliminatedActions)
         {
@@ -114,28 +114,6 @@ where first.IsRightMover || second.IsLeftMover
           }
         }
       }
-
-      foreach (var sequentialization in civlTypeChecker.Sequentializations.Where(x => x.rule == InductiveSequentializationRule.ISR))
-      {
-        foreach (var rightMover in sequentialization.EliminatedActions.Append(sequentialization.TargetAction))
-        {
-          foreach (var action in civlTypeChecker.MoverActions.Where(x => x.LayerRange.Contains(sequentialization.Layer)))
-          {
-            var moverCheckContext1 = new MoverCheckContext
-            {
-              layer = sequentialization.Layer,
-              extraAssumptions = sequentialization.GenerateRightMoverCheckAssumptions(rightMover, rightMover.FirstImpl.InParams)
-            };
-            var moverCheckContext2 = new MoverCheckContext
-            {
-              layer = sequentialization.Layer,
-              extraAssumptions = sequentialization.GenerateRightMoverCheckAssumptions(rightMover, rightMover.SecondImpl.InParams)
-            };
-            moverChecking.CreateCommutativityChecker(rightMover, action, moverCheckContext1);
-            moverChecking.CreateGatePreservationChecker(action, rightMover, moverCheckContext2);
-          }
-        }
-      }
     }
 
     private IEnumerable<Requires> DisjointnessAndWellFormedRequires(IEnumerable<Variable> paramVars, HashSet<Variable> frame)

Source/Concurrency/MoverCheck.cs

@@ -323,49 +323,33 @@ void CheckModifies(IEnumerable<Variable> modifiedVars)
               {
                 tc.Error(this, "caller must not be a mover procedure");
               }
-              if (!IsAsync)
+              if (IsAsync)
               {
-                // check there is no application of IS_RIGHT in the entire chain of refined actions
-                var calleeRefinedAction = calleeDecl.RefinedAction;
-                while (calleeRefinedAction != null)
+                if (isSynchronized)
                 {
-                  if (calleeRefinedAction.HasAttribute(CivlAttributes.IS_RIGHT))
+                  // check that entire chain of refined actions all the way to highestRefinedAction is comprised of left movers
+                  var calleeRefinedAction = calleeDecl.RefinedAction;
+                  while (calleeRefinedAction != null)
                   {
-                    tc.Error(this, "this must be an async call");
-                    break;
+                    var calleeActionDecl = calleeRefinedAction.ActionDecl;
+                    if (!calleeActionDecl.IsLeftMover)
+                    {
+                      tc.Error(this,
+                        $"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
+                      break;
+                    }
+                    if (calleeActionDecl == highestRefinedActionDecl)
+                    {
+                      break;
+                    }
+                    calleeRefinedAction = calleeActionDecl.RefinedAction;
                   }
-                  var calleeActionDecl = calleeRefinedAction.ActionDecl;
-                  if (calleeActionDecl == highestRefinedActionDecl)
-                  {
-                    break;
-                  }
-                  calleeRefinedAction = calleeActionDecl.RefinedAction;
                 }
-              }
-              else if (isSynchronized)
-              {
-                // check that entire chain of refined actions all the way to highestRefinedAction is comprised of left movers
-                var calleeRefinedAction = calleeDecl.RefinedAction;
-                while (calleeRefinedAction != null)
+                else if (callerDecl.HasMoverType)
                 {
-                  var calleeActionDecl = calleeRefinedAction.ActionDecl;
-                  if (!calleeActionDecl.IsLeftMover)
-                  {
-                    tc.Error(this,
-                      $"callee abstraction in synchronized call must be a left mover: {calleeActionDecl.Name}");
-                    break;
-                  }
-                  if (calleeActionDecl == highestRefinedActionDecl)
-                  {
-                    break;
-                  }
-                  calleeRefinedAction = calleeActionDecl.RefinedAction;
+                  tc.Error(this, "async call must be synchronized in mover procedure");
                 }
               }
-              else if (callerDecl.HasMoverType)
-              {
-                tc.Error(this, "async call must be synchronized");
-              }
             }
           }
         }

Source/Core/AST/Commands/CallCmd.cs

@@ -86,10 +86,8 @@ public static class CivlAttributes
     public const string HIDE = "hide";
     public const string PENDING_ASYNC = "pending_async";
     public const string SYNC = "sync";
-    public const string IS_RIGHT = "IS_right";
-    public const string IS_LEFT = "IS_left";
 
-    private static string[] CIVL_ATTRIBUTES = { LAYER, YIELDS, MARK, HIDE, PENDING_ASYNC, SYNC, IS_LEFT, IS_RIGHT };
+    private static string[] CIVL_ATTRIBUTES = { LAYER, YIELDS, MARK, HIDE, PENDING_ASYNC, SYNC };
 
     public const string LINEAR = "linear";
     public const string LINEAR_IN = "linear_in";

Source/Core/CivlAttributes.cs

@@ -1,4 +1,4 @@
-// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %parallel-boogie -timeLimit:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 const N: int; // size of the ring

Test/civl/inductive-sequentialization/ChangRoberts.bpl

@@ -1,2 +1,2 @@
-issue-1005.bpl(14,10): Error: async call must be synchronized
+issue-1005.bpl(14,10): Error: async call must be synchronized in mover procedure
 1 type checking errors detected in issue-1005.bpl