Boogie: add /printCFG command line option, which prints each implementation's CFG in Graphviz format

3 files changed, 33 insertions, 0 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 44adce15..ae26d8db 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -18,6 +18,7 @@ namespace Microsoft.Boogie {
   using Microsoft.Boogie.AbstractInterpretation;

   using System.Diagnostics.Contracts;

   using System.Diagnostics;

+  using System.Linq;

   using VC;

   using AI = Microsoft.AbstractInterpretationFramework;

   using BoogiePL = Microsoft.Boogie;

@@ -178,6 +179,14 @@ namespace Microsoft.Boogie {
           return;

         }

 

+        if (CommandLineOptions.Clo.PrintCFGPrefix != null) {

+          foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>()) {

+            using (StreamWriter sw = new StreamWriter(CommandLineOptions.Clo.PrintCFGPrefix + "." + impl.Name + ".dot")) {

+              sw.Write(program.ProcessLoops(impl).ToDot());

+            }

+          }

+        }

+

         EliminateDeadVariablesAndInline(program);

 

         int errorCount, verified, inconclusives, timeOuts, outOfMemories;

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index c28d8c8a..7d55e177 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -450,6 +450,7 @@ namespace Microsoft.Boogie {
     public string PrintErrorModelFile = null;

     public string/*?*/ ModelViewFile = null;

     public int EnhancedErrorMessages = 0;

+    public string PrintCFGPrefix = null;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public bool UseArrayTheory = false;

     public bool UseLabels = true;

@@ -834,6 +835,12 @@ namespace Microsoft.Boogie {
           ps.GetNumericArgument(ref EnhancedErrorMessages, 2);

           return true;

 

+        case "printCFG":

+          if (ps.ConfirmArgumentCount(1)) {

+            PrintCFGPrefix = args[ps.i];

+          }

+          return true;

+

         case "inlineDepth":

           ps.GetNumericArgument(ref InlineDepth);

           return true;

@@ -1449,6 +1456,10 @@ namespace Microsoft.Boogie {
                 0 (default) - no enhanced error messages

                 1 - Z3 error model enhanced error messages

 

+  /printCFG:<prefix> : print control flow graph of each implementation in

+                       Graphviz format to files named:

+                         <prefix>.<procedure name>.dot

+

   ---- Inference options -----------------------------------------------------

 

   /infer:<flags>

diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs
index e5e8444c..b5590865 100644
--- a/Source/Graph/Graph.cs
+++ b/Source/Graph/Graph.cs
@@ -843,6 +843,19 @@ namespace Graphing {
         }

         return dag.TopologicalSort();

     }

+

+    public string ToDot(Func<Node, string> NodeLabel = null, Func<Node, string> NodeStyle = null) {

+      NodeLabel = NodeLabel ?? (n => n.ToString());

+      NodeStyle = NodeStyle ?? (n => "[shape=box]");

+      var s = new StringBuilder();

+      s.AppendLine("digraph G {");

+      foreach (var n in Nodes)

+        s.AppendLine("  \"" + NodeLabel(n) + "\" " + NodeStyle(n) + ";");

+      foreach (var e in Edges)

+        s.AppendLine("  \"" + NodeLabel(e.Item1) + "\" -> \"" + NodeLabel(e.Item2) + "\";");

+      s.AppendLine("}");

+      return s.ToString();

+    }

   } // end: class Graph

 

   public class GraphProgram {