Add and unify --show-class-hierarchy command line option

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, [email protected]
 
 #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

@@ -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/HierarchyTestInterface2.java

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

jbmc/regression/jbmc/class_hierarchy/test_json.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, false);
+        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/regression/jbmc/class_hierarchy/test_plain.desc

@@ -16,11 +16,12 @@ Author: Daniel Kroening, [email protected]
 #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, [email protected]
   "(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.cpp

@@ -192,3 +192,24 @@ void class_hierarchyt::output(
       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/src/jbmc/jbmc_parse_options.h

@@ -20,9 +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
 {
@@ -96,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