From 2e85a80ec246a7670f3130096938badc9bc05667 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 16 Nov 2023 15:46:58 -0800 Subject: [PATCH] relax linear type checking by allowing arbitrary expressions to be assigned to a linear variable but making the variable unavailable --- Source/Concurrency/LinearTypeChecker.cs | 36 ++++++++++--------- .../regression-tests/linear/typecheck.bpl | 2 -- .../linear/typecheck.bpl.expect | 27 +++++++------- 3 files changed, 32 insertions(+), 33 deletions(-) diff --git a/Source/Concurrency/LinearTypeChecker.cs b/Source/Concurrency/LinearTypeChecker.cs index dd7513ced..8e09da6e3 100644 --- a/Source/Concurrency/LinearTypeChecker.cs +++ b/Source/Concurrency/LinearTypeChecker.cs @@ -198,6 +198,7 @@ private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) { if (cmd is AssignCmd assignCmd) { + var lhsVarsToAdd = new HashSet(); for (int i = 0; i < assignCmd.Lhss.Count; i++) { var lhsVar = assignCmd.Lhss[i].DeepAssignedVariable; @@ -205,38 +206,43 @@ private HashSet PropagateAvailableLinearVarsAcrossBlock(Block b) { 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() + var args = nAryExpr.Args.Where(arg => linearTypes.Contains(arg.Type)).Cast() .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); } diff --git a/Test/civl/regression-tests/linear/typecheck.bpl b/Test/civl/regression-tests/linear/typecheck.bpl index dc8fc376c..e0b728223 100644 --- a/Test/civl/regression-tests/linear/typecheck.bpl +++ b/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; diff --git a/Test/civl/regression-tests/linear/typecheck.bpl.expect b/Test/civl/regression-tests/linear/typecheck.bpl.expect index a330c3010..15a7a7784 100644 --- a/Test/civl/regression-tests/linear/typecheck.bpl.expect +++ b/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