added a test

Source/Concurrency/LinearTypeChecker.cs

@@ -515,9 +515,14 @@ public override Cmd VisitUnpackCmd(UnpackCmd node)
           continue;
         }
         isLinearUnpack = true;
-        if (FindLinearKind(node.Constructor.InParams[j]) == LinearKind.ORDINARY)
+        var field = node.Constructor.InParams[j];
+        if (FindLinearKind(field) == LinearKind.ORDINARY)
         {
-          Error(unpackedLhs[j], $"source of unpack must be linear field: {node.Constructor.InParams[j]}");
+          Error(unpackedLhs[j], $"source of unpack must be linear field: {field}");
+        }
+        else if (InvalidAssignmentWithKeyCollection(unpackedLhs[j].Decl, field))
+        {
+          Error(unpackedLhs[j], $"Mismatch in key collection between source and target");
         }
       }
       if (isLinearUnpack)
@@ -644,17 +649,14 @@ enclosingProc is not YieldProcedureDecl &&
           {
             if (InvalidAssignmentWithKeyCollection(node.Outs[0].Decl, modifiedArgument))
             {
-              Error(node, $"Mismatch in key collection between source and target");
+              Error(node.Outs[0], $"Mismatch in key collection between source and target");
             }
           }
           else if (originalProc.Name == "Map_Join")
           {
-            if (node.Ins[1] is IdentifierExpr ie)
+            if (node.Ins[1] is IdentifierExpr ie && InvalidAssignmentWithKeyCollection(modifiedArgument, ie.Decl))
             {
-              if (InvalidAssignmentWithKeyCollection(modifiedArgument, ie.Decl))
-              {
-                Error(node, $"Mismatch in key collection between source and target");
-              }
+              Error(node.Ins[1], $"Mismatch in key collection between source and target");
             }
           }
           else if (originalProc.Name == "Map_Get" || originalProc.Name == "Map_Put")
@@ -672,6 +674,13 @@ enclosingProc is not YieldProcedureDecl &&
             }
           }
         }
+        else if (originalProc.Name == "Map_Unpack")
+        {
+          if (node.Ins[0] is IdentifierExpr ie && !AreKeysCollected(ie.Decl))
+          {
+            Error(node.Ins[0], $"Mismatch in key collection between source and target");
+          }
+        }
       }
 
       if (originalProc.Name == "create_multi_asyncs" || originalProc.Name == "create_asyncs")

Test/civl/regression-tests/no-collect-keys.bpl

@@ -0,0 +1,108 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+var {:linear "no_collect_keys"} {:layer 0,1} g: Map int int;
+var {:linear} {:layer 0,1} h: Map int int;
+
+atomic action {:layer 1} A()
+modifies g, h;
+{
+    var {:linear} l: Map int int;
+    var {:linear "no_collect_keys"} m: Map int int;
+    l := h;
+    h := l;
+    m := g;
+    g := m;
+}
+
+atomic action {:layer 1} B() {
+    var {:linear} l: Map int int;
+    var {:linear "no_collect_keys"} m: Map int int;
+    l := g;
+    m := h;
+}
+
+atomic action {:layer 1} X1({:linear "no_collect_keys"} a: Map int int)
+{
+
+}
+
+atomic action {:layer 1} Y1()
+{
+    var {:linear} l: Map int int;
+    call l := Map_MakeEmpty();
+    call X1(l);
+}
+
+atomic action {:layer 1} X2({:linear } a: Map int int)
+{
+
+}
+
+atomic action {:layer 1} Y2()
+{
+    var {:linear "no_collect_keys"} l: Map int int;
+    call l := Map_MakeEmpty();
+    call X2(l);
+}
+
+atomic action {:layer 1} X3() returns ({:linear "no_collect_keys"} a: Map int int)
+{
+    call a := Map_MakeEmpty();
+}
+
+atomic action {:layer 1} Y3()
+{
+    var {:linear} l: Map int int;
+    call l := X3();
+}
+
+atomic action {:layer 1} X4() returns ({:linear} a: Map int int)
+{
+    call a := Map_MakeEmpty();
+}
+
+datatype D { D({:linear "no_collect_keys"} d: Map int int) }
+
+datatype E { E({:linear} e: Map int int) }
+
+atomic action {:layer 1} Y4()
+{
+    var {:linear "no_collect_keys"} l: Map int int;
+    var {:linear} l': Map int int;
+    var {:linear} d: D;
+    var {:linear "no_collect_keys"} e: E;
+
+    call l := X4();
+    d := D(l);
+    D(l) := d;
+
+    call l' := Map_MakeEmpty();
+    d := D(l');
+    D(l') := d;
+
+    e := E(l');
+    e := E(l);
+}
+
+atomic action {:layer 1} C() {
+    var {:linear "no_collect_keys"} l: Map int int;
+    var {:linear} l': Map int int;
+    var {:linear} s: Set int;
+    var m: [int]int;
+    var {:linear} one_int: One int;
+    var i: int;
+
+    call l := Map_MakeEmpty();
+    call l' := Map_MakeEmpty();
+
+    call s, m := Map_Unpack(l);
+    call one_int, i := Map_Get(l, 0);
+    call Map_Put(l, one_int, i);
+    call i := Map_GetValue(l', 0);
+    call Map_PutValue(l', 0, i);
+    call l' := Map_Split(l, s);
+    call Map_Join(l', l);
+    call l := Map_Split(l', s);
+    call Map_Join(l, l');
+}

Test/civl/regression-tests/no-collect-keys.bpl.expect

@@ -0,0 +1,13 @@
+no-collect-keys.bpl(21,9): Error: Mismatch in key collection between source and target
+no-collect-keys.bpl(46,4): Error: Mismatch in key collection between source and target
+no-collect-keys.bpl(57,4): Error: Mismatch in key collection between source and target
+no-collect-keys.bpl(82,6): Error: Mismatch in key collection between source and target
+no-collect-keys.bpl(85,11): Error: Mismatch in key collection between source and target
+no-collect-keys.bpl(99,28): Error: Mismatch in key collection between source and target
+no-collect-keys.bpl(100,4): Error: Keys must be collected
+no-collect-keys.bpl(101,4): Error: Keys must be collected
+no-collect-keys.bpl(102,4): Error: Keys must not be collected
+no-collect-keys.bpl(103,4): Error: Keys must not be collected
+no-collect-keys.bpl(104,9): Error: Mismatch in key collection between source and target
+no-collect-keys.bpl(105,22): Error: Mismatch in key collection between source and target
+12 type checking errors detected in no-collect-keys.bpl