Fix handling of null array in string refinement [TG-3726] #2351
Conversation
romainbrenguier
requested review from
martin-cs and
peterschrammel
as code owners
| symbol_exprt array_sym = fresh_symbol("char_array_null", array_type); | ||
| return to_array_string_expr(array_sym); | ||
| } | ||
| symbol_name = "char_array_null"; |
There was a problem hiding this comment.
So does to_array_string_expr reuse the same symbol when given an already-existing name?
There was a problem hiding this comment.
to_array_string_expr is just a cast, fresh_symbol always create a new symbol, but if the expression is already in the map we return that value.
|
Could a regression (or unit) test please be added? This sounds like a bug fix, but then we should make sure there is no regression at some later point in time. |
romainbrenguier
force-pushed
the
bugfix/null-array
branch
from
9142f5e to
38b407d
Compare
The bug I have seen is a bit difficult to reproduce, so I'm adding unit tests for array_poolt, I think that's more useful. |
You will know best what's right here! I just operate under the simple assumption that anything that says "fix" or "bugfix" should come with a test to justify it, and I'm more than happy when that can be fulfilled in some way. |
romainbrenguier
force-pushed
the
bugfix/null-array
branch
from
38b407d to
500d16d
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 500d16d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76499199
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).
make_char_array was returning a new symbol every time NULL was encountered which is a problem when we want to compare these symbols.
The previous version was making make_char_array_for_char_pointer look more complicated than it actually is, this version should be much clearer.
romainbrenguier
force-pushed
the
bugfix/null-array
branch
from
500d16d to
349472f
Compare
There was a problem hiding this comment.
Passed Diffblue compatibility checks (cbmc commit: 349472f).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76518719
|
|
||
| WHEN("Looking for two pointer symbols") | ||
| { | ||
|
|
romainbrenguier
force-pushed
the
bugfix/null-array
branch
from
349472f to
b2089b7
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: b2089b7).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/76532224
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).
|
compatibility check failed with |
e6d196d Merge pull request diffblue#2355 from owen-jones-diffblue/owen-jones-diffblue/add-name-to-array-type 6f7580d Merge pull request diffblue#2351 from romainbrenguier/bugfix/null-array b2089b7 Add unit test for array_poolt 2df6d81 Set name of java array types 50e02b0 Simplify make_char_array_for_char_pointer 645eda9 Improve invariant message 3c7a671 Look up for null pointer in array pool 32a4186 Merge pull request diffblue#2302 from romainbrenguier/refactor/ci-lazy-methods c4aadab Extract handle_virtual_methods_with_no_callees cac016d Extract a convert_and_analyze_method method ca0adc9 Correct indentation 24b6936 Extract entry_point_methods method 360fabe Merge pull request diffblue#2356 from peterschrammel/fix-goto-simplification 4394016 Temporary fix to enable if-then-else simplifications d433438 Test for if-then-else optimisation in goto convert e5d1c12 Merge pull request diffblue#2354 from Degiorgio/disable-soundness-check-for-shared-pointers 7d4d4bd Skip check for unsoundness in shared pointer handling (java only) 8e6244c Merge pull request diffblue#2043 from peterschrammel/fail-on-uncaught-exception ec3010f Merge pull request diffblue#1994 from tautschnig/concurrency-soundness 1a9850a Merge pull request diffblue#2326 from tautschnig/c++-enum b71efaf Merge pull request diffblue#2019 from tautschnig/remove-unused 26b13ae Abort concurrency encoding in possibly unsound cases cd2ef4b Enable throwing of AssertionError 653d887 Remove wrong assumption from goto check 07acde4 Refactor user-defined assertion translation for Java 04c0205 Assert that there is uncaught exception 1daf466 Use resolver to translate cpp_name to scoped base_name 471b20f Remove prop_assignmentt interface 2639cf1 Remove unused solvers/prop/prop_conv_store.{h,cpp} 502687e Remove unused solver/prop/prop_wrapper.h ae56978 Remove unused goto-analyzer/static_analyzer.{h,cpp} 2260f82 Remove path_accelerationt interface d350e5c Remove unused nondet_ifthenelse.{h,cpp} a4936f8 Remove unused cpp/recursion_counter.h 71cfbbd Remove unused sorted_vector.h 4d4c9c6 Revert "added pipe_stream class" 2696420 Revert "new exception class" 3fb06ba Revert "Added utility class to convert strings into expressions" 55bdbc7 Recompile regression test class files 118f41f Merge pull request diffblue#2352 from tautschnig/c++-auto-tc 5a4dc8d Merge pull request diffblue#2315 from diffblue/fix-goto 199d4cc prevent half-constructed GOTO instructions 72156d5 C++ front-end: fix auto+references after already-typechecked cleanup 8fac5ed Merge pull request diffblue#2069 from romainbrenguier/refactor/convert_instruction 309d207 remove conversion for non-deterministic-goto 67081d5 Extract convert_pop function cd98a1f Extract convert_switch function f2acb00 Extract convert_dup2_x2 function 66cf709 Extract convert_dup2_x1 function e0735af Extract convert_dup2 function 51f53ca Extract convert_const function d627638 Extract convert_invoke function fcfca08 Extract replace_calls_to_cprover_assume function 0a521a4 Extract convert_checkcast function 4c28f99 Extract convert_athrow function 21e37a8 Extract convert_monitorexit function a7bbf53 Extract do_exception_handling function 0aa1c8e Extract convert_monitorenter function 48dd97f Extract convert_multianewarray function edc4a28 Extract convert_newarray function f8d00f6 Extract convert_new function b846798 Extract convert_putstatic function 27af4a2 Extract convert_putfield function f1edff9 Extract convert_getstatic function 68bddf1 Remove redundant assert 6f0f3fb Extract convert_cmp2 function 3049281 Extract convert_cmp function 5a5788c Extract convert_ushr function 305ede8 Extract convert_iinc function 61d03da Extract convert_ifnull function b4f6d04 Extract convert_if_nonull function 0e911d4 Extract convert_if function 651246e Extract convert_if_cmp function fc95df1 Extract convert_ret function ce58dca Extract convert_aload/store/astore functions 14e3c35 Extract convert_invokedynamic function 939bb53 Rename iterators and use auto ddb31a0 Extract draw_edges_from_ret_to_jsr function 390063f Extract try_catch_handler function 87a4f31 Make label static 36ed947 Replace assert by invariant 036f1b1 Use auto for iterator types git-subtree-dir: cbmc git-subtree-split: e6d196d
A new symbol was generated each time we were looking for null in the array pool, which made equality checking on the output wrong.