Making lastIndexOf precise diffblue/test-gen#77

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -82,8 +82,8 @@ Function: string_constraint_generatort::add_axioms_for_index_of_string
 
  Purpose: add axioms stating that the returned value is an index greater than
           from_index such that str at that index starts with substring and is
-          the first occurence of substring in str, or -1 if str does not contain
-          substring.
+          the first occurence of substring in str after from_index,
+          or returned value is -1 if str does not contain substring.
 
 \*******************************************************************/
 
@@ -190,12 +190,17 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
 
 Function: string_constraint_generatort::add_axioms_for_last_index_of_string
 
-  Inputs: two string expressions and an integer expression
+  Inputs:
+    str - a string expression
+    substring - a string expression
+    from_index - an expression representing an index in strings
 
  Outputs: a integer expression
 
- Purpose: add axioms stating that the returned value is either -1 or less
-          than from_index and the string beggining there has prefix substring
+ Purpose: add axioms stating that the returned value is an index less than
+          from_index such that str at that index starts with substring and is
+          the last occurence of substring in str before from_index,
+          or the returned value is -1 if str does not contain substring.
 
 \*******************************************************************/
 
@@ -209,10 +214,16 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   symbol_exprt contains=fresh_boolean("contains_substring");
 
   // We add axioms:
-  // a1 : contains => |substring| >= length &&offset <= from_index
-  // a2 : !contains => offset=-1
-  // a3 : forall 0 <= witness<substring.length,
-  //        contains => str[witness+offset]=substring[witness]
+  // a1 : contains => |substring| >= length && offset <= from_index
+  // a2 : !contains <=> offset=-1
+  // a3 : forall n:[0, substring.length[,
+  //        contains => str[n+offset]=substring[n]
+  // a4 : forall n:[offset+1, min(from_index, |str| - |substring|)].
+  //        contains =>
+  //          (exists m:[0,|substring|[. str[m+n]!=substring[m]])
+  // a5:  forall n:[0, min(from_index, |str| - |substring|)].
+  //        !contains =>
+  //          (exists m:[0,|substring|[. str[m+n]!=substring[m])
 
   implies_exprt a1(
     contains,
@@ -222,7 +233,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
       binary_relation_exprt(offset, ID_le, from_index)));
   axioms.push_back(a1);
 
-  implies_exprt a2(
+  equal_exprt a2(
     not_exprt(contains),
     equal_exprt(offset, from_integer(-1, index_type)));
   axioms.push_back(a2);
@@ -232,6 +243,32 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   string_constraintt a3(qvar, substring.length(), contains, constr3);
   axioms.push_back(a3);
 
+  // end_index is min(from_index, |str| - |substring|)
+  minus_exprt length_diff(str.length(), substring.length());
+  if_exprt end_index(
+    binary_relation_exprt(from_index, ID_le, length_diff),
+    from_index,
+    length_diff);
+  string_not_contains_constraintt a4(
+    plus_exprt(offset, from_integer(1, index_type)),
+    from_index,
+    end_index,
+    from_integer(0, index_type),
+    substring.length(),
+    str,
+    substring);
+  axioms.push_back(a4);
+
+  string_not_contains_constraintt a5(
+    from_integer(0, index_type),
+    end_index,
+    not_exprt(contains),
+    from_integer(0, index_type),
+    substring.length(),
+    str,
+    substring);
+  axioms.push_back(a5);
+
   return offset;
 }