Tighten up global extern detection in phi_function #3752
Conversation
JohnDumbell
requested review from
kroening,
peterschrammel and
tautschnig
as code owners
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: aa8ca8a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/96936683
|
@JohnDumbell Could you please rebase? It seems Travis is acting up. |
|
There is the potentially problematic assumption here that a statically allocated variable is initialised if the symbol's .value member is non-nil. |
JohnDumbell
force-pushed
the
jd/enhancement/phi_merge_explicit_exclude_extern
branch
from
aa8ca8a to
0e1b02a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 0e1b02a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97023637
| ^.*:\s+dynamic_object[0-9]+(@[0-9]+)?#0\) | ||
| ^.*\?\s+dynamic_object[0-9]+(@[0-9]+)?#0\s+: | ||
| \([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\) | ||
| \([^\s]+guard[^\s]+ \? [^\s]+#0 : [^\s]+\) |
There was a problem hiding this comment.
Here and below: these are duplicates, should be checking for the else position
|
@kroening fair point, how about just saying all globals are merged "naturally" (i.e. it's up to the frontend to construct a program where global initialisation trivially dominates the rest of the program, which is usually true because it happens in Locals, dynamic objects we can both guarantee that gen 0 is not reachable, as we always assign them an explicit nondet value when they are |
|
@JohnDumbell if accepted that would correspond to |
JohnDumbell
force-pushed
the
jd/enhancement/phi_merge_explicit_exclude_extern
branch
from
0e1b02a to
2f819cf
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 2f819cf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97038298
|
@JohnDumbell I spoke to @kroening -- he's happy with the plan proposed above |
The is_not_nil check was a little broad and causing uninitialized values to get merged in some situations. Made the condition for being an external global stricter.
The tests that should have caught this were too specific when checking for the names of the variables and at some point in the past dynamic_object got given a prefix, which meant that the check to make sure no zero generation existed always passed (even with a #0 there) because the variable name wasn't exact. Made the matching far more forgiving and it now looks for anything that vaguely looks like a guard statement with a 0 generation object.
JohnDumbell
force-pushed
the
jd/enhancement/phi_merge_explicit_exclude_extern
branch
from
2f819cf to
466ac7a
Compare
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 466ac7a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/97288170
The external check was a little too broad and some gen 0 dynamic objects were getting put into guards accidentally. The tests that would have helped show something had changed were also quite badly out of date which didn't help matters.
@tautschnig I made sure your additional test passes, but please just check that the new condition is good for whatever you needed too. (I was thinking the the is_not_nil could go if global externs should never be considered for removal)