diff --git a/regression/jbmc-strings/StringIndexOf/Test.class b/regression/jbmc-strings/StringIndexOf/Test.class new file mode 100644 index 00000000000..73660394203 Binary files /dev/null and b/regression/jbmc-strings/StringIndexOf/Test.class differ diff --git a/regression/jbmc-strings/StringIndexOf/Test.java b/regression/jbmc-strings/StringIndexOf/Test.java new file mode 100644 index 00000000000..6732eba723a --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/Test.java @@ -0,0 +1,46 @@ +public class Test { + + public boolean check(String input_String, char input_char, int input_int) { + // Verify indexOf is conform to its specification + int i = input_String.indexOf(input_char, input_int); + + assert i < input_String.length(); + + int lower_bound; + if (input_int < 0) + lower_bound = 0; + else + lower_bound = input_int; + + if (i == -1) { + for (int j = lower_bound; j < input_String.length(); j++) + assert input_String.charAt(j) != input_char; + } else { + assert i >= lower_bound; + assert input_String.charAt(i) == input_char; + + for (int j = lower_bound; j < i; j++) + assert input_String.charAt(j) != input_char; + } + return true; + } + + public boolean check2() { + // Verification should fail, this is to check the solver does + // not get a contradiction + int i = "hello".indexOf('o', 1); + assert i == 4; + i = "hello".indexOf('h', 1); + assert i == -1; + i = "hello".indexOf('e', 4); + assert i == -1; + i = "hello".indexOf('e', 8); + assert i == -1; + i = "hello".indexOf('x', 0); + assert i == -1; + i = "hello".indexOf('h', -1000); + assert i == 0; + assert false; + return true; + } +} diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc new file mode 100644 index 00000000000..9c17878eb94 --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/test.desc @@ -0,0 +1,7 @@ +CORE +Test.class +--refine-strings --function Test.check --unwind 4 --string-max-length 3 --java-assume-inputs-non-null +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/regression/jbmc-strings/StringIndexOf/test2.desc b/regression/jbmc-strings/StringIndexOf/test2.desc new file mode 100644 index 00000000000..6fdbcd101f0 --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/test2.desc @@ -0,0 +1,14 @@ +CORE +Test.class +--refine-strings --function Test.check2 --unwind 10 --string-max-length 10 --java-assume-inputs-non-null +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 32 .* SUCCESS +assertion at file Test.java line 34 .* SUCCESS +assertion at file Test.java line 36 .* SUCCESS +assertion at file Test.java line 38 .* SUCCESS +assertion at file Test.java line 40 .* SUCCESS +assertion at file Test.java line 42 .* SUCCESS +assertion at file Test.java line 43 .* FAILURE +^VERIFICATION FAILED$ +-- diff --git a/regression/jbmc-strings/StringIndexOf/test_thorough.desc b/regression/jbmc-strings/StringIndexOf/test_thorough.desc new file mode 100644 index 00000000000..8e05fa5bfa7 --- /dev/null +++ b/regression/jbmc-strings/StringIndexOf/test_thorough.desc @@ -0,0 +1,7 @@ +THOROUGH +Test.class +--refine-strings --function Test.check --unwind 10 --string-max-length 10 --java-assume-inputs-non-null +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 27f7e96bfb7..295c18df903 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -59,15 +59,19 @@ exprt string_constraint_generatort::add_axioms_for_index_of( equal_exprt(str[index], c))); axioms.push_back(a3); + const auto zero = from_integer(0, index_type); + const if_exprt lower_bound( + binary_relation_exprt(from_index, ID_le, zero), zero, from_index); + symbol_exprt n=fresh_univ_index("QA_index_of", index_type); string_constraintt a4( - n, from_index, index, contains, not_exprt(equal_exprt(str[n], c))); + n, lower_bound, index, contains, not_exprt(equal_exprt(str[n], c))); axioms.push_back(a4); symbol_exprt m=fresh_univ_index("QA_index_of", index_type); string_constraintt a5( m, - from_index, + lower_bound, str.length(), not_exprt(contains), not_exprt(equal_exprt(str[m], c))); diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 8ff90e94676..fec692c9bf9 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1076,12 +1076,19 @@ exprt fill_in_array_expr(const array_exprt &expr, std::size_t string_max_length) /// expression will be: `index==0 ? 24 : index==2 ? 42 : 12` /// * for an array access `(g1?arr1:arr2)[x]` where `arr1 := {12}` and /// `arr2 := {34}`, the constructed expression will be: `g1 ? 12 : 34` +/// * for an access in an empty array `{ }[x]` returns a fresh symbol, this +/// corresponds to a non-deterministic result /// \param expr: an expression containing array accesses +/// \param symbol_generator: function which given a prefix and a type generates +/// a fresh symbol of the given type /// \return an expression containing no array access -static void substitute_array_access(exprt &expr) +static void substitute_array_access( + exprt &expr, + const std::function + &symbol_generator) { for(auto &op : expr.operands()) - substitute_array_access(op); + substitute_array_access(op, symbol_generator); if(expr.id()==ID_index) { @@ -1110,9 +1117,9 @@ static void substitute_array_access(exprt &expr) // Substitute recursively in branches of conditional expressions if_exprt if_expr=to_if_expr(index_expr.array()); exprt true_case=index_exprt(if_expr.true_case(), index_expr.index()); - substitute_array_access(true_case); + substitute_array_access(true_case, symbol_generator); exprt false_case=index_exprt(if_expr.false_case(), index_expr.index()); - substitute_array_access(false_case); + substitute_array_access(false_case, symbol_generator); expr=if_exprt(if_expr.cond(), true_case, false_case); return; } @@ -1124,13 +1131,17 @@ static void substitute_array_access(exprt &expr) "above")); array_exprt &array_expr=to_array_expr(index_expr.array()); - // 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) if(array_expr.operands().empty()) + { + expr = symbol_generator("out_of_bound_access", char_type); return; + } size_t last_index=array_expr.operands().size()-1; - const typet &char_type=index_expr.array().type().subtype(); exprt ite=array_expr.operands().back(); if(ite.type()!=char_type) @@ -1342,6 +1353,12 @@ static std::pair> check_axioms( const auto eom=messaget::eom; static const std::string indent = " "; static const std::string indent2 = " "; + // clang-format off + const auto gen_symbol = [&](const irep_idt &id, const typet &type) + { + return generator.fresh_symbol(id, type); + }; + // clang-format on stream << "string_refinementt::check_axioms:" << eom; @@ -1383,7 +1400,8 @@ static std::pair> check_axioms( negaxiom = simplify_expr(negaxiom, ns); exprt with_concretized_arrays = concretize_arrays_in_expression(negaxiom, max_string_length, ns); - substitute_array_access(with_concretized_arrays); + + substitute_array_access(with_concretized_arrays, gen_symbol); stream << indent << i << ".\n"; debug_check_axioms_step( @@ -1439,7 +1457,7 @@ static std::pair> check_axioms( exprt with_concrete_arrays = concretize_arrays_in_expression(negaxiom, max_string_length, ns); - substitute_array_access(with_concrete_arrays); + substitute_array_access(with_concrete_arrays, gen_symbol); stream << indent << i << ".\n"; debug_check_axioms_step(