added right mover checks

Source/Concurrency/CivlCoreTypes.cs

@@ -86,6 +86,8 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
 
     public int PendingAsyncStartIndex => ActionDecl.OutParams.Count;
 
+    public Expr ExitCondition => ActionDecl.FindExprAttribute("exit_condition");
+
     public bool TriviallyCommutesWith(Action other)
     {
       return !this.ModifiedGlobalVars.Intersect(other.UsedGlobalVarsInAction).Any() &&

Source/Concurrency/InductiveSequentialization.cs

@@ -58,12 +58,17 @@ protected virtual List<Declaration> GenerateCheckers()
       return decls;
     }
 
-    public virtual IEnumerable<Expr> GenerateMoverCheckAssumptions(Action action, List<Variable> actionArgs, Action leftMover,
+    public virtual IEnumerable<Expr> GenerateLeftMoverCheckAssumptions(Action action, List<Variable> actionArgs, Action leftMover,
       List<Variable> leftMoverArgs)
     {
       return new List<Expr>();
     }
 
+    public virtual IEnumerable<Expr> GenerateRightMoverCheckAssumptions(Action rightMover, List<Variable> rightMoverArgs)
+    {
+      return new List<Expr>();
+    }
+
     public IEnumerable<AssertCmd> Preconditions(Action pendingAsync, Substitution subst)
     {
       var cmds = new List<AssertCmd>();
@@ -632,7 +637,7 @@ private List<Declaration> GenerateInconsistencyChecker(Action E1, Action E2)
         targetAction.tok,
         Expr.Not(Expr.And(Substituter.Apply(substE1, gateE1), Substituter.Apply(substE2, Expr.And(GetExitCondition(E2), gateE2)))) ,
         $"Inconsistency check failed for {targetAction.Name}, {E1.Name}, {E2.Name}"));
-
+      
       CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
       return GetCheckerTuple($"{rule}_InconsistencyChecker_{targetAction.Name}_{E1.Name}_{E2.Name}", new List<Requires>(),
         new List<Variable>(), new List<Variable>(), locals,  cmds);
@@ -646,23 +651,16 @@ private Expr GetNonBlockExpression(Action action)
       return TransitionRelationComputation.Cooperation(civlTypeChecker, action, frame);
     }
 
-    private Expr GetExitCondition(Action action){
-       Expr X = Expr.False;
-       var assumeCmds = action.Impl.Blocks[0].Cmds.OfType<AssumeCmd>();
-       foreach (var c in assumeCmds) 
-      {
-        var ex = QKeyValue.FindAttribute(c.Attributes, i => (i.Key == "exit_condition"));
-        if (ex != null)
-        {
-          X = (Expr)ex.Params[0];
-        }
-      }
-       return X;
+    private Expr GetExitCondition(Action action)
+    {
+      var subst = Substituter.SubstitutionFromDictionary(
+        action.ActionDecl.InParams.Zip(action.Impl.InParams.Select(x => (Expr)Expr.Ident(x))).ToDictionary(x => x.Item1, x => x.Item2));
+      var exitCondition = action.ExitCondition;
+      return exitCondition == null ? Expr.False : Substituter.Apply(subst, exitCondition);
     }
 
     protected List<Declaration> GenerateExitConditionProperty1Checker(Action action)
     {
-      var exit = GetExitCondition(action);
       var eliminatedActionDecls = EliminatedActionDecls.ToHashSet();
       var elimExprs = new List<Expr>();
       var notElimExprs = new List<Expr>();
@@ -685,14 +683,13 @@ protected List<Declaration> GenerateExitConditionProperty1Checker(Action action)
         GetCheck(action.tok, Expr.And(elimExprs), "Exit condition property 1 failed"),
       };
 
-      // CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
+      //CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
       return GetCheckerTuple($"{rule}_ExitProperty1Checker_{action.Name}", new List<Requires>(),
         action.Impl.InParams, action.Impl.OutParams, new List<Variable>(),  cmds);
     }
 
     protected List<Declaration> GenerateExitConditionProperty2Checker(Action action)
     {
-      var exit = GetExitCondition(action);
       var eliminatedActionDecls = EliminatedActionDecls.ToHashSet();
       var elimExprs = new List<Expr>();
       var notElimExprs = new List<Expr>();
@@ -715,10 +712,21 @@ protected List<Declaration> GenerateExitConditionProperty2Checker(Action action)
         GetCheck(action.tok, Expr.And(notElimExprs), "Exit condition property 2 failed"),
       };
 
-      // CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
+      //CivlUtil.ResolveAndTypecheck(civlTypeChecker.Options, cmds);
       return GetCheckerTuple($"{rule}_ExitProperty2Checker_{action.Name}", new List<Requires>(),
         action.Impl.InParams, action.Impl.OutParams, new List<Variable>(),  cmds);
     }
+
+    public override IEnumerable<Expr> GenerateRightMoverCheckAssumptions(Action rightMover, List<Variable> rightMoverArgs)
+    {
+      var subst = Substituter.SubstitutionFromDictionary(
+        rightMover.ActionDecl.InParams.Zip(rightMoverArgs.Select(x => (Expr)Expr.Ident(x))).ToDictionary(x => x.Item1, x => x.Item2));
+      var exitCondition = rightMover.ExitCondition;
+      return new List<Expr> {
+        exitCondition == null ? Expr.False : Substituter.Apply(subst, exitCondition)
+      };
+    }
+
     /*
      * This method generates the extra assumption for the left-mover check of the abstraction of an eliminated action.
      * The arguments leftMover and leftMoverArgs pertain to the action being moved left.
@@ -735,7 +743,7 @@ protected List<Declaration> GenerateExitConditionProperty2Checker(Action action)
      *   (1) the permissions in the invocation are disjoint from the permissions in the invariant invocation, or
      *   (2) the permissions in the invocation is contained in the permissions of one of the pending asyncs created by the invariant invocation.
      */
-    public override IEnumerable<Expr> GenerateMoverCheckAssumptions(Action action, List<Variable> actionArgs, Action leftMover,
+    public override IEnumerable<Expr> GenerateLeftMoverCheckAssumptions(Action action, List<Variable> actionArgs, Action leftMover,
       List<Variable> leftMoverArgs)
     {
       var invariantFormalMap =

Source/Concurrency/MoverCheck.cs

@@ -90,12 +90,12 @@ where first.IsRightMover || second.IsLeftMover
             var moverCheckContext1 = new MoverCheckContext
             {
               layer = sequentialization.Layer,
-              extraAssumptions = sequentialization.GenerateMoverCheckAssumptions(action, action.FirstImpl.InParams, leftMover, leftMover.SecondImpl.InParams)
+              extraAssumptions = sequentialization.GenerateLeftMoverCheckAssumptions(action, action.FirstImpl.InParams, leftMover, leftMover.SecondImpl.InParams)
             };
             var moverCheckContext2 = new MoverCheckContext
             {
               layer = sequentialization.Layer,
-              extraAssumptions = sequentialization.GenerateMoverCheckAssumptions(action, action.SecondImpl.InParams, leftMover, leftMover.FirstImpl.InParams)
+              extraAssumptions = sequentialization.GenerateLeftMoverCheckAssumptions(action, action.SecondImpl.InParams, leftMover, leftMover.FirstImpl.InParams)
             };
             moverChecking.CreateCommutativityChecker(action, leftMover, moverCheckContext1);
             moverChecking.CreateGatePreservationChecker(leftMover, action, moverCheckContext2);
@@ -121,7 +121,18 @@ where first.IsRightMover || second.IsLeftMover
         {
           foreach (var action in civlTypeChecker.MoverActions.Where(x => x.LayerRange.Contains(sequentialization.Layer)))
           {
-            // moverChecking.CreateRightMoverCheckers(rightMover, action);
+            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);
           }
         }
       }

Source/Core/AST/Absy.cs

@@ -260,12 +260,15 @@ public void ResolveAttributes(ResolutionContext rc)
       }
     }
 
-    public void TypecheckAttributes(TypecheckingContext rc)
+    public void TypecheckAttributes(TypecheckingContext tc)
     {
+      var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld;
+      tc.GlobalAccessOnlyInOld = false;
       for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
       {
-        kv.Typecheck(rc);
+        kv.Typecheck(tc);
       }
+      tc.GlobalAccessOnlyInOld = oldGlobalAccessOnlyInOld;
     }
 
     public List<int> FindLayers()

Test/civl/inductive-sequentialization/snapshot-IS2-part.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 13 verified, 0 errors
+Boogie program verifier finished with 15 verified, 0 errors

Test/civl/inductive-sequentialization/snapshot-scatter-gather-full.bpl

@@ -63,15 +63,14 @@ modifies r1, pSet;
 
 }
 
-async action {:layer 1} read_f({:linear_in} perm: One Permission)
+async action {:layer 1} {:exit_condition Set_IsSubset(WholeTidPermission(perm->val->t_id), Set_Add(pSet, perm->val))} read_f({:linear_in} perm: One Permission)
 creates read_f, main_s;
 modifies r1, pSet;
 {
     var {:pool "K"} k:int;
     var {:pool "V"} v:Value;
     assert 1 <= perm->val->mem_index && perm->val->mem_index <=n;
     assume {:add_to_pool "A", 0, n} true;
-    assume {:exit_condition Set_IsSubset(WholeTidPermission(perm->val->t_id), Set_Add(pSet, perm->val) )} true;
 
     if (*) {
         assume {:add_to_pool "K", mem[perm->val->mem_index]->ts, k} {:add_to_pool "V", mem[perm->val->mem_index]->value, v} true;

Test/civl/inductive-sequentialization/snapshot-scatter-gather-full.bpl.expect

@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 15 verified, 0 errors
+Boogie program verifier finished with 20 verified, 0 errors