From 5ae149f294726b7e4bc2dadce714327391f7a7eb Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Wed, 15 Nov 2023 05:55:42 -0800 Subject: [PATCH] fixed pack rule when linear types are involved --- Source/Concurrency/LinearDomainCollector.cs | 4 +- Source/Concurrency/LinearTypeChecker.cs | 39 +++++++++++-------- Test/civl/regression-tests/linear_types.bpl | 7 ++++ .../regression-tests/linear_types_error.bpl | 7 ++++ .../linear_types_error.bpl.expect | 3 +- 5 files changed, 40 insertions(+), 20 deletions(-) diff --git a/Source/Concurrency/LinearDomainCollector.cs b/Source/Concurrency/LinearDomainCollector.cs index 8a1341093..3543c3e69 100644 --- a/Source/Concurrency/LinearDomainCollector.cs +++ b/Source/Concurrency/LinearDomainCollector.cs @@ -87,12 +87,12 @@ private LinearDomainCollector(Program program, CheckingContext checkingContext) this.visitedTypes = new HashSet(); } - public static (Dictionary, Dictionary) Collect(Program program, CheckingContext checkingContext) + public static (Dictionary, Dictionary, HashSet) 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 index 44a233f26..fe6f0b340 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -11,6 +11,7 @@ public class LinearTypeChecker : ReadOnlyVisitor private CivlTypeChecker civlTypeChecker; private Dictionary domainNameToLinearDomain; private Dictionary linearTypeToLinearDomain; + private HashSet linearTypes; private Dictionary> availableLinearVars; public LinearTypeChecker(CivlTypeChecker civlTypeChecker) @@ -220,8 +221,8 @@ private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) else { // pack - var args = ((NAryExpr)rhsExpr).Args.Cast().Select(arg => arg.Decl) - .Where(v => LinearDomainCollector.FindLinearKind(v) != LinearKind.ORDINARY); + var args = ((NAryExpr)rhsExpr).Args.Where(arg => linearTypes.Contains(arg.Type)).Cast() + .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(); - 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>(); 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 index 4f9a12a9f..63cbc6cbe 100644 --- 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 index 030987556..24d214d3a 100644 --- 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 index e8e1d4825..bf9731aae 100644 --- 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