[TG-2721] Use sparse arrays in string_refinementt::get

regression/jbmc-strings/long_string/Test.java

@@ -0,0 +1,41 @@
+import org.cprover.CProverString;
+
+public class Test {
+    public static void check(String s, String t) {
+        // Filter
+        if(s == null || t == null)
+            return;
+
+        // Act
+        String u = s.concat(t);
+
+        // Filter out
+        if(u.length() < 3_000_000)
+            return;
+        if(CProverString.charAt(u, 500_000) != 'a')
+            return;
+        if(CProverString.charAt(u, 2_000_000) != 'b')
+            return;
+
+        // Assert
+        assert(false);
+    }
+
+    public static void checkAbort(String s, String t) {
+        // Filter
+        if(s == null || t == null)
+            return;
+
+        // Act
+        String u = s.concat(t);
+
+        // Filter out
+        if(u.length() < 67_108_864)
+            return;
+        if(CProverString.charAt(u, 2_000_000) != 'b')
+            return;
+
+        // Assert
+        assert(false);
+    }
+}

regression/jbmc-strings/long_string/test.desc

@@ -0,0 +1,11 @@
+CORE
+Test.class
+--refine-strings --function Test.check --string-max-input-length 2000000
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 21 .* FAILURE
+--
+--
+This checks that the solver manage to violate assertions even when this requires
+some very long strings, as long as they don't exceed the arbitrary limit that
+is set by the solver (64M characters).

regression/jbmc-strings/long_string/test_abort.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--refine-strings --function Test.checkAbort
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This tests should abort, because concretizing a string of the required
+length may take to much memory.

src/solvers/refinement/string_constraint_generator.h

@@ -177,8 +177,6 @@ class string_constraint_generatort final
   array_string_exprt
   fresh_string(const typet &index_type, const typet &char_type);
   array_string_exprt get_string_expr(const exprt &expr);
-  plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2);
-
 
   static constant_exprt constant_char(int i, const typet &char_type);
 
@@ -447,6 +445,9 @@ exprt minimum(const exprt &a, const exprt &b);
 /// \return expression representing the maximum of two expressions
 exprt maximum(const exprt &a, const exprt &b);
 
+/// \return Boolean true when the sum of the two expressions overflows
+exprt sum_overflows(const plus_exprt &sum);
+
 exprt length_constraint_for_concat_char(
   const array_string_exprt &res,
   const array_string_exprt &s1);

src/solvers/refinement/string_constraint_generator_code_points.cpp

@@ -128,12 +128,11 @@ exprt string_constraint_generatort::add_axioms_for_code_point_at(
   const symbol_exprt result = fresh_symbol("char", return_type);
   const exprt index1 = from_integer(1, str.length().type());
   const exprt &char1=str[pos];
-  const exprt &char2=str[plus_exprt_with_overflow_check(pos, index1)];
+  const exprt &char2 = str[plus_exprt(pos, index1)];
   const typecast_exprt char1_as_int(char1, return_type);
   const typecast_exprt char2_as_int(char2, return_type);
   const exprt pair = pair_value(char1_as_int, char2_as_int, return_type);
-  const exprt is_low =
-    is_low_surrogate(str[plus_exprt_with_overflow_check(pos, index1)]);
+  const exprt is_low = is_low_surrogate(str[plus_exprt(pos, index1)]);
   const and_exprt return_pair(is_high_surrogate(str[pos]), is_low);
 
   lemmas.push_back(implies_exprt(return_pair, equal_exprt(result, pair)));
@@ -210,8 +209,8 @@ exprt string_constraint_generatort::add_axioms_for_offset_by_code_point(
   const typet &return_type=f.type();
   const symbol_exprt result = fresh_symbol("offset_by_code_point", return_type);
 
-  const exprt minimum = plus_exprt_with_overflow_check(index, offset);
-  const exprt maximum = plus_exprt_with_overflow_check(minimum, offset);
+  const exprt minimum = plus_exprt(index, offset);
+  const exprt maximum = plus_exprt(minimum, offset);
   lemmas.push_back(binary_relation_exprt(result, ID_le, maximum));
   lemmas.push_back(binary_relation_exprt(result, ID_ge, minimum));
 

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -18,12 +18,15 @@ Author: Romain Brenguier, [email protected]
 /// at index `end_index'`.
 /// Where start_index' is max(0, start_index) and end_index' is
 /// max(min(end_index, s2.length), start_index')
+/// If s1.length + end_index' - start_index' is greater than the maximal integer
+/// of the type of res.length, then the result gets truncated to the size
+/// of this maximal integer.
 ///
 /// These axioms are:
-///   1. \f$|res| = |s_1| + end\_index' - start\_index' \f$
+///   1. \f$|res| = overflow ? |s_1| + end\_index' - start\_index'
+///                          : max_int \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$
+///   3. \f$\forall i< |res| - |s_1|.\ res[i+|s_1|] = s_2[start\_index'+i]\f$
 ///
 /// \param res: an array of characters expression
 /// \param s1: an array of characters expression
@@ -59,7 +62,8 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
       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);
+    const minus_exprt upper_bound(res.length(), s1.length());
+    return string_constraintt(idx2, upper_bound, res_eq);
   }());
 
   return from_integer(0, get_return_code_type());
@@ -77,10 +81,13 @@ exprt length_constraint_for_concat_substr(
   const exprt &start,
   const exprt &end)
 {
+  PRECONDITION(res.length().type().id() == ID_signedbv);
   const exprt start1 = maximum(start, from_integer(0, start.type()));
   const exprt end1 = maximum(minimum(end, s2.length()), start1);
   const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
-  return equal_exprt(res.length(), res_length);
+  const exprt overflow = sum_overflows(res_length);
+  const exprt max_int = to_signedbv_type(res.length().type()).largest_expr();
+  return equal_exprt(res.length(), if_exprt(overflow, max_int, res_length));
 }
 
 /// Add axioms enforcing that the length of `res` is that of the concatenation

src/solvers/refinement/string_constraint_generator_format.cpp

@@ -358,6 +358,7 @@ exprt string_constraint_generatort::add_axioms_for_format(
   const typet &index_type = res.length().type();
 
   for(const format_elementt &fe : format_strings)
+  {
     if(fe.is_format_specifier())
     {
       const format_specifiert &fs=fe.get_format_specifier();
@@ -392,24 +393,37 @@ exprt string_constraint_generatort::add_axioms_for_format(
         add_axioms_for_constant(str, fe.get_format_text().get_content());
       intermediary_strings.push_back(str);
     }
+  }
+
+  exprt return_code = from_integer(0, get_return_code_type());
 
   if(intermediary_strings.empty())
-    return to_array_string_expr(
-      array_exprt(array_typet(char_type, from_integer(0, index_type))));
+  {
+    lemmas.push_back(equal_exprt(res.length(), from_integer(0, index_type)));
+    return return_code;
+  }
 
-  auto it=intermediary_strings.begin();
-  array_string_exprt str = *(it++);
-  exprt return_code = from_integer(0, signedbv_typet(32));
-  for(; it!=intermediary_strings.end(); ++it)
+  array_string_exprt str = intermediary_strings[0];
+
+  if(intermediary_strings.size() == 1)
   {
+    // Copy the first string
+    return add_axioms_for_substring(
+      res, str, from_integer(0, index_type), str.length());
+  }
+
+  // start after the first string and stop before the last
+  for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
+  {
+    const array_string_exprt &intermediary = intermediary_strings[i];
     const array_string_exprt fresh = fresh_string(index_type, char_type);
     return_code =
-      bitor_exprt(return_code, add_axioms_for_concat(fresh, str, *it));
+      bitor_exprt(return_code, add_axioms_for_concat(fresh, str, intermediary));
     str = fresh;
   }
-  // Copy
-  add_axioms_for_substring(res, str, from_integer(0, index_type), str.length());
-  return return_code;
+
+  return bitor_exprt(
+    return_code, add_axioms_for_concat(res, str, intermediary_strings.back()));
 }
 
 /// Construct a string from a constant array.

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -352,8 +352,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   lemmas.push_back(a3);
 
   const exprt index1 = from_integer(1, index_type);
-  const exprt from_index_plus_one =
-    plus_exprt_with_overflow_check(from_index, index1);
+  const plus_exprt from_index_plus_one(from_index, index1);
   const if_exprt end_index(
     binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
     from_index_plus_one,

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -130,31 +130,19 @@ symbol_exprt string_constraint_generatort::fresh_boolean(
   return b;
 }
 
-/// Create a plus expression while adding extra constraints to axioms in order
-/// to prevent overflows.
-/// \param op1: First term of the sum
-/// \param op2: Second term of the sum
-/// \return A plus expression representing the sum of the arguments
-plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check(
-  const exprt &op1, const exprt &op2)
-{
-  plus_exprt sum(plus_exprt(op1, op2));
-
-  exprt zero=from_integer(0, op1.type());
-
-  binary_relation_exprt neg1(op1, ID_lt, zero);
-  binary_relation_exprt neg2(op2, ID_lt, zero);
-  binary_relation_exprt neg_sum(sum, ID_lt, zero);
-
-  // We prevent overflows by adding the following constraint:
-  // If the signs of the two operands are the same, then the sign of the sum
-  // should also be the same.
-  implies_exprt no_overflow(equal_exprt(neg1, neg2),
-                            equal_exprt(neg1, neg_sum));
-
-  lemmas.push_back(no_overflow);
-
-  return sum;
+exprt sum_overflows(const plus_exprt &sum)
+{
+  PRECONDITION(sum.operands().size() == 2);
+  const exprt zero = from_integer(0, sum.op0().type());
+  const binary_relation_exprt op0_negative(sum.op0(), ID_lt, zero);
+  const binary_relation_exprt op1_negative(sum.op1(), ID_lt, zero);
+  const binary_relation_exprt sum_negative(sum, ID_lt, zero);
+
+  // overflow happens when we add two values of same sign but their sum has a
+  // different sign
+  return and_exprt(
+    equal_exprt(op0_negative, op1_negative),
+    notequal_exprt(op1_negative, sum_negative));
 }
 
 /// Associate an actual finite length to infinite arrays

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -36,11 +36,10 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
   symbol_exprt isprefix=fresh_boolean("isprefix");
   const typet &index_type=str.length().type();
 
-  implies_exprt a1(
-    isprefix,
-    str.axiom_for_length_ge(plus_exprt_with_overflow_check(
-      prefix.length(), offset)));
-  lemmas.push_back(a1);
+  // Axiom 1.
+  lemmas.push_back(
+    implies_exprt(
+      isprefix, str.axiom_for_length_ge(plus_exprt(prefix.length(), offset))));
 
   symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type);
   string_constraintt a2(

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -175,9 +175,8 @@ exprt string_constraint_generatort::add_axioms_for_trim(
   const symbol_exprt idx = fresh_exist_index("index_trim", index_type);
   const exprt space_char = from_integer(' ', char_type);
 
-  exprt a1=str.axiom_for_length_ge(
-    plus_exprt_with_overflow_check(idx, res.length()));
-  lemmas.push_back(a1);
+  // Axiom 1.
+  lemmas.push_back(str.axiom_for_length_ge(plus_exprt(idx, res.length())));
 
   binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type));
   lemmas.push_back(a2);
@@ -197,32 +196,31 @@ exprt string_constraint_generatort::add_axioms_for_trim(
   string_constraintt a6(n, idx, non_print);
   constraints.push_back(a6);
 
-  symbol_exprt n2=fresh_univ_index("QA_index_trim2", index_type);
-  minus_exprt bound(str.length(), plus_exprt_with_overflow_check(idx,
-                                                                 res.length()));
-  binary_relation_exprt eqn2(
-    str[plus_exprt(idx, plus_exprt(res.length(), n2))],
-    ID_le,
-    space_char);
-
-  string_constraintt a7(n2, bound, eqn2);
-  constraints.push_back(a7);
+  // Axiom 7.
+  constraints.push_back([&] { // NOLINT
+    const symbol_exprt n2 = fresh_univ_index("QA_index_trim2", index_type);
+    const minus_exprt bound(minus_exprt(str.length(), idx), res.length());
+    const binary_relation_exprt eqn2(
+      str[plus_exprt(idx, plus_exprt(res.length(), n2))], ID_le, space_char);
+    return string_constraintt(n2, bound, eqn2);
+  }());
 
   symbol_exprt n3=fresh_univ_index("QA_index_trim3", index_type);
   equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
   string_constraintt a8(n3, res.length(), eqn3);
   constraints.push_back(a8);
 
-  minus_exprt index_before(
-    plus_exprt_with_overflow_check(idx, res.length()),
-      from_integer(1, index_type));
-  binary_relation_exprt no_space_before(str[index_before], ID_gt, space_char);
-  or_exprt a9(
-    equal_exprt(idx, str.length()),
-    and_exprt(
-      binary_relation_exprt(str[idx], ID_gt, space_char),
-      no_space_before));
-  lemmas.push_back(a9);
+  // Axiom 9.
+  lemmas.push_back([&] {
+    const plus_exprt index_before(
+      idx, minus_exprt(res.length(), from_integer(1, index_type)));
+    const binary_relation_exprt no_space_before(
+      str[index_before], ID_gt, space_char);
+    return or_exprt(
+      equal_exprt(idx, str.length()),
+      and_exprt(
+        binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before));
+  }());
   return from_integer(0, f.type());
 }
 
@@ -511,10 +509,7 @@ exprt string_constraint_generatort::add_axioms_for_delete_char_at(
   const array_string_exprt str = get_string_expr(f.arguments()[2]);
   exprt index_one=from_integer(1, str.length().type());
   return add_axioms_for_delete(
-    res,
-    str,
-    f.arguments()[3],
-    plus_exprt_with_overflow_check(f.arguments()[3], index_one));
+    res, str, f.arguments()[3], plus_exprt(f.arguments()[3], index_one));
 }
 
 /// Add axioms stating that `res` corresponds to the input `str`