String solver: stop relying on array size

jbmc/regression/jbmc-strings/literal_length/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.class
+--function test.main --trace
+^EXIT=10$
+^SIGNAL=0$
+^\[.*assertion.1\].* line 6.* FAILURE$
+abc_constarray=\{ 'a', 'b', 'c' \}
+--
+--
+Check that the string literal used in the constructor is properly concretized
+in the trace even if it is not part of the equation.
+This is necessary for test generation.

jbmc/regression/jbmc-strings/literal_length/test.java

@@ -0,0 +1,8 @@
+public class test
+{
+  public static void main()
+  {
+    String x = new String("abc");
+    assert false;
+  }
+}

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

@@ -88,18 +88,25 @@ 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));
+  return refined_string_exprt(
+    array_pool.get_or_create_length(arr), 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()));
+  const mp_integer n = numeric_cast_v<mp_integer>(
+    to_constant_expr(to_array_type(s.type()).size()));
   std::set<exprt> ret;
   for(mp_integer i = 0; i < n; ++i)
     ret.insert(from_integer(i));
@@ -179,17 +186,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 +257,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 +315,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 +365,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 +416,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 +469,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 +520,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/array_pool.cpp

@@ -21,25 +21,48 @@ operator()(const irep_idt &prefix, const typet &type)
   return result;
 }
 
-exprt array_poolt::get_length(const array_string_exprt &s) const
+exprt array_poolt::get_or_create_length(const array_string_exprt &s)
 {
-  if(s.length() == infinity_exprt(s.length().type()))
+  if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>((exprt)s))
   {
-    auto it = length_of_array.find(s);
-    if(it != length_of_array.end())
-      return it->second;
+    return if_exprt{
+      if_expr->cond(),
+      get_or_create_length(to_array_string_expr(if_expr->true_case())),
+      get_or_create_length(to_array_string_expr(if_expr->false_case()))};
   }
-  return s.length();
+
+  auto emplace_result =
+    length_of_array.emplace(s, symbol_exprt(s.length_type()));
+  if(emplace_result.second)
+  {
+    emplace_result.first->second =
+      fresh_symbol("string_length", s.length_type());
+  }
+
+  return emplace_result.first->second;
+}
+
+optionalt<exprt>
+array_poolt::get_length_if_exists(const array_string_exprt &s) const
+{
+  auto find_result = length_of_array.find(s);
+  if(find_result != length_of_array.end())
+    return find_result->second;
+  return {};
 }
 
 array_string_exprt
 array_poolt::fresh_string(const typet &index_type, const typet &char_type)
 {
-  symbol_exprt length = fresh_symbol("string_length", index_type);
-  array_typet array_type(char_type, length);
+  array_typet array_type{char_type, infinity_exprt(index_type)};
   symbol_exprt content = fresh_symbol("string_content", array_type);
   array_string_exprt str = to_array_string_expr(content);
-  created_strings_value.insert(str);
+  arrays_of_pointers.emplace(
+    address_of_exprt(index_exprt(str, from_integer(0, index_type))), str);
+
+  // add length to length_of_array map
+  get_or_create_length(str);
+
   return str;
 }
 
@@ -87,40 +110,73 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
     to_array_string_expr(fresh_symbol(symbol_name, char_array_type));
   const auto insert_result =
     arrays_of_pointers.insert({char_pointer, array_sym});
+
+  // add length to length_of_array map
+  get_or_create_length(array_sym);
+
   return to_array_string_expr(insert_result.first->second);
 }
 
+/// Given an array_string_exprt, get the size of the underlying array. If that
+/// size is undefined, create a new symbol for the size.
+/// Then add an entry from `array_expr` to that size in the `length_of_array`
+/// map.
+///
+/// This function should only be used at the creation of the
+/// `array_string_exprt`s, as it is the only place where we can reliably refer
+/// to the size in the type of the array.
+static void attempt_assign_length_from_type(
+  const array_string_exprt &array_expr,
+  std::unordered_map<array_string_exprt, exprt, irep_hash> &length_of_array,
+  symbol_generatort &symbol_generator)
+{
+  DATA_INVARIANT(
+    array_expr.id() != ID_if,
+    "attempt_assign_length_from_type does not handle if exprts");
+  // This invariant seems always true, but I don't know why.
+  // If we find a case where this is violated, try calling
+  // attempt_assign_length_from_type on the true and false cases.
+  const exprt &size_from_type = to_array_type(array_expr.type()).size();
+  const exprt &size_to_assign =
+    size_from_type != infinity_exprt(size_from_type.type())
+      ? size_from_type
+      : symbol_generator("string_length", array_expr.length_type());
+
+  const auto emplace_result =
+    length_of_array.emplace(array_expr, size_to_assign);
+  INVARIANT(
+    emplace_result.second,
+    "attempt_assign_length_from_type should only be called when no entry"
+    "for the array_string_exprt exists in the length_of_array map");
+}
+
 void array_poolt::insert(
   const exprt &pointer_expr,
-  array_string_exprt &array_expr)
+  const array_string_exprt &array_expr)
 {
-  const exprt &length = array_expr.length();
-  if(length == infinity_exprt(length.type()))
-  {
-    auto pair = length_of_array.insert(
-      std::make_pair(array_expr, fresh_symbol("string_length", length.type())));
-    array_expr.length() = pair.first->second;
-  }
-
   const auto it_bool =
     arrays_of_pointers.insert(std::make_pair(pointer_expr, array_expr));
-  created_strings_value.insert(array_expr);
+
   INVARIANT(
     it_bool.second, "should not associate two arrays to the same pointer");
+
+  attempt_assign_length_from_type(array_expr, length_of_array, fresh_symbol);
 }
 
-const std::set<array_string_exprt> &array_poolt::created_strings() const
+/// Return a map mapping all array_string_exprt of the array_pool to their
+/// length.
+const std::unordered_map<array_string_exprt, exprt, irep_hash> &
+array_poolt::created_strings() const
 {
-  return created_strings_value;
+  return length_of_array;
 }
 
-const array_string_exprt &
-array_poolt::find(const exprt &pointer, const exprt &length)
+array_string_exprt array_poolt::find(const exprt &pointer, const exprt &length)
 {
   const array_typet array_type(pointer.type().subtype(), length);
   const array_string_exprt array =
     make_char_array_for_char_pointer(pointer, array_type);
-  return *created_strings_value.insert(array).first;
+  return array;
 }
 
 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)

src/solvers/strings/array_pool.h

@@ -53,17 +53,31 @@ class array_poolt final
     return arrays_of_pointers;
   }
 
-  /// Associate an actual finite length to infinite arrays
+  /// Get the length of an array_string_exprt from the array_pool. If the length
+  /// does not yet exist, create a new symbol and add it to the pool.
+  ///
+  /// If the array_string_exprt is an `if` expression, the true and false parts
+  /// are handled independently (and recursively). That is, no new length symbol
+  /// is added to the pool for `if` expressions, but symbols may be added for
+  /// each of the parts.
   /// \param s: array expression representing a string
   /// \return expression for the length of `s`
-  exprt get_length(const array_string_exprt &s) const;
+  exprt get_or_create_length(const array_string_exprt &s);
 
-  void insert(const exprt &pointer_expr, array_string_exprt &array);
+  /// As opposed to get_length(), do not create a new symbol if the length
+  /// of the array_string_exprt does not have one in the array_pool, but instead
+  /// return an empty optional.
+  /// \param s: array expression representing a string
+  /// \return expression for the length of `s`, or empty optional
+  optionalt<exprt> get_length_if_exists(const array_string_exprt &s) const;
+
+  void insert(const exprt &pointer_expr, const array_string_exprt &array);
 
   /// Creates a new array if the pointer is not pointing to an array
-  const array_string_exprt &find(const exprt &pointer, const exprt &length);
+  array_string_exprt find(const exprt &pointer, const exprt &length);
 
-  const std::set<array_string_exprt> &created_strings() const;
+  const std::unordered_map<array_string_exprt, exprt, irep_hash> &
+  created_strings() const;
 
   /// Construct a string expression whose length and content are new variables
   /// \param index_type: type used to index characters of the strings
@@ -74,18 +88,19 @@ class array_poolt final
 
 private:
   /// Associate arrays to char pointers
+  /// Invariant: Each array_string_exprt in this map has a corresponding entry
+  ///            in length_of_array.
+  ///            This is enforced whenever we add an element to
+  ///            `arrays_of_pointers`, i.e. fresh_string()
+  ///            and make_char_array_for_char_pointer().
   std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
 
   /// Associate length to arrays of infinite size
-  std::unordered_map<array_string_exprt, symbol_exprt, irep_hash>
-    length_of_array;
+  std::unordered_map<array_string_exprt, exprt, irep_hash> length_of_array;
 
   /// Generate fresh symbols
   symbol_generatort &fresh_symbol;
 
-  /// Strings created in the pool
-  std::set<array_string_exprt> created_strings_value;
-
   array_string_exprt make_char_array_for_char_pointer(
     const exprt &char_pointer,
     const typet &char_array_type);