Fix add_axioms_for_concat_substr

What was happening for start and end index out of bound wasn't clear and
could lead to empty index set because the strings where sometimes
indexed at negative indices.
The behavior is now similar to substring: the actual start index is
`start_index' = max(0, start_index)` (where start_index is the argument value) and the
actual end index is `max(min(end_index, s2.length), start_index')`.

Author: romainbrenguier

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -14,22 +14,16 @@ Author: Romain Brenguier, [email protected]
 #include <solvers/refinement/string_constraint_generator.h>
 
 /// Add axioms enforcing that `res` is 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.
+/// the substring of `s2` starting at index `start_index'` and ending
+/// at index `end_index'`.
+/// Where start_index' is max(0, start_index) and end_index' is
+/// max(min(end_index, s2.length), start_index')
 ///
 /// These axioms are:
-///   1. \f$end\_index > start\_index \Rightarrow |res| = |s_1| + end\_index -
-///        start\_index
-///     \f$
-///   2. \f$end\_index \le start\_index \Rightarrow res = s_1 \f$
-///   3. \f$\forall i<|s_1|. res[i]=s_1[i] \f$
-///   4. \f$\forall i< end\_index - start\_index.\ res[i+|s_1|]
-///        = s_2[start\_index+i]\f$
+///   1. \f$|res| = |s_1| + end\_index' - start\_index' \f$
+///   2. \f$\forall i<|s_1|. res[i]=s_1[i] \f$
+///   3. \f$\forall i< end\_index' - start\_index'.\ res[i+|s_1|]
+///        = s_2[start\_index'+i]\f$
 ///
 /// \param res: an array of characters expression
 /// \param s1: an array of characters expression
@@ -44,28 +38,33 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   const exprt &start_index,
   const exprt &end_index)
 {
-  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));
-  lemmas.push_back(a1);
-
-  implies_exprt a2(not_exprt(prem), equal_exprt(res.length(), s1.length()));
-  lemmas.push_back(a2);
+  const typet &index_type = start_index.type();
+  const exprt start1 = maximum(start_index, from_integer(0, index_type));
+  const exprt end1 = maximum(minimum(end_index, s2.length()), start1);
+
+  // Axiom 1.
+  lemmas.push_back([&] { // NOLINT
+    const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
+    return equal_exprt(res.length(), res_length);
+  }());
+
+  // Axiom 2.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt idx =
+      fresh_univ_index("QA_index_concat", res.length().type());
+    return string_constraintt(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
+  }());
+
+  // Axiom 3.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt idx2 =
+      fresh_univ_index("QA_index_concat2", res.length().type());
+    const equal_exprt res_eq(
+      res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
+    return string_constraintt(idx2, minus_exprt(end1, start1), res_eq);
+  }());
 
-  symbol_exprt idx=fresh_univ_index("QA_index_concat", res.length().type());
-  string_constraintt a3(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
-  constraints.push_back(a3);
-
-  symbol_exprt idx2=fresh_univ_index("QA_index_concat2", res.length().type());
-  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);
-  constraints.push_back(a4);
-
-  // We should have a enum type for the possible error codes
-  return from_integer(0, res.length().type());
+  return from_integer(0, get_return_code_type());
 }
 
 /// Add axioms enforcing that `res` is the concatenation of `s1` with