Merge pull request #1001 from allredj/pr/add-axioms-for-concat-substr

Add add_axioms_for_concat_substr

Author: allredj

regression/strings-smoke-tests/java_replace/test.desc

@@ -6,3 +6,5 @@ test_replace.class
 ^VERIFICATION SUCCESSFUL$
 --
 diffblue/test-gen#256
+This test is only effective with a model of
+java.lang.String.replace(LCharSequence; LCharSequence).

src/solvers/refinement/string_constraint_generator.h

@@ -145,6 +145,11 @@ class string_constraint_generatort
   string_exprt add_axioms_for_copy(const function_application_exprt &f);
   string_exprt add_axioms_for_concat(
     const string_exprt &s1, const string_exprt &s2);
+  string_exprt add_axioms_for_concat_substr(
+    const string_exprt &s1,
+    const string_exprt &s2,
+    const exprt &start_index,
+    const exprt &end_index);
   string_exprt add_axioms_for_concat(const function_application_exprt &f);
   string_exprt add_axioms_for_concat_int(const function_application_exprt &f);
   string_exprt add_axioms_for_concat_long(const function_application_exprt &f);

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -13,60 +13,98 @@ Author: Romain Brenguier, [email protected]
 
 #include <solvers/refinement/string_constraint_generator.h>
 
-/// add axioms to say that the returned string expression is equal to the
-/// concatenation of the two string expressions given as input
-/// \par parameters: two string expressions
+/// Add axioms to say that the returned string expression is equal to the
+/// concatenation of s1 with the substring of s2 starting at index start_index
+/// and ending at index end_index.
+///
+/// If start_index >= end_index, the value returned is s1.
+/// If end_index > |s2| and/or start_index < 0, the appended string will be of
+/// length end_index - start_index and padded with non-deterministic values.
+///
+/// \param s1: string expression
+/// \param s2: string expression
+/// \param start_index: expression representing an integer
+/// \param end_index: expression representing an integer
 /// \return a new string expression
-string_exprt string_constraint_generatort::add_axioms_for_concat(
-  const string_exprt &s1, const string_exprt &s2)
+string_exprt string_constraint_generatort::add_axioms_for_concat_substr(
+  const string_exprt &s1,
+  const string_exprt &s2,
+  const exprt &start_index,
+  const exprt &end_index)
 {
   const refined_string_typet &ref_type=to_refined_string_type(s1.type());
   string_exprt res=fresh_string(ref_type);
 
   // We add axioms:
-  // a1 : |res|=|s1|+|s2|
-  // a2 : |s1| <= |res| (to avoid overflow with very long strings)
-  // a3 : |s2| <= |res| (to avoid overflow with very long strings)
-  // a4 : forall i<|s1|. res[i]=s1[i]
-  // a5 : forall i<|s2|. res[i+|s1|]=s2[i]
-
-  equal_exprt a1(
-    res.length(), plus_exprt_with_overflow_check(s1.length(), s2.length()));
+  // a1 : end_index > start_index => |res|=|s1|+ end_index - start_index
+  // a2 : end_index <= start_index => res = s1
+  // a3 : forall i<|s1|. res[i]=s1[i]
+  // a4 : forall i< end_index - start_index. res[i+|s1|]=s2[start_index+i]
+
+  binary_relation_exprt prem(end_index, ID_gt, start_index);
+
+  exprt res_length=plus_exprt_with_overflow_check(
+    s1.length(), minus_exprt(end_index, start_index));
+  implies_exprt a1(prem, equal_exprt(res.length(), res_length));
   axioms.push_back(a1);
-  axioms.push_back(s1.axiom_for_is_shorter_than(res));
-  axioms.push_back(s2.axiom_for_is_shorter_than(res));
+
+  implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length()));
+  axioms.push_back(a2);
 
   symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type());
-  string_constraintt a4(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  axioms.push_back(a4);
+  string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
+  axioms.push_back(a3);
 
   symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type());
-  equal_exprt res_eq(s2[idx2], res[plus_exprt(idx2, s1.length())]);
-  string_constraintt a5(idx2, s2.length(), res_eq);
-  axioms.push_back(a5);
+  equal_exprt res_eq(
+    res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start_index, idx2)]);
+  string_constraintt a4(idx2, minus_exprt(end_index, start_index), res_eq);
+  axioms.push_back(a4);
 
   return res;
 }
 
-/// add axioms to say that the returned string expression is equal to the
-/// concatenation of the two string arguments of the function application
-/// \par parameters: function application with two arguments which are strings
+/// Add axioms to say that the returned string expression is equal to the
+/// concatenation of the two string expressions given as input.
+///
+/// \param s1: the string expression to append to
+/// \param s2: the string expression to append to the first one
+/// \return a new string expression
+string_exprt string_constraint_generatort::add_axioms_for_concat(
+  const string_exprt &s1, const string_exprt &s2)
+{
+  exprt index_zero=from_integer(0, s2.length().type());
+  return add_axioms_for_concat_substr(s1, s2, index_zero, s2.length());
+}
+
+/// Add axioms to say that the returned string expression is equal to the
+/// concatenation of the two string arguments of the function application.
+///
+/// In case 4 arguments instead of 2 are given the last two arguments are
+/// intepreted as a start index and last index from which we extract a substring
+/// of the second argument: this is similar to the Java
+/// StringBuilder.append(CharSequence s, int start, int end) method.
+///
+/// \param f: function application with two arguments which are strings
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat(
   const function_application_exprt &f)
 {
   const function_application_exprt::argumentst &args=f.arguments();
-  assert(args.size()==2);
-
+  PRECONDITION(args.size()>=2);
   string_exprt s1=get_string_expr(args[0]);
   string_exprt s2=get_string_expr(args[1]);
-
+  if(args.size()!=2)
+  {
+    PRECONDITION(args.size()==4);
+    return add_axioms_for_concat_substr(s1, s2, args[2], args[3]);
+  }
   return add_axioms_for_concat(s1, s2);
 }
 
-/// add axioms corresponding to the StringBuilder.append(I) java function
-/// \par parameters: function application with two arguments: a string and an
-///   integer
+/// Add axioms corresponding to the StringBuilder.append(I) java function
+/// \param f: function application with two arguments: a string and an
+///           integer
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat_int(
   const function_application_exprt &f)
@@ -79,8 +117,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_int(
 }
 
 /// Add axioms corresponding to the StringBuilder.append(J) java function
-/// \par parameters: function application with two arguments: a string and a
-/// integer of type long
+/// \param f: function application with two arguments: a string and an
+///           integer of type long
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat_long(
   const function_application_exprt &f)
@@ -91,8 +129,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_long(
   return add_axioms_for_concat(s1, s2);
 }
 
-/// add axioms corresponding to the StringBuilder.append(Z) java function
-/// \par parameters: function application two arguments: a string and a bool
+/// Add axioms corresponding to the StringBuilder.append(Z) java function
+/// \param f: function application two arguments: a string and a bool
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat_bool(
   const function_application_exprt &f)
@@ -103,9 +141,8 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_bool(
   return add_axioms_for_concat(s1, s2);
 }
 
-/// add axioms corresponding to the StringBuilder.append(C) java function
-/// \par parameters: function application with two arguments: a string and a
-///   char
+/// Add axioms corresponding to the StringBuilder.append(C) java function
+/// \param f: function application with two arguments: a string and a char
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat_char(
   const function_application_exprt &f)
@@ -116,37 +153,34 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_char(
   return add_axioms_for_concat(s1, s2);
 }
 
-/// add axioms corresponding to the StringBuilder.append(D) java function
-/// \par parameters: function application with two arguments: a string and a
-///   double
+/// Add axioms corresponding to the StringBuilder.append(D) java function
+/// \param f: function application with two arguments: a string and a double
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat_double(
   const function_application_exprt &f)
 {
   string_exprt s1=get_string_expr(args(f, 2)[0]);
-  assert(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
   string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, true);
   return add_axioms_for_concat(s1, s2);
 }
 
-/// add axioms corresponding to the StringBuilder.append(F) java function
-/// \par parameters: function application with two arguments: a string and a
-///   float
+/// Add axioms corresponding to the StringBuilder.append(F) java function
+/// \param f: function application with two arguments: a string and a float
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat_float(
   const function_application_exprt &f)
 {
   string_exprt s1=get_string_expr(args(f, 2)[0]);
-  assert(refined_string_typet::is_refined_string_type(f.type()));
+  PRECONDITION(refined_string_typet::is_refined_string_type(f.type()));
   refined_string_typet ref_type=to_refined_string_type(f.type());
   string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, false);
   return add_axioms_for_concat(s1, s2);
 }
 
 /// Add axioms corresponding to the StringBuilder.appendCodePoint(I) function
-/// \par parameters: function application with two arguments: a string and a
-///   code point
+/// \param f: function application with two arguments: a string and a code point
 /// \return a new string expression
 string_exprt string_constraint_generatort::add_axioms_for_concat_code_point(
   const function_application_exprt &f)