added more instrumentation to Houdini

when vcgen fails, instead of stopping houdini, the failing vc is added to a list of blacklisted vcs
fixed bug in the call graph generation when inlining is used

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;