From 8fa42b3279d1b09373e4aa9ebef9669babd6986b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 2 Jan 2018 11:10:45 +0000 Subject: [PATCH] Class hierarchy: add DOT output, unit tests This also adds a goto-instrument command to output the class hierarchy in text or DOT format. This is currently not usable with vanilla cbmc because none of its tools can produce GOTO binaries from Java class files, but out-of-tree tools can, and JBMC will surely gain support for GBF or its successors in the near future. --- .../goto-instrument/class-hierarchy/dot.desc | 6 ++ .../goto-instrument/class-hierarchy/main.c | 4 ++ .../class-hierarchy/plain.desc | 5 ++ .../goto_instrument_parse_options.cpp | 14 ++++ .../goto_instrument_parse_options.h | 1 + src/goto-programs/class_hierarchy.cpp | 20 ++++++ src/goto-programs/class_hierarchy.h | 1 + unit/Makefile | 1 + unit/goto-programs/HierarchyTest.class | Bin 0 -> 286 bytes unit/goto-programs/HierarchyTest.java | 12 ++++ unit/goto-programs/HierarchyTestChild1.class | Bin 0 -> 203 bytes unit/goto-programs/HierarchyTestChild2.class | Bin 0 -> 203 bytes .../HierarchyTestGrandchild.class | Bin 0 -> 275 bytes .../HierarchyTestInterface1.class | Bin 0 -> 127 bytes .../HierarchyTestInterface1.java | 1 + .../HierarchyTestInterface2.class | Bin 0 -> 127 bytes .../HierarchyTestInterface2.java | 1 + unit/goto-programs/class_hierarchy_output.cpp | 66 ++++++++++++++++++ 18 files changed, 132 insertions(+) create mode 100644 regression/goto-instrument/class-hierarchy/dot.desc create mode 100644 regression/goto-instrument/class-hierarchy/main.c create mode 100644 regression/goto-instrument/class-hierarchy/plain.desc create mode 100644 unit/goto-programs/HierarchyTest.class create mode 100644 unit/goto-programs/HierarchyTest.java create mode 100644 unit/goto-programs/HierarchyTestChild1.class create mode 100644 unit/goto-programs/HierarchyTestChild2.class create mode 100644 unit/goto-programs/HierarchyTestGrandchild.class create mode 100644 unit/goto-programs/HierarchyTestInterface1.class create mode 100644 unit/goto-programs/HierarchyTestInterface1.java create mode 100644 unit/goto-programs/HierarchyTestInterface2.class create mode 100644 unit/goto-programs/HierarchyTestInterface2.java create mode 100644 unit/goto-programs/class_hierarchy_output.cpp diff --git a/regression/goto-instrument/class-hierarchy/dot.desc b/regression/goto-instrument/class-hierarchy/dot.desc new file mode 100644 index 00000000000..77ea28c0e76 --- /dev/null +++ b/regression/goto-instrument/class-hierarchy/dot.desc @@ -0,0 +1,6 @@ +CORE +main.c +--class-hierarchy --dot +digraph class_hierarchy +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/class-hierarchy/main.c b/regression/goto-instrument/class-hierarchy/main.c new file mode 100644 index 00000000000..3999d746391 --- /dev/null +++ b/regression/goto-instrument/class-hierarchy/main.c @@ -0,0 +1,4 @@ + +void main() +{ +} diff --git a/regression/goto-instrument/class-hierarchy/plain.desc b/regression/goto-instrument/class-hierarchy/plain.desc new file mode 100644 index 00000000000..52367db0168 --- /dev/null +++ b/regression/goto-instrument/class-hierarchy/plain.desc @@ -0,0 +1,5 @@ +CORE +main.c +--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 fd53a05a765..931a5d9d2b2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -675,6 +676,18 @@ int goto_instrument_parse_optionst::doit() return 0; } + if(cmdline.isset("class-hierarchy")) + { + class_hierarchyt hierarchy; + hierarchy(goto_model.symbol_table); + if(cmdline.isset("dot")) + hierarchy.output_dot(std::cout); + else + hierarchy.output(std::cout); + + return 0; + } + if(cmdline.isset("dot")) { namespacet ns(goto_model.symbol_table); @@ -1474,6 +1487,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" "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5a89e2cf9df..5f17c96fca1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -44,6 +44,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)" \ "(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 8c8ea2091be..89916e317d3 100644 --- a/src/goto-programs/class_hierarchy.cpp +++ b/src/goto-programs/class_hierarchy.cpp @@ -99,3 +99,23 @@ void class_hierarchyt::output(std::ostream &out) const << ch << '\n'; } } + +/// Output class hierarchy in Graphviz DOT format +/// \param ostr: stream to write DOT to +void class_hierarchyt::output_dot(std::ostream &ostr) const +{ + ostr << "digraph class_hierarchy {\n" + << " rankdir=BT;\n" + << " node [fontsize=12 shape=box];\n"; + for(const auto &c : class_map) + { + for(const auto &ch : c.second.parents) + { + ostr << " \"" << c.first << "\" -> " + << "\"" << ch << "\" " + << " [arrowhead=\"vee\"];" + << "\n"; + } + } + ostr << "}\n"; +} diff --git a/src/goto-programs/class_hierarchy.h b/src/goto-programs/class_hierarchy.h index 5cd33b4d864..8c96798bade 100644 --- a/src/goto-programs/class_hierarchy.h +++ b/src/goto-programs/class_hierarchy.h @@ -52,6 +52,7 @@ class class_hierarchyt } void output(std::ostream &) const; + void output_dot(std::ostream &) const; protected: void get_children_trans_rec(const irep_idt &, idst &) const; diff --git a/unit/Makefile b/unit/Makefile index 043d8ef8d37..d31665a8505 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -17,6 +17,7 @@ SRC += unit_tests.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ goto-programs/goto_trace_output.cpp \ + goto-programs/class_hierarchy_output.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ diff --git a/unit/goto-programs/HierarchyTest.class b/unit/goto-programs/HierarchyTest.class new file mode 100644 index 0000000000000000000000000000000000000000..178576f3fe8ce9d61e9e31aa1f16eb9b9f9e643b GIT binary patch literal 286 zcmY+9JW#2mo|x>S0v$RUjk zAsti;7jSWR~I&;!Z#9drxhY>3hq&2f(* F{{fcBJtqJF literal 0 HcmV?d00001 diff --git a/unit/goto-programs/HierarchyTest.java b/unit/goto-programs/HierarchyTest.java new file mode 100644 index 00000000000..1011449de1b --- /dev/null +++ b/unit/goto-programs/HierarchyTest.java @@ -0,0 +1,12 @@ +public class HierarchyTest { + // These fields exist only so the classloader will load all test classes: + HierarchyTestGrandchild field1; + HierarchyTestChild2 field2; +} + +class HierarchyTestChild1 extends HierarchyTest {} + +class HierarchyTestChild2 extends HierarchyTest {} + +class HierarchyTestGrandchild extends HierarchyTestChild1 + implements HierarchyTestInterface1, HierarchyTestInterface2 {} diff --git a/unit/goto-programs/HierarchyTestChild1.class b/unit/goto-programs/HierarchyTestChild1.class new file mode 100644 index 0000000000000000000000000000000000000000..b0fab05a72e8e1a3b4343d34af719be191ab0c19 GIT binary patch literal 203 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj6ZvpuoTcbOH!40x?h@kY)q2WPvnDgjH)h1LH=pG&_)F0}HYPNe&>7 HiGdRU7`iA1 literal 0 HcmV?d00001 diff --git a/unit/goto-programs/HierarchyTestChild2.class b/unit/goto-programs/HierarchyTestChild2.class new file mode 100644 index 0000000000000000000000000000000000000000..22fbbc9739b64e49c4888f0f3db74ebce3363492 GIT binary patch literal 203 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj6ZvpuoTcbOH!40x?h@kY)q2WPvnDgjH)h1LH=pG&_)F0}FBjNe&>7 HiGdRU86qeN literal 0 HcmV?d00001 diff --git a/unit/goto-programs/HierarchyTestGrandchild.class b/unit/goto-programs/HierarchyTestGrandchild.class new file mode 100644 index 0000000000000000000000000000000000000000..17f3fa40a712391dddd9dd534567524c8dd7f6b1 GIT binary patch literal 275 zcmX^0Z`VEs1_l!bK`sVn1|D_>UUmjPb_RZS1_4F}Hk-`6%o00B24)S-Fh&Lz=lqmZ zMh1SL%)C^;(%hufqL9R-9H0nSaDHh~a;jS1R71V2#Ii(225}tHj0^%G1^PLOdFlH8Nm;4MC2R}~j0{Xbt3ZH}ff-0LF|Yst DdI}-6 literal 0 HcmV?d00001 diff --git a/unit/goto-programs/HierarchyTestInterface1.java b/unit/goto-programs/HierarchyTestInterface1.java new file mode 100644 index 00000000000..47d1a8ddd62 --- /dev/null +++ b/unit/goto-programs/HierarchyTestInterface1.java @@ -0,0 +1 @@ +interface HierarchyTestInterface1 {} diff --git a/unit/goto-programs/HierarchyTestInterface2.class b/unit/goto-programs/HierarchyTestInterface2.class new file mode 100644 index 0000000000000000000000000000000000000000..14eb47f76565dcad26c0d216c92618a21b2703e0 GIT binary patch literal 127 zcmX^0Z`VEs1_l!bc6J61R3p8t#Ii(225}tHj0^%G1^PLOdFlH8Nm;4MC2R}~j0{Xbt3ZH}ff-0LF|Yst DdVL|c literal 0 HcmV?d00001 diff --git a/unit/goto-programs/HierarchyTestInterface2.java b/unit/goto-programs/HierarchyTestInterface2.java new file mode 100644 index 00000000000..bee58260862 --- /dev/null +++ b/unit/goto-programs/HierarchyTestInterface2.java @@ -0,0 +1 @@ +interface HierarchyTestInterface2 {} diff --git a/unit/goto-programs/class_hierarchy_output.cpp b/unit/goto-programs/class_hierarchy_output.cpp new file mode 100644 index 00000000000..bdde2d2ab06 --- /dev/null +++ b/unit/goto-programs/class_hierarchy_output.cpp @@ -0,0 +1,66 @@ +/*******************************************************************\ + + Module: Unit tests for class_hierarchyt output functions + + Author: Diffblue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include + +#include + +#include +#include + +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; + + 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); +} + +SCENARIO( + "Output a simple class hierarchy" + "[core][goto-programs][class_hierarchy]") +{ + symbol_tablet symbol_table = + load_java_class("HierarchyTest", "goto-programs/"); + class_hierarchyt hierarchy; + + std::stringstream output_stream; + 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); + require_parent_child_relationship( + "HierarchyTest", "HierarchyTestChild2", output, output_dot); + require_parent_child_relationship( + "HierarchyTestChild1", "HierarchyTestGrandchild", output, output_dot); + require_parent_child_relationship( + "HierarchyTestInterface1", "HierarchyTestGrandchild", output, output_dot); + require_parent_child_relationship( + "HierarchyTestInterface2", "HierarchyTestGrandchild", output, output_dot); +}