From 74a4744b6d51dd05ce511047b6c77e083458ac13 Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <shaz@fb.com>
Date: Thu, 9 Nov 2023 05:56:35 -0800
Subject: [PATCH] miscellaneous bug fixes

---
 Source/Concurrency/CivlTypeChecker.cs       | 2 +-
 Source/Concurrency/LinearDomainCollector.cs | 9 +++++++++
 Source/Concurrency/LinearTypeChecker.cs     | 1 +
 Source/Core/AST/AbsyExpr.cs                 | 9 +++------
 4 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index 179cc552d..a123a36d6 100644
--- 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
index 61be6bfe0..8a1341093 100644
--- 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
index 85c3ec3d7..44a233f26 100644
--- 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
index 33a8b1788..62c108329 100644
--- 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}");
             }