[Civl] Fixes issue 1094

Source/Concurrency/CivlTypeChecker.cs

@@ -67,7 +67,7 @@ public CivlTypeChecker(ConcurrencyOptions options, Program program)
         program.AddTopLevelDeclaration(skipImplementation);
       }
       program.TopLevelDeclarations.OfType<YieldProcedureDecl>()
-        .Where(decl => !decl.HasMoverType && decl.RefinedAction == null).ForEach(decl =>
+        .Where(decl => !decl.MoverType.HasValue && decl.RefinedAction == null).ForEach(decl =>
         {
           decl.RefinedAction = new ActionDeclRef(Token.NoToken, SkipActionDecl.Name)
           {
@@ -358,8 +358,7 @@ public IEnumerable<Variable> GlobalVariablesAtLayer(int layerNum)
       return GlobalVariables.Where(v => v.LayerRange.LowerLayer <= layerNum && layerNum < v.LayerRange.UpperLayer);
     }
 
-    public IEnumerable<Action> MoverActions => actionDeclToAction.Keys
-      .Where(actionDecl => actionDecl.HasMoverType).Select(actionDecl => actionDeclToAction[actionDecl]);
+    public IEnumerable<Action> MoverActions => actionDeclToAction.Keys.Select(actionDecl => actionDeclToAction[actionDecl]);
 
     public IEnumerable<Action> AtomicActions => actionDeclToAction.Values;
 

Source/Concurrency/YieldSufficiencyChecker.cs

@@ -225,7 +225,7 @@ private void AtomicityCheck()
         }
       }
 
-      private bool IsMoverProcedure => yieldingProc.HasMoverType && yieldingProc.Layer == currLayerNum;
+      private bool IsMoverProcedure => yieldingProc.MoverType.HasValue && yieldingProc.Layer == currLayerNum;
 
       private bool CheckAtomicity(Dictionary<Absy, HashSet<int>> simulationRelation)
       {
@@ -331,12 +331,12 @@ private string CallCmdLabel(CallCmd callCmd)
         var callee = (YieldProcedureDecl)callCmd.Proc;
         if (callCmd.IsAsync)
         {
-          if (callee.HasMoverType && callee.Layer == currLayerNum)
+          if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
           {
-            return MoverTypeToLabel(callee.MoverType);
+            return MoverTypeToLabel(callee.MoverType.Value);
           }
 
-          if (!callee.HasMoverType && callee.Layer < currLayerNum && callCmd.HasAttribute(CivlAttributes.SYNC))
+          if (!callee.MoverType.HasValue && callee.Layer < currLayerNum && callCmd.HasAttribute(CivlAttributes.SYNC))
           {
             return MoverTypeToLabel(callee.RefinedActionAtLayer(currLayerNum).MoverType);
           }
@@ -345,12 +345,12 @@ private string CallCmdLabel(CallCmd callCmd)
         }
         else
         {
-          if (callee.HasMoverType && callee.Layer == currLayerNum)
+          if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
           {
-            return MoverTypeToLabel(callee.MoverType);
+            return MoverTypeToLabel(callee.MoverType.Value);
           }
 
-          if (!callee.HasMoverType && callee.Layer < currLayerNum)
+          if (!callee.MoverType.HasValue && callee.Layer < currLayerNum)
           {
             return MoverTypeToLabel(callee.RefinedActionAtLayer(currLayerNum).MoverType);
           }
@@ -400,12 +400,12 @@ private string CallCmdLabelAsync(CallCmd callCmd)
         var callee = (YieldProcedureDecl)callCmd.Proc;
         if (callCmd.IsAsync)
         {
-          if (callee.HasMoverType && callee.Layer == currLayerNum)
+          if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
           {
             return ModifiesGlobalLabel(callee.Modifies);
           }
 
-          if (!callee.HasMoverType && callee.Layer < currLayerNum)
+          if (!callee.MoverType.HasValue && callee.Layer < currLayerNum)
           {
             if (callCmd.HasAttribute(CivlAttributes.SYNC))
             {
@@ -428,12 +428,12 @@ private string CallCmdLabelAsync(CallCmd callCmd)
         }
         else
         {
-          if (callee.HasMoverType && callee.Layer == currLayerNum)
+          if (callee.MoverType.HasValue && callee.Layer == currLayerNum)
           {
             return ModifiesGlobalLabel(callee.Modifies);
           }
 
-          if (!callee.HasMoverType && callee.Layer < currLayerNum)
+          if (!callee.MoverType.HasValue && callee.Layer < currLayerNum)
           {
             return ModifiesGlobalLabel(callee.RefinedActionAtLayer(currLayerNum).ModifiedVars);
           }

Source/Concurrency/YieldingProcChecker.cs

@@ -31,7 +31,7 @@ public static void AddInvariantCheckers(CivlTypeChecker civlTypeChecker, List<De
         {
           var yieldProcedureDecl = (YieldProcedureDecl)impl.Proc;
           if (yieldProcedureDecl.Layer > layerNum ||
-              yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.HasMoverType)
+              yieldProcedureDecl.Layer == layerNum && !yieldProcedureDecl.MoverType.HasValue)
           {
             duplicator.VisitImplementation(impl);
           }

Source/Concurrency/YieldingProcDuplicator.cs

@@ -52,7 +52,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node)
         var requires = VisitRequiresSeq(node.Requires);
         var preserves = VisitRequiresSeq(node.Preserves);
         var ensures = VisitEnsuresSeq(node.Ensures);
-        if (node.HasMoverType && layerNum == node.Layer && !doRefinementCheck)
+        if (node.MoverType.HasValue && layerNum == node.Layer && !doRefinementCheck)
         {
           requires = requires.Select(req => new Requires(req.tok, true, req.Condition, req.Comment, req.Attributes)).ToList();
           preserves = preserves.Select(req => new Requires(req.tok, true, req.Condition, req.Comment, req.Attributes)).ToList();
@@ -70,7 +70,7 @@ public override Procedure VisitYieldProcedureDecl(YieldProcedureDecl node)
           requires,
           [],
           ensures,
-          (node.HasMoverType && node.Layer == layerNum
+          (node.MoverType.HasValue && node.Layer == layerNum
             ? node.ModifiedVars.Select(Expr.Ident)
             : civlTypeChecker.GlobalVariables.Select(v => Expr.Ident(v))).ToList()
           );
@@ -304,7 +304,7 @@ cmd is AssertCmd assertCmd && makeAssume
       {
         if (yieldingProc.Layer < layerNum)
         {
-          Debug.Assert(!yieldingProc.HasMoverType);
+          Debug.Assert(!yieldingProc.MoverType.HasValue);
           if (newCall.HasAttribute(CivlAttributes.SYNC))
           {
             // synchronize the called atomic action
@@ -313,14 +313,14 @@ cmd is AssertCmd assertCmd && makeAssume
         }
         else
         {
-          if (yieldingProc.HasMoverType && yieldingProc.Layer == layerNum)
+          if (yieldingProc.MoverType.HasValue && yieldingProc.Layer == layerNum)
           {
             // synchronize the called mover procedure
             AddDuplicateCall(newCall, false);
           }
           else if (doRefinementCheck)
           {
-            Debug.Assert(!yieldingProc.HasMoverType);
+            Debug.Assert(!yieldingProc.MoverType.HasValue);
           }
           else
           {
@@ -331,7 +331,7 @@ cmd is AssertCmd assertCmd && makeAssume
       }
 
       // handle synchronous calls to yielding procedures
-      if (yieldingProc.HasMoverType)
+      if (yieldingProc.MoverType.HasValue)
       {
         AddDuplicateCall(newCall, yieldingProc.Layer > layerNum);
       }
@@ -400,8 +400,8 @@ void ProcessPendingCallCmds()
       {
         if (callCmd.Proc is YieldProcedureDecl yieldingProc)
         {
-          Debug.Assert(layerNum <= yieldingProc.Layer || !yieldingProc.HasMoverType);
-          if (layerNum > yieldingProc.Layer || layerNum == yieldingProc.Layer && yieldingProc.HasMoverType)
+          Debug.Assert(layerNum <= yieldingProc.Layer || !yieldingProc.MoverType.HasValue);
+          if (layerNum > yieldingProc.Layer || layerNum == yieldingProc.Layer && yieldingProc.MoverType.HasValue)
           {
             ProcessPendingCallCmds();
             ProcessCallCmd(callCmd);

Source/Concurrency/YieldingProcInstrumentation.cs

@@ -354,7 +354,7 @@ private void TransformImpls(Dictionary<Implementation, List<Cmd>> implToPrecondi
         // For mover procedures, simply add disjointness assumptions at the beginning of the first block.
         linearPermissionInstrumentation.AddDisjointnessAndWellFormedAssumptions(impl);
         var yieldingProc = GetYieldingProc(impl);
-        if (yieldingProc.HasMoverType && yieldingProc.Layer == layerNum)
+        if (yieldingProc.MoverType.HasValue && yieldingProc.Layer == layerNum)
         {
           impl.Blocks[0].Cmds.InsertRange(0, linearPermissionInstrumentation.DisjointnessAndWellFormedAssumeCmds(impl, true));
         }

Source/Core/AST/Absy.cs

@@ -2721,7 +2721,7 @@ void TypecheckSpec(List<int> layers, Action<TypecheckingContext> f)
       {
         var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld;
         if (this is YieldProcedureDecl yieldProcedureDecl &&
-            (!yieldProcedureDecl.HasMoverType || layers.Any(layer => layer < yieldProcedureDecl.Layer)))
+            (!yieldProcedureDecl.MoverType.HasValue || layers.Any(layer => layer < yieldProcedureDecl.Layer)))
         {
           tc.GlobalAccessOnlyInOld = true;
         }
@@ -2736,9 +2736,9 @@ void TypecheckSpec(List<int> layers, Action<TypecheckingContext> f)
       foreach (Requires e in Preserves)
       {
         if (this is YieldProcedureDecl yieldProcedureDecl &&
-            (!yieldProcedureDecl.HasMoverType || e.Layers.Any(layer => layer < yieldProcedureDecl.Layer)))
+            (!yieldProcedureDecl.MoverType.HasValue || e.Layers.Any(layer => layer < yieldProcedureDecl.Layer)))
         {
-          if (yieldProcedureDecl.HasMoverType)
+          if (yieldProcedureDecl.MoverType.HasValue)
           {
             tc.Error(e, $"only layer {yieldProcedureDecl.Layer} allowed for preserves clause");
           }
@@ -2864,7 +2864,6 @@ public enum MoverType
     Right,
     Left,
     Both,
-    None
   }
 
   public class ActionDecl : Procedure
@@ -2922,14 +2921,6 @@ public override void Resolve(ResolutionContext rc)
       if (RefinedAction != null)
       {
         RefinedAction.Resolve(rc);
-        if (!HasMoverType)
-        {
-          MoverType = MoverType.Atomic;
-        }
-        if (RefinedAction.ActionDecl is { HasMoverType: false })
-        {
-          RefinedAction.ActionDecl.MoverType = MoverType.Atomic;
-        }
       }
     }
 
@@ -3025,8 +3016,6 @@ public IEnumerable<ActionDeclRef> ActionDeclRefs()
 
     public bool HasPreconditions => Requires.Count > 0 || YieldRequires.Count > 0;
 
-    public bool HasMoverType => MoverType != MoverType.None;
-
     public bool IsRightMover => MoverType == MoverType.Right || MoverType == MoverType.Both;
 
     public bool IsLeftMover => MoverType == MoverType.Left || MoverType == MoverType.Both;
@@ -3051,7 +3040,7 @@ public YieldingLoop(int layer, List<CallCmd> yieldInvariants)
 
   public class YieldProcedureDecl : Procedure
   {
-    public MoverType MoverType;
+    public MoverType? MoverType;
     public List<CallCmd> YieldRequires;
     public List<CallCmd> YieldPreserves;
     public List<CallCmd> YieldEnsures;
@@ -3061,7 +3050,7 @@ public class YieldProcedureDecl : Procedure
     public HashSet<Variable> VisibleFormals; // set during resolution
     public Dictionary<Block, YieldingLoop> YieldingLoops; // empty initially, filled up during type checking
 
-    public YieldProcedureDecl(IToken tok, string name, MoverType moverType, List<Variable> inParams,
+    public YieldProcedureDecl(IToken tok, string name, MoverType? moverType, List<Variable> inParams,
       List<Variable> outParams,
       List<Requires> requires, List<Requires> preserves, List<Ensures> ensures, List<IdentifierExpr> modifies,
       List<CallCmd> yieldRequires, List<CallCmd> yieldPreserves, List<CallCmd> yieldEnsures,
@@ -3117,7 +3106,7 @@ public override void Resolve(ResolutionContext rc)
       rc.StateMode = oldStateMode;
       rc.Proc = null;
 
-      if (!HasMoverType)
+      if (!MoverType.HasValue)
       {
         VisibleFormals = RefinedAction == null
           ? new HashSet<Variable>()
@@ -3128,13 +3117,9 @@ public override void Resolve(ResolutionContext rc)
       if (RefinedAction != null)
       {
         RefinedAction.Resolve(rc);
-        if (RefinedAction.ActionDecl is { HasMoverType: false })
-        {
-          RefinedAction.ActionDecl.MoverType = MoverType.Atomic;
-        }
       }
 
-      if (!HasMoverType)
+      if (!MoverType.HasValue)
       {
         if (Modifies.Any())
         {
@@ -3160,7 +3145,7 @@ public override void Typecheck(TypecheckingContext tc)
         }
       }
 
-      if (HasMoverType)
+      if (MoverType.HasValue)
       {
         Modifies.Where(ie => !ie.Decl.LayerRange.Contains(Layer)).ForEach(ie =>
         {
@@ -3219,12 +3204,10 @@ public IEnumerable<CallCmd> CallCmds()
     {
       return YieldEnsures.Union(YieldPreserves).Union(YieldRequires);
     }
-
-    public bool HasMoverType => MoverType != MoverType.None;
 
-    public bool IsRightMover => MoverType == MoverType.Right || MoverType == MoverType.Both;
+    public bool IsRightMover => MoverType.HasValue && (MoverType.Value == Boogie.MoverType.Right || MoverType.Value == Boogie.MoverType.Both);
 
-    public bool IsLeftMover => MoverType == MoverType.Left || MoverType == MoverType.Both;
+    public bool IsLeftMover => MoverType.HasValue && (MoverType.Value == Boogie.MoverType.Left || MoverType.Value == Boogie.MoverType.Both);
 
     public ActionDecl RefinedActionAtLayer(int layer)
     {

Source/Core/AST/Commands/AbsyCmd.cs

@@ -1555,7 +1555,7 @@ public override void Typecheck(TypecheckingContext tc)
       }
 
       var callerDecl = (YieldProcedureDecl)tc.Proc;
-      if (callerDecl.HasMoverType)
+      if (callerDecl.MoverType.HasValue)
       {
         return;
       }

Source/Core/AST/Commands/CallCmd.cs

@@ -312,7 +312,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
         tc.Error(this, "layer of callee must not be more than layer of caller");
         return;
       }
-      if (!calleeDecl.HasMoverType && calleeDecl.RefinedAction == null)
+      if (!calleeDecl.MoverType.HasValue && calleeDecl.RefinedAction == null)
       {
         return;
       }
@@ -323,7 +323,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
         return;
       }
       // call is synchronous or synchronized
-      if (!calleeDecl.HasMoverType)
+      if (!calleeDecl.MoverType.HasValue)
       {
         Debug.Assert(calleeDecl.RefinedAction != null);
         if (callerDecl.Layer > calleeDecl.Layer)
@@ -340,7 +340,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
         }
         else // callerDecl.Layer == calleeDecl.Layer
         {
-          if (callerDecl.HasMoverType)
+          if (callerDecl.MoverType.HasValue)
           {
             tc.Error(this, "caller must not be a mover procedure");
           }
@@ -350,7 +350,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
           }
         }
       }
-      else // calleeDecl.HasMoverType
+      else // calleeDecl.MoverType.HasValue
       {
         if (callerDecl.Layer > calleeDecl.Layer)
         {
@@ -372,7 +372,7 @@ void CheckRefinedChainIsLeftMover(YieldProcedureDecl callerDecl, YieldProcedureD
       {
         tc.Error(this, "layer of callee must not be more than layer of caller");
       }
-      else if (yieldInvariantDecl.Layer == callerDecl.Layer && callerDecl.HasMoverType)
+      else if (yieldInvariantDecl.Layer == callerDecl.Layer && callerDecl.MoverType.HasValue)
       {
         tc.Error(this, "layer of callee must be less than layer of caller");
       }
@@ -627,7 +627,7 @@ private LayerRange FormalLayerRange(YieldProcedureDecl callerDecl, Variable call
       case YieldProcedureDecl yieldProcedureDecl:
       {
         formalLayerRange = calleeFormal.LayerRange;
-        if (!yieldProcedureDecl.HasMoverType && yieldProcedureDecl.VisibleFormals.Contains(calleeFormal))
+        if (!yieldProcedureDecl.MoverType.HasValue && yieldProcedureDecl.VisibleFormals.Contains(calleeFormal))
         {
           formalLayerRange = new LayerRange(formalLayerRange.LowerLayer, callerDecl.Layer);
         }

Source/Core/Analysis/ModSetCollector.cs

@@ -23,7 +23,7 @@ public void CollectModifies(Program program)
   {
     var implementedProcs = new HashSet<Procedure>(program.Implementations.Where(impl => impl.Proc != null).Select(impl => impl.Proc));
     program.Procedures.Where(proc =>
-      proc.GetType() == typeof(Procedure) || proc is ActionDecl || (proc is YieldProcedureDecl yieldProcedureDecl && yieldProcedureDecl.HasMoverType))
+      proc.GetType() == typeof(Procedure) || proc is ActionDecl || (proc is YieldProcedureDecl yieldProcedureDecl && yieldProcedureDecl.MoverType.HasValue))
       .ForEach(proc =>
       {
         modSets.Add(proc, new HashSet<Variable>());
@@ -138,7 +138,7 @@ public override Cmd VisitCallCmd(CallCmd callCmd)
     Procedure callee = callCmd.Proc;
     Debug.Assert(callee != null);
     if (enclosingProc is YieldProcedureDecl callerDecl &&
-        callee is YieldProcedureDecl calleeDecl && !calleeDecl.HasMoverType && calleeDecl.RefinedAction != null)
+        callee is YieldProcedureDecl calleeDecl && !calleeDecl.MoverType.HasValue && calleeDecl.RefinedAction != null)
     {
       callee = calleeDecl.RefinedActionAtLayer(callerDecl.Layer);
     }