Do not assign to objects that have gone out of scope #1116
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
pkesseli
reviewed
Jul 11, 2017
src/goto-symex/symex_goto.cpp
Outdated
| // do not merge when we don't have a local symbol in the goto | ||
| // state; those should have been filtered out already in | ||
| // goto_symext::symex_assign_symbol | ||
| CHECK_RETURN(l2!=0 || it->get_level_1().empty()); |
There was a problem hiding this comment.
This assertion gets violated with local_out_of_scope4.c:
extern int OPCODE;
void f(int *opcode) {
if(*opcode==0)
int *opcode_trace=opcode;
else
__CPROVER_assume(0==1);
}
void main(void)
{
f(&OPCODE);
__CPROVER_assert(0==1, "");
}There was a problem hiding this comment.
Yes, it seems I've got quite a bit more work to do here. I've figured out some of the cases (function parameters), with others still to be done. My apologies that this is taking much longer than expected.
There was a problem hiding this comment.
My apologies for dragging up such obscure use cases ;-) . Unfortunately the CEGIS module applies arrays of pointers in a lot of scenarios.
Pointer dereferencing may yield objects that have meanwhile gone out of scope. Assigning to them is unnecessary, and performing a merge on those would yield inconsistent equations (as witnessed by the included regression test). Filtering out the merge in phi nodes is not easily possible as there are several cases where it is permissible that only one of the states entering the phi node has an (L1) object, such as declarations only seen in one branch. Fixes: diffblue#1115
|
I hope to have addressed all failures in this updated version of the patch. |
pkesseli
approved these changes
Jul 12, 2017
peterschrammel
approved these changes
Jul 12, 2017
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Pointer dereferencing may yield objects that have meanwhile gone out of scope.
As an optimisation, assigning to them is unnecessary. It is, however, essential
not to perform a merge when only one of the states entering the phi node
actually has an (L1) object. The optimisation guarantees that the latter does
not happen.
Fixes: #1115