diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.class new file mode 100644 index 00000000000..26c221c378b Binary files /dev/null and b/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.class differ diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java b/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java new file mode 100644 index 00000000000..2379460e758 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/HierarchyTest.java @@ -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 {} diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild1.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild1.class new file mode 100644 index 00000000000..4c2de35ba53 Binary files /dev/null and b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild1.class differ diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild2.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild2.class new file mode 100644 index 00000000000..9115bd86b11 Binary files /dev/null and b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestChild2.class differ diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestGrandchild.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestGrandchild.class new file mode 100644 index 00000000000..bb429b7bc9b Binary files /dev/null and b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestGrandchild.class differ diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.class new file mode 100644 index 00000000000..a015b79c4f9 Binary files /dev/null and b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.class differ diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java new file mode 100644 index 00000000000..47d1a8ddd62 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface1.java @@ -0,0 +1 @@ +interface HierarchyTestInterface1 {} diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.class b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.class new file mode 100644 index 00000000000..14eb47f7656 Binary files /dev/null and b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.class differ diff --git a/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java new file mode 100644 index 00000000000..bee58260862 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/HierarchyTestInterface2.java @@ -0,0 +1 @@ +interface HierarchyTestInterface2 {} diff --git a/jbmc/regression/jbmc/class_hierarchy/test_json.desc b/jbmc/regression/jbmc/class_hierarchy/test_json.desc new file mode 100644 index 00000000000..1a61736d0b1 --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/test_json.desc @@ -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 *\}, diff --git a/jbmc/regression/jbmc/class_hierarchy/test_plain.desc b/jbmc/regression/jbmc/class_hierarchy/test_plain.desc new file mode 100644 index 00000000000..fa11b97bfeb --- /dev/null +++ b/jbmc/regression/jbmc/class_hierarchy/test_plain.desc @@ -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 diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 630fc2a283a..a498ab73879 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -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 diff --git a/jbmc/src/jbmc/jbmc_parse_options.h b/jbmc/src/jbmc/jbmc_parse_options.h index 6de84d59d97..616b1d1b9d9 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.h +++ b/jbmc/src/jbmc/jbmc_parse_options.h @@ -22,10 +22,11 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include +#include #include #include #include -#include #include @@ -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 \ diff --git a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp index 75970716f91..cb8566296f8 100644 --- a/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp +++ b/jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp @@ -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); } diff --git a/regression/goto-instrument/class-hierarchy/dot.desc b/regression/goto-instrument/class-hierarchy/dot.desc index 77ea28c0e76..e164706a3cc 100644 --- a/regression/goto-instrument/class-hierarchy/dot.desc +++ b/regression/goto-instrument/class-hierarchy/dot.desc @@ -1,6 +1,6 @@ CORE main.c ---class-hierarchy --dot +--show-class-hierarchy --dot digraph class_hierarchy ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/class-hierarchy/plain.desc b/regression/goto-instrument/class-hierarchy/plain.desc index 52367db0168..88144582815 100644 --- a/regression/goto-instrument/class-hierarchy/plain.desc +++ b/regression/goto-instrument/class-hierarchy/plain.desc @@ -1,5 +1,5 @@ CORE main.c ---class-hierarchy +--show-class-hierarchy ^EXIT=0$ ^SIGNAL=0$ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 66feb778817..013a206a00b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -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" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 185b793a3a1..60fbe8bd485 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -16,11 +16,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include -#include #include #include +#include +#include #include @@ -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)" \ diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp index 7f0e7fe558b..e5fbb743019 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -15,6 +15,7 @@ Date: April 2016 #include +#include #include #include @@ -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; + } +} diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index 1d180369765..daf071451bf 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -20,8 +20,19 @@ Date: April 2016 #include #include +#include + +// 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 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 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