Introducing GOTO program statistics.

The module collects a basic summary statistical information about
passed GOTO program. Data like number of variables, functions,
loops, conditional jumps, etc. are collected.

The statistical data are especially useful for raw comparison of two
GOTO programs. For instance, it can tell us how effective was program
slicing.

Author: marek-trtik

cbmc/src/goto-programs/goto_statistics.cpp

@@ -0,0 +1,89 @@
+/*******************************************************************\
+
+Module: goto_statistics.cpp
+
+Author: Marek Trtik
+
+\*******************************************************************/
+
+#include "goto_statistics.h"
+#include <sstream>
+
+void goto_statisticst::extend(
+  const goto_functionst &functions,
+  const symbol_tablet & table)
+{
+  for(auto const &elem : functions.function_map)
+  {
+    for(const auto &instr : elem.second.body.instructions)
+    {
+      switch(instr.type)
+      {
+        case FUNCTION_CALL:
+          ++num_function_calls;
+          break;
+        case ASSERT:
+          ++num_assertions;
+          break;
+        case ASSUME:
+          ++num_assumptions;
+          break;
+        case GOTO:
+          if (instr.guard.is_true())
+            ++num_unconditional_gotos;
+          else
+            ++num_conditional_gotos;
+          if(instr.is_backwards_goto())
+            ++num_loops;
+          break;
+        default:
+          break;
+      }
+      ++num_instructions;
+    }
+    ++num_functions;
+  }
+  for(const auto &name_symbol : table.symbols)
+  {
+    if(name_symbol.second.is_lvalue and name_symbol.second.is_state_var)
+    {
+      if(name_symbol.second.is_auxiliary)
+        ++num_auxiliary_variables;
+      else
+        ++num_genuine_variables;
+    }
+  }
+}
+
+jsont to_json(const goto_statisticst &stats)
+{
+  struct localt
+  {
+    static std::string to_string(const std::size_t number)
+    {
+      std::stringstream sstr;
+      sstr << number;
+      return sstr.str();
+    }
+  };
+
+  json_objectt json_stats;
+  json_stats["num_functions"]=
+    json_numbert(localt::to_string(stats.get_num_functions()));
+  json_stats["num_instructions"]=
+    json_numbert(localt::to_string(stats.get_num_instructions()));
+  json_stats["num_genuine_variables"]=
+    json_numbert(localt::to_string(stats.get_num_genuine_variables()));
+  json_stats["num_auxiliary_variables"]=
+    json_numbert(localt::to_string(stats.get_num_auxiliary_variables()));
+  json_stats["num_function_calls"]=
+    json_numbert(localt::to_string(stats.get_num_function_calls()));
+  json_stats["num_unconditional_gotos"]=
+    json_numbert(localt::to_string(stats.get_num_unconditional_gotos()));
+  json_stats["num_conditional_gotos"]=
+    json_numbert(localt::to_string(stats.get_num_conditional_gotos()));
+  json_stats["num_loops"]=
+    json_numbert(localt::to_string(stats.get_num_loops()));
+
+  return json_stats;
+}

cbmc/src/goto-programs/goto_statistics.h

@@ -0,0 +1,102 @@
+/*******************************************************************\
+
+Module: goto_statistics.h
+
+Author: Marek Trtik
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_PROGRAMS_GOTO_STATISTICS_H
+#define CPROVER_GOTO_PROGRAMS_GOTO_STATISTICS_H
+
+/// \file goto-programs/goto_statistics.h
+/// \brief Computation of statistal properties of a GOTO program.
+
+#include <cstddef>
+#include <util/json.h>
+#include "goto_model.h"
+
+class goto_statisticst
+{
+public:
+  goto_statisticst():
+    num_functions(0UL),
+    num_instructions(0UL),
+    num_genuine_variables(0UL),
+    num_auxiliary_variables(0UL),
+    num_function_calls(0UL),
+    num_unconditional_gotos(0UL),
+    num_conditional_gotos(0UL),
+    num_assumptions(0UL),
+    num_assertions(0UL),
+    num_loops(0UL)
+  {}
+
+  void extend(
+    const goto_functionst &functions,
+    const symbol_tablet &table);
+
+  void extend(const goto_modelt &model)
+  {
+    extend(model.goto_functions, model.symbol_table);
+  }
+
+  void clear() { *this=goto_statisticst(); }
+
+  std::size_t get_num_functions() const
+  {
+    return num_functions;
+  }
+
+  std::size_t get_num_instructions() const
+  {
+    return num_instructions;
+  }
+
+  std::size_t get_num_genuine_variables() const
+  {
+    return num_genuine_variables;
+  }
+
+  std::size_t get_num_auxiliary_variables() const
+  {
+    return num_auxiliary_variables;
+  }
+
+  std::size_t get_num_function_calls() const
+  {
+    return num_function_calls;
+  }
+
+  std::size_t get_num_unconditional_gotos() const
+  {
+    return num_unconditional_gotos;
+  }
+
+  std::size_t get_num_conditional_gotos() const
+  {
+    return num_conditional_gotos;
+  }
+
+  std::size_t get_num_loops() const
+  {
+    return num_loops;
+  }
+
+private:
+  std::size_t num_functions;
+  std::size_t num_instructions;
+  std::size_t num_genuine_variables;
+  std::size_t num_auxiliary_variables;
+  std::size_t num_function_calls;
+  std::size_t num_unconditional_gotos;
+  std::size_t num_conditional_gotos;
+  std::size_t num_assumptions;
+  std::size_t num_assertions;
+  std::size_t num_loops;
+};
+
+jsont to_json(const goto_statisticst &stats);
+
+#endif
+