[Civl] miscellaneous bug fixes (#806)

boogie-org · Nov 9, 2023 · aa56ffb · aa56ffb
1 parent df0de3b
commit aa56ffb
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 7 deletions.
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
@@ -385,7 +385,7 @@ public static void CheckRefinementSignature(YieldProcedureDecl proc, CheckingCon
         var procInParams = proc.InParams.Where(x => proc.VisibleFormals.Contains(x)).ToList();
         var procOutParams = proc.OutParams.Where(x => proc.VisibleFormals.Contains(x)).ToList();
         var actionInParams = refinedActionDecl.InParams;
-        var actionOutParams = refinedActionDecl.OutParams.SkipLast(refinedActionDecl.Creates.Count).ToList();
+        var actionOutParams = refinedActionDecl.OutParams;
         signatureMatcher.MatchFormals(procInParams, actionInParams, SignatureMatcher.IN);
         signatureMatcher.MatchFormals(procOutParams, actionOutParams, SignatureMatcher.OUT);
       }

diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs
@@ -158,6 +158,15 @@ private bool ContainsPermissionType(Type type)
             }));
           }
         }
+        if (type is MapType mapType)
+        {
+          mapType.Arguments.ForEach(argType => ContainsPermissionType(argType));
+          ContainsPermissionType(mapType.Result);
+          if (ContainsPermissionType(mapType.Result))
+          {
+            linearTypes.Add(type);
+          }
+        }
       }
       return linearTypes.Contains(type);
     }

diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs
@@ -408,6 +408,7 @@ lheapValExpr.Args[0].Type is CtorType ctorType &&
           {
             return ExtractRootFromAccessPathExpr(lheapValExpr.Args[0]);
           }
+          return ExtractRootFromAccessPathExpr(nAryExpr.Args[0]);
         }
       }
       return null;

diff --git a/Source/Core/AST/AbsyExpr.cs b/Source/Core/AST/AbsyExpr.cs
@@ -1357,12 +1357,9 @@ public override void Typecheck(TypecheckingContext tc)
           if (Decl is GlobalVariable)
           {
             var globalVarLayerRange = Decl.LayerRange;
-            if (actionDecl.HasMoverType)
-            {
-              // a global variable introduced at layer n is visible to a mover action only at layer n+1 or higher
-              globalVarLayerRange = new LayerRange(globalVarLayerRange.LowerLayer + 1, globalVarLayerRange.UpperLayer);
-            }
-            if (!actionDecl.LayerRange.Subset(globalVarLayerRange))
+            if (!actionDecl.LayerRange.Subset(globalVarLayerRange) ||
+                // a global variable introduced at layer n is visible to a mover action only at layer n+1 or higher
+                actionDecl.HasMoverType && actionDecl.LayerRange.LowerLayer == globalVarLayerRange.LowerLayer)
             {
               tc.Error(this, $"variable not available across layers in {actionDecl.LayerRange}: {Decl.Name}");
             }