Make direct children of a class publicly available #2482

antlechner · 2018-06-26T13:41:47Z

Previously it was only possible to retrieve all children of a class (i.e. those that inherit directly and those that inherit by transitivity) given its ID. The new function retrieves only those children that inherit directly from the given class.

This new function is not used anywhere in CBMC but will be useful for Diffblue code.

I'm not sure how I would write a unit test for this, so if you think a test is necessary, some advice on that would be appreciated. It looks like there are no tests for anything in class_hierarchy.h in cbmc/unit, but there are some tests related to this file in jbmc/unit/java_bytecode/goto-programs. I'm not sure if those tests are supposed to be in the jbmc folder as the code in goto-programs is not Java-specific? In any case, the change in this PR is quite small so maybe a test is not necessary. Let me know what you think.

antlechner · 2018-06-26T13:42:45Z

@peterschrammel @mgudemann @romainbrenguier Could you have a look at this please?

tautschnig · 2018-06-26T13:47:55Z

Could unit tests please be added (there are some for this code in jbmc/unit/java_bytecode/goto-programs/class_hierarchy_output.cpp already)?

antlechner · 2018-06-26T13:49:44Z

@tautschnig I asked about that in the PR description. :) So you think it's fine to add unit tests for cbmc code in the jbmc unit folder (and the already existing tests are in the right place)?

tautschnig

Wouldn't this be rather trivial if using class_hierarchy_grapht instead? Then it's just node.out ?!

tautschnig · 2018-06-26T13:54:57Z

So you think it's fine to add unit tests for cbmc code in the jbmc unit folder (and the already existing tests are in the right place)?

Then at least it's tested somewhere :-) Yes, I think that would be a perfectly ok place.

allredj

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

antlechner · 2018-06-26T15:45:08Z

@tautschnig I didn't know much about the difference between class_hierarchyt and class_hierarchy_grapht and why we have both, so I asked @smowton about this in person. If I understand correctly, class_hierarchyt is old code and is still used in various places but class_hierarchy_grapht is a better representation (as it's graph-based) of the same thing that is generally preferred now.
If that's correct, I could do the following:

create helper functions with the same functionality as class_hierarchyt::get_direct_children and class_hierarchyt::get_children_trans in class_hierarchy_grapht (using node.out and some conversions between irep_idt and node_indext)
add unit tests for the new functions in ..._grapht
revert the original commit of this PR
add documentation to class_hierarchyt explaining that it is deprecated and class_hierarchy_grapht should be used instead whenever possible, to make sure others like me won't get confused about this in the future.
Does this sound like what you had in mind?

tautschnig · 2018-06-26T16:02:40Z

Does this sound like what you had in mind?

You seem to be going for a grand plan :-) - I'd be totally fine with you using class_hierarchy_grapht as-is. My slight pushback on your initial proposal is all based on not growing the code base when (seemingly) not necessary. If, however, you can afford the extra time then surely what you are suggesting is great.

antlechner · 2018-06-26T18:20:54Z

@tautschnig That makes sense. From my point of view, of course it's much nicer to have a clean interface of CBMC structures that we can use directly in Diffblue code without having to understand the implementation details of those structures and use five lines of set-up code every time we use them. So I hope my new approach is a good compromise. Of course it adds even more to the code base than my previous approach... But the idea is that it should be a step on the way to move everything in class_hierarchyt to class_hierarchy_grapht, and once that is all done and the old class_hierarchyt is removed, everything should be in a tidier state than before. So hopefully this change will be useful for everyone in the long run. :)
I've done steps 1, 3 and 4 from my plan above. I'll add unit tests for the new functions tomorrow.

allredj

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

allredj

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

allredj

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

antlechner · 2018-06-27T14:39:50Z

src/goto-programs/class_hierarchy.cpp

@@ -13,6 +13,7 @@ Date: April 2016

 #include "class_hierarchy.h"

+#include <iterator>


This line was only needed to make the "AWS cbmc-windows" build happy, which would otherwise complain about back_inserter in ids_from_indices.

class_hierarchy_grapht is a more advanced representation of the class hierarchy than class_hierarchyt. So ideally we want to migrate all functions from the old version to the graph-based representation. This commit does this for the functions get_parents_trans, get_children_trans, and introduces a new function get_direct_children.

This way everything related to class_hierarchy_grapht appears first in the file, followed by everything related to class_hierarchyt. Ideally these parts should be split into different files in the future.

These two tests were previously never run because of a missing comma in the SCENARIO line. The two scenarios also need to have different names.

antlechner · 2018-06-27T14:56:58Z

@tautschnig Step 2 is done - I added unit tests for all the new functions (except helper functions). I also noticed that the previously existing tests for class hierarchies were never actually run so I fixed that. Could you please re-review?

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 6f861fc).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77479794
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: ff7b37c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77480971
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

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

tautschnig · 2018-06-27T15:40:13Z

@antlechner Thanks a lot for all the work, this looks all very good to me. Just one bit:

[...] I also noticed that the previously existing tests for class hierarchies were never actually run so I fixed that.

How come these were not being run and 2) which change is it that now makes them run?

tautschnig

Looks good to me as said, just that question (#2482 (comment)) about unit tests remains open.

antlechner · 2018-06-27T15:49:54Z

@tautschnig Glad I found a way to make this change that works for everyone!

which change is it that now makes them run?

The change is in its own commit: 79cad15
(Or in case that should disappear after a force-push, it's the one called "Fix existing class hierarchy test syntax".)

How come these were not being run

They used the wrong syntax in the SCENARIO line: a comma was missing so the tags weren't applied properly. It's also apparently not ok for two scenarios to have the same name (I tried just adding the commas first and got errors about the names being identical when trying to run the tests).

tautschnig · 2018-06-27T15:54:39Z

The change is in its own commit: 79cad15

Oh, wow, slightly scary that syntax errors lead to silently ignored unit tests.

antlechner · 2018-06-27T16:04:02Z

Agreed! I greped for that particular mistake in both unit and jbmc/unit and luckily couldn't find any other occurrences of it.

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

antlechner requested review from kroening, peterschrammel, smowton and tautschnig as code owners June 26, 2018 13:41

tautschnig reviewed Jun 26, 2018

View reviewed changes

allredj reviewed Jun 26, 2018

View reviewed changes

antlechner force-pushed the antonia/direct-children-of-class branch 2 times, most recently from 9a63fba to 9359747 Compare June 26, 2018 18:16

antlechner force-pushed the antonia/direct-children-of-class branch from 9359747 to 4c650a2 Compare June 26, 2018 18:39

allredj reviewed Jun 26, 2018

View reviewed changes

antlechner force-pushed the antonia/direct-children-of-class branch 2 times, most recently from 3cd0c3c to 11b8026 Compare June 27, 2018 11:18

allredj reviewed Jun 27, 2018

View reviewed changes

antlechner force-pushed the antonia/direct-children-of-class branch from 11b8026 to 6f861fc Compare June 27, 2018 14:37

antlechner commented Jun 27, 2018

View reviewed changes

antlechner force-pushed the antonia/direct-children-of-class branch from 6f861fc to ff7b37c Compare June 27, 2018 14:40

antlechner added 5 commits June 27, 2018 15:53

Move non-graph function below graph functions

3ecac30

This way everything related to class_hierarchy_grapht appears first in the file, followed by everything related to class_hierarchyt. Ideally these parts should be split into different files in the future.

Add documentation to class_hierarchyt

dbac316

Fix existing class hierarchy test syntax

79cad15

These two tests were previously never run because of a missing comma in the SCENARIO line. The two scenarios also need to have different names.

Add tests for new class_hierarchy_grapht functions

9af7ef1

antlechner force-pushed the antonia/direct-children-of-class branch from ff7b37c to 9af7ef1 Compare June 27, 2018 14:53

allredj reviewed Jun 27, 2018

View reviewed changes

tautschnig approved these changes Jun 27, 2018

View reviewed changes

peterschrammel approved these changes Jun 27, 2018

View reviewed changes

peterschrammel merged commit bbf0d02 into diffblue:develop Jun 27, 2018

antlechner deleted the antonia/direct-children-of-class branch June 28, 2018 08:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Make direct children of a class publicly available #2482

Make direct children of a class publicly available #2482

antlechner commented Jun 26, 2018

antlechner commented Jun 26, 2018

tautschnig commented Jun 26, 2018

antlechner commented Jun 26, 2018 •

edited

Loading

tautschnig left a comment

tautschnig commented Jun 26, 2018

allredj left a comment

antlechner commented Jun 26, 2018

tautschnig commented Jun 26, 2018

antlechner commented Jun 26, 2018

allredj left a comment

allredj left a comment

allredj left a comment

antlechner Jun 27, 2018

antlechner commented Jun 27, 2018

allredj left a comment

allredj left a comment

allredj left a comment

tautschnig commented Jun 27, 2018

tautschnig left a comment

antlechner commented Jun 27, 2018

tautschnig commented Jun 27, 2018

antlechner commented Jun 27, 2018

		@@ -13,6 +13,7 @@ Date: April 2016

		#include "class_hierarchy.h"

		#include <iterator>

Make direct children of a class publicly available #2482

Make direct children of a class publicly available #2482

Conversation

antlechner commented Jun 26, 2018

antlechner commented Jun 26, 2018

tautschnig commented Jun 26, 2018

antlechner commented Jun 26, 2018 • edited Loading

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig commented Jun 26, 2018

allredj left a comment

Choose a reason for hiding this comment

antlechner commented Jun 26, 2018

tautschnig commented Jun 26, 2018

antlechner commented Jun 26, 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

antlechner Jun 27, 2018

Choose a reason for hiding this comment

antlechner commented Jun 27, 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

tautschnig commented Jun 27, 2018

tautschnig left a comment

Choose a reason for hiding this comment

antlechner commented Jun 27, 2018

tautschnig commented Jun 27, 2018

antlechner commented Jun 27, 2018

antlechner commented Jun 26, 2018 •

edited

Loading