From 2a8bc979f0c122ba7362335a1fea364a3b1ab122 Mon Sep 17 00:00:00 2001 From: Bryan Parno Date: Tue, 16 Dec 2014 14:03:19 -0800 Subject: Added an annotation, :split_here, for predicate statements. The annotation allows the programmer to manually indicate where the verification of a procedure implementation should be split into pieces. --- Source/VCGeneration/VC.cs | 150 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 147 insertions(+), 3 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 5e83a337..b989c029 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1056,6 +1056,141 @@ namespace VC { throw new cce.UnreachableException(); } + /// + /// Starting from the 0-index "split_here" annotation in begin, verifies until it reaches a subsequent "split_here" annotation + /// Returns a list of blocks where all code not verified has asserts converted into assumes + /// + /// Implementation's collection of blocks + /// Block containing the first split_here from which to start verifying + /// 0-based ID of the "split_here" annotation within begin at which to start verifying + /// True if the entire split is contained within block begin + /// Set of all blocks containing a "split_here" annotation + /// + // Note: Current implementation may over report errors. + // For example, if the control flow graph is a diamond (e.g., A -> B, C, B->D, C->D), + // and there is a split in B and an error in D, then D will be verified twice and hence report the error twice. + // Best solution may be to memoize blocks that have been fully verified and be sure not to verify them again + private static List DoManualSplit(List blocks, Block begin, int begin_split_id, bool blockInternalSplit, IEnumerable endPoints) { + // Compute the set of blocks reachable from begin but not included in endPoints. These will be verified in their entirety. + var blocksToVerifyEntirely = new HashSet(); + var reachableEndPoints = new HashSet(); // Reachable end points will be verified up to their first split point + var todo = new Stack(); + todo.Push(begin); + while (todo.Count > 0) { + var currentBlock = todo.Pop(); + if (blocksToVerifyEntirely.Contains(currentBlock)) continue; + blocksToVerifyEntirely.Add(currentBlock); + var exit = currentBlock.TransferCmd as GotoCmd; + if (exit != null) + foreach (Block targetBlock in exit.labelTargets) { + if (!endPoints.Contains(targetBlock)) { + todo.Push(targetBlock); + } else { + reachableEndPoints.Add(targetBlock); + } + } + + } + blocksToVerifyEntirely.Remove(begin); + + // Convert assumes to asserts in "unreachable" blocks, including portions of blocks containing "split_here" + 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 (!blockInternalSplit && blocksToVerifyEntirely.Contains(currentBlock)) continue; // All reachable blocks must be checked in their entirety, so don't change anything + // Otherwise, we only verify a portion of the current block, so we'll need to look at each of its commands + + // !verify -> convert assert to assume + var verify = (currentBlock == begin && begin_split_id == -1) // -1 tells us to start verifying from the very beginning (i.e., there is no split in the begin block) + || (reachableEndPoints.Contains(currentBlock) // This endpoint is reachable from begin, so we verify until we hit the first split point + && !blockInternalSplit); // Don't bother verifying if all of the splitting is within the begin block + var newCmds = new List(); + var split_here_count = 0; + + foreach (Cmd c in currentBlock.Cmds) { + var p = c as PredicateCmd; + if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "split_here")) { + if (currentBlock == begin) { // Verify everything between the begin_split_id we were given and the next split + if (split_here_count == begin_split_id) { + verify = true; + } else if (split_here_count == begin_split_id + 1) { + verify = false; + } + } else { // We're in an endPoint so we stop verifying as soon as we hit a "split_here" + verify = false; + } + split_here_count++; + } + + var asrt = c as AssertCmd; + if (verify || asrt == null) + newCmds.Add(c); + else + newCmds.Add(AssertTurnedIntoAssume(asrt)); + } + + newBlock.Cmds = newCmds; + } + + // 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; + } + + public static List FindManualSplits(Implementation/*!*/ impl, Dictionary/*!*/ gotoCmdOrigins, VCGen/*!*/ par) { + Contract.Requires(impl != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + + var splitPoints = new Dictionary(); + foreach (var b in impl.Blocks) { + foreach (Cmd c in b.Cmds) { + var p = c as PredicateCmd; + if (p != null && QKeyValue.FindBoolAttribute(p.Attributes, "split_here")) { + int count; + splitPoints.TryGetValue(b, out count); + splitPoints[b] = count + 1; + } + } + } + + if (splitPoints.Count() == 0) { // No manual split points here + return null; + } + + List splits = new List(); + Block entryPoint = impl.Blocks[0]; + var newEntryBlocks = DoManualSplit(impl.Blocks, entryPoint, -1, splitPoints.Keys.Contains(entryPoint), splitPoints.Keys); + splits.Add(new Split(newEntryBlocks, gotoCmdOrigins, par, impl)); // REVIEW: Does gotoCmdOrigins need to be changed at all? + + foreach (KeyValuePair pair in splitPoints) { + for (int i = 0; i < pair.Value; i++) { + bool blockInternalSplit = i < pair.Value - 1; // There's at least one more split, after this one, in the current block + var newBlocks = DoManualSplit(impl.Blocks, pair.Key, i, blockInternalSplit, splitPoints.Keys); + Split s = new Split(newBlocks, gotoCmdOrigins, par, impl); // REVIEW: Does gotoCmdOrigins need to be changed at all? + splits.Add(s); + } + } + + return splits; + } + public static List/*!*/ DoSplit(Split initial, double max_cost, int max) { Contract.Requires(initial != null); Contract.Ensures(cce.NonNullElements(Contract.Result>())); @@ -1639,7 +1774,14 @@ namespace VC { Stack work = new Stack(); List currently_running = new List(); ResetPredecessors(impl.Blocks); - work.Push(new Split(impl.Blocks, gotoCmdOrigins, this, impl)); + List manual_splits = Split.FindManualSplits(impl, gotoCmdOrigins, this); + if (manual_splits != null) { + foreach (var split in manual_splits) { + work.Push(split); + } + } else { + work.Push(new Split(impl.Blocks, gotoCmdOrigins, this, impl)); + } bool keep_going = max_kg_splits > 1; int total = 0; @@ -2710,6 +2852,7 @@ namespace VC { } } + // Compute the set of blocks reachable from blocks containing "start_checking_here" var blocksToCheck = new HashSet(); foreach (var b in startPoints) { var todo = new Stack(); @@ -2726,9 +2869,10 @@ namespace VC { } if (!wasThere) blocksToCheck.Remove(b); } - + + // Convert asserts to assumes in "unreachable" blocks, as well as in portions of blocks before we reach "start_checking_here" foreach (var b in impl.Blocks) { - if (blocksToCheck.Contains(b)) continue; + if (blocksToCheck.Contains(b)) continue; // All reachable blocks must be checked in their entirety, so don't change anything var newCmds = new List(); var copyMode = false; foreach (Cmd c in b.Cmds) { -- cgit v1.2.3