Propagate array_pool to constraint generation

Argument will be required to query string lengths.

Author: Joel Allred

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -88,16 +88,21 @@ exprt get_data_pointer(const array_string_exprt &arr)
 
 /// Creates a `string_exprt` of the proper string type.
 /// \param [in] str: string to convert
+/// \param array_pool: pool of arrays representing strings
 /// \return corresponding `string_exprt`
-refined_string_exprt make_refined_string_exprt(const array_string_exprt &arr)
+refined_string_exprt make_refined_string_exprt(
+  const array_string_exprt &arr,
+  array_poolt &array_pool)
 {
   return refined_string_exprt(arr.length(), get_data_pointer(arr));
 }
 
 /// For a constant `string_exprt`, creates a full index set.
 /// \param [in] s: `string_exprt` to create index set for
+/// \param array_pool: pool of arrays representing strings
 /// \return the corresponding index set
-std::set<exprt> full_index_set(const array_string_exprt &s)
+std::set<exprt>
+full_index_set(const array_string_exprt &s, array_poolt &array_pool)
 {
   const mp_integer n = numeric_cast_v<mp_integer>(to_constant_expr(s.length()));
   std::set<exprt> ret;
@@ -179,17 +184,20 @@ SCENARIO(
   // initialize architecture with sensible default values
   config.set_arch("none");
 
+  symbol_generatort symbol_generator;
+  array_poolt array_pool(symbol_generator);
+
   // Creating strings
   const auto ab_array = make_string_exprt("ab");
   const auto b_array = make_string_exprt("b");
   const auto a_array = make_string_exprt("a");
   const auto empty_array = make_string_exprt("");
   const auto cd_array = make_string_exprt("cd");
-  const auto ab = make_refined_string_exprt(ab_array);
-  const auto b = make_refined_string_exprt(b_array);
-  const auto a = make_refined_string_exprt(a_array);
-  const auto empty = make_refined_string_exprt(empty_array);
-  const auto cd = make_refined_string_exprt(cd_array);
+  const auto ab = make_refined_string_exprt(ab_array, array_pool);
+  const auto b = make_refined_string_exprt(b_array, array_pool);
+  const auto a = make_refined_string_exprt(a_array, array_pool);
+  const auto empty = make_refined_string_exprt(empty_array, array_pool);
+  const auto cd = make_refined_string_exprt(cd_array, array_pool);
 
   GIVEN("The not_contains axioms of String.lastIndexOf(String, Int)")
   {
@@ -247,8 +255,8 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_ab = full_index_set(ab_array);
-      const std::set<exprt> index_set_b = full_index_set(b_array);
+      const std::set<exprt> index_set_ab = full_index_set(ab_array, array_pool);
+      const std::set<exprt> index_set_b = full_index_set(b_array, array_pool);
 
       // List of new lemmas to be returned
       std::vector<exprt> lemmas;
@@ -305,7 +313,7 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_a = full_index_set(a_array);
+      const std::set<exprt> index_set_a = full_index_set(a_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(
@@ -355,8 +363,8 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_a = full_index_set(a_array);
-      const std::set<exprt> index_set_b = full_index_set(b_array);
+      const std::set<exprt> index_set_a = full_index_set(a_array, array_pool);
+      const std::set<exprt> index_set_b = full_index_set(b_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(
@@ -406,7 +414,7 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_a = full_index_set(a_array);
+      const std::set<exprt> index_set_a = full_index_set(a_array, array_pool);
       const std::set<exprt> index_set_empty = {
         generator.fresh_symbol("z", t.length_type())};
 
@@ -459,7 +467,7 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_ab = full_index_set(ab_array);
+      const std::set<exprt> index_set_ab = full_index_set(ab_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(
@@ -510,8 +518,8 @@ SCENARIO(
     WHEN("we instantiate and simplify")
     {
       // Making index sets
-      const std::set<exprt> index_set_ab = full_index_set(ab_array);
-      const std::set<exprt> index_set_cd = full_index_set(cd_array);
+      const std::set<exprt> index_set_ab = full_index_set(ab_array, array_pool);
+      const std::set<exprt> index_set_cd = full_index_set(cd_array, array_pool);
 
       // Instantiate the lemmas
       std::vector<exprt> lemmas = instantiate_not_contains(

src/solvers/strings/string_builtin_function.cpp

@@ -144,11 +144,17 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
   auto pair = [&]() -> std::pair<exprt, string_constraintst> {
     if(args.size() == 0)
       return add_axioms_for_concat(
-        generator.fresh_symbol, result, input1, input2);
+        generator.fresh_symbol, result, input1, input2, array_pool);
     if(args.size() == 2)
     {
       return add_axioms_for_concat_substr(
-        generator.fresh_symbol, result, input1, input2, args[0], args[1]);
+        generator.fresh_symbol,
+        result,
+        input1,
+        input2,
+        args[0],
+        args[1],
+        array_pool);
     }
     UNREACHABLE;
   }();
@@ -159,10 +165,10 @@ string_constraintst string_concatenation_builtin_functiont::constraints(
 exprt string_concatenation_builtin_functiont::length_constraint() const
 {
   if(args.size() == 0)
-    return length_constraint_for_concat(result, input1, input2);
+    return length_constraint_for_concat(result, input1, input2, array_pool);
   if(args.size() == 2)
     return length_constraint_for_concat_substr(
-      result, input1, input2, args[0], args[1]);
+      result, input1, input2, args[0], args[1], array_pool);
   UNREACHABLE;
 }
 
@@ -214,7 +220,7 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
 
 exprt string_concat_char_builtin_functiont::length_constraint() const
 {
-  return length_constraint_for_concat_char(result, input);
+  return length_constraint_for_concat_char(result, input, array_pool);
 }
 
 optionalt<exprt> string_set_char_builtin_functiont::eval(
@@ -491,7 +497,7 @@ string_constraintst string_insertion_builtin_functiont::constraints(
   if(args.size() == 1)
   {
     auto pair = add_axioms_for_insert(
-      generator.fresh_symbol, result, input1, input2, args[0]);
+      generator.fresh_symbol, result, input1, input2, args[0], array_pool);
     pair.second.existential.push_back(equal_exprt(pair.first, return_code));
     return pair.second;
   }
@@ -503,7 +509,7 @@ string_constraintst string_insertion_builtin_functiont::constraints(
 exprt string_insertion_builtin_functiont::length_constraint() const
 {
   if(args.size() == 1)
-    return length_constraint_for_insert(result, input1, input2);
+    return length_constraint_for_insert(result, input1, input2, array_pool);
   if(args.size() == 3)
     UNIMPLEMENTED;
   UNREACHABLE;
@@ -562,7 +568,7 @@ string_constraintst string_of_int_builtin_functiont::constraints(
   string_constraint_generatort &generator) const
 {
   auto pair = add_axioms_for_string_of_int_with_radix(
-    result, arg, radix, 0, generator.ns);
+    result, arg, radix, 0, generator.ns, array_pool);
   pair.second.existential.push_back(equal_exprt(pair.first, return_code));
   return pair.second;
 }

src/solvers/strings/string_constraint_generator.h

@@ -96,33 +96,38 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2);
+  const array_string_exprt &s2,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &s1,
   const array_string_exprt &s2,
   const exprt &start_index,
-  const exprt &end_index);
+  const exprt &end_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_insert(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const array_string_exprt &s1,
   const array_string_exprt &s2,
-  const exprt &offset);
+  const exprt &offset,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_string_of_int_with_radix(
   const array_string_exprt &res,
   const exprt &input_int,
   const exprt &radix,
   size_t max_size,
-  const namespacet &ns);
+  const namespacet &ns,
+  array_poolt &array_pool);
 
 string_constraintst add_constraint_on_characters(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &s,
   const exprt &start,
   const exprt &end,
-  const std::string &char_set);
+  const std::string &char_set,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -196,6 +201,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
 std::pair<exprt, string_constraintst> add_axioms_for_constant(
   const array_string_exprt &res,
   irep_idt sval,
+  array_poolt &array_pool,
   const exprt &guard = true_exprt());
 
 std::pair<exprt, string_constraintst> add_axioms_for_delete(
@@ -260,7 +266,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
   const exprt &arg,
-  const exprt &guard);
+  const exprt &guard,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_literal(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -270,9 +277,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_int(
   const array_string_exprt &res,
   const exprt &input_int,
   size_t max_size,
-  const namespacet &ns);
-std::pair<exprt, string_constraintst>
-add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i);
+  const namespacet &ns,
+  array_poolt &array_pool);
+std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
+  const array_string_exprt &res,
+  const exprt &i,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
   const function_application_exprt &f,
   array_poolt &array_pool);
@@ -283,23 +293,29 @@ std::pair<exprt, string_constraintst> add_axioms_from_long(
 std::pair<exprt, string_constraintst> add_axioms_from_bool(
   const function_application_exprt &f,
   array_poolt &array_pool);
-std::pair<exprt, string_constraintst>
-add_axioms_from_bool(const array_string_exprt &res, const exprt &i);
+std::pair<exprt, string_constraintst> add_axioms_from_bool(
+  const array_string_exprt &res,
+  const exprt &b,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_char(
   const function_application_exprt &f,
   array_poolt &array_pool);
-std::pair<exprt, string_constraintst>
-add_axioms_from_char(const array_string_exprt &res, const exprt &i);
+std::pair<exprt, string_constraintst> add_axioms_from_char(
+  const array_string_exprt &res,
+  const exprt &c,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &str,
   const exprt &c,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &haystack,
   const array_string_exprt &needle,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -308,12 +324,14 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &haystack,
   const array_string_exprt &needle,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &str,
   const exprt &c,
-  const exprt &from_index);
+  const exprt &from_index,
+  array_poolt &array_pool);
 
 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   symbol_generatort &fresh_symbol,
@@ -338,8 +356,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   const namespacet &ns);
 std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   const array_string_exprt &res,
-  const exprt &i,
-  size_t max_size);
+  const exprt &int_expr,
+  size_t max_size,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   symbol_generatort &fresh_symbol,
   const array_string_exprt &res,
@@ -377,7 +396,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
   const array_string_exprt &res,
   const array_string_exprt &str,
   const exprt &start,
-  const exprt &end);
+  const exprt &end,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_substring(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -390,7 +410,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
 
 std::pair<exprt, string_constraintst> add_axioms_for_code_point(
   const array_string_exprt &res,
-  const exprt &code_point);
+  const exprt &code_point,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst>
 add_axioms_for_char_literal(const function_application_exprt &f);
 
@@ -422,13 +443,15 @@ string_constraintst add_axioms_for_characters_in_integer_string(
   const array_string_exprt &str,
   const std::size_t max_string_length,
   const exprt &radix,
-  const unsigned long radix_ul);
+  const unsigned long radix_ul,
+  array_poolt &array_pool);
 string_constraintst add_axioms_for_correct_number_format(
   const array_string_exprt &str,
   const exprt &radix_as_char,
   const unsigned long radix_ul,
   const std::size_t max_size,
-  const bool strict_formatting);
+  const bool strict_formatting,
+  array_poolt &array_pool);
 std::pair<exprt, string_constraintst> add_axioms_for_parse_int(
   symbol_generatort &fresh_symbol,
   const function_application_exprt &f,
@@ -470,21 +493,25 @@ exprt sum_overflows(const plus_exprt &sum);
 
 exprt length_constraint_for_concat_char(
   const array_string_exprt &res,
-  const array_string_exprt &s1);
+  const array_string_exprt &s1,
+  array_poolt &array_pool);
 exprt length_constraint_for_concat(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2);
+  const array_string_exprt &s2,
+  array_poolt &array_pool);
 exprt length_constraint_for_concat_substr(
   const array_string_exprt &res,
   const array_string_exprt &s1,
   const array_string_exprt &s2,
-  const exprt &start_index,
-  const exprt &end_index);
+  const exprt &start,
+  const exprt &end,
+  array_poolt &array_pool);
 exprt length_constraint_for_insert(
   const array_string_exprt &res,
   const array_string_exprt &s1,
-  const array_string_exprt &s2);
+  const array_string_exprt &s2,
+  array_poolt &array_pool);
 
 exprt zero_if_negative(const exprt &expr);