Merge pull request #2236 from diffblue/show-class-hierarchy

JSON output for show-class-hierarchy

Author: peterschrammel

jbmc/regression/jbmc/class_hierarchy/HierarchyTest.class

@@ -0,0 +1,18 @@
+public abstract class HierarchyTest {
+  // These fields exist only so the classloader will load all test classes:
+  HierarchyTestGrandchild field1;
+  HierarchyTestChild2 field2;
+
+  abstract void foo();
+}
+
+class HierarchyTestChild1 extends HierarchyTest {
+  void foo() {}
+}
+
+class HierarchyTestChild2 extends HierarchyTest {
+  void foo() {}
+}
+
+class HierarchyTestGrandchild extends HierarchyTestChild1
+  implements HierarchyTestInterface1, HierarchyTestInterface2 {}

jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java

@@ -0,0 +1 @@
+interface HierarchyTestInterface1 {}

jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild1.class

@@ -0,0 +1 @@
+interface HierarchyTestInterface2 {}

jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild2.class

@@ -0,0 +1,7 @@
+CORE symex-driven-lazy-loading-expected-failure
+HierarchyTest.class
+--show-class-hierarchy --json-ui
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+\{\n *"isAbstract": true,\n *"name": "java::HierarchyTest",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestChild(1|2)",\n *"java::HierarchyTestChild(1|2)"\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestGrandchild",\n *"parents": \[\n *"java::HierarchyTestChild1",\n *"java::HierarchyTestInterface1",\n *"java::HierarchyTestInterface2"\n *\],\n *"children": \[\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestChild2",\n *"parents": \[\n *"java::HierarchyTest"\n *\],\n *"children": \[\n *\]\n *\},\n *\{\n *"isAbstract": false,\n *"name": "java::HierarchyTestChild1",\n *"parents": \[\n *"java::HierarchyTest"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},\n *\{\n *"isAbstract": true,\n *"name": "java::HierarchyTestInterface1",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},\n *\{\n *"isAbstract": true,\n *"name": "java::HierarchyTestInterface2",\n *"parents": \[\n *"java::java.lang.Object"\n *\],\n *"children": \[\n *"java::HierarchyTestGrandchild"\n *\]\n *\},

jbmc/regression/jbmc/class_hierarchy/HierarchyTestGrandchild.class

@@ -0,0 +1,7 @@
+CORE symex-driven-lazy-loading-expected-failure
+HierarchyTest.class
+--show-class-hierarchy
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+java::HierarchyTest \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestChild(1|2)\n *java::HierarchyTestChild(1|2)\njava::HierarchyTestGrandchild:\n *parents:\n *java::HierarchyTestChild1\n *java::HierarchyTestInterface1\n *java::HierarchyTestInterface2\n *children:\njava::HierarchyTestChild2:\n *parents:\n *java::HierarchyTest\n *children:\njava::HierarchyTestChild1:\n *parents:\n *java::HierarchyTest\n *children:\n *java::HierarchyTestGrandchild\njava::HierarchyTestInterface1 \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestGrandchild\njava::HierarchyTestInterface2 \(abstract\):\n *parents:\n *java::java\.lang\.Object\n *children:\n *java::HierarchyTestGrandchild

jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.class

@@ -645,6 +645,16 @@ int jbmc_parse_optionst::get_goto_program(
       *this, options, get_message_handler());
     lazy_goto_model.initialize(cmdline);
 
+    // Show the class hierarchy
+    if(cmdline.isset("show-class-hierarchy"))
+    {
+      class_hierarchyt hierarchy;
+      hierarchy(lazy_goto_model.symbol_table);
+      show_class_hierarchy(
+        hierarchy, get_message_handler(), ui_message_handler.get_ui());
+      return CPROVER_EXIT_SUCCESS;
+    }
+
     // Add failed symbols for any symbol created prior to loading any
     // particular function:
     add_failed_symbols(lazy_goto_model.symbol_table);
@@ -1079,6 +1089,7 @@ void jbmc_parse_optionst::help()
     " --show-symbol-table          show loaded symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
+    HELP_SHOW_CLASS_HIERARCHY
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK

jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java

@@ -22,10 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cbmc/bmc.h>
 
+#include <goto-instrument/cover.h>
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_trace.h>
 #include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/show_properties.h>
-#include <goto-instrument/cover.h>
 
 #include <goto-symex/path_storage.h>
 
@@ -60,6 +61,7 @@ class optionst;
   "(string-max-input-length):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_CLASS_HIERARCHY \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
   OPT_SHOW_PROPERTIES \

jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.class

@@ -17,21 +17,15 @@
 void require_parent_child_relationship(
   const std::string &parent_raw,
   const std::string &child_raw,
-  const std::string &output,
   const std::string &output_dot)
 {
   std::string parent = "java::" + parent_raw;
   std::string child = "java::" + child_raw;
 
-  std::stringstream
-    plain_child_expectation, plain_parent_expectation, dot_expectation;
+  std::stringstream dot_expectation;
 
-  plain_child_expectation << "Child of " << parent << ": " << child;
-  plain_parent_expectation << "Parent of " << child << ": " << parent;
   dot_expectation << "\"" << child << "\" -> \"" << parent << "\"";
 
-  REQUIRE(output.find(plain_child_expectation.str()) != std::string::npos);
-  REQUIRE(output.find(plain_parent_expectation.str()) != std::string::npos);
   REQUIRE(output_dot.find(dot_expectation.str()) != std::string::npos);
 }
 
@@ -47,20 +41,18 @@ SCENARIO(
   std::stringstream output_dot_stream;
 
   hierarchy(symbol_table);
-  hierarchy.output(output_stream);
   hierarchy.output_dot(output_dot_stream);
 
-  std::string output = output_stream.str();
   std::string output_dot = output_dot_stream.str();
 
   require_parent_child_relationship(
-    "HierarchyTest", "HierarchyTestChild1", output, output_dot);
+    "HierarchyTest", "HierarchyTestChild1", output_dot);
   require_parent_child_relationship(
-    "HierarchyTest", "HierarchyTestChild2", output, output_dot);
+    "HierarchyTest", "HierarchyTestChild2", output_dot);
   require_parent_child_relationship(
-    "HierarchyTestChild1", "HierarchyTestGrandchild", output, output_dot);
+    "HierarchyTestChild1", "HierarchyTestGrandchild", output_dot);
   require_parent_child_relationship(
-    "HierarchyTestInterface1", "HierarchyTestGrandchild", output, output_dot);
+    "HierarchyTestInterface1", "HierarchyTestGrandchild", output_dot);
   require_parent_child_relationship(
-    "HierarchyTestInterface2", "HierarchyTestGrandchild", output, output_dot);
+    "HierarchyTestInterface2", "HierarchyTestGrandchild", output_dot);
 }

jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java

@@ -1,6 +1,6 @@
 CORE
 main.c
---class-hierarchy --dot
+--show-class-hierarchy --dot
 digraph class_hierarchy
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/class_hierarchy/test_json.desc

@@ -1,5 +1,5 @@
 CORE
 main.c
---class-hierarchy
+--show-class-hierarchy
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/jbmc/class_hierarchy/test_plain.desc

@@ -652,16 +652,17 @@ int goto_instrument_parse_optionst::doit()
       return 0;
     }
 
-    if(cmdline.isset("class-hierarchy"))
+    if(cmdline.isset("show-class-hierarchy"))
     {
       class_hierarchyt hierarchy;
       hierarchy(goto_model.symbol_table);
       if(cmdline.isset("dot"))
         hierarchy.output_dot(std::cout);
       else
-        hierarchy.output(std::cout);
+        show_class_hierarchy(
+          hierarchy, get_message_handler(), ui_message_handler.get_ui());
 
-      return 0;
+      return CPROVER_EXIT_SUCCESS;
     }
 
     if(cmdline.isset("dot"))
@@ -1472,7 +1473,7 @@ void goto_instrument_parse_optionst::help()
     " --call-graph                 show graph of function calls\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --reachable-call-graph       show graph of function calls potentially reachable from main function\n"
-    " --class-hierarchy            show class hierarchy\n"
+    HELP_SHOW_CLASS_HIERARCHY
     // NOLINTNEXTLINE(whitespace/line_length)
     " --show-threaded              show instructions that may be executed by more than one thread\n"
     "\n"

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -16,11 +16,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 
+#include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_functions.h>
-#include <goto-programs/show_goto_functions.h>
-#include <goto-programs/show_properties.h>
 #include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_const_function_pointers.h>
+#include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 
 #include <analyses/goto_check.h>
 
@@ -50,7 +51,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(max-var):(max-po-trans):(ignore-arrays)" \
   "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
   "(call-graph)(reachable-call-graph)" \
-  "(class-hierarchy)" \
+  OPT_SHOW_CLASS_HIERARCHY \
   "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
   "(nondet-volatile)(isr):" \
   "(stack-depth):(nondet-static)" \

jbmc/src/jbmc/jbmc_parse_options.h

@@ -15,6 +15,7 @@ Date: April 2016
 
 #include <ostream>
 
+#include <util/json_stream.h>
 #include <util/std_types.h>
 #include <util/symbol_table.h>
 
@@ -30,6 +31,9 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
     {
       const struct_typet &struct_type = to_struct_type(symbol_pair.second.type);
 
+      class_map[symbol_pair.first].is_abstract =
+        struct_type.get_bool(ID_abstract);
+
       const irept::subt &bases=
         struct_type.find(ID_bases).get_sub();
 
@@ -123,17 +127,23 @@ void class_hierarchyt::get_parents_trans_rec(
     get_parents_trans_rec(child, dest);
 }
 
-void class_hierarchyt::output(std::ostream &out) const
+/// Output the class hierarchy in plain text
+/// \param out: the output stream
+/// \param children_only: print the children only and do not print the parents
+void class_hierarchyt::output(std::ostream &out, bool children_only) const
 {
   for(const auto &c : class_map)
   {
-    for(const auto &pa : c.second.parents)
-      out << "Parent of " << c.first << ": "
-          << pa << '\n';
-
+    out << c.first << (c.second.is_abstract ? " (abstract)" : "") << ":\n";
+    if(!children_only)
+    {
+      out << "  parents:\n";
+      for(const auto &pa : c.second.parents)
+        out << "    " << pa << '\n';
+    }
+    out << "  children:\n";
     for(const auto &ch : c.second.children)
-      out << "Child of " << c.first << ": "
-          << ch << '\n';
+      out << "    " << ch << '\n';
   }
 }
 
@@ -156,3 +166,50 @@ void class_hierarchyt::output_dot(std::ostream &ostr) const
   }
   ostr << "}\n";
 }
+
+/// Output the class hierarchy in JSON format
+/// \param json_stream: the output JSON stream array
+/// \param children_only: print the children only and do not print the parents
+void class_hierarchyt::output(
+  json_stream_arrayt &json_stream,
+  bool children_only) const
+{
+  for(const auto &c : class_map)
+  {
+    json_stream_objectt &json_class = json_stream.push_back_stream_object();
+    json_class["name"] = json_stringt(c.first);
+    json_class["isAbstract"] = jsont::json_boolean(c.second.is_abstract);
+    if(!children_only)
+    {
+      json_stream_arrayt &json_parents =
+        json_class.push_back_stream_array("parents");
+      for(const auto &pa : c.second.parents)
+        json_parents.push_back(json_stringt(pa));
+    }
+    json_stream_arrayt &json_children =
+      json_class.push_back_stream_array("children");
+    for(const auto &ch : c.second.children)
+      json_children.push_back(json_stringt(ch));
+  }
+}
+
+void show_class_hierarchy(
+  const class_hierarchyt &hierarchy,
+  message_handlert &message_handler,
+  ui_message_handlert::uit ui,
+  bool children_only)
+{
+  messaget msg(message_handler);
+  switch(ui)
+  {
+  case ui_message_handlert::uit::PLAIN:
+    hierarchy.output(msg.result(), children_only);
+    msg.result() << messaget::eom;
+    break;
+  case ui_message_handlert::uit::JSON_UI:
+    hierarchy.output(msg.result().json_stream(), children_only);
+    break;
+  case ui_message_handlert::uit::XML_UI:
+    UNIMPLEMENTED;
+  }
+}

jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp

@@ -20,8 +20,19 @@ Date: April 2016
 
 #include <util/graph.h>
 #include <util/irep.h>
+#include <util/ui_message.h>
+
+// clang-format off
+#define OPT_SHOW_CLASS_HIERARCHY \
+  "(show-class-hierarchy)"
+
+#define HELP_SHOW_CLASS_HIERARCHY \
+  " --show-class-hierarchy       show the class hierarchy\n"
+// clang-format on
 
 class symbol_tablet;
+class json_stream_arrayt;
+class message_handlert;
 
 class class_hierarchyt
 {
@@ -32,6 +43,7 @@ class class_hierarchyt
   {
   public:
     idst parents, children;
+    bool is_abstract;
   };
 
   typedef std::map<irep_idt, entryt> class_mapt;
@@ -55,8 +67,9 @@ class class_hierarchyt
     return result;
   }
 
-  void output(std::ostream &) const;
+  void output(std::ostream &, bool children_only) const;
   void output_dot(std::ostream &) const;
+  void output(json_stream_arrayt &, bool children_only) const;
 
 protected:
   void get_children_trans_rec(const irep_idt &, idst &) const;
@@ -93,4 +106,15 @@ class class_hierarchy_grapht : public grapht<class_hierarchy_graph_nodet>
   nodes_by_namet nodes_by_name;
 };
 
+/// Output the class hierarchy
+/// \param hierarchy: the class hierarchy to be printed
+/// \param message_handler: the message handler
+/// \param ui: the UI format
+/// \param children_only: print the children only and do not print the parents
+void show_class_hierarchy(
+  const class_hierarchyt &hierarchy,
+  message_handlert &message_handler,
+  ui_message_handlert::uit ui,
+  bool children_only = false);
+
 #endif // CPROVER_GOTO_PROGRAMS_CLASS_HIERARCHY_H