Fix bugs in String.indexOf(c) TG-1846 #1668

romainbrenguier · 2017-12-14T07:27:49Z

This adds a test that checks with a loop that the result of indexOf found by CBMC is compatible with the Java specification. It is marked as Thorough as it is a bit long to run (about 20s).
This corrects a bug with the lower bound of the constraints that was discovered with this test and a problem with empty array not being concretized which was causing a crash in bv_refinement.

tautschnig

How does this one relate to #1634?

tautschnig · 2017-12-14T09:15:46Z

regression/jbmc-strings/StringIndexOf/Test.java

+    assert(i == -1);
+    i = "hello".indexOf('x', 0);
+    assert(i == -1);
+    i = "hello".indexOf('h', -1000);


Would the test complete more quickly if you were to use a slightly shorter string?

actually this test is relatively quick (0.4s on my computer), it is the other one, in the previous function that is slow.

Ah, sorry, will comment on the other one then - I should have noticed...

romainbrenguier · 2017-12-14T10:10:04Z

@tautschnig

How does this one relate to #1634?

This removes the need for PR1634, as now we should not provide any arrays to the function changed in that PR

tautschnig · 2017-12-14T12:59:31Z

regression/jbmc-strings/StringIndexOf/test.desc

@@ -0,0 +1,7 @@
+THOROUGH
+Test.class
+--refine-strings --function Test.check --unwind 10 --string-max-length 10 --java-assume-inputs-non-null


So how about reducing the limits to, e.g., 3? Would that make the test complete more quickly?

I try with 3 and 4 and it finishes with 1 second but with 5 it takes a long time. Then checking only 3 characters seems a bit limited. The reason I wrote this tests was to make sure the constraints I wrote for indexOf were correct, (they weren't at that point), now that we know that the constraints are correct, there won't be any bug specific to indexOf as long as we don't change them. So I think we don't have to run this test on CI, but it is still nice to have it available.

How about you include a quick version with 3 or 4 marked as CORE, and this one (THOROUGH) in addition?

allredj · 2017-12-14T14:47:35Z

src/solvers/refinement/string_refinement.cpp

-    // Empty arrays do not need to be substituted.
+    const typet &char_type = index_expr.array().type().subtype();
+
+    // Access to an empty array is undefined (non determinstic result)


allredj · 2017-12-14T14:51:13Z

regression/jbmc-strings/StringIndexOf/Test.java

+      assert input_String.charAt(i) == input_char;
+
+      for(int j = lower_bound; j < i; j++)
+        assert(input_String.charAt(j) != input_char);


Nit: Keep homogeneous syntax for assertions within the same file.

allredj · 2017-12-14T15:07:57Z

regression/jbmc-strings/StringIndexOf/Test.java

+    }
+    else
+    {
+      assert i >= input_int;


Shouldn't this be assert i >= lower_bound?

allredj · 2017-12-14T15:12:22Z

src/solvers/refinement/string_refinement.cpp

@@ -1078,10 +1078,13 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length)
 ///    `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34`
 /// \param expr: an expression containing array accesses
 /// \return an expression containing no array access
-static void substitute_array_access(exprt &expr)
+static void substitute_array_access(


Update function documentation

allredj · 2017-12-14T15:13:34Z

src/solvers/refinement/string_refinement.cpp

    if(array_expr.operands().empty())
+    {
+      expr = symbol_generator("out_of_bound_access", char_type);


Is the type important here? Why is it char_type?

yes, this is an access in an array of characters so we are expecting the result to be of the type of the elements of the array

We make the result non-deterministic by introducing a new symbol

In substitute_array_access, we generate an unbound symbol for each access in an empty array.

One of these is exhaustive and too slow to run so it is marked as THOROUGH and should be run every time axioms for the indexOf methods are touched.

allredj

LGTM

martin-cs

Looks OK apart from the comments. I haven't been following the string solver closely enough to say for sure it is correct but it looks like the kind of thing that would be a bug fix.

martin-cs · 2017-12-15T22:26:35Z

src/solvers/refinement/string_refinement.cpp

+  const auto gen_symbol = [&](const irep_idt &id, const typet &type)
+  {
+    return generator.fresh_symbol(id, type);
+  };


Why have the function as a parameter; why not just call generator.fresh_symbol? Fresh symbol functions feel kind of stateful to me so I think I'd prefer them to be member functions.

Also, can we change the description of the PR as this looks like a refactoring rather than a bug fix.

@martin-cs @romainbrenguier is on holiday now so I'm taking over his open PRs. About fresh_symbol, it seems @romainbrenguier already adressed your comment. About the name of the PR, the main goal was to fix some bugs. The refactoring is just a side-effect of that and the commits messages are explicit enough. Do you agree?

peterschrammel · 2017-12-19T09:20:29Z

src/solvers/refinement/string_refinement.cpp

-    // Empty arrays do not need to be substituted.
+    const typet &char_type = index_expr.array().type().subtype();
+
+    // Access to an empty array is undefined (non deterministic result)


Why? Where do you recognise that this should throw an exception in java?

@peterschrammel The exception is (intended) to be thrown at the model level. That's now the contract of the string methods in jbmc. I'm not sure whether this is sufficiently clearly stated, though.

67ec6f2 Merge remote-tracking branch 'upstream/develop' into pull-support-20180104 fabc99e Merge pull request diffblue#1563 from NathanJPhillips/feature/lazy-loading 2d67e42 Merge pull request diffblue#1692 from NathanJPhillips/feature/numbering-at 5266ba2 Merge commit 'ac4756fc3bb0e853f04de2b69f300d65cfbfc553' into pull-support-20171212 4f4a9c7 Add at method to template_numberingt d9cc0c0 Merge pull request diffblue#1685 from peterschrammel/remove-existing-coverage-goals f13c871 Update a comment in instrument_cover_goals 6c39443 Remove existing coverage goals a2cf16d Store symbol type instead of followed type when clean casting f96efb4 Change template parameter name to not clash with existing type b0cd57b Encapsulate lazy_goto_modelt::goto_functions ef02f4d Update test to handle changed symbol creation order 441d269 Reset counter used by get_fresh_aux_symbol in unit tests f759f25 Fix new test to run remove_java_new pass cb09d8e Fix new tests to use lazy loading 166563f Do lowering of java_new as a function-level pass 3779782 Always convert the main function from bytecode into the symbol_table 7e52e22 Always allow the main function not to have a body c938b08 Encapsulate maps in language_filest 87c6b28 Don't erase symbol in java_bytecode_convert_methodt::convert e3e44c8 Do type-checking as a function pass 2ba1364 Update load_all_functions 5f06e36 Recreate initialize in final aa5440b Moved call to final to lazy_goto_modelt::finalize a659bc0 Add lazy_goto_functions_mapt 7e1ecc9 Allow post-processing functions to run on a function-by-function basis 0c05be6 Allow convert_lazy_method on functions that don't have a lazy body 05a8da2 Make goto_convert_functions not add directly to function map c078858 Introduce lazy_goto_modelt a22dd1c Merge pull request diffblue#1671 from thk123/bugfix/TG-1278/correct-access-level 5b6eb00 Merge pull request diffblue#1668 from romainbrenguier/bugfix/string-index-of#TG-1846 9062853 Tidied up the generic specalised class copying the base class visibility f934ca3 String classes should be public 7b06a00 Merge pull request diffblue#1498 from smowton/smowton/feature/call_graph_improvements f3b4c9b Test for verification of the indexOf method 9a7fa2d Correct lower bound in String indexOf 682cd1a Use a symbol generator to avoid name clashes 28a2ada Access in empty array should be unconstrained d41403f Merge pull request diffblue#1665 from romainbrenguier/bugfix/string-out-of-bound#TG-1808 ac7e649 Use CProverString function in jbmc tests 22dc353 Add CProverString class for jbmc-strings tests ef610b3 Use CProverString functions in strings-smoke-tests 5c716c1 Add a CProverString class for string-smoke-tests 6b619e0 Deactivate preprocessing of charAt and substring bcfaaa4 Merge pull request diffblue#1664 from svorenova/refactoring_tg1190 c2a8bae Refactoring in specialization of generic classes 7a98e15 Rename call graph constructors 6228ed3 Slice global inits: use improved call graph d136bbc Expose limited call graph via goto-instrument 9c29bee Improve call graph unit tests 8ed3ccb Add documentation to call graph 8f6f429 Add call graph helpers 3b06a16 Call graph: add constructors that only include reachable functions 9b65862 grapht: add get_reachable function aaa8513 Call graph -> grapht transformation 8115248 Call graph: optionally record callsites git-subtree-dir: cbmc git-subtree-split: 67ec6f2

romainbrenguier requested review from martin-cs and peterschrammel as code owners December 14, 2017 07:27

romainbrenguier requested a review from allredj December 14, 2017 07:27

tautschnig reviewed Dec 14, 2017

View reviewed changes

romainbrenguier mentioned this pull request Dec 14, 2017

Prevent empty arrays from being passed to the solver #1634

Closed

romainbrenguier force-pushed the bugfix/string-index-of#TG-1846 branch 2 times, most recently from 8b56b29 to 039c420 Compare December 14, 2017 12:55

tautschnig reviewed Dec 14, 2017

View reviewed changes

allredj reviewed Dec 14, 2017

View reviewed changes

romainbrenguier added 3 commits December 14, 2017 15:58

Access in empty array should be unconstrained

28a2ada

We make the result non-deterministic by introducing a new symbol

Use a symbol generator to avoid name clashes

682cd1a

In substitute_array_access, we generate an unbound symbol for each access in an empty array.

Correct lower bound in String indexOf

9a7fa2d

romainbrenguier force-pushed the bugfix/string-index-of#TG-1846 branch 3 times, most recently from 140ae57 to b93fe24 Compare December 14, 2017 17:30

romainbrenguier requested a review from allredj December 15, 2017 07:34

Test for verification of the indexOf method

f3b4c9b

One of these is exhaustive and too slow to run so it is marked as THOROUGH and should be run every time axioms for the indexOf methods are touched.

romainbrenguier force-pushed the bugfix/string-index-of#TG-1846 branch from b93fe24 to f3b4c9b Compare December 15, 2017 07:36

allredj approved these changes Dec 15, 2017

View reviewed changes

martin-cs reviewed Dec 15, 2017

View reviewed changes

peterschrammel reviewed Dec 19, 2017

View reviewed changes

allredj self-assigned this Dec 19, 2017

peterschrammel approved these changes Dec 19, 2017

View reviewed changes

allredj merged commit 5b6eb00 into diffblue:develop Dec 20, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix bugs in String.indexOf(c) TG-1846 #1668

Fix bugs in String.indexOf(c) TG-1846 #1668

romainbrenguier commented Dec 14, 2017

tautschnig left a comment

tautschnig Dec 14, 2017

romainbrenguier Dec 14, 2017

tautschnig Dec 14, 2017

romainbrenguier commented Dec 14, 2017

tautschnig Dec 14, 2017

romainbrenguier Dec 14, 2017

tautschnig Dec 14, 2017 •

edited

Loading

allredj Dec 14, 2017

allredj Dec 14, 2017

allredj Dec 14, 2017

allredj Dec 14, 2017

allredj Dec 14, 2017

romainbrenguier Dec 14, 2017

allredj left a comment

martin-cs left a comment

martin-cs Dec 15, 2017

martin-cs Dec 15, 2017

allredj Dec 18, 2017

peterschrammel Dec 19, 2017

allredj Dec 19, 2017

Fix bugs in String.indexOf(c) TG-1846 #1668

Fix bugs in String.indexOf(c) TG-1846 #1668

Conversation

romainbrenguier commented Dec 14, 2017

tautschnig 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

romainbrenguier commented Dec 14, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig Dec 14, 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

allredj left a comment

Choose a reason for hiding this comment

martin-cs 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

tautschnig Dec 14, 2017 •

edited

Loading