From 0b24d7e0d92d414a89f297d489c202d6dafa8e41 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 26 Jan 2024 16:29:19 +0100 Subject: [PATCH] Undo namespace changes --- Source/VCGeneration/Split.cs | 1558 ++++++++++--------- Source/VCGeneration/SplitAndVerifyWorker.cs | 522 ++++--- 2 files changed, 1069 insertions(+), 1011 deletions(-) diff --git a/Source/VCGeneration/Split.cs b/Source/VCGeneration/Split.cs index 5fba058a7..09bb8464d 100644 --- a/Source/VCGeneration/Split.cs +++ b/Source/VCGeneration/Split.cs @@ -11,1031 +11,1049 @@ using Microsoft.Boogie.SMTLib; using VCGeneration; -namespace VC; +namespace VC +{ -using System.Threading.Tasks; + using System.Threading.Tasks; -public class Split : ProofRun -{ - public VCGenOptions Options { get; } - private readonly Random randomGen; - public ImplementationRun Run { get; } + public class Split : ProofRun + { + public VCGenOptions Options { get; } + private readonly Random randomGen; + public ImplementationRun Run { get; } - public int? RandomSeed => Implementation.RandomSeed ?? Options.RandomSeed; + public int? RandomSeed => Implementation.RandomSeed ?? Options.RandomSeed; - public List Blocks { get; } - readonly List bigBlocks = new(); - public List Asserts => Blocks.SelectMany(block => block.cmds.OfType()).ToList(); - public readonly IReadOnlyList TopLevelDeclarations; + public List Blocks { get; } + readonly List bigBlocks = new(); + public List Asserts => Blocks.SelectMany(block => block.cmds.OfType()).ToList(); + public readonly IReadOnlyList TopLevelDeclarations; - readonly Dictionary /*!*/ - stats = new Dictionary(); - static int currentId = -1; + readonly Dictionary /*!*/ + stats = new Dictionary(); - Block splitBlock; - bool assertToAssume; + static int currentId = -1; - List /*!*/ - assumizedBranches = new List(); + Block splitBlock; + bool assertToAssume; - double score; - bool scoreComputed; - double totalCost; - int assertionCount; - double assertionCost; // without multiplication by paths + List /*!*/ + assumizedBranches = new List(); - public Dictionary GotoCmdOrigins { get; } + double score; + bool scoreComputed; + double totalCost; + int assertionCount; + double assertionCost; // without multiplication by paths - public readonly VerificationConditionGenerator /*!*/ parent; + public Dictionary GotoCmdOrigins { get; } - public Implementation /*!*/ Implementation => Run.Implementation; + public readonly VerificationConditionGenerator /*!*/ + parent; - Dictionary /*!*/ - copies = new Dictionary(); + public Implementation /*!*/ Implementation => Run.Implementation; - bool doingSlice; - double sliceInitialLimit; - double sliceLimit; - bool slicePos; + Dictionary /*!*/ + copies = new Dictionary(); - HashSet /*!*/ - protectedFromAssertToAssume = new HashSet(); + bool doingSlice; + double sliceInitialLimit; + double sliceLimit; + bool slicePos; - HashSet /*!*/ - keepAtAll = new HashSet(); + HashSet /*!*/ + protectedFromAssertToAssume = new HashSet(); - // async interface - public int SplitIndex { get; set; } - public VerificationConditionGenerator.ErrorReporter reporter; + HashSet /*!*/ + keepAtAll = new HashSet(); - public Split(VCGenOptions options, List /*!*/ blocks, - Dictionary /*!*/ gotoCmdOrigins, - VerificationConditionGenerator /*!*/ par, ImplementationRun run) - { - Contract.Requires(cce.NonNullElements(blocks)); - Contract.Requires(gotoCmdOrigins != null); - Contract.Requires(par != null); - this.Blocks = blocks; - this.GotoCmdOrigins = gotoCmdOrigins; - parent = par; - this.Run = run; - this.Options = options; - Interlocked.Increment(ref currentId); - - TopLevelDeclarations = par.program.TopLevelDeclarations; - PrintTopLevelDeclarationsForPruning(par.program, Implementation, "before"); - TopLevelDeclarations = Prune.GetLiveDeclarations(options, par.program, blocks).ToList(); - PrintTopLevelDeclarationsForPruning(par.program, Implementation, "after"); - randomGen = new Random(RandomSeed ?? 0); - } + // async interface + public int SplitIndex { get; set; } + public VerificationConditionGenerator.ErrorReporter reporter; - private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix) - { - if (!Options.Prune || Options.PrintPrunedFile == null) + public Split(VCGenOptions options, List /*!*/ blocks, + Dictionary /*!*/ gotoCmdOrigins, + VerificationConditionGenerator /*!*/ par, ImplementationRun run) { - return; + Contract.Requires(cce.NonNullElements(blocks)); + Contract.Requires(gotoCmdOrigins != null); + Contract.Requires(par != null); + this.Blocks = blocks; + this.GotoCmdOrigins = gotoCmdOrigins; + parent = par; + this.Run = run; + this.Options = options; + Interlocked.Increment(ref currentId); + + TopLevelDeclarations = par.program.TopLevelDeclarations; + PrintTopLevelDeclarationsForPruning(par.program, Implementation, "before"); + TopLevelDeclarations = Prune.GetLiveDeclarations(options, par.program, blocks).ToList(); + PrintTopLevelDeclarationsForPruning(par.program, Implementation, "after"); + randomGen = new Random(RandomSeed ?? 0); } - using var writer = new TokenTextWriter( - $"{Options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, - Options.PrettyPrint, Options); + private void PrintTopLevelDeclarationsForPruning(Program program, Implementation implementation, string suffix) + { + if (!Options.Prune || Options.PrintPrunedFile == null) + { + return; + } - var functionAxioms = - program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); - var constantAxioms = - program.Constants.Where(f => f.DefinitionAxioms.Any()).SelectMany(c => c.DefinitionAxioms); + using var writer = new TokenTextWriter( + $"{Options.PrintPrunedFile}-{suffix}-{Util.EscapeFilename(implementation.Name)}.bpl", false, + Options.PrettyPrint, Options); - foreach (var declaration in (TopLevelDeclarations ?? program.TopLevelDeclarations). - Except(functionAxioms.Concat(constantAxioms)).ToList()) { - declaration.Emit(writer, 0); - } + var functionAxioms = + program.Functions.Where(f => f.DefinitionAxioms.Any()).SelectMany(f => f.DefinitionAxioms); + var constantAxioms = + program.Constants.Where(f => f.DefinitionAxioms.Any()).SelectMany(c => c.DefinitionAxioms); - writer.Close(); - } + foreach (var declaration in (TopLevelDeclarations ?? program.TopLevelDeclarations) + .Except(functionAxioms.Concat(constantAxioms)).ToList()) + { + declaration.Emit(writer, 0); + } - public double Cost - { - get + writer.Close(); + } + + public double Cost { - ComputeBestSplit(); - return totalCost; + get + { + ComputeBestSplit(); + return totalCost; + } } - } - public bool LastChance - { - get + public bool LastChance { - ComputeBestSplit(); - return assertionCount == 1 && score < 0; + get + { + ComputeBestSplit(); + return assertionCount == 1 && score < 0; + } } - } - public string Stats - { - get + public string Stats { - ComputeBestSplit(); - return $"(cost:{totalCost:0}/{assertionCost:0}{(LastChance ? " last" : "")})"; + get + { + ComputeBestSplit(); + return $"(cost:{totalCost:0}/{assertionCost:0}{(LastChance ? " last" : "")})"; + } } - } - public void DumpDot(int splitNum) - { - using (StreamWriter sw = File.CreateText($"{Implementation.Name}.split.{splitNum}.dot")) + public void DumpDot(int splitNum) { - sw.WriteLine("digraph G {"); + using (StreamWriter sw = File.CreateText($"{Implementation.Name}.split.{splitNum}.dot")) + { + sw.WriteLine("digraph G {"); - ComputeBestSplit(); - List saved = assumizedBranches; - Contract.Assert(saved != null); - assumizedBranches = new List(); - DoComputeScore(false); - assumizedBranches = saved; + ComputeBestSplit(); + List saved = assumizedBranches; + Contract.Assert(saved != null); + assumizedBranches = new List(); + DoComputeScore(false); + assumizedBranches = saved; - foreach (Block b in bigBlocks) - { - Contract.Assert(b != null); - BlockStats s = GetBlockStats(b); - foreach (Block t in s.virtualSuccessors) + foreach (Block b in bigBlocks) { - Contract.Assert(t != null); - sw.WriteLine("n{0} -> n{1};", s.id, GetBlockStats(t).id); + Contract.Assert(b != null); + BlockStats s = GetBlockStats(b); + foreach (Block t in s.virtualSuccessors) + { + Contract.Assert(t != null); + sw.WriteLine("n{0} -> n{1};", s.id, GetBlockStats(t).id); + } + + sw.WriteLine("n{0} [label=\"{1}:\\n({2:0.0}+{3:0.0})*{4:0.0}\"{5}];", + s.id, b.Label, + s.assertionCost, s.assumptionCost, s.incomingPaths, + s.assertionCost > 0 ? ",shape=box" : ""); } - sw.WriteLine("n{0} [label=\"{1}:\\n({2:0.0}+{3:0.0})*{4:0.0}\"{5}];", - s.id, b.Label, - s.assertionCost, s.assumptionCost, s.incomingPaths, - s.assertionCost > 0 ? ",shape=box" : ""); + sw.WriteLine("}"); + sw.Close(); } - sw.WriteLine("}"); - sw.Close(); - } - - string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum); - using (StreamWriter sw = File.CreateText(filename)) - { - 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 = backup; - Options.PrintDesugarings = oldPrintDesugaringSetting; - Options.PrintUnstructured = oldPrintUnstructured; + string filename = string.Format("{0}.split.{1}.bpl", Implementation.Name, splitNum); + using (StreamWriter sw = File.CreateText(filename)) + { + 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 = backup; + Options.PrintDesugarings = oldPrintDesugaringSetting; + Options.PrintUnstructured = oldPrintUnstructured; + } } - } - int bsid; + int bsid; - BlockStats GetBlockStats(Block b) - { - Contract.Requires(b != null); - Contract.Ensures(Contract.Result() != null); - - if (!stats.TryGetValue(b, out var s)) + BlockStats GetBlockStats(Block b) { - s = new BlockStats(b, bsid++); - stats[b] = s; - } + Contract.Requires(b != null); + Contract.Ensures(Contract.Result() != null); - return cce.NonNull(s); - } + if (!stats.TryGetValue(b, out var s)) + { + s = new BlockStats(b, bsid++); + stats[b] = s; + } - double AssertionCost(PredicateCmd c) - { - return 1.0; - } + return cce.NonNull(s); + } - void CountAssertions(Block b) - { - Contract.Requires(b != null); - BlockStats s = GetBlockStats(b); - if (s.assertionCost >= 0) + double AssertionCost(PredicateCmd c) { - return; // already done + return 1.0; } - s.bigBlock = true; - s.assertionCost = 0; - s.assumptionCost = 0; - foreach (Cmd c in b.Cmds) + void CountAssertions(Block b) { - if (c is AssertCmd) + Contract.Requires(b != null); + BlockStats s = GetBlockStats(b); + if (s.assertionCost >= 0) { - double cost = AssertionCost((AssertCmd) c); - s.assertionCost += cost; - assertionCount++; - assertionCost += cost; + return; // already done } - else if (c is AssumeCmd) + + s.bigBlock = true; + s.assertionCost = 0; + s.assumptionCost = 0; + foreach (Cmd c in b.Cmds) { - s.assumptionCost += AssertionCost((AssumeCmd) c); + if (c is AssertCmd) + { + double cost = AssertionCost((AssertCmd)c); + s.assertionCost += cost; + assertionCount++; + assertionCost += cost; + } + else if (c is AssumeCmd) + { + s.assumptionCost += AssertionCost((AssumeCmd)c); + } } - } - foreach (Block c in b.Exits()) - { - Contract.Assert(c != null); - s.virtualSuccessors.Add(c); - } - - if (s.virtualSuccessors.Count == 1) - { - Block next = s.virtualSuccessors[0]; - BlockStats se = GetBlockStats(next); - CountAssertions(next); - if (next.Predecessors.Count > 1 || se.virtualSuccessors.Count != 1) + foreach (Block c in b.Exits()) { - return; + Contract.Assert(c != null); + s.virtualSuccessors.Add(c); } - s.virtualSuccessors[0] = se.virtualSuccessors[0]; - s.assertionCost += se.assertionCost; - s.assumptionCost += se.assumptionCost; - se.bigBlock = false; - } - } + if (s.virtualSuccessors.Count == 1) + { + Block next = s.virtualSuccessors[0]; + BlockStats se = GetBlockStats(next); + CountAssertions(next); + if (next.Predecessors.Count > 1 || se.virtualSuccessors.Count != 1) + { + return; + } - HashSet /*!*/ ComputeReachableNodes(Block /*!*/ b) - { - Contract.Requires(b != null); - Contract.Ensures(cce.NonNull(Contract.Result>())); - BlockStats s = GetBlockStats(b); - if (s.reachableBlocks != null) - { - return s.reachableBlocks; + s.virtualSuccessors[0] = se.virtualSuccessors[0]; + s.assertionCost += se.assertionCost; + s.assumptionCost += se.assumptionCost; + se.bigBlock = false; + } } - HashSet blocks = new HashSet(); - s.reachableBlocks = blocks; - blocks.Add(b); - foreach (Block /*!*/ succ in b.Exits()) + HashSet /*!*/ ComputeReachableNodes(Block /*!*/ b) { - Contract.Assert(succ != null); - foreach (Block r in ComputeReachableNodes(succ)) + Contract.Requires(b != null); + Contract.Ensures(cce.NonNull(Contract.Result>())); + BlockStats s = GetBlockStats(b); + if (s.reachableBlocks != null) { - Contract.Assert(r != null); - blocks.Add(r); + return s.reachableBlocks; } - } - - return blocks; - } - double ProverCost(double vcCost) - { - return vcCost * vcCost; - } + HashSet blocks = new HashSet(); + s.reachableBlocks = blocks; + blocks.Add(b); + foreach (Block /*!*/ succ in b.Exits()) + { + Contract.Assert(succ != null); + foreach (Block r in ComputeReachableNodes(succ)) + { + Contract.Assert(r != null); + blocks.Add(r); + } + } - void ComputeBestSplit() - { - if (scoreComputed) - { - return; + return blocks; } - scoreComputed = true; - - assertionCount = 0; - - foreach (Block b in Blocks) + double ProverCost(double vcCost) { - Contract.Assert(b != null); - CountAssertions(b); + return vcCost * vcCost; } - foreach (Block b in Blocks) + void ComputeBestSplit() { - Contract.Assert(b != null); - BlockStats bs = GetBlockStats(b); - if (bs.bigBlock) + if (scoreComputed) { - bigBlocks.Add(b); - foreach (Block ch in bs.virtualSuccessors) - { - Contract.Assert(ch != null); - BlockStats chs = GetBlockStats(ch); - if (!chs.bigBlock) - { - Options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b); - DumpDot(-1); - Contract.Assert(false); - throw new cce.UnreachableException(); - } - - chs.virtualPredecessors.Add(b); - } + return; } - } - assumizedBranches.Clear(); - totalCost = ProverCost(DoComputeScore(false)); + scoreComputed = true; - score = double.PositiveInfinity; - Block bestSplit = null; - List savedBranches = new List(); + assertionCount = 0; - foreach (Block b in bigBlocks) - { - Contract.Assert(b != null); - GotoCmd gt = b.TransferCmd as GotoCmd; - if (gt == null) + foreach (Block b in Blocks) { - continue; + Contract.Assert(b != null); + CountAssertions(b); } - List targ = cce.NonNull(gt.labelTargets); - if (targ.Count < 2) + foreach (Block b in Blocks) { - continue; - } - // caution, we only consider two first exits + Contract.Assert(b != null); + BlockStats bs = GetBlockStats(b); + if (bs.bigBlock) + { + bigBlocks.Add(b); + foreach (Block ch in bs.virtualSuccessors) + { + Contract.Assert(ch != null); + BlockStats chs = GetBlockStats(ch); + if (!chs.bigBlock) + { + Options.OutputWriter.WriteLine("non-big {0} accessed from {1}", ch, b); + DumpDot(-1); + Contract.Assert(false); + throw new cce.UnreachableException(); + } - double left0, right0, left1, right1; - splitBlock = b; + chs.virtualPredecessors.Add(b); + } + } + } assumizedBranches.Clear(); - assumizedBranches.Add(cce.NonNull(targ[0])); - left0 = DoComputeScore(true); - right0 = DoComputeScore(false); + totalCost = ProverCost(DoComputeScore(false)); - assumizedBranches.Clear(); - for (int idx = 1; idx < targ.Count; idx++) + score = double.PositiveInfinity; + Block bestSplit = null; + List savedBranches = new List(); + + foreach (Block b in bigBlocks) { - assumizedBranches.Add(cce.NonNull(targ[idx])); - } + Contract.Assert(b != null); + GotoCmd gt = b.TransferCmd as GotoCmd; + if (gt == null) + { + continue; + } - left1 = DoComputeScore(true); - right1 = DoComputeScore(false); + List targ = cce.NonNull(gt.labelTargets); + if (targ.Count < 2) + { + continue; + } + // caution, we only consider two first exits - double currentScore = ProverCost(left1) + ProverCost(right1); - double otherScore = ProverCost(left0) + ProverCost(right0); + double left0, right0, left1, right1; + splitBlock = b; - if (otherScore < currentScore) - { - currentScore = otherScore; assumizedBranches.Clear(); assumizedBranches.Add(cce.NonNull(targ[0])); - } + left0 = DoComputeScore(true); + right0 = DoComputeScore(false); - if (currentScore < score) - { - score = currentScore; - bestSplit = splitBlock; - savedBranches.Clear(); - savedBranches.AddRange(assumizedBranches); - } - } + assumizedBranches.Clear(); + for (int idx = 1; idx < targ.Count; idx++) + { + assumizedBranches.Add(cce.NonNull(targ[idx])); + } - if (Options.VcsPathSplitMult * score > totalCost) - { - splitBlock = null; - score = -1; - } - else - { - assumizedBranches = savedBranches; - splitBlock = bestSplit; - } - } + left1 = DoComputeScore(true); + right1 = DoComputeScore(false); - void UpdateIncommingPaths(BlockStats s) - { - Contract.Requires(s != null); - if (s.incomingPaths < 0.0) - { - int count = 0; - s.incomingPaths = 0.0; - if (!keepAtAll.Contains(s.block)) - { - return; - } + double currentScore = ProverCost(left1) + ProverCost(right1); + double otherScore = ProverCost(left0) + ProverCost(right0); - foreach (Block b in s.virtualPredecessors) - { - Contract.Assert(b != null); - BlockStats ch = GetBlockStats(b); - Contract.Assert(ch != null); - UpdateIncommingPaths(ch); - if (ch.incomingPaths > 0.0) + if (otherScore < currentScore) + { + currentScore = otherScore; + assumizedBranches.Clear(); + assumizedBranches.Add(cce.NonNull(targ[0])); + } + + if (currentScore < score) { - s.incomingPaths += ch.incomingPaths; - count++; + score = currentScore; + bestSplit = splitBlock; + savedBranches.Clear(); + savedBranches.AddRange(assumizedBranches); } } - if (count > 1) + if (Options.VcsPathSplitMult * score > totalCost) { - s.incomingPaths *= Options.VcsPathJoinMult; + splitBlock = null; + score = -1; + } + else + { + assumizedBranches = savedBranches; + splitBlock = bestSplit; } } - } - - void ComputeBlockSetsHelper(Block b, bool allowSmall) - { - Contract.Requires(b != null); - if (keepAtAll.Contains(b)) - { - return; - } - - keepAtAll.Add(b); - if (allowSmall) + void UpdateIncommingPaths(BlockStats s) { - foreach (Block ch in b.Exits()) + Contract.Requires(s != null); + if (s.incomingPaths < 0.0) { - Contract.Assert(ch != null); - if (b == splitBlock && assumizedBranches.Contains(ch)) + int count = 0; + s.incomingPaths = 0.0; + if (!keepAtAll.Contains(s.block)) { - continue; + return; } - ComputeBlockSetsHelper(ch, allowSmall); - } - } - else - { - foreach (Block ch in GetBlockStats(b).virtualSuccessors) - { - Contract.Assert(ch != null); - if (b == splitBlock && assumizedBranches.Contains(ch)) + foreach (Block b in s.virtualPredecessors) { - continue; + Contract.Assert(b != null); + BlockStats ch = GetBlockStats(b); + Contract.Assert(ch != null); + UpdateIncommingPaths(ch); + if (ch.incomingPaths > 0.0) + { + s.incomingPaths += ch.incomingPaths; + count++; + } } - ComputeBlockSetsHelper(ch, allowSmall); + if (count > 1) + { + s.incomingPaths *= Options.VcsPathJoinMult; + } } } - } - void ComputeBlockSets(bool allowSmall) - { - protectedFromAssertToAssume.Clear(); - keepAtAll.Clear(); + void ComputeBlockSetsHelper(Block b, bool allowSmall) + { + Contract.Requires(b != null); + if (keepAtAll.Contains(b)) + { + return; + } - Debug.Assert(splitBlock == null || GetBlockStats(splitBlock).bigBlock); - Debug.Assert(GetBlockStats(Blocks[0]).bigBlock); + keepAtAll.Add(b); - if (assertToAssume) - { - foreach (Block b in allowSmall ? Blocks : bigBlocks) + if (allowSmall) { - Contract.Assert(b != null); - if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock))) + foreach (Block ch in b.Exits()) { - keepAtAll.Add(b); + Contract.Assert(ch != null); + if (b == splitBlock && assumizedBranches.Contains(ch)) + { + continue; + } + + ComputeBlockSetsHelper(ch, allowSmall); } } - - foreach (Block b in assumizedBranches) + else { - Contract.Assert(b != null); - foreach (Block r in ComputeReachableNodes(b)) + foreach (Block ch in GetBlockStats(b).virtualSuccessors) { - Contract.Assert(r != null); - if (allowSmall || GetBlockStats(r).bigBlock) + Contract.Assert(ch != null); + if (b == splitBlock && assumizedBranches.Contains(ch)) { - keepAtAll.Add(r); - protectedFromAssertToAssume.Add(r); + continue; } + + ComputeBlockSetsHelper(ch, allowSmall); } } } - else - { - ComputeBlockSetsHelper(Blocks[0], allowSmall); - } - } - - bool ShouldAssumize(Block b) - { - Contract.Requires(b != null); - return assertToAssume && !protectedFromAssertToAssume.Contains(b); - } - double DoComputeScore(bool aa) - { - assertToAssume = aa; - ComputeBlockSets(false); - - foreach (Block b in bigBlocks) + void ComputeBlockSets(bool allowSmall) { - Contract.Assert(b != null); - GetBlockStats(b).incomingPaths = -1.0; - } + protectedFromAssertToAssume.Clear(); + keepAtAll.Clear(); - GetBlockStats(Blocks[0]).incomingPaths = 1.0; + Debug.Assert(splitBlock == null || GetBlockStats(splitBlock).bigBlock); + Debug.Assert(GetBlockStats(Blocks[0]).bigBlock); - double cost = 0.0; - foreach (Block b in bigBlocks) - { - Contract.Assert(b != null); - if (keepAtAll.Contains(b)) + if (assertToAssume) { - BlockStats s = GetBlockStats(b); - UpdateIncommingPaths(s); - double local = s.assertionCost; - if (ShouldAssumize(b)) + foreach (Block b in allowSmall ? Blocks : bigBlocks) { - local = (s.assertionCost + s.assumptionCost) * Options.VcsAssumeMult; + Contract.Assert(b != null); + if (ComputeReachableNodes(b).Contains(cce.NonNull(splitBlock))) + { + keepAtAll.Add(b); + } } - else + + foreach (Block b in assumizedBranches) { - local = s.assumptionCost * Options.VcsAssumeMult + s.assertionCost; + Contract.Assert(b != null); + foreach (Block r in ComputeReachableNodes(b)) + { + Contract.Assert(r != null); + if (allowSmall || GetBlockStats(r).bigBlock) + { + keepAtAll.Add(r); + protectedFromAssertToAssume.Add(r); + } + } } - - local = local + local * s.incomingPaths * Options.VcsPathCostMult; - cost += local; + } + else + { + ComputeBlockSetsHelper(Blocks[0], allowSmall); } } - return cost; - } - - List SliceCmds(Block b) - { - Contract.Requires(b != null); - Contract.Ensures(Contract.Result>() != null); - - List seq = b.Cmds; - Contract.Assert(seq != null); - if (!doingSlice && !ShouldAssumize(b)) + bool ShouldAssumize(Block b) { - return seq; + Contract.Requires(b != null); + return assertToAssume && !protectedFromAssertToAssume.Contains(b); } - List res = new List(); - foreach (Cmd c in seq) + double DoComputeScore(bool aa) { - Contract.Assert(c != null); - AssertCmd a = c as AssertCmd; - Cmd theNewCmd = c; - bool swap = false; - if (a != null) + assertToAssume = aa; + ComputeBlockSets(false); + + foreach (Block b in bigBlocks) { - if (doingSlice) - { - double cost = AssertionCost(a); - bool first = (sliceLimit - cost) >= 0 || sliceInitialLimit == sliceLimit; - sliceLimit -= cost; - swap = slicePos == first; - } - else if (assertToAssume) - { - swap = true; - } - else - { - Contract.Assert(false); - throw new cce.UnreachableException(); - } + Contract.Assert(b != null); + GetBlockStats(b).incomingPaths = -1.0; + } + + GetBlockStats(Blocks[0]).incomingPaths = 1.0; - if (swap) + double cost = 0.0; + foreach (Block b in bigBlocks) + { + Contract.Assert(b != null); + if (keepAtAll.Contains(b)) { - theNewCmd = VerificationConditionGenerator.AssertTurnedIntoAssume(Options, a); + BlockStats s = GetBlockStats(b); + UpdateIncommingPaths(s); + double local = s.assertionCost; + if (ShouldAssumize(b)) + { + local = (s.assertionCost + s.assumptionCost) * Options.VcsAssumeMult; + } + else + { + local = s.assumptionCost * Options.VcsAssumeMult + s.assertionCost; + } + + local = local + local * s.incomingPaths * Options.VcsPathCostMult; + cost += local; } } - res.Add(theNewCmd); + return cost; } - return res; - } - - Block CloneBlock(Block b) - { - Contract.Requires(b != null); - Contract.Ensures(Contract.Result() != null); - - if (copies.TryGetValue(b, out var res)) + List SliceCmds(Block b) { - return cce.NonNull(res); - } + Contract.Requires(b != null); + Contract.Ensures(Contract.Result>() != null); - res = new Block(b.tok, b.Label, SliceCmds(b), b.TransferCmd); - GotoCmd gt = b.TransferCmd as GotoCmd; - copies[b] = res; - if (gt != null) - { - GotoCmd newGoto = new GotoCmd(gt.tok, new List(), new List()); - res.TransferCmd = newGoto; - int pos = 0; - foreach (Block ch in cce.NonNull(gt.labelTargets)) + List seq = b.Cmds; + Contract.Assert(seq != null); + if (!doingSlice && !ShouldAssumize(b)) { - Contract.Assert(ch != null); - Contract.Assert(doingSlice || - (assertToAssume || (keepAtAll.Contains(ch) || assumizedBranches.Contains(ch)))); - if (doingSlice || - ((b != splitBlock || assumizedBranches.Contains(ch) == assertToAssume) && - keepAtAll.Contains(ch))) + return seq; + } + + List res = new List(); + foreach (Cmd c in seq) + { + Contract.Assert(c != null); + AssertCmd a = c as AssertCmd; + Cmd theNewCmd = c; + bool swap = false; + if (a != null) { - newGoto.AddTarget(CloneBlock(ch)); + if (doingSlice) + { + double cost = AssertionCost(a); + bool first = (sliceLimit - cost) >= 0 || sliceInitialLimit == sliceLimit; + sliceLimit -= cost; + swap = slicePos == first; + } + else if (assertToAssume) + { + swap = true; + } + else + { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + + if (swap) + { + theNewCmd = VerificationConditionGenerator.AssertTurnedIntoAssume(Options, a); + } } - pos++; + res.Add(theNewCmd); } - } - - return res; - } - Split DoSplit() - { - Contract.Ensures(Contract.Result() != null); + return res; + } - copies.Clear(); - CloneBlock(Blocks[0]); - List newBlocks = new List(); - Dictionary newGotoCmdOrigins = new Dictionary(); - foreach (Block b in Blocks) + Block CloneBlock(Block b) { - Contract.Assert(b != null); - if (copies.TryGetValue(b, out var tmp)) + Contract.Requires(b != null); + Contract.Ensures(Contract.Result() != null); + + if (copies.TryGetValue(b, out var res)) { - newBlocks.Add(cce.NonNull(tmp)); - if (GotoCmdOrigins.ContainsKey(b.TransferCmd)) - { - newGotoCmdOrigins[tmp.TransferCmd] = GotoCmdOrigins[b.TransferCmd]; - } + return cce.NonNull(res); + } - foreach (Block p in b.Predecessors) + res = new Block(b.tok, b.Label, SliceCmds(b), b.TransferCmd); + GotoCmd gt = b.TransferCmd as GotoCmd; + copies[b] = res; + if (gt != null) + { + GotoCmd newGoto = new GotoCmd(gt.tok, new List(), new List()); + res.TransferCmd = newGoto; + int pos = 0; + foreach (Block ch in cce.NonNull(gt.labelTargets)) { - Contract.Assert(p != null); - if (copies.TryGetValue(p, out var tmp2)) + Contract.Assert(ch != null); + Contract.Assert(doingSlice || + (assertToAssume || (keepAtAll.Contains(ch) || assumizedBranches.Contains(ch)))); + if (doingSlice || + ((b != splitBlock || assumizedBranches.Contains(ch) == assertToAssume) && + keepAtAll.Contains(ch))) { - tmp.Predecessors.Add(tmp2); + newGoto.AddTarget(CloneBlock(ch)); } + + pos++; } } + + return res; } - return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run); - } + Split DoSplit() + { + Contract.Ensures(Contract.Result() != null); - Split SplitAt(int idx) - { - Contract.Ensures(Contract.Result() != null); + copies.Clear(); + CloneBlock(Blocks[0]); + List newBlocks = new List(); + Dictionary newGotoCmdOrigins = new Dictionary(); + 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)) + { + newGotoCmdOrigins[tmp.TransferCmd] = GotoCmdOrigins[b.TransferCmd]; + } - assertToAssume = idx == 0; - doingSlice = false; - ComputeBlockSets(true); + foreach (Block p in b.Predecessors) + { + Contract.Assert(p != null); + if (copies.TryGetValue(p, out var tmp2)) + { + tmp.Predecessors.Add(tmp2); + } + } + } + } - return DoSplit(); - } + return new Split(Options, newBlocks, newGotoCmdOrigins, parent, Run); + } - Split SliceAsserts(double limit, bool pos) - { - Contract.Ensures(Contract.Result() != null); - - slicePos = pos; - sliceLimit = limit; - sliceInitialLimit = limit; - doingSlice = true; - Split r = DoSplit(); - /* - Console.WriteLine("split {0} / {1} -->", limit, pos); - List tmp = impl.Blocks; - impl.Blocks = r.blocks; - EmitImpl(impl, false); - impl.Blocks = tmp; - */ - - return r; - } + Split SplitAt(int idx) + { + Contract.Ensures(Contract.Result() != null); - void Print() - { - List tmp = Implementation.Blocks; - Contract.Assert(tmp != null); - Implementation.Blocks = Blocks; - ConditionGeneration.EmitImpl(Options, Run, false); - Implementation.Blocks = tmp; - } + assertToAssume = idx == 0; + doingSlice = false; + ComputeBlockSets(true); - public Counterexample ToCounterexample(ProverContext context) - { - Contract.Requires(context != null); - Contract.Ensures(Contract.Result() != null); + return DoSplit(); + } - List trace = new List(); - foreach (Block block in Blocks) + Split SliceAsserts(double limit, bool pos) { - Contract.Assert(block != null); - trace.Add(block); + Contract.Ensures(Contract.Result() != null); + + slicePos = pos; + sliceLimit = limit; + sliceInitialLimit = limit; + doingSlice = true; + Split r = DoSplit(); + /* + Console.WriteLine("split {0} / {1} -->", limit, pos); + List tmp = impl.Blocks; + impl.Blocks = r.blocks; + EmitImpl(impl, false); + impl.Blocks = tmp; + */ + + return r; } - foreach (Block block in Blocks) + void Print() { - Contract.Assert(block != null); - foreach (Cmd command in block.Cmds) + List tmp = Implementation.Blocks; + Contract.Assert(tmp != null); + Implementation.Blocks = Blocks; + ConditionGeneration.EmitImpl(Options, Run, false); + Implementation.Blocks = tmp; + } + + public Counterexample ToCounterexample(ProverContext context) + { + Contract.Requires(context != null); + Contract.Ensures(Contract.Result() != null); + + List trace = new List(); + foreach (Block block in Blocks) { - if (command is AssertCmd assertCmd) + Contract.Assert(block != null); + trace.Add(block); + } + + foreach (Block block in Blocks) + { + Contract.Assert(block != null); + foreach (Cmd command in block.Cmds) { - var counterexample = VerificationConditionGenerator.AssertCmdToCounterexample(Options, assertCmd, - cce.NonNull(block.TransferCmd), trace, null, null, null, context, this); - Counterexamples.Add(counterexample); - return counterexample; + if (command is AssertCmd assertCmd) + { + var counterexample = VerificationConditionGenerator.AssertCmdToCounterexample(Options, assertCmd, + cce.NonNull(block.TransferCmd), trace, null, null, null, context, this); + Counterexamples.Add(counterexample); + return counterexample; + } } } - } - Contract.Assume(false); - throw new cce.UnreachableException(); - } + Contract.Assume(false); + throw new cce.UnreachableException(); + } - public static List /*!*/ DoSplit(Split initial, double splitThreshold, int maxSplits) - { - Contract.Requires(initial != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); + 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 result = new List { initial }; + var run = initial.Run; + var result = new List { initial }; - while (result.Count < maxSplits) - { - Split best = null; - int bestIndex = 0; - for (var index = 0; index < result.Count; index++) { - var split = result[index]; - Contract.Assert(split != null); - split.ComputeBestSplit(); // TODO check totalCost first - if (split.totalCost > splitThreshold && - (best == null || best.totalCost < split.totalCost) && - (split.assertionCount > 1 || split.splitBlock != null)) { - best = split; - bestIndex = index; + while (result.Count < maxSplits) + { + Split best = null; + int bestIndex = 0; + for (var index = 0; index < result.Count; index++) + { + var split = result[index]; + Contract.Assert(split != null); + split.ComputeBestSplit(); // TODO check totalCost first + if (split.totalCost > splitThreshold && + (best == null || best.totalCost < split.totalCost) && + (split.assertionCount > 1 || split.splitBlock != null)) + { + best = split; + bestIndex = index; + } } - } - if (best == null) - { - break; // no split found - } + if (best == null) + { + break; // no split found + } - Split s0, s1; + Split s0, s1; - bool splitStats = initial.Options.TraceVerify; + bool splitStats = initial.Options.TraceVerify; - if (splitStats) - { - run.OutputWriter.WriteLine("{0} {1} -->", best.splitBlock == null ? "SLICE" : ("SPLIT@" + best.splitBlock.Label), - best.Stats); - if (best.splitBlock != null) + if (splitStats) { - GotoCmd g = best.splitBlock.TransferCmd as GotoCmd; - if (g != null) + run.OutputWriter.WriteLine("{0} {1} -->", + best.splitBlock == null ? "SLICE" : ("SPLIT@" + best.splitBlock.Label), + best.Stats); + if (best.splitBlock != null) { - run.OutputWriter.Write(" exits: "); - foreach (Block b in cce.NonNull(g.labelTargets)) - { - Contract.Assert(b != null); - run.OutputWriter.Write("{0} ", b.Label); - } - - run.OutputWriter.WriteLine(""); - run.OutputWriter.Write(" assumized: "); - foreach (Block b in best.assumizedBranches) + GotoCmd g = best.splitBlock.TransferCmd as GotoCmd; + if (g != null) { - Contract.Assert(b != null); - run.OutputWriter.Write("{0} ", b.Label); + run.OutputWriter.Write(" exits: "); + foreach (Block b in cce.NonNull(g.labelTargets)) + { + Contract.Assert(b != null); + run.OutputWriter.Write("{0} ", b.Label); + } + + run.OutputWriter.WriteLine(""); + run.OutputWriter.Write(" assumized: "); + foreach (Block b in best.assumizedBranches) + { + Contract.Assert(b != null); + run.OutputWriter.Write("{0} ", b.Label); + } + + run.OutputWriter.WriteLine(""); } - - run.OutputWriter.WriteLine(""); } } - } - - if (best.splitBlock != null) - { - s0 = best.SplitAt(0); - s1 = best.SplitAt(1); - } - else - { - best.splitBlock = null; - s0 = best.SliceAsserts(best.assertionCost / 2, true); - s1 = best.SliceAsserts(best.assertionCost / 2, false); - } - if (true) - { - var ss = new List - { - s0.Blocks[0], - s1.Blocks[0] - }; - try + if (best.splitBlock != null) { - best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.Blocks[0], ss); + s0 = best.SplitAt(0); + s1 = best.SplitAt(1); } - catch (Exception e) + else { - run.OutputWriter.WriteLine(e); - best.DumpDot(-1); - s0.DumpDot(-2); - s1.DumpDot(-3); - Contract.Assert(false); - throw new cce.UnreachableException(); + best.splitBlock = null; + s0 = best.SliceAsserts(best.assertionCost / 2, true); + s1 = best.SliceAsserts(best.assertionCost / 2, false); } - } - if (splitStats) - { - s0.ComputeBestSplit(); - s1.ComputeBestSplit(); - run.OutputWriter.WriteLine(" --> {0}", s0.Stats); - run.OutputWriter.WriteLine(" --> {0}", s1.Stats); - } - - if (initial.Options.TraceVerify) - { - best.Print(); - } + if (true) + { + var ss = new List + { + s0.Blocks[0], + s1.Blocks[0] + }; + try + { + best.SoundnessCheck(new HashSet>(new BlockListComparer()), best.Blocks[0], ss); + } + catch (Exception e) + { + run.OutputWriter.WriteLine(e); + best.DumpDot(-1); + s0.DumpDot(-2); + s1.DumpDot(-3); + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } - result[bestIndex] = s0; - result.Add(s1); - } + if (splitStats) + { + s0.ComputeBestSplit(); + s1.ComputeBestSplit(); + run.OutputWriter.WriteLine(" --> {0}", s0.Stats); + run.OutputWriter.WriteLine(" --> {0}", s1.Stats); + } - return result; - } + if (initial.Options.TraceVerify) + { + best.Print(); + } - public VerificationRunResult ReadOutcome(int iteration, Checker checker, VerifierCallback callback) - { - Contract.EnsuresOnThrow(true); - SolverOutcome outcome = cce.NonNull(checker).ReadOutcome(); + result[bestIndex] = s0; + result.Add(s1); + } - if (Options.Trace && SplitIndex >= 0) - { - 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}", - string.Join("\n ", CoveredElements.Select(s => s.Description).OrderBy(s => s))); + return result; } - var resourceCount = checker.GetProverResourceCount(); - var result = new VerificationRunResult( - vcNum: SplitIndex + 1, - Iteration: iteration, - StartTime: checker.ProverStart, - Outcome: outcome, - RunTime: checker.ProverRunTime, - MaxCounterExamples: checker.Options.ErrorLimit, - CounterExamples: Counterexamples, - Asserts: Asserts, - CoveredElements: CoveredElements, - ResourceCount: resourceCount, - SolverUsed: (Options as SMTLibSolverOptions)?.Solver); - callback.OnVCResult(result); - - if (Options.VcsDumpSplits) + public VerificationRunResult ReadOutcome(int iteration, Checker checker, VerifierCallback callback) { - DumpDot(SplitIndex); - } - - return result; - } - - public List Counterexamples { get; } = new(); - - public HashSet CoveredElements { get; } = new(); - - /// - /// As a side effect, updates "this.parent.CumulativeAssertionCount". - /// - public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCallback callback, ModelViewInfo mvInfo, uint timeout, - uint rlimit, CancellationToken cancellationToken) - { - Contract.Requires(checker != null); - Contract.Requires(callback != null); + Contract.EnsuresOnThrow(true); + SolverOutcome outcome = cce.NonNull(checker).ReadOutcome(); - VCExpr vc; - // Lock impl since we're setting impl.Blocks that is used to generate the VC. - lock (Implementation) { - Implementation.Blocks = Blocks; + if (Options.Trace && SplitIndex >= 0) + { + Run.OutputWriter.WriteLine(" --> split #{0} done, [{1} s] {2}", SplitIndex + 1, + checker.ProverRunTime.TotalSeconds, outcome); + } - var absyIds = new ControlFlowIdMap(); + if (Options.Trace && Options.TrackVerificationCoverage) + { + Run.OutputWriter.WriteLine("Proof dependencies:\n {0}", + string.Join("\n ", CoveredElements.Select(s => s.Description).OrderBy(s => s))); + } - ProverContext ctx = checker.TheoremProver.Context; - Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator; - var cc = new VerificationConditionGenerator.CodeExprConversionClosure(traceWriter, checker.Pool.Options, absyIds, ctx); - bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition); + var resourceCount = checker.GetProverResourceCount(); + var result = new VerificationRunResult( + vcNum: SplitIndex + 1, + Iteration: iteration, + StartTime: checker.ProverStart, + Outcome: outcome, + RunTime: checker.ProverRunTime, + MaxCounterExamples: checker.Options.ErrorLimit, + CounterExamples: Counterexamples, + Asserts: Asserts, + CoveredElements: CoveredElements, + ResourceCount: resourceCount, + SolverUsed: (Options as SMTLibSolverOptions)?.Solver); + callback.OnVCResult(result); + + if (Options.VcsDumpSplits) + { + DumpDot(SplitIndex); + } - var exprGen = ctx.ExprGen; - VCExpr controlFlowVariableExpr = exprGen.Integer(BigNum.ZERO); - vc = parent.GenerateVCAux(Implementation, controlFlowVariableExpr, absyIds, checker.TheoremProver.Context); - Contract.Assert(vc != null); + return result; + } - vc = QuantifierInstantiationEngine.Instantiate(Implementation, exprGen, bet, vc); + public List Counterexamples { get; } = new(); - VCExpr controlFlowFunctionAppl = - 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 VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, Implementation.Blocks, Implementation.debugInfos, callback, - mvInfo, checker.TheoremProver.Context, parent.program, this); - } + public HashSet CoveredElements { get; } = new(); - if (Options.TraceVerify && SplitIndex >= 0) + /// + /// As a side effect, updates "this.parent.CumulativeAssertionCount". + /// + public async Task BeginCheck(TextWriter traceWriter, Checker checker, VerifierCallback callback, + ModelViewInfo mvInfo, uint timeout, + uint rlimit, CancellationToken cancellationToken) { - Run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex); - Print(); - } + Contract.Requires(checker != null); + Contract.Requires(callback != null); - checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions().Select(kv => new OptionValue(kv.Key, kv.Value))); - await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken); - } + VCExpr vc; + // Lock impl since we're setting impl.Blocks that is used to generate the VC. + lock (Implementation) + { + Implementation.Blocks = Blocks; + + var absyIds = new ControlFlowIdMap(); + + ProverContext ctx = checker.TheoremProver.Context; + Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator; + var cc = new VerificationConditionGenerator.CodeExprConversionClosure(traceWriter, checker.Pool.Options, + absyIds, ctx); + bet.SetCodeExprConverter(cc.CodeExprToVerificationCondition); + + var exprGen = ctx.ExprGen; + VCExpr controlFlowVariableExpr = exprGen.Integer(BigNum.ZERO); + vc = parent.GenerateVCAux(Implementation, controlFlowVariableExpr, absyIds, checker.TheoremProver.Context); + Contract.Assert(vc != null); + + vc = QuantifierInstantiationEngine.Instantiate(Implementation, exprGen, bet, vc); + + VCExpr controlFlowFunctionAppl = + 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 VerificationConditionGenerator.ErrorReporter(Options, GotoCmdOrigins, absyIds, + Implementation.Blocks, Implementation.debugInfos, callback, + mvInfo, checker.TheoremProver.Context, parent.program, this); + } - public string Description - { - get - { - string description = cce.NonNull(Implementation.Name); - if (SplitIndex >= 0) { - description += "_split" + SplitIndex; + if (Options.TraceVerify && SplitIndex >= 0) + { + Run.OutputWriter.WriteLine("-- after split #{0}", SplitIndex); + Print(); } - return description; + checker.TheoremProver.SetAdditionalSmtOptions(Implementation.GetExtraSMTOptions() + .Select(kv => new OptionValue(kv.Key, kv.Value))); + await checker.BeginCheck(Description, vc, reporter, timeout, rlimit, cancellationToken); } - } - private void SoundnessCheck(HashSet /*!*/> /*!*/ cache, Block /*!*/ orig, - List /*!*/ copies) - { - Contract.Requires(cce.NonNull(cache)); - Contract.Requires(orig != null); - Contract.Requires(copies != null); + public string Description { - var t = new List {orig}; - foreach (Block b in copies) + get { - Contract.Assert(b != null); - t.Add(b); - } + string description = cce.NonNull(Implementation.Name); + if (SplitIndex >= 0) + { + description += "_split" + SplitIndex; + } - if (cache.Contains(t)) - { - return; + return description; } - - cache.Add(t); } - for (int i = 0; i < orig.Cmds.Count; ++i) + private void SoundnessCheck(HashSet /*!*/> /*!*/ cache, Block /*!*/ orig, + List /*!*/ copies) { - Cmd cmd = orig.Cmds[i]; - if (cmd is AssertCmd) + Contract.Requires(cce.NonNull(cache)); + Contract.Requires(orig != null); + Contract.Requires(copies != null); { - int found = 0; - foreach (Block c in copies) + var t = new List { orig }; + foreach (Block b in copies) { - Contract.Assert(c != null); - if (c.Cmds[i] == cmd) - { - found++; - } + Contract.Assert(b != null); + t.Add(b); } - if (found == 0) + if (cache.Contains(t)) { - throw new Exception(string.Format("missing assertion: {0}({1})", cmd.tok.filename, cmd.tok.line)); + return; } + + cache.Add(t); } - } - foreach (Block exit in orig.Exits()) - { - Contract.Assert(exit != null); - List newcopies = new List(); - foreach (Block c in copies) + for (int i = 0; i < orig.Cmds.Count; ++i) { - foreach (Block cexit in c.Exits()) + Cmd cmd = orig.Cmds[i]; + if (cmd is AssertCmd) { - Contract.Assert(cexit != null); - if (cexit.Label == exit.Label) + int found = 0; + foreach (Block c in copies) { - newcopies.Add(cexit); + Contract.Assert(c != null); + if (c.Cmds[i] == cmd) + { + found++; + } + } + + if (found == 0) + { + throw new Exception(string.Format("missing assertion: {0}({1})", cmd.tok.filename, cmd.tok.line)); } } } - if (newcopies.Count == 0) + foreach (Block exit in orig.Exits()) { - throw new Exception("missing exit " + exit.Label); - } + Contract.Assert(exit != null); + List newcopies = new List(); + foreach (Block c in copies) + { + foreach (Block cexit in c.Exits()) + { + Contract.Assert(cexit != null); + if (cexit.Label == exit.Label) + { + newcopies.Add(cexit); + } + } + } + + if (newcopies.Count == 0) + { + throw new Exception("missing exit " + exit.Label); + } - SoundnessCheck(cache, exit, newcopies); + SoundnessCheck(cache, exit, newcopies); + } } - } - public int NextRandom() { - return randomGen.Next(); + public int NextRandom() + { + return randomGen.Next(); + } } } \ No newline at end of file diff --git a/Source/VCGeneration/SplitAndVerifyWorker.cs b/Source/VCGeneration/SplitAndVerifyWorker.cs index fdecf765b..cbe258df6 100644 --- a/Source/VCGeneration/SplitAndVerifyWorker.cs +++ b/Source/VCGeneration/SplitAndVerifyWorker.cs @@ -8,297 +8,337 @@ using VCGeneration; using static VC.ConditionGeneration; -namespace VC; - -public class SplitAndVerifyWorker +namespace VC { - - private readonly VCGenOptions options; - private readonly VerifierCallback callback; - private readonly ModelViewInfo mvInfo; - private readonly ImplementationRun run; - - private readonly int maxKeepGoingSplits; - public List ManualSplits { get; } - private double maxVcCost; - - private bool DoSplitting => ManualSplits.Count > 1 || KeepGoing; - private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); - private bool KeepGoing => maxKeepGoingSplits > 1; - - private VcOutcome vcOutcome; - private double remainingCost; - private double provenCost; - private int total; - private int splitNumber; - - private int totalResourceCount; - - public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, ImplementationRun run, - Dictionary gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, - VcOutcome vcOutcome) + public class SplitAndVerifyWorker { - this.options = options; - this.callback = callback; - this.mvInfo = mvInfo; - this.run = run; - this.vcOutcome = vcOutcome; - var maxSplits = options.VcsMaxSplits; - VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits); - - maxKeepGoingSplits = options.VcsMaxKeepGoingSplits; - VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits); - - maxVcCost = options.VcsMaxCost; - var tmpMaxVcCost = -1; - VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost); - if (tmpMaxVcCost >= 0) - { - maxVcCost = tmpMaxVcCost; - } - - - ResetPredecessors(Implementation.Blocks); - ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator); - - if (ManualSplits.Count == 1 && maxSplits > 1) { - ManualSplits = Split.DoSplit(ManualSplits[0], maxVcCost, maxSplits); - maxVcCost = 1.0; - } - - splitNumber = DoSplitting ? 0 : -1; - } - public async Task WorkUntilDone(CancellationToken cancellationToken) - { - TrackSplitsCost(ManualSplits); - await Task.WhenAll(ManualSplits.Select(split => DoWorkForMultipleIterations(split, cancellationToken))); + private readonly VCGenOptions options; + private readonly VerifierCallback callback; + private readonly ModelViewInfo mvInfo; + private readonly ImplementationRun run; - return vcOutcome; - } + private readonly int maxKeepGoingSplits; + public List ManualSplits { get; } + private double maxVcCost; - public int ResourceCount => totalResourceCount; - - /// - /// The cumulative time spent processing SMT queries. When running with - /// `vcsCores > 1`, this may also include time spent restarting the prover. - /// - public TimeSpan TotalProverElapsedTime { get; private set; } - - private void TrackSplitsCost(List splits) - { - if (!TrackingProgress) + private bool DoSplitting => ManualSplits.Count > 1 || KeepGoing; + private bool TrackingProgress => DoSplitting && (callback.OnProgress != null || options.Trace); + private bool KeepGoing => maxKeepGoingSplits > 1; + + private VcOutcome vcOutcome; + private double remainingCost; + private double provenCost; + private int total; + private int splitNumber; + + private int totalResourceCount; + + public SplitAndVerifyWorker(VCGenOptions options, VerificationConditionGenerator verificationConditionGenerator, + ImplementationRun run, + Dictionary gotoCmdOrigins, VerifierCallback callback, ModelViewInfo mvInfo, + VcOutcome vcOutcome) { - return; - } + this.options = options; + this.callback = callback; + this.mvInfo = mvInfo; + this.run = run; + this.vcOutcome = vcOutcome; + var maxSplits = options.VcsMaxSplits; + VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_splits", ref maxSplits); + + maxKeepGoingSplits = options.VcsMaxKeepGoingSplits; + VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_keep_going_splits", ref maxKeepGoingSplits); + + maxVcCost = options.VcsMaxCost; + var tmpMaxVcCost = -1; + VerificationConditionGenerator.CheckIntAttributeOnImpl(run, "vcs_max_cost", ref tmpMaxVcCost); + if (tmpMaxVcCost >= 0) + { + maxVcCost = tmpMaxVcCost; + } - foreach (var split in splits) { - remainingCost += split.Cost; - total++; - } - } - async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellationToken) - { - int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1; - split.SplitIndex = currentSplitNumber; - var tasks = Enumerable.Range(0, options.RandomizeVcIterations).Select(iteration => - DoWork(iteration, split, cancellationToken)); - await Task.WhenAll(tasks); - } + ResetPredecessors(Implementation.Blocks); + ManualSplits = ManualSplitFinder.FocusAndSplit(options, run, gotoCmdOrigins, verificationConditionGenerator); - async Task DoWork(int iteration, Split split, CancellationToken cancellationToken) - { - var checker = await split.parent.CheckerPool.FindCheckerFor(split.parent.program, split, cancellationToken); - - try { - cancellationToken.ThrowIfCancellationRequested(); - await StartCheck(iteration, split, checker, cancellationToken); - await checker.ProverTask; - await ProcessResultAndReleaseChecker(iteration, split, checker, cancellationToken); - TotalProverElapsedTime += checker.ProverRunTime; - } - catch { - await checker.GoBackToIdle(); - throw; + if (ManualSplits.Count == 1 && maxSplits > 1) + { + ManualSplits = Split.DoSplit(ManualSplits[0], maxVcCost, maxSplits); + maxVcCost = 1.0; + } + + splitNumber = DoSplitting ? 0 : -1; } - } - private async Task StartCheck(int iteration, Split split, Checker checker, CancellationToken cancellationToken) - { - if (options.Trace && DoSplitting) { - var splitNum = split.SplitIndex + 1; - var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}"; - run.OutputWriter.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...", - split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost)); + public async Task WorkUntilDone(CancellationToken cancellationToken) + { + TrackSplitsCost(ManualSplits); + await Task.WhenAll(ManualSplits.Select(split => DoWorkForMultipleIterations(split, cancellationToken))); + + return vcOutcome; } - callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total, - provenCost / (remainingCost + provenCost)); + public int ResourceCount => totalResourceCount; - var timeout = KeepGoing && split.LastChance ? options.VcsFinalAssertTimeout : - KeepGoing ? options.VcsKeepGoingTimeout : - run.Implementation.GetTimeLimit(options); - await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, Implementation.GetResourceLimit(options), cancellationToken); - } + /// + /// The cumulative time spent processing SMT queries. When running with + /// `vcsCores > 1`, this may also include time spent restarting the prover. + /// + public TimeSpan TotalProverElapsedTime { get; private set; } - private Implementation Implementation => run.Implementation; + private void TrackSplitsCost(List splits) + { + if (!TrackingProgress) + { + return; + } - private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Checker checker, CancellationToken cancellationToken) - { - if (TrackingProgress) { - lock (this) { - remainingCost -= split.Cost; + foreach (var split in splits) + { + remainingCost += split.Cost; + total++; } } - var result = split.ReadOutcome(iteration, checker, callback); - lock (this) { - vcOutcome = MergeOutcomes(vcOutcome, result.Outcome); - totalResourceCount += result.ResourceCount; + async Task DoWorkForMultipleIterations(Split split, CancellationToken cancellationToken) + { + int currentSplitNumber = DoSplitting ? Interlocked.Increment(ref splitNumber) - 1 : -1; + split.SplitIndex = currentSplitNumber; + var tasks = Enumerable.Range(0, options.RandomizeVcIterations).Select(iteration => + DoWork(iteration, split, cancellationToken)); + await Task.WhenAll(tasks); } - var proverFailed = IsProverFailed(result.Outcome); - - if (TrackingProgress) { - lock (this) { - if (proverFailed) { - // even if the prover fails, we have learned something, i.e., it is - // annoying to watch Boogie say Timeout, 0.00% a couple of times - provenCost += split.Cost / 100; - } else { - provenCost += split.Cost; - } + + async Task DoWork(int iteration, Split split, CancellationToken cancellationToken) + { + var checker = await split.parent.CheckerPool.FindCheckerFor(split.parent.program, split, cancellationToken); + + try + { + cancellationToken.ThrowIfCancellationRequested(); + await StartCheck(iteration, split, checker, cancellationToken); + await checker.ProverTask; + await ProcessResultAndReleaseChecker(iteration, split, checker, cancellationToken); + TotalProverElapsedTime += checker.ProverRunTime; + } + catch + { + await checker.GoBackToIdle(); + throw; } } - callback.OnProgress?.Invoke("VCprove", splitNumber < 0 ? 0 : splitNumber, total, provenCost / (remainingCost + provenCost)); + private async Task StartCheck(int iteration, Split split, Checker checker, CancellationToken cancellationToken) + { + if (options.Trace && DoSplitting) + { + var splitNum = split.SplitIndex + 1; + var splitIdxStr = options.RandomizeVcIterations > 1 ? $"{splitNum} (iteration {iteration})" : $"{splitNum}"; + run.OutputWriter.WriteLine(" checking split {1}/{2}, {3:0.00}%, {0} ...", + split.Stats, splitIdxStr, total, 100 * provenCost / (provenCost + remainingCost)); + } - if (proverFailed) { - await HandleProverFailure(split, checker, callback, result, cancellationToken); - } else { - await checker.GoBackToIdle(); - } - } + callback.OnProgress?.Invoke("VCprove", split.SplitIndex, total, + provenCost / (remainingCost + provenCost)); - public static bool IsProverFailed(SolverOutcome outcome) - { - switch (outcome) - { - case SolverOutcome.Valid: - case SolverOutcome.Invalid: - case SolverOutcome.Undetermined: - return false; - case SolverOutcome.OutOfMemory: - case SolverOutcome.TimeOut: - case SolverOutcome.OutOfResource: - return true; - default: - Contract.Assert(false); - throw new cce.UnreachableException(); + var timeout = KeepGoing && split.LastChance ? options.VcsFinalAssertTimeout : + KeepGoing ? options.VcsKeepGoingTimeout : + run.Implementation.GetTimeLimit(options); + await split.BeginCheck(run.OutputWriter, checker, callback, mvInfo, timeout, + Implementation.GetResourceLimit(options), cancellationToken); } - } - private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome newOutcome) - { - switch (newOutcome) + private Implementation Implementation => run.Implementation; + + private async Task ProcessResultAndReleaseChecker(int iteration, Split split, Checker checker, + CancellationToken cancellationToken) { - case SolverOutcome.Valid: - return currentVcOutcome; - case SolverOutcome.Invalid: - return VcOutcome.Errors; - case SolverOutcome.OutOfMemory: - if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) + if (TrackingProgress) + { + lock (this) { - return VcOutcome.OutOfMemory; + remainingCost -= split.Cost; } + } - return currentVcOutcome; - case SolverOutcome.TimeOut: - if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) - { - return VcOutcome.TimedOut; - } + var result = split.ReadOutcome(iteration, checker, callback); + lock (this) + { + vcOutcome = MergeOutcomes(vcOutcome, result.Outcome); + totalResourceCount += result.ResourceCount; + } - return currentVcOutcome; - case SolverOutcome.OutOfResource: - if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) - { - return VcOutcome.OutOfResource; - } + var proverFailed = IsProverFailed(result.Outcome); - return currentVcOutcome; - case SolverOutcome.Undetermined: - if (currentVcOutcome != VcOutcome.Errors) + if (TrackingProgress) + { + lock (this) { - return VcOutcome.Inconclusive; + if (proverFailed) + { + // even if the prover fails, we have learned something, i.e., it is + // annoying to watch Boogie say Timeout, 0.00% a couple of times + provenCost += split.Cost / 100; + } + else + { + provenCost += split.Cost; + } } - return currentVcOutcome; - default: - Contract.Assert(false); - throw new cce.UnreachableException(); + } + + callback.OnProgress?.Invoke("VCprove", splitNumber < 0 ? 0 : splitNumber, total, + provenCost / (remainingCost + provenCost)); + + if (proverFailed) + { + await HandleProverFailure(split, checker, callback, result, cancellationToken); + } + else + { + await checker.GoBackToIdle(); + } } - } - private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, VerificationRunResult verificationRunResult, CancellationToken cancellationToken) - { - if (split.LastChance) { - string msg = "some timeout"; - if (split.reporter is { resourceExceededMessage: { } }) { - msg = split.reporter.resourceExceededMessage; + public static bool IsProverFailed(SolverOutcome outcome) + { + switch (outcome) + { + case SolverOutcome.Valid: + case SolverOutcome.Invalid: + case SolverOutcome.Undetermined: + return false; + case SolverOutcome.OutOfMemory: + case SolverOutcome.TimeOut: + case SolverOutcome.OutOfResource: + return true; + default: + Contract.Assert(false); + throw new cce.UnreachableException(); } + } - var cex = split.ToCounterexample(checker.TheoremProver.Context); - callback.OnCounterexample(cex, msg); - split.Counterexamples.Add(cex); - // Update one last time the result with the dummy counter-example to indicate the position of the timeout - var result = verificationRunResult with { - CounterExamples = split.Counterexamples - }; - vcOutcome = VcOutcome.Errors; - await checker.GoBackToIdle(); - return; + private static VcOutcome MergeOutcomes(VcOutcome currentVcOutcome, SolverOutcome newOutcome) + { + switch (newOutcome) + { + case SolverOutcome.Valid: + return currentVcOutcome; + case SolverOutcome.Invalid: + return VcOutcome.Errors; + case SolverOutcome.OutOfMemory: + if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) + { + return VcOutcome.OutOfMemory; + } + + return currentVcOutcome; + case SolverOutcome.TimeOut: + if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) + { + return VcOutcome.TimedOut; + } + + return currentVcOutcome; + case SolverOutcome.OutOfResource: + if (currentVcOutcome != VcOutcome.Errors && currentVcOutcome != VcOutcome.Inconclusive) + { + return VcOutcome.OutOfResource; + } + + return currentVcOutcome; + case SolverOutcome.Undetermined: + if (currentVcOutcome != VcOutcome.Errors) + { + return VcOutcome.Inconclusive; + } + + return currentVcOutcome; + default: + Contract.Assert(false); + throw new cce.UnreachableException(); + } } - await checker.GoBackToIdle(); + private async Task HandleProverFailure(Split split, Checker checker, VerifierCallback callback, + VerificationRunResult verificationRunResult, CancellationToken cancellationToken) + { + if (split.LastChance) + { + string msg = "some timeout"; + if (split.reporter is { resourceExceededMessage: { } }) + { + msg = split.reporter.resourceExceededMessage; + } - if (maxKeepGoingSplits > 1) { - var newSplits = Split.DoSplit(split, maxVcCost, maxKeepGoingSplits); - if (options.Trace) { - await run.OutputWriter.WriteLineAsync($"split {split.SplitIndex+1} was split into {newSplits.Count} parts"); - } - Contract.Assert(newSplits != null); - maxVcCost = 1.0; // for future - TrackSplitsCost(newSplits); - - if (vcOutcome != VcOutcome.Errors) { - vcOutcome = VcOutcome.Correct; + var cex = split.ToCounterexample(checker.TheoremProver.Context); + callback.OnCounterexample(cex, msg); + split.Counterexamples.Add(cex); + // Update one last time the result with the dummy counter-example to indicate the position of the timeout + var result = verificationRunResult with + { + CounterExamples = split.Counterexamples + }; + vcOutcome = VcOutcome.Errors; + await checker.GoBackToIdle(); + return; } - await Task.WhenAll(newSplits.Select(newSplit => DoWorkForMultipleIterations(newSplit, cancellationToken))); - return; - } - Contract.Assert(vcOutcome != VcOutcome.Correct); - if (vcOutcome == VcOutcome.TimedOut) { - string msg = "some timeout"; - if (split.reporter is { resourceExceededMessage: { } }) { - msg = split.reporter.resourceExceededMessage; + await checker.GoBackToIdle(); + + if (maxKeepGoingSplits > 1) + { + var newSplits = Split.DoSplit(split, maxVcCost, maxKeepGoingSplits); + if (options.Trace) + { + await run.OutputWriter.WriteLineAsync($"split {split.SplitIndex + 1} was split into {newSplits.Count} parts"); + } + + Contract.Assert(newSplits != null); + maxVcCost = 1.0; // for future + TrackSplitsCost(newSplits); + + if (vcOutcome != VcOutcome.Errors) + { + vcOutcome = VcOutcome.Correct; + } + + await Task.WhenAll(newSplits.Select(newSplit => DoWorkForMultipleIterations(newSplit, cancellationToken))); + return; } - callback.OnTimeout(msg); - } else if (vcOutcome == VcOutcome.OutOfMemory) { - string msg = "out of memory"; - if (split.reporter is { resourceExceededMessage: { } }) { - msg = split.reporter.resourceExceededMessage; + Contract.Assert(vcOutcome != VcOutcome.Correct); + if (vcOutcome == VcOutcome.TimedOut) + { + string msg = "some timeout"; + if (split.reporter is { resourceExceededMessage: { } }) + { + msg = split.reporter.resourceExceededMessage; + } + + callback.OnTimeout(msg); } + else if (vcOutcome == VcOutcome.OutOfMemory) + { + string msg = "out of memory"; + if (split.reporter is { resourceExceededMessage: { } }) + { + msg = split.reporter.resourceExceededMessage; + } - callback.OnOutOfMemory(msg); - } else if (vcOutcome == VcOutcome.OutOfResource) { - string msg = "out of resource"; - if (split.reporter is { resourceExceededMessage: { } }) { - msg = split.reporter.resourceExceededMessage; + callback.OnOutOfMemory(msg); } + else if (vcOutcome == VcOutcome.OutOfResource) + { + string msg = "out of resource"; + if (split.reporter is { resourceExceededMessage: { } }) + { + msg = split.reporter.resourceExceededMessage; + } - callback.OnOutOfResource(msg); + callback.OnOutOfResource(msg); + } } } } \ No newline at end of file