diff --git a/Source/Concurrency/NoninterferenceChecker.cs b/Source/Concurrency/NoninterferenceChecker.cs index 3d8557849..018ebbef6 100644 --- a/Source/Concurrency/NoninterferenceChecker.cs +++ b/Source/Concurrency/NoninterferenceChecker.cs @@ -14,14 +14,19 @@ public static string PermissionCollectorLocalName(LinearDomain domain) { return "linear_" + domain.DomainName + "_available"; } - - public static List CreateNoninterferenceCheckers( + + public static List CreateNoninterferenceCheckerDecls( CivlTypeChecker civlTypeChecker, int layerNum, AbsyMap absyMap, YieldInvariantDecl yieldInvariantDecl, List declLocalVariables) { + if (!yieldInvariantDecl.Requires.Any()) + { + return new List(); + } + var linearTypeChecker = civlTypeChecker.linearTypeChecker; var domainToHoleVar = new Dictionary(); Dictionary localVarMap = new Dictionary(); @@ -35,7 +40,8 @@ public static List CreateNoninterferenceCheckers( domainToHoleVar[domain] = inParam; } - foreach (Variable local in declLocalVariables.Union(yieldInvariantDecl.InParams).Union(yieldInvariantDecl.OutParams)) + foreach (Variable local in declLocalVariables.Union(yieldInvariantDecl.InParams) + .Union(yieldInvariantDecl.OutParams)) { var copy = CopyLocal(local); locals.Add(copy); @@ -43,13 +49,9 @@ public static List CreateNoninterferenceCheckers( map[local] = Expr.Ident(copy); } - Dictionary oldLocalMap = new Dictionary(); Dictionary assumeMap = new Dictionary(map); foreach (Variable g in civlTypeChecker.GlobalVariables) { - var copy = OldGlobalLocal(civlTypeChecker, g); - locals.Add(copy); - oldLocalMap[g] = Expr.Ident(copy); Formal f = SnapshotGlobalFormal(civlTypeChecker, g); inputs.Add(f); assumeMap[g] = Expr.Ident(f); @@ -57,64 +59,47 @@ public static List CreateNoninterferenceCheckers( var linearPermissionInstrumentation = new LinearPermissionInstrumentation(civlTypeChecker, layerNum, absyMap, domainToHoleVar, localVarMap); - var yieldInfos = new List(); var noninterferenceCheckerName = $"yield_{yieldInvariantDecl.Name}"; - if (yieldInvariantDecl.Requires.Count > 0) - { - var disjointnessCmds = linearPermissionInstrumentation.ProcDisjointnessAndWellFormedAssumeCmds(yieldInvariantDecl, true); - var yieldPredicates = yieldInvariantDecl.Requires.Select(requires => - requires.Free - ? (PredicateCmd)new AssumeCmd(requires.tok, requires.Condition) - : (PredicateCmd)new AssertCmd(requires.tok, requires.Condition)).ToList(); - yieldInfos.Add(new YieldInfo(disjointnessCmds, yieldPredicates)); - } - - var filteredYieldInfos = yieldInfos.Where(info => - info.invariantCmds.Any(predCmd => new GlobalAccessChecker().AccessesGlobal(predCmd.Expr))); - if (!filteredYieldInfos.Any()) - { - return new List(); - } + var disjointnessCmds = + linearPermissionInstrumentation.ProcDisjointnessAndWellFormedAssumeCmds(yieldInvariantDecl, true); + var invariantCmds = yieldInvariantDecl.Requires.Select(requires => + requires.Free + ? (PredicateCmd)new AssumeCmd(requires.tok, requires.Condition) + : (PredicateCmd)new AssertCmd(requires.tok, requires.Condition)).ToList(); Substitution assumeSubst = Substituter.SubstitutionFromDictionary(assumeMap); - Substitution oldSubst = Substituter.SubstitutionFromDictionary(oldLocalMap); Substitution subst = Substituter.SubstitutionFromDictionary(map); List noninterferenceCheckerBlocks = new List(); List labelTargets = new List(); Block noninterferenceCheckerBlock = BlockHelper.Block("exit", new List()); labelTargets.Add(noninterferenceCheckerBlock); noninterferenceCheckerBlocks.Add(noninterferenceCheckerBlock); - int yieldCount = 0; - foreach (var kv in filteredYieldInfos) - { - var newCmds = new List(kv.disjointnessCmds); - foreach (var predCmd in kv.invariantCmds) - { - var newExpr = Substituter.ApplyReplacingOldExprs(assumeSubst, oldSubst, predCmd.Expr); - newCmds.Add(new AssumeCmd(predCmd.tok, newExpr)); - } - foreach (var predCmd in kv.invariantCmds) + var newCmds = new List(disjointnessCmds); + foreach (var predCmd in invariantCmds) + { + var newExpr = Substituter.Apply(assumeSubst, predCmd.Expr); + newCmds.Add(new AssumeCmd(predCmd.tok, newExpr)); + } + foreach (var predCmd in invariantCmds) + { + if (predCmd is AssertCmd) { - if (predCmd is AssertCmd) - { - var newExpr = Substituter.ApplyReplacingOldExprs(subst, oldSubst, predCmd.Expr); - AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes); - assertCmd.Description = new FailureOnlyDescription("Non-interference check failed"); - newCmds.Add(assertCmd); - } + var newExpr = Substituter.Apply(subst, predCmd.Expr); + AssertCmd assertCmd = new AssertCmd(predCmd.tok, newExpr, predCmd.Attributes); + assertCmd.Description = new FailureOnlyDescription("Non-interference check failed"); + newCmds.Add(assertCmd); } - - newCmds.Add(CmdHelper.AssumeCmd(Expr.False)); - noninterferenceCheckerBlock = BlockHelper.Block("L" + yieldCount++, newCmds); - labelTargets.Add(noninterferenceCheckerBlock); - noninterferenceCheckerBlocks.Add(noninterferenceCheckerBlock); } - + newCmds.Add(CmdHelper.AssumeCmd(Expr.False)); + noninterferenceCheckerBlock = BlockHelper.Block("L", newCmds); + labelTargets.Add(noninterferenceCheckerBlock); + noninterferenceCheckerBlocks.Add(noninterferenceCheckerBlock); noninterferenceCheckerBlocks.Insert(0, BlockHelper.Block("enter", new List(), labelTargets)); // Create the yield checker procedure - noninterferenceCheckerName = civlTypeChecker.AddNamePrefix($"NoninterferenceChecker_{noninterferenceCheckerName}"); + noninterferenceCheckerName = + civlTypeChecker.AddNamePrefix($"NoninterferenceChecker_{noninterferenceCheckerName}"); var noninterferenceCheckerProc = DeclHelper.Procedure(noninterferenceCheckerName, inputs, new List(), new List(), new List(), new List()); CivlUtil.AddInlineAttribute(noninterferenceCheckerProc); @@ -122,7 +107,7 @@ public static List CreateNoninterferenceCheckers( // Create the yield checker implementation var noninterferenceCheckerImpl = DeclHelper.Implementation(noninterferenceCheckerProc, inputs, new List(), locals, noninterferenceCheckerBlocks); - return new List {noninterferenceCheckerProc, noninterferenceCheckerImpl}; + return new List { noninterferenceCheckerProc, noninterferenceCheckerImpl }; } private static LocalVariable CopyLocal(Variable v) @@ -139,58 +124,5 @@ private static Formal SnapshotGlobalFormal(CivlTypeChecker civlTypeChecker, Vari { return civlTypeChecker.Formal($"snapshot_{v.Name}", v.TypedIdent.Type, true); } - - private static LocalVariable OldGlobalLocal(CivlTypeChecker civlTypeChecker, Variable v) - { - return civlTypeChecker.LocalVariable($"old_{v.Name}", v.TypedIdent.Type); - } - } - - class YieldInfo - { - public List disjointnessCmds; - public List invariantCmds; - - public YieldInfo(List disjointnessCmds, List invariantCmds) - { - this.disjointnessCmds = disjointnessCmds; - this.invariantCmds = invariantCmds; - } - } - - class GlobalAccessChecker : ReadOnlyVisitor - { - private bool accessesGlobal; - private int insideOldExpr; - - public GlobalAccessChecker() - { - this.accessesGlobal = false; - this.insideOldExpr = 0; - } - - public bool AccessesGlobal(Expr expr) - { - Visit(expr); - return accessesGlobal; - } - - public override Expr VisitOldExpr(OldExpr node) - { - insideOldExpr++; - base.VisitOldExpr(node); - insideOldExpr--; - return node; - } - - public override Expr VisitIdentifierExpr(IdentifierExpr node) - { - if (node.Decl is GlobalVariable && insideOldExpr == 0) - { - accessesGlobal = true; - } - - return node; - } } } \ No newline at end of file diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 0594653d7..61501af81 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -203,7 +203,7 @@ private void AddNoninterferenceCheckers() if (layerNum == yieldInvariant.Layer) { noninterferenceCheckerDecls.AddRange( - NoninterferenceChecker.CreateNoninterferenceCheckers(civlTypeChecker, + NoninterferenceChecker.CreateNoninterferenceCheckerDecls(civlTypeChecker, layerNum, absyMap, yieldInvariant, new List())); } } diff --git a/Test/civl/regression-tests/non-interference-1.bpl.expect b/Test/civl/regression-tests/non-interference-1.bpl.expect index 28836da61..9ed2f19b1 100644 --- a/Test/civl/regression-tests/non-interference-1.bpl.expect +++ b/Test/civl/regression-tests/non-interference-1.bpl.expect @@ -2,6 +2,6 @@ non-interference-1.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-1.bpl(7,3): anon0 non-interference-1.bpl(12,5): inline$AtomicIncr$0$anon0 - (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/regression-tests/non-interference-2.bpl.expect b/Test/civl/regression-tests/non-interference-2.bpl.expect index a73fbf6eb..c1176c36d 100644 --- a/Test/civl/regression-tests/non-interference-2.bpl.expect +++ b/Test/civl/regression-tests/non-interference-2.bpl.expect @@ -2,10 +2,10 @@ non-interference-2.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-2.bpl(7,3): anon0 non-interference-2.bpl(12,5): inline$AtomicIncr$0$anon0 - (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L0 + (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L non-interference-2.bpl(25,1): Error: Non-interference check failed Execution trace: non-interference-2.bpl(34,3): anon0 - (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L0 + (0,0): inline$Civl_NoninterferenceChecker_yield_PC$0$L Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/civl/regression-tests/parallel1.bpl.expect b/Test/civl/regression-tests/parallel1.bpl.expect index 94258cd36..4b52e2854 100644 --- a/Test/civl/regression-tests/parallel1.bpl.expect +++ b/Test/civl/regression-tests/parallel1.bpl.expect @@ -2,6 +2,6 @@ parallel1.bpl(25,1): Error: Non-interference check failed Execution trace: parallel1.bpl(7,3): anon0 parallel1.bpl(12,5): inline$AtomicIncr$0$anon0 - (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Yield$0$L Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/civl/regression-tests/perm4.bpl.expect b/Test/civl/regression-tests/perm4.bpl.expect index 8beed4435..1b9cf6ab2 100644 --- a/Test/civl/regression-tests/perm4.bpl.expect +++ b/Test/civl/regression-tests/perm4.bpl.expect @@ -1,6 +1,6 @@ perm4.bpl(87,1): Error: Non-interference check failed Execution trace: perm4.bpl(68,13): anon0 - (0,0): inline$Civl_NoninterferenceChecker_yield_Yield_g$0$L0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Yield_g$0$L Boogie program verifier finished with 4 verified, 1 error diff --git a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect index 5e4908a82..093836a59 100644 --- a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect +++ b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect @@ -2,6 +2,6 @@ yield-invariant-fails.bpl(7,1): Error: Non-interference check failed Execution trace: yield-invariant-fails.bpl(11,5): anon0 yield-invariant-fails.bpl(19,7): inline$atomic_A$0$anon0 - (0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L0 + (0,0): inline$Civl_NoninterferenceChecker_yield_Inv$0$L Boogie program verifier finished with 0 verified, 1 error