Add an add_axioms_for_concat_substr function

Implements the concatenation of a substring of the second argument.
This will make the encoding of StringBuilder.append(CharSequence s,
int start, int end) more efficient.

Part of test-gen/#256

Author: romainbrenguier

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

@@ -14,53 +14,85 @@ 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
+/// 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
+/// concatenation of the two string expressions given as input
+/// \par parameters: two string expressions
+/// \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
+/// StringBuiledr.append(CharSequence s, int start, int end) method.
 /// \par parameters: 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);
-
+  assert(args.size()>=2);
   string_exprt s1=get_string_expr(args[0]);
   string_exprt s2=get_string_expr(args[1]);
-
+  if(args.size()!=2)
+  {
+    assert(args.size()==4);
+    return add_axioms_for_concat_substr(s1, s2, args[2], args[3]);
+  }
   return add_axioms_for_concat(s1, s2);
 }