diff --git a/Source/Core/AST/AbsyCmd.cs b/Source/Core/AST/AbsyCmd.cs index a6400e232..97b66daf7 100644 --- a/Source/Core/AST/AbsyCmd.cs +++ b/Source/Core/AST/AbsyCmd.cs @@ -368,10 +368,9 @@ int FreshAnon() return anon++; } - HashSet allLabels = new HashSet(); + private readonly HashSet allLabels = new(); - Errors /*!*/ - errorHandler; + private readonly Errors /*!*/ errorHandler; [ContractInvariantMethod] void ObjectInvariant() @@ -3445,6 +3444,8 @@ public override void Emit(TokenTextWriter stream, int level) public class ReturnCmd : TransferCmd { + public QKeyValue Attributes { get; set; } + public ReturnCmd(IToken /*!*/ tok) : base(tok) { @@ -3476,6 +3477,8 @@ public class GotoCmd : TransferCmd [Rep] public List LabelNames; [Rep] public List LabelTargets; + public QKeyValue Attributes { get; set; } + [ContractInvariantMethod] void ObjectInvariant() { diff --git a/Source/Core/AST/Block.cs b/Source/Core/AST/Block.cs index c6ac50740..4cb78df21 100644 --- a/Source/Core/AST/Block.cs +++ b/Source/Core/AST/Block.cs @@ -128,7 +128,11 @@ public bool IsLive(Variable v) return liveVarsBefore.Contains(v); } - public Block(IToken tok) + public static Block ShallowClone(Block block) { + return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd); + } + + public Block(IToken tok, TransferCmd cmd) : this(tok, "", new List(), new ReturnCmd(tok)) { } diff --git a/Source/Core/AST/CallCmd.cs b/Source/Core/AST/CallCmd.cs index e35541b6d..f20360987 100644 --- a/Source/Core/AST/CallCmd.cs +++ b/Source/Core/AST/CallCmd.cs @@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) Contract.Assert(a != null); // These probably won't have IDs, but copy if they do. if (callId is not null) { - a.CopyIdWithModificationsFrom(tok, req, + (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req, id => new TrackedCallRequiresAssumed(callId, id)); } @@ -1066,7 +1066,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) #endregion if (callId is not null) { - assume.CopyIdWithModificationsFrom(tok, e, + (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e, id => new TrackedCallEnsures(callId, id)); } diff --git a/Source/Core/AST/ICarriesAttributes.cs b/Source/Core/AST/ICarriesAttributes.cs index a24485f89..1f9bbf412 100644 --- a/Source/Core/AST/ICarriesAttributes.cs +++ b/Source/Core/AST/ICarriesAttributes.cs @@ -51,23 +51,25 @@ public void AddStringAttribute(IToken tok, string name, string parameter) Attributes = new QKeyValue(tok, name, new List() {parameter}, Attributes); } + } -public static class CarriesAttributesExtensions -{ - public static void CopyIdFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src) +public static class CarriesAttributesExtensions { + + public static void CopyIdFrom(this ICarriesAttributes destination, IToken tok, ICarriesAttributes src) { var id = src.FindStringAttribute("id"); if (id is not null) { - dest.AddStringAttribute(tok, "id", id); + destination.AddStringAttribute(tok, "id", id); } } - public static void CopyIdWithModificationsFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src, Func modifier) + public static void CopyIdWithModificationsFrom(this ICarriesAttributes destination, IToken tok, + ICarriesAttributes src, Func modifier) { var id = src.FindStringAttribute("id"); if (id is not null) { - dest.AddStringAttribute(tok, "id", modifier(id).SolverLabel); + destination.AddStringAttribute(tok, "id", modifier(id).SolverLabel); } } } \ No newline at end of file diff --git a/Source/Core/AST/Implementation.cs b/Source/Core/AST/Implementation.cs index 6d6d2415c..7a6c565ac 100644 --- a/Source/Core/AST/Implementation.cs +++ b/Source/Core/AST/Implementation.cs @@ -462,19 +462,19 @@ void BlocksWriters(TokenTextWriter stream) { } public void EmitImplementation(TokenTextWriter stream, int level, IEnumerable blocks, - bool showLocals) { + bool showLocals, string nameSuffix = "") { EmitImplementation(stream, level, writer => { foreach (var block in blocks) { block.Emit(writer, level + 1); } - }, showLocals); + }, showLocals, nameSuffix); } - public void EmitImplementation(TokenTextWriter stream, int level, Action printBlocks, bool showLocals) + private void EmitImplementation(TokenTextWriter stream, int level, Action printBlocks, bool showLocals, string nameSuffix = "") { stream.Write(this, level, "implementation "); EmitAttributes(stream); - stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(this.Name)); + stream.Write(this, level, "{0}", TokenTextWriter.SanitizeIdentifier(Name) + nameSuffix); EmitSignature(stream, false); stream.WriteLine(); diff --git a/Source/Core/AST/Program.cs b/Source/Core/AST/Program.cs index 45011b574..82ec6e4ba 100644 --- a/Source/Core/AST/Program.cs +++ b/Source/Core/AST/Program.cs @@ -498,7 +498,7 @@ public static Graph BuildCallGraph(CoreOptions options, Program return callGraph; } - public static Graph GraphFromBlocks(List blocks, bool forward = true) + public static Graph GraphFromBlocksSubset(IReadOnlyList blocks, IReadOnlySet subset = null, bool forward = true) { var result = new Graph(); if (!blocks.Any()) @@ -506,6 +506,9 @@ public static Graph GraphFromBlocks(List blocks, bool forward = tr return result; } void AddEdge(Block a, Block b) { + if (subset != null && (!subset.Contains(a) || !subset.Contains(b))) { + return; + } Contract.Assert(a != null && b != null); if (forward) { result.AddEdge(a, b); @@ -514,7 +517,7 @@ void AddEdge(Block a, Block b) { } } - result.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph + result.AddSource(blocks[0]); foreach (var block in blocks) { if (block.TransferCmd is GotoCmd gtc) @@ -525,6 +528,10 @@ void AddEdge(Block a, Block b) { } return result; } + + public static Graph GraphFromBlocks(IReadOnlyList blocks, bool forward = true) { + return GraphFromBlocksSubset(blocks, null, forward); + } public static Graph /*!*/ GraphFromImpl(Implementation impl, bool forward = true) { diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index b850527c2..eecb93c6b 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -1032,6 +1032,7 @@ TransferCmd = (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; Token y; List/*!*/ xs; List ss = new List(); + QKeyValue kv = null; .) ( "goto" (. y = t; .) Idents (. foreach(IToken/*!*/ s in xs){ @@ -1039,7 +1040,9 @@ TransferCmd ss.Add(s.val); } tc = new GotoCmd(y, ss); .) - | "return" (. tc = new ReturnCmd(t); .) + | "return" + { Attribute } + (. tc = new ReturnCmd(t) { Attributes = kv }; .) ) ";" . @@ -1688,6 +1691,7 @@ SpecBlock List/*!*/ xs; List ss = new List(); b = dummyBlock; + QKeyValue kv = null; Expr/*!*/ e; .) Ident ":" @@ -1706,8 +1710,13 @@ SpecBlock ss.Add(s.val); } b = new Block(x,x.val,cs,new GotoCmd(y,ss)); .) - | "return" Expression - (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .) + | "return" + { Attribute } + Expression + (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) { + Attributes = kv + }); + .) ) ";" . diff --git a/Source/Core/CoreOptions.cs b/Source/Core/CoreOptions.cs index d0d472ff5..b7ab2e965 100644 --- a/Source/Core/CoreOptions.cs +++ b/Source/Core/CoreOptions.cs @@ -10,6 +10,8 @@ namespace Microsoft.Boogie public interface CoreOptions : PrintOptions { public TextWriter OutputWriter { get; } + bool UseBaseNameForFileName { get; } + public enum TypeEncoding { Predicates, diff --git a/Source/Core/Generic/ListExtensions.cs b/Source/Core/Generic/ListExtensions.cs new file mode 100644 index 000000000..6825839b8 --- /dev/null +++ b/Source/Core/Generic/ListExtensions.cs @@ -0,0 +1,31 @@ +using System.Collections; +using System.Collections.Generic; +using System.Linq; + +namespace Microsoft.Boogie; + +public static class ListExtensions { + public static IReadOnlyList Reversed(this IReadOnlyList list) { + return new ReversedReadOnlyList(list); + } +} + +class ReversedReadOnlyList : IReadOnlyList { + private readonly IReadOnlyList inner; + + public ReversedReadOnlyList(IReadOnlyList inner) { + this.inner = inner; + } + + public IEnumerator GetEnumerator() { + return Enumerable.Range(0, inner.Count).Select(index => this[index]).GetEnumerator(); + } + + IEnumerator IEnumerable.GetEnumerator() { + return GetEnumerator(); + } + + public int Count => inner.Count; + + public T this[int index] => inner[^(index + 1)]; +} \ No newline at end of file diff --git a/Source/Core/Util.cs b/Source/Core/Generic/Util.cs similarity index 100% rename from Source/Core/Util.cs rename to Source/Core/Generic/Util.cs diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index ff6ecb84f..cc67d930f 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -1536,6 +1536,7 @@ void TransferCmd(out TransferCmd/*!*/ tc) { Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; Token y; List/*!*/ xs; List ss = new List(); + QKeyValue kv = null; if (la.kind == 55) { Get(); @@ -1548,7 +1549,10 @@ void TransferCmd(out TransferCmd/*!*/ tc) { } else if (la.kind == 56) { Get(); - tc = new ReturnCmd(t); + while (la.kind == 26) { + Attribute(ref kv); + } + tc = new ReturnCmd(t) { Attributes = kv }; } else SynErr(148); Expect(10); } @@ -2558,6 +2562,7 @@ void SpecBlock(out Block/*!*/ b) { List/*!*/ xs; List ss = new List(); b = dummyBlock; + QKeyValue kv = null; Expr/*!*/ e; Ident(out x); @@ -2583,8 +2588,14 @@ void SpecBlock(out Block/*!*/ b) { } else if (la.kind == 56) { Get(); + while (la.kind == 26) { + Attribute(ref kv); + } Expression(out e); - b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); + b = new Block(x,x.val,cs,new ReturnExprCmd(t,e) { + Attributes = kv + }); + } else SynErr(174); Expect(10); } diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index 2e0ae6c67..46df39226 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -523,14 +523,14 @@ private Dictionary> ComputeGlobalControlDependences() foreach (var impl in prog.NonInlinedImplementations()) { var blockGraph = prog.ProcessLoops(options, impl); - localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok)); + localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok, new ReturnCmd(prog.tok))); foreach (var keyValue in localCtrlDeps[impl]) { globalCtrlDep.Add(keyValue.Key, keyValue.Value); } } - var callGraph = Program.BuildCallGraph(options, prog); + Graph callGraph = Program.BuildCallGraph(options, prog); // Add inter-procedural control dependence nodes based on calls foreach (var impl in prog.NonInlinedImplementations()) @@ -548,7 +548,7 @@ private Dictionary> ComputeGlobalControlDependences() var indirectCallees = ComputeIndirectCallees(callGraph, directCallee); foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl])) { - foreach (var c in indirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item)) + foreach (var c in indirectCallees.Select(item => item.Blocks).SelectMany(Item => Item)) { globalCtrlDep[control].Add(c); } @@ -562,17 +562,18 @@ private Dictionary> ComputeGlobalControlDependences() // Finally reverse the dependences - var result = new Dictionary>(); - foreach (var keyValue in globalCtrlDep) + Dictionary> result = new Dictionary>(); + + foreach (var KeyValue in globalCtrlDep) { - foreach (var v in keyValue.Value) + foreach (var v in KeyValue.Value) { if (!result.ContainsKey(v)) { result[v] = new HashSet(); } - result[v].Add(keyValue.Key); + result[v].Add(KeyValue.Key); } } diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props index d81beeac1..2965b7047 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -2,7 +2,7 @@ - 3.2.5 + 3.3.0 net6.0 false Boogie diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs index 171797990..764ea17a4 100644 --- a/Source/ExecutionEngine/CommandLineOptions.cs +++ b/Source/ExecutionEngine/CommandLineOptions.cs @@ -105,7 +105,7 @@ static void PassifyAllImplementations(ExecutionEngineOptions options, ProcessedP foreach(var implementation in processedProgram.Program.Implementations) { vcGenerator.PrepareImplementation(new ImplementationRun(implementation, options.OutputWriter), - callback, out _, out _, out _); + callback, out _, out _); } } diff --git a/Source/ExecutionEngine/ConsolePrinter.cs b/Source/ExecutionEngine/ConsolePrinter.cs index ecb6b4220..183a7028c 100644 --- a/Source/ExecutionEngine/ConsolePrinter.cs +++ b/Source/ExecutionEngine/ConsolePrinter.cs @@ -177,8 +177,9 @@ public virtual void ReportBplError(IToken tok, string message, bool error, TextW message = $"{category}: {message}"; } - var s = tok != null - ? $"{ExecutionEngine.GetFileNameForConsole(Options, tok.filename)}({tok.line},{tok.col}): {message}" + var s = tok != null + ? string.Format("{0}({1},{2}): {3}", ExecutionEngine.GetFileNameForConsole(Options, tok.filename), tok.line, + tok.col, message) : message; if (error) diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 23e42ec75..7cc6abc0c 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -736,16 +736,15 @@ public async Task> GetVerificationTasks(Program { var writer = TextWriter.Null; var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, CheckerPool); - var run = new ImplementationRun(implementation, writer); var collector = new VerificationResultCollector(Options); vcGenerator.PrepareImplementation(run, collector, out _, - out var gotoCmdOrigins, out var modelViewInfo); ConditionGeneration.ResetPredecessors(run.Implementation.Blocks); - var splits = ManualSplitFinder.FocusAndSplit(program, Options, run, gotoCmdOrigins, vcGenerator).ToList(); + var splits = ManualSplitFinder.GetParts(Options, run, + (token, blocks) => new ManualSplit(Options, () => blocks, vcGenerator, run, token)).ToList(); for (var index = 0; index < splits.Count; index++) { var split = splits[index]; split.SplitIndex = index; @@ -1310,6 +1309,8 @@ public void ProcessErrors(OutputPrinter printer, return; } + // When an assertion fails on multiple paths, only show an error for one of them. + errors = errors.DistinctBy(e => e.FailingAssert).ToList(); errors.Sort(new CounterexampleComparer()); foreach (Counterexample error in errors) { diff --git a/Source/ExecutionEngine/ExecutionEngineOptions.cs b/Source/ExecutionEngine/ExecutionEngineOptions.cs index f7e4806df..baf7c48a1 100644 --- a/Source/ExecutionEngine/ExecutionEngineOptions.cs +++ b/Source/ExecutionEngine/ExecutionEngineOptions.cs @@ -22,7 +22,6 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions ShowEnvironment ShowEnv { get; } string Version { get; } string Environment { get; } - bool UseBaseNameForFileName { get; } HashSet Libraries { get; set; } bool NoResolve { get; } bool NoTypecheck { get; } diff --git a/Source/ExecutionEngine/VerificationTask.cs b/Source/ExecutionEngine/VerificationTask.cs index 43dda6925..50f3fd8e5 100644 --- a/Source/ExecutionEngine/VerificationTask.cs +++ b/Source/ExecutionEngine/VerificationTask.cs @@ -44,7 +44,7 @@ public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgra public IVerificationTask FromSeed(int newSeed) { - var split = new ManualSplit(Split.Options, () => Split.Blocks, Split.GotoCmdOrigins, + var split = new ManualSplit(Split.Options, () => Split.Blocks, Split.parent, Split.Run, Split.Token, newSeed); split.SplitIndex = Split.SplitIndex; return new VerificationTask(engine, ProcessedProgram, split, modelViewInfo); diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 2738566dd..2af21485a 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -99,22 +99,22 @@ public bool DominatedBy(Node dominee, Node dominator, List path = null) return true; } - int currentDominatorNum = nodeNumberToImmediateDominator[domineeNum]; + int currentDominator = nodeNumberToImmediateDominator[domineeNum]; while (true) { - if (currentDominatorNum == dominatorNum) + if (currentDominator == dominatorNum) { return true; } - if (currentDominatorNum == sourceNum) + if (currentDominator == sourceNum) { return false; } - path?.Add(postOrderNumberToNode[currentDominatorNum]); + path?.Add(postOrderNumberToNode[currentDominator]); - currentDominatorNum = nodeNumberToImmediateDominator[currentDominatorNum]; + currentDominator = nodeNumberToImmediateDominator[currentDominator]; } } @@ -623,35 +623,55 @@ public List SuccessorsAsList(Node n) } } - // This method gives a simpler way to compute dominators but it assmumes the graph is a DAG. - // With acyclicty we can compute all dominators by traversing the graph (once) in topological order - // (using the property: A vertex's dominator set is unaffected by vertices that come later). - // The method does not check the graph for the DAG property. That risk is on the caller. - public Dictionary> DominatorsFast() + /// + /// This method gives a simpler way to compute dominators but it assmumes the graph is a DAG. + /// With acyclicty we can compute all dominators by traversing the graph (once) in topological order + /// (using the property: A vertex's dominator set is unaffected by vertices that come later). + /// The method does not check the graph for the DAG property. That risk is on the caller. + /// + public Dictionary> AcyclicDominators() { - var topoSorted = TopologicalSort().ToList(); - var dominators = new Dictionary>(); - topoSorted.ForEach(u => dominators[u] = topoSorted.ToHashSet()); - foreach (var node in topoSorted) + var dominatorsPerNode = new Dictionary>(); + foreach (var node in TopologicalSort()) { - var s = new HashSet(); - var predecessors = Predecessors(node).ToList(); - if (predecessors.Count != 0) - { - s.UnionWith(dominators[predecessors.First()]); - predecessors.ForEach(v => s.IntersectWith(dominators[v])); + var predecessors = Predecessors(node); + var dominatorsForNode = Intersection(predecessors.Select(p => dominatorsPerNode[p])); + dominatorsForNode.Add(node); + dominatorsPerNode[node] = dominatorsForNode; + } + return dominatorsPerNode; + } + + public static HashSet Intersection(IEnumerable> sets) { + var first = true; + HashSet result = null; + foreach (var set in sets) { + if (first) { + result = set.ToHashSet(); + first = false; + } else { + result!.IntersectWith(set); } - s.Add(node); - dominators[node] = s; } - return dominators; + + if (result == null) { + return new HashSet(); + } + + return result; } - // Use this method only for DAGs because it uses DominatorsFast() for computing dominators + /// + /// Use this method only for DAGs because it uses DominatorsFast() for computing dominators + /// public Dictionary ImmediateDominator() { - List topoSorted = TopologicalSort().ToList(); - Dictionary> dominators = DominatorsFast(); + var topoSorted = TopologicalSort().ToList(); + var indexPerNode = new Dictionary(); + for (int index = 0; index < topoSorted.Count; index++) { + indexPerNode[topoSorted[index]] = index; + } + var dominators = AcyclicDominators(); var immediateDominator = new Dictionary(); foreach (var node in Nodes) { @@ -659,9 +679,10 @@ public Dictionary ImmediateDominator() { dominators[node].Remove(node); } - immediateDominator[node] = topoSorted.ElementAt(dominators[node].Max(e => topoSorted.IndexOf(e))); + immediateDominator[node] = topoSorted.ElementAt(dominators[node].Max(e => indexPerNode[e])); } - immediateDominator[source] = source; + + immediateDominator.Remove(source); return immediateDominator; } @@ -686,7 +707,7 @@ public List ImmediatelyDominatedBy(Node /*!*/ n) return dominees ?? new List(); } - public List TopologicalSort(bool reversed = false) + public List TopologicalSort(bool reversed = false) { TarjanTopSort(out var acyclic, out var sortedList, reversed); return acyclic ? sortedList : new List(); @@ -1133,7 +1154,7 @@ public string ToDot(Func NodeLabel = null, Func Node return s.ToString(); } - public ICollection ComputeReachability(Node start, bool forward = true) + public ISet ComputeReachability(Node start, bool forward = true) { var todo = new Stack(); var visited = new HashSet(); diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index ee24e7bfa..a787a8a65 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -168,7 +168,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0); new RemoveBackEdges(vcgen).ConvertCfg2Dag(run, taskID: taskId); - var gotoCmdOrigins = vcgen.PassifyImpl(run, out var mvInfo); + vcgen.PassifyImpl(run, out var mvInfo); ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out var ecollector); this.houdiniAssertConstants = ecollector.houdiniAssertConstants; @@ -196,7 +196,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false)); proverInterface.DefineMacro(macro, conjecture); conjecture = exprGen.Function(macro); - handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, gotoCmdOrigins, absyIds, impl.Blocks, impl.debugInfos, collector, + handler = new VerificationConditionGenerator.ErrorReporter(this.houdini.Options, absyIds, impl.Blocks, impl.debugInfos, collector, mvInfo, proverInterface.Context, program, this); } diff --git a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs index 6c39f1ec0..2500faf71 100644 --- a/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs @@ -98,8 +98,9 @@ procedure Procedure(y: int) var engine = ExecutionEngine.CreateWithoutSharedCache(options); var tasks = await engine.GetVerificationTasks(program); - // The first split is empty. Maybe it can be optimized away - Assert.AreEqual(4, tasks.Count); + // The implicit return at the end gets a separate VC. + // first split is empty. Maybe it can be optimized away + Assert.AreEqual(5, tasks.Count); var outcomes = new List { SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid }; for (var index = 0; index < outcomes.Count; index++) diff --git a/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs b/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs index fb0087cd8..94505c1c9 100644 --- a/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs +++ b/Source/UnitTests/ExecutionEngineTests/RandomSeedTest.cs @@ -17,7 +17,7 @@ public class RandomSeedTest axiom N <= 3; procedure nEquals3() - ensures true; + ensures 1 == 1; { }"; diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 2e7f91060..8188ebb07 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -222,7 +222,7 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu Block origStartBlock = impl.Blocks[0]; Block insertionPoint = new Block( - new Token(-17, -4), blockLabel, startCmds, + Token.NoToken, blockLabel, startCmds, new GotoCmd(impl.tok, new List {origStartBlock.Label}, new List {origStartBlock})); impl.Blocks.Insert(0, insertionPoint); // make insertionPoint the start block @@ -236,7 +236,7 @@ protected static void InjectPreconditions(VCGenOptions options, ImplementationRu AssumeCmd c = new AssumeCmd(req.tok, e, CivlAttributes.ApplySubstitutionToPoolHints(formalProcImplSubst, req.Attributes)); // Copy any {:id ...} from the precondition to the assumption, so // we can track it while analyzing verification coverage. - c.CopyIdFrom(req.tok, req); + (c as ICarriesAttributes).CopyIdFrom(req.tok, req); c.IrrelevantForChecksumComputation = true; insertionPoint.Cmds.Add(c); if (debugWriter != null) @@ -450,8 +450,6 @@ public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool pr options.PrintDesugarings = oldPrintDesugaringSetting; } - - public static void ResetPredecessors(List blocks) { Contract.Requires(blocks != null); @@ -881,8 +879,7 @@ private void AddDebugInfo(Cmd c, Dictionary incarnationMap, List { foreach (var param in current.Params) { - if (param is IdentifierExpr identifierExpr) - { + if (param is IdentifierExpr identifierExpr) { debugExprs.Add(incarnationMap.GetValueOrDefault(identifierExpr.Decl, identifierExpr)); } else @@ -1200,7 +1197,7 @@ protected void TurnIntoPassiveCmd(TextWriter traceWriter, Cmd c, Block enclosing var assumeCmd = new AssumeCmd(c.tok, assumption); // Copy any {:id ...} from the assignment to the assumption, so // we can track it while analyzing verification coverage. - assumeCmd.CopyIdFrom(assign.tok, assign); + (assumeCmd as ICarriesAttributes).CopyIdFrom(assign.tok, assign); passiveCmds.Add(assumeCmd); } @@ -1394,7 +1391,7 @@ public Block CreateBlockBetween(int predIndex, Block succ) bs.Add(succ); Block newBlock = new Block( - new Token(-17, -4), + Token.NoToken, newBlockLabel, new List(), new GotoCmd(Token.NoToken, ls, bs) diff --git a/Source/VCGeneration/AssertCounterexample.cs b/Source/VCGeneration/Counterexample/AssertCounterexample.cs similarity index 82% rename from Source/VCGeneration/AssertCounterexample.cs rename to Source/VCGeneration/Counterexample/AssertCounterexample.cs index e43d6fecd..522b55cd0 100644 --- a/Source/VCGeneration/AssertCounterexample.cs +++ b/Source/VCGeneration/Counterexample/AssertCounterexample.cs @@ -6,23 +6,19 @@ namespace Microsoft.Boogie; public class AssertCounterexample : Counterexample { - [Peer] public AssertCmd FailingAssert; - [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(FailingAssert != null); } public AssertCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun) - : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssert) { Contract.Requires(trace != null); Contract.Requires(failingAssert != null); Contract.Requires(context != null); - this.FailingAssert = failingAssert; } protected override Cmd ModelFailingCommand => FailingAssert; @@ -32,10 +28,7 @@ public override int GetLocation() return FailingAssert.tok.line * 1000 + FailingAssert.tok.col; } - public override byte[] Checksum - { - get { return FailingAssert.Checksum; } - } + public override byte[] Checksum => FailingAssert.Checksum; public override Counterexample Clone() { diff --git a/Source/VCGeneration/Counterexamples/CallCounterexample.cs b/Source/VCGeneration/Counterexample/CallCounterexample.cs similarity index 86% rename from Source/VCGeneration/Counterexamples/CallCounterexample.cs rename to Source/VCGeneration/Counterexample/CallCounterexample.cs index e98ce17b3..199df0c15 100644 --- a/Source/VCGeneration/Counterexamples/CallCounterexample.cs +++ b/Source/VCGeneration/Counterexample/CallCounterexample.cs @@ -6,9 +6,8 @@ namespace Microsoft.Boogie; public class CallCounterexample : Counterexample { - public CallCmd FailingCall; - public Requires FailingRequires; - public AssertRequiresCmd FailingFailingAssert; + public readonly CallCmd FailingCall; + public readonly Requires FailingRequires; [ContractInvariantMethod] void ObjectInvariant() @@ -20,7 +19,7 @@ void ObjectInvariant() public CallCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertRequiresCmd failingAssertRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum = null) - : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssertRequires) { var failingRequires = failingAssertRequires.Requires; var failingCall = failingAssertRequires.Call; @@ -31,7 +30,6 @@ public CallCounterexample(VCGenOptions options, List trace, List Contract.Requires(failingRequires != null); this.FailingCall = failingCall; this.FailingRequires = failingRequires; - this.FailingFailingAssert = failingAssertRequires; this.checksum = checksum; this.SugaredCmdChecksum = failingCall.Checksum; } @@ -52,7 +50,7 @@ public override byte[] Checksum public override Counterexample Clone() { - var ret = new CallCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, Model, MvInfo, Context, ProofRun, Checksum); + var ret = new CallCounterexample(Options, Trace, AugmentedTrace, (AssertRequiresCmd)FailingAssert, Model, MvInfo, Context, ProofRun, Checksum); ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } diff --git a/Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs b/Source/VCGeneration/Counterexample/CalleeCounterexampleInfo.cs similarity index 100% rename from Source/VCGeneration/Counterexamples/CalleeCounterexampleInfo.cs rename to Source/VCGeneration/Counterexample/CalleeCounterexampleInfo.cs diff --git a/Source/VCGeneration/Counterexamples/Counterexample.cs b/Source/VCGeneration/Counterexample/Counterexample.cs similarity index 97% rename from Source/VCGeneration/Counterexamples/Counterexample.cs rename to Source/VCGeneration/Counterexample/Counterexample.cs index da9cdca9c..15d4cab2b 100644 --- a/Source/VCGeneration/Counterexamples/Counterexample.cs +++ b/Source/VCGeneration/Counterexample/Counterexample.cs @@ -25,6 +25,7 @@ void ObjectInvariant() protected readonly VCGenOptions Options; [Peer] public List Trace; public readonly List AugmentedTrace; + public AssertCmd FailingAssert { get; } public Model Model { get; } public readonly ModelViewInfo MvInfo; public readonly ProverContext Context; @@ -35,7 +36,7 @@ void ObjectInvariant() public Dictionary CalleeCounterexamples; internal Counterexample(VCGenOptions options, List trace, List augmentedTrace, Model model, - VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun) + VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, AssertCmd failingAssert) { Contract.Requires(trace != null); Contract.Requires(context != null); @@ -45,6 +46,7 @@ internal Counterexample(VCGenOptions options, List trace, List au this.MvInfo = mvInfo; this.Context = context; this.ProofRun = proofRun; + this.FailingAssert = failingAssert; this.CalleeCounterexamples = new Dictionary(); // the call to instance method GetModelValue in the following code requires the fields Model and Context to be initialized if (augmentedTrace != null) @@ -112,7 +114,7 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { int numBlock = -1; string ind = new string(' ', indent); - foreach (var block in Trace) + foreach (Block block in Trace) { Contract.Assert(block != null); numBlock++; @@ -120,13 +122,9 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) { tw.WriteLine("{0}", ind); } - else - { + else { // for ErrorTrace == 1 restrict the output; - // do not print tokens with -17:-4 as their location because they have been - // introduced in the translation and do not give any useful feedback to the user - if (Options.ErrorTrace == 1 && block.tok.line == -17 && block.tok.col == -4) - { + if (Options.ErrorTrace == 1 && block.tok == Token.NoToken) { continue; } @@ -137,8 +135,7 @@ public void Print(int indent, TextWriter tw, Action blockAction = null) for (int numInstr = 0; numInstr < block.Cmds.Count; numInstr++) { var loc = new TraceLocation(numBlock, numInstr); - if (!CalleeCounterexamples.ContainsKey(loc)) - { + if (!CalleeCounterexamples.ContainsKey(loc)) { continue; } diff --git a/Source/VCGeneration/Counterexamples/CounterexampleComparer.cs b/Source/VCGeneration/Counterexample/CounterexampleComparer.cs similarity index 100% rename from Source/VCGeneration/Counterexamples/CounterexampleComparer.cs rename to Source/VCGeneration/Counterexample/CounterexampleComparer.cs diff --git a/Source/VCGeneration/ReturnCounterexample.cs b/Source/VCGeneration/Counterexample/ReturnCounterexample.cs similarity index 85% rename from Source/VCGeneration/ReturnCounterexample.cs rename to Source/VCGeneration/Counterexample/ReturnCounterexample.cs index 526ee4959..98092c946 100644 --- a/Source/VCGeneration/ReturnCounterexample.cs +++ b/Source/VCGeneration/Counterexample/ReturnCounterexample.cs @@ -7,8 +7,7 @@ namespace Microsoft.Boogie; public class ReturnCounterexample : Counterexample { public TransferCmd FailingReturn; - public Ensures FailingEnsures; - public AssertEnsuresCmd FailingFailingAssert; + public readonly Ensures FailingEnsures; [ContractInvariantMethod] void ObjectInvariant() @@ -21,7 +20,7 @@ void ObjectInvariant() public ReturnCounterexample(VCGenOptions options, List trace, List augmentedTrace, AssertEnsuresCmd failingAssertEnsures, TransferCmd failingReturn, Model model, VC.ModelViewInfo mvInfo, ProverContext context, ProofRun proofRun, byte[] checksum) - : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun) + : base(options, trace, augmentedTrace, model, mvInfo, context, proofRun, failingAssertEnsures) { var failingEnsures = failingAssertEnsures.Ensures; Contract.Requires(trace != null); @@ -31,7 +30,6 @@ public ReturnCounterexample(VCGenOptions options, List trace, List /// Returns the checksum of the corresponding assertion. @@ -51,7 +49,7 @@ public override int GetLocation() public override Counterexample Clone() { - var ret = new ReturnCounterexample(Options, Trace, AugmentedTrace, FailingFailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); + var ret = new ReturnCounterexample(Options, Trace, AugmentedTrace, (AssertEnsuresCmd)FailingAssert, FailingReturn, Model, MvInfo, Context, ProofRun, checksum); ret.CalleeCounterexamples = CalleeCounterexamples; return ret; } diff --git a/Source/VCGeneration/Counterexamples/TraceLocation.cs b/Source/VCGeneration/Counterexample/TraceLocation.cs similarity index 100% rename from Source/VCGeneration/Counterexamples/TraceLocation.cs rename to Source/VCGeneration/Counterexample/TraceLocation.cs diff --git a/Source/VCGeneration/VerifierCallback.cs b/Source/VCGeneration/Counterexample/VerifierCallback.cs similarity index 100% rename from Source/VCGeneration/VerifierCallback.cs rename to Source/VCGeneration/Counterexample/VerifierCallback.cs diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs deleted file mode 100644 index 2da576e11..000000000 --- a/Source/VCGeneration/FocusAttribute.cs +++ /dev/null @@ -1,147 +0,0 @@ -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Linq; -using Microsoft.Boogie; -using VC; -using Block = Microsoft.Boogie.Block; -using Cmd = Microsoft.Boogie.Cmd; -using PredicateCmd = Microsoft.Boogie.PredicateCmd; -using QKeyValue = Microsoft.Boogie.QKeyValue; -using ReturnCmd = Microsoft.Boogie.ReturnCmd; -using TransferCmd = Microsoft.Boogie.TransferCmd; -using VCGenOptions = Microsoft.Boogie.VCGenOptions; - -namespace VCGeneration; - -public static class FocusAttribute -{ - - public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VerificationConditionGenerator par) - { - var impl = run.Implementation; - var dag = Program.GraphFromImpl(impl); - var topologicallySortedBlocks = dag.TopologicalSort().ToList(); - // By default, we process the foci in a top-down fashion, i.e., in the topological order. - // If the user sets the RelaxFocus flag, we use the reverse (topological) order. - var focusBlocks = GetFocusBlocks(topologicallySortedBlocks); - if (par.CheckerPool.Options.RelaxFocus) { - focusBlocks.Reverse(); - } - if (!focusBlocks.Any()) { - return new List { new(options, () => impl.Blocks, gotoCmdOrigins, par, run, run.Implementation.tok) }; - } - - var ancestorsPerBlock = new Dictionary>(); - var descendantsPerBlock = new Dictionary>(); - focusBlocks.ForEach(fb => ancestorsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block, false).ToHashSet()); - focusBlocks.ForEach(fb => descendantsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block, true).ToHashSet()); - var result = new List(); - var duplicator = new Duplicator(); - - FocusRec(run.Implementation.tok, 0, impl.Blocks, new List()); - return result; - - void FocusRec(IToken focusToken, int focusIndex, IReadOnlyList blocksToInclude, IReadOnlyList freeAssumeBlocks) - { - if (focusIndex == focusBlocks.Count) - { - // it is important for l to be consistent with reverse topological order. - var sortedBlocks = dag.TopologicalSort().Where(blocksToInclude.Contains).Reverse(); - // assert that the root block, impl.Blocks[0], is in l - var newBlocks = new List(); - var oldToNewBlockMap = new Dictionary(blocksToInclude.Count()); - foreach (var block in sortedBlocks) - { - var newBlock = (Block)duplicator.Visit(block); - newBlocks.Add(newBlock); - oldToNewBlockMap[block] = newBlock; - // freeBlocks consist of the predecessors of the relevant foci. - // Their assertions turn into assumes and any splits inside them are disabled. - if(freeAssumeBlocks.Contains(block)) - { - newBlock.Cmds = block.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(DisableSplits).ToList(); - } - if (block.TransferCmd is GotoCmd gtc) - { - var targets = gtc.LabelTargets.Where(blocksToInclude.Contains).ToList(); - newBlock.TransferCmd = new GotoCmd(gtc.tok, - targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), - targets.Select(blk => oldToNewBlockMap[blk]).ToList()); - } - } - newBlocks.Reverse(); - Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]); - result.Add(new ManualSplit(options, () => - { - BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); - return newBlocks; - }, gotoCmdOrigins, par, run, focusToken)); - } - else if (!blocksToInclude.Contains(focusBlocks[focusIndex].Block) || freeAssumeBlocks.Contains(focusBlocks[focusIndex].Block)) - { - FocusRec(focusBlocks[focusIndex].Token, focusIndex + 1, blocksToInclude, freeAssumeBlocks); - } - else - { - var (block, nextToken) = focusBlocks[focusIndex]; // assert b in blocks - var dominatedBlocks = DominatedBlocks(topologicallySortedBlocks, block, blocksToInclude); - // the first part takes all blocks except the ones dominated by the focus block - FocusRec(nextToken, focusIndex + 1, blocksToInclude.Where(blk => !dominatedBlocks.Contains(blk)).ToList(), freeAssumeBlocks); - var ancestors = ancestorsPerBlock[block]; - ancestors.Remove(block); - var descendants = descendantsPerBlock[block]; - // the other part takes all the ancestors, the focus block, and the descendants. - FocusRec(nextToken, focusIndex + 1, - ancestors.Union(descendants).Intersect(blocksToInclude).ToList(), - ancestors.Union(freeAssumeBlocks).ToList()); - } - } - } - - // finds all the blocks dominated by focusBlock in the subgraph - // which only contains vertices of subgraph. - private static HashSet DominatedBlocks(List topologicallySortedBlocks, Block focusBlock, IEnumerable subgraph) - { - var dominators = new Dictionary>(); - foreach (var b in topologicallySortedBlocks.Where(subgraph.Contains)) - { - var s = new HashSet(); - var pred = b.Predecessors.Where(subgraph.Contains).ToList(); - if (pred.Count != 0) - { - s.UnionWith(dominators[pred[0]]); - pred.ForEach(blk => s.IntersectWith(dominators[blk])); - } - s.Add(b); - dominators[b] = s; - } - return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet(); - } - - private static Cmd DisableSplits(Cmd command) - { - if (command is not PredicateCmd pc) - { - return command; - } - - for (var kv = pc.Attributes; kv != null; kv = kv.Next) - { - if (kv.Key == "split") - { - kv.AddParam(new LiteralExpr(Token.NoToken, false)); - } - } - return command; - } - - private static List<(Block Block, IToken Token)> GetFocusBlocks(List blocks) { - return blocks. - Select(block => (Block: block, FocusCommand: block.Cmds.FirstOrDefault(IsFocusCmd)?.tok)). - Where(t => t.FocusCommand != null).ToList(); - } - - private static bool IsFocusCmd(Cmd c) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); - } -} \ No newline at end of file diff --git a/Source/VCGeneration/LoopExtractor.cs b/Source/VCGeneration/LoopExtractor.cs index a8fa2bc30..e0f40524b 100644 --- a/Source/VCGeneration/LoopExtractor.cs +++ b/Source/VCGeneration/LoopExtractor.cs @@ -313,10 +313,7 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G continue; } - Block newBlock = new Block(block.tok) - { - Label = block.Label - }; + var newBlock = Block.ShallowClone(block); if (headRecursion && block == header) { CallCmd callCmd = (CallCmd) (loopHeaderToCallCmd2[header]).Clone(); @@ -334,11 +331,8 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G blockMap[block] = newBlock; if (newBlocksCreated.TryGetValue(block, out var original)) { - var newBlock2 = new Block(original.tok) - { - Label = original.Label, - Cmds = Substituter.Apply(subst, original.Cmds) - }; + var newBlock2 = Block.ShallowClone(original); + newBlock2.Cmds = Substituter.Apply(subst, original.Cmds); blockMap[original] = newBlock2; } @@ -350,22 +344,18 @@ static void CreateProceduresForLoops(CoreOptions options, Implementation impl, G auxGotoCmd.LabelTargets != null && auxGotoCmd.LabelTargets.Count >= 1); //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode var loopNodes = GetBlocksInAllNaturalLoops(options, header, g); //var loopNodes = g.NaturalLoops(header, source); - foreach (var bl in auxGotoCmd.LabelTargets) - { - if (!g.Nodes.Contains(bl) || //newly created blocks are not present in NaturalLoop(header, xx, g) - loopNodes.Contains(bl)) - { + foreach (var bl in auxGotoCmd.LabelTargets) { + if (!g.Nodes.Contains(bl) || // newly created blocks are not present in NaturalLoop(header, xx, g) + loopNodes.Contains(bl)) { continue; } - var auxNewBlock = new Block(bl.tok) - { - Label = bl.Label, - //these blocks may have read/write locals that are not present in naturalLoops - //we need to capture these variables - Cmds = Substituter.Apply(subst, bl.Cmds) - }; - //add restoration code for such blocks + var auxNewBlock = Block.ShallowClone(bl); + // these blocks may have read/write locals that are not present in naturalLoops + // we need to capture these variables + auxNewBlock.Cmds = Substituter.Apply(subst, bl.Cmds); + + // add restoration code for such blocks if (loopHeaderToAssignCmd.TryGetValue(header, out var assignCmd)) { auxNewBlock.Cmds.Add(assignCmd); diff --git a/Source/VCGeneration/ManualSplit.cs b/Source/VCGeneration/ManualSplit.cs index 09927d3c1..5b47299b7 100644 --- a/Source/VCGeneration/ManualSplit.cs +++ b/Source/VCGeneration/ManualSplit.cs @@ -1,22 +1,22 @@ using System; using System.Collections.Generic; using Microsoft.Boogie; +using VCGeneration; namespace VC; public class ManualSplit : Split { - public IToken Token { get; } + public IImplementationPartOrigin Token { get; } public ManualSplit(VCGenOptions options, Func> blocks, - Dictionary gotoCmdOrigins, - VerificationConditionGenerator par, + VerificationConditionGenerator parent, ImplementationRun run, - IToken token, int? randomSeed = null) - : base(options, blocks, gotoCmdOrigins, par, run, randomSeed) + IImplementationPartOrigin origin, int? randomSeed = null) + : base(options, blocks, parent, run, randomSeed) { - Token = token; + Token = origin; } } \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs deleted file mode 100644 index ffc6806d2..000000000 --- a/Source/VCGeneration/ManualSplitFinder.cs +++ /dev/null @@ -1,216 +0,0 @@ -#nullable enable -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Linq; -using Microsoft.Boogie; -using VC; - -namespace VCGeneration; - -public static class ManualSplitFinder { - public static IEnumerable FocusAndSplit(Program program, VCGenOptions options, ImplementationRun run, - Dictionary gotoCmdOrigins, VerificationConditionGenerator par) { - var focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); - return focussedImpl.SelectMany(s => FindManualSplits(program, s)); - } - - private static List FindManualSplits(Program program, ManualSplit initialSplit) { - Contract.Requires(initialSplit.Implementation != null); - Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); - - var splitOnEveryAssert = initialSplit.Options.VcsSplitOnEveryAssert; - initialSplit.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); - - var splitPoints = new Dictionary>(); - foreach (var block in initialSplit.Blocks) { - foreach (Cmd command in block.Cmds) { - if (ShouldSplitHere(command, splitOnEveryAssert)) { - splitPoints.GetOrCreate(block, () => new List()).Add(command.tok); - } - } - } - var splits = new List(); - if (!splitPoints.Any()) { - splits.Add(initialSplit); - } else { - Block entryPoint = initialSplit.Blocks[0]; - var blockAssignments = PickBlocksToVerify(initialSplit.Blocks, splitPoints); - var entryBlockHasSplit = splitPoints.ContainsKey(entryPoint); - var firstSplitBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, - -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert); - if (firstSplitBlocks != null) - { - splits.Add(new ManualSplit(initialSplit.Options, () => { - BlockTransformations.Optimize(firstSplitBlocks); - return firstSplitBlocks; - }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, initialSplit.Token)); - } - foreach (var block in initialSplit.Blocks) { - var tokens = splitPoints.GetValueOrDefault(block); - if (tokens == null) { - continue; - } - - for (int i = 0; i < tokens.Count; i++) { - var token = tokens[i]; - bool lastSplitInBlock = i == tokens.Count - 1; - var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, block, lastSplitInBlock, splitOnEveryAssert); - if (newBlocks != null) - { - splits.Add(new ManualSplit(initialSplit.Options, - () => { - BlockTransformations.Optimize(newBlocks); - return newBlocks; - }, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run, token)); - } - } - } - } - return splits; - } - - private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here") - || c is AssertCmd && splitOnEveryAssert; - } - - // Verify b with the last split in blockAssignments[b] - private static Dictionary PickBlocksToVerify(List blocks, Dictionary> splitPoints) { - var todo = new Stack(); - var blockAssignments = new Dictionary(); - var immediateDominator = Program.GraphFromBlocks(blocks).ImmediateDominator(); - todo.Push(blocks[0]); - while (todo.Count > 0) { - var currentBlock = todo.Pop(); - if (blockAssignments.Keys.Contains(currentBlock)) { - continue; - } - - if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. - { - blockAssignments[currentBlock] = currentBlock; - } else if (splitPoints.ContainsKey(immediateDominator[currentBlock])) // if the currentBlock's dominator has a split then it will be associated with that split - { - blockAssignments[currentBlock] = immediateDominator[currentBlock]; - } else { - Contract.Assert(blockAssignments.Keys.Contains(immediateDominator[currentBlock])); - blockAssignments[currentBlock] = blockAssignments[immediateDominator[currentBlock]]; - } - if (currentBlock.TransferCmd is GotoCmd exit) { - exit.LabelTargets.ForEach(blk => todo.Push(blk)); - } - } - return blockAssignments; - } - - private static List SplitOnAssert(VCGenOptions options, List oldBlocks, AssertCmd assertToKeep) { - var oldToNewBlockMap = new Dictionary(oldBlocks.Count); - - var newBlocks = new List(oldBlocks.Count); - foreach (var oldBlock in oldBlocks) { - var newBlock = new Block(oldBlock.tok) { - Label = oldBlock.Label, - Cmds = oldBlock.Cmds.Select(cmd => - cmd != assertToKeep ? CommandTransformations.AssertIntoAssume(options, cmd) : cmd).ToList() - }; - oldToNewBlockMap[oldBlock] = newBlock; - newBlocks.Add(newBlock); - } - - AddBlockJumps(oldBlocks, oldToNewBlockMap); - return newBlocks; - } - private static List? DoPreAssignedManualSplit(VCGenOptions options, List blocks, - Dictionary blockAssignments, int splitNumberWithinBlock, - Block containingBlock, bool lastSplitInBlock, bool splitOnEveryAssert) { - var newBlocks = new List(blocks.Count); // Copies of the original blocks - //var duplicator = new Duplicator(); - var assertionCount = 0; - var oldToNewBlockMap = new Dictionary(blocks.Count); // Maps original blocks to their new copies in newBlocks - foreach (var currentBlock in blocks) { - var newBlock = new Block(currentBlock.tok) - { - Label = currentBlock.Label - }; - - oldToNewBlockMap[currentBlock] = newBlock; - newBlocks.Add(newBlock); - if (currentBlock == containingBlock) - { - newBlock.Cmds = GetCommandsForBlockWithSplit(currentBlock); - } else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) - { - newBlock.Cmds = GetCommandsForBlockImmediatelyDominatedBySplit(currentBlock); - } else { - newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList(); - } - } - - if (assertionCount == 0) - { - return null; - } - - // Patch the edges between the new blocks - AddBlockJumps(blocks, oldToNewBlockMap); - return newBlocks; - - List GetCommandsForBlockWithSplit(Block currentBlock) - { - var newCmds = new List(); - var splitCount = -1; - var verify = splitCount == splitNumberWithinBlock; - foreach (Cmd command in currentBlock.Cmds) { - if (ShouldSplitHere(command, splitOnEveryAssert)) { - splitCount++; - verify = splitCount == splitNumberWithinBlock; - } - - if (verify && BlockTransformations.IsNonTrivialAssert(command)) - { - assertionCount++; - } - newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command)); - } - - return newCmds; - } - - List GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock) - { - var verify = true; - var newCmds = new List(); - foreach (var command in currentBlock.Cmds) { - verify = !ShouldSplitHere(command, splitOnEveryAssert) && verify; - if (verify && BlockTransformations.IsNonTrivialAssert(command)) - { - assertionCount++; - } - newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(options, command)); - } - - return newCmds; - } - } - - private static void AddBlockJumps(List oldBlocks, Dictionary oldToNewBlockMap) - { - foreach (var oldBlock in oldBlocks) { - var newBlock = oldToNewBlockMap[oldBlock]; - if (oldBlock.TransferCmd is ReturnCmd returnCmd) { - ((ReturnCmd)newBlock.TransferCmd).tok = returnCmd.tok; - continue; - } - - var gotoCmd = (GotoCmd)oldBlock.TransferCmd; - var newLabelTargets = new List(gotoCmd.LabelTargets.Count()); - var newLabelNames = new List(gotoCmd.LabelTargets.Count()); - foreach (var target in gotoCmd.LabelTargets) { - newLabelTargets.Add(oldToNewBlockMap[target]); - newLabelNames.Add(oldToNewBlockMap[target].Label); - } - - oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets); - } - } -} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/BlockRewriter.cs b/Source/VCGeneration/Splits/BlockRewriter.cs new file mode 100644 index 000000000..dc93dab28 --- /dev/null +++ b/Source/VCGeneration/Splits/BlockRewriter.cs @@ -0,0 +1,136 @@ +#nullable enable +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +using System.Linq; +using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; +using VC; + +namespace VCGeneration.Splits; + +public class BlockRewriter { + private readonly Dictionary assumedAssertions = new(); + private readonly IReadOnlyList reversedBlocks; + public List OrderedBlocks { get; } + public VCGenOptions Options { get; } + public Graph Dag { get; } + public Func, ManualSplit> CreateSplit { get; } + + public BlockRewriter(VCGenOptions options, List blocks, + Func, ManualSplit> createSplit) { + this.Options = options; + CreateSplit = createSplit; + Dag = Program.GraphFromBlocks(blocks); + OrderedBlocks = Dag.TopologicalSort(); + reversedBlocks = OrderedBlocks.Reversed(); + } + + public Cmd TransformAssertCmd(Cmd cmd) { + if (cmd is AssertCmd assertCmd) { + return assumedAssertions.GetOrCreate(assertCmd, + () => VerificationConditionGenerator.AssertTurnedIntoAssume(Options, assertCmd)); + } + + return cmd; + } + + public IEnumerable GetSplitsForIsolatedPaths(Block lastBlock, IReadOnlySet? blocksToInclude, + IToken origin) { + var blockToVisit = new Stack>(); + var newToOldBlocks = new Dictionary(); + var newLastBlock = Block.ShallowClone(lastBlock); + newLastBlock.Predecessors = lastBlock.Predecessors; + blockToVisit.Push(ImmutableStack.Create(newLastBlock)); + newToOldBlocks[newLastBlock] = lastBlock; + + while (blockToVisit.Any()) { + var path = blockToVisit.Pop(); + var firstBlock = path.Peek(); + IEnumerable predecessors = firstBlock.Predecessors; + if (blocksToInclude != null) { + predecessors = predecessors.Where(blocksToInclude.Contains); + } + + var hadPredecessors = false; + foreach (var oldPrevious in predecessors) { + hadPredecessors = true; + var newPrevious = Block.ShallowClone(oldPrevious); + newPrevious.Predecessors = oldPrevious.Predecessors; + newPrevious.Cmds = oldPrevious.Cmds.Select(TransformAssertCmd).ToList(); + + newToOldBlocks[newPrevious] = oldPrevious; + if (newPrevious.TransferCmd is GotoCmd gotoCmd) { + newPrevious.TransferCmd = + new GotoCmd(gotoCmd.tok, new List { firstBlock.Label }, new List { + firstBlock + }); + } + + blockToVisit.Push(path.Push(newPrevious)); + } + + if (!hadPredecessors) { + var filteredDag = blocksToInclude == null + ? Dag + : Program.GraphFromBlocksSubset(OrderedBlocks, blocksToInclude); + var nonDominatedBranches = path.Where(b => + !filteredDag.DominatorMap.DominatedBy(lastBlock, newToOldBlocks[b])).ToList(); + var singletonBlock = Block.ShallowClone(firstBlock); + singletonBlock.TransferCmd = new ReturnCmd(origin); + singletonBlock.Cmds = path.SelectMany(b => b.Cmds).ToList(); + yield return CreateSplit(new PathOrigin(origin, nonDominatedBranches), new List { singletonBlock }); + } + } + } + + public (List NewBlocks, Dictionary Mapping) ComputeNewBlocks( + ISet blocksToInclude, + ISet freeAssumeBlocks) { + return ComputeNewBlocks(blocksToInclude, block => + freeAssumeBlocks.Contains(block) + ? block.Cmds.Select(c => CommandTransformations.AssertIntoAssume(Options, c)).ToList() + : block.Cmds); + } + + public (List NewBlocks, Dictionary Mapping) ComputeNewBlocks( + ISet? blocksToInclude, + Func> getCommands) + { + var newBlocks = new List(); + var oldToNewBlockMap = new Dictionary(reversedBlocks.Count); + + // Traverse backwards to allow settings the jumps to the new blocks + foreach (var block in reversedBlocks) + { + if (blocksToInclude != null && !blocksToInclude.Contains(block)) { + continue; + } + + var newBlock = Block.ShallowClone(block); + newBlocks.Add(newBlock); + oldToNewBlockMap[block] = newBlock; + // freeBlocks consist of the predecessors of the relevant foci. + // Their assertions turn into assumes and any splits inside them are disabled. + newBlock.Cmds = getCommands(block); + + if (block.TransferCmd is GotoCmd gtc) + { + var targets = blocksToInclude == null ? gtc.LabelTargets : gtc.LabelTargets.Where(blocksToInclude.Contains).ToList(); + newBlock.TransferCmd = new GotoCmd(gtc.tok, + targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(), + targets.Select(blk => oldToNewBlockMap[blk]).ToList()); + } + } + newBlocks.Reverse(); + + BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); + return (newBlocks, oldToNewBlockMap); + } + + + public static bool ShouldIsolate(bool splitOnEveryAssert, QKeyValue? isolateAttribute) + { + return splitOnEveryAssert || isolateAttribute != null; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/FocusAttributeHandler.cs b/Source/VCGeneration/Splits/FocusAttributeHandler.cs new file mode 100644 index 000000000..b9d327250 --- /dev/null +++ b/Source/VCGeneration/Splits/FocusAttributeHandler.cs @@ -0,0 +1,116 @@ +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +using System.Linq; +using Microsoft.Boogie; +using VC; +using VCGeneration.Splits; +using Block = Microsoft.Boogie.Block; +using Cmd = Microsoft.Boogie.Cmd; +using PredicateCmd = Microsoft.Boogie.PredicateCmd; +using QKeyValue = Microsoft.Boogie.QKeyValue; + +namespace VCGeneration; + +public class FocusAttributeHandler { + + /// + /// Each focus block creates two options. + /// We recurse twice for each focus, leading to potentially 2^N splits + /// + public static List GetParts(VCGenOptions options, ImplementationRun run, + Func, ManualSplit> createPart) + { + var rewriter = new BlockRewriter(options, run.Implementation.Blocks, createPart); + + var implementation = run.Implementation; + var dag = rewriter.Dag; + + // By default, we process the foci in a top-down fashion, i.e., in the topological order. + // If the user sets the RelaxFocus flag, we use the reverse (topological) order. + var focusBlocks = GetFocusBlocks(rewriter.OrderedBlocks); + if (rewriter.Options.RelaxFocus) { + focusBlocks.Reverse(); + } + if (!focusBlocks.Any()) { + return new List { rewriter.CreateSplit(new ImplementationRootOrigin(run.Implementation), implementation.Blocks) }; + } + + var ancestorsPerBlock = new Dictionary>(); + var descendantsPerBlock = new Dictionary>(); + focusBlocks.ForEach(fb => { + var reachables = dag.ComputeReachability(fb.Block, false).ToHashSet(); + reachables.Remove(fb.Block); + ancestorsPerBlock[fb.Block] = reachables; + }); + focusBlocks.ForEach(fb => descendantsPerBlock[fb.Block] = dag.ComputeReachability(fb.Block).ToHashSet()); + var result = new List(); + + AddSplitsFromIndex(ImmutableStack.Empty, 0, implementation.Blocks.ToHashSet(), ImmutableHashSet.Empty); + return result; + + void AddSplitsFromIndex(ImmutableStack path, int focusIndex, ISet blocksToInclude, ISet freeAssumeBlocks) { + var allFocusBlocksHaveBeenProcessed = focusIndex == focusBlocks.Count; + if (allFocusBlocksHaveBeenProcessed) { + var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, freeAssumeBlocks); + IImplementationPartOrigin token = path.Any() + ? new PathOrigin(run.Implementation.tok, path.ToList()) // TODO fix + : new ImplementationRootOrigin(run.Implementation); + result.Add(rewriter.CreateSplit(token, newBlocks)); + } else { + var (focusBlock, nextToken) = focusBlocks[focusIndex]; // assert b in blocks + if (!blocksToInclude.Contains(focusBlock) || freeAssumeBlocks.Contains(focusBlock)) + { + // This focus block can not be reached in our current path, so we ignore it by continuing + AddSplitsFromIndex(path, focusIndex + 1, blocksToInclude, freeAssumeBlocks); + } + else + { + var dominatedBlocks = DominatedBlocks(rewriter.OrderedBlocks, focusBlock, blocksToInclude); + // Recursive call that does NOT focus the block + // Contains all blocks except the ones dominated by the focus block + AddSplitsFromIndex(path, focusIndex + 1, + blocksToInclude.Where(blk => !dominatedBlocks.Contains(blk)).ToHashSet(), freeAssumeBlocks); + var ancestors = ancestorsPerBlock[focusBlock]; + var descendants = descendantsPerBlock[focusBlock]; + + // Recursive call that does focus the block + // Contains all the ancestors, the focus block, and the descendants. + AddSplitsFromIndex(path.Push(focusBlock), focusIndex + 1, + ancestors.Union(descendants).Intersect(blocksToInclude).ToHashSet(), + ancestors.Union(freeAssumeBlocks).ToHashSet()); + } + } + } + } + + // finds all the blocks dominated by focusBlock in the subgraph + // which only contains vertices of subgraph. + private static HashSet DominatedBlocks(List topologicallySortedBlocks, Block focusBlock, ISet subgraph) + { + var dominatorsPerBlock = new Dictionary>(); + foreach (var block in topologicallySortedBlocks.Where(subgraph.Contains)) + { + var dominatorsForBlock = new HashSet(); + var predecessors = block.Predecessors.Where(subgraph.Contains).ToList(); + if (predecessors.Count != 0) + { + dominatorsForBlock.UnionWith(dominatorsPerBlock[predecessors[0]]); + predecessors.ForEach(blk => dominatorsForBlock.IntersectWith(dominatorsPerBlock[blk])); + } + dominatorsForBlock.Add(block); + dominatorsPerBlock[block] = dominatorsForBlock; + } + return subgraph.Where(blk => dominatorsPerBlock[blk].Contains(focusBlock)).ToHashSet(); + } + + private static List<(Block Block, IToken Token)> GetFocusBlocks(List blocks) { + return blocks. + Select(block => (Block: block, FocusCommand: block.Cmds.FirstOrDefault(IsFocusCmd)?.tok)). + Where(t => t.FocusCommand != null).ToList(); + } + + private static bool IsFocusCmd(Cmd c) { + return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); + } +} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs new file mode 100644 index 000000000..1d90a36e0 --- /dev/null +++ b/Source/VCGeneration/Splits/IsolateAttributeOnAssertsHandler.cs @@ -0,0 +1,106 @@ +#nullable enable +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +using System.Linq; +using Microsoft.Boogie; +using VC; +using VCGeneration.Splits; + +namespace VCGeneration; + +class IsolateAttributeOnAssertsHandler { + + public static (List IsolatedParts, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, + Func, ManualSplit> createPart) { + var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart); + + var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert; + partToDivide.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); + + var isolatedAssertions = new HashSet(); + var results = new List(); + + foreach (var b in partToDivide.Blocks) { + b.Predecessors.Clear(); + } + Implementation.ComputePredecessorsForBlocks(partToDivide.Blocks); + foreach (var block in partToDivide.Blocks) { + foreach (var assert in block.Cmds.OfType()) { + var attributes = assert.Attributes; + var isolateAttribute = QKeyValue.FindAttribute(attributes, p => p.Key == "isolate"); + if (!BlockRewriter.ShouldIsolate(splitOnEveryAssert, isolateAttribute)) { + continue; + } + + isolatedAssertions.Add(assert); + if (isolateAttribute != null && isolateAttribute.Params.OfType().Any(p => Equals(p, "paths"))) { + results.AddRange(rewriter.GetSplitsForIsolatedPaths(block, null, assert.tok).Select(p => { + var newAssertBlock = p.Blocks.Last(); + newAssertBlock.Cmds = GetCommandsForBlockWithAssert(newAssertBlock, assert); + return p; + })); + } else { + results.Add(GetSplitForIsolatedAssertion(block, assert)); + } + } + } + + if (!results.Any()) { + return (results,partToDivide); + } + + return (results,GetSplitWithoutIsolatedAssertions()); + + ManualSplit GetSplitForIsolatedAssertion(Block blockWithAssert, AssertCmd assertCmd) { + var blocksToKeep = rewriter.Dag.ComputeReachability(blockWithAssert, false); + + List GetCommands(Block oldBlock) => + oldBlock == blockWithAssert + ? GetCommandsForBlockWithAssert(oldBlock, assertCmd) + : oldBlock.Cmds.Select(rewriter.TransformAssertCmd).ToList(); + + var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToKeep, GetCommands); + return rewriter.CreateSplit(new IsolatedAssertionOrigin(assertCmd), newBlocks); + } + + List GetCommandsForBlockWithAssert(Block currentBlock, AssertCmd assert) + { + var result = new List(); + foreach (var command in currentBlock.Cmds) { + if (assert == command) { + result.Add(command); + break; + } + result.Add(rewriter.TransformAssertCmd(command)); + } + + return result; + } + + ManualSplit GetSplitWithoutIsolatedAssertions() { + var origin = new ImplementationRootOrigin(partToDivide.Implementation); + if (!isolatedAssertions.Any()) { + return rewriter.CreateSplit(origin, partToDivide.Blocks); + } + + var (newBlocks, mapping) = rewriter.ComputeNewBlocks(null, GetCommands); + + return rewriter.CreateSplit(origin, newBlocks); + + List GetCommands(Block block) => block.Cmds.Select(cmd => + isolatedAssertions.Contains(cmd) ? rewriter.TransformAssertCmd(cmd) : cmd).ToList(); + } + } +} + + +public class IsolatedAssertionOrigin : TokenWrapper, IImplementationPartOrigin { + public AssertCmd IsolatedAssert { get; } + + public IsolatedAssertionOrigin(AssertCmd isolatedAssert) : base(isolatedAssert.tok) { + this.IsolatedAssert = isolatedAssert; + } + + public string ShortName => $"/assert@{IsolatedAssert.Line}"; +} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs new file mode 100644 index 000000000..5f7c1de04 --- /dev/null +++ b/Source/VCGeneration/Splits/IsolateAttributeOnJumpsHandler.cs @@ -0,0 +1,87 @@ +#nullable enable +using System; +using System.Collections.Generic; +using System.Collections.Immutable; +using System.Diagnostics; +using System.Linq; +using Microsoft.Boogie; +using VC; +using VCGeneration.Splits; +using VCGeneration.Transformations; + +namespace VCGeneration; + +class IsolateAttributeOnJumpsHandler { + public static (List Isolated, ManualSplit Remainder) GetParts(VCGenOptions options, ManualSplit partToDivide, + Func, ManualSplit> createPart) { + + var rewriter = new BlockRewriter(options, partToDivide.Blocks, createPart); + + var results = new List(); + var blocks = partToDivide.Blocks; + var dag = Program.GraphFromBlocks(blocks); + + var splitOnEveryAssert = partToDivide.Options.VcsSplitOnEveryAssert; + partToDivide.Run.Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); + + var isolatedBlocks = new HashSet(); + + foreach (var block in partToDivide.Blocks) { + if (block.TransferCmd is not GotoCmd gotoCmd) { + continue; + } + + var isTypeOfAssert = gotoCmd.tok is GotoFromReturn; + var isolateAttribute = QKeyValue.FindAttribute(gotoCmd.Attributes, p => p.Key == "isolate"); + var isolate = BlockRewriter.ShouldIsolate(isTypeOfAssert && splitOnEveryAssert, isolateAttribute); + if (!isolate) { + continue; + } + + isolatedBlocks.Add(block); + var ancestors = dag.ComputeReachability(block, false); + var descendants = dag.ComputeReachability(block, true); + var blocksToInclude = ancestors.Union(descendants).ToHashSet(); + + var originalReturn = ((GotoFromReturn)gotoCmd.tok).Origin; + if (isolateAttribute != null && isolateAttribute.Params.OfType().Any(p => Equals(p, "paths"))) { + // These conditions hold if the goto was originally a return + Debug.Assert(gotoCmd.LabelTargets.Count == 1); + Debug.Assert(gotoCmd.LabelTargets[0].TransferCmd is not GotoCmd); + results.AddRange(rewriter.GetSplitsForIsolatedPaths(gotoCmd.LabelTargets[0], blocksToInclude, originalReturn.tok)); + } else { + var (newBlocks, _) = rewriter.ComputeNewBlocks(blocksToInclude, ancestors.ToHashSet()); + results.Add(rewriter.CreateSplit(new ReturnOrigin(originalReturn), newBlocks)); + } + } + + if (!results.Any()) { + return (results,partToDivide); + } + + return (results, GetPartWithoutIsolatedReturns()); + + ManualSplit GetPartWithoutIsolatedReturns() { + var (newBlocks, mapping) = rewriter.ComputeNewBlocks(blocks.ToHashSet(), new HashSet()); + foreach (var (oldBlock, newBlock) in mapping) { + if (isolatedBlocks.Contains(oldBlock)) { + newBlock.TransferCmd = new ReturnCmd(Token.NoToken); + } + } + BlockTransformations.DeleteBlocksNotLeadingToAssertions(newBlocks); + return rewriter.CreateSplit(new ImplementationRootOrigin(partToDivide.Implementation), + newBlocks); + } + } +} + + +public class ReturnOrigin : TokenWrapper, IImplementationPartOrigin { + public ReturnCmd IsolatedReturn { get; } + + public ReturnOrigin(ReturnCmd isolatedReturn) : base(isolatedReturn.tok) { + this.IsolatedReturn = isolatedReturn; + } + + public string ShortName => $"/return@{IsolatedReturn.Line}"; +} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/ManualSplitFinder.cs b/Source/VCGeneration/Splits/ManualSplitFinder.cs new file mode 100644 index 000000000..4b553b055 --- /dev/null +++ b/Source/VCGeneration/Splits/ManualSplitFinder.cs @@ -0,0 +1,32 @@ +#nullable enable +using System; +using System.Collections.Generic; +using System.Linq; +using Microsoft.Boogie; +using VC; + +namespace VCGeneration; + + +public static class ManualSplitFinder { + + public static IEnumerable GetParts(VCGenOptions options, ImplementationRun run, + Func, ManualSplit> createPart) { + + var focussedParts = FocusAttributeHandler.GetParts(options, run, createPart); + var result = focussedParts.SelectMany(focussedPart => { + var (isolatedJumps, withoutIsolatedJumps) = + IsolateAttributeOnJumpsHandler.GetParts(options, focussedPart, createPart); + var (isolatedAssertions, withoutIsolatedAssertions) = + IsolateAttributeOnAssertsHandler.GetParts(options, withoutIsolatedJumps, createPart); + + var splitParts = SplitAttributeHandler.GetParts(withoutIsolatedAssertions); + return isolatedJumps.Concat(isolatedAssertions).Concat(splitParts); + }); + return result; + } +} + +public interface IImplementationPartOrigin : IToken { + string ShortName { get; } +} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/PathToken.cs b/Source/VCGeneration/Splits/PathToken.cs new file mode 100644 index 000000000..b0dabe1cd --- /dev/null +++ b/Source/VCGeneration/Splits/PathToken.cs @@ -0,0 +1,27 @@ +#nullable enable +using System.Collections.Generic; +using System.Collections.Immutable; +using System.IO; +using System.Linq; +using Microsoft.Boogie; +using Microsoft.Boogie.GraphUtil; + +namespace VCGeneration; + +public class PathOrigin : TokenWrapper, IImplementationPartOrigin { + + public PathOrigin(IToken inner, List branches) : base(inner) { + Branches = branches; + } + + public List Branches { get; } + public string ShortName => $"/assert@{line}[{string.Join(",", Branches.Select(b => b.tok.line))}]"; +} + +class ImplementationRootOrigin : TokenWrapper, IImplementationPartOrigin { + public ImplementationRootOrigin(Implementation implementation) : base(implementation.tok) + { + } + + public string ShortName => ""; +} \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Splits/Split.cs similarity index 96% rename from Source/VCGeneration/Split.cs rename to Source/VCGeneration/Splits/Split.cs index fc5ff9473..5d31404f0 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Splits/Split.cs @@ -10,6 +10,7 @@ using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; using System.Threading.Tasks; +using VCGeneration; namespace VC { @@ -55,8 +56,6 @@ public IReadOnlyList PrunedDeclarations { int assertionCount; double assertionCost; // without multiplication by paths - public Dictionary GotoCmdOrigins { get; } - public readonly VerificationConditionGenerator /*!*/ parent; @@ -76,14 +75,11 @@ public readonly VerificationConditionGenerator /*!*/ public VerificationConditionGenerator.ErrorReporter reporter; public Split(VCGenOptions options, Func> /*!*/ getBlocks, - Dictionary /*!*/ gotoCmdOrigins, - VerificationConditionGenerator /*!*/ par, ImplementationRun run, int? randomSeed = null) + VerificationConditionGenerator /*!*/ parent, ImplementationRun run, int? randomSeed = null) { - Contract.Requires(gotoCmdOrigins != null); - Contract.Requires(par != null); + Contract.Requires(parent != null); this.getBlocks = getBlocks; - this.GotoCmdOrigins = gotoCmdOrigins; - parent = par; + this.parent = parent; this.Run = run; this.Options = options; Interlocked.Increment(ref currentId); @@ -91,17 +87,26 @@ public Split(VCGenOptions options, Func> /*!*/ getBlocks, RandomSeed = randomSeed ?? Implementation.RandomSeed ?? Options.RandomSeed ?? 0; randomGen = new Random(RandomSeed); } - - public void PrintSplit() { + + private void PrintSplit() { if (Options.PrintSplitFile == null) { return; } + + var printToConsole = Options.PrintSplitFile == "-"; + if (printToConsole) { + Thread.Sleep(100); + } - using var writer = new TokenTextWriter( - $"{Options.PrintSplitFile}-{Util.EscapeFilename(Implementation.Name)}-{SplitIndex}.spl", false, - Options.PrettyPrint, Options); + var prefix = this is ManualSplit manualSplit ? manualSplit.Token.ShortName : ""; + var name = Implementation.Name + prefix; + using var writer = printToConsole + ? new TokenTextWriter("", Options.OutputWriter, false, Options.PrettyPrint, Options) + : new TokenTextWriter( + $"{Options.PrintSplitFile}-{Util.EscapeFilename(name)}.spl", false, + Options.PrettyPrint, Options); - Implementation.EmitImplementation(writer, 0, Blocks, false); + Implementation.EmitImplementation(writer, 0, Blocks, false, prefix); PrintSplitDeclarations(writer); } @@ -654,7 +659,6 @@ private Split DoSplit() copies.Clear(); CloneBlock(Blocks[0]); var newBlocks = new List(); - var newGotoCmdOrigins = new Dictionary(); foreach (var block in Blocks) { Contract.Assert(block != null); @@ -664,10 +668,6 @@ private Split DoSplit() } newBlocks.Add(cce.NonNull(tmp)); - if (GotoCmdOrigins.TryGetValue(block.TransferCmd, out var origin)) - { - newGotoCmdOrigins[tmp.TransferCmd] = origin; - } foreach (var predecessor in block.Predecessors) { @@ -679,7 +679,7 @@ private Split DoSplit() } } - return new Split(Options, () => newBlocks, newGotoCmdOrigins, parent, Run); + return new Split(Options, () => newBlocks, parent, Run); } private Split SplitAt(int idx) @@ -949,7 +949,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0])))); vc = exprGen.Implies(eqExpr, vc); - reporter = new VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, + reporter = new VerificationConditionGenerator.ErrorReporter(Options, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, mvInfo, checker.TheoremProver.Context, parent.program, this); } diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs similarity index 97% rename from Source/VCGeneration/SplitAndVerifyWorker.cs rename to Source/VCGeneration/Splits/SplitAndVerifyWorker.cs index a42723458..57f3bfb33 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/Splits/SplitAndVerifyWorker.cs @@ -39,8 +39,7 @@ public SplitAndVerifyWorker( Program program, VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, - ImplementationRun run, - Dictionary gotoCmdOrigins, + ImplementationRun run, VerifierCallback callback, ModelViewInfo mvInfo, VcOutcome vcOutcome) @@ -66,7 +65,8 @@ public SplitAndVerifyWorker( ResetPredecessors(Implementation.Blocks); - ManualSplits = ManualSplitFinder.FocusAndSplit(program, options, run, gotoCmdOrigins, verificationConditionGenerator).ToList(); + ManualSplits = ManualSplitFinder.GetParts(options, run, + (token, blocks) => new ManualSplit(options, () => blocks, verificationConditionGenerator, run, token)).ToList(); if (ManualSplits.Count == 1 && maxSplits > 1) { diff --git a/Source/VCGeneration/Splits/SplitAttributeHandler.cs b/Source/VCGeneration/Splits/SplitAttributeHandler.cs new file mode 100644 index 000000000..4e145da9d --- /dev/null +++ b/Source/VCGeneration/Splits/SplitAttributeHandler.cs @@ -0,0 +1,216 @@ +#nullable enable +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; +using VC; + +namespace VCGeneration; + +class SplitAttributeHandler { + + public static List GetParts(ManualSplit partToSplit) { + var splitsPerBlock = new Dictionary>(); + var splits = new HashSet(); + foreach (var block in partToSplit.Blocks) { + var splitsForThisBlock = new List(); + foreach (var command in block.Cmds) { + if (!ShouldSplitHere(command)) { + continue; + } + + splits.Add(command); + splitsForThisBlock.Add(command); + } + + if (splitsForThisBlock.Any()) { + splitsPerBlock[block] = splitsForThisBlock; + } + } + + if (!splits.Any()) { + return new List { partToSplit }; + } + + var vcs = new List(); + var entryPoint = partToSplit.Blocks[0]; + var blockStartToSplit = GetMapFromBlockStartToSplit(partToSplit.Blocks, splitsPerBlock); + + var beforeSplitsVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, blockStartToSplit, + entryPoint, splits, null); + if (beforeSplitsVc != null) + { + vcs.Add(beforeSplitsVc); + } + foreach (var block in partToSplit.Blocks) { + var splitsForBlock = splitsPerBlock.GetValueOrDefault(block); + if (splitsForBlock == null) { + continue; + } + + foreach (var split in splitsForBlock) + { + var splitVc = GetImplementationPartAfterSplit(CreateVc, partToSplit, + blockStartToSplit, block, splits, split); + if (splitVc != null) + { + vcs.Add(splitVc); + } + } + } + return vcs; + + ManualSplit CreateVc(IImplementationPartOrigin token, List blocks) { + return new ManualSplit(partToSplit.Options, () => { + BlockTransformations.Optimize(blocks); + return blocks; + }, partToSplit.parent, partToSplit.Run, token); + } + } + + private static bool ShouldSplitHere(Cmd c) { + if (c is not PredicateCmd predicateCmd) { + return false; + } + + return QKeyValue.FindBoolAttribute(predicateCmd.Attributes, "split_here"); + } + + private static Dictionary GetMapFromBlockStartToSplit(List blocks, Dictionary> splitsPerBlock) { + var todo = new Stack(); + var blockAssignments = new Dictionary(); + var immediateDominators = Program.GraphFromBlocks(blocks).ImmediateDominator(); + todo.Push(blocks[0]); + while (todo.Count > 0) { + var currentBlock = todo.Pop(); + if (blockAssignments.Keys.Contains(currentBlock)) { + continue; + } + + if (!immediateDominators.TryGetValue(currentBlock, out var immediateDominator)) + { + blockAssignments[currentBlock] = null; + } + else if (splitsPerBlock.TryGetValue(immediateDominator, out var splitsForDominator)) // if the currentBlock's dominator has a split then it will be associated with that split + { + blockAssignments[currentBlock] = splitsForDominator.Last(); + } + else { + Contract.Assert(blockAssignments.Keys.Contains(immediateDominator)); + blockAssignments[currentBlock] = blockAssignments[immediateDominator]; + } + + if (currentBlock.TransferCmd is GotoCmd gotoCmd) { + gotoCmd.LabelTargets.ForEach(block => todo.Push(block)); + } + } + return blockAssignments; + } + + private static ManualSplit? GetImplementationPartAfterSplit(Func, ManualSplit> createVc, + ManualSplit partToSplit, + Dictionary blockStartToSplit, Block blockWithSplit, + HashSet splits, Cmd? split) + { + var assertionCount = 0; + + var newBlocks = UpdateBlocks(partToSplit.Blocks, currentBlock => { + if (currentBlock == blockWithSplit) { + return GetCommandsForBlockWithSplit(currentBlock); + } + + if (blockStartToSplit[currentBlock] == split) { + return GetCommandsForBlockImmediatelyDominatedBySplit(currentBlock); + } + + return currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(partToSplit.Options, x)).ToList(); + }); + + if (assertionCount == 0) { + return null; + } + + return createVc(new SplitOrigin(split?.tok ?? partToSplit.Token), newBlocks); + + List GetCommandsForBlockImmediatelyDominatedBySplit(Block currentBlock) + { + var verify = true; + var newCmds = new List(); + foreach (var command in currentBlock.Cmds) { + verify &= !splits.Contains(command); + if (verify && BlockTransformations.IsNonTrivialAssert(command)) + { + assertionCount++; + } + newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(partToSplit.Options, command)); + } + + return newCmds; + } + + List GetCommandsForBlockWithSplit(Block currentBlock) + { + var newCmds = new List(); + var verify = false; + foreach (var command in currentBlock.Cmds) { + if (splits.Contains(command)) { + verify = command == split; + } + + if (verify && BlockTransformations.IsNonTrivialAssert(command)) + { + assertionCount++; + } + newCmds.Add(verify ? command : CommandTransformations.AssertIntoAssume(partToSplit.Options, command)); + } + + return newCmds; + } + } + + private static List UpdateBlocks(IReadOnlyList blocks, + Func> getCommands) + { + var newBlocks = new List(blocks.Count); + var oldToNewBlockMap = new Dictionary(newBlocks.Count); + foreach (var currentBlock in blocks) { + var newBlock = Block.ShallowClone(currentBlock); + + oldToNewBlockMap[currentBlock] = newBlock; + newBlocks.Add(newBlock); + newBlock.Cmds = getCommands(currentBlock); + } + + AddJumpsToNewBlocks(oldToNewBlockMap); + return newBlocks; + } + + private static void AddJumpsToNewBlocks(Dictionary oldToNewBlockMap) + { + foreach (var (oldBlock, newBlock) in oldToNewBlockMap) { + if (oldBlock.TransferCmd is ReturnCmd returnCmd) { + ((ReturnCmd)newBlock.TransferCmd).tok = returnCmd.tok; + continue; + } + + var gotoCmd = (GotoCmd)oldBlock.TransferCmd; + var newLabelTargets = new List(gotoCmd.LabelTargets.Count); + var newLabelNames = new List(gotoCmd.LabelTargets.Count); + foreach (var target in gotoCmd.LabelTargets) { + newLabelTargets.Add(oldToNewBlockMap[target]); + newLabelNames.Add(oldToNewBlockMap[target].Label); + } + + oldToNewBlockMap[oldBlock].TransferCmd = new GotoCmd(gotoCmd.tok, newLabelNames, newLabelTargets); + } + } +} + +class SplitOrigin : TokenWrapper, IImplementationPartOrigin { + public SplitOrigin(IToken inner) : base(inner) + { + } + + public string ShortName => $"/split@{line}"; +} \ No newline at end of file diff --git a/Source/VCGeneration/Splits/TokenWrapper.cs b/Source/VCGeneration/Splits/TokenWrapper.cs new file mode 100644 index 000000000..d7ea8427d --- /dev/null +++ b/Source/VCGeneration/Splits/TokenWrapper.cs @@ -0,0 +1,48 @@ +#nullable enable +using Microsoft.Boogie; + +namespace VCGeneration; + +public class TokenWrapper : IToken { + public IToken Inner { get; } + + public TokenWrapper(IToken inner) { + this.Inner = inner; + } + + public int CompareTo(IToken? other) { + return Inner.CompareTo(other); + } + + public int kind { + get => Inner.kind; + set => Inner.kind = value; + } + + public string filename { + get => Inner.filename; + set => Inner.filename = value; + } + + public int pos { + get => Inner.pos; + set => Inner.pos = value; + } + + public int col { + get => Inner.col; + set => Inner.col = value; + } + + public int line { + get => Inner.line; + set => Inner.line = value; + } + + public string val { + get => Inner.val; + set => Inner.val = value; + } + + public bool IsValid => Inner.IsValid; +} \ No newline at end of file diff --git a/Source/VCGeneration/Transformations/DesugarReturns.cs b/Source/VCGeneration/Transformations/DesugarReturns.cs index 4362273a6..90ab89089 100644 --- a/Source/VCGeneration/Transformations/DesugarReturns.cs +++ b/Source/VCGeneration/Transformations/DesugarReturns.cs @@ -1,84 +1,70 @@ using System; using System.Collections.Generic; using System.Diagnostics.Contracts; +using System.Linq; using Microsoft.Boogie; using VC; namespace VCGeneration.Transformations; public static class DesugarReturns { - public static Block GenerateUnifiedExit(Implementation impl, out Dictionary gotoCmdOrigins) - { - Contract.Requires(impl != null); - Contract.Requires(gotoCmdOrigins != null); - Contract.Ensures(Contract.Result() != null); - - gotoCmdOrigins = new(); - Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); - Block exitBlock = null; + public static Block GenerateUnifiedExit(Implementation impl) + { + Contract.Requires(impl != null); + Contract.Ensures(Contract.Result() != null); - #region Create a unified exit block, if there's more than one + Contract.Ensures(Contract.Result().TransferCmd is ReturnCmd); + Block exitBlock = null; - { - int returnBlocks = 0; - foreach (Block b in impl.Blocks) - { - if (b.TransferCmd is ReturnCmd) - { - exitBlock = b; - returnBlocks++; - } - } - - if (returnBlocks > 1) - { - string unifiedExitLabel = "GeneratedUnifiedExit"; - var unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List(), - new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); - Contract.Assert(unifiedExit != null); - foreach (Block b in impl.Blocks) - { - if (b.TransferCmd is ReturnCmd returnCmd) - { - List labels = new List(); - labels.Add(unifiedExitLabel); - List bs = new List(); - bs.Add(unifiedExit); - GotoCmd go = new GotoCmd(returnCmd.tok, labels, bs); - gotoCmdOrigins[go] = returnCmd; - b.TransferCmd = go; - unifiedExit.Predecessors.Add(b); - } - } + int returnBlocks = 0; + foreach (var block in impl.Blocks.Where(block => block.TransferCmd is ReturnCmd)) + { + exitBlock = block; + returnBlocks++; + } - exitBlock = unifiedExit; - impl.Blocks.Add(unifiedExit); + if (returnBlocks > 1) + { + string unifiedExitLabel = "GeneratedUnifiedExit"; + var unifiedExit = new Block(Token.NoToken, unifiedExitLabel, new List(), + new ReturnCmd(impl.StructuredStmts != null ? impl.StructuredStmts.EndCurly : Token.NoToken)); + Contract.Assert(unifiedExit != null); + foreach (var block in impl.Blocks) { + if (block.TransferCmd is not ReturnCmd returnCmd) { + continue; } - Contract.Assert(exitBlock != null); + var gotoLabels = new List { unifiedExitLabel }; + var gotoTargets = new List { unifiedExit }; + var gotoCmd = new GotoCmd(new GotoFromReturn(returnCmd), gotoLabels, gotoTargets) { + Attributes = returnCmd.Attributes + }; + block.TransferCmd = gotoCmd; + unifiedExit.Predecessors.Add(block); } - return exitBlock; - #endregion + exitBlock = unifiedExit; + impl.Blocks.Add(unifiedExit); } - - /// - /// Modifies an implementation by inserting all postconditions - /// as assert statements at the end of the implementation - /// Returns the possibly-new unified exit block of the implementation - /// - /// - /// The unified exit block that has - /// already been constructed for the implementation (and so - /// is already an element of impl.Blocks) - /// - public static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock, - Dictionary gotoCmdOrigins) + + Contract.Assert(exitBlock != null); + return exitBlock; + } + + /// + /// Modifies an implementation by inserting all postconditions + /// as assert statements at the end of the implementation + /// Returns the possibly-new unified exit block of the implementation + /// + /// The unified exit block that has + /// already been constructed for the implementation (and so + /// is already an element of impl.Blocks) + /// + public static void InjectPostConditions(VCGenOptions options, ImplementationRun run, Block unifiedExitBlock) { var impl = run.Implementation; Contract.Requires(impl != null); Contract.Requires(unifiedExitBlock != null); - Contract.Requires(gotoCmdOrigins != null); Contract.Requires(impl.Proc != null); Contract.Requires(unifiedExitBlock.TransferCmd is ReturnCmd); @@ -89,7 +75,7 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun debugWriter.WriteLine("Effective postcondition:"); } - Substitution formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); + var formalProcImplSubst = Substituter.SubstitutionFromDictionary(impl.GetImplFormalMap(options)); // (free and checked) ensures clauses foreach (Ensures ens in impl.Proc.Ensures) @@ -98,18 +84,18 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun if (!ens.Free) { - Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition); - Ensures ensCopy = (Ensures) cce.NonNull(ens.Clone()); - ensCopy.Condition = e; - AssertEnsuresCmd c = new AssertEnsuresCmd(ensCopy); - c.ErrorDataEnhanced = ensCopy.ErrorDataEnhanced; + var ensuresCopy = (Ensures) cce.NonNull(ens.Clone()); + ensuresCopy.Condition = Substituter.Apply(formalProcImplSubst, ens.Condition); + AssertEnsuresCmd assert = new AssertEnsuresCmd(ensuresCopy) { + ErrorDataEnhanced = ensuresCopy.ErrorDataEnhanced + }; // Copy any {:id ...} from the postcondition to the assumption, so // we can track it while analyzing verification coverage. - c.CopyIdFrom(ens.tok, ens); - unifiedExitBlock.Cmds.Add(c); + assert.CopyIdFrom(ens.tok, ens); + unifiedExitBlock.Cmds.Add(assert); if (debugWriter != null) { - c.Emit(debugWriter, 1); + assert.Emit(debugWriter, 1); } } else if (ens.CanAlwaysAssume()) @@ -128,4 +114,12 @@ public static void InjectPostConditions(VCGenOptions options, ImplementationRun debugWriter.WriteLine(); } } +} + +class GotoFromReturn : TokenWrapper { + public ReturnCmd Origin { get; } + + public GotoFromReturn(ReturnCmd origin) : base(origin.tok) { + this.Origin = origin; + } } \ No newline at end of file diff --git a/Source/VCGeneration/Transformations/RemoveBackEdges.cs b/Source/VCGeneration/Transformations/RemoveBackEdges.cs index 731f7a1e5..f9233af03 100644 --- a/Source/VCGeneration/Transformations/RemoveBackEdges.cs +++ b/Source/VCGeneration/Transformations/RemoveBackEdges.cs @@ -9,7 +9,7 @@ namespace VCGeneration.Transformations; public class RemoveBackEdges { - private VerificationConditionGenerator generator; + private readonly VerificationConditionGenerator generator; public RemoveBackEdges(VerificationConditionGenerator generator) { this.generator = generator; @@ -48,7 +48,7 @@ public void ConvertCfg2Dag(ImplementationRun run, Dictionary> // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges // below assumes that the start node has no predecessor) impl.Blocks.Insert(0, - new Block(new Token(-17, -4), "0", new List(), + new Block(Token.NoToken, "0", new List(), new GotoCmd(Token.NoToken, new List { impl.Blocks[0].Label }, new List { impl.Blocks[0] }))); ConditionGeneration.ResetPredecessors(impl.Blocks); @@ -206,14 +206,7 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary GotoCmdOrigins { get; set; } public ModelViewInfo ModelViewInfo { get; set; } } @@ -114,7 +113,7 @@ public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, List gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(traceWriter, codeExpr.Blocks, + vcgen.ConvertBlocks2PassiveCmd(traceWriter, codeExpr.Blocks, new List(), new ModelViewInfo(codeExpr), debugInfos); VCExpr startCorrect = vcgen.LetVC(codeExpr.Blocks, null, absyIds, ctx, out var ac, isPositiveContext); VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect); @@ -380,7 +379,7 @@ public override async Task VerifyImplementation(ImplementationRun run callback.OnProgress?.Invoke("VCgen", 0, 0, 0.0); - PrepareImplementation(run, callback, out var smokeTester, out var dataGotoCmdOrigins, out var dataModelViewInfo); + PrepareImplementation(run, callback, out var smokeTester, out var dataModelViewInfo); VcOutcome vcOutcome = VcOutcome.Correct; @@ -400,15 +399,14 @@ public override async Task VerifyImplementation(ImplementationRun run else { // If possible, we use the old counterexample, but with the location information of "a" - var cex = AssertCmdToCloneCounterexample(CheckerPool.Options, a, oldCex, impl.Blocks[0], - dataGotoCmdOrigins); + var cex = AssertCmdToCloneCounterexample(CheckerPool.Options, a, oldCex, impl.Blocks[0]); callback.OnCounterexample(cex, null); } } } } - var worker = new SplitAndVerifyWorker(program, Options, this, run, dataGotoCmdOrigins, callback, + var worker = new SplitAndVerifyWorker(program, Options, this, run, callback, dataModelViewInfo, vcOutcome); vcOutcome = await worker.WorkUntilDone(cancellationToken); @@ -427,7 +425,6 @@ public override async Task VerifyImplementation(ImplementationRun run public void PrepareImplementation(ImplementationRun run, VerifierCallback callback, out SmokeTester smokeTester, - out Dictionary gotoCmdOrigins, out ModelViewInfo modelViewInfo) { var data = implementationData.GetOrCreateValue(run.Implementation)!; @@ -447,7 +444,7 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba if (!data.Passified) { data.Passified = true; - data.GotoCmdOrigins = gotoCmdOrigins = PassifyImpl(run, out modelViewInfo); + PassifyImpl(run, out modelViewInfo); data.ModelViewInfo = modelViewInfo; ExpandAsserts(run.Implementation); @@ -466,7 +463,6 @@ public void PrepareImplementation(ImplementationRun run, VerifierCallback callba else { modelViewInfo = data.ModelViewInfo; - gotoCmdOrigins = data.GotoCmdOrigins; } } @@ -475,7 +471,6 @@ public class ErrorReporter : ProverInterface.ErrorHandler { private ProofRun split; private new VCGenOptions options; - Dictionary gotoCmdOrigins; ControlFlowIdMap absyIds; @@ -491,7 +486,6 @@ public class ErrorReporter : ProverInterface.ErrorHandler [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(gotoCmdOrigins != null); Contract.Invariant(absyIds != null); Contract.Invariant(cce.NonNullElements(blocks)); Contract.Invariant(callback != null); @@ -510,7 +504,6 @@ public override void AddCoveredElement(TrackedNodeComponent elt) } public ErrorReporter(VCGenOptions options, - Dictionary /*!*/ gotoCmdOrigins, ControlFlowIdMap /*!*/ absyIds, List /*!*/ blocks, Dictionary> debugInfos, @@ -519,13 +512,11 @@ public ErrorReporter(VCGenOptions options, ProverContext /*!*/ context, Program /*!*/ program, ProofRun split) : base(options) { - Contract.Requires(gotoCmdOrigins != null); Contract.Requires(absyIds != null); Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(callback != null); Contract.Requires(context != null); Contract.Requires(program != null); - this.gotoCmdOrigins = gotoCmdOrigins; this.absyIds = absyIds; this.blocks = blocks; this.debugInfos = debugInfos; @@ -568,7 +559,7 @@ public override void OnModel(IList labels /*!*/ /*!*/, Model model, Contract.Assert(traceNodes.Contains(entryBlock)); trace.Add(entryBlock); - Counterexample newCounterexample = TraceCounterexample(options, entryBlock, traceNodes, trace, model, MvInfo, + var newCounterexample = TraceCounterexample(options, entryBlock, traceNodes, trace, model, MvInfo, debugInfos, context, split, new Dictionary()); if (newCounterexample == null) @@ -580,15 +571,12 @@ public override void OnModel(IList labels /*!*/ /*!*/, Model model, if (newCounterexample is ReturnCounterexample returnExample) { - foreach (var block in returnExample.Trace) + foreach (var b in returnExample.Trace) { - Contract.Assert(block != null); - Contract.Assume(block.TransferCmd != null); - var cmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); - if (cmd != null) - { - returnExample.FailingReturn = cmd; - break; + Contract.Assert(b != null); + Contract.Assume(b.TransferCmd != null); + if (b.TransferCmd.tok is GotoFromReturn gotoFromReturn) { + returnExample.FailingReturn = gotoFromReturn.Origin; } } } @@ -660,14 +648,14 @@ public void DesugarCalls(Implementation impl) } } - public Dictionary PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) + public void PassifyImpl(ImplementationRun run, out ModelViewInfo modelViewInfo) { Contract.Requires(run != null); Contract.Requires(program != null); Contract.Ensures(Contract.Result>() != null); var impl = run.Implementation; - var exitBlock = DesugarReturns.GenerateUnifiedExit(impl, out var gotoCmdOrigins); + var exitBlock = DesugarReturns.GenerateUnifiedExit(impl); #region Debug Tracing @@ -706,7 +694,7 @@ public Dictionary PassifyImpl(ImplementationRun run, out if (lvar.TypedIdent.WhereExpr != null) { var exp = Expr.Binary(lvar.tok, BinaryOperator.Opcode.And, lvar.TypedIdent.WhereExpr, - LiteralExpr.Literal(true)); + Expr.Literal(true)); Cmd c = new AssumeCmd(lvar.tok, exp, new QKeyValue(lvar.tok, "where", new List(new object[] { idExp }), null)); cc.Add(c); @@ -722,7 +710,7 @@ public Dictionary PassifyImpl(ImplementationRun run, out InjectPreconditions(Options, run, cc); // append postconditions, starting in exitBlock and continuing into other blocks, if needed - DesugarReturns.InjectPostConditions(Options, run, exitBlock, gotoCmdOrigins); + DesugarReturns.InjectPostConditions(Options, run, exitBlock); } #endregion @@ -796,8 +784,6 @@ public Dictionary PassifyImpl(ImplementationRun run, out #endregion Peep-hole optimizations HandleSelectiveChecking(impl); - - return gotoCmdOrigins; } #region Simplified May-Unverified Analysis and Instrumentation @@ -1367,12 +1353,11 @@ public static Counterexample AssertCmdToCounterexample(VCGenOptions options, Ass /// public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options, AssertCmd assert, Counterexample cex, - Block implEntryBlock, Dictionary gotoCmdOrigins) + Block implEntryBlock) { Contract.Requires(assert != null); Contract.Requires(cex != null); Contract.Requires(implEntryBlock != null); - Contract.Requires(gotoCmdOrigins != null); Contract.Ensures(Contract.Result() != null); Counterexample cc; @@ -1445,7 +1430,7 @@ public static Counterexample AssertCmdToCloneCounterexample(VCGenOptions options { Contract.Assert(block != null); Contract.Assume(block.TransferCmd != null); - returnCmd = gotoCmdOrigins.GetValueOrDefault(block.TransferCmd); + returnCmd = block.TransferCmd.tok is GotoFromReturn gotoFromReturn ? gotoFromReturn.Origin : null; if (returnCmd != null) { break; diff --git a/Source/VCGeneration/VerificationRunResult.cs b/Source/VCGeneration/VerificationRunResult.cs index 9f48dc5a1..0ddcd0baa 100644 --- a/Source/VCGeneration/VerificationRunResult.cs +++ b/Source/VCGeneration/VerificationRunResult.cs @@ -27,17 +27,9 @@ public void ComputePerAssertOutcomes(out Dictionary pe if (Outcome == SolverOutcome.Valid) { perAssertOutcome = Asserts.ToDictionary(cmd => cmd, _ => SolverOutcome.Valid); } else { - foreach (var counterExample in CounterExamples) { - AssertCmd underlyingAssert; - if (counterExample is AssertCounterexample assertCounterexample) { - underlyingAssert = assertCounterexample.FailingAssert; - } else if (counterExample is CallCounterexample callCounterexample) { - underlyingAssert = callCounterexample.FailingFailingAssert; - } else if (counterExample is ReturnCounterexample returnCounterexample) { - underlyingAssert = returnCounterexample.FailingFailingAssert; - } else { - continue; - } + foreach (var counterExample in CounterExamples) + { + var underlyingAssert = counterExample.FailingAssert; // We ensure that the underlyingAssert is among the original asserts if (!Asserts.Contains(underlyingAssert)) { diff --git a/Test/aitest0/Issue25.bpl b/Test/aitest0/Issue25.bpl index 28481b41e..7f04782a6 100644 --- a/Test/aitest0/Issue25.bpl +++ b/Test/aitest0/Issue25.bpl @@ -7,8 +7,8 @@ axiom 0 <= N; procedure vacuous_post() ensures (forall k, l: int :: 0 <= k && k <= l && l < N ==> N < N); // Used to verify at some point (see https://github.com/boogie-org/boogie/issues/25). { -var x: int; -x := -N; -while (x != x) { -} + var x: int; + x := -N; + while (x != x) { + } } diff --git a/Test/aitest0/Issue25.bpl.expect b/Test/aitest0/Issue25.bpl.expect index de1be84d4..650e46069 100644 --- a/Test/aitest0/Issue25.bpl.expect +++ b/Test/aitest0/Issue25.bpl.expect @@ -1,8 +1,8 @@ -Issue25.bpl(12,1): Error: a postcondition could not be proved on this return path +Issue25.bpl(12,3): Error: a postcondition could not be proved on this return path Issue25.bpl(8,1): Related location: this is the postcondition that could not be proved Execution trace: - Issue25.bpl(11,3): anon0 - Issue25.bpl(12,1): anon2_LoopHead - Issue25.bpl(12,1): anon2_LoopDone + Issue25.bpl(11,5): anon0 + Issue25.bpl(12,3): anon2_LoopHead + Issue25.bpl(12,3): anon2_LoopDone Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/civl/regression-tests/intro-nonblocking.bpl.expect b/Test/civl/regression-tests/intro-nonblocking.bpl.expect index 1a747e1d9..08c401b27 100644 --- a/Test/civl/regression-tests/intro-nonblocking.bpl.expect +++ b/Test/civl/regression-tests/intro-nonblocking.bpl.expect @@ -1,5 +1,4 @@ intro-nonblocking.bpl(4,13): Error: Cooperation check for intro failed Execution trace: - (0,0): init Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/civl/regression-tests/left-mover.bpl.expect b/Test/civl/regression-tests/left-mover.bpl.expect index 44ada71cb..383a2cd10 100644 --- a/Test/civl/regression-tests/left-mover.bpl.expect +++ b/Test/civl/regression-tests/left-mover.bpl.expect @@ -10,6 +10,5 @@ Execution trace: left-mover.bpl(6,24): inline$inc$0$Return left-mover.bpl(26,24): Error: Cooperation check for block failed Execution trace: - (0,0): init Boogie program verifier finished with 3 verified, 3 errors diff --git a/Test/civl/regression-tests/non-interference-1.bpl.expect b/Test/civl/regression-tests/non-interference-1.bpl.expect index 9ed2f19b1..be24ba16a 100644 --- a/Test/civl/regression-tests/non-interference-1.bpl.expect +++ b/Test/civl/regression-tests/non-interference-1.bpl.expect @@ -2,6 +2,5 @@ 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$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 c1176c36d..4bbae5629 100644 --- a/Test/civl/regression-tests/non-interference-2.bpl.expect +++ b/Test/civl/regression-tests/non-interference-2.bpl.expect @@ -2,10 +2,8 @@ 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$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$L Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect index b97bf307f..55715916a 100644 --- a/Test/civl/regression-tests/pa-noninterference-check.bpl.expect +++ b/Test/civl/regression-tests/pa-noninterference-check.bpl.expect @@ -1,6 +1,5 @@ pa-noninterference-check.bpl(26,1): Error: Non-interference check failed Execution trace: - (0,0): init pa-noninterference-check.bpl(19,7): inline$A_Incr$0$anon0 pa-noninterference-check.bpl(16,34): inline$A_Incr$0$Return diff --git a/Test/civl/regression-tests/parallel1.bpl.expect b/Test/civl/regression-tests/parallel1.bpl.expect index 4b52e2854..0bc33ffe1 100644 --- a/Test/civl/regression-tests/parallel1.bpl.expect +++ b/Test/civl/regression-tests/parallel1.bpl.expect @@ -2,6 +2,5 @@ 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$L Boogie program verifier finished with 3 verified, 1 error diff --git a/Test/civl/regression-tests/parallel6.bpl.expect b/Test/civl/regression-tests/parallel6.bpl.expect index 0ff7beb24..9a6a6e2be 100644 --- a/Test/civl/regression-tests/parallel6.bpl.expect +++ b/Test/civl/regression-tests/parallel6.bpl.expect @@ -7,6 +7,5 @@ Execution trace: parallel6.bpl(11,5): anon0_0 parallel6.bpl(30,7): inline$atomic_incr$2$anon0 parallel6.bpl(30,7): inline$atomic_incr$3$anon0 - (0,0): Civl_ReturnChecker Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/regression-tests/pending-async-1.bpl.expect b/Test/civl/regression-tests/pending-async-1.bpl.expect index 86c6fbf94..5e0a35e06 100644 --- a/Test/civl/regression-tests/pending-async-1.bpl.expect +++ b/Test/civl/regression-tests/pending-async-1.bpl.expect @@ -5,7 +5,6 @@ Execution trace: pending-async-1.bpl(51,3): anon0$1 pending-async-1.bpl(11,9): inline$B$1$anon0 pending-async-1.bpl(51,3): anon0$2 - (0,0): Civl_ReturnChecker pending-async-1.bpl(67,3): Error: Pending asyncs to action A created by this call are not summarized Execution trace: pending-async-1.bpl(67,3): anon0 diff --git a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect index 29a3c680e..d6951c016 100644 --- a/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect +++ b/Test/civl/regression-tests/pending-async-noninterference-fail.bpl.expect @@ -1,6 +1,5 @@ pending-async-noninterference-fail.bpl(7,1): Error: Non-interference check failed Execution trace: - (0,0): init pending-async-noninterference-fail.bpl(12,5): inline$A$0$anon0 pending-async-noninterference-fail.bpl(9,32): inline$A$0$Return diff --git a/Test/civl/regression-tests/refinement.bpl.expect b/Test/civl/regression-tests/refinement.bpl.expect index 4974958b5..7203ec2a4 100644 --- a/Test/civl/regression-tests/refinement.bpl.expect +++ b/Test/civl/regression-tests/refinement.bpl.expect @@ -5,13 +5,11 @@ Execution trace: refinement.bpl(10,3): anon0$1 refinement.bpl(10,3): anon0_0 refinement.bpl(58,5): inline$INCR$1$anon0 - (0,0): Civl_ReturnChecker refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state in a way that does not match the refined atomic action Execution trace: refinement.bpl(18,3): anon0 refinement.bpl(64,5): inline$DECR$0$anon0 refinement.bpl(18,3): anon0$1 - (0,0): Civl_RefinementChecker refinement.bpl(15,28): Error: A yield-to-yield fragment modifies layer-2 state subsequent to a yield-to-yield fragment that already modified layer-2 state Execution trace: refinement.bpl(18,3): anon0 @@ -19,11 +17,9 @@ Execution trace: refinement.bpl(18,3): anon0$1 refinement.bpl(18,3): anon0_0 refinement.bpl(58,5): inline$INCR$0$anon0 - (0,0): Civl_ReturnChecker refinement.bpl(37,28): Error: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: refinement.bpl(41,1): anon0 - (0,0): Civl_ReturnChecker refinement.bpl(43,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals Execution trace: refinement.bpl(46,3): anon0 @@ -32,6 +28,5 @@ Execution trace: refinement.bpl(46,3): anon0_0 refinement.bpl(48,3): anon2_LoopHead refinement.bpl(58,5): inline$INCR$1$anon0 - (0,0): Civl_UnchangedChecker Boogie program verifier finished with 3 verified, 5 errors diff --git a/Test/civl/regression-tests/refinement2.bpl.expect b/Test/civl/regression-tests/refinement2.bpl.expect index 3005f0993..24cb32f73 100644 --- a/Test/civl/regression-tests/refinement2.bpl.expect +++ b/Test/civl/regression-tests/refinement2.bpl.expect @@ -1,15 +1,11 @@ refinement2.bpl(13,28): Error: On some path no yield-to-yield fragment matched the refined atomic action Execution trace: refinement2.bpl(16,5): anon0 - (0,0): Civl_call_refinement_4 refinement2.bpl(27,28): inline$atomic_nop$0$Return - (0,0): Civl_ReturnChecker refinement2.bpl(13,28): Error: A yield-to-yield fragment illegally modifies layer-2 globals Execution trace: refinement2.bpl(16,5): anon0 - (0,0): Civl_call_refinement_3 refinement2.bpl(22,7): inline$atomic_incr$0$anon0 refinement2.bpl(19,28): inline$atomic_incr$0$Return - (0,0): Civl_UnchangedChecker Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect index 093836a59..8bab02145 100644 --- a/Test/civl/regression-tests/yield-invariant-fails.bpl.expect +++ b/Test/civl/regression-tests/yield-invariant-fails.bpl.expect @@ -2,6 +2,5 @@ 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$L Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/commandline/SplitOnEveryAssert.bpl b/Test/commandline/SplitOnEveryAssert.bpl index 2e3878802..f65fd1203 100644 --- a/Test/commandline/SplitOnEveryAssert.bpl +++ b/Test/commandline/SplitOnEveryAssert.bpl @@ -3,18 +3,18 @@ // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Verifying Ex ... -// CHECK: checking split 1/11 .* -// CHECK: checking split 2/11 .* -// CHECK: checking split 3/11 .* -// CHECK: --> split #3 done, \[.* s\] Invalid -// CHECK: checking split 4/11 .* -// CHECK: checking split 5/11 .* -// CHECK: checking split 6/11 .* -// CHECK: checking split 7/11 .* -// CHECK: checking split 8/11 .* -// CHECK: checking split 9/11 .* -// CHECK: checking split 10/11 .* -// CHECK: checking split 11/11 .* +// CHECK: checking split 1/12 .* +// CHECK: checking split 2/12 .* +// CHECK: checking split 3/12 .* +// CHECK: checking split 4/12 .* +// CHECK: --> split #4 done, \[.* s\] Invalid +// CHECK: checking split 5/12 .* +// CHECK: checking split 6/12 .* +// CHECK: checking split 7/12 .* +// CHECK: checking split 8/12 .* +// CHECK: checking split 9/12 .* +// CHECK: checking split 10/12 .* +// CHECK: checking split 11/12 .* // CHECK-L: SplitOnEveryAssert.bpl(31,5): Error: this assertion could not be proved procedure Ex() returns (y: int) diff --git a/Test/pruning/Focus.bpl b/Test/implementationDivision/focus/focus.bpl similarity index 100% rename from Test/pruning/Focus.bpl rename to Test/implementationDivision/focus/focus.bpl diff --git a/Test/pruning/Focus.bpl.expect b/Test/implementationDivision/focus/focus.bpl.expect similarity index 50% rename from Test/pruning/Focus.bpl.expect rename to Test/implementationDivision/focus/focus.bpl.expect index 71c2b6338..2c28a1a35 100644 --- a/Test/pruning/Focus.bpl.expect +++ b/Test/implementationDivision/focus/focus.bpl.expect @@ -1,3 +1,3 @@ -Focus.bpl(15,5): Error: this assertion could not be proved +focus.bpl(15,5): Error: this assertion could not be proved Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl new file mode 100644 index 000000000..59cd30f93 --- /dev/null +++ b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl @@ -0,0 +1,42 @@ +// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure IsolateAssertion(x: int, y: int) +{ + var z: int; + z := 0; + if (x > 0) { + z := z + 1; + } else { + z := z + 2; + } + + if (y > 0) { + z := z + 3; + } else { + z := z + 4; + } + assert z > 1; + assert {:isolate} z > 5; + assert z > 6; +} + +procedure IsolatePathsAssertion(x: int, y: int) +{ + var z: int; + z := 0; + if (x > 0) { + z := z + 1; + } else { + z := z + 2; + } + + if (y > 0) { + z := z + 3; + } else { + z := z + 4; + } + assert z > 1; + assert {:isolate "paths"} z > 5; // fails on three out of four paths + assert z > 6; +} \ No newline at end of file diff --git a/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect new file mode 100644 index 000000000..27589907d --- /dev/null +++ b/Test/implementationDivision/isolateAssertion/isolateAssertion.bpl.expect @@ -0,0 +1,183 @@ +implementation IsolateAssertion/assert@20(x: int, y: int) +{ + + anon0: + goto anon7_Then, anon7_Else; + + anon7_Then: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#2 == z#AT#0; + goto anon8_Then, anon8_Else; + + anon7_Else: + assume {:partition} 0 >= x; + assume z#AT#1 == 0 + 2; + assume z#AT#2 == z#AT#1; + goto anon8_Then, anon8_Else; + + anon8_Then: + assume {:partition} y > 0; + assume z#AT#3 == z#AT#2 + 3; + assume z#AT#5 == z#AT#3; + goto anon6; + + anon8_Else: + assume {:partition} 0 >= y; + assume z#AT#4 == z#AT#2 + 4; + assume z#AT#5 == z#AT#4; + goto anon6; + + anon6: + assume z#AT#5 > 1; + assert {:isolate} z#AT#5 > 5; + return; +} + + +implementation IsolateAssertion(x: int, y: int) +{ + + anon0: + goto anon7_Then, anon7_Else; + + anon7_Then: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#2 == z#AT#0; + goto anon8_Then, anon8_Else; + + anon7_Else: + assume {:partition} 0 >= x; + assume z#AT#1 == 0 + 2; + assume z#AT#2 == z#AT#1; + goto anon8_Then, anon8_Else; + + anon8_Then: + assume {:partition} y > 0; + assume z#AT#3 == z#AT#2 + 3; + assume z#AT#5 == z#AT#3; + goto anon6; + + anon8_Else: + assume {:partition} 0 >= y; + assume z#AT#4 == z#AT#2 + 4; + assume z#AT#5 == z#AT#4; + goto anon6; + + anon6: + assert z#AT#5 > 1; + assume z#AT#5 > 5; + assert z#AT#5 > 6; + return; +} + + +isolateAssertion.bpl(20,3): Error: this assertion could not be proved +isolateAssertion.bpl(21,3): Error: this assertion could not be proved +implementation IsolatePathsAssertion/assert@40[29,35](x: int, y: int) +{ + + anon0: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#2 == z#AT#0; + assume {:partition} y > 0; + assume z#AT#3 == z#AT#2 + 3; + assume z#AT#5 == z#AT#3; + assume z#AT#5 > 1; + assert {:isolate "paths"} z#AT#5 > 5; + return; +} + + +implementation IsolatePathsAssertion/assert@40[31,35](x: int, y: int) +{ + + anon0: + assume {:partition} 0 >= x; + assume z#AT#1 == 0 + 2; + assume z#AT#2 == z#AT#1; + assume {:partition} y > 0; + assume z#AT#3 == z#AT#2 + 3; + assume z#AT#5 == z#AT#3; + assume z#AT#5 > 1; + assert {:isolate "paths"} z#AT#5 > 5; + return; +} + + +implementation IsolatePathsAssertion/assert@40[29,37](x: int, y: int) +{ + + anon0: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#2 == z#AT#0; + assume {:partition} 0 >= y; + assume z#AT#4 == z#AT#2 + 4; + assume z#AT#5 == z#AT#4; + assume z#AT#5 > 1; + assert {:isolate "paths"} z#AT#5 > 5; + return; +} + + +implementation IsolatePathsAssertion/assert@40[31,37](x: int, y: int) +{ + + anon0: + assume {:partition} 0 >= x; + assume z#AT#1 == 0 + 2; + assume z#AT#2 == z#AT#1; + assume {:partition} 0 >= y; + assume z#AT#4 == z#AT#2 + 4; + assume z#AT#5 == z#AT#4; + assume z#AT#5 > 1; + assert {:isolate "paths"} z#AT#5 > 5; + return; +} + + +implementation IsolatePathsAssertion(x: int, y: int) +{ + + anon0: + goto anon7_Then, anon7_Else; + + anon7_Then: + assume {:partition} x > 0; + assume z#AT#0 == 0 + 1; + assume z#AT#2 == z#AT#0; + goto anon8_Then, anon8_Else; + + anon7_Else: + assume {:partition} 0 >= x; + assume z#AT#1 == 0 + 2; + assume z#AT#2 == z#AT#1; + goto anon8_Then, anon8_Else; + + anon8_Then: + assume {:partition} y > 0; + assume z#AT#3 == z#AT#2 + 3; + assume z#AT#5 == z#AT#3; + goto anon6; + + anon8_Else: + assume {:partition} 0 >= y; + assume z#AT#4 == z#AT#2 + 4; + assume z#AT#5 == z#AT#4; + goto anon6; + + anon6: + assert z#AT#5 > 1; + assume z#AT#5 > 5; + assert z#AT#5 > 6; + return; +} + + +isolateAssertion.bpl(40,3): Error: this assertion could not be proved +isolateAssertion.bpl(41,3): Error: this assertion could not be proved + +Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl b/Test/implementationDivision/isolateJump/isolateJump.bpl new file mode 100644 index 000000000..d40ee651c --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateJump.bpl @@ -0,0 +1,38 @@ +// RUN: %boogie /printSplit:- /errorTrace:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure IsolateReturn(x: int, y: int) returns (r: int) + ensures r > 4; +{ + r := 0; + if (x > 0) { + r := r + 1; + } else { + r := r + 2; + } + + if (y > 0) { + r := r + 3; + return {:isolate}; + } + + r := r + 4; +} + +procedure IsolateReturnPaths(x: int, y: int) returns (r: int) + ensures r > 4; +{ + r := 0; + if (x > 0) { + r := r + 1; + } else { + r := r + 2; + } + + if (y > 0) { + r := r + 3; + return {:isolate "paths"}; + } + + r := r + 4; +} \ No newline at end of file diff --git a/Test/implementationDivision/isolateJump/isolateJump.bpl.expect b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect new file mode 100644 index 000000000..3c47dc663 --- /dev/null +++ b/Test/implementationDivision/isolateJump/isolateJump.bpl.expect @@ -0,0 +1,126 @@ +implementation IsolateReturn/return@16(x: int, y: int) returns (r: int) +{ + + anon0: + goto anon6_Then, anon6_Else; + + anon6_Then: + assume {:partition} x > 0; + assume r#AT#0 == 0 + 1; + assume r#AT#2 == r#AT#0; + goto anon7_Then; + + anon6_Else: + assume {:partition} 0 >= x; + assume r#AT#1 == 0 + 2; + assume r#AT#2 == r#AT#1; + goto anon7_Then; + + anon7_Then: + assume {:partition} y > 0; + assume r#AT#3 == r#AT#2 + 3; + assume r#AT#5 == r#AT#3; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assert r#AT#5 > 4; + return; +} + + +implementation IsolateReturn(x: int, y: int) returns (r: int) +{ + + anon0: + goto anon6_Then, anon6_Else; + + anon6_Then: + assume {:partition} x > 0; + assume r#AT#0 == 0 + 1; + assume r#AT#2 == r#AT#0; + goto anon7_Else; + + anon6_Else: + assume {:partition} 0 >= x; + assume r#AT#1 == 0 + 2; + assume r#AT#2 == r#AT#1; + goto anon7_Else; + + anon7_Else: + assume {:partition} 0 >= y; + assume r#AT#4 == r#AT#2 + 4; + assume r#AT#5 == r#AT#4; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assert r#AT#5 > 4; + return; +} + + +isolateJump.bpl(16,21): Error: a postcondition could not be proved on this return path +isolateJump.bpl(5,3): Related location: this is the postcondition that could not be proved +implementation IsolateReturnPaths/assert@34[27](x: int, y: int) returns (r: int) +{ + + anon0: + assume {:partition} x > 0; + assume r#AT#0 == 0 + 1; + assume r#AT#2 == r#AT#0; + assume {:partition} y > 0; + assume r#AT#3 == r#AT#2 + 3; + assume r#AT#5 == r#AT#3; + assert r#AT#5 > 4; + return; +} + + +implementation IsolateReturnPaths/assert@34[29](x: int, y: int) returns (r: int) +{ + + anon0: + assume {:partition} 0 >= x; + assume r#AT#1 == 0 + 2; + assume r#AT#2 == r#AT#1; + assume {:partition} y > 0; + assume r#AT#3 == r#AT#2 + 3; + assume r#AT#5 == r#AT#3; + assert r#AT#5 > 4; + return; +} + + +implementation IsolateReturnPaths(x: int, y: int) returns (r: int) +{ + + anon0: + goto anon6_Then, anon6_Else; + + anon6_Then: + assume {:partition} x > 0; + assume r#AT#0 == 0 + 1; + assume r#AT#2 == r#AT#0; + goto anon7_Else; + + anon6_Else: + assume {:partition} 0 >= x; + assume r#AT#1 == 0 + 2; + assume r#AT#2 == r#AT#1; + goto anon7_Else; + + anon7_Else: + assume {:partition} 0 >= y; + assume r#AT#4 == r#AT#2 + 4; + assume r#AT#5 == r#AT#4; + goto GeneratedUnifiedExit; + + GeneratedUnifiedExit: + assert r#AT#5 > 4; + return; +} + + +isolateJump.bpl(34,29): Error: a postcondition could not be proved on this return path +isolateJump.bpl(23,3): Related location: this is the postcondition that could not be proved + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl b/Test/implementationDivision/split/AssumeFalseSplit.bpl similarity index 50% rename from Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl rename to Test/implementationDivision/split/AssumeFalseSplit.bpl index 148216280..92c6bb87f 100644 --- a/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl +++ b/Test/implementationDivision/split/AssumeFalseSplit.bpl @@ -1,8 +1,5 @@ -// RUN: %parallel-boogie /printSplit:%t "%s" > "%t" +// RUN: %boogie /printSplit:- "%s" > "%t" // RUN: %diff "%s.expect" "%t" -// RUN: %diff %S/Foo.split.0.bpl.expect %t-Foo-0.spl -// RUN: %diff %S/Foo.split.1.bpl.expect %t-Foo-1.spl -// RUN: %diff %S/Foo.split.2.bpl.expect %t-Foo-2.spl procedure Foo() { diff --git a/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect new file mode 100644 index 000000000..29725f4eb --- /dev/null +++ b/Test/implementationDivision/split/AssumeFalseSplit.bpl.expect @@ -0,0 +1,36 @@ +implementation Foo/split@4() +{ + + anon3_Then: + assert 2 == 1 + 1; + assume false; + return; +} + + +implementation Foo/split@11() +{ + + anon3_Else: + assume 2 == 1 + 1; + assert {:split_here} 2 == 2; + assume 3 == 2 + 1; + assume 1 == 1; + goto ; +} + + +implementation Foo/split@12() +{ + + anon3_Else: + assume 2 == 1 + 1; + assume 2 == 2; + assert {:split_here} 3 == 2 + 1; + assert 1 == 1; + goto ; +} + + + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test0/Split/Split.bpl b/Test/implementationDivision/split/Split.bpl similarity index 64% rename from Test/test0/Split/Split.bpl rename to Test/implementationDivision/split/Split.bpl index e99d76351..4c7fdaf45 100644 --- a/Test/test0/Split/Split.bpl +++ b/Test/implementationDivision/split/Split.bpl @@ -1,9 +1,5 @@ -// RUN: %parallel-boogie /printSplit:%t "%s" > "%t" +// RUN: %boogie /printSplit:- "%s" > "%t" // RUN: %diff "%s.expect" "%t" -// RUN: %diff %S/Foo.split.0.bpl.expect %t-Foo-0.spl -// RUN: %diff %S/Foo.split.1.bpl.expect %t-Foo-1.spl -// RUN: %diff %S/Foo.split.2.bpl.expect %t-Foo-2.spl -// RUN: %diff %S/Foo.split.3.bpl.expect %t-Foo-3.spl procedure Foo() returns (y: int) ensures y >= 0; diff --git a/Test/implementationDivision/split/Split.bpl.expect b/Test/implementationDivision/split/Split.bpl.expect new file mode 100644 index 000000000..9f213b896 --- /dev/null +++ b/Test/implementationDivision/split/Split.bpl.expect @@ -0,0 +1,112 @@ +implementation Foo/split@4() returns (y: int) +{ + + anon0: + assert 5 + 0 == 5; + assert 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} 0 >= x#AT#0; + assume y#AT#2 == y#AT#0; + assert y#AT#2 >= 0; + return; +} + + +implementation Foo/split@15() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assert {:split_here} (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} x#AT#1 < 3; + assert 2 < 2; + assume y#AT#1 * y#AT#1 > 4; + goto ; +} + + +implementation Foo/split@22() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} 3 <= x#AT#1; + assert {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8; + assert 2 < 2; + goto ; +} + + +implementation Foo/split@25() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + goto anon6_Then, anon6_Else; + + anon6_Else: + assume {:partition} 3 <= x#AT#1; + assume y#AT#1 * y#AT#1 * y#AT#1 < 8; + assume 2 < 2; + goto anon4; + + anon4: + assert {:split_here} (x#AT#1 + y#AT#1) * (x#AT#1 + y#AT#1) == 25; + assert x#AT#1 + y#AT#1 == 5; + assert x#AT#1 * x#AT#1 <= 25; + assume false; + return; + + anon6_Then: + assume {:partition} x#AT#1 < 3; + assume 2 < 2; + assume y#AT#1 * y#AT#1 > 4; + goto anon4; +} + + +implementation Foo/split@19() returns (y: int) +{ + + anon0: + assume 5 + 0 == 5; + assume 5 * 5 <= 25; + assume x#AT#0 + y#AT#0 == 5; + assume x#AT#0 * x#AT#0 <= 25; + assume {:partition} x#AT#0 > 0; + assume x#AT#1 == x#AT#0 - 1; + assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; + assume y#AT#1 == y#AT#0 + 1; + assume {:partition} x#AT#1 < 3; + assume 2 < 2; + assert {:split_here} y#AT#1 * y#AT#1 > 4; + goto ; +} + + +Split.bpl(15,5): Error: this assertion could not be proved +Execution trace: + Split.bpl(8,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/pruning/MonomorphicSplit.bpl b/Test/pruning/MonomorphicSplit.bpl index 15351bb11..1fccbd8bf 100644 --- a/Test/pruning/MonomorphicSplit.bpl +++ b/Test/pruning/MonomorphicSplit.bpl @@ -1,5 +1,5 @@ // RUN: %parallel-boogie /prune:1 /errorTrace:0 /printSplit:"%t" /printSplitDeclarations "%s" > "%t" -// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit--1.spl" +// RUN: %OutputCheck "%s" --file-to-check="%t-monomorphicSplit.spl" // The following checks are a bit simplistic, but this is // on purpose to reduce brittleness. We assume there would now be two uses clauses diff --git a/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect b/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect deleted file mode 100644 index 37fad75c9..000000000 --- a/Test/test0/AssumeFalseSplit/AssumeFalseSplit.bpl.expect +++ /dev/null @@ -1,2 +0,0 @@ - -Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect deleted file mode 100644 index c8727ad27..000000000 --- a/Test/test0/AssumeFalseSplit/Foo.split.0.bpl.expect +++ /dev/null @@ -1,10 +0,0 @@ -implementation Foo() -{ - - anon3_Then: - assert 2 == 1 + 1; - assume false; - return; -} - - diff --git a/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect deleted file mode 100644 index 29ba05d16..000000000 --- a/Test/test0/AssumeFalseSplit/Foo.split.1.bpl.expect +++ /dev/null @@ -1,12 +0,0 @@ -implementation Foo() -{ - - anon3_Else: - assume 2 == 1 + 1; - assert {:split_here} 2 == 2; - assume 3 == 2 + 1; - assume 1 == 1; - goto ; -} - - diff --git a/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect b/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect deleted file mode 100644 index 838d5aebd..000000000 --- a/Test/test0/AssumeFalseSplit/Foo.split.2.bpl.expect +++ /dev/null @@ -1,12 +0,0 @@ -implementation Foo() -{ - - anon3_Else: - assume 2 == 1 + 1; - assume 2 == 2; - assert {:split_here} 3 == 2 + 1; - assert 1 == 1; - goto ; -} - - diff --git a/Test/test0/Split/Foo.split.0.bpl.expect b/Test/test0/Split/Foo.split.0.bpl.expect deleted file mode 100644 index 79578bccc..000000000 --- a/Test/test0/Split/Foo.split.0.bpl.expect +++ /dev/null @@ -1,15 +0,0 @@ -implementation Foo() returns (y: int) -{ - - anon0: - assert 5 + 0 == 5; - assert 5 * 5 <= 25; - assume x#AT#0 + y#AT#0 == 5; - assume x#AT#0 * x#AT#0 <= 25; - assume {:partition} 0 >= x#AT#0; - assume y#AT#2 == y#AT#0; - assert y#AT#2 >= 0; - return; -} - - diff --git a/Test/test0/Split/Foo.split.1.bpl.expect b/Test/test0/Split/Foo.split.1.bpl.expect deleted file mode 100644 index 37297e028..000000000 --- a/Test/test0/Split/Foo.split.1.bpl.expect +++ /dev/null @@ -1,19 +0,0 @@ -implementation Foo() returns (y: int) -{ - - anon0: - assume 5 + 0 == 5; - assume 5 * 5 <= 25; - assume x#AT#0 + y#AT#0 == 5; - assume x#AT#0 * x#AT#0 <= 25; - assume {:partition} x#AT#0 > 0; - assume x#AT#1 == x#AT#0 - 1; - assert {:split_here} (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; - assume y#AT#1 == y#AT#0 + 1; - assume {:partition} x#AT#1 < 3; - assert 2 < 2; - assume y#AT#1 * y#AT#1 > 4; - goto ; -} - - diff --git a/Test/test0/Split/Foo.split.2.bpl.expect b/Test/test0/Split/Foo.split.2.bpl.expect deleted file mode 100644 index 7f28a2ebf..000000000 --- a/Test/test0/Split/Foo.split.2.bpl.expect +++ /dev/null @@ -1,19 +0,0 @@ -implementation Foo() returns (y: int) -{ - - anon0: - assume 5 + 0 == 5; - assume 5 * 5 <= 25; - assume x#AT#0 + y#AT#0 == 5; - assume x#AT#0 * x#AT#0 <= 25; - assume {:partition} x#AT#0 > 0; - assume x#AT#1 == x#AT#0 - 1; - assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; - assume y#AT#1 == y#AT#0 + 1; - assume {:partition} 3 <= x#AT#1; - assert {:split_here} y#AT#1 * y#AT#1 * y#AT#1 < 8; - assert 2 < 2; - goto ; -} - - diff --git a/Test/test0/Split/Foo.split.3.bpl.expect b/Test/test0/Split/Foo.split.3.bpl.expect deleted file mode 100644 index eb031aa38..000000000 --- a/Test/test0/Split/Foo.split.3.bpl.expect +++ /dev/null @@ -1,35 +0,0 @@ -implementation Foo() returns (y: int) -{ - - anon0: - assume 5 + 0 == 5; - assume 5 * 5 <= 25; - assume x#AT#0 + y#AT#0 == 5; - assume x#AT#0 * x#AT#0 <= 25; - assume {:partition} x#AT#0 > 0; - assume x#AT#1 == x#AT#0 - 1; - assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; - assume y#AT#1 == y#AT#0 + 1; - goto anon6_Then, anon6_Else; - - anon6_Else: - assume {:partition} 3 <= x#AT#1; - assume y#AT#1 * y#AT#1 * y#AT#1 < 8; - assume 2 < 2; - goto anon4; - - anon4: - assert {:split_here} (x#AT#1 + y#AT#1) * (x#AT#1 + y#AT#1) == 25; - assert x#AT#1 + y#AT#1 == 5; - assert x#AT#1 * x#AT#1 <= 25; - assume false; - return; - - anon6_Then: - assume {:partition} x#AT#1 < 3; - assume 2 < 2; - assume y#AT#1 * y#AT#1 > 4; - goto anon4; -} - - diff --git a/Test/test0/Split/Foo.split.4.bpl.expect b/Test/test0/Split/Foo.split.4.bpl.expect deleted file mode 100644 index 83b9850a7..000000000 --- a/Test/test0/Split/Foo.split.4.bpl.expect +++ /dev/null @@ -1,31 +0,0 @@ -implementation Foo() returns (y: int) -{ - - PreconditionGeneratedEntry: - goto anon0; - - anon0: - assume 5 + 0 == 5; - assume 5 * 5 <= 25; - goto anon5_LoopHead; - - anon5_LoopHead: - assume x#AT#0 + y#AT#0 == 5; - assume x#AT#0 * x#AT#0 <= 25; - goto anon5_LoopBody; - - anon5_LoopBody: - assume {:partition} x#AT#0 > 0; - assume x#AT#1 == x#AT#0 - 1; - assume (x#AT#1 + y#AT#0) * (x#AT#1 + y#AT#0) > 25; - assume y#AT#1 == y#AT#0 + 1; - goto anon6_Then; - - anon6_Then: - assume {:partition} x#AT#1 < 3; - assume 2 < 2; - assert {:split_here} y#AT#1 * y#AT#1 > 4; - goto ; -} - - diff --git a/Test/test0/Split/Split.bpl.expect b/Test/test0/Split/Split.bpl.expect deleted file mode 100644 index 67f8e9921..000000000 --- a/Test/test0/Split/Split.bpl.expect +++ /dev/null @@ -1,5 +0,0 @@ -Split.bpl(19,5): Error: this assertion could not be proved -Execution trace: - Split.bpl(12,5): anon0 - -Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test0/SplitOnEveryAssert.bpl b/Test/test0/SplitOnEveryAssert.bpl index c883fb50c..d1313c7c9 100644 --- a/Test/test0/SplitOnEveryAssert.bpl +++ b/Test/test0/SplitOnEveryAssert.bpl @@ -3,18 +3,18 @@ // RUN: %OutputCheck --file-to-check "%t" "%s" // CHECK: Verifying DoTheSplitting ... -// CHECK: checking split 1/11.* -// CHECK: checking split 2/11.* -// CHECK: checking split 3/11.* -// CHECK: --> split #3 done, \[.* s\] Invalid -// CHECK: checking split 4/11.* -// CHECK: checking split 5/11.* -// CHECK: checking split 6/11.* -// CHECK: checking split 7/11.* -// CHECK: checking split 8/11.* -// CHECK: checking split 9/11.* -// CHECK: checking split 10/11.* -// CHECK: checking split 11/11.* +// CHECK: checking split 1/12.* +// CHECK: checking split 2/12.* +// CHECK: checking split 3/12.* +// CHECK: checking split 4/12.* +// CHECK: --> split #4 done, \[.* s\] Invalid +// CHECK: checking split 5/12.* +// CHECK: checking split 6/12.* +// CHECK: checking split 7/12.* +// CHECK: checking split 8/12.* +// CHECK: checking split 9/12.* +// CHECK: checking split 10/12.* +// CHECK: checking split 11/12.* // CHECK-L: SplitOnEveryAssert.bpl(36,5): Error: this assertion could not be proved // Verify the second procedure is NOT split. .* is necessary to match the blank line in-between. diff --git a/Test/test2/Structured.bpl.expect b/Test/test2/Structured.bpl.expect index a349c0d87..22c885b42 100644 --- a/Test/test2/Structured.bpl.expect +++ b/Test/test2/Structured.bpl.expect @@ -22,6 +22,5 @@ Execution trace: Structured.bpl(355,3): anon4_LoopHead Structured.bpl(358,7): anon4_LoopBody Structured.bpl(361,7): anon5_LoopBody - (0,0): anon3 Boogie program verifier finished with 16 verified, 4 errors