Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486] by tautschnig · Pull Request #2220 · diffblue/cbmc

tautschnig · 2018-05-22T10:52:51Z

With level-2 counters incremented on declaration and non-deterministic
initialisation upon allocation, the only remaining sources are pointer
dereferencing, where uninitialised objects necessarily refer to invalid objects.

This is a cleaner implementation of 369f077.

This is another bit factored out from #35.

smowton

Should rename the PR? Since #2168 has landed in the meantime this is really just a cleanup now I think?

tautschnig · 2018-05-23T07:51:00Z

Should rename the PR? Since #2168 has landed in the meantime this is really just a cleanup now I think?

Not entirely: the implementation in #2168 did not yet consider the case that neither branch had SSA level2 at zero, which would occur with uninitialized globals, hence the argc/argv/envp fix in this PR before doing the "cleanup" part.

smowton · 2018-05-23T08:14:19Z

Aha, in that case can we have a test to exhibit the change here?

tautschnig · 2018-06-07T19:02:02Z

@smowton Apologies for the delay. I have amended the commit message, adding: "Removing only the code introduced in 369f077 would yield a wrong result for regression/cbmc/Local_out_of_scope3." -- so the test is actually already in place.

smowton · 2018-06-08T09:32:09Z

Cool, in that case lgtm

allredj

Passed Diffblue compatibility checks (cbmc commit: ec8c07c).

peterschrammel

A couple of clang-format complaints, otherwise good to go.

smowton · 2018-07-05T08:01:06Z

@tautschnig is there a reason you dropped this? Looks good to go AFAICT. There were a couple of spurious Travis failures that I just restarted.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 2311826).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90528381

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: c7f9d6e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90998307

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 8f1745d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93272998

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 04d5957).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/93794605

tautschnig · 2018-12-19T13:13:38Z

This now fixes even more bugs with fewer changes.

smowton · 2018-12-19T14:19:26Z

src/goto-symex/symex_goto.cpp

+    (dest_count == 0 && !symbol.value.is_not_nil()))
  {
-    rhs = dest_state_rhs;
+    if(goto_count == 0)


Note the dest_count == 0 && goto_count == 0 case is forbidden above, so this implies `dest_state.guard.is_false() && dest_count != 0) -- not sure if this can be distangled to make that clearer, or perhaps clarify with a comment

If dest_state.guard.is_false() then really we don't care about dest_count, because it sits on a dead branch. Any idea what you'd like the comment to say?

How about just pulling out

if( (dest_state.guard.is_false() && goto_count == 0) || (goto_state.guard.is_false() && dest_count == 0)) { return; }

It does mean testing is_false() multiple times, but it makes it clearer which cases are possible. Comment-wise, I guess we should add something like // If the symbol is not initialised on one path and the other path is unreachable we don't need to generate anything

Mind taking another look at the latest version of this PR? Your comments helped make clear which change fixes which bug!

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 72f3bea).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95266652

In 646cf29, initialisation of dynamic objects was added, but extern symbols were not considered. Includes a test that fails without this fix.

…object With level-2 counters incremented on declaration and non-deterministic initialisation upon allocation, the only remaining sources are pointer dereferencing, where uninitialised objects necessarily refer to invalid objects. This is a cleaner implementation of 369f077. Removing only the code introduced in 369f077 would yield a wrong result for regression/cbmc/Local_out_of_scope3. Fixes: diffblue#1630

smowton

Looks good! I have a feeling the previous version used !is_not_nil() where the current one uses is_not_nil() (without the !), so double-check that?

tautschnig · 2018-12-19T17:35:31Z

Looks good! I have a feeling the previous version used !is_not_nil() where the current one uses is_not_nil() (without the !), so double-check that?

Well, one of them did... - which was a bug...

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: eaa7d93).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/95298901

tautschnig requested review from kroening and peterschrammel as code owners May 22, 2018 10:52

smowton approved these changes May 23, 2018

View reviewed changes

tautschnig assigned kroening and peterschrammel May 23, 2018

tautschnig assigned tautschnig and unassigned kroening and peterschrammel Jun 1, 2018

tautschnig force-pushed the phi-cleanup branch from 039803d to 22a7844 Compare June 7, 2018 19:00

tautschnig changed the title ~~Skip phi assignment if neither merged state has an initialised object~~ Skip phi assignment if one of the merged states has an uninitialised object Jun 7, 2018

tautschnig assigned kroening and peterschrammel and unassigned tautschnig Jun 7, 2018

tautschnig force-pushed the phi-cleanup branch 3 times, most recently from c82bfd7 to ec8c07c Compare June 14, 2018 07:56

allredj reviewed Jun 14, 2018

View reviewed changes

peterschrammel approved these changes Jun 14, 2018

View reviewed changes

tautschnig assigned tautschnig and unassigned peterschrammel Jun 14, 2018

tautschnig force-pushed the phi-cleanup branch from ec8c07c to ea7c5c1 Compare June 20, 2018 07:22

tautschnig removed their assignment Jun 20, 2018

tautschnig assigned tautschnig and unassigned kroening Jul 6, 2018

tautschnig force-pushed the phi-cleanup branch from ea7c5c1 to 3f7757e Compare September 3, 2018 18:41

tautschnig changed the title ~~Skip phi assignment if one of the merged states has an uninitialised object~~ Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574] Nov 7, 2018

allredj reviewed Nov 7, 2018

View reviewed changes

tautschnig force-pushed the phi-cleanup branch 4 times, most recently from 7359f23 to c7f9d6e Compare November 11, 2018 22:16

allredj reviewed Nov 11, 2018

View reviewed changes

This was referenced Nov 27, 2018

Symex wrongly nondets local variable inherited after START_THREAD #1630

Closed

Patch set for SV-COMP'19 [depends-on: #2000, #3462] #3486

Closed

tautschnig force-pushed the phi-cleanup branch from c7f9d6e to 124c7ff Compare December 1, 2018 09:21

tautschnig changed the title ~~Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574]~~ Skip phi assignment if one of the merged states has an uninitialised object [blocks: #35, #2574, #3486] Dec 1, 2018

tautschnig added the bugfix label Dec 1, 2018

tautschnig force-pushed the phi-cleanup branch from 124c7ff to 8f1745d Compare December 2, 2018 09:21

allredj reviewed Dec 2, 2018

View reviewed changes

tautschnig force-pushed the phi-cleanup branch from 8f1745d to 04d5957 Compare December 6, 2018 09:38

allredj reviewed Dec 6, 2018

View reviewed changes

tautschnig force-pushed the phi-cleanup branch from 04d5957 to 72f3bea Compare December 19, 2018 13:12

smowton reviewed Dec 19, 2018

View reviewed changes

allredj reviewed Dec 19, 2018

View reviewed changes

tautschnig force-pushed the phi-cleanup branch from 72f3bea to 6184ab0 Compare December 19, 2018 15:23

tautschnig added 2 commits December 19, 2018 17:03

Fix handling of extern symbols in phi_function

e743f02

In 646cf29, initialisation of dynamic objects was added, but extern symbols were not considered. Includes a test that fails without this fix.

tautschnig force-pushed the phi-cleanup branch from 6184ab0 to eaa7d93 Compare December 19, 2018 17:03

smowton approved these changes Dec 19, 2018

View reviewed changes

allredj reviewed Dec 19, 2018

View reviewed changes

tautschnig merged commit a94389d into diffblue:develop Dec 19, 2018

tautschnig deleted the phi-cleanup branch December 19, 2018 18:32

tautschnig mentioned this pull request Dec 21, 2018

[SV-COMP'18 15/19] Cure of consequences of some concurrency bug related to pthread_join. #2004

Closed

Conversation

tautschnig commented May 22, 2018

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented May 23, 2018

Uh oh!

smowton commented May 23, 2018

Uh oh!

tautschnig commented Jun 7, 2018

Uh oh!

smowton commented Jun 8, 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!

smowton commented Jul 5, 2018

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!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Dec 19, 2018

Uh oh!

smowton Dec 19, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Dec 19, 2018

Choose a reason for hiding this comment

Uh oh!

smowton Dec 19, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Dec 19, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Dec 19, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants