Revert irept change that stopped sharing and add unit test #1860

tautschnig · 2018-02-17T10:35:53Z

This is the test from #1855 provided by @NathanJPhillips, with the modification to only make it run when SHARING is enabled.

kroening · 2018-02-19T08:45:05Z

This seems to do more than the title suggests?

tautschnig · 2018-02-19T08:51:52Z

The title might just have been very long and probably had priorities wrong - it's changed now.

tautschnig · 2018-02-19T08:53:59Z

@NathanJPhillips any objections against this one? @smowton is out for the week; anyone else who wants to jump on this one?

kroening · 2018-02-19T08:56:38Z

I should stress that I am happy to re-contemplate using C++ standard library idioms for irept, with a sufficiently strong case that it'll be robust.

NathanJPhillips · 2018-02-19T11:46:08Z

Adding a test and then immediately commenting it out because you know that it would fail seems like a red flag to me. Reuben's change may have been more conservative that it needed to be, but that is better than allowing incorrect behaviour. If you find a bug then it is fine to fix it straight away and then apply optimisations later: incremental is good. The performance impact of Reuben's fix was already analysed and accepted at the time it was applied. Reverting the fix would not be a good solution even if we didn't have the optimisation already in review.

Saying that irept was good for 15 years ignores the fact that we are constantly finding and fixing bugs in CBMC. As we exercise the product on more challenging tasks it is not good enough just to have it work as well as it used to.

tautschnig · 2018-02-19T13:15:43Z

@NathanJPhillips Sentence-by-sentence response:

Adding a test and then immediately commenting it out because you know that it would fail seems like a red flag to me.

Ok, but it seems better than not having a test?

Reuben's change may have been more conservative that it needed to be, but that is better than allowing incorrect behaviour.

No, performance and memory consumption matter. "Allowing" incorrect behaviour is different from exhibiting it.

If you find a bug then it is fine to fix it straight away and then apply optimisations later: incremental is good.

Incrementally following the wrong route permits backtracking, which is what this PR does.

The performance impact of Reuben's fix was already analysed and accepted at the time it was applied.

Which simply shows that my performance analysis was not good enough.

Reverting the fix would not be a good solution even if we didn't have the optimisation already in review.

Why? On the contrary, allowing people to use a broken solution is not a good solution.

Saying that irept was good for 15 years ignores the fact that we are constantly finding and fixing bugs in CBMC.

The way you are conflating one data structure with the entire code base severely undermines the credibility of what you are saying.

As we exercise the product on more challenging tasks it is not good enough just to have it work as well as it used to.

I don't know what the size of your experimental corpus is. Mine is the >400 million lines of C code in Debian.

NathanJPhillips · 2018-02-19T14:19:57Z

I have no disagreements with @tautschnig response. If people aren't convinced by my earlier comment then go ahead with this revert.

martin-cs

Approve because I believe this to be a correct implementation of : #1855 (comment)

FWIW I have noticed a small but significant slow-down in a key use-case today. It was something that was added in the past ... 6-9 months and must be pretty core. I'll try with this patch and see if it changes anything.

martin-cs · 2018-02-20T19:41:42Z

src/util/irep.h

@@ -122,6 +122,7 @@ class irept
  {
    if(data!=&empty_d)
    {
+      // NOLINTNEXTLINE(build/deprecated)
      assert(data->ref_count!=0);


I'd be kinda happier if this was an invariant for the sake of uniformity. I was going to add a comment along the lines of "but everywhere it is used also uses std_expr.h or std_types.h so it won't make much difference" but that's not true (shows how often I wander through the front-end!). Not exactly sure of the impact on build speed but ... I guess we can put off converting this until we've done things like minimising the use of headers to improve build speed.

I am very open to resolving this in a different way, i.e., by actually using INVARIANT. I just feared some undesirable impact.

tautschnig · 2018-02-21T13:57:41Z

I'll try with this patch and see if it changes anything.

@martin-cs, if you have any results on this then please let me know.

tautschnig · 2018-03-23T20:31:34Z

Marking this as do-not-merge as #1970 ought to be merged first and experiments to come up with memory regression tests are in progress.

kroening · 2018-06-08T17:39:58Z

This one seems to be essential before we do the release.

tautschnig · 2018-06-08T18:02:36Z

On top of 63acc5b on a customer-provided
benchmark:

size of program expression: 127981 steps
slicing removed 16144 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to refinement loop with MiniSAT 2.2.1 with simplifier
converting SSA
Running refinement loop with MiniSAT 2.2.1 with simplifier
BV-Refinement: post-processing
BV-Refinement: iteration 1
1014336 variables, 4131455 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
BV-Refinement: got UNSAT, and the proof passes => UNSAT
Total iterations: 1
Runtime decision procedure: 1.84756s

User time (seconds): 16.42
User time (seconds): 16.43
User time (seconds): 16.41

#1855 + #2316
User time (seconds): 14.14
User time (seconds): 13.97
User time (seconds): 14.03
86633882 calls to small_shared_ptrtirept::dt::~small_shared_ptrt()

#1860 + #2316
User time (seconds): 12.39
User time (seconds): 12.57
User time (seconds): 12.64

#2316
User time (seconds): 14.66
User time (seconds): 14.52
User time (seconds): 14.38
105950686 calls to small_shared_ptrtirept::dt::~small_shared_ptrt()

This partially reverts commit b741d4b. While safer to use, these changes prevented sharing on irept's where non-const references had been taken to any irept stored in their sub/named_sub collections. The newly introduced cow.h and small_shared_ptr.h are kept in place, but all modifications to irept are reverted.

Using invariant.h would drag in a number of additional headers into almost every file thus it seems preferable to maintain the assert here.

Separately test irept and exprt, where the latter are expected to have the very same behaviour.

allredj

This PR failed Diffblue compatibility checks (cbmc commit: cbce4bc).
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 needs an update PR to test-gen.

tautschnig · 2018-06-14T11:59:59Z

What is it that this PR breaks in test-gen? That's a bit unexpected, except if it is about missing include files (which should likely be fixed either way).

allredj · 2018-06-14T12:01:48Z

Seems to be a missing include, indeed.

allredj · 2018-06-14T12:23:09Z

Test-gen update is ready for review: https://github.com/diffblue/test-gen/pull/1941

allredj · 2018-06-14T14:08:36Z

Sorry the test-gen update exhibited a another bug. I'll try to fix all that as quickly as possible, but that might not be done today...

kroening · 2018-06-18T11:04:17Z

This is getting urgent, as blocking release!

allredj · 2018-06-18T11:49:45Z

The submodule update https://github.com/diffblue/test-gen/pull/1941 has now been rebase on the fix. Waiting for CI.

allredj · 2018-06-18T13:04:52Z

@tautschnig could you please rebase on cbmc/develop?

allredj · 2018-06-18T16:36:46Z

@kroening this needs a rebase on cbmc/develop.

8a7893c Merge pull request diffblue#2375 from diffblue/unit-dependencies 9258284 fix build depenencies of unit test binary f7cd161 Merge pull request diffblue#2371 from diffblue/fix-tests2 82753bc make test independent of index type f5f32da Merge pull request diffblue#2364 from smowton/smowton/fix/autodetect-default-cxx-dialect d437f60 Merge pull request diffblue#2368 from polgreen/doc_replace_func_bodies 6048517 Merge pull request diffblue#2353 from tautschnig/g++8-fixes2 e2e6d82 Merge pull request diffblue#2190 from tautschnig/more-stats 7210136 Make it clearer that <=> will always be stringified 560f82b Travis: test more g++ and clang versions d46a55c Add new goto-instrument option print-global-state-size 961b29a Silence GCC 8's warning about using realloc/memmove on non-POD ca1b03c Documentation wording for replace function bodies d8c5a98 Cleanup options handling of count-eloc, list-eloc, print-path-lengths 6cd6d31 Unit test framwork: use references when catching exceptions 6882da6 Merge pull request diffblue#2367 from diffblue/fix-tests bcc3bef make regression/cbmc/bounds_check1 independent of types used 4de4538 switch regression/cbmc/Typecast2 to preprocessed code 91a9c64 Amend two tests that explicitly target C++98 2b2b797 goto-gcc: select default language standard depending on emulated compiler 52a8afc Merge pull request diffblue#1898 from tautschnig/always-inline cbe691b Merge pull request diffblue#2363 from diffblue/Makefile-TAR 9d40a9e Merge pull request diffblue#2365 from diffblue/solaris_errno 9efd705 add model for ___errno for Solaris 11 eaa2e05 update Solaris instructions 2f142d5 allow customizing the tar command for solver download 8cc1848 Merge pull request diffblue#1860 from tautschnig/restore-irept-sharing fea5db0 Merge pull request diffblue#2361 from diffblue/fix-goto2 7c0d750 Merge pull request diffblue#2362 from smowton/smowton/fix/tolerate-cxx-namespace-attribute e440a25 introduce INCOMPLETE_GOTO and turn guarded goto into a stateless pass 1f1835b C++ frontend: tolerate namespace attributes cbce4bc Unit test of irept's public API abdb044 Unit test to check that irept implements sharing d58fd18 Silence the linter on assert in irep.h 3d64070 Partially revert "Use small intrusive pointer in irep" 688a0ab Macros are not needed outside translation units 9c93f59 Fully interpret __attribute__((always_inline)) d1f617b Apply symbol replacement in type_arg members git-subtree-dir: cbmc git-subtree-split: 8a7893c

tautschnig mentioned this pull request Feb 17, 2018

Restore irept sharing #1855

Closed

tautschnig force-pushed the restore-irept-sharing branch 2 times, most recently from fae5b58 to cffaf8b Compare February 17, 2018 13:39

tautschnig requested review from kroening, peterschrammel and smowton as code owners February 17, 2018 13:39

tautschnig changed the title ~~Unit test to check that irept implements sharing~~ Unit test to check that irept implements sharing and revert change that stopped sharing Feb 17, 2018

tautschnig force-pushed the restore-irept-sharing branch 2 times, most recently from 6f51d21 to 83b1bb4 Compare February 17, 2018 22:18

tautschnig requested review from cesaro, mgudemann and thk123 as code owners February 17, 2018 22:18

tautschnig added the bugfix label Feb 17, 2018

tautschnig force-pushed the restore-irept-sharing branch from 83b1bb4 to e4a88e3 Compare February 17, 2018 22:48

peterschrammel approved these changes Feb 18, 2018

View reviewed changes

tautschnig changed the title ~~Unit test to check that irept implements sharing and revert change that stopped sharing~~ Revert irept change that stopped sharing and add unit test Feb 19, 2018

kroening approved these changes Feb 19, 2018

View reviewed changes

martin-cs approved these changes Feb 20, 2018

View reviewed changes

tautschnig self-assigned this Feb 21, 2018

tautschnig assigned martin-cs Feb 21, 2018

tautschnig force-pushed the restore-irept-sharing branch 2 times, most recently from 743b042 to 3c3b88c Compare March 22, 2018 20:11

tautschnig mentioned this pull request Mar 23, 2018

Java bytecode build fixes #1970

Merged

tautschnig added the do not merge label Mar 23, 2018

tautschnig force-pushed the restore-irept-sharing branch from 920f9e4 to 28b337b Compare March 24, 2018 18:23

tautschnig mentioned this pull request Mar 25, 2018

Memory regression test [blocks: #2035] #1971

Closed

tautschnig force-pushed the restore-irept-sharing branch 3 times, most recently from 68ef907 to d2e2802 Compare March 27, 2018 17:31

tautschnig and others added 4 commits June 14, 2018 08:57

Silence the linter on assert in irep.h

d58fd18

Using invariant.h would drag in a number of additional headers into almost every file thus it seems preferable to maintain the assert here.

Unit test to check that irept implements sharing

abdb044

Separately test irept and exprt, where the latter are expected to have the very same behaviour.

Unit test of irept's public API

cbce4bc

tautschnig force-pushed the restore-irept-sharing branch 2 times, most recently from cc49fcb to cbce4bc Compare June 14, 2018 09:13

allredj reviewed Jun 14, 2018

View reviewed changes

allredj suggested changes Jun 14, 2018

View reviewed changes

kroening removed the do not merge label Jun 18, 2018

kroening merged commit 8cc1848 into diffblue:develop Jun 19, 2018

tautschnig deleted the restore-irept-sharing branch January 11, 2019 15:59

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Revert irept change that stopped sharing and add unit test #1860

Revert irept change that stopped sharing and add unit test #1860

tautschnig commented Feb 17, 2018

kroening commented Feb 19, 2018

tautschnig commented Feb 19, 2018

tautschnig commented Feb 19, 2018

kroening commented Feb 19, 2018

NathanJPhillips commented Feb 19, 2018 •

edited

Loading

tautschnig commented Feb 19, 2018

NathanJPhillips commented Feb 19, 2018

martin-cs left a comment

martin-cs Feb 20, 2018

tautschnig Feb 21, 2018

tautschnig commented Feb 21, 2018

tautschnig commented Mar 23, 2018

kroening commented Jun 8, 2018

tautschnig commented Jun 8, 2018

allredj left a comment

allredj left a comment

tautschnig commented Jun 14, 2018

allredj commented Jun 14, 2018

allredj commented Jun 14, 2018

allredj commented Jun 14, 2018

kroening commented Jun 18, 2018

allredj commented Jun 18, 2018

allredj commented Jun 18, 2018

allredj commented Jun 18, 2018

Revert irept change that stopped sharing and add unit test #1860

Revert irept change that stopped sharing and add unit test #1860

Conversation

tautschnig commented Feb 17, 2018

kroening commented Feb 19, 2018

tautschnig commented Feb 19, 2018

tautschnig commented Feb 19, 2018

kroening commented Feb 19, 2018

NathanJPhillips commented Feb 19, 2018 • edited Loading

tautschnig commented Feb 19, 2018

NathanJPhillips commented Feb 19, 2018

martin-cs left a comment

Choose a reason for hiding this comment

martin-cs Feb 20, 2018

Choose a reason for hiding this comment

tautschnig Feb 21, 2018

Choose a reason for hiding this comment

tautschnig commented Feb 21, 2018

tautschnig commented Mar 23, 2018

kroening commented Jun 8, 2018

tautschnig commented Jun 8, 2018

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 14, 2018

allredj commented Jun 14, 2018

allredj commented Jun 14, 2018

allredj commented Jun 14, 2018

kroening commented Jun 18, 2018

allredj commented Jun 18, 2018

allredj commented Jun 18, 2018

allredj commented Jun 18, 2018

NathanJPhillips commented Feb 19, 2018 •

edited

Loading