1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
namespace Microsoft.Boogie {
using System;
using System.Collections.Generic;
using System.Diagnostics.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) {
Contract.Requires(program != null);
cce.BeginExpose(program);
foreach (Declaration m in program.TopLevelDeclarations) {
Implementation impl = m as Implementation;
if (impl != null) {
if (impl.Blocks != null && impl.Blocks.Count > 0) {
Contract.Assume(cce.IsConsistent(impl));
cce.BeginExpose(impl);
Block start = impl.Blocks[0];
Contract.Assume(start != null);
Contract.Assume(cce.IsConsistent(start));
Visit(start);
// We reset the state...
foreach (Block b in impl.Blocks) {
cce.BeginExpose(b);
b.TraversingStatus = Block.VisitState.ToVisit;
cce.EndExpose();
}
cce.EndExpose();
}
}
}
cce.EndExpose();
}
static void Visit(Block b) {
Contract.Requires(b != null);
Contract.Assume(cce.IsExposable(b));
if (b.TraversingStatus == Block.VisitState.BeingVisited) {
cce.BeginExpose(b);
// we got here through a back-edge
b.widenBlock = true;
cce.EndExpose();
} else if (b.TraversingStatus == Block.VisitState.AlreadyVisited) {
// do nothing... we already saw this node
} else if (b.TransferCmd is GotoCmd) {
Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);
GotoCmd g = (GotoCmd)b.TransferCmd;
cce.BeginExpose(b);
cce.BeginExpose(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.
Contract.Assume(g.labelTargets != null);
cce.BeginExpose(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);
{
Contract.Assert(succ != null);
Visit(succ);
}
cce.EndExpose();
Contract.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.
Contract.Assume(g.labelNames == null || g.labelNames.Length == g.labelTargets.Length);
cce.EndExpose();
} else {
Contract.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) {
Contract.Requires(block.widenBlock);
Contract.Requires(block != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
Contract.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) {
Contract.Requires(block != null);
Contract.Requires(cce.NonNullElements(path));
Contract.Requires(cce.NonNullElements(path));
#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
{
Contract.Assert(block.TransferCmd is GotoCmd);
GotoCmd successors = (GotoCmd)block.TransferCmd;
Contract.Assert(successors != null);
if (successors.labelTargets != null)
foreach (Block nextBlock in successors.labelTargets) {
Contract.Assert(nextBlock != null);
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);
Contract.Assert(nextBlock == path[path.Count - 1]);
path.RemoveAt(path.Count - 1);
}
}
#endregion
}
}
}
|
