[Civl] relax linear type checking

Source/Concurrency/LinearTypeChecker.cs

@@ -198,45 +198,51 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
       {
         if (cmd is AssignCmd assignCmd)
         {
+          var lhsVarsToAdd = new HashSet<Variable>();
           for (int i = 0; i < assignCmd.Lhss.Count; i++)
           {
             var lhsVar = assignCmd.Lhss[i].DeepAssignedVariable;
             if (SkipCheck(lhsVar))
             {
               continue;
             }
-            var rhsExpr = assignCmd.Rhss[i];
             var lhsDomainName = LinearDomainCollector.FindDomainName(lhsVar);
+            var rhsExpr = assignCmd.Rhss[i];
             if (rhsExpr is IdentifierExpr ie)
             {
-              if (!start.Contains(ie.Decl))
+              if (start.Contains(ie.Decl))
               {
-                Error(ie, "unavailable source for a linear read");
+                start.Remove(ie.Decl);
               }
               else
               {
-                start.Remove(ie.Decl);
+                Error(ie, "unavailable source for a linear read");
               }
+              lhsVarsToAdd.Add(lhsVar); // add always to prevent cascading error messages
             }
-            else
+            else if (lhsDomainName == null && rhsExpr is NAryExpr { Fun: FunctionCall { Func: DatatypeConstructor } } nAryExpr)
             {
               // pack
-              var args = ((NAryExpr)rhsExpr).Args.Where(arg => linearTypes.Contains(arg.Type)).Cast<IdentifierExpr>()
+              var args = nAryExpr.Args.Where(arg => linearTypes.Contains(arg.Type)).Cast<IdentifierExpr>()
                 .Select(arg => arg.Decl);
-              if (args.Any(v => !start.Contains(v)))
+              if (args.All(v => start.Contains(v)))
               {
-                Error(rhsExpr, "unavailable source for a linear read");
+                start.ExceptWith(args);
               }
               else
               {
-                start.ExceptWith(args);
+                Error(rhsExpr, "unavailable source for a linear read");
               }
+              lhsVarsToAdd.Add(lhsVar); // add always to prevent cascading error messages
+            }
+            else
+            {
+              // assignment may violate the disjointness invariant
+              // therefore, drop lhsVar from the set of available variables
+              start.Remove(lhsVar);
             }
           }
-          assignCmd.Lhss
-            .Where(assignLhs =>
-              LinearDomainCollector.FindLinearKind(assignLhs.DeepAssignedVariable) != LinearKind.ORDINARY)
-            .ForEach(assignLhs => start.Add(assignLhs.DeepAssignedVariable));
+          start.UnionWith(lhsVarsToAdd);
         }
         else if (cmd is UnpackCmd unpackCmd)
         {
@@ -503,10 +509,6 @@ public override Cmd VisitAssignCmd(AssignCmd node)
             }
           });
         }
-        else
-        {
-          Error(node, $"Only variable can be assigned to linear variable {lhsVar.Name}");
-        }
       }
       return base.VisitAssignCmd(node);
     }

Test/civl/regression-tests/linear/typecheck.bpl

@@ -34,8 +34,6 @@ yield procedure {:layer 1} D()
 
     b[a] := true;
 
-    a := f(a);
-
     a := c;
 
     c := a;

Test/civl/regression-tests/linear/typecheck.bpl.expect

@@ -1,15 +1,14 @@
 typecheck.bpl(35,9): Error: Only simple assignment allowed on linear variable b
-typecheck.bpl(37,6): Error: Only variable can be assigned to linear variable a
-typecheck.bpl(39,6): Error: Only linear variable can be assigned to linear variable a
-typecheck.bpl(43,6): Error: The domains of source and target of assignment must be the same
-typecheck.bpl(49,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment
-typecheck.bpl(53,4): Error: Linear variable a can occur only once as an input parameter
-typecheck.bpl(55,4): Error: Only variable can be passed to linear parameter: f(a)
-typecheck.bpl(57,4): Error: The domains of parameter b and argument d must be the same
-typecheck.bpl(59,4): Error: The domains of formal and actual parameters must be the same
-typecheck.bpl(61,4): Error: Only linear variable can be passed to linear parameter: c
-typecheck.bpl(69,0): Error: Output variable d must be available at a return
-typecheck.bpl(78,0): Error: Global variable g must be available at a return
-typecheck.bpl(83,7): Error: unavailable source for a linear read
-typecheck.bpl(84,0): Error: Output variable r must be available at a return
-14 type checking errors detected in typecheck.bpl
+typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a
+typecheck.bpl(41,6): Error: The domains of source and target of assignment must be the same
+typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment
+typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter
+typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter: f(a)
+typecheck.bpl(55,4): Error: The domains of parameter b and argument d must be the same
+typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same
+typecheck.bpl(59,4): Error: Only linear variable can be passed to linear parameter: c
+typecheck.bpl(67,0): Error: Output variable d must be available at a return
+typecheck.bpl(76,0): Error: Global variable g must be available at a return
+typecheck.bpl(81,7): Error: unavailable source for a linear read
+typecheck.bpl(82,0): Error: Output variable r must be available at a return
+13 type checking errors detected in typecheck.bpl