diff --git a/Source/Houdini/HoudiniSession.cs b/Source/Houdini/HoudiniSession.cs index 2cbdcc41b..e4d0959c5 100644 --- a/Source/Houdini/HoudiniSession.cs +++ b/Source/Houdini/HoudiniSession.cs @@ -129,7 +129,7 @@ public class HoudiniStatistics public HashSet CoveredElements { get; } = new(); private VCExpr conjecture; private ProverInterface.ErrorHandler handler; - ConditionGeneration.VerificationResultCollector collector; + VerificationResultCollector collector; HashSet unsatCoreSet; HashSet houdiniConstants; public HashSet houdiniAssertConstants; @@ -163,7 +163,7 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf this.Description = impl.Name; this.houdini = houdini; this.stats = stats; - collector = new ConditionGeneration.VerificationResultCollector(houdini.Options); + collector = new VerificationResultCollector(houdini.Options); collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0); vcgen.ConvertCFG2DAG(run, taskID: taskID); diff --git a/Source/VCGeneration/BlockListComparer.cs b/Source/VCGeneration/BlockListComparer.cs new file mode 100644 index 000000000..3df87811c --- /dev/null +++ b/Source/VCGeneration/BlockListComparer.cs @@ -0,0 +1,29 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; + +namespace VC; + +class BlockListComparer : IEqualityComparer> +{ + public bool Equals(List x, List y) + { + return x == y || x.SequenceEqual(y); + } + + public int GetHashCode(List obj) + { + int h = 0; + Contract.Assume(obj != null); + foreach (var b in obj) + { + if (b != null) + { + h += b.GetHashCode(); + } + } + + return h; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/BlockStats.cs b/Source/VCGeneration/BlockStats.cs new file mode 100644 index 000000000..eba08b349 --- /dev/null +++ b/Source/VCGeneration/BlockStats.cs @@ -0,0 +1,40 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Boogie; + +namespace VC; + +class BlockStats +{ + public bool bigBlock; + public int id; + public double assertionCost; + public double assumptionCost; // before multiplier + public double incomingPaths; + + public List /*!>!*/ + virtualSuccessors = new List(); + + public List /*!>!*/ + virtualPredecessors = new List(); + + public HashSet reachableBlocks; + public readonly Block block; + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(cce.NonNullElements(virtualSuccessors)); + Contract.Invariant(cce.NonNullElements(virtualPredecessors)); + Contract.Invariant(block != null); + } + + + public BlockStats(Block b, int i) + { + Contract.Requires(b != null); + block = b; + assertionCost = -1; + id = i; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/BlockTransformations.cs b/Source/VCGeneration/BlockTransformations.cs new file mode 100644 index 000000000..89f17aac7 --- /dev/null +++ b/Source/VCGeneration/BlockTransformations.cs @@ -0,0 +1,64 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; + +namespace VCGeneration; + +public static class BlockTransformations +{ + public static List PostProcess(List blocks) + { + void DeleteFalseGotos (Block b) + { + var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse); + if (firstFalseIdx != -1) + { + b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList(); + b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd; + } + + return; + + bool IsAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; } + } + + bool ContainsAssert(Block b) + { + return b.Cmds.Exists(IsNonTrivialAssert); + bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } + } + + blocks.ForEach(DeleteFalseGotos); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously + var todo = new Stack(); + var peeked = new HashSet(); + var interestingBlocks = new HashSet(); + todo.Push(blocks[0]); + while(todo.Any()) + { + var currentBlock = todo.Peek(); + var pop = peeked.Contains(currentBlock); + peeked.Add(currentBlock); + var interesting = false; + var exit = currentBlock.TransferCmd as GotoCmd; + if (exit != null && !pop) { + exit.labelTargets.ForEach(b => todo.Push(b)); + } else if (exit != null) { + Contract.Assert(pop); + var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); + currentBlock.TransferCmd = gtc; + interesting = interesting || gtc.labelTargets.Count() != 0; + } + if (pop) + { + interesting = interesting || ContainsAssert(currentBlock); + if (interesting) { + interestingBlocks.Add(currentBlock); + } + todo.Pop(); + } + } + interestingBlocks.Add(blocks[0]); // must not be empty + return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. + } +} \ No newline at end of file diff --git a/Source/VCGeneration/CommandTransformations.cs b/Source/VCGeneration/CommandTransformations.cs new file mode 100644 index 000000000..a39bac235 --- /dev/null +++ b/Source/VCGeneration/CommandTransformations.cs @@ -0,0 +1,17 @@ +using Microsoft.Boogie; +using VC; + +namespace VCGeneration; + +public class CommandTransformations +{ + public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c) + { + if (c is AssertCmd assrt) + { + return VCGen.AssertTurnedIntoAssume(options, assrt); + } + + return c; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 8a0c7aed7..418d47198 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -1,7 +1,6 @@ using System; using System.Linq; using System.Collections; -using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics; using System.Threading; @@ -511,46 +510,6 @@ public virtual void Close() } - public class VerificationResultCollector : VerifierCallback - { - private readonly VCGenOptions options; - - public VerificationResultCollector(VCGenOptions options) : base(options.PrintProverWarnings) - { - this.options = options; - } - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(examples)); - Contract.Invariant(cce.NonNullElements(vcResults)); - } - - public readonly ConcurrentQueue examples = new(); - public readonly ConcurrentQueue vcResults = new(); - - public override void OnCounterexample(Counterexample ce, string /*?*/ reason) - { - //Contract.Requires(ce != null); - ce.InitializeModelStates(); - examples.Enqueue(ce); - } - - public override void OnUnreachableCode(ImplementationRun run) - { - //Contract.Requires(impl != null); - run.OutputWriter.WriteLine("found unreachable code:"); - EmitImpl(options, run, false); - // TODO report error about next to last in seq - } - - public override void OnVCResult(VerificationRunResult result) - { - vcResults.Enqueue(result); - } - } - public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool printDesugarings) { var impl = run.Implementation; diff --git a/Source/VCGeneration/FocusAttribute.cs b/Source/VCGeneration/FocusAttribute.cs new file mode 100644 index 000000000..e08874579 --- /dev/null +++ b/Source/VCGeneration/FocusAttribute.cs @@ -0,0 +1,139 @@ +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, VCGen par) + { + bool IsFocusCmd(Cmd c) { + return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); + } + + List GetFocusBlocks(List blocks) { + return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList(); + } + + var impl = run.Implementation; + var dag = Program.GraphFromImpl(impl); + var topoSorted = 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(topoSorted); + if (par.CheckerPool.Options.RelaxFocus) { + focusBlocks.Reverse(); + } + if (!focusBlocks.Any()) { + var f = new List(); + f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run)); + return f; + } + // finds all the blocks dominated by focusBlock in the subgraph + // which only contains vertices of subgraph. + HashSet DominatedBlocks(Block focusBlock, IEnumerable subgraph) + { + var dominators = new Dictionary>(); + var todo = new Queue(); + foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk))) + { + 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(); + } + + Cmd DisableSplits(Cmd c) + { + if (c is PredicateCmd pc) + { + for (var kv = pc.Attributes; kv != null; kv = kv.Next) + { + if (kv.Key == "split") + { + kv.AddParam(new LiteralExpr(Token.NoToken, false)); + } + } + } + return c; + } + + var Ancestors = new Dictionary>(); + var Descendants = new Dictionary>(); + focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet()); + focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet()); + var s = new List(); + var duplicator = new Duplicator(); + void FocusRec(int focusIdx, IEnumerable blocks, IEnumerable freeBlocks) + { + if (focusIdx == focusBlocks.Count()) + { + // it is important for l to be consistent with reverse topological order. + var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse(); + // assert that the root block, impl.Blocks[0], is in l + Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]); + var newBlocks = new List(); + var oldToNewBlockMap = new Dictionary(blocks.Count()); + foreach (Block b in l) + { + var newBlock = (Block)duplicator.Visit(b); + newBlocks.Add(newBlock); + oldToNewBlockMap[b] = newBlock; + // freeBlocks consist of the predecessors of the relevant foci. + // Their assertions turn into assumes and any splits inside them are disabled. + if(freeBlocks.Contains(b)) + { + newBlock.Cmds = b.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList(); + } + if (b.TransferCmd is GotoCmd gtc) + { + var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk)); + 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]]); + s.Add(new Split(options, BlockTransformations.PostProcess(newBlocks), gotoCmdOrigins, par, run)); + } + else if (!blocks.Contains(focusBlocks[focusIdx]) + || freeBlocks.Contains(focusBlocks[focusIdx])) + { + FocusRec(focusIdx + 1, blocks, freeBlocks); + } + else + { + var b = focusBlocks[focusIdx]; // assert b in blocks + var dominatedBlocks = DominatedBlocks(b, blocks); + // the first part takes all blocks except the ones dominated by the focus block + FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks); + var ancestors = Ancestors[b]; + ancestors.Remove(b); + var descendants = Descendants[b]; + // the other part takes all the ancestors, the focus block, and the descendants. + FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks)); + } + } + + FocusRec(0, impl.Blocks, new List()); + return s; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/ManualSplitFinder.cs b/Source/VCGeneration/ManualSplitFinder.cs new file mode 100644 index 000000000..76c3922d6 --- /dev/null +++ b/Source/VCGeneration/ManualSplitFinder.cs @@ -0,0 +1,167 @@ +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; +using VC; + +namespace VCGeneration; + +public static class ManualSplitFinder +{ + + public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par, bool splitOnEveryAssert) + { + List focussedImpl = FocusAttribute.FocusImpl(options, run, gotoCmdOrigins, par); + var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList(); + return splits; + } + + public static List FindManualSplits(Split initialSplit, bool splitOnEveryAssert) + { + Contract.Requires(initialSplit.Implementation != null); + Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); + + var splitPoints = new Dictionary(); + foreach (var b in initialSplit.Blocks) + { + foreach (Cmd c in b.Cmds) + { + var p = c as PredicateCmd; + if (ShouldSplitHere(c, splitOnEveryAssert)) + { + splitPoints.TryGetValue(b, out var count); + splitPoints[b] = count + 1; + } + } + } + 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.Keys.Contains(entryPoint); + var baseSplitBlocks = BlockTransformations.PostProcess(DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert)); + splits.Add(new Split(initialSplit.Options, baseSplitBlocks, initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); + foreach (KeyValuePair pair in splitPoints) + { + for (int i = 0; i < pair.Value; i++) + { + bool lastSplitInBlock = i == pair.Value - 1; + var newBlocks = DoPreAssignedManualSplit(initialSplit.Options, initialSplit.Blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert); + splits.Add(new Split(initialSplit.Options, BlockTransformations.PostProcess(newBlocks), initialSplit.GotoCmdOrigins, initialSplit.parent, initialSplit.Run)); // REVIEW: Does gotoCmdOrigins need to be changed at all? + } + } + } + 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; + } + else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. + { + blockAssignments[currentBlock] = currentBlock; + } + else if (splitPoints.Keys.Contains(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 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 oldToNewBlockMap = new Dictionary(blocks.Count()); // Maps original blocks to their new copies in newBlocks + foreach (var currentBlock in blocks) + { + var newBlock = (Block)duplicator.VisitBlock(currentBlock); + oldToNewBlockMap[currentBlock] = newBlock; + newBlocks.Add(newBlock); + if (currentBlock == containingBlock) + { + var newCmds = new List(); + var splitCount = -1; + var verify = splitCount == splitNumberWithinBlock; + foreach (Cmd c in currentBlock.Cmds) + { + if (ShouldSplitHere(c, splitOnEveryAssert)) + { + splitCount++; + verify = splitCount == splitNumberWithinBlock; + } + newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c)); + } + newBlock.Cmds = newCmds; + } + else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) + { + var verify = true; + var newCmds = new List(); + foreach(Cmd c in currentBlock.Cmds) { + verify = !ShouldSplitHere(c, splitOnEveryAssert) && verify; + newCmds.Add(verify ? c : CommandTransformations.AssertIntoAssume(options, c)); + } + newBlock.Cmds = newCmds; + } + else + { + newBlock.Cmds = currentBlock.Cmds.Select(x => CommandTransformations.AssertIntoAssume(options, x)).ToList(); + } + } + // Patch the edges between the new blocks + foreach (var oldBlock in blocks) + { + if (oldBlock.TransferCmd is ReturnCmd) + { + 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); + } + return newBlocks; + } +} \ No newline at end of file diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 71b04876a..1fdb94a58 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -9,6 +9,7 @@ using Microsoft.BaseTypes; using Microsoft.Boogie.VCExprAST; using Microsoft.Boogie.SMTLib; +using VCGeneration; namespace VC { @@ -17,56 +18,21 @@ namespace VC public class Split : ProofRun { - private VCGenOptions options; + public VCGenOptions Options { get; } - public int? RandomSeed => Implementation.RandomSeed ?? options.RandomSeed; - private Random randomGen; + public int? RandomSeed => Implementation.RandomSeed ?? Options.RandomSeed; + private readonly Random randomGen; - private ImplementationRun run; - - class BlockStats - { - public bool bigBlock; - public int id; - public double assertionCost; - public double assumptionCost; // before multiplier - public double incomingPaths; - - public List /*!>!*/ - virtualSuccessors = new List(); - - public List /*!>!*/ - virtualPredecessors = new List(); - - public HashSet reachableBlocks; - public readonly Block block; - - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(cce.NonNullElements(virtualSuccessors)); - Contract.Invariant(cce.NonNullElements(virtualPredecessors)); - Contract.Invariant(block != null); - } - - - public BlockStats(Block b, int i) - { - Contract.Requires(b != null); - block = b; - assertionCost = -1; - id = i; - } - } + public ImplementationRun Run { get; } [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(blocks)); + Contract.Invariant(cce.NonNullElements(Blocks)); Contract.Invariant(cce.NonNullElements(bigBlocks)); Contract.Invariant(cce.NonNullDictionaryAndValues(stats)); Contract.Invariant(cce.NonNullElements(assumizedBranches)); - Contract.Invariant(gotoCmdOrigins != null); + Contract.Invariant(GotoCmdOrigins != null); Contract.Invariant(parent != null); Contract.Invariant(Implementation != null); Contract.Invariant(copies != null); @@ -75,8 +41,8 @@ void ObjectInvariant() } - private readonly List blocks; - public List Asserts => blocks.SelectMany(block => block.cmds.OfType()).ToList(); + public List Blocks { get; } + public List Asserts => Blocks.SelectMany(block => block.cmds.OfType()).ToList(); public readonly IReadOnlyList TopLevelDeclarations; readonly List bigBlocks = new(); @@ -96,13 +62,11 @@ void ObjectInvariant() int assertionCount; double assertionCost; // without multiplication by paths - Dictionary /*!*/ - gotoCmdOrigins; + public Dictionary GotoCmdOrigins { get; } - readonly public VCGen /*!*/ - parent; + public readonly VCGen /*!*/ parent; - public Implementation /*!*/ Implementation => run.Implementation; + public Implementation /*!*/ Implementation => Run.Implementation; Dictionary /*!*/ copies = new Dictionary(); @@ -129,11 +93,11 @@ public Split(VCGenOptions options, List /*!*/ blocks, Contract.Requires(cce.NonNullElements(blocks)); Contract.Requires(gotoCmdOrigins != null); Contract.Requires(par != null); - this.blocks = blocks; - this.gotoCmdOrigins = gotoCmdOrigins; + this.Blocks = blocks; + this.GotoCmdOrigins = gotoCmdOrigins; this.parent = par; - this.run = run; - this.options = options; + this.Run = run; + this.Options = options; Interlocked.Increment(ref currentId); TopLevelDeclarations = par.program.TopLevelDeclarations; @@ -145,14 +109,14 @@ public Split(VCGenOptions options, List /*!*/ blocks, private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix) { - if (!options.Prune || options.PrintPrunedFile == null) + if (!Options.Prune || Options.PrintPrunedFile == null) { return; } using var writer = new TokenTextWriter( - $"{options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, - options.PrettyPrint, options); + $"{Options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, + Options.PrettyPrint, Options); var functionAxioms = program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); @@ -230,17 +194,17 @@ public void DumpDot(int splitNum) string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum); using (System.IO.StreamWriter sw = System.IO.File.CreateText(filename)) { - int oldPrintUnstructured = options.PrintUnstructured; - options.PrintUnstructured = 2; // print only the unstructured program - bool oldPrintDesugaringSetting = options.PrintDesugarings; - options.PrintDesugarings = false; + int oldPrintUnstructured = Options.PrintUnstructured; + Options.PrintUnstructured = 2; // print only the unstructured program + bool oldPrintDesugaringSetting = Options.PrintDesugarings; + Options.PrintDesugarings = false; List backup = Implementation.Blocks; Contract.Assert(backup != null); - Implementation.Blocks = blocks; - Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, options), 0); + Implementation.Blocks = Blocks; + Implementation.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false, Options), 0); Implementation.Blocks = backup; - options.PrintDesugarings = oldPrintDesugaringSetting; - options.PrintUnstructured = oldPrintUnstructured; + Options.PrintDesugarings = oldPrintDesugaringSetting; + Options.PrintUnstructured = oldPrintUnstructured; } } @@ -357,13 +321,13 @@ void ComputeBestSplit() assertionCount = 0; - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); CountAssertions(b); } - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); BlockStats bs = GetBlockStats(b); @@ -376,7 +340,7 @@ void ComputeBestSplit() BlockStats chs = GetBlockStats(ch); if (!chs.bigBlock) { - options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b); + Options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b); DumpDot(-1); Contract.Assert(false); throw new cce.UnreachableException(); @@ -446,7 +410,7 @@ void ComputeBestSplit() } } - if (options.VcsPathSplitMult * score > totalCost) + if (Options.VcsPathSplitMult * score > totalCost) { splitBlock = null; score = -1; @@ -485,7 +449,7 @@ void UpdateIncommingPaths(BlockStats s) if (count > 1) { - s.incomingPaths *= options.VcsPathJoinMult; + s.incomingPaths *= Options.VcsPathJoinMult; } } } @@ -534,11 +498,11 @@ void ComputeBlockSets(bool allowSmall) keepAtAll.Clear(); Debug.Assert(splitBlock == null || GetBlockStats(splitBlock).bigBlock); - Debug.Assert(GetBlockStats(blocks[0]).bigBlock); + Debug.Assert(GetBlockStats(Blocks[0]).bigBlock); if (assertToAssume) { - foreach (Block b in allowSmall ? blocks : bigBlocks) + foreach (Block b in allowSmall ? Blocks : bigBlocks) { Contract.Assert(b != null); if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock))) @@ -563,7 +527,7 @@ void ComputeBlockSets(bool allowSmall) } else { - ComputeBlockSetsHelper(blocks[0], allowSmall); + ComputeBlockSetsHelper(Blocks[0], allowSmall); } } @@ -584,7 +548,7 @@ double DoComputeScore(bool aa) GetBlockStats(b).incomingPaths = -1.0; } - GetBlockStats(blocks[0]).incomingPaths = 1.0; + GetBlockStats(Blocks[0]).incomingPaths = 1.0; double cost = 0.0; foreach (Block b in bigBlocks) @@ -597,14 +561,14 @@ double DoComputeScore(bool aa) double local = s.assertionCost; if (ShouldAssumize(b)) { - local = (s.assertionCost + s.assumptionCost) * options.VcsAssumeMult; + local = (s.assertionCost + s.assumptionCost) * Options.VcsAssumeMult; } else { - local = s.assumptionCost * options.VcsAssumeMult + s.assertionCost; + local = s.assumptionCost * Options.VcsAssumeMult + s.assertionCost; } - local = local + local * s.incomingPaths * options.VcsPathCostMult; + local = local + local * s.incomingPaths * Options.VcsPathCostMult; cost += local; } } @@ -652,7 +616,7 @@ List SliceCmds(Block b) if (swap) { - theNewCmd = VCGen.AssertTurnedIntoAssume(options, a); + theNewCmd = VCGen.AssertTurnedIntoAssume(Options, a); } } @@ -704,18 +668,18 @@ Split DoSplit() Contract.Ensures(Contract.Result() != null); copies.Clear(); - CloneBlock(blocks[0]); + CloneBlock(Blocks[0]); List newBlocks = new List(); Dictionary newGotoCmdOrigins = new Dictionary(); - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); if (copies.TryGetValue(b, out var tmp)) { newBlocks.Add(cce.NonNull(tmp)); - if (gotoCmdOrigins.ContainsKey(b.TransferCmd)) + if (GotoCmdOrigins.ContainsKey(b.TransferCmd)) { - newGotoCmdOrigins[tmp.TransferCmd] = gotoCmdOrigins[b.TransferCmd]; + newGotoCmdOrigins[tmp.TransferCmd] = GotoCmdOrigins[b.TransferCmd]; } foreach (Block p in b.Predecessors) @@ -729,7 +693,7 @@ Split DoSplit() } } - return new Split(options, newBlocks, newGotoCmdOrigins, parent, run); + return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run); } Split SplitAt(int idx) @@ -767,8 +731,8 @@ void Print() { List tmp = Implementation.Blocks; Contract.Assert(tmp != null); - Implementation.Blocks = blocks; - ConditionGeneration.EmitImpl(options, run, false); + Implementation.Blocks = Blocks; + ConditionGeneration.EmitImpl(Options, Run, false); Implementation.Blocks = tmp; } @@ -778,13 +742,13 @@ public Counterexample ToCounterexample(ProverContext context) Contract.Ensures(Contract.Result() != null); List trace = new List(); - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); trace.Add(b); } - foreach (Block b in blocks) + foreach (Block b in Blocks) { Contract.Assert(b != null); foreach (Cmd c in b.Cmds) @@ -792,7 +756,7 @@ public Counterexample ToCounterexample(ProverContext context) Contract.Assert(c != null); if (c is AssertCmd) { - var counterexample = VCGen.AssertCmdToCounterexample(options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this); + var counterexample = VCGen.AssertCmdToCounterexample(Options, (AssertCmd) c, cce.NonNull(b.TransferCmd), trace, null, null, null, context, this); Counterexamples.Add(counterexample); return counterexample; } @@ -803,339 +767,12 @@ public Counterexample ToCounterexample(ProverContext context) throw new cce.UnreachableException(); } - // 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; - } - else if (immediateDominator[currentBlock] == currentBlock) // if the currentBlock doesn't have a predecessor. - { - blockAssignments[currentBlock] = currentBlock; - } - else if (splitPoints.Keys.Contains(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 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 oldToNewBlockMap = new Dictionary(blocks.Count()); // Maps original blocks to their new copies in newBlocks - foreach (var currentBlock in blocks) - { - var newBlock = (Block)duplicator.VisitBlock(currentBlock); - oldToNewBlockMap[currentBlock] = newBlock; - newBlocks.Add(newBlock); - if (currentBlock == containingBlock) - { - var newCmds = new List(); - var splitCount = -1; - var verify = splitCount == splitNumberWithinBlock; - foreach (Cmd c in currentBlock.Cmds) - { - if (ShouldSplitHere(c, splitOnEveryAssert)) - { - splitCount++; - verify = splitCount == splitNumberWithinBlock; - } - newCmds.Add(verify ? c : AssertIntoAssume(options, c)); - } - newBlock.Cmds = newCmds; - } - else if (lastSplitInBlock && blockAssignments[currentBlock] == containingBlock) - { - var verify = true; - var newCmds = new List(); - foreach(Cmd c in currentBlock.Cmds) { - verify = !ShouldSplitHere(c, splitOnEveryAssert) && verify; - newCmds.Add(verify ? c : AssertIntoAssume(options, c)); - } - newBlock.Cmds = newCmds; - } - else - { - newBlock.Cmds = currentBlock.Cmds.Select(x => AssertIntoAssume(options, x)).ToList(); - } - } - // Patch the edges between the new blocks - foreach (var oldBlock in blocks) - { - if (oldBlock.TransferCmd is ReturnCmd) - { - 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); - } - return newBlocks; - } - - private static List PostProcess(List blocks) - { - void DeleteFalseGotos (Block b) - { - bool isAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; } - var firstFalseIdx = b.Cmds.FindIndex(c => isAssumeFalse(c)); - if (firstFalseIdx != -1) - { - b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList(); - b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd; - } - } - - bool ContainsAssert(Block b) - { - bool isNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); } - return b.Cmds.Exists(cmd => isNonTrivialAssert(cmd)); - } - - blocks.ForEach(b => DeleteFalseGotos(b)); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously - var todo = new Stack(); - var peeked = new HashSet(); - var interestingBlocks = new HashSet(); - todo.Push(blocks[0]); - while(todo.Count() > 0) - { - var currentBlock = todo.Peek(); - var pop = peeked.Contains(currentBlock); - peeked.Add(currentBlock); - var interesting = false; - var exit = currentBlock.TransferCmd as GotoCmd; - if (exit != null && !pop) { - exit.labelTargets.ForEach(b => todo.Push(b)); - } else if (exit != null) { - Contract.Assert(pop); - var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList()); - currentBlock.TransferCmd = gtc; - interesting = interesting || gtc.labelTargets.Count() != 0; - } - if (pop) - { - interesting = interesting || ContainsAssert(currentBlock); - if (interesting) { - interestingBlocks.Add(currentBlock); - } - todo.Pop(); - } - } - interestingBlocks.Add(blocks[0]); // must not be empty - return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders. - } - - private static bool ShouldSplitHere(Cmd c, bool splitOnEveryAssert) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "split_here") - || c is AssertCmd && splitOnEveryAssert; - } - - public static List FindManualSplits(Split initialSplit, bool splitOnEveryAssert) - { - Contract.Requires(initialSplit.Implementation != null); - Contract.Ensures(Contract.Result>() == null || cce.NonNullElements(Contract.Result>())); - - var splitPoints = new Dictionary(); - foreach (var b in initialSplit.blocks) - { - foreach (Cmd c in b.Cmds) - { - var p = c as PredicateCmd; - if (ShouldSplitHere(c, splitOnEveryAssert)) - { - splitPoints.TryGetValue(b, out var count); - splitPoints[b] = count + 1; - } - } - } - 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.Keys.Contains(entryPoint); - var baseSplitBlocks = PostProcess(DoPreAssignedManualSplit(initialSplit.options, initialSplit.blocks, blockAssignments, -1, entryPoint, !entryBlockHasSplit, splitOnEveryAssert)); - splits.Add(new Split(initialSplit.options, baseSplitBlocks, initialSplit.gotoCmdOrigins, initialSplit.parent, initialSplit.run)); - foreach (KeyValuePair pair in splitPoints) - { - for (int i = 0; i < pair.Value; i++) - { - bool lastSplitInBlock = i == pair.Value - 1; - var newBlocks = DoPreAssignedManualSplit(initialSplit.options, initialSplit.blocks, blockAssignments, i, pair.Key, lastSplitInBlock, splitOnEveryAssert); - splits.Add(new Split(initialSplit.options, PostProcess(newBlocks), initialSplit.gotoCmdOrigins, initialSplit.parent, initialSplit.run)); // REVIEW: Does gotoCmdOrigins need to be changed at all? - } - } - } - return splits; - } - - public static List FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par) - { - bool IsFocusCmd(Cmd c) { - return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus"); - } - - List GetFocusBlocks(List blocks) { - return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList(); - } - - var impl = run.Implementation; - var dag = Program.GraphFromImpl(impl); - var topoSorted = 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(topoSorted); - if (par.CheckerPool.Options.RelaxFocus) { - focusBlocks.Reverse(); - } - if (!focusBlocks.Any()) { - var f = new List(); - f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run)); - return f; - } - // finds all the blocks dominated by focusBlock in the subgraph - // which only contains vertices of subgraph. - HashSet DominatedBlocks(Block focusBlock, IEnumerable subgraph) - { - var dominators = new Dictionary>(); - var todo = new Queue(); - foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk))) - { - var s = new HashSet(); - var pred = b.Predecessors.Where(blk => subgraph.Contains(blk)).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(); - } - - Cmd DisableSplits(Cmd c) - { - if (c is PredicateCmd pc) - { - for (var kv = pc.Attributes; kv != null; kv = kv.Next) - { - if (kv.Key == "split") - { - kv.AddParam(new LiteralExpr(Token.NoToken, false)); - } - } - } - return c; - } - - var Ancestors = new Dictionary>(); - var Descendants = new Dictionary>(); - focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet()); - focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet()); - var s = new List(); - var duplicator = new Duplicator(); - void FocusRec(int focusIdx, IEnumerable blocks, IEnumerable freeBlocks) - { - if (focusIdx == focusBlocks.Count()) - { - // it is important for l to be consistent with reverse topological order. - var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse(); - // assert that the root block, impl.Blocks[0], is in l - Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]); - var newBlocks = new List(); - var oldToNewBlockMap = new Dictionary(blocks.Count()); - foreach (Block b in l) - { - var newBlock = (Block)duplicator.Visit(b); - newBlocks.Add(newBlock); - oldToNewBlockMap[b] = newBlock; - // freeBlocks consist of the predecessors of the relevant foci. - // Their assertions turn into assumes and any splits inside them are disabled. - if(freeBlocks.Contains(b)) - { - newBlock.Cmds = b.Cmds.Select(c => Split.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList(); - } - if (b.TransferCmd is GotoCmd gtc) - { - var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk)); - 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]]); - s.Add(new Split(options, PostProcess(newBlocks), gotoCmdOrigins, par, run)); - } - else if (!blocks.Contains(focusBlocks[focusIdx]) - || freeBlocks.Contains(focusBlocks[focusIdx])) - { - FocusRec(focusIdx + 1, blocks, freeBlocks); - } - else - { - var b = focusBlocks[focusIdx]; // assert b in blocks - var dominatedBlocks = DominatedBlocks(b, blocks); - // the first part takes all blocks except the ones dominated by the focus block - FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks); - var ancestors = Ancestors[b]; - ancestors.Remove(b); - var descendants = Descendants[b]; - // the other part takes all the ancestors, the focus block, and the descendants. - FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks)); - } - } - - FocusRec(0, impl.Blocks, new List()); - return s; - } - - public static List FocusAndSplit(VCGenOptions options, ImplementationRun run, Dictionary gotoCmdOrigins, VCGen par, bool splitOnEveryAssert) - { - List focussedImpl = FocusImpl(options, run, gotoCmdOrigins, par); - var splits = focussedImpl.Select(s => FindManualSplits(s, splitOnEveryAssert)).SelectMany(x => x).ToList(); - return splits; - } - public static List /*!*/ DoSplit(Split initial, double splitThreshold, int maxSplits) { Contract.Requires(initial != null); Contract.Ensures(cce.NonNullElements(Contract.Result>())); - var run = initial.run; + var run = initial.Run; var result = new List { initial }; while (result.Count < maxSplits) @@ -1161,7 +798,7 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun Split s0, s1; - bool splitStats = initial.options.TraceVerify; + bool splitStats = initial.Options.TraceVerify; if (splitStats) { @@ -1208,12 +845,12 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun { var ss = new List { - s0.blocks[0], - s1.blocks[0] + s0.Blocks[0], + s1.Blocks[0] }; try { - best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.blocks[0], ss); + best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.Blocks[0], ss); } catch (System.Exception e) { @@ -1234,7 +871,7 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun run.OutputWriter.WriteLine(" --> {0}", s1.Stats); } - if (initial.options.TraceVerify) + if (initial.Options.TraceVerify) { best.Print(); } @@ -1246,41 +883,18 @@ public static List FocusAndSplit(VCGenOptions options, ImplementationRun return result; } - class BlockListComparer : IEqualityComparer> - { - public bool Equals(List x, List y) - { - return x == y || x.SequenceEqual(y); - } - - public int GetHashCode(List obj) - { - int h = 0; - Contract.Assume(obj != null); - foreach (var b in obj) - { - if (b != null) - { - h += b.GetHashCode(); - } - } - - return h; - } - } - public (Bpl.Outcome outcome, VerificationRunResult result, int resourceCount) ReadOutcome(int iteration, Checker checker, VerifierCallback callback) { Contract.EnsuresOnThrow(true); Bpl.Outcome outcome = cce.NonNull(checker).ReadOutcome(); - if (options.Trace && SplitIndex >= 0) + if (Options.Trace && SplitIndex >= 0) { - run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, + Run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, checker.ProverRunTime.TotalSeconds, outcome); } - if (options.Trace && options.TrackVerificationCoverage) { - run.OutputWriter.WriteLine("Proof dependencies:\n {0}", + if (Options.Trace && Options.TrackVerificationCoverage) { + Run.OutputWriter.WriteLine("Proof dependencies:\n {0}", string.Join("\n ", CoveredElements.Select(s => s.Description).OrderBy(s => s))); } @@ -1296,10 +910,10 @@ public int GetHashCode(List obj) Asserts: Asserts, CoveredElements: CoveredElements, ResourceCount: resourceCount, - SolverUsed: (options as SMTLibSolverOptions)?.Solver); + SolverUsed: (Options as SMTLibSolverOptions)?.Solver); callback.OnVCResult(result); - if (options.VcsDumpSplits) + if (Options.VcsDumpSplits) { DumpDot(SplitIndex); } @@ -1323,7 +937,7 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa VCExpr vc; // Lock impl since we're setting impl.Blocks that is used to generate the VC. lock (Implementation) { - Implementation.Blocks = blocks; + Implementation.Blocks = Blocks; var absyIds = new ControlFlowIdMap(); @@ -1343,13 +957,13 @@ public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCa exprGen.ControlFlowFunctionApplication(exprGen.Integer(BigNum.ZERO), exprGen.Integer(BigNum.ZERO)); VCExpr eqExpr = exprGen.Eq(controlFlowFunctionAppl, exprGen.Integer(BigNum.FromInt(absyIds.GetId(Implementation.Blocks[0])))); vc = exprGen.Implies(eqExpr, vc); - reporter = new VCGen.ErrorReporter(options, gotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, + reporter = new VCGen.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, mvInfo, checker.TheoremProver.Context, parent.program, this); } - if (options.TraceVerify && SplitIndex >= 0) + if (Options.TraceVerify && SplitIndex >= 0) { - run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex); + Run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex); Print(); } @@ -1370,16 +984,6 @@ public string Description } } - private static Cmd AssertIntoAssume(VCGenOptions options, Cmd c) - { - if (c is AssertCmd assrt) - { - return VCGen.AssertTurnedIntoAssume(options, assrt); - } - - return c; - } - private void SoundnessCheck(HashSet /*!*/> /*!*/ cache, Block /*!*/ orig, List /*!*/ copies) { diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index ca3942fd7..d361ada9a 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -7,6 +7,7 @@ using System.Threading; using System.Threading.Tasks; using Microsoft.Boogie; +using VCGeneration; using static VC.ConditionGeneration; using Outcome = Microsoft.Boogie.Outcome; @@ -68,7 +69,7 @@ public SplitAndVerifyWorker(VCGenOptions options, VCGen vcGen, ImplementationRun Implementation.CheckBooleanAttribute("vcs_split_on_every_assert", ref splitOnEveryAssert); ResetPredecessors(Implementation.Blocks); - manualSplits = Split.FocusAndSplit(options, run, gotoCmdOrigins, vcGen, splitOnEveryAssert); + manualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, vcGen, splitOnEveryAssert); if (manualSplits.Count == 1 && maxSplits > 1) { manualSplits = Split.DoSplit(manualSplits[0], maxVcCost, maxSplits); diff --git a/Source/VCGeneration/VerificationResultCollector.cs b/Source/VCGeneration/VerificationResultCollector.cs new file mode 100644 index 000000000..6957914ad --- /dev/null +++ b/Source/VCGeneration/VerificationResultCollector.cs @@ -0,0 +1,45 @@ +using System.Collections.Concurrent; +using System.Diagnostics.Contracts; +using Microsoft.Boogie; + +namespace VC; + +public class VerificationResultCollector : VerifierCallback +{ + private readonly VCGenOptions options; + + public VerificationResultCollector(VCGenOptions options) : base(options.PrintProverWarnings) + { + this.options = options; + } + + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(cce.NonNullElements(examples)); + Contract.Invariant(cce.NonNullElements(vcResults)); + } + + public readonly ConcurrentQueue examples = new(); + public readonly ConcurrentQueue vcResults = new(); + + public override void OnCounterexample(Counterexample ce, string /*?*/ reason) + { + //Contract.Requires(ce != null); + ce.InitializeModelStates(); + examples.Enqueue(ce); + } + + public override void OnUnreachableCode(ImplementationRun run) + { + //Contract.Requires(impl != null); + run.OutputWriter.WriteLine("found unreachable code:"); + ConditionGeneration.EmitImpl(options, run, false); + // TODO report error about next to last in seq + } + + public override void OnVCResult(VerificationRunResult result) + { + vcResults.Enqueue(result); + } +} \ No newline at end of file