diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 57 |
2 files changed, 52 insertions, 7 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 58731f10..eab8bc36 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -390,6 +390,8 @@ namespace Microsoft.Boogie { // Coalesce blocks
if (CommandLineOptions.Clo.CoalesceBlocks) {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Coalescing blocks...");
Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index ed3d1afc..986bc80c 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -255,25 +255,46 @@ namespace Microsoft.Boogie.Houdini { private Checker checker;
private Graph<Implementation> callGraph;
private bool continueAtError;
+ private HashSet<Implementation> vcgenFailures;
public Houdini(Program program, bool continueAtError) {
this.program = program;
- this.callGraph = BuildCallGraph();
this.continueAtError = continueAtError;
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Collecting existential constants...");
this.houdiniConstants = CollectExistentialConstants();
+
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Building call graph...");
+ this.callGraph = BuildCallGraph();
+
Inline();
+
this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
this.checker = new Checker(vcgen, program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+ vcgenFailures = new HashSet<Implementation>();
Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Beginning VC generation for Houdini...");
foreach (Implementation impl in callGraph.Nodes) {
- // make a different simplify log file for each function
- String simplifyLog = null;
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
+ try {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Generating VC for {0}", impl.Name);
+ // make a different simplify log file for each function
+ String simplifyLog = null;
+ if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
+ simplifyLog = impl.ToString() + CommandLineOptions.Clo.SimplifyLogFilePath;
+ }
+ HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ houdiniSessions.Add(impl, session);
+ }
+ catch (VCGenException) {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("VC generation failed");
+ vcgenFailures.Add(impl);
}
- HoudiniSession session = new HoudiniSession(vcgen, checker, program, impl, simplifyLog, CommandLineOptions.Clo.SimplifyLogFileAppend);
- houdiniSessions.Add(impl, session);
}
this.houdiniSessions = new ReadOnlyDictionary<Implementation, HoudiniSession>(houdiniSessions);
}
@@ -281,6 +302,7 @@ namespace Microsoft.Boogie.Houdini { private void Inline() {
if (CommandLineOptions.Clo.InlineDepth < 0)
return;
+
foreach (Implementation impl in callGraph.Nodes) {
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
@@ -292,6 +314,23 @@ namespace Microsoft.Boogie.Houdini { impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
}
+
+ int count = CommandLineOptions.Clo.InlineDepth;
+ Graph<Implementation> oldCallGraph = callGraph;
+ while (count > 0) {
+ callGraph = new Graph<Implementation>();
+ foreach (Tuple<Implementation, Implementation> edge in oldCallGraph.Edges) {
+ callGraph.AddEdge(edge.Item1, edge.Item2);
+ }
+ foreach (Implementation impl in oldCallGraph.Nodes) {
+ foreach (Implementation succ0 in oldCallGraph.Successors(impl)) {
+ foreach (Implementation succ1 in oldCallGraph.Successors(succ0)) {
+ callGraph.AddEdge(impl, succ1);
+ }
+ }
+ }
+ count--;
+ }
}
private ReadOnlyDictionary<string, IdentifierExpr> CollectExistentialConstants() {
@@ -349,6 +388,7 @@ namespace Microsoft.Boogie.Houdini { sccs.Compute();
foreach (SCC<Implementation> scc in sccs) {
foreach (Implementation impl in scc) {
+ if (vcgenFailures.Contains(impl)) continue;
queue.Enqueue(impl);
}
}
@@ -806,6 +846,9 @@ namespace Microsoft.Boogie.Houdini { public HoudiniOutcome PerformHoudiniInference() {
HoudiniState current = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants.Keys));
this.NotifyStart(program, houdiniConstants.Keys.Count);
+ foreach (Implementation impl in vcgenFailures) {
+ current.addToBlackList(impl.Name);
+ }
while (current.WorkQueue.Count > 0) {
bool exceptional = false;
|