From 7eddc91246319f928a26a9705117d67633f2ff4d Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 2 Jan 2020 19:51:15 -0800 Subject: [PATCH] clean up of refinement checking --- .../Concurrency/RefinementInstrumentation.cs | 336 ++++++++---------- .../YieldingProcInstrumentation.cs | 207 ++++++----- Test/civl/bar.bpl.expect | 4 - Test/civl/foo.bpl.expect | 2 - Test/civl/lock2.bpl | 4 +- Test/civl/parallel1.bpl.expect | 2 - Test/civl/refinement.bpl.expect | 10 +- Test/civl/t1.bpl.expect | 1 - Test/civl/wsq.bpl | 64 ++-- 9 files changed, 284 insertions(+), 346 deletions(-) diff --git a/Source/Concurrency/RefinementInstrumentation.cs b/Source/Concurrency/RefinementInstrumentation.cs index 55949102c..4e5a49dac 100644 --- a/Source/Concurrency/RefinementInstrumentation.cs +++ b/Source/Concurrency/RefinementInstrumentation.cs @@ -3,105 +3,116 @@ namespace Microsoft.Boogie { - interface RefinementInstrumentation + class RefinementInstrumentation { - List NewLocalVars { get; } - List CreateAssumeCmds(); - List CreateFinalAssertCmds(); - List CreateAssertCmds(); - List CreateUpdateCmds(); - List CreateUpdatesToOldOutputVars(); - List CreateInitCmds(); - List CreateYieldingLoopHeaderInitCmds(Block header); - List CreateYieldingLoopHeaderAssertCmds(Block header); - } - - class NoneRefinementInstrumentation : RefinementInstrumentation - { - public List NewLocalVars => new List(); + public virtual List NewLocalVars => new List(); - public List CreateAssumeCmds() + public virtual List CreateInitCmds() { return new List(); } - public List CreateFinalAssertCmds() + public virtual List CreateAssumeCmds() { return new List(); } - public List CreateAssertCmds() + public virtual List CreateAssertCmds() { return new List(); } - public List CreateUpdateCmds() + public virtual List CreateReturnAssertCmds() { return new List(); } - public List CreateUpdatesToOldOutputVars() + public virtual List CreateUnchangedGlobalsAssertCmds() { return new List(); } - public List CreateInitCmds() + public virtual List CreateUnchangedOutputsAssertCmds() { return new List(); } - public List CreateYieldingLoopHeaderInitCmds(Block header) + public virtual List CreateUpdatesToRefinementVars() { return new List(); } - public List CreateYieldingLoopHeaderAssertCmds(Block header) + public virtual List CreateUpdatesToOldOutputVars() { return new List(); } } - - class SomeRefinementInstrumentation : RefinementInstrumentation + + class SkipRefinementInstrumentation : RefinementInstrumentation + { + protected Dictionary oldGlobalMap; + + public SkipRefinementInstrumentation( + CivlTypeChecker civlTypeChecker, + YieldingProc yieldingProc, + Dictionary oldGlobalMap) + { + this.oldGlobalMap = new Dictionary(); + foreach (Variable v in civlTypeChecker.sharedVariables) + { + var layerRange = civlTypeChecker.GlobalVariableLayerRange(v); + if (layerRange.lowerLayerNum <= yieldingProc.upperLayer && yieldingProc.upperLayer < layerRange.upperLayerNum) + { + this.oldGlobalMap[v] = oldGlobalMap[v]; + } + } + } + + public override List CreateAssertCmds() + { + return CreateUnchangedGlobalsAssertCmds(); + } + + public override List CreateUnchangedGlobalsAssertCmds() + { + var cmds = new List(); + var assertExpr = Expr.And(this.oldGlobalMap.Select(kvPair => Expr.Eq(Expr.Ident(kvPair.Key), Expr.Ident(kvPair.Value)))); + assertExpr.Typecheck(new TypecheckingContext(null)); + AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr); + skipAssertCmd.ErrorData = "Globals must not be modified"; + cmds.Add(skipAssertCmd); + return cmds; + } + } + + class ActionRefinementInstrumentation : SkipRefinementInstrumentation { - private Dictionary oldGlobalMap; private Dictionary oldOutputMap; private List newLocalVars; private Variable pc; private Variable ok; private Expr alpha; private Expr beta; - private Dictionary pcsForYieldingLoopsHeaders; - private Dictionary oksForYieldingLoopHeaders; private Dictionary transitionRelationCache; - public SomeRefinementInstrumentation( + public ActionRefinementInstrumentation( CivlTypeChecker civlTypeChecker, Implementation impl, Implementation originalImpl, - Dictionary oldGlobalMap, - HashSet yieldingLoopHeaders) + Dictionary oldGlobalMap): + base (civlTypeChecker, civlTypeChecker.procToYieldingProc[originalImpl.Proc] as ActionProc, oldGlobalMap) { newLocalVars = new List(); - YieldingProc yieldingProc = civlTypeChecker.procToYieldingProc[originalImpl.Proc]; - int layerNum = yieldingProc.upperLayer; - pc = Pc(); + ActionProc actionProc = civlTypeChecker.procToYieldingProc[originalImpl.Proc] as ActionProc; + int layerNum = actionProc.upperLayer; + pc = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); newLocalVars.Add(pc); - ok = Ok(); + ok = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool)); newLocalVars.Add(ok); this.transitionRelationCache = new Dictionary(); - this.oldGlobalMap = new Dictionary(); - foreach (Variable v in civlTypeChecker.sharedVariables) - { - var layerRange = civlTypeChecker.GlobalVariableLayerRange(v); - if (layerRange.lowerLayerNum <= yieldingProc.upperLayer && yieldingProc.upperLayer < layerRange.upperLayerNum) - { - this.oldGlobalMap[v] = oldGlobalMap[v]; - } - } - oldOutputMap = new Dictionary(); foreach (Variable f in impl.OutParams) { @@ -115,73 +126,57 @@ public SomeRefinementInstrumentation( { foroldMap[g] = Expr.Ident(oldGlobalMap[g]); } - if (yieldingProc is ActionProc actionProc) - { - // The parameters of an atomic action come from the implementation that denotes the atomic action specification. - // To use the transition relation computed below in the context of the yielding procedure of the refinement check, - // we need to substitute the parameters. - AtomicAction atomicAction = actionProc.refinedAction; - Implementation atomicActionImpl = atomicAction.impl; - Dictionary alwaysMap = new Dictionary(); - for (int i = 0; i < impl.InParams.Count; i++) - { - alwaysMap[atomicActionImpl.InParams[i]] = Expr.Ident(impl.InParams[i]); - } - - for (int i = 0; i < impl.OutParams.Count; i++) - { - alwaysMap[atomicActionImpl.OutParams[i]] = Expr.Ident(impl.OutParams[i]); - } - if (atomicAction.HasPendingAsyncs) - { - Variable collectedPAs = civlTypeChecker.implToPendingAsyncCollector[originalImpl]; - alwaysMap[atomicActionImpl.OutParams.Last()] = Expr.Ident(collectedPAs); - LocalVariable copy = Old(collectedPAs); - newLocalVars.Add(copy); - oldOutputMap[collectedPAs] = copy; - } - Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap); - Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); - Expr betaExpr = GetTransitionRelation(atomicAction); - beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); - Expr alphaExpr = Expr.And(atomicAction.gate.Select(g => g.Expr)); - alphaExpr.Type = Type.Bool; - alpha = Substituter.Apply(always, alphaExpr); - } - else + // The parameters of an atomic action come from the implementation that denotes the atomic action specification. + // To use the transition relation computed below in the context of the yielding procedure of the refinement check, + // we need to substitute the parameters. + AtomicAction atomicAction = actionProc.refinedAction; + Implementation atomicActionImpl = atomicAction.impl; + Dictionary alwaysMap = new Dictionary(); + for (int i = 0; i < impl.InParams.Count; i++) { - beta = OldEqualityExprForGlobals(); - alpha = Expr.True; + alwaysMap[atomicActionImpl.InParams[i]] = Expr.Ident(impl.InParams[i]); } - pcsForYieldingLoopsHeaders = new Dictionary(); - oksForYieldingLoopHeaders = new Dictionary(); - foreach (Block header in yieldingLoopHeaders) + for (int i = 0; i < impl.OutParams.Count; i++) { - var pcForYieldingLoopHeader = PcForYieldingLoopHeader(header); - newLocalVars.Add(pcForYieldingLoopHeader); - pcsForYieldingLoopsHeaders[header] = pcForYieldingLoopHeader; - var okForYieldingLoopHeader = OkForYieldingLoopHeader(header); - newLocalVars.Add(okForYieldingLoopHeader); - oksForYieldingLoopHeaders[header] = okForYieldingLoopHeader; + alwaysMap[atomicActionImpl.OutParams[i]] = Expr.Ident(impl.OutParams[i]); } - } - - private Expr GetTransitionRelation(AtomicAction atomicAction) - { - if (!transitionRelationCache.ContainsKey(atomicAction)) + if (atomicAction.HasPendingAsyncs) { - transitionRelationCache[atomicAction] = - TransitionRelationComputation. - Refinement(atomicAction, new HashSet(this.oldGlobalMap.Keys)); + Variable collectedPAs = civlTypeChecker.implToPendingAsyncCollector[originalImpl]; + alwaysMap[atomicActionImpl.OutParams.Last()] = Expr.Ident(collectedPAs); + LocalVariable copy = Old(collectedPAs); + newLocalVars.Add(copy); + oldOutputMap[collectedPAs] = copy; } - return transitionRelationCache[atomicAction]; + + Substitution always = Substituter.SubstitutionFromHashtable(alwaysMap); + Substitution forold = Substituter.SubstitutionFromHashtable(foroldMap); + Expr betaExpr = GetTransitionRelation(atomicAction); + beta = Substituter.ApplyReplacingOldExprs(always, forold, betaExpr); + Expr alphaExpr = Expr.And(atomicAction.gate.Select(g => g.Expr)); + alphaExpr.Type = Type.Bool; + alpha = Substituter.Apply(always, alphaExpr); } - public List NewLocalVars => newLocalVars; + public override List NewLocalVars => newLocalVars; + + public override List CreateInitCmds() + { + var cmds = new List(); + List lhss = new List(); + List rhss = new List(); + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); + rhss.Add(Expr.False); + lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); + rhss.Add(Expr.False); + cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); + cmds.AddRange(CreateUpdatesToOldOutputVars()); + return cmds; + } - public List CreateAssumeCmds() + public override List CreateAssumeCmds() { var cmds = new List(); // assume pc || alpha(i, g); @@ -191,40 +186,52 @@ public List CreateAssumeCmds() return cmds; } - public List CreateFinalAssertCmds() + public override List CreateAssertCmds() { - var cmds = CreateAssertCmds(); - AssertCmd assertCmd = new AssertCmd(Token.NoToken, Expr.Ident(ok)); - assertCmd.ErrorData = "Failed to execute atomic action before procedure return"; - cmds.Add(assertCmd); + Expr assertExpr; + var cmds = new List(); + + // assert pc || g_old == g || beta(i, g_old, o, g); + assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(OldEqualityExprForGlobals(), beta)); + assertExpr.Typecheck(new TypecheckingContext(null)); + var skipOrBetaAssertCmd = new AssertCmd(Token.NoToken, assertExpr); + skipOrBetaAssertCmd.ErrorData = "Transition invariant violated in initial state"; + cmds.Add(skipOrBetaAssertCmd); + + // assert pc ==> o_old == o && g_old == g; + assertExpr = Expr.Imp(Expr.Ident(pc), OldEqualityExpr()); + assertExpr.Typecheck(new TypecheckingContext(null)); + AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr); + skipAssertCmd.ErrorData = "Transition invariant violated in final state"; + cmds.Add(skipAssertCmd); return cmds; } - public List CreateAssertCmds() + public override List CreateReturnAssertCmds() { - var cmds = new List(); - cmds.Add(CreateSkipOrBetaAssertCmd()); - cmds.Add(CreateSkipAssertCmd()); + var cmds = CreateUnchangedOutputsAssertCmds(); + AssertCmd assertCmd = new AssertCmd(Token.NoToken, Expr.Ident(ok)); + assertCmd.ErrorData = "Failed to execute atomic action before procedure return"; + cmds.Add(assertCmd); return cmds; } - public List CreateInitCmds() + public override List CreateUnchangedOutputsAssertCmds() { + // assert pc ==> o_old == o; var cmds = new List(); - List lhss = new List(); - List rhss = new List(); - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(pc))); - rhss.Add(Expr.False); - lhss.Add(new SimpleAssignLhs(Token.NoToken, Expr.Ident(ok))); - rhss.Add(Expr.False); - cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss)); - cmds.AddRange(CreateUpdatesToOldOutputVars()); + Expr bb = OldEqualityExprForOutputs(); + var assertExpr = Expr.Imp(Expr.Ident(pc), bb); + assertExpr.Typecheck(new TypecheckingContext(null)); + AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr); + skipAssertCmd.ErrorData = "Outputs must not be modified"; + cmds.Add(skipAssertCmd); return cmds; } - - public List CreateUpdateCmds() + + public override List CreateUpdatesToRefinementVars() { - // pc, ok := g_old == g ==> pc, ok || beta(i, g_old, o, g); + // pc, ok := g_old == g ==> pc, beta(i, g_old, o, g) || o_old == o && ok; Expr aa = OldEqualityExprForGlobals(); List pcUpdateLHS = new List { @@ -235,7 +242,7 @@ public List CreateUpdateCmds() new Expr[] { Expr.Imp(aa, Expr.Ident(pc)), - Expr.Or(Expr.Ident(ok), beta) + Expr.Or(beta, Expr.And(OldEqualityExprForOutputs(), Expr.Ident(ok))), }); foreach (Expr e in pcUpdateRHS) { @@ -244,7 +251,7 @@ public List CreateUpdateCmds() return new List {new AssignCmd(Token.NoToken, pcUpdateLHS, pcUpdateRHS)}; } - public List CreateUpdatesToOldOutputVars() + public override List CreateUpdatesToOldOutputVars() { List lhss = new List(); List rhss = new List(); @@ -261,56 +268,15 @@ public List CreateUpdatesToOldOutputVars() return cmds; } - public List CreateYieldingLoopHeaderInitCmds(Block header) - { - var newCmds = new List(); - var pcForYieldingLoopHeader = pcsForYieldingLoopsHeaders[header]; - var okForYieldingLoopHeader = oksForYieldingLoopHeaders[header]; - var assignCmd = new AssignCmd(Token.NoToken, - new List - { - new SimpleAssignLhs(Token.NoToken, Expr.Ident(pcForYieldingLoopHeader)), - new SimpleAssignLhs(Token.NoToken, Expr.Ident(okForYieldingLoopHeader)) - }, - new List {Expr.Ident(pc), Expr.Ident(ok)}); - newCmds.Add(assignCmd); - return newCmds; - } - - public List CreateYieldingLoopHeaderAssertCmds(Block header) - { - var newCmds = new List(); - var pcForYieldingLoopHeader = pcsForYieldingLoopsHeaders[header]; - var pcAssertCmd = new AssertCmd(header.tok, Expr.Eq(Expr.Ident(pcForYieldingLoopHeader), Expr.Ident(pc))); - pcAssertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers"; - newCmds.Add(pcAssertCmd); - var okForYieldingLoopHeader = oksForYieldingLoopHeaders[header]; - var okAssertCmd = new AssertCmd(header.tok, Expr.Imp(Expr.Ident(okForYieldingLoopHeader), Expr.Ident(ok))); - okAssertCmd.ErrorData = "Specification state must not change for transitions ending in loop headers"; - newCmds.Add(okAssertCmd); - return newCmds; - } - - private AssertCmd CreateSkipOrBetaAssertCmd() - { - // assert pc || g_old == g || beta(i, g_old, o, g); - var aa = OldEqualityExprForGlobals(); - var assertExpr = Expr.Or(Expr.Ident(pc), Expr.Or(aa, beta)); - assertExpr.Typecheck(new TypecheckingContext(null)); - var skipOrBetaAssertCmd = new AssertCmd(Token.NoToken, assertExpr); - skipOrBetaAssertCmd.ErrorData = "Transition invariant violated in initial state"; - return skipOrBetaAssertCmd; - } - - private AssertCmd CreateSkipAssertCmd() + private Expr GetTransitionRelation(AtomicAction atomicAction) { - // assert pc ==> o_old == o && g_old == g; - Expr bb = OldEqualityExpr(); - var assertExpr = Expr.Imp(Expr.Ident(pc), bb); - assertExpr.Typecheck(new TypecheckingContext(null)); - AssertCmd skipAssertCmd = new AssertCmd(Token.NoToken, assertExpr); - skipAssertCmd.ErrorData = "Transition invariant violated in final state"; - return skipAssertCmd; + if (!transitionRelationCache.ContainsKey(atomicAction)) + { + transitionRelationCache[atomicAction] = + TransitionRelationComputation. + Refinement(atomicAction, new HashSet(this.oldGlobalMap.Keys)); + } + return transitionRelationCache[atomicAction]; } private Expr OldEqualityExpr() @@ -332,28 +298,6 @@ private LocalVariable Old(Variable v) { return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, $"og_old_{v.Name}", v.TypedIdent.Type)); - } - - private LocalVariable Pc() - { - return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_pc", Type.Bool)); - } - - private LocalVariable Ok() - { - return new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "og_ok", Type.Bool)); - } - - private LocalVariable PcForYieldingLoopHeader(Block header) - { - return new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, $"og_pc_{header.Label}", Type.Bool)); - } - - private LocalVariable OkForYieldingLoopHeader(Block header) - { - return new LocalVariable(Token.NoToken, - new TypedIdent(Token.NoToken, $"og_ok_{header.Label}", Type.Bool)); - } + } } } diff --git a/Source/Concurrency/YieldingProcInstrumentation.cs b/Source/Concurrency/YieldingProcInstrumentation.cs index 8aa78dd46..105c5ccee 100644 --- a/Source/Concurrency/YieldingProcInstrumentation.cs +++ b/Source/Concurrency/YieldingProcInstrumentation.cs @@ -145,9 +145,6 @@ private Formal OldGlobalFormal(Variable v) private void TransformImpl(Implementation impl) { - HashSet yieldingLoopHeaders; - Graph graph = ComputeYieldingLoopHeaders(impl, out yieldingLoopHeaders); - // initialize globalSnapshotInstrumentation globalSnapshotInstrumentation = new GlobalSnapshotInstrumentation(civlTypeChecker); @@ -156,16 +153,25 @@ private void TransformImpl(Implementation impl) YieldingProc yieldingProc = civlTypeChecker.procToYieldingProc[originalImpl.Proc]; if (yieldingProc.upperLayer == this.layerNum) { - refinementInstrumentation = new SomeRefinementInstrumentation( - civlTypeChecker, - impl, - originalImpl, - globalSnapshotInstrumentation.OldGlobalMap, - yieldingLoopHeaders); + if (yieldingProc is ActionProc) + { + refinementInstrumentation = new ActionRefinementInstrumentation( + civlTypeChecker, + impl, + originalImpl, + globalSnapshotInstrumentation.OldGlobalMap); + } + else + { + refinementInstrumentation = new SkipRefinementInstrumentation( + civlTypeChecker, + yieldingProc, + globalSnapshotInstrumentation.OldGlobalMap); + } } else { - refinementInstrumentation = new NoneRefinementInstrumentation(); + refinementInstrumentation = new RefinementInstrumentation(); } // initialize noninterferenceInstrumentation @@ -180,7 +186,7 @@ private void TransformImpl(Implementation impl) layerNum, absyMap, globalSnapshotInstrumentation.OldGlobalMap, yieldProc); } - DesugarConcurrency(impl, graph, yieldingLoopHeaders); + DesugarConcurrency(impl); impl.LocVars.AddRange(globalSnapshotInstrumentation.NewLocalVars); impl.LocVars.AddRange(refinementInstrumentation.NewLocalVars); @@ -198,7 +204,7 @@ private Block AddInitialBlock(Implementation impl) return new Block(Token.NoToken, "og_init", initCmds, gotoCmd); } - private Graph ComputeYieldingLoopHeaders(Implementation impl, out HashSet yieldingLoopHeaders) + private void ComputeYieldingLoops(Implementation impl, out HashSet yieldingLoopHeaders, out HashSet blocksInYieldingLoops) { Graph graph; impl.PruneUnreachableBlocks(); @@ -224,7 +230,20 @@ private Graph ComputeYieldingLoopHeaders(Implementation impl, out HashSet } } - return graph; + blocksInYieldingLoops = GetBlocksInAllNaturalLoops(yieldingLoopHeaders, graph); + } + + private HashSet GetBlocksInAllNaturalLoops(HashSet headers, Graph g) + { + var allBlocksInNaturalLoops = new HashSet(); + foreach (Block header in headers) + { + foreach (Block source in g.BackEdgeNodes(header)) + { + g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b)); + } + } + return allBlocksInNaturalLoops; } private bool IsYieldingHeader(Graph graph, Block header) @@ -248,7 +267,13 @@ private bool IsYieldingHeader(Graph graph, Block header) return false; } - private void DesugarConcurrency(Implementation impl, Graph graph, HashSet yieldingLoopHeaders) + private void AddEdge(GotoCmd gotoCmd, Block b) + { + gotoCmd.labelNames.Add(b.Label); + gotoCmd.labelTargets.Add(b); + } + + private void DesugarConcurrency(Implementation impl) { var allYieldPredicates = CollectYields(impl); var allNonemptyYieldPredicates = allYieldPredicates.Values.Where(x => x.Count > 0); @@ -258,9 +283,41 @@ private void DesugarConcurrency(Implementation impl, Graph graph, HashSet } var yieldCheckerBlock = CreateYieldCheckerBlock(); + var refinementCheckerBlock = CreateRefinementCheckerBlock(); + var refinementCheckerForYieldingLoopsBlock = CreateRefinementCheckerBlockForYieldingLoops(); var returnBlock = CreateReturnBlock(); SplitBlocks(impl); + HashSet yieldingLoopHeaders; + HashSet blocksInYieldingLoops; + ComputeYieldingLoops(impl, out yieldingLoopHeaders, out blocksInYieldingLoops); + foreach (Block header in yieldingLoopHeaders) + { + foreach (Block pred in header.Predecessors) + { + var gotoCmd = pred.TransferCmd as GotoCmd; + AddEdge(gotoCmd, yieldCheckerBlock); + if (blocksInYieldingLoops.Contains(pred)) + { + AddEdge(gotoCmd, refinementCheckerForYieldingLoopsBlock); + } + else + { + AddEdge(gotoCmd, refinementCheckerBlock); + } + } + List firstCmds; + List secondCmds; + SplitCmds(header.Cmds, out firstCmds, out secondCmds); + List newCmds = new List(); + newCmds.AddRange(firstCmds); + newCmds.AddRange(globalSnapshotInstrumentation.CreateUpdatesToOldGlobalVars()); + newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars()); + newCmds.AddRange(noninterferenceInstrumentation.CreateUpdatesToPermissionCollector(header)); + newCmds.AddRange(secondCmds); + header.Cmds = newCmds; + } + // add jumps to yieldCheckerBlock and returnBlock foreach (var b in impl.Blocks) { @@ -288,8 +345,15 @@ private void DesugarConcurrency(Implementation impl, Graph graph, HashSet } if (addEdge) { - gotoCmd.labelNames.Add(yieldCheckerBlock.Label); - gotoCmd.labelTargets.Add(yieldCheckerBlock); + AddEdge(gotoCmd, yieldCheckerBlock); + if (blocksInYieldingLoops.Contains(b)) + { + AddEdge(gotoCmd, refinementCheckerForYieldingLoopsBlock); + } + else + { + AddEdge(gotoCmd, refinementCheckerBlock); + } } } else @@ -297,15 +361,6 @@ private void DesugarConcurrency(Implementation impl, Graph graph, HashSet b.TransferCmd = new GotoCmd(b.TransferCmd.tok, new List { returnBlock.Label }, new List { returnBlock }); } } - foreach (Block header in yieldingLoopHeaders) - { - foreach (Block pred in header.Predecessors) - { - var gotoCmd = pred.TransferCmd as GotoCmd; - gotoCmd.labelNames.Add(yieldCheckerBlock.Label); - gotoCmd.labelTargets.Add(yieldCheckerBlock); - } - } // desugar YieldCmd, CallCmd, and ParCallCmd foreach (Block b in impl.Blocks) @@ -316,7 +371,10 @@ private void DesugarConcurrency(Implementation impl, Graph graph, HashSet if (cmd is YieldCmd yieldCmd) { var newCmds = new List(); - newCmds.AddRange(refinementInstrumentation.CreateUpdateCmds()); + if (!blocksInYieldingLoops.Contains(b)) + { + newCmds.AddRange(refinementInstrumentation.CreateUpdatesToRefinementVars()); + } var yieldPredicates = allYieldPredicates[yieldCmd]; newCmds.AddRange(yieldPredicates); newCmds.AddRange(DesugarYieldCmd(yieldCmd, yieldPredicates)); @@ -326,7 +384,10 @@ private void DesugarConcurrency(Implementation impl, Graph graph, HashSet else if (cmd is CallCmd callCmd && yieldingProcs.Contains(callCmd.Proc)) { List newCmds = new List(); - newCmds.AddRange(refinementInstrumentation.CreateUpdateCmds()); + if (!blocksInYieldingLoops.Contains(b)) + { + newCmds.AddRange(refinementInstrumentation.CreateUpdatesToRefinementVars()); + } if (callCmd.IsAsync) { if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) @@ -360,7 +421,10 @@ private void DesugarConcurrency(Implementation impl, Graph graph, HashSet else if (cmd is ParCallCmd parCallCmd) { List newCmds = new List(); - newCmds.AddRange(refinementInstrumentation.CreateUpdateCmds()); + if (!blocksInYieldingLoops.Contains(b)) + { + newCmds.AddRange(refinementInstrumentation.CreateUpdatesToRefinementVars()); + } newCmds.AddRange(DesugarParCallCmd(parCallCmd)); if (civlTypeChecker.sharedVariables.Count > 0) { @@ -375,8 +439,9 @@ private void DesugarConcurrency(Implementation impl, Graph graph, HashSet } } - impl.Blocks.AddRange(InstrumentYieldingLoopHeaders(graph, yieldingLoopHeaders)); impl.Blocks.Add(yieldCheckerBlock); + impl.Blocks.Add(refinementCheckerBlock); + impl.Blocks.Add(refinementCheckerForYieldingLoopsBlock); impl.Blocks.Add(returnBlock); impl.Blocks.Insert(0, AddInitialBlock(impl)); } @@ -463,17 +528,33 @@ private void SplitBlocks(Implementation impl) private Block CreateYieldCheckerBlock() { var newCmds = new List(); - newCmds.AddRange(refinementInstrumentation.CreateAssertCmds()); newCmds.AddRange(noninterferenceInstrumentation.CreateCallToYieldProc()); newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); return new Block(Token.NoToken, "YieldChecker", newCmds, new ReturnCmd(Token.NoToken)); } + private Block CreateRefinementCheckerBlock() + { + var newCmds = new List(); + newCmds.AddRange(refinementInstrumentation.CreateAssertCmds()); + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); + return new Block(Token.NoToken, "RefinementChecker", newCmds, new ReturnCmd(Token.NoToken)); + } + + private Block CreateRefinementCheckerBlockForYieldingLoops() + { + var newCmds = new List(); + newCmds.AddRange(refinementInstrumentation.CreateUnchangedGlobalsAssertCmds()); + newCmds.AddRange(refinementInstrumentation.CreateUnchangedOutputsAssertCmds()); + newCmds.Add(new AssumeCmd(Token.NoToken, Expr.False)); + return new Block(Token.NoToken, "RefinementCheckerForYieldingLoops", newCmds, new ReturnCmd(Token.NoToken)); + } + private Block CreateReturnBlock() { var returnBlockCmds = new List(); - returnBlockCmds.AddRange(refinementInstrumentation.CreateUpdateCmds()); - returnBlockCmds.AddRange(refinementInstrumentation.CreateFinalAssertCmds()); + returnBlockCmds.AddRange(refinementInstrumentation.CreateUpdatesToRefinementVars()); + returnBlockCmds.AddRange(refinementInstrumentation.CreateReturnAssertCmds()); return new Block(Token.NoToken, "ReturnChecker", returnBlockCmds, new ReturnCmd(Token.NoToken)); } @@ -565,68 +646,6 @@ private Formal ParCallDesugarFormal(Variable v, int count, bool incoming) new TypedIdent(Token.NoToken, $"og_{count}_{v.Name}", v.TypedIdent.Type), incoming); } - private List InstrumentYieldingLoopHeaders(Graph graph, HashSet yieldingLoopHeaders) - { - var newBlocks = new List(); - var headerToInstrumentationBlocks = new Dictionary>(); - var headerToNonBackEdgeInstrumentationBlocks = new Dictionary>(); - foreach (Block header in yieldingLoopHeaders) - { - headerToInstrumentationBlocks[header] = new List(); - headerToNonBackEdgeInstrumentationBlocks[header] = new List(); - foreach (Block pred in header.Predecessors) - { - var gotoCmd = pred.TransferCmd as GotoCmd; - if (gotoCmd.labelTargets.Count == 1) - { - headerToInstrumentationBlocks[header].Add(pred); - if (!graph.BackEdgeNodes(header).Contains(pred)) - { - headerToNonBackEdgeInstrumentationBlocks[header].Add(pred); - } - } - else - { - var newBlock = new Block(Token.NoToken, $"{pred.Label}_to_{header.Label}", new List(), pred.TransferCmd); - pred.TransferCmd = new GotoCmd(Token.NoToken, new List { newBlock.Label }, new List { newBlock }); - headerToInstrumentationBlocks[header].Add(newBlock); - if (!graph.BackEdgeNodes(header).Contains(pred)) - { - headerToNonBackEdgeInstrumentationBlocks[header].Add(newBlock); - } - newBlocks.Add(newBlock); - } - } - } - - foreach (Block header in yieldingLoopHeaders) - { - foreach (Block pred in headerToInstrumentationBlocks[header]) - { - pred.cmds.AddRange(refinementInstrumentation.CreateUpdateCmds()); - } - - foreach (Block pred in headerToNonBackEdgeInstrumentationBlocks[header]) - { - pred.cmds.AddRange(refinementInstrumentation.CreateYieldingLoopHeaderInitCmds(header)); - } - - List firstCmds; - List secondCmds; - SplitCmds(header.Cmds, out firstCmds, out secondCmds); - List newCmds = new List(); - newCmds.AddRange(firstCmds); - newCmds.AddRange(refinementInstrumentation.CreateYieldingLoopHeaderAssertCmds(header)); - newCmds.AddRange(globalSnapshotInstrumentation.CreateUpdatesToOldGlobalVars()); - newCmds.AddRange(refinementInstrumentation.CreateUpdatesToOldOutputVars()); - newCmds.AddRange(noninterferenceInstrumentation.CreateUpdatesToPermissionCollector(header)); - newCmds.AddRange(secondCmds); - header.Cmds = newCmds; - } - - return newBlocks; - } - private void SplitCmds(List cmds, out List firstCmds, out List secondCmds) { firstCmds = new List(); diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect index b4a64d106..ccb7c7688 100644 --- a/Test/civl/bar.bpl.expect +++ b/Test/civl/bar.bpl.expect @@ -1,15 +1,11 @@ bar.bpl(28,3): Error: Non-interference check failed Execution trace: bar.bpl(7,3): anon0 - bar.bpl(7,3): anon0_1 bar.bpl(14,5): inline$AtomicIncr$0$anon0 - (0,0): YieldChecker (0,0): inline$Impl_YieldChecker_PC_1$0$L0 bar.bpl(28,3): Error: Non-interference check failed Execution trace: bar.bpl(38,3): anon0 - bar.bpl(38,3): anon0_1 - (0,0): YieldChecker (0,0): inline$Impl_YieldChecker_PC_1$0$L0 Boogie program verifier finished with 8 verified, 2 errors diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect index dad9a12fe..fd5dcb970 100644 --- a/Test/civl/foo.bpl.expect +++ b/Test/civl/foo.bpl.expect @@ -1,9 +1,7 @@ foo.bpl(30,3): Error: Non-interference check failed Execution trace: foo.bpl(7,3): anon0 - foo.bpl(7,3): anon0_1 foo.bpl(14,5): inline$AtomicIncr$0$anon0 - (0,0): YieldChecker (0,0): inline$Impl_YieldChecker_PC_1$0$L0 Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/lock2.bpl b/Test/civl/lock2.bpl index a32cc252e..c99326e25 100644 --- a/Test/civl/lock2.bpl +++ b/Test/civl/lock2.bpl @@ -36,10 +36,10 @@ procedure {:yields} {:layer 1} {:refines "AtomicEnter"} Enter() yield; while (true) { call _old := CAS(0, 1); - yield; if (_old == 0) { break; } + yield; while (true) { call curr := Read(); yield; @@ -72,4 +72,4 @@ procedure {:atomic} {:layer 1,2} AtomicLeave() modifies b; { b := 0; } -procedure {:yields} {:layer 0} {:refines "AtomicLeave"} Leave(); \ No newline at end of file +procedure {:yields} {:layer 0} {:refines "AtomicLeave"} Leave(); diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect index afbdb5a5f..d9d91410c 100644 --- a/Test/civl/parallel1.bpl.expect +++ b/Test/civl/parallel1.bpl.expect @@ -1,9 +1,7 @@ parallel1.bpl(30,3): Error: Non-interference check failed Execution trace: parallel1.bpl(7,3): anon0 - parallel1.bpl(7,3): anon0_1 parallel1.bpl(14,5): inline$AtomicIncr$0$anon0 - (0,0): YieldChecker (0,0): inline$Impl_YieldChecker_PC_1$0$L0 Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/refinement.bpl.expect b/Test/civl/refinement.bpl.expect index 1a164101b..487379684 100644 --- a/Test/civl/refinement.bpl.expect +++ b/Test/civl/refinement.bpl.expect @@ -2,16 +2,16 @@ Execution trace: refinement.bpl(8,3): anon0 refinement.bpl(8,3): anon0_2 - refinement.bpl(43,5): inline$INCR$1$anon0 - refinement.bpl(8,3): anon0_1 refinement.bpl(43,5): inline$INCR$0$anon0 - (0,0): YieldChecker + refinement.bpl(8,3): anon0_1 + refinement.bpl(43,5): inline$INCR$1$anon0 + (0,0): RefinementChecker (0,0): Error: Transition invariant violated in initial state Execution trace: refinement.bpl(17,3): anon0 refinement.bpl(17,3): anon0_2 refinement.bpl(50,5): inline$DECR$0$anon0 - (0,0): YieldChecker + (0,0): RefinementChecker (0,0): Error: Transition invariant violated in final state Execution trace: refinement.bpl(17,3): anon0 @@ -19,6 +19,6 @@ Execution trace: refinement.bpl(50,5): inline$DECR$0$anon0 refinement.bpl(17,3): anon0_1 refinement.bpl(43,5): inline$INCR$0$anon0 - (0,0): YieldChecker + (0,0): RefinementChecker Boogie program verifier finished with 6 verified, 3 errors diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect index 7c1429677..a9b5cb8a4 100644 --- a/Test/civl/t1.bpl.expect +++ b/Test/civl/t1.bpl.expect @@ -3,7 +3,6 @@ Execution trace: t1.bpl(99,13): anon0 t1.bpl(99,13): anon0_1 t1.bpl(99,13): anon0_1$1 - (0,0): YieldChecker (0,0): inline$Impl_YieldChecker_A_1$0$L1 Boogie program verifier finished with 10 verified, 1 error diff --git a/Test/civl/wsq.bpl b/Test/civl/wsq.bpl index 23b79fb4c..4b42fea7f 100644 --- a/Test/civl/wsq.bpl +++ b/Test/civl/wsq.bpl @@ -9,8 +9,6 @@ function {:inline} {:linear "tid"} TidCollector(x: Tid) : [Tid]bool MapConstBool(false)[x := true] } - - var {:layer 0,3} H: int; var {:layer 0,3} T: int; var {:layer 0,3} items: [int]int; @@ -99,7 +97,7 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); var {:layer 3} oldH:int; var {:layer 3} oldT:int; var {:layer 3} oldStatusT:bool; - + yield; assert {:layer 3} {:expand} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} {:expand} {:expand} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -114,7 +112,7 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); assert {:layer 3} tid == ptTid && t == T; assert {:layer 3} oldH <= H && oldT == T; assert {:layer 3} (forall i:int :: i>=T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); - + call writeItems_put(tid,t, task); call oldH, oldT := GhostRead(); @@ -126,7 +124,7 @@ ensures {:layer 3} {:expand} emptyInv(put_in_cs, take_in_cs, items,status,T); assert {:layer 3} oldH <= H && oldT == T; assert {:layer 3} (forall i:int :: i>T ==> status[i] == NOT_IN_Q && items[i] == EMPTY); - + call writeT_put(tid, t+1); call oldH, oldT := GhostRead(); @@ -162,7 +160,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - + while(true) invariant {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; invariant {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -172,7 +170,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && !take_in_cs && !put_in_cs; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); assert {:layer 3} oldH <= H && oldT == T; - + call t := readT_take_init(tid); call oldH, oldT := GhostRead(); @@ -182,7 +180,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} t == T; assert {:layer 3} items[t-1] == EMPTY ==> H > t-1; assert {:layer 3} oldH <= H && oldT == T; - + t := t-1; call writeT_take(tid, t); @@ -193,7 +191,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} t == T; assert {:layer 3} items[t] == EMPTY ==> H > t; assert {:layer 3} oldH <= H && oldT == T; - + call h := readH_take(tid); call oldH, oldT := GhostRead(); @@ -208,7 +206,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} h <= H; assert {:layer 3} oldH == h; - if(t H ==> items[T] != EMPTY; assert {:layer 3} oldH <= H && oldT == T && !put_in_cs && take_in_cs; - if(t>h) { + if (t>h) { call takeExitCS(tid); call oldH, oldT := GhostRead(); @@ -246,7 +244,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ } call writeT_take_eq(tid, h+1); call oldH, oldT := GhostRead(); - + yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); @@ -255,19 +253,8 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} oldT == T; assert {:layer 3} task == items[t]; assert {:layer 3} !put_in_cs; - - call chk := CAS_H_take(tid, h,h+1); - call oldH, oldT := GhostRead(); - yield; - assert {:layer 3} chk ==> (h+1 == oldH && h_ss[tid] == oldH -1 && task != EMPTY); - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1) && tid == ptTid && h_ss[tid] == h && t_ss[tid] == t; - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} h+1 == T; - assert {:layer 3} task == items[t]; - assert {:layer 3} !take_in_cs; - assert {:layer 3} !put_in_cs; - assert {:layer 3} oldH <= H && oldT == T; + call chk := CAS_H_take(tid, h,h+1); if (chk) { call oldH, oldT := GhostRead(); @@ -286,7 +273,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} h+1 == T && task == items[t] && !take_in_cs && !put_in_cs; assert {:layer 3} oldH <= H && oldT == T; } - + call oldH, oldT := GhostRead(); yield; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T) && tid == ptTid && !put_in_cs; @@ -336,7 +323,7 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); assert {:layer 3} oldH <= H; assert {:layer 3} !steal_in_cs[tid]; - + call h := readH_steal(tid); call oldH, oldT := GhostRead(); @@ -350,7 +337,6 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ call t := readT_steal(tid); - call oldH, oldT := GhostRead(); yield; assert {:layer 3} steal_in_cs[tid]; @@ -374,9 +360,8 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} oldH <= H; return; } - - call task, taskstatus := readItems(tid, h); + call task, taskstatus := readItems(tid, h); call oldH, oldT := GhostRead(); yield; @@ -389,6 +374,15 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} h == H ==> status[H] == IN_Q; call chk := CAS_H_steal(tid, h,h+1); + if (chk) { + call oldH, oldT := GhostRead(); + yield; + assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; + assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); + assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); + assert {:layer 3} oldH <= H && task != EMPTY; + return; + } call oldH, oldT := GhostRead(); yield; @@ -399,18 +393,8 @@ ensures {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_ assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); assert {:layer 3} oldH <= H; - - if(chk) { - call oldH, oldT := GhostRead(); - yield; - assert {:layer 3} stealerTid(tid) && !steal_in_cs[tid]; - assert {:layer 3} queueInv(steal_in_cs,put_in_cs,take_in_cs,items, status, H, T-1); - assert {:layer 3} ideasInv(put_in_cs,items, status, H, T, take_in_cs, steal_in_cs, h_ss, t_ss); - assert {:layer 3} oldH <= H && task != EMPTY; - return; - } } - + call oldH, oldT := GhostRead(); yield; assert {:layer 3} chk && task != EMPTY;