diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 4 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 6 | ||||
| -rw-r--r-- | Source/Graph/Graph.cs | 19 |
3 files changed, 25 insertions, 4 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index 96d68bec..e5c52add 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -136,6 +136,10 @@ <Project>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</Project>
<Name>SMTLib</Name>
</ProjectReference>
+ <ProjectReference Include="..\Provers\Z3api\Z3api.csproj">
+ <Project>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</Project>
+ <Name>Z3api</Name>
+ </ProjectReference>
<ProjectReference Include="..\Provers\Z3\Z3.csproj">
<Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
<Name>Z3</Name>
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index c2ef05f9..52b802a8 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -362,7 +362,6 @@ namespace Microsoft.Boogie { void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g, List<Implementation/*!*/>/*!*/ loopImpls) {
Contract.Requires(impl != null);
Contract.Requires(cce.NonNullElements(loopImpls));
- Contract.Requires(cce.NonNullElements(g.TopologicalSort()));
// Enumerate the headers
// for each header h:
// create implementation p_h with
@@ -454,7 +453,9 @@ namespace Microsoft.Boogie { loopHeaderToCallCmd[header] = callCmd;
}
- foreach (Block/*!*/ header in g.Headers) {
+ IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();
+ foreach (Block/*!*/ header in sortedHeaders)
+ {
Contract.Assert(header != null);
LoopProcedure loopProc = loopHeaderToLoopProc[header];
Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();
@@ -608,7 +609,6 @@ namespace Microsoft.Boogie { Implementation impl = d as Implementation;
if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {
Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);
- Contract.Assert(cce.NonNullElements(g.TopologicalSort()));
g.ComputeLoops();
if (!g.Reducible) {
throw new Exception("Irreducible flow graphs are unsupported.");
diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 768f499e..6bfd5c34 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -761,7 +761,24 @@ namespace Graphing { return;
}
-
+ public IEnumerable<Node> SortHeadersByDominance()
+ {
+ Graph<Node> dag = new Graph<Node>();
+ foreach (Node b in headers)
+ {
+ dag.AddSource(b);
+ foreach (Node c in headers)
+ {
+ if (b.Equals(c)) continue;
+ if (DominatorMap.DominatedBy(b, c))
+ {
+ Debug.Assert(!DominatorMap.DominatedBy(c, b));
+ dag.AddEdge(b, c);
+ }
+ }
+ }
+ return dag.TopologicalSort();
+ }
} // end: class Graph
public class GraphProgram {
|