Add null check on virtual function calls after its subexpressions #3469
Conversation
smowton
requested review from
cesaro,
cristina-david,
NathanJPhillips,
peterschrammel,
pkesseli and
thk123
as code owners
smowton
force-pushed
the
smowton/fix/java-null-check-ordering
branch
from
01c5f1a to
4e7f03b
Compare
smowton
force-pushed
the
smowton/fix/java-null-check-ordering
branch
from
4e7f03b to
c163469
Compare
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: c163469).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92705699
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.
There was a problem hiding this comment.
Change looks correct - the unit tests are nice, but I'm not sure about exactly how they are structured. I also think it'd be nice to add an integration/regression test for where this is going wrong (i.e your example without field = new B() presumably does something wrong?)
| goto_functions.function_map.at("java::VirtualCallNullChecks.main:()V"); | ||
|
|
||
| THEN("The callee should be of the form some_ptr->field") | ||
| { |
There was a problem hiding this comment.
❓ I'm not sure on the point of this THEN block - is it just to check that the first function call is what you're expecting? ⛏️ It might be a little clearer to use std::find_if and perhaps a check that is really is the function call you're looking for (i.e. the identifier is java::B.virtualmethod:()V)
There was a problem hiding this comment.
Yes, it's to stop the test passing because I loaded an empty class file or the compiler optimised the call away or similar. I'll add a comment.
| THEN("All pointer usages should be safe") | ||
| { | ||
| local_safe_pointerst safe_pointers(ns); | ||
| safe_pointers(main_function.body); |
There was a problem hiding this comment.
I'm not sure it is best practise for unit test to depend on an entirely separate analysis (it seems as likely as not that this analysis would miss that ASSUME(a->b != null && a != null) a->b.function() TBH. I'd probably explicitly assert what you're expecting in the code
There was a problem hiding this comment.
It's tricky -- I want to assert that every use of a pointer is preceded by a corresponding ptr != null assumption. I can write that, but it would be an exact rewrite of safe_pointers :)
|
Joel-bot is failing due to a previously merged PR - can't see this causing any compile errors, but once that relevant PR is merged, I'll do a manual bump for this to check it doesn't cause any unexpected changes to tests. |
| goto_functionst goto_functions; | ||
| goto_convert(symbol_table, goto_functions, null_message_handler); | ||
|
|
||
| WHEN("The virtual call is converted") |
There was a problem hiding this comment.
Strictly the code to do this should be in this block.
smowton
force-pushed
the
smowton/fix/java-null-check-ordering
branch
3 times, most recently
from
713025e to
fd1ded1
Compare
|
@thk123 added comments and a regression test. The regression test is awkward because it's hard to talk about two different derefs on the same line, but hopefully it suffices with the unit test also present. |
For example, for "x->y . f()" we should `assert(x != null); assert(x->y != null);`, not the other way around.
smowton
force-pushed
the
smowton/fix/java-null-check-ordering
branch
from
fd1ded1 to
6af4d4e
Compare
| @@ -0,0 +1,26 @@ | |||
| public class Test { | |||
|
|
|||
| public static void main(int argc) { | |||
There was a problem hiding this comment.
⛏️ Would rather only use main methods for actual main methods (e.g. one that takes a String[] args)
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: 6af4d4e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92737138
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.
For example, for "x->y . f()" we should
assert(x != null); assert(x->y != null);, not the other way around.