[TG-3912] Sanitize string_constraintt bounds

src/solvers/Makefile

@@ -166,6 +166,7 @@ SRC = $(BOOLEFORCE_SRC) \
       refinement/string_builtin_function.cpp \
       refinement/string_refinement.cpp \
       refinement/string_refinement_util.cpp \
+      refinement/string_constraint.cpp \
       refinement/string_constraint_generator_code_points.cpp \
       refinement/string_constraint_generator_comparison.cpp \
       refinement/string_constraint_generator_concat.cpp \

src/solvers/refinement/string_constraint.cpp

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+ Module: String solver
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include "string_constraint.h"
+
+#include <solvers/sat/satcheck.h>
+#include <util/symbol_table.h>
+
+/// Runs a solver instance to verify whether an expression can only be
+//  non-negative.
+/// \param expr: the expression to check for negativity
+/// \return true if `expr < 0` is unsatisfiable, false otherwise
+static bool cannot_be_neg(const exprt &expr)
+{
+  satcheck_no_simplifiert sat_check;
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  boolbvt solver(ns, sat_check);
+  const exprt zero = from_integer(0, expr.type());
+  const binary_relation_exprt non_neg(expr, ID_lt, zero);
+  solver << non_neg;
+  return solver() == decision_proceduret::resultt::D_UNSATISFIABLE;
+}
+
+string_constraintt::string_constraintt(
+  const symbol_exprt &_univ_var,
+  const exprt &lower_bound,
+  const exprt &upper_bound,
+  const exprt &body)
+  : univ_var(_univ_var),
+    lower_bound(lower_bound),
+    upper_bound(upper_bound),
+    body(body)
+{
+  INVARIANT(
+    cannot_be_neg(lower_bound),
+    "String constraints must have non-negative lower bound.\n" +
+      lower_bound.pretty());
+  INVARIANT(
+    cannot_be_neg(upper_bound),
+    "String constraints must have non-negative upper bound.\n" +
+      upper_bound.pretty());
+}

src/solvers/refinement/string_constraint.h

@@ -68,16 +68,10 @@ class string_constraintt final
   string_constraintt() = delete;
 
   string_constraintt(
-    symbol_exprt _univ_var,
-    exprt lower_bound,
-    exprt upper_bound,
-    exprt body)
-    : univ_var(_univ_var),
-      lower_bound(lower_bound),
-      upper_bound(upper_bound),
-      body(body)
-  {
-  }
+    const symbol_exprt &_univ_var,
+    const exprt &lower_bound,
+    const exprt &upper_bound,
+    const exprt &body);
 
   // Default bound inferior is 0
   string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)

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

@@ -39,26 +39,33 @@ exprt string_constraint_generatort::add_axioms_for_equals(
 
   typet index_type=s1.length().type();
 
-
-  implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
-  lemmas.push_back(a1);
-
-  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])));
-  constraints.push_back(a2);
-
-  symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
-  exprt zero=from_integer(0, index_type);
-  and_exprt bound_witness(
-    binary_relation_exprt(witness, ID_lt, s1.length()),
-    binary_relation_exprt(witness, ID_ge, zero));
-  and_exprt witnessing(bound_witness, notequal_exprt(s1[witness], s2[witness]));
-  and_exprt diff_length(
-    notequal_exprt(s1.length(), s2.length()),
-    equal_exprt(witness, from_integer(-1, index_type)));
-  implies_exprt a3(not_exprt(eq), or_exprt(diff_length, witnessing));
-  lemmas.push_back(a3);
+  // Axiom 1.
+  lemmas.push_back(implies_exprt(eq, equal_exprt(s1.length(), s2.length())));
+
+  // Axiom 2.
+  constraints.push_back([&] {
+    const symbol_exprt qvar = fresh_univ_index("QA_equal", index_type);
+    return string_constraintt(
+      qvar,
+      zero_if_negative(s1.length()),
+      implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
+  }());
+
+  // Axiom 3.
+  lemmas.push_back([&] {
+    const symbol_exprt witness =
+      fresh_exist_index("witness_unequal", index_type);
+    const exprt zero = from_integer(0, index_type);
+    const and_exprt bound_witness(
+      binary_relation_exprt(witness, ID_lt, s1.length()),
+      binary_relation_exprt(witness, ID_ge, zero));
+    const and_exprt witnessing(
+      bound_witness, notequal_exprt(s1[witness], s2[witness]));
+    const and_exprt diff_length(
+      notequal_exprt(s1.length(), s2.length()),
+      equal_exprt(witness, from_integer(-1, index_type)));
+    return implies_exprt(not_exprt(eq), or_exprt(diff_length, witnessing));
+  }());
 
   return tc_eq;
 }
@@ -132,7 +139,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 +234,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 +267,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

@@ -50,20 +50,21 @@ exprt string_constraint_generatort::add_axioms_for_concat_substr(
     length_constraint_for_concat_substr(res, s1, s2, start_index, end_index));
 
   // Axiom 2.
-  constraints.push_back([&] { // NOLINT
+  constraints.push_back([&] {
     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.
-  constraints.push_back([&] { // NOLINT
+  constraints.push_back([&] {
     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)]);
     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);