Java: make null-pointer and similar checks fatal #2191

smowton · 2018-05-17T08:32:49Z

These previously used code_assertt, which asserts but then continues -- this
changes them to use assert(condition); assume(condition), which ensures subsequent
code is not executed in conditions which are in practice impossible.

With --java-throw-runtime-exceptions this is irrelevant, as a real exception is raised
and the conditional GOTO guarding the throw has the same effect as the assume.

smowton · 2018-05-17T08:39:45Z

This will need a test-gen bump once test-gen#1794 is in.

tautschnig · 2018-05-17T09:01:23Z

src/java_bytecode/java_bytecode_instrument.cpp

+/// \param loc: original source location
+/// \param comment: human-readable assertion description
+/// \param property_class: assertion property class
+static source_locationt with_assertion_description(


Possibly useful, but please make this more generally available. On quick inspection almost every place that git grep -n set_comment highlights could benefit from this.

I don't think that makes the code more readable.

tautschnig · 2018-05-17T09:07:30Z

src/util/assert_or_die.h

+
+#include "std_code.h"
+
+codet create_assert_or_die(const exprt &condition, const source_locationt &loc);


I think expr_util or std_code are perfectly good places to put this, no need for a new file.

Be specific about the return type. There is no need to hide the fact that it returns a code_blockt.

I'm not sure I like the name. How about aborting_assert?

smowton · 2018-05-17T10:16:52Z

@tautschnig @peterschrammel changes applied, please re-review.

tautschnig · 2018-05-17T10:40:40Z

src/util/std_code.cpp

+  result.copy_to_operands(code_assertt(condition));
+  result.copy_to_operands(code_assumet(condition));
+  for(auto &op : result.operands())
+    op.add_source_location() = loc;


How about:

code_blockt result; result.add(code_assertt(condition), loc); result.add(code_assumet(condition), loc);

or (leaving the loop intact)

code_blockt result({code_assertt(condition), code_assumet(condition)});

martin-cs

Seems in line with the general state of affairs.

smowton · 2018-05-17T14:24:37Z

This has exposed some probably unrelated test failures. To investigate.

smowton · 2018-05-18T14:58:25Z

The problem was another fragile string solver test that required some luck to test; it was failing because the md5sum of the binary changed / moon wasn't aligned with Saturn, rather than due to the actual change introduced here.. I've hardened the test, hopefully now this will pass CI.

smowton · 2018-05-18T16:19:09Z

Bump: https://github.com/diffblue/test-gen/pull/1830

These previously used code_assertt, which asserts but then continues -- this changes them to use assert(condition); assume(condition), which ensures subsequent code is not executed in conditions which are in practice impossible. With --java-throw-runtime-exceptions this is irrelevant, as a real exception is raised and the conditional GOTO guarding the throw has the same effect as the assume.

This test previously checked that the *sum* of the arguments' sizes didn't exceed some critical bound, but this didn't exclude the case where one of them is just within bounds (but still long enough to cause a memout when we try to concretise it) and the other just long enough to push the sum over the boundary. Instead we'll check that one or the other is very long, and the other one acceptably short.

kroening · 2018-05-20T17:34:36Z

BTW, related to this, I would be strongly in favour of making --java-throw-runtime-exceptions the default for jbmc. The Java semantics is very clear on these, this isn't the same situation as in C.

There can be a --java-runtime-exceptions-block or the like.

smowton · 2018-05-20T20:49:24Z

@kroening as a prereq to --java-throw-runtime-exceptions we need to get a lot better at modelling control flow, otherwise a lot of implausible exceptional flows blur symex's certainty about the state of the world and the formula grows remarkably.

peterschrammel · 2018-05-21T08:25:01Z

@smowton, could using https://github.com/diffblue/cbmc/blob/develop/src/analyses/goto_check.cpp#L1478 improve the situation (at least for NPEs)?

31ef182 Merge pull request diffblue#2208 from diffblue/cleanout-goto-programs 0e84d3e Merge pull request diffblue#2195 from smowton/smowton/feature/smarter-reachability-slicer c801126 Merge pull request diffblue#2209 from diffblue/travis-no-osx-g++ 3487bf7 Reachability slicer: mark reachable code more precisely 85e8451 Merge pull request diffblue#2066 from tautschnig/bv-endianness 5e5eafb Merge pull request diffblue#2191 from smowton/smowton/feature/java-fatal-assertions 8a68ab8 remove g++ build on OS X; this is identical to the clang++ build 48e5b25 Amend faulty long-string test 3f718ba Java: make null-pointer and similar checks fatal 821eb1d remove basic_blocks and goto_program_irep d87c2db Merge pull request diffblue#2203 from diffblue/typed-lookup d77dea3 strongly type the lookup() methods in namespacet 2382f27 Merge pull request diffblue#2193 from martin-cs/feature/correct-instruction-documentation c314272 Merge pull request diffblue#2181 from diffblue/format-expr-constants 514a0a5 Merge pull request diffblue#2167 from diffblue/parse_unwindset_options 0102452 move escape(s) to string_utils f1b6174 use unwindsett in goto-instrument dcc907a introduce unwindsett for unwinding limits 10aeae8 format_expr now does index, c_bool constants, string constants 92b92d6 Correct the documentation of ASSERT : it does not alter control flow. a11add8 Expand the documentation of the goto-program instructions. a06503b Merge pull request diffblue#2197 from tautschnig/fix-help 05e4bc3 Remove stray whitespace previously demanded by clang-format 3261f4d Fix help output of --generate-function-body-options 7c67b23 Merge pull request diffblue#2110 from tautschnig/type-mismatch-exception 18fb262 Merge pull request diffblue#2025 from tautschnig/stack-depth-fix 9191b6a Merge pull request diffblue#2199 from tautschnig/simplifier-typing f99e631 Merge pull request diffblue#2198 from tautschnig/fix-test-desc 1a79a11 stack depth instrumentation: __CPROVER_initialize may be empty a7690ba Merge pull request diffblue#2185 from smowton/smowton/fix/tolerate-ts18661-types fc02e8f Restore returns before writing the simplified binary 49333eb Make restore_returns handle simplified programs 46f7987 Fix perl regular expressioons in regression test descriptions 9fe432b Merge pull request diffblue#1899 from danpoe/sharing-map-catch-unit-tests 9cc6aae Merge pull request diffblue#2081 from hannes-steffenhagen-diffblue/floating_point_simplificiation da19abe Tolerate TS 18661 (_Float32 et al) types a055454 Try all rounding modes when domain is unknown 5f7bc15 Add float support to constant propagator domain 3dc2244 Move adjust_float_expressions to goto-programs 06d8bea Merge pull request diffblue#2187 from diffblue/move-convert-nondet 6d8c3fa Merge pull request diffblue#2189 from thk123/bugfix/json-parser-restart 2ad157f Merge pull request diffblue#2186 from smowton/smowton/fix/call-graph-uninit-field cd54ad7 Corrected state persistence in the json parser 4447be0 Fix uninitialised collect_callsites field in call_grapht ead0aa3 Merge pull request diffblue#2188 from smowton/smowton/fix/init-string-types-without-refine-strings 57988fc Fix String type initialisation when --refine-strings is not active 6a76aff Move convert_nondet to java_bytecode ac6eb21 Merge pull request diffblue#1858 from danpoe/dependence-graph-fix 10b8b09 Merge pull request diffblue#2011 from thomasspriggs/final_classes a154593 Merge pull request diffblue#2087 from danpoe/feature/small-map 7002909 More dependence graph tests 66263ea Make dependence graph merge() return true when abstract state changes 3aa6dca Control dependency computation fix a408423 Simplified state merging in the dependence graph 0315816 Merge pull request diffblue#2180 from thomasspriggs/json_id2string 8941567 Merge pull request diffblue#2124 from smowton/smowton/feature/fallback-function-provider cd04e70 JBMC: use simple method stubbing pass a6b2cda Add Java simple method stubbing pass ec1127c Lazy goto model: hook for driver program to replace or stub functions b6a4382 Remove `id2string` from inside calls to the `json_stringt` constructor. b673ebb Add storage of final modifier status of java classes in `java_class_typet`. a2ad909 Small map 808dade Provide suitable diagnostics for equality-without-matching-types 89cf6fe Throw appropriate exceptions when converting constraints 2ae66c2 Produce a proper error message when catching a std::runtime_error at top level e7b3ade Workaround for Visual Studio loss of CV qualifier bug 1f661f5 Move sharing map and sharing node unit tests to util 47463a3 Use std::size_t instead of unsigned in the sharing map 3e22217 Sharing map documentation e54f740 Fix sharing map compiler warnings bcc489c Move sharing map unit tests to catch 34114b8 Use a specialised endianness map for flattening git-subtree-dir: cbmc git-subtree-split: 31ef182

smowton requested review from cesaro, chrisr-diffblue, kroening, martin-cs, mgudemann, peterschrammel, tautschnig and thk123 as code owners May 17, 2018 08:32

smowton mentioned this pull request May 17, 2018

More precise control-flow graph using the simplifier #2031

Closed

tautschnig reviewed May 17, 2018

View reviewed changes

smowton force-pushed the smowton/feature/java-fatal-assertions branch from 95a99fc to 730d9d4 Compare May 17, 2018 10:16

smowton force-pushed the smowton/feature/java-fatal-assertions branch from 730d9d4 to 4ece6fd Compare May 17, 2018 10:20

tautschnig approved these changes May 17, 2018

View reviewed changes

martin-cs approved these changes May 17, 2018

View reviewed changes

smowton force-pushed the smowton/feature/java-fatal-assertions branch from 4ece6fd to 598b3d7 Compare May 18, 2018 09:54

peterschrammel approved these changes May 18, 2018

View reviewed changes

smowton force-pushed the smowton/feature/java-fatal-assertions branch from 0285250 to c2fc85e Compare May 20, 2018 11:20

smowton added 2 commits May 20, 2018 17:13

smowton force-pushed the smowton/feature/java-fatal-assertions branch from c2fc85e to 48e5b25 Compare May 20, 2018 16:13

kroening approved these changes May 20, 2018

View reviewed changes

kroening added the Java Front End label May 20, 2018

smowton merged commit 5e5eafb into diffblue:develop May 20, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Java: make null-pointer and similar checks fatal #2191

Java: make null-pointer and similar checks fatal #2191

smowton commented May 17, 2018

smowton commented May 17, 2018

tautschnig May 17, 2018

peterschrammel May 17, 2018

tautschnig May 17, 2018

smowton commented May 17, 2018

tautschnig May 17, 2018

martin-cs left a comment

smowton commented May 17, 2018

smowton commented May 18, 2018

smowton commented May 18, 2018

kroening commented May 20, 2018

smowton commented May 20, 2018

peterschrammel commented May 21, 2018


		#include "std_code.h"

		codet create_assert_or_die(const exprt &condition, const source_locationt &loc);

Java: make null-pointer and similar checks fatal #2191

Java: make null-pointer and similar checks fatal #2191

Conversation

smowton commented May 17, 2018

smowton commented May 17, 2018

tautschnig May 17, 2018

Choose a reason for hiding this comment

peterschrammel May 17, 2018

Choose a reason for hiding this comment

tautschnig May 17, 2018

Choose a reason for hiding this comment

smowton commented May 17, 2018

tautschnig May 17, 2018

Choose a reason for hiding this comment

martin-cs left a comment

Choose a reason for hiding this comment

smowton commented May 17, 2018

smowton commented May 18, 2018

smowton commented May 18, 2018

kroening commented May 20, 2018

smowton commented May 20, 2018

peterschrammel commented May 21, 2018