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

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;
+    }
+}

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$
+--

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$
+--

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$
+--

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)));

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_exprt(const irep_idt &, const typet &)>
+    &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<bool, std::vector<exprt>> 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<bool, std::vector<exprt>> 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<bool, std::vector<exprt>> 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(