[TG-1121] Bugfix for multi-dimensional arrays with non-const size and non-const access #2173

majakusber · 2018-05-09T13:52:15Z

This resolves the bug when cannot unpack array of non-const size crash occurred for multi-dimensional arrays with non-const size and non-const array access. The problem was that during symex the array access was attempted using byte_extract instruction because the subtype of the multi-dimensional array got lost during dereferencing.

The solution allows any pointer to be dereferenced to void pointer (during symex).

thk123 · 2018-05-09T14:16:13Z

src/pointer-analysis/value_set_dereference.cpp

+    return true; // always ok (anything can be dereferenced to void type)
+
+  if(
+    object_type.id() == ID_pointer && dereference_type.id() == ID_pointer &&


The first if handles void*, this one handles void** - what about void***? (not possible I assume in Java but perhaps in C?)

Is it necessary to restrict this to a matching number of ID_pointer levels? So int** vs. void** is ok, but int* vs. void** isn't?

Good points. I took a shot at it in the next commit, let me know what you think.

thk123

LGTM - would obviously be best to have a test to explores this void*** and mismatched depth scenarios, presumably in C, do either of @peterschrammel or @tautschnig have any suggestions of the kind of code that might exhibit this?

thk123 · 2018-05-09T15:55:45Z

src/pointer-analysis/value_set_dereference.cpp

+  if(
+    dereference_unwrapped.id() == ID_empty &&
+    object_unwrapped.id() != ID_pointer)
+    return true;


Nit: since the condition of the if is multi line I suggest wrapping this return true in braces to make it clearer.

tautschnig · 2018-05-09T18:34:34Z

src/pointer-analysis/value_set_dereference.cpp

+  // - object_type=(int **), dereference_type=(void **) is ok;
+  // - object_type=(int *), dereference_type=(void **) is not ok;
+  typet object_unwrapped = object_type;
+  typet dereference_unwrapped = dereference_type;


I would have used pointers here, but I won't insist. There are a couple of places in the codebase that dig through array or pointer types, and those tend to use pointers to avoid repeated construction of a non-trivial object.

I tend to insist that pointers should be used here.

tautschnig · 2018-05-09T18:39:15Z

would obviously be best to have a test to explores this void*** and mismatched depth scenarios, presumably in C, do either of @peterschrammel or @tautschnig have any suggestions of the kind of code that might exhibit this?

I think that something like int a[1][1]; int **a_ptr = a; void *v_ptr = a_ptr; int x = (int *)v_ptr; might trigger this? Testing and debugging would be really appreciated, if feasible! I believe that in many cases the effect of this PR will only be noticed through improved performance, and thus might go completely unnoticed.

peterschrammel · 2018-05-09T18:47:09Z

src/pointer-analysis/value_set_dereference.cpp

+  // - object_type=(int **), dereference_type=(void **) is ok;
+  // - object_type=(int *), dereference_type=(void **) is not ok;
+  typet object_unwrapped = object_type;
+  typet dereference_unwrapped = dereference_type;


I tend to insist that pointers should be used here.

peterschrammel · 2018-05-09T18:48:38Z

src/pointer-analysis/value_set_dereference.cpp

  if(
-    object_type.id() == ID_pointer && dereference_type.id() == ID_pointer &&


Please squash this commit with the first one.

peterschrammel · 2018-05-09T18:56:51Z

I believe that in many cases the effect of this PR will only be noticed through improved performance, and thus might go completely unnoticed.

The problem that triggered this bugfix are arrays of polymorphic types in java, where goto-symex failed to narrow to the actual type when indexing an array of void pointers, introducing byte extract expressions that cannot be flattened.

majakusber · 2018-05-14T10:08:38Z

I updated to code according to reviews, added additional case to the type comparison and some debug information.

For testing this - we have several regression tests that demonstrate that things now work as expected for arrays (see the commits). I was trying to add an example that would go wrong, but didn't succeed. The example suggested by @tautschnig does not trigger this. It only gives a warning during goto-program initialisation during typecheck, the warning being incompatible pointer types. Since the dereference_type_compare function is private, it's not possible to write isolated unit tests for it without changing the class itself and for the public function that calls it it's also too complex.

Let me know if you would agree with merging this with successful tests only or if you think a failing example is needed too.

tautschnig · 2018-05-14T10:21:22Z

src/pointer-analysis/value_set_dereference.cpp

+    dereference_unwrapped = &dereference_unwrapped->subtype();
+  }
+  if(
+    dereference_unwrapped->id() == ID_empty)


Nit pick: this line breaking seems unnecessary now.

tautschnig · 2018-05-14T10:23:54Z

src/pointer-analysis/value_set_dereference.cpp

+                    << messaget::endl;
+    message.debug() << " dereference_type: " << dereference_type.pretty()
+                    << messaget::eom;
+  }


I don't think this debug output should stay in, because it newly introduces a message handler that might not match the front-end's one.

Actually the entire commit "Adding debug information to dereference type comparison" should be dropped, I believe.

I was unsure whether this 'forced' debug is a good idea actually. The thing is that it took us a long time to find the problem in symex so for future cases this output could save us time. But I agree it's not ideal.

"forced debug" is better known as "warning" :-) So if you want to keep it in (and you have given good reasons for doing so), then please make sure there is a message handler in place so that proper output can be generated. If that's a bigger project than is feasible right now, you might just create a fresh PR with just this commit in it?

I meant forced in that I create a message handler especially for this :)

I'm not sure I understand; depending on who should be able to control this output it would either be guarded by #ifdef DEBUG or be passed a configured message handler.

I wanted to do it via a message handler (and changing the debug() above into warning()) but passing the message handler is a nightmare... so I did it as #ifdef DEBUG instead.

majakusber · 2018-05-15T10:08:16Z

There is a failing test on the test-gen PR, connected to enums. I added a 'do not merge' label while I investigate it.

thk123 · 2018-05-21T11:07:00Z

Rebased to see if subsequent fixes fix the bump for this to.

thk123

TG pointer bump passes.

779fa71 Merge pull request diffblue#2253 from peterschrammel/documentation/override2 40ecff8 Merge pull request diffblue#2250 from tautschnig/expr-iterator-deque 050b344 Re-enable enforcement of override without virtual b5dec9c Get legalistic about use of override without virtual b51e2a8 Merge pull request diffblue#2196 from peterschrammel/check-module-includes d5eabdf expr_iterator: use a std::deque to implement the stack fada0af Add module dependency definition files a90ea44 Add module dependency check to CPP-LINT 88f8cfc Remove unnecessary includes d6986d8 Fix relative include paths 0f9c202 Merge pull request diffblue#2242 from diffblue/section-name-warning b7f5886 Merge pull request diffblue#2241 from diffblue/ld_mode 5c11eb7 Merge pull request diffblue#2245 from mgudemann/fix/warning/clang_self_assign f7e5fb5 Merge pull request diffblue#2229 from diffblue/ssize_t 1a504c9 Merge pull request diffblue#2244 from diffblue/solver-Makefile-fix 4bb1bf0 Fix clang++'s warning about self-assign 9a0aa9c Merge pull request diffblue#2235 from thomasspriggs/test-pl-colour 4c2cb3a remove linker mode from gcc_mode 303908f add separate path for ld 524091f factor out creation of hybrid binaries b9127f3 linker_script_merget now takes exactly one ELF + goto binary cd967db update year + add Michael 0d95cc5 missing const method qualifiers 6f04d98 fix ordering problem in solvers/Makefile 8f6bae0 remove a warning about section names 8befd02 Merge pull request diffblue#2238 from owen-jones-diffblue/owen-jones-diffblue/doc/irep_id 34b0ac6 Merge pull request diffblue#2236 from diffblue/show-class-hierarchy 8e8e450 Merge pull request diffblue#2232 from owen-jones-diffblue/owen-jones-diffblue/generic-bounded-types 01dc76b Add section on irep_idt and dstringt 2f4c6ad Add and unify --show-class-hierarchy command line option 56256f1 Minor typos in irept documentation 3cf4e3a Merge pull request diffblue#2178 from thomasspriggs/remove_java_bytecode_parse_treet_swap 1a7235d use __CPROVER_size_t and __CPROVER_ssize_t for __CPROVER_POINTER_OBJECT/OFFSET a018e2f Add JSON output for class hierarchy 68c45ed Improve class hierarchy output eeb732f Switch `push_back` to `emplace_back` when constructing `parse_trees`. f154840 Delete copy constructor of `class java_bytecode_parse_treet`. c5cbcec Fix instances where copying was being used instead of moving. 52a669f Remove `java_bytecode::swap` and return using `optionalt` instead. fabbd04 Give up parsing generic method signature with bound 77f8162 Colour code tests passing vs failing. e5e0897 Merge pull request diffblue#2126 from danpoe/refactor/sharing-map-small-nodes f55bd96 Merge pull request diffblue#2231 from smowton/smowton/fix/jbmc-tests af02973 Merge pull request diffblue#2202 from smowton/smowton/fix/java-lang-class-fields 42a78af JBMC tests: suffix logfiles when using symex-driven loading af2defd Removed obsolete sharing map unit test 1d7fbd3 Refactor sharing map nodes to reduce memory consumption 5235938 Restore testing of jbmc 8a59f6f Object factory: permit null pointers within java.lang.Class 8412eb0 Merge pull request diffblue#2228 from peterschrammel/move-remaining-java-tests 369577a Move remaining java tests to jbmc/regression/ bfe3d3d Merge pull request diffblue#2226 from tautschnig/inline-get-str-cont 2b00973 Merge pull request diffblue#2227 from tautschnig/fptr-removal 3f7685f Merge pull request diffblue#2223 from diffblue/fp-builtins 3b3dc71 Distinct names of return-value symbols 4f7fade Cleanup: use symbolt::symbol_expr 8372862 function-pointer removal: Set the mode of a return symbol 272cde0 Inline get_string_container 72a0379 test __builtin_isinf, __builtin_isinf_sign, __builtin_isnormal f156ef0 Merge pull request diffblue#2222 from tautschnig/attributes a69c603 add __builtin_isnormal 83aeddd added __builtin_isinf_sign 87d467e fix return types of various __builtin_is* functions 61af061 added typecast_exprt::conditional_cast e1b906a Support GCC's fallthrough attribute d6d0a49 C front-end: support alias attributes on variables 376beab Merge pull request diffblue#2218 from diffblue/builtin_fpclassify c3603e3 added a test for raw __builtin_fpclassify 52595bd add support for __builtin_fpclassify 50d1c79 Merge pull request diffblue#2214 from tautschnig/tg-only 3c59312 Remove unused substitute.{h,cpp} d3e131c Revert "Set memory limit utility" a4389fe Merge pull request diffblue#2210 from tautschnig/verbosity-cleanup c250880 Merge pull request diffblue#2211 from tautschnig/travis-osx-cleanup c8597a4 Merge pull request diffblue#2174 from romainbrenguier/bugfix/not_contains#TG-3150 b08ef94 Merge pull request diffblue#2216 from peterschrammel/update-codeowners 471ab0f Merge pull request diffblue#2207 from diffblue/remove-solvers-cvc 215cd69 Use enum entries instead of numeric values when comparing verbosity 6344b4f Warn if user-specified verbosity is out of range bf04bcb Use a single implementation of eval_verbosity b4731eb Do not redundantly set the message handler 42ec63a Clean up .gitignore 19200bf Update CODEOWNERS for /jbmc 0487376 Merge pull request diffblue#2173 from svorenova/gs_tg1121 6af2270 Update regression test that no longer throws an exception bc17328 Enable previously failing regression tests 146bb29 Adding debug information to dereference type comparison 7b9a20a Allow pointers to be dereferenced to void types 108129c Merge pull request diffblue#2118 from diffblue/remove-jbmc 11411e4 Travis/OSX follow-up cleanup: remove unnecessary environment variables 386faa8 Test for String.contains and very large strings 9e73699 Refactor negation of not contains constraints 29a8818 Build jbmc on CI f196e74 Update compilation instructions 1b7c84a Add JBMC README 03d6f5b Shorten goto-analyzer-taint-ansi-c tests to goto-analyzer-taint 8dc0d74 Remove obsolete jbmc-cover tests f36da08 Move Java regression tests b6742ca Move Java unit tests e247458 Add JANALYZER tool 4588753 Add JDIFF tool a20f2c1 Move java_bytecode, jbmc and miniz to jbmc/src 987106f Make unit test independent of java_bytecode d945452 Adapt cpplint header guard check 28907b2 remove (pre-SMT-LIB) CVC interface git-subtree-dir: cbmc git-subtree-split: 779fa71

majakusber requested review from chrisr-diffblue, martin-cs, peterschrammel and smowton as code owners May 9, 2018 13:52

thk123 reviewed May 9, 2018

View reviewed changes

majakusber force-pushed the gs_tg1121 branch from cfec504 to d7795f4 Compare May 9, 2018 15:52

thk123 reviewed May 9, 2018

View reviewed changes

tautschnig approved these changes May 9, 2018

View reviewed changes

peterschrammel reviewed May 9, 2018

View reviewed changes

majakusber force-pushed the gs_tg1121 branch from d7795f4 to adbf3d9 Compare May 14, 2018 09:43

tautschnig assigned smowton, peterschrammel, martin-cs and chrisr-diffblue May 14, 2018

peterschrammel approved these changes May 14, 2018

View reviewed changes

tautschnig reviewed May 14, 2018

View reviewed changes

peterschrammel assigned majakusber and unassigned peterschrammel May 14, 2018

tautschnig reviewed May 14, 2018

View reviewed changes

majakusber force-pushed the gs_tg1121 branch from adbf3d9 to ed6380a Compare May 14, 2018 12:39

thk123 added the do not merge label May 15, 2018

majakusber force-pushed the gs_tg1121 branch from ed6380a to c68e80f Compare May 16, 2018 14:00

thk123 force-pushed the gs_tg1121 branch from c68e80f to 452c7c1 Compare May 21, 2018 11:04

Allow pointers to be dereferenced to void types

7b9a20a

svorenova added 3 commits May 21, 2018 16:14

Adding debug information to dereference type comparison

146bb29

Enable previously failing regression tests

bc17328

Update regression test that no longer throws an exception

6af2270

thk123 force-pushed the gs_tg1121 branch from 452c7c1 to 6af2270 Compare May 21, 2018 15:14

thk123 removed the do not merge label May 21, 2018

thk123 approved these changes May 21, 2018

View reviewed changes

thk123 merged commit 0487376 into diffblue:develop May 21, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[TG-1121] Bugfix for multi-dimensional arrays with non-const size and non-const access #2173

[TG-1121] Bugfix for multi-dimensional arrays with non-const size and non-const access #2173

majakusber commented May 9, 2018

thk123 May 9, 2018

tautschnig May 9, 2018

majakusber May 9, 2018

thk123 left a comment

thk123 May 9, 2018

tautschnig May 9, 2018

peterschrammel May 9, 2018

tautschnig commented May 9, 2018

peterschrammel May 9, 2018

peterschrammel May 9, 2018

peterschrammel commented May 9, 2018

majakusber commented May 14, 2018 •

edited

Loading

tautschnig May 14, 2018

tautschnig May 14, 2018

tautschnig May 14, 2018

majakusber May 14, 2018

tautschnig May 14, 2018

majakusber May 14, 2018

tautschnig May 14, 2018

majakusber May 14, 2018

majakusber commented May 15, 2018

thk123 commented May 21, 2018

thk123 left a comment

		if(
		object_type.id() == ID_pointer && dereference_type.id() == ID_pointer &&

[TG-1121] Bugfix for multi-dimensional arrays with non-const size and non-const access #2173

[TG-1121] Bugfix for multi-dimensional arrays with non-const size and non-const access #2173

Conversation

majakusber commented May 9, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

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

tautschnig commented May 9, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented May 9, 2018

majakusber commented May 14, 2018 • 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

Choose a reason for hiding this comment

majakusber commented May 15, 2018

thk123 commented May 21, 2018

thk123 left a comment

Choose a reason for hiding this comment

majakusber commented May 14, 2018 •

edited

Loading