Depth limited search #2381

polgreen · 2018-06-21T09:57:01Z

Implements a depth limited search on a grapht, and a call_grapht helper function that uses this on the directed graph from a a call graph to get functions reachable within N steps.

This is part of the re-doing of PR #1587

allredj

Passed Diffblue compatibility checks (cbmc commit: d6fa1d1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76929306

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 2cabda1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76933233
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 2e99c82).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76935453
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 394e71b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76955418
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.

Common spurious failures:

the cbmc commit has disappeared in the mean time (e.g. in a force-push)
the author is not in the list of contributors (e.g. first-time contributors).

polgreen · 2018-06-21T15:38:02Z

How do I fix the failure above? @peterschrammel, @thk123, or @allredj?

allredj · 2018-06-21T15:49:49Z

This only failed because the commit for which the build was triggered was squashed. The updated build should start soon (https://travis-ci.com/diffblue/test-gen/builds/76961329).

allredj

Passed Diffblue compatibility checks (cbmc commit: baf05f6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76961329

smowton · 2018-06-23T13:45:31Z

See comments on #2385

tautschnig

Just a few small issues, otherwise looks good.

tautschnig · 2018-06-23T20:00:56Z

src/util/graph.h

@@ -252,6 +252,16 @@ class grapht
  std::vector<node_indext>
  get_reachable(const std::vector<node_indext> &src, bool forwards) const;

+  std::vector<node_indext> depth_limited_search(


Nit pick, just placing it here for I can't comment on commit messages on GitHub: typo in the commit message (s/depht/depth/).

tautschnig · 2018-06-23T20:07:58Z

src/util/graph.h

@@ -252,6 +252,16 @@ class grapht
  std::vector<node_indext>
  get_reachable(const std::vector<node_indext> &src, bool forwards) const;

+  std::vector<node_indext> depth_limited_search(
+    const node_indext &src,
+    std::size_t &limit,


I believe @smowton has commented on this: not clear why this is passed by reference.

tautschnig · 2018-06-23T20:10:08Z

src/util/graph.h

+  std::vector<bool> visited(nodes.size(), false);
+
+  for(const auto &node : src)
+    visited[node] = true;


I'd suggest a PRECONDITON(node < nodes.size()); here.

tautschnig · 2018-06-23T20:11:53Z

src/util/graph.h

+  std::vector<bool> &visited,
+  bool forwards) const
+{
+  PRECONDITION(nodes.size() < std::numeric_limits<std::size_t>::max());


This is a surprising condition, effectively only ruling out the case nodes.size() == std::numeric_limits<std::size_t>::max(). Why is that useful?

Ah, it should be <=, and then it rules out any case where the number of nodes is bigger than std::numeric_limits<std::size_t>::max(), because if it is, this function won't work because i access the nodes by an index that is a std::size_t. But I guess if the graph needs more nodes than std::numeric_limits<std::size_t>::max() something will fail earlier than this? I couldn't find any explicit checks elsewhere in graph.h

The type of nodes.size() is (a typedef resolving to) std::size_t, and thus this will trivially be true. I think it's safe to drop this PRECONDITION.

tautschnig · 2018-06-23T20:12:30Z

src/util/graph.h

+
+  for(const auto &n : src)
+  {
+    result.push_back(n);


You might just construct result from src?

tautschnig · 2018-06-23T20:13:57Z

src/analyses/call_graph_helpers.cpp

+std::set<irep_idt> get_functions_reachable_within_n_steps(
+  const call_grapht::directed_grapht &graph,
+  const std::set<irep_idt> &start_functions,
+  std::size_t &n,


Why is this is a reference?

tautschnig · 2018-06-23T20:17:14Z

src/analyses/call_graph_helpers.cpp

+  bool forwards)
+{
+  std::set<irep_idt> start_functions;
+  start_functions.insert(start_function);


You can do std::set<irep_idt> start_functions({ start_function }); (and I think you could even just pass {start function} directly to get_functions_reachable_within_n_steps.

tautschnig · 2018-06-23T20:17:38Z

src/analyses/call_graph_helpers.h

+/// \param graph: call graph
+/// \param start_functions: set of start functions
+/// \param n: number of steps to consider
+/// \param forwards: if true, get callees; otherwise get callers


Please document the return value as well.

polgreen · 2018-06-25T08:45:57Z

changes made, plus changes requested by @smowton on #2385

smowton

Thanks for doing the extra work on this!

smowton · 2018-06-25T09:26:06Z

src/util/graph.h

+  const node_indext from, size_t depth) const
+{
+  std::set<node_indext> result;
+    depth_limited_search(from, depth, result);


tautschnig

Comments on the Doxygen CI failures

tautschnig · 2018-06-25T09:35:08Z

src/analyses/call_graph_helpers.h

+/// \param graph: call graph
+/// \param start_function: single start function
+/// \param n: number of steps to consider
+/// \param forwards: if true, get callees; otherwise get callers


No such parameter.

tautschnig · 2018-06-25T09:38:48Z

src/util/graph.h

+/// excluding the start node unless a self loop exists.
+/// \param from : vector of node indices to start from
+/// \param depth : depth limit
+/// \return set of node indices of reachable nodes


I have no idea why Doxygen can't cope with this one, or at least I can't see anything wrong with it. You might try moving the documentation to the declarations above to see whether that makes Doxygen happier.

Would you mind trying to move the documentation to the declaration? It seems Doxygen is still refusing to play along.

that's weird, because get_reachable is documented in the same way and in the same place. The only difference is get_reachable doesn't document the return

polgreen · 2018-06-26T08:46:32Z

I've fixed the clang format and the doxygen error with parameter naming, but I really don't know what I can do about this one:

/home/travis/build/diffblue/cbmc/src/util/graph.h:632: warning: no matching class member found for 
  template < N >
  std::set< typename N::node_indext > grapht< N >::depth_limited_search(nodet::node_indext from, size_t depth) const
Possible candidates:

smowton · 2018-06-26T09:17:09Z

@polgreen I think the cause is that both grapht and graph_nodet define a type called node_indext. The inline prototype uses node_indext which is implicitly grapht<N>::node_indext, but the out-of-line definitions use typename N::node_indext, where N is derived from graph_nodet. The types happen to be the same, but Doxygen is unhappy that you're getting them from different places.

Suggested solution: change the out-of-line definition to use typename grapht<N>::node_indext

There's also a genuine Travis failure to look at.

polgreen · 2018-06-26T09:32:14Z

It's currently completely consistent with the way get_reachable does it though?!

The appveyor failure seems to be completely unrelated to any code I've changed? I haven't touched type2name.cpp or convert_integer_literal.cpp. I can't tell what the travis failure is, possible the same?

smowton · 2018-06-26T09:53:27Z

I guess the difference is get_reachable is documented on the definition, and depth_limited_search is documented on the declaration / prototype -- I guess Doxygen wants the doc commands to hand when parsing the method definition, which in once case means trying to pair it up with the class member, but in the other case the docs are right there so there's no need to try to find a correspondence?

FWIW I think get_reachable is also being a bit dodgy using different typedefs of the same type in its declaration and definition.

Speaking of which, for consistency the docs should probably move to the implementation, since that's what every other documented grapht method does at the moment.

smowton · 2018-06-26T09:54:47Z

AppVeyor's complaint:

..\util/graph.h(319) : error C2143: syntax error : missing ';' before '<'
689        ..\util/graph.h(313) : see reference to class template instantiation 'grapht<N>::tarjant' being compiled
690        ..\util/graph.h(343) : see reference to class template instantiation 'grapht<N>' being compiled
691..\util/graph.h(319) : error C4430: missing type specifier - int assumed. Note: C++ does not support default-int
692..\util/graph.h(319) : error C2238: unexpected token(s) preceding ';'

smowton · 2018-06-26T09:56:37Z

Travis:

../util/graph.h:319:10: error: ‘stack’ in namespace ‘std’ does not name a template type
     std::stack<node_indext> scc_stack;
          ^
In file included from graphml.h:19:0,
                 from graphml.cpp:12:
../util/graph.h: In member function ‘std::__debug::vector<typename N::node_indext> grapht<N>::get_reachable(const std::__debug::vector<typename N::node_indext>&, bool) const’:
../util/graph.h:595:3: error: ‘stack’ is not a member of ‘std’
   std::stack<node_indext, std::vector<node_indext>> s(src);
   ^
../util/graph.h:595:25: error: expected primary-expression before ‘,’ token
   std::stack<node_indext, std::vector<node_indext>> s(src);
                         ^
../util/graph.h:595:50: error: expected primary-expression before ‘>’ token
   std::stack<node_indext, std::vector<node_indext>> s(src);
                                                  ^
../util/graph.h:597:10: error: ‘s’ was not declared in this scope
   while(!s.empty())
          ^
../util/graph.h: In member function ‘std::size_t grapht<N>::connected_subgraphs(std::__debug::vector<typename N::node_indext>&)’:
../util/graph.h:670:5: error: ‘stack’ is not a member of ‘std’
     std::stack<node_indext> s;
     ^
../util/graph.h:670:27: error: expected primary-expression before ‘>’ token
     std::stack<node_indext> s;
                           ^
../util/graph.h:670:29: error: ‘s’ was not declared in this scope
     std::stack<node_indext> s;

polgreen · 2018-06-26T12:39:03Z

I've added some debug code because I've no idea why the appveyor unit test isn't working, and I can't recreate it anywhere else.

The doxygen failure over the grapht issue is still there. Both tautschn and smowton's suggested changes haven't made it go away. Can we write this one off as being a case where doxygen can't cope with c++ templates?

/home/travis/build/diffblue/cbmc/src/util/graph.h:632: warning: no matching class member found for 
  template < N >
  std::set< typename grapht< N >::node_indext > grapht< N >::depth_limited_search(nodet::node_indext from, size_t depth) const
Possible candidates:
  std::set< node_indext > grapht< N >::depth_limited_search(const std::vector< node_indext > &from, std::size_t depth) const
  std::set< node_indext > grapht< N >::depth_limited_search(node_indext from, std::size_t depth) const
  void grapht< N >::depth_limited_search(node_indext from, std::size_t depth, std::set< node_indext > &result) const

polgreen · 2018-06-26T12:59:44Z

@smowton, the documentation for the function is in the declaration and not the implementation because @tautschnig asked me to move it. It was originally by the implementation. Can you please agree on what you would like it to be and where you would like it to be?

polgreen · 2018-06-26T13:25:26Z

After a discussion with Michael, I am undoing the changes that were proposed in this comment:
#2385 (comment)

Whilst it might make the algorithm look more complicated, it is necessary to have the depth limited search algorithm work for a vector of nodes, and not from a single source node, because we need to be able to consider the full frontier of nodes at once.

Note that the change resulting from this comment will need to be reverted for the same reason:
#2385 (comment)

Example from Michael:
Consider graph with nodes a, b, c, d and edges a -> b -> c and a -> c -> d
Because you'd put c into the result set coming from a, b you'd never explore the edge c -> d

smowton · 2018-06-26T14:03:27Z

@tautschnig re: where the docs should be, I don't mind except it should be consistent within the file -- at the moment some functions have it on the decl and some on the defn. I only noticed since it might shut Doxygen up.

polgreen · 2018-06-26T14:21:03Z

RE: where the docs go: the reason Michael asked me to move it in the first place was because it might shut doxygen up. It won't...

This performs a depth limited depth-first search on a grapht

Gets all functions reachable within n steps, by calling depth limited search

allredj

Passed Diffblue compatibility checks (cbmc commit: 904132d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77361603

6fd77f4 Merge pull request diffblue#2472 from smowton/smowton/fix/nondet-stringbuilders 5423ea4 Merge pull request diffblue#2488 from polgreen/common_call_graph_funcs a2a5662 Merge pull request diffblue#2263 from JohnDumbell/bugfix/nondet_direct_return bbf0d02 Merge pull request diffblue#2482 from antlechner/antonia/direct-children-of-class c982c21 Merge pull request diffblue#2486 from Degiorgio/jbmc-synchronoization-asymmetry-fix 8e7b6e7 Java object factory: initialize AbstractStringBuilder-derived types correctly 9af7ef1 Add tests for new class_hierarchy_grapht functions 79cad15 Fix existing class hierarchy test syntax dbac316 Add documentation to class_hierarchyt 3ecac30 Move non-graph function below graph functions 4badd8f Add useful functions to class_hierarchy_grapht 610467e Merge pull request diffblue#2480 from smowton/smowton/admin/graph-unit-tests 2431ac0 Doxygen formatting for dependence_graph test includes 19a1ceb factor out common call graph unit test functions into header deff59d Add tests for grapht::make_chordal and grapht::connected_subgraphs e94208f Merge pull request diffblue#2428 from tautschnig/vs-ref d00d833 Fix: several grapht functions were uncompilable if ever called b9014de Merge pull request diffblue#2381 from polgreen/depth_limited_search 7c767ab Merge pull request diffblue#2485 from tautschnig/vs-unreachable da76500 JBMC: Fixed asymmetry between synchronized blocks and methods. 5918640 Merge pull request diffblue#2487 from JohnDumbell/bugfix/add_java_load_class d65c655 Merge pull request diffblue#2484 from tautschnig/vs-printf 91e8b89 Fix for nondet replacement on a direct return (pre-remove returns) 904132d unit tests for depth limited search on call graph 2c76d0d call graph helper interface to depth limited search 64fdb9b depht limited search for grapht e708bfb Adds --java-load-class to tests that require it 6665c69 Remove unreachable instructions 6e4d5a7 printf does not and should not have a left-hand side 2111f7c Merge pull request diffblue#2475 from tautschnig/vs-wmm 6566d10 Merge pull request diffblue#2469 from tautschnig/vs-string2 3703974 Merge pull request diffblue#2477 from tautschnig/vs-string-abstraction cf797da Merge pull request diffblue#2473 from tautschnig/vs-update c07a09b Merge pull request diffblue#2476 from tautschnig/vs-cex e504e80 Remove unused parameter in string abstraction 4d88b98 Remove unused parameter in counterexample beautification 888f168 Remove unused parameter from update_scores 461754d Remove unused parameters in goto-instrument/wmm 93300aa Use string2unsigned when reading/expecting an unsigned 1a7033a String refinement: Take a reference to avoid copy git-subtree-dir: cbmc git-subtree-split: 6fd77f4

polgreen requested review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton, tautschnig and thk123 as code owners June 21, 2018 09:57

polgreen force-pushed the depth_limited_search branch from ebe000a to d6fa1d1 Compare June 21, 2018 10:57

allredj reviewed Jun 21, 2018

View reviewed changes

polgreen force-pushed the depth_limited_search branch 2 times, most recently from 2cabda1 to 2e99c82 Compare June 21, 2018 11:47

allredj reviewed Jun 21, 2018

View reviewed changes

polgreen mentioned this pull request Jun 21, 2018

Aggressive slicer v2 #2385

Merged

polgreen force-pushed the depth_limited_search branch from 2e99c82 to 394e71b Compare June 21, 2018 12:18

allredj reviewed Jun 21, 2018

View reviewed changes

polgreen force-pushed the depth_limited_search branch from 394e71b to baf05f6 Compare June 21, 2018 12:43

allredj reviewed Jun 21, 2018

View reviewed changes

tautschnig approved these changes Jun 23, 2018

View reviewed changes

tautschnig assigned kroening, peterschrammel and polgreen Jun 23, 2018

polgreen force-pushed the depth_limited_search branch from baf05f6 to d836478 Compare June 25, 2018 08:48

smowton approved these changes Jun 25, 2018

View reviewed changes

tautschnig unassigned kroening and peterschrammel Jun 25, 2018

tautschnig reviewed Jun 25, 2018

View reviewed changes

polgreen force-pushed the depth_limited_search branch 3 times, most recently from 2d1bf04 to b16b6a2 Compare June 26, 2018 08:45

polgreen force-pushed the depth_limited_search branch 2 times, most recently from 2c68bde to d4ee0e5 Compare June 26, 2018 09:34

polgreen force-pushed the depth_limited_search branch from d4ee0e5 to 4411f63 Compare June 26, 2018 11:29

polgreen added 3 commits June 26, 2018 17:10

depht limited search for grapht

64fdb9b

This performs a depth limited depth-first search on a grapht

call graph helper interface to depth limited search

2c76d0d

Gets all functions reachable within n steps, by calling depth limited search

unit tests for depth limited search on call graph

904132d

polgreen force-pushed the depth_limited_search branch from 19fc2a0 to 904132d Compare June 26, 2018 15:12

allredj reviewed Jun 26, 2018

View reviewed changes

tautschnig merged commit b9014de into diffblue:develop Jun 27, 2018

Depth limited search #2381

Depth limited search #2381

Conversation

polgreen commented Jun 21, 2018

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

polgreen commented Jun 21, 2018

allredj commented Jun 21, 2018

allredj left a comment

Choose a reason for hiding this comment

smowton commented Jun 23, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

polgreen commented Jun 25, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

polgreen commented Jun 26, 2018

smowton commented Jun 26, 2018

polgreen commented Jun 26, 2018

smowton commented Jun 26, 2018

smowton commented Jun 26, 2018

smowton commented Jun 26, 2018

polgreen commented Jun 26, 2018

polgreen commented Jun 26, 2018

polgreen commented Jun 26, 2018 • edited Loading

smowton commented Jun 26, 2018

polgreen commented Jun 26, 2018

allredj left a comment

Choose a reason for hiding this comment

polgreen commented Jun 26, 2018 •

edited

Loading