Merge pull request diffblue#226 from diffblue/feature/goto_statistics

SEC-41 : Introducing GOTO program statistics.

Author: marek-trtik

cbmc/src/goto-programs/goto_statistics.cpp

@@ -0,0 +1,79 @@
+/*******************************************************************\
+
+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 && name_symbol.second.is_state_var)
+    {
+      if(name_symbol.second.is_auxiliary)
+        ++num_auxiliary_variables;
+      else
+        ++num_user_variables;
+    }
+  }
+}
+
+jsont to_json(const goto_statisticst &stats)
+{
+  json_objectt json_stats;
+  json_stats["num_functions"]=
+    json_numbert(std::to_string(stats.get_num_functions()));
+  json_stats["num_instructions"]=
+    json_numbert(std::to_string(stats.get_num_instructions()));
+  json_stats["num_user_variables"]=
+    json_numbert(std::to_string(stats.get_num_user_variables()));
+  json_stats["num_auxiliary_variables"]=
+    json_numbert(std::to_string(stats.get_num_auxiliary_variables()));
+  json_stats["num_function_calls"]=
+    json_numbert(std::to_string(stats.get_num_function_calls()));
+  json_stats["num_unconditional_gotos"]=
+    json_numbert(std::to_string(stats.get_num_unconditional_gotos()));
+  json_stats["num_conditional_gotos"]=
+    json_numbert(std::to_string(stats.get_num_conditional_gotos()));
+  json_stats["num_loops"]=
+    json_numbert(std::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 statistical 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_user_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_user_variables() const
+  {
+    return num_user_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_user_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
+