fixed pack rule when linear types are involved

boogie-org · Nov 15, 2023 · 5ae149f · 5ae149f
1 parent aa56ffb
commit 5ae149f
Show file tree

Hide file tree

Showing 5 changed files with 40 additions and 20 deletions.
diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs
@@ -87,12 +87,12 @@ private LinearDomainCollector(Program program, CheckingContext checkingContext)
       this.visitedTypes = new HashSet<Type>();
     }
 
-    public static (Dictionary<string, LinearDomain>, Dictionary<Type, LinearDomain>) Collect(Program program, CheckingContext checkingContext)
+    public static (Dictionary<string, LinearDomain>, Dictionary<Type, LinearDomain>, HashSet<Type>) Collect(Program program, CheckingContext checkingContext)
     {
       var collector = new LinearDomainCollector(program, checkingContext);
       collector.PopulateLinearDomains();
       collector.VisitProgram(program);
-      return (collector.linearDomains, collector.MakeLinearDomains());
+      return (collector.linearDomains, collector.MakeLinearDomains(), collector.linearTypes);
     }
 
     public static LinearKind FindLinearKind(Variable v)

diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs
@@ -11,6 +11,7 @@ public class LinearTypeChecker : ReadOnlyVisitor
     private CivlTypeChecker civlTypeChecker;
     private Dictionary<string, LinearDomain> domainNameToLinearDomain;
     private Dictionary<Type, LinearDomain> linearTypeToLinearDomain;
+    private HashSet<Type> linearTypes;
     private Dictionary<Absy, HashSet<Variable>> availableLinearVars;
 
     public LinearTypeChecker(CivlTypeChecker civlTypeChecker)
@@ -220,8 +221,8 @@ private HashSet<Variable> PropagateAvailableLinearVarsAcrossBlock(Block b)
             else
             {
               // pack
-              var args = ((NAryExpr)rhsExpr).Args.Cast<IdentifierExpr>().Select(arg => arg.Decl)
-                .Where(v => LinearDomainCollector.FindLinearKind(v) != LinearKind.ORDINARY);
+              var args = ((NAryExpr)rhsExpr).Args.Where(arg => linearTypes.Contains(arg.Type)).Cast<IdentifierExpr>()
+                .Select(arg => arg.Decl);
               if (args.Any(v => !start.Contains(v)))
               {
                 Error(rhsExpr, "unavailable source for a linear read");
@@ -487,23 +488,27 @@ public override Cmd VisitAssignCmd(AssignCmd node)
           }
           rhsVars.Add(rhs.Decl);
         }
-        else if (lhsDomainName == null && rhsExpr is NAryExpr nAryExpr && nAryExpr.Fun is FunctionCall functionCall && functionCall.Func is DatatypeConstructor)
+        else if (lhsDomainName == null && rhsExpr is NAryExpr { Fun: FunctionCall { Func: DatatypeConstructor } } nAryExpr)
         {
           // pack
-          var args = nAryExpr.Args.OfType<IdentifierExpr>();
-          if (args.Count() < nAryExpr.Args.Count)
+          nAryExpr.Args.ForEach(arg =>
           {
-            Error(node, $"A source of pack must be a variable");
-          }
-          else if (args.Any(arg => LinearDomainCollector.FindDomainName(arg.Decl) != null))
-          {
-            Error(node, $"A target of pack must not be a linear variable of name domain");
-          }
-          else
-          {
-            rhsVars.UnionWith(args.Select(arg => arg.Decl)
-              .Where(v => LinearDomainCollector.FindLinearKind(v) != LinearKind.ORDINARY));
-          }
+            if (linearTypes.Contains(arg.Type))
+            {
+              if (arg is IdentifierExpr ie)
+              {
+                rhsVars.Add(ie.Decl);
+              }
+              else
+              {
+                Error(node, $"A source of pack of linear type must be a variable");
+              }
+            }
+            else if (arg is IdentifierExpr ie && LinearDomainCollector.FindDomainName(ie.Decl) != null)
+            {
+              Error(node, $"A source of pack must not be a linear variable of name domain");
+            }
+          });
         }
         else
         {
@@ -718,7 +723,7 @@ public override Variable VisitVariable(Variable node)
 
     public void TypeCheck()
     {
-      (this.domainNameToLinearDomain, this.linearTypeToLinearDomain) = LinearDomainCollector.Collect(program, checkingContext);
+      (this.domainNameToLinearDomain, this.linearTypeToLinearDomain, this.linearTypes) = LinearDomainCollector.Collect(program, checkingContext);
       this.availableLinearVars = new Dictionary<Absy, HashSet<Variable>>();
       this.VisitProgram(program);
       foreach (var absy in this.availableLinearVars.Keys)

diff --git a/Test/civl/regression-tests/linear_types.bpl b/Test/civl/regression-tests/linear_types.bpl
@@ -75,3 +75,10 @@ atomic action {:layer 1, 2} A10({:linear_in} a: Foo) returns (b: Foo)
     Foo(x) := a;
     b := Foo(x);
 }
+
+datatype Bar { Bar(x: Lval int, y: int) }
+
+atomic action {:layer 1, 2} A11({:linear_in} a: Lval int) returns (b: Bar)
+{
+    b := Bar(a, 3+4);
+}
diff --git a/Test/civl/regression-tests/linear_types_error.bpl b/Test/civl/regression-tests/linear_types_error.bpl
@@ -77,3 +77,10 @@ atomic action {:layer 1, 2} A13({:linear_in} a: Foo) returns (b: Foo)
     var x: Lheap int;
     b := Foo(x);
 }
+
+datatype Bar { Bar(x: Lval int, y: int) }
+
+atomic action {:layer 1, 2} A14({:linear_in} a: Lval int) returns (b: Bar)
+{
+    b := Bar(Lval(3), 3+4);
+}
diff --git a/Test/civl/regression-tests/linear_types_error.bpl.expect b/Test/civl/regression-tests/linear_types_error.bpl.expect
@@ -13,4 +13,5 @@ linear_types_error.bpl(59,4): Error: Primitive assigns to input variable: l'
 linear_types_error.bpl(66,0): Error: Output variable b must be available at a return
 linear_types_error.bpl(72,14): Error: unavailable source for a linear read
 linear_types_error.bpl(78,9): Error: unavailable source for a linear read
-15 type checking errors detected in linear_types_error.bpl
+linear_types_error.bpl(85,6): Error: A source of pack of linear type must be a variable
+16 type checking errors detected in linear_types_error.bpl