diff options
| author |  tabarbe <unknown> | 2010-07-16 22:25:27 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-16 22:25:27 +0000 |
| commit | 951ae331104cd20be6241b009ead77bef850fdb9 (patch) | |
| tree | cd23025f598ed472b790775eb92ef85671cbe0d3 /Source/AbsInt/Traverse.cs | |
| parent | 555a2a738b4ff6410e2096937e5d924bea617b9a (diff) | |
Boogie: Renamed the AbsInt sources for use in the port I have done. Regressions with the changed code will take ~10 minutes. I hope I don't break anyone's build.
Diffstat (limited to 'Source/AbsInt/Traverse.cs')
| -rw-r--r-- | Source/AbsInt/Traverse.cs | 182 |
1 files changed, 182 insertions, 0 deletions
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs new file mode 100644 index 00000000..694811da --- /dev/null +++ b/Source/AbsInt/Traverse.cs @@ -0,0 +1,182 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie
+{
+ using System;
+ using System.Collections.Generic;
+ using Microsoft.Contracts;
+
+ /// <summary>
+ /// This class provides the functionality of traversing a program to determine which
+ /// blocks are blocks where the widening operator may need to be applied. Assumes
+ /// all 'currentlyTraversed' bits to be initially false, and leaves them that way in
+ /// the end. Assumes the 'widenBlock' bits are initially false, and sets them
+ /// appropriately.
+ /// </summary>
+ public class WidenPoints
+ {
+ /// <summary>
+ /// Compute the widen points of a program
+ /// </summary>
+ public static void Compute(Program! program)
+ {
+ expose (program)
+ {
+ foreach (Declaration m in program.TopLevelDeclarations)
+ {
+ Implementation impl = m as Implementation;
+ if (impl != null)
+ {
+ if (impl.Blocks != null && impl.Blocks.Count > 0)
+ {
+ assume impl.IsConsistent;
+ expose (impl) {
+ Block start = impl.Blocks[0];
+ assume start != null;
+ assume start.IsConsistent;
+ Visit(start);
+
+ // We reset the state...
+ foreach(Block b in impl.Blocks) {
+ expose (b) {
+ b.TraversingStatus = Block.VisitState.ToVisit;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ static void Visit(Block! b)
+ {
+ assume b.IsExposable;
+ if (b.TraversingStatus == Block.VisitState.BeingVisited)
+ {
+ expose (b)
+ {
+ // we got here through a back-edge
+ b.widenBlock = true;
+ }
+ }
+ else if(b.TraversingStatus == Block.VisitState.AlreadyVisited)
+ {
+ // do nothing... we already saw this node
+ }
+ else if (b.TransferCmd is GotoCmd)
+ {
+ assert b.TraversingStatus == Block.VisitState.ToVisit;
+
+ GotoCmd g = (GotoCmd)b.TransferCmd;
+ expose (b)
+ {
+ expose (g) { //PM: required for the subsequent expose (g.labelTargets)
+ b.TraversingStatus = Block.VisitState.BeingVisited;
+
+ // labelTargets is made non-null by Resolve, which we assume
+ // has already called in a prior pass.
+ assume g.labelTargets != null;
+ expose (g.labelTargets) {
+ foreach (Block succ in g.labelTargets)
+// invariant b.currentlyTraversed;
+ //PM: The following loop invariant will work once properties are axiomatized
+ //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length);
+ {
+ assert succ != null;
+ Visit(succ);
+ }
+ }
+
+ assert b.TraversingStatus == Block.VisitState.BeingVisited;
+// System.Diagnostics.Debug.Assert(b.currentlyTraversed);
+
+ b.TraversingStatus = Block.VisitState.AlreadyVisited;
+
+ //PM: The folowing assumption is needed because we cannot prove that a simple field update
+ //PM: leaves the value of a property unchanged.
+ assume (g.labelNames != null ==> g.labelNames.Length == g.labelTargets.Length);
+ }
+ }
+ }
+ else
+ {
+ assert b.TransferCmd == null || b.TransferCmd is ReturnCmd; // It must be a returnCmd;
+ }
+ }
+
+ static private Block rootBlock = null; // The root point we have to consider
+
+ /// <summary>
+ /// Compute the blocks in the body loop.
+ /// <param name ="block"> Tt is the head of the loop. It must be a widen block </param>
+ /// <return> The blocks that are in the loop from block </return>
+ /// </summary>
+ public static List<Block!> ComputeLoopBodyFrom(Block! block)
+ requires block.widenBlock;
+ {
+ assert rootBlock == null;
+ rootBlock = block;
+
+ List<Block!> blocksInLoop = new List<Block!>(); // We use a list just because .net does not define a set
+ List<Block!> visitingPath = new List<Block!>(); // The order is important, as we want paths
+
+ blocksInLoop.Add(block);
+
+ DoDFSVisit(block, visitingPath, blocksInLoop);
+
+ visitingPath.Add(block);
+
+
+ rootBlock = null; // We reset the invariant
+
+ return blocksInLoop;
+ }
+
+ /// <summary>
+ /// Perform the Depth-first search of the so to find the loop
+ /// <param name = "block"> The block to visit </param>
+ /// <param name = "path"> The path we are visiting so far </param>
+ /// </summary>
+ private static void DoDFSVisit(Block! block, List<Block!>! path, List<Block!>! blocksInPath)
+ {
+ #region case 1. We visit the root => We are done, "path" is a path inside the loop
+ if(block == rootBlock && path.Count > 1)
+ {
+ blocksInPath.AddRange(path); // Add all the blocks in this path
+ }
+
+ #endregion
+ #region case 2. We visit a node that ends with a return => "path" is not inside the loop
+ if(block.TransferCmd is ReturnCmd)
+ {
+ return;
+ }
+ #endregion
+ #region case 3. We visit a node with successors => continue the exploration of its successors
+ {
+ assert block.TransferCmd is GotoCmd;
+ GotoCmd! successors = (GotoCmd) block.TransferCmd;
+
+ if (successors.labelTargets != null)
+ foreach (Block! nextBlock in successors.labelTargets)
+ {
+ if(path.Contains(nextBlock)) // If the current path has already seen the block, just skip it
+ continue;
+ // Otherwise we perform the DFS visit
+ path.Add(nextBlock);
+ DoDFSVisit(nextBlock, path, blocksInPath);
+
+ assert nextBlock == path[path.Count-1];
+ path.RemoveAt(path.Count-1);
+ }
+
+ }
+
+ #endregion
+ }
+ }
+}
|