Feature/new instrumentation runtime exceptions #912
Conversation
cristina-david
force-pushed
the
feature/new-instrumentation-runtime-exceptions
branch
from
229ddc4 to
e262241
Compare
thk123
left a comment
thk123
left a comment
There was a problem hiding this comment.
Looks good - seems to be missing at least a couple of test cases (I think ideally there would also be test cases for when --java-throw-runttime-execptions isn't enabled as it isn't clear what the expected behaviour is then.
There was a problem hiding this comment.
To avoid having to fix this in 4 places - could a helper function get_exception(const irep_idt &exception_type) handle this logic?
There was a problem hiding this comment.
Not a suggested change - but I don't really understand what the code looks like if throw_runtime_exceptions is disabled - perhaps some documentation (or maybe extract this also into a method so you can document in the name?)
There was a problem hiding this comment.
One letter variable names aren't advised by the coding standard - perhaps something that explains what this code block does? array_index_read_block?
There was a problem hiding this comment.
Yes, I agree. However, the c here is declared much earlier in the function (https://github.com/cristina-david/cbmc/blob/feature/new-instrumentation-runtime-exceptions/src/java_bytecode/java_bytecode_convert_method.cpp#L1454) and used to set the converted instruction. So, I would like to avoid changing it everywhere in this PR.
There was a problem hiding this comment.
It would be nice if the test could test more than this - I don't know if this is possible on CBMC, but something that actually validates that CBMC has figured out a run time exception should be thrown
There was a problem hiding this comment.
I don't see a test that validates this, unless this test does: NullPointerException1 but this is currently KNOWNBUG and doesn't enable the --throw-runtime-exceptions`.
There was a problem hiding this comment.
I've added NullPointerException2.
There was a problem hiding this comment.
Also missing a test as far as I can tell.
src/cbmc/cbmc_parse_options.h
Outdated
smowton
left a comment
smowton
left a comment
There was a problem hiding this comment.
Some correctness questions
There was a problem hiding this comment.
Surely this should have prefix java::java.lang.
There was a problem hiding this comment.
Should be or_exprt I think? I believe this is testing for idx < 0 && idx >= arr.length
There was a problem hiding this comment.
Similar qualifying of the name to above
There was a problem hiding this comment.
Similar to above, this seems to throw if length >= 0?
There was a problem hiding this comment.
I think op != null && op instanceof Target -> op != null && !op instanceof Target
cristina-david
force-pushed
the
feature/new-instrumentation-runtime-exceptions
branch
4 times, most recently
from
0df5a69 to
75bdc66
Compare
cristina-david
force-pushed
the
feature/new-instrumentation-runtime-exceptions
branch
3 times, most recently
from
9bcf8a4 to
d6a4f3a
Compare
cristina-david
force-pushed
the
feature/new-instrumentation-runtime-exceptions
branch
from
d6a4f3a to
18714d5
Compare
|
@thk123 I added more regression tests, including some that do not set the |
cristina-david
force-pushed
the
feature/new-instrumentation-runtime-exceptions
branch
from
ed4e2c3 to
20f8791
Compare
smowton
left a comment
smowton
left a comment
There was a problem hiding this comment.
LGTM, just one possible change:
Since the old-style logic now largely duplicates the code in the functions that creates exceptions, could we factor that in? For example, could we rename throw_exception -> check_condition (bool use_exception, exprt cond), where check_condition either asserts !cond or generates if(cond) throw ... depending on the use_exception parameter?
|
@cristina-david can this be merged? Already approved by @smowton and @thk123 |
|
This is now part of #1019 together with more refactoring so I'll close it here. |
4 participants
This PR introduces the flag --java-throw-runtime-exceptions such that, whenever used, instead of adding runtime exceptions instrumentation in the form of assertions, we actually throw the corresponding exceptions.
The only problem here is that some of the instrumentation for NullPointerException is added in goto_check.cpp, whereas the rest of the instrumentation is added earlier in java_bytecode_convert_method.cpp. In my opinion, we should do all the instrumentation before goto_check.cpp for two reasons: 1. the exceptions to be thrown are language specific; 2. we presumably don't want to instrument all the dereferences given that many are introduced by us, e.g. when accessing array->length, and they shouldn't throw an exception. Therefore, I've added all the exception throwing instrumentation, including that for null dereference, in java_bytecode_convert_method.cpp. For now, I didn't touch the instrumentation in goto_check.cpp, but I think it should be disabled whenever the --java-throw-runtime-exceptions flag is on. Otherwise, we introduce redundant instrumentation.