Share a common class_hierarchyt instance across multiple users #3216

smowton · 2018-10-22T11:30:23Z

This is an alternative to #3204, see that PR for details.

smowton · 2018-10-22T14:25:33Z

@thk123 note this breaks test-gen; the fix is to mirror the change made in jbmc_parse_options.cpp (owning a class_hierarchyt instance which is then passed to remove_exceptions / remove_instanceof).

tautschnig · 2018-10-22T15:39:59Z

Would it be possible to have the first four commits in a separate PR? It seems those should go in without debate and wouldn't break TG either. Only the last one is really what #3204 was about?!

smowton · 2018-10-22T15:42:56Z

@tautschnig they're just incidental cleanups in the immediate vicinity of the main change, which I split into their own commits to avoid dirtying the main functional ones. I don't think they're significant enough to bother making their own PR.

tautschnig · 2018-10-22T16:29:46Z

Up to you, but I think we might become better at getting changes merged if we were to arrive at a one-commit-per-PR model. There's a cost in rebasing changes to PR authors and re-reviewing to reviewers.

allredj

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

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

peterschrammel

Looks good, but needs a TG bump, @thk123.

thk123

This is in place of the analysis cache I assume? Will make a TG bump now. Otherwise LGTM.

jbmc/src/java_bytecode/remove_exceptions.cpp

thk123 · 2018-10-23T09:05:09Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -529,6 +529,9 @@ int jbmc_parse_optionst::doit()
      *this, options, get_message_handler());
    lazy_goto_model.initialize(cmdline, options);

+    class_hierarchy = util_make_unique<class_hierarchyt>();
+    (*class_hierarchy)(lazy_goto_model.symbol_table);


😕 Can't think of a better way to write this, but is a bit of a head scratcher. 💡 Perhaps pull into a static method in class_hierachy.h: std::unique_ptr<class_hierachyt> create_hierachy(const symbol_tablet &)`?

Added an extra constructor, take another look?

smowton · 2018-10-23T09:10:48Z

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

thk123

Thanks for making the TG bump

thk123 · 2018-10-23T09:49:17Z

src/goto-programs/class_hierarchy.h

@@ -57,6 +57,10 @@ class class_hierarchyt
  void operator()(const symbol_tablet &);

  class_hierarchyt() = default;
+  explicit class_hierarchyt(const symbol_tablet &symbol_table)


💚 Why even have the default constructor + operator? This is perfect!

for cases where the user wants to allocate it in advance, e.g. as a member of another class that won't have access to the symbol table until its own operator(), so I won't kill the no-arg constructor. However agreed this is better when possible.

thk123 · 2018-10-23T09:49:39Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -606,12 +609,13 @@ int jbmc_parse_optionst::get_goto_program(
      *this, options, get_message_handler());
    lazy_goto_model.initialize(cmdline, options);

+    class_hierarchy = util_make_unique<class_hierarchyt>();


⛏️ Use the new constructor

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 9998ed8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88821470
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 734dedf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88824136
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 1b43a8a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88835479
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

owen-mc-diffblue · 2018-10-23T15:26:33Z

jbmc/src/jbmc/jbmc_parse_options.cpp

-      class_hierarchyt hierarchy;
-      hierarchy(lazy_goto_model.symbol_table);
-      show_class_hierarchy(hierarchy, ui_message_handler);
+      show_class_hierarchy((*class_hierarchy), ui_message_handler);


Why the extra brackets?

oops, fixed

smowton · 2018-10-23T15:49:51Z

Merging blocked for now because test-gen can't be validated due to problems with a previous PR merged against cbmc/develop.

Allows alloc-and-init in one go.

The class hierarchy never changes once the symbol table is computed. By sharing one instance owned by the driver program, particularly across function passes, we can avoid many potentially expensive recomputations.

To pacify clang-format. All hail clang-format.

smowton · 2018-10-24T09:34:04Z

Rebased on fixed cbmc/develop

allredj

This PR failed Diffblue compatibility checks (cbmc commit: 5e9aba8).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88984909
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).

The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.

owen-mc-diffblue · 2018-10-24T12:30:56Z

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -552,6 +552,9 @@ int jbmc_parse_optionst::doit()
      *this, options, get_message_handler());
    lazy_goto_model.initialize(cmdline, options);

+    class_hierarchy =
+      util_make_unique<class_hierarchyt>(lazy_goto_model.symbol_table);


Why is this needed here?

smowton requested review from cesaro, cristina-david, NathanJPhillips, peterschrammel, pkesseli and thk123 as code owners October 22, 2018 11:30

smowton mentioned this pull request Oct 22, 2018

Add analysis cache #3204

Closed

5 tasks

smowton changed the title ~~Smowton/feature/shared class hierarchy~~ Share a common class_hierarchyt instance across multiple users Oct 22, 2018

smowton force-pushed the smowton/feature/shared-class-hierarchy branch from f32775c to fff81e8 Compare October 23, 2018 07:13

smowton assigned thk123, tautschnig and peterschrammel and unassigned thk123 Oct 23, 2018

allredj reviewed Oct 23, 2018

View reviewed changes

peterschrammel reviewed Oct 23, 2018

View reviewed changes

thk123 reviewed Oct 23, 2018

View reviewed changes

smowton force-pushed the smowton/feature/shared-class-hierarchy branch from fff81e8 to 5b71f90 Compare October 23, 2018 09:17

smowton requested review from kroening and tautschnig as code owners October 23, 2018 09:17

smowton force-pushed the smowton/feature/shared-class-hierarchy branch 2 times, most recently from 9998ed8 to 734dedf Compare October 23, 2018 09:24

thk123 approved these changes Oct 23, 2018

View reviewed changes

allredj reviewed Oct 23, 2018

View reviewed changes

smowton force-pushed the smowton/feature/shared-class-hierarchy branch from 734dedf to 1b43a8a Compare October 23, 2018 11:16

allredj reviewed Oct 23, 2018

View reviewed changes

owen-mc-diffblue reviewed Oct 23, 2018

View reviewed changes

smowton force-pushed the smowton/feature/shared-class-hierarchy branch from 1b43a8a to cf4c264 Compare October 23, 2018 15:49

smowton added 7 commits October 24, 2018 10:32

Add missing doc-string for a remove_exceptions overload

be44674

Fix missing newline at end of file

253e331

Make jdiff log message match janalyzer

22638e2

Add whitespace between unrelated pass invocations

e39721f

Add one-shot constructor to class_hierarchyt

eb5df0a

Allows alloc-and-init in one go.

Avoid recomputing class hierarchy

df455b8

The class hierarchy never changes once the symbol table is computed. By sharing one instance owned by the driver program, particularly across function passes, we can avoid many potentially expensive recomputations.

Remove unnecessary newline

5e9aba8

To pacify clang-format. All hail clang-format.

smowton force-pushed the smowton/feature/shared-class-hierarchy branch from cf4c264 to 5e9aba8 Compare October 24, 2018 09:32

peterschrammel approved these changes Oct 24, 2018

View reviewed changes

allredj reviewed Oct 24, 2018

View reviewed changes

smowton merged commit af06d4e into diffblue:develop Oct 24, 2018

owen-mc-diffblue reviewed Oct 24, 2018

View reviewed changes

Share a common class_hierarchyt instance across multiple users #3216

Share a common class_hierarchyt instance across multiple users #3216

Uh oh!

Conversation

smowton commented Oct 22, 2018

Uh oh!

smowton commented Oct 22, 2018

Uh oh!

tautschnig commented Oct 22, 2018

Uh oh!

smowton commented Oct 22, 2018

Uh oh!

tautschnig commented Oct 22, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Oct 23, 2018

Uh oh!

thk123 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Oct 23, 2018

Uh oh!

smowton commented Oct 24, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!