Add code to calculate various interesting statistics about Dafny files.

4 files changed, 175 insertions, 5 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 125ab11e..af940439 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -56,6 +56,8 @@ namespace Microsoft.Dafny
     public bool AllowGlobals = false;

     public bool CountVerificationErrors = true;

     public bool Optimize = false;

+    public bool PrintStats = false;

+    public bool PrintFunctionCallGraph = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

       var args = ps.args;  // convenient synonym

@@ -172,6 +174,14 @@ namespace Microsoft.Dafny
         case "allowGlobals":

           AllowGlobals = true;

           return true;

+        

+        case "stats":

+          PrintStats = true;

+          return true;

+

+        case "funcCallGraph":

+          PrintFunctionCallGraph = true;

+          return true;

 

         case "countVerificationErrors": {

           int countErrors = 1; // defaults to reporting verification errors

@@ -267,7 +277,7 @@ namespace Microsoft.Dafny
   /noAutoReq    Ignore autoReq attributes

   /allowGlobals Allow the implicit class '_default' to contain fields, instance functions,

                 and instance methods.  These class members are declared at the module scope,

-                outside of explicit classes.  This command-line option is provided to simply

+                outside of explicit classes.  This command-line option is provided to simplify

                 a transition from the behavior in the language prior to version 1.9.3, from

                 which point onward all functions and methods declared at the module scope are

                 implicitly static and fields declarations are not allowed at the module scope.

@@ -282,6 +292,8 @@ namespace Microsoft.Dafny
                     System.Collections.Immutable.dll in the source directory to successfully 

                     compile).

                   - passes /optimize flag to csc.exe.

+  /stats        Print interesting statistics about the Dafny files supplied.

+  /funcCallGraph Print out the function call graph.  Format is: func,mod=callee*

 ");

       base.Usage();  // also print the Boogie options

     }

diff --git a/Source/Dafny/SccGraph.cs b/Source/Dafny/SccGraph.cs
index 01a72fc5..20b4f65e 100644
--- a/Source/Dafny/SccGraph.cs
+++ b/Source/Dafny/SccGraph.cs
@@ -6,8 +6,8 @@ namespace Microsoft.Dafny {
 

   public class Graph<Node> where Node : class

   {

-    enum VisitedStatus { Unvisited, OnStack, Visited }

-    class Vertex {

+    public enum VisitedStatus { Unvisited, OnStack, Visited }

+    public class Vertex {

       public readonly Node N;

       public readonly List<Vertex/*!*/>/*!*/ Successors = new List<Vertex/*!*/>();

       public List<Vertex/*!*/> SccMembers;  // non-null only for the representative of the SCC

@@ -65,6 +65,10 @@ namespace Microsoft.Dafny {
     {

     }

 

+    public IEnumerable<Vertex> GetVertices() {

+      return vertices.Values;

+    }

+

     /// <summary>

     /// Idempotently adds a vertex 'n' to the graph.

     /// </summary>

@@ -97,7 +101,7 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Returns the vertex for 'n' if 'n' is in the graph.  Otherwise, returns null.

     /// </summary>

-    Vertex FindVertex(Node n) {

+    public Vertex FindVertex(Node n) {

       Vertex v;

       if (vertices.TryGetValue(n, out v)) {

         Contract.Assert(v != null);  // follows from postcondition of TryGetValue (since 'vertices' maps to the type Vertex!)

diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs
index f9421659..63659696 100644
--- a/Source/Dafny/Util.cs
+++ b/Source/Dafny/Util.cs
@@ -8,7 +8,7 @@ using Microsoft.Boogie;
 

 

 namespace Microsoft.Dafny {

-  class Util

+  public class Util

   {

     public static string Comma<T>(IEnumerable<T> l, Func<T, string> f) {

       return Comma(",", l, f);

@@ -175,5 +175,152 @@ namespace Microsoft.Dafny {
       }

     }

 

+    /// <summary>

+    /// Class dedicated to traversing the function call graph

+    /// </summary>

+    class FunctionCallFinder : TopDownVisitor<List<Function>> {

+      protected override bool VisitOneExpr(Expression expr, ref List<Function> calls) {

+        if (expr is FunctionCallExpr) {

+          calls.Add(((FunctionCallExpr)expr).Function);

+        }

+        return true;

+      }

+    }

+

+    static Graph<Function> BuildFunctionCallGraph(Dafny.Program program) {

+      Graph<Function> functionCallGraph = new Graph<Function>();

+      FunctionCallFinder callFinder = new FunctionCallFinder();

+

+      foreach (var module in program.Modules) {

+        foreach (var decl in module.TopLevelDecls) {

+          if (decl is ClassDecl) {

+            var c = (ClassDecl)decl;

+            foreach (var member in c.Members) {

+              if (member is Function) {

+                var f = (Function)member;

+

+                List<Function> calls = new List<Function>();

+                foreach (var e in f.Reads) { if (e != null && e.E != null) { callFinder.Visit(e.E, calls); } }

+                foreach (var e in f.Req) { if (e != null) { callFinder.Visit(e, calls); } }

+                foreach (var e in f.Ens) { if (e != null) { callFinder.Visit(e, calls); } }

+                if (f.Body != null) {

+                  callFinder.Visit(f.Body, calls);

+                }

+

+                foreach (var callee in calls) {

+                  functionCallGraph.AddEdge(f, callee);

+                }

+              }

+            }

+          }

+        }

+      }

+

+      return functionCallGraph;

+    }

+

+    /// <summary>

+    /// Prints the program's function call graph in a format suitable for consumption in other tools

+    /// </summary>

+    public static void PrintFunctionCallGraph(Dafny.Program program) {

+      var functionCallGraph = BuildFunctionCallGraph(program);

+

+      foreach (var vertex in functionCallGraph.GetVertices()) {

+        var func = vertex.N;

+        Console.Write("{0},{1}=", func.CompileName, func.EnclosingClass.Module.CompileName);

+        foreach (var callee in vertex.Successors) {

+          Console.Write("{0} ", callee.N.CompileName);

+        }

+        Console.Write("\n");

+      }

+    }

+

+    /// <summary>

+    /// Generic statistic counter

+    /// </summary>

+    static void IncrementStat(IDictionary<string, ulong> stats, string stat) {

+      ulong currentValue;

+      if (stats.TryGetValue(stat, out currentValue)) {

+        stats[stat] += 1;

+      } else {

+        stats.Add(stat, 1);

+      }

+    }

+

+    /// <summary>

+    /// Track the maximum value of some statistic

+    /// </summary>

+    static void UpdateMax(IDictionary<string, ulong> stats, string stat, ulong val) {

+      ulong currentValue;

+      if (stats.TryGetValue(stat, out currentValue)) {

+        if (val > currentValue) {

+          stats[stat] = val;

+        }

+      } else {

+        stats.Add(stat, val);

+      }

+    }

+

+    /// <summary>

+    /// Compute various interesting statistics about the Dafny program

+    /// </summary>

+    public static void PrintStats(Dafny.Program program) {

+      SortedDictionary<string, ulong> stats = new SortedDictionary<string, ulong>();

+

+      foreach (var module in program.Modules) {

+        IncrementStat(stats, "Modules");

+        UpdateMax(stats, "Module height (max)", (ulong)module.Height);

+

+        ulong num_scc = (ulong)module.CallGraph.TopologicallySortedComponents().Count;

+        UpdateMax(stats, "Call graph width (max)", num_scc);

+

+        foreach (var decl in module.TopLevelDecls) {

+          if (decl is DatatypeDecl) {

+            IncrementStat(stats, "Datatypes");

+          } else if (decl is ClassDecl) {

+            var c = (ClassDecl)decl;

+            if (c.Name != "_default") {

+              IncrementStat(stats, "Classes");

+            }

+

+            foreach (var member in c.Members) {

+              if (member is Function) {

+                IncrementStat(stats, "Functions (total)");

+                var f = (Function)member;

+                if (f.IsRecursive) {

+                  IncrementStat(stats, "Functions recursive");

+                }

+              } else if (member is Method) {

+                IncrementStat(stats, "Methods (total)");

+                var method = (Method)member;

+                if (method.IsRecursive) {

+                  IncrementStat(stats, "Methods recursive");

+                }

+                if (method.IsGhost) {

+                  IncrementStat(stats, "Methods ghost");

+                }

+              }

+            }

+          }

+        }

+      }

+

+      // Print out the results, with some nice formatting

+      Console.WriteLine("");

+      Console.WriteLine("Statistics");

+      Console.WriteLine("----------");

+

+      int max_key_length = 0;

+      foreach (var key in stats.Keys) {

+        if (key.Length > max_key_length) {

+          max_key_length = key.Length;

+        }

+      }

+

+      foreach (var keypair in stats) {

+        string keyString = keypair.Key.PadRight(max_key_length + 2);

+        Console.WriteLine("{0} {1,4}", keyString, keypair.Value);

+      }

+    }

   }

 }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index ce4d726f..9fdc9320 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -199,6 +199,13 @@ namespace Microsoft.Dafny
           }

           exitValue = allOk ? ExitValue.VERIFIED : ExitValue.NOT_VERIFIED;

         }

+

+        if (err == null && dafnyProgram != null && DafnyOptions.O.PrintStats) {

+          Util.PrintStats(dafnyProgram);

+        }

+        if (err == null && dafnyProgram != null && DafnyOptions.O.PrintFunctionCallGraph) {

+          Util.PrintFunctionCallGraph(dafnyProgram);

+        }

       }

       return exitValue;

     }