Make directed callgraph include nodes with no edges #2053

owen-mc-diffblue · 2018-04-13T09:01:19Z

No description provided.

tautschnig · 2018-04-13T10:37:58Z

Would you mind explaining (in the commit message) why this is a desirable feature?

tautschnig · 2018-04-13T10:41:19Z

src/analyses/call_graph.cpp

+  // To make sure we include unreachable functions we first create indices
+  // for all functions in the function map
+  for(const auto &f : goto_model.goto_functions.function_map)
+    function_indices[f.first];


This function is only computing a different representation of the same underlying graph. Do your changes just fix up a bit of information that is present in the original call graph, or will it actually yield a different graph?

owen-mc-diffblue · 2018-04-13T12:57:48Z

@tautschnig Thanks for your review. Thinking about it further I realise this is the wrong fix, because it assumes the callgraph has been created for all goto functions.

I still think there might be an underlying problem: callgrapht only stores edges, so it has no way of storing a node without any edges. So if you create the callgraph of all functions and then get the directed graph from it then it will be missing nodes that you would expect to be there. Perhaps this is the intended behaviour of callgrapht, and the error is in my assumption that getting a directed graph from it would give me a graph with nodes corresponding to the functions that were passed to the constructor of the callgraph. I would value your opinion on this. If I am correct then the fix would be to keep a list of nodes when callgraph is created and use that in get_directed_graph().

tautschnig · 2018-04-13T14:59:58Z

I'd say that it's a call graph, hence nodes without edges don't seem to fit the bill as there's no call to be found. But then you expected to find those here, so you will have different requirements. If you can share your requirements, maybe that helps to come up with an answer? From what I've seen so far I'd say you need both the call graph and the list of functions (which can independently be obtained).

smowton · 2018-04-16T12:32:20Z

Personally I'd expect "the call graph of {f, g, h}" to yield a graph containing exactly three nodes, and edges representing calls, not for functions to disappear entirely if they don't have callers or callees.

One reason for this: it is expected that a call graph would not always be totally connected, but for us to retain both independent subgraphs in that case. In the particular case where one of the components was of size 1 (i.e. a single node with no associated edges), I don't think that special case should be treated differently.

(Example: if there are edges a -> b and c -> d, we would retain all 4 nodes, but graphs {a, b} and {c, d} are unconnected. It's surprising to me if in the case a -> b, a -> c we don't create graphs {a, b, c} and {d}, but rather throw the 'd' graph away entirely)

Long story short I suggest @owen-jones-diffblue should make the original call_grapht retain a vector of functions it was originally constructed upon, to be used if/when get_directed_graph is called.

owen-mc-diffblue · 2018-04-17T04:54:07Z

I agree with @smowton, and I have implemented his suggestion.

tautschnig · 2018-04-17T05:54:01Z

Can you please confirm that goto-instrument --reachable-call-graph and goto-instrument --slice-global-inits are not adversely affected by this change?

NathanJPhillips · 2018-04-17T09:40:25Z

src/analyses/call_graph.cpp

@@ -129,7 +133,9 @@ void call_grapht::add(
  const irep_idt &caller,
  const irep_idt &callee)
 {
-  graph.insert(std::pair<irep_idt, irep_idt>(caller, callee));
+  edges.insert(std::pair<irep_idt, irep_idt>(caller, callee));


std::make_pair or even just brace initialise?

owen-mc-diffblue · 2018-04-17T10:06:19Z

@tautschnig They shouldn't be affected because they both use call_grapht::create_from_root_function(), so the graph is connected. Also, the graph has at least two nodes because it has __CPROVER__start and the user-supplied entry function, so all edges will have an edge going into or out of them. I don't know how to run them but their tests were failing before and are now passing.

tautschnig · 2018-04-17T10:13:36Z

Would you mind doing the extra exercise of adding a regression test for --reachable-call-graph (and possibly also --call-graph, which now should definitively provide distinct output) in regression/goto-instrument/? All it would take is a small C program that has a few functions where not all of them are called from main.

owen-mc-diffblue · 2018-04-17T13:14:32Z

@tautschnig I have added those tests. I put them in a commit before the main changes, to signify that they pass before and after the changes.

As you seem to have already noticed, slice-global-inits-1 already tests that an unreachable function (func1) is dealt with appropriately in goto-instrument --slice-global-inits.

owen-mc-diffblue · 2018-04-17T13:16:28Z

By the way, this PR should not be merged yet as I have to fix problems caused in a repository which relies on cbmc first.

Make sure that changes to call_grapht do not alter these two options to goto-instrument

smowton

Looks great, tiny nitpick

smowton · 2018-04-19T13:30:48Z

src/analyses/call_graph.h

  typedef std::pair<irep_idt, irep_idt> edget;

+


don't add blank line

Note, if the callgraph was created from a particular entry point then this will not change the output. It is only when the callgraph is created for a goto_functionst that the output will change - it will now include functions that have no edges, i.e. that are not called by any other functions and which don't call any other functions.

owen-mc-diffblue · 2018-04-19T13:41:15Z

https://github.com/diffblue/test-gen/pull/1717

31c47c2 Merge pull request diffblue#2113 from diffblue/java_new_array_data fb3025d Merge pull request diffblue#2107 from thk123/feature/TG-3271/interpreter-tracking-mock-exceptions 32bf48e Merge pull request diffblue#2105 from tautschnig/determinise-test 7254a2a show java_new_array_data side effects 0f1482c Merge pull request diffblue#2094 from smowton/smowton/fix/tmp-object-factory-prefix 3cfec66 Merge pull request diffblue#2106 from diffblue/ptrmember_on_array bf4c39c Merge pull request diffblue#1966 from JohnDumbell/JohnDumbell/Update-Assertion-Validation 74a37c6 Merge pull request diffblue#1988 from tautschnig/cadical 74dc576 Merge pull request diffblue#2003 from tautschnig/bitfield-offset 8916906 Merge pull request diffblue#2008 from tautschnig/section-bug 0bd83ab Extension to interpreter class a0ca0ba fix array->f typechecking e1f4120 Make virtual function resolution independent of string table entry ordering 714ccff Merge pull request diffblue#2072 from danpoe/feature/small-shared-two-way-ptr 16b6c20 Merge pull request diffblue#2046 from thk123/gs_tg2922 04cb909 Merge pull request diffblue#2102 from thk123/formatting/sort-includes-clang-format 7070ba1 Sort includes using clang-format 9874a6b Reformatting touched output function f2a4054 Remove redundant default constructor 54fb9ab Use format rather than from_expr for output 781bf7c Introduce exceptions for all conversion steps. 21997b2 Add documentation to convert_bitvector 015b284 Test demonstrating logging with clause for dealing with Windows 9d41b0c Disable nested exception printing for Windows b866015 Provide the original goto statement in the error a97bc28 Introduce throwing a guard conversion exception 12f25c2 Introduce throwing bv_conversion expection 9bd5222 Convert flatten_byte_extract to use structured exceptions 3207291 Introduce nested exception printing 35c4be7 Small shared two way pointer 7d247da Merge pull request diffblue#2099 from mgudemann/bugfix/build/glucose_syrup 1776a9e Merge pull request diffblue#1950 from romainbrenguier/refactor/prop_conv_straightforward 4147243 Change set_variable_name API to consume irep_idt 2d8be06 Rename `it` to pair in boolbvt::print_assignment 4365c28 Simplify boolbvt::set_to b18109f Make make_(free_)bv_expr return exprt 5724a35 Simplify loop in prop_conv::get 4987f3a Remove useless comments 13e87a9 Simplify dec_solve a0500f6 Use standard algorithm for finding an element ba13c94 Use auto for iterator types 9179571 Remove useless includes a905a07 Replace throws by invariant or preconditions 7db44fc Remove virtual keyword where not needed 990f33e Initialize at declaration instead of construction c1a93b3 Renaming `it` to symbol 8eb20f6 Use ranged for dc799e0 Assert replaced by unreachable c34e073 Add support for CaDiCaL 1bd9efd Merge pull request diffblue#2097 from peterschrammel/java-cleanup-replace a079f46 Clang-format moved file 2eb3714 Move replace_java_nondet to java_bytecode 9a8c292 Remove unnecessary include c8cf100 Remove Java refs from ANSI-C docs 0090952 Merge pull request diffblue#2096 from diffblue/cleanout-java aa3caa3 Fix CMake build for Glucose Syrup 1156930 Merge pull request diffblue#1244 from tautschnig/goto-gcc-at-fix 706e391 Merge pull request diffblue#2093 from owen-jones-diffblue/owen-jones-diffblue/remove_unnecessary_irep_id_hash 290feb4 Merge pull request diffblue#2095 from diffblue/get_json_stream_precondition ac2df21 Merge pull request diffblue#2027 from tautschnig/linking-multiple-conflicts dd0d602 Merge pull request diffblue#2030 from tautschnig/goto-cc-linux-kernel 42e58d4 Merge pull request diffblue#2085 from tautschnig/from_expr-cleanup 692f92d remove dependency on java_bytecode 8c6165d precondition for get_json_stream() e28a662 Remove unused typedef 5626fb7 Merge pull request diffblue#2092 from smowton/smowton/cleanup/diffblue-spelling 4840154 Replace stack by deque and use range-based for loop 987edbe Use range-based for loops 92ac82c Remove redundant irep_id_hash for unordered maps dc2b436 Remove redundant irep_id_hash for sets 5aa2c2d Attribute main function arguments to __CPROVER_start b7ef5af Merge pull request diffblue#2053 from owen-jones-diffblue/owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions 252474f String tests: DiffBlue -> Diffblue de1915a Merge pull request diffblue#2074 from owen-jones-diffblue/owen-jones-diffblue/lazy-methods-no-candidate-callees d73f6bc Make directed callgraph include nodes with no edges 2a45e61 Only the top-level section should be considered for renaming 9c66a66 fixup! Support __attribute__((section("x")) e133964 C front-end: Section/ASM renaming also needs to be applied to aliases 0cfc72f Test --call-graph and --reachable-call-graph 1c34d22 Test lazy-loading when there are no candidates 289a439 Deal with virtual function calls with no candidate targets 9347615 Remove incorrect comment 18b1962 Fix order of parameters in function header 82058da Store virtual function calls instead of virtual call-sites 3653550 Use unordered set of irep_ids in ci_lazy_methods c31d43f Remove code duplication 945f885 Rename two variables and make one more local b7d70e7 Replace do-while loop with equally valid while loop 58b990d Use from_{expr,type} matching the language of the expression/type 177c8c1 goto-cc: support thin ar archives, refactoring e80008e goto-cc: support GCC's print-sysroot* options 38e6fa5 Accept the --build-id option in goto-ld f3bbb12 Linking: report multiple conflicts 495f109 Fixing member offset computation in presence of bitfields 5109eab Add @<file> arguments to the original command line 97d556e Update desc file to add pass variables. eea76ec Add a regression test. c14e907 Increase AssertionError arguments allowed from 2 to 3 git-subtree-dir: cbmc git-subtree-split: 31c47c2

owen-mc-diffblue requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton, tautschnig and thk123 as code owners April 13, 2018 09:01

owen-mc-diffblue changed the title ~~Make directed callgraph include uncalled functions~~ Make directed callgraph include nodes with no edges Apr 13, 2018

tautschnig reviewed Apr 13, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch from 66d0f52 to 2bdb24d Compare April 16, 2018 16:52

owen-mc-diffblue force-pushed the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch from 2bdb24d to 7750ec7 Compare April 17, 2018 08:23

NathanJPhillips approved these changes Apr 17, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch from 7750ec7 to fec5e78 Compare April 17, 2018 09:58

owen-mc-diffblue force-pushed the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch from fec5e78 to 7cc2257 Compare April 17, 2018 13:13

tautschnig approved these changes Apr 17, 2018

View reviewed changes

owen-mc-diffblue force-pushed the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch 3 times, most recently from 7e10e68 to 1444044 Compare April 18, 2018 12:50

Test --call-graph and --reachable-call-graph

0cfc72f

Make sure that changes to call_grapht do not alter these two options to goto-instrument

owen-mc-diffblue force-pushed the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch from 1444044 to a8ae0cd Compare April 19, 2018 08:46

smowton approved these changes Apr 19, 2018

View reviewed changes

src/analyses/call_graph.h Outdated

typedef std::pair<irep_idt, irep_idt> edget;

Copy link

Contributor

smowton Apr 19, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

don't add blank line

owen-mc-diffblue force-pushed the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch from a8ae0cd to d73f6bc Compare April 19, 2018 13:35

smowton merged commit b7ef5af into diffblue:develop Apr 19, 2018

owen-mc-diffblue deleted the owen-jones-diffblue/bugfix/make-callgraph-include-uncalled-functions branch April 19, 2018 14:35

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make directed callgraph include nodes with no edges #2053

Make directed callgraph include nodes with no edges #2053

owen-mc-diffblue commented Apr 13, 2018 •

edited

Loading

tautschnig commented Apr 13, 2018

tautschnig Apr 13, 2018

owen-mc-diffblue commented Apr 13, 2018

tautschnig commented Apr 13, 2018

smowton commented Apr 16, 2018

owen-mc-diffblue commented Apr 17, 2018

tautschnig commented Apr 17, 2018

NathanJPhillips Apr 17, 2018

owen-mc-diffblue commented Apr 17, 2018

tautschnig commented Apr 17, 2018

owen-mc-diffblue commented Apr 17, 2018

owen-mc-diffblue commented Apr 17, 2018

smowton left a comment

smowton Apr 19, 2018

owen-mc-diffblue commented Apr 19, 2018

Make directed callgraph include nodes with no edges #2053

Make directed callgraph include nodes with no edges #2053

Conversation

owen-mc-diffblue commented Apr 13, 2018 • edited Loading

tautschnig commented Apr 13, 2018

tautschnig Apr 13, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 13, 2018

tautschnig commented Apr 13, 2018

smowton commented Apr 16, 2018

owen-mc-diffblue commented Apr 17, 2018

tautschnig commented Apr 17, 2018

NathanJPhillips Apr 17, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 17, 2018

tautschnig commented Apr 17, 2018

owen-mc-diffblue commented Apr 17, 2018

owen-mc-diffblue commented Apr 17, 2018

smowton left a comment

Choose a reason for hiding this comment

smowton Apr 19, 2018

Choose a reason for hiding this comment

owen-mc-diffblue commented Apr 19, 2018

owen-mc-diffblue commented Apr 13, 2018 •

edited

Loading