Feature/new instrumentation runtime exceptions #912

cristina-david · 2017-05-12T10:03:23Z

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.

thk123

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.

thk123 · 2017-05-23T16:32:35Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  const exprt &class2,
+  const source_locationt &original_loc)
+{
+  // TODO: use std::move


To avoid having to fix this in 4 places - could a helper function get_exception(const irep_idt &exception_type) handle this logic?

thk123 · 2017-05-23T16:35:05Z

src/java_bytecode/java_bytecode_convert_method.cpp

+      }
+      else
+      {
+        const typecast_exprt lhs(op[0], pointer_typet(empty_typet()));


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?)

thk123 · 2017-05-23T16:36:22Z

src/java_bytecode/java_bytecode_convert_method.cpp

-      check.add_source_location()
-        .set_property_class("array-create-negative-size");
-      checkandcreate.move_to_operands(check);
+      c=code_blockt();


One letter variable names aren't advised by the coding standard - perhaps something that explains what this code block does? array_index_read_block?

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.

thk123 · 2017-05-23T16:37:48Z

regression/cbmc-java/NegativeArraySizeException/test.desc

+--java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$


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

thk123 · 2017-05-23T16:38:43Z

src/java_bytecode/java_bytecode_convert_method_class.h

+    const exprt &length,
+    const source_locationt &original_sloc);
+
+  codet throw_null_dereference_exception(


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`.

I've added NullPointerException2.

thk123 · 2017-05-23T16:38:54Z

src/java_bytecode/java_bytecode_convert_method_class.h

+    const exprt &expr,
+    const source_locationt &original_sloc);
+
+  codet throw_class_cast_exception(


Also missing a test as far as I can tell.

thk123 · 2017-05-23T16:39:38Z

src/cbmc/cbmc_parse_options.h

@@ -61,6 +61,7 @@ class optionst;
  "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
  "(graphml-witness):" \
  "(java-max-vla-length):(java-unwind-enum-static)" \
+  "(java-throw-runtime-exceptions)" \


Missing help documentation

smowton

Some correctness questions

smowton · 2017-05-24T12:10:49Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  {
+    exc_symbol.is_static_lifetime=true;
+    exc_symbol.base_name="ArrayIndexOutOfBoundsException";
+    exc_symbol.name="ArrayIndexOutOfBoundsException";


Surely this should have prefix java::java.lang.

smowton · 2017-05-24T12:11:56Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  const binary_relation_exprt lt_zero(idx, ID_lt, zero);
+  const member_exprt length_field(array_struct, "length", java_int_type());
+  const binary_relation_exprt ge_length(idx, ID_ge, length_field);
+  const and_exprt and_expr(lt_zero, ge_length);


Should be or_exprt I think? I believe this is testing for idx < 0 && idx >= arr.length

smowton · 2017-05-24T12:12:32Z

src/java_bytecode/java_bytecode_convert_method.cpp

+  const source_locationt &original_loc)
+{
+  symbolt exc_symbol;
+  if(!symbol_table.has_symbol("NegativeArraySizeException"))


Similar qualifying of the name to above

smowton · 2017-05-24T12:14:06Z

src/java_bytecode/java_bytecode_convert_method.cpp

+
+  code_ifthenelset if_code;
+  if_code.add_source_location()=original_loc;
+  if_code.cond()=ge_zero;


Similar to above, this seems to throw if length >= 0?

smowton · 2017-05-24T12:16:26Z

src/java_bytecode/java_bytecode_convert_method.cpp

+
+  code_ifthenelset if_code;
+  if_code.add_source_location()=original_loc;
+  if_code.cond()=and_expr;


I think op != null && op instanceof Target -> op != null && !op instanceof Target

…ception

cristina-david · 2017-05-31T09:30:29Z

@thk123 I added more regression tests, including some that do not set the --java-throw-runtime-exceptions flag for NullPointerException and ClassCastException.

cristina-david · 2017-05-31T09:44:30Z

@smowton and @thk123 Thanks for your comments, I think I've addressed all of them.

smowton

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?

sara-db · 2017-06-22T08:32:43Z

@cristina-david can this be merged? Already approved by @smowton and @thk123

cristina-david · 2017-06-29T10:28:56Z

This is now part of #1019 together with more refactoring so I'll close it here.

cristina-david force-pushed the feature/new-instrumentation-runtime-exceptions branch from 229ddc4 to e262241 Compare May 12, 2017 10:23

cristina-david mentioned this pull request May 22, 2017

Throw ArithmeticException whenever a division-by-zero is encountered #950

Closed

thk123 suggested changes May 23, 2017

View reviewed changes

smowton suggested changes May 24, 2017

View reviewed changes

cristina-david force-pushed the feature/new-instrumentation-runtime-exceptions branch 4 times, most recently from 0df5a69 to 75bdc66 Compare May 30, 2017 14:54

cristina-david added 9 commits May 30, 2017 16:30

Add instrumentation that throws exceptions

27b4597

Add --java-throw-runtime-exceptions flag

b8d9415

Add instrumentation for throwing NullPointerException and ClassCastEx…

17575c5

…ception

Add instrumentation for NegativeArraySizeException

adb3b18

Add instrumentation for NegativeArraySizeException

58e2ca3

Add instrumentation for ArrayIndexOutOfBoundsException

7894cbb

Add regression test for NegativeArraySizeException

9f9b22d

Add regression test for ArrayIndexOutOfBoundsException

3ac8e40

Use better function names

e960c50

cristina-david force-pushed the feature/new-instrumentation-runtime-exceptions branch 3 times, most recently from 9bcf8a4 to d6a4f3a Compare May 30, 2017 17:31

cristina-david added 3 commits May 31, 2017 08:53

Address reviewers comments

60c7c8c

Added regression test for throwing NullPointerException

30e7349

Added more comments

18714d5

cristina-david force-pushed the feature/new-instrumentation-runtime-exceptions branch from d6a4f3a to 18714d5 Compare May 31, 2017 07:53

Added more regression tests for runtime exceptions

20f8791

cristina-david force-pushed the feature/new-instrumentation-runtime-exceptions branch from ed4e2c3 to 20f8791 Compare May 31, 2017 09:41

thk123 approved these changes May 31, 2017

View reviewed changes

smowton approved these changes May 31, 2017

View reviewed changes

cristina-david closed this Jun 29, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feature/new instrumentation runtime exceptions #912

Feature/new instrumentation runtime exceptions #912

cristina-david commented May 12, 2017

thk123 left a comment

thk123 May 23, 2017

thk123 May 23, 2017

thk123 May 23, 2017

cristina-david May 30, 2017 •

edited

Loading

thk123 May 23, 2017

thk123 May 23, 2017

cristina-david May 30, 2017

thk123 May 23, 2017

thk123 May 23, 2017

cristina-david May 30, 2017

smowton left a comment

smowton May 24, 2017

smowton May 24, 2017

smowton May 24, 2017

smowton May 24, 2017

smowton May 24, 2017

cristina-david commented May 31, 2017

cristina-david commented May 31, 2017

smowton left a comment

sara-db commented Jun 22, 2017

cristina-david commented Jun 29, 2017

Feature/new instrumentation runtime exceptions #912

Feature/new instrumentation runtime exceptions #912

Conversation

cristina-david commented May 12, 2017

thk123 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cristina-david May 30, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

cristina-david commented May 31, 2017

cristina-david commented May 31, 2017

smowton left a comment

Choose a reason for hiding this comment

sara-db commented Jun 22, 2017

cristina-david commented Jun 29, 2017

cristina-david May 30, 2017 •

edited

Loading