Fix string_constraintt bound values

Some of the bounds could be negative, potentially leading to
inconsistencies in the index set.
Bounds that are at risk have been replaced by `maximum(0, old_bound)`.

Author: Joel Allred

src/solvers/refinement/string_constraint_generator.h

@@ -458,4 +458,5 @@ exprt length_constraint_for_insert(
   const array_string_exprt &s1,
   const array_string_exprt &s2);
 
+exprt zero_if_negative(const exprt &expr);
 #endif

src/solvers/refinement/string_constraint_generator_comparison.cpp

@@ -45,7 +45,9 @@ exprt string_constraint_generatort::add_axioms_for_equals(
 
   symbol_exprt qvar=fresh_univ_index("QA_equal", index_type);
   string_constraintt a2(
-    qvar, s1.length(), implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
+    qvar,
+    zero_if_negative(s1.length()),
+    implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
   constraints.push_back(a2);
 
   symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
@@ -132,7 +134,8 @@ exprt string_constraint_generatort::add_axioms_for_equals_ignore_case(
     fresh_univ_index("QA_equal_ignore_case", index_type);
   const exprt constr2 =
     character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
-  const string_constraintt a2(qvar, s1.length(), implies_exprt(eq, constr2));
+  const string_constraintt a2(
+    qvar, zero_if_negative(s1.length()), implies_exprt(eq, constr2));
   constraints.push_back(a2);
 
   const symbol_exprt witness =
@@ -226,7 +229,9 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const symbol_exprt i = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a2(
-    i, s1.length(), implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
+    i,
+    zero_if_negative(s1.length()),
+    implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
   constraints.push_back(a2);
 
   const symbol_exprt x = fresh_exist_index("index_compare_to", index_type);
@@ -257,7 +262,9 @@ exprt string_constraint_generatort::add_axioms_for_compare_to(
 
   const symbol_exprt i2 = fresh_univ_index("QA_compare_to", index_type);
   const string_constraintt a4(
-    i2, x, implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])));
+    i2,
+    zero_if_negative(x),
+    implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])));
   constraints.push_back(a4);
 
   return res;

src/solvers/refinement/string_constraint_generator_concat.cpp

@@ -53,7 +53,8 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
   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]));
+    return string_constraintt(
+      idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
   }());
 
   // Axiom 3.
@@ -63,7 +64,7 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
     const equal_exprt res_eq(
       res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
     const minus_exprt upper_bound(res.length(), s1.length());
-    return string_constraintt(idx2, upper_bound, res_eq);
+    return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
   }());
 
   return from_integer(0, get_return_code_type());
@@ -120,7 +121,8 @@ exprt string_constraint_generatort::add_axioms_for_concat_char(
   lemmas.push_back(length_constraint_for_concat_char(res, s1));
 
   symbol_exprt idx = fresh_univ_index("QA_index_concat_char", index_type);
-  string_constraintt a2(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
+  string_constraintt a2(
+    idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
   constraints.push_back(a2);
 
   equal_exprt a3(res[s1.length()], c);

src/solvers/refinement/string_constraint_generator_indexof.cpp

@@ -59,20 +59,21 @@ exprt string_constraint_generatort::add_axioms_for_index_of(
       equal_exprt(str[index], c)));
   lemmas.push_back(a3);
 
-  const auto zero = from_integer(0, index_type);
-  const if_exprt lower_bound(
-    binary_relation_exprt(from_index, ID_le, zero), zero, from_index);
+  const exprt lower_bound(zero_if_negative(from_index));
 
   symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a4(
-    n, lower_bound, index, implies_exprt(contains, notequal_exprt(str[n], c)));
+    n,
+    lower_bound,
+    zero_if_negative(index),
+    implies_exprt(contains, notequal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
   string_constraintt a5(
     m,
     lower_bound,
-    str.length(),
+    zero_if_negative(str.length()),
     implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
   constraints.push_back(a5);
 
@@ -128,7 +129,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of_string(
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   string_constraintt a3(
     qvar,
-    needle.length(),
+    zero_if_negative(needle.length()),
     implies_exprt(
       contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
   constraints.push_back(a3);
@@ -221,7 +222,7 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of_string(
   symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
   equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
   const string_constraintt a3(
-    qvar, needle.length(), implies_exprt(contains, constr3));
+    qvar, zero_if_negative(needle.length()), implies_exprt(contains, constr3));
   constraints.push_back(a3);
 
   // end_index is min(from_index, |str| - |substring|)
@@ -361,15 +362,15 @@ exprt string_constraint_generatort::add_axioms_for_last_index_of(
   const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type);
   const string_constraintt a4(
     n,
-    plus_exprt(index, index1),
-    end_index,
+    zero_if_negative(plus_exprt(index, index1)),
+    zero_if_negative(end_index),
     implies_exprt(contains, notequal_exprt(str[n], c)));
   constraints.push_back(a4);
 
   const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
   const string_constraintt a5(
     m,
-    end_index,
+    zero_if_negative(end_index),
     implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
   constraints.push_back(a5);
 

src/solvers/refinement/string_constraint_generator_insert.cpp

@@ -53,7 +53,9 @@ exprt string_constraint_generatort::add_axioms_for_insert(
   constraints.push_back([&] { // NOLINT
     const symbol_exprt i = fresh_symbol("QA_insert2", index_type);
     return string_constraintt(
-      i, s2.length(), equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
+      i,
+      zero_if_negative(s2.length()),
+      equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
   }());
 
   // Axiom 4.
@@ -62,7 +64,7 @@ exprt string_constraint_generatort::add_axioms_for_insert(
     return string_constraintt(
       i,
       offset1,
-      s1.length(),
+      zero_if_negative(s1.length()),
       equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
   }());
 

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -324,7 +324,8 @@ void string_constraint_generatort::add_constraint_on_characters(
   const and_exprt char_in_set(
     binary_relation_exprt(chr, ID_ge, from_integer(low_char, chr.type())),
     binary_relation_exprt(chr, ID_le, from_integer(high_char, chr.type())));
-  const string_constraintt sc(qvar, start, end, char_in_set);
+  const string_constraintt sc(
+    qvar, zero_if_negative(start), zero_if_negative(end), char_in_set);
   constraints.push_back(sc);
 }
 
@@ -627,3 +628,11 @@ exprt maximum(const exprt &a, const exprt &b)
 {
   return if_exprt(binary_relation_exprt(a, ID_le, b), b, a);
 }
+
+/// Returns a non-negative version of the argument.
+/// \param  expr: expression of which we want a non-negative version
+/// \return `max(0, expr)`
+exprt zero_if_negative(const exprt &expr)
+{
+  return maximum(from_integer(0, expr.type()), expr);
+}

src/solvers/refinement/string_constraint_generator_testing.cpp

@@ -54,7 +54,8 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix(
     const symbol_exprt qvar = fresh_univ_index("QA_isprefix", index_type);
     const exprt body = implies_exprt(
       isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
-    return string_constraintt(qvar, prefix.length(), body);
+    return string_constraintt(
+      qvar, maximum(from_integer(0, index_type), prefix.length()), body);
   }());
 
   // Axiom 3.
@@ -169,7 +170,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix(
   const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
   string_constraintt a2(
     qvar,
-    s0.length(),
+    zero_if_negative(s0.length()),
     implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
   constraints.push_back(a2);
 
@@ -239,7 +240,7 @@ exprt string_constraint_generatort::add_axioms_for_contains(
   const plus_exprt qvar_shifted(qvar, startpos);
   string_constraintt a4(
     qvar,
-    s1.length(),
+    zero_if_negative(s1.length()),
     implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
   constraints.push_back(a4);
 

src/solvers/refinement/string_constraint_generator_transformation.cpp

@@ -52,14 +52,16 @@ exprt string_constraint_generatort::add_axioms_for_set_length(
 
   const symbol_exprt idx = fresh_univ_index("QA_index_set_length", index_type);
   const string_constraintt a2(
-    idx, minimum(s1.length(), k), equal_exprt(s1[idx], res[idx]));
+    idx,
+    zero_if_negative(minimum(s1.length(), k)),
+    equal_exprt(s1[idx], res[idx]));
   constraints.push_back(a2);
 
   symbol_exprt idx2 = fresh_univ_index("QA_index_set_length2", index_type);
   string_constraintt a3(
     idx2,
-    s1.length(),
-    res.length(),
+    zero_if_negative(s1.length()),
+    zero_if_negative(res.length()),
     equal_exprt(res[idx2], constant_char(0, char_type)));
   constraints.push_back(a3);
 
@@ -131,7 +133,9 @@ exprt string_constraint_generatort::add_axioms_for_substring(
   constraints.push_back([&] {
     const symbol_exprt idx = fresh_univ_index("QA_index_substring", index_type);
     return string_constraintt(
-      idx, res.length(), equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
+      idx,
+      zero_if_negative(res.length()),
+      equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
   }());
 
   return from_integer(0, signedbv_typet(32));
@@ -193,7 +197,7 @@ exprt string_constraint_generatort::add_axioms_for_trim(
 
   symbol_exprt n=fresh_univ_index("QA_index_trim", index_type);
   binary_relation_exprt non_print(str[n], ID_le, space_char);
-  string_constraintt a6(n, idx, non_print);
+  string_constraintt a6(n, zero_if_negative(idx), non_print);
   constraints.push_back(a6);
 
   // Axiom 7.
@@ -202,12 +206,12 @@ exprt string_constraint_generatort::add_axioms_for_trim(
     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);
+    return string_constraintt(n2, zero_if_negative(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);
+  string_constraintt a8(n3, zero_if_negative(res.length()), eqn3);
   constraints.push_back(a8);
 
   // Axiom 9.
@@ -291,7 +295,8 @@ exprt string_constraint_generatort::add_axioms_for_to_lower_case(
     binary_relation_exprt(str[idx], ID_lt, from_integer(0x100, char_type)));
   if_exprt conditional_convert(is_upper_case, converted, non_converted);
 
-  string_constraintt a2(idx, res.length(), conditional_convert);
+  string_constraintt a2(
+    idx, zero_if_negative(res.length()), conditional_convert);
   constraints.push_back(a2);
 
   return from_integer(0, f.type());
@@ -338,7 +343,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
   minus_exprt diff(char_A, char_a);
   equal_exprt convert(res[idx1], plus_exprt(str[idx1], diff));
   implies_exprt body1(is_lower_case, convert);
-  string_constraintt a2(idx1, res.length(), body1);
+  string_constraintt a2(idx1, zero_if_negative(res.length()), body1);
   constraints.push_back(a2);
 
   symbol_exprt idx2=fresh_univ_index("QA_upper_case2", index_type);
@@ -348,7 +353,7 @@ exprt string_constraint_generatort::add_axioms_for_to_upper_case(
       binary_relation_exprt(str[idx2], ID_le, char_z)));
   equal_exprt eq(res[idx2], str[idx2]);
   implies_exprt body2(is_not_lower_case, eq);
-  string_constraintt a3(idx2, res.length(), body2);
+  string_constraintt a3(idx2, zero_if_negative(res.length()), body2);
   constraints.push_back(a3);
   return from_integer(0, signedbv_typet(32));
 }
@@ -406,13 +411,15 @@ exprt string_constraint_generatort::add_axioms_for_char_set(
 
   const symbol_exprt q = fresh_univ_index("QA_char_set", position.type());
   const equal_exprt a3_body(res[q], str[q]);
-  const string_constraintt a3(q, minimum(res.length(), position), a3_body);
+  const string_constraintt a3(
+    q, minimum(zero_if_negative(res.length()), position), a3_body);
   constraints.push_back(a3);
 
   const symbol_exprt q2 = fresh_univ_index("QA_char_set2", position.type());
   const plus_exprt lower_bound(position, from_integer(1, position.type()));
   const equal_exprt a4_body(res[q2], str[q2]);
-  const string_constraintt a4(q2, lower_bound, res.length(), a4_body);
+  const string_constraintt a4(
+    q2, lower_bound, zero_if_negative(res.length()), a4_body);
   constraints.push_back(a4);
 
   return if_exprt(
@@ -489,7 +496,8 @@ exprt string_constraint_generatort::add_axioms_for_replace(
     implies_exprt case2(
       not_exprt(equal_exprt(str[qvar], old_char)),
       equal_exprt(res[qvar], str[qvar]));
-    string_constraintt a2(qvar, res.length(), and_exprt(case1, case2));
+    string_constraintt a2(
+      qvar, zero_if_negative(res.length()), and_exprt(case1, case2));
     constraints.push_back(a2);
     return from_integer(0, f.type());
   }