fixed error messages

Author: shazqadeer

Source/Concurrency/LinearTypeChecker.cs

@@ -11,6 +11,7 @@ public class LinearTypeChecker : ReadOnlyVisitor
 
     public Program program;
     private CheckingContext checkingContext;
+    private HashSet<(Absy, string)> errors;
     private CivlTypeChecker civlTypeChecker;
     private Dictionary<Type, ActionDecl> pendingAsyncTypeToActionDecl;
     private Dictionary<Type, LinearDomain> permissionTypeToLinearDomain;
@@ -22,6 +23,7 @@ public LinearTypeChecker(CivlTypeChecker civlTypeChecker)
       this.civlTypeChecker = civlTypeChecker;
       this.program = civlTypeChecker.program;
       this.checkingContext = civlTypeChecker.checkingContext;
+      this.errors = new ();
       this.pendingAsyncTypeToActionDecl = new ();
       foreach (var actionDecl in program.TopLevelDeclarations.OfType<ActionDecl>().Where(actionDecl => actionDecl.MaybePendingAsync))
       {
@@ -39,6 +41,11 @@ public LinearTypeChecker(CivlTypeChecker civlTypeChecker)
 
     private void Error(Absy node, string message)
     {
+      if (errors.Contains((node, message)))
+      {
+        return;
+      }
+      errors.Add((node, message));
       checkingContext.Error(node, message);
     }
 
@@ -125,15 +132,13 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
             {
               continue;
             }
-            // assignment may violate the disjointness invariant
-            // therefore, drop lhsVar from the set of available variables
-            // but possibly add it to lhsVarsToAdd (added to start later)
             var lhsVar = lhs.DeepAssignedVariable;
-            start.Remove(lhsVar);
             var rhsExpr = assignCmd.Rhss[i];
             if (rhsExpr is IdentifierExpr ie)
             {
-              if (start.Contains(ie.Decl))
+              var rhsIsAvailable = start.Contains(ie.Decl);
+              start.Remove(lhsVar);
+              if (rhsIsAvailable)
               {
                 start.Remove(ie.Decl);
                 lhsVarsToAdd.Add(lhsVar);
@@ -143,38 +148,32 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
                       !IsPrimitiveLinearType(rhsExpr.Type))
             {
               // pack
-              bool addLhsVar = true;
-              for (int j = 0; j < constructor.InParams.Count; j++)
-              {
-                var field = constructor.InParams[j];
-                if (IsOrdinaryType(field.TypedIdent.Type))
-                {
-                  continue;
-                }
-                var arg = (IdentifierExpr)nAryExpr.Args[j];
-                if (start.Contains(arg.Decl))
-                {
-                  start.Remove(arg.Decl);
-                }
-                else
-                {
-                  addLhsVar = false;
-                }
-              }
-              if (addLhsVar)
+              var linearArgs = constructor.InParams.Zip(nAryExpr.Args)
+                                .Where(x => !IsOrdinaryType(x.First.TypedIdent.Type))
+                                .Select(x => x.Second).OfType<IdentifierExpr>();
+              bool rhsIsAvailable = linearArgs.All(ie => start.Contains(ie.Decl));
+              start.Remove(lhsVar);
+              if (rhsIsAvailable)
               {
+                linearArgs.ForEach(ie => { start.Remove(ie.Decl); });
                 lhsVarsToAdd.Add(lhsVar);
               }
             }
+            else
+            {
+              start.Remove(lhsVar);
+            }
           }
           start.UnionWith(lhsVarsToAdd);
         }
         else if (cmd is UnpackCmd unpackCmd)
         {
           if (!IsOrdinaryType(unpackCmd.Rhs.Type))
           {
-            var ie = unpackCmd.Rhs as IdentifierExpr;
-            if (start.Contains(ie.Decl))
+            var ie = (IdentifierExpr)unpackCmd.Rhs;
+            var rhsIsAvailable = start.Contains(ie.Decl);
+            unpackCmd.UnpackedLhs.ForEach(arg => start.Remove(arg.Decl));
+            if (rhsIsAvailable)
             {
               start.Remove(ie.Decl);
               unpackCmd.UnpackedLhs
@@ -217,7 +216,7 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
             }
             else
             {
-              Error(ie, $"unavailable source {ie} for linear parameter at position {i}");
+              Error(callCmd, $"unavailable source {ie} for linear parameter at position {i}");
             }
           }
           var originalProc = (Procedure)Monomorphizer.GetOriginalDecl(callCmd.Proc);
@@ -273,7 +272,7 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
                 }
                 else
                 {
-                  Error(ie, $"unavailable source {ie} for linear parameter at position {i}");
+                  Error(parCallCallCmd, $"unavailable source {ie} for linear parameter at position {i}");
                 }
               }
             }
@@ -727,15 +726,17 @@ public static LinearKind FindLinearKind(Variable v)
     public int CheckLinearParameters(CallCmd callCmd, HashSet<Variable> availableLinearVarsAtCallCmd)
     {
       int errorCount = 0;
-      foreach (var (ie, formal) in callCmd.Ins.Zip(callCmd.Proc.InParams))
+      for (int i = 0; i < callCmd.Ins.Count; i++)
       {
+        var ie = callCmd.Ins[i];
+        var formal = callCmd.Proc.InParams[i];
         if (FindLinearKind(formal) == LinearKind.ORDINARY)
         {
           continue;
         }
         if (ie is IdentifierExpr actual && !availableLinearVarsAtCallCmd.Contains(actual.Decl))
         {
-          Error(actual, "argument must be available");
+          Error(callCmd, $"unavailable source {ie} for linear parameter at position {i}");
           errorCount++;
         }
       }

Test/civl/regression-tests/linear/async-bug.bpl.expect

@@ -1,3 +1,3 @@
-async-bug.bpl(18,15): Error: unavailable source tid for linear parameter at position 0
+async-bug.bpl(18,4): Error: unavailable source tid for linear parameter at position 0
 async-bug.bpl(19,0): Error: input variable tid must be available at a return
 2 type checking errors detected in async-bug.bpl

Test/civl/regression-tests/yield-requires-ensures-errors-3.bpl.expect

@@ -1,2 +1,2 @@
-yield-requires-ensures-errors-3.bpl(10,29): Error: argument must be available
+yield-requires-ensures-errors-3.bpl(10,9): Error: unavailable source a for linear parameter at position 0
 1 type checking errors detected in yield-requires-ensures-errors-3.bpl

Test/civl/regression-tests/yield-requires-ensures-errors-4.bpl.expect

@@ -1,4 +1,4 @@
-yield-requires-ensures-errors-4.bpl(15,29): Error: argument must be available
-yield-requires-ensures-errors-4.bpl(16,28): Error: argument must be available
-yield-requires-ensures-errors-4.bpl(17,30): Error: argument must be available
+yield-requires-ensures-errors-4.bpl(15,9): Error: unavailable source c for linear parameter at position 0
+yield-requires-ensures-errors-4.bpl(16,8): Error: unavailable source b for linear parameter at position 0
+yield-requires-ensures-errors-4.bpl(17,10): Error: unavailable source c for linear parameter at position 0
 3 type checking errors detected in yield-requires-ensures-errors-4.bpl