Fix handling of null array in string refinement [TG-3726]

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -184,59 +184,37 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
   PRECONDITION(
     char_array_type.subtype().id() == ID_unsignedbv ||
     char_array_type.subtype().id() == ID_signedbv);
-  std::string symbol_name;
-  if(
-    char_pointer.id() == ID_address_of &&
-    (to_address_of_expr(char_pointer).object().id() == ID_index) &&
-    char_pointer.op0().op0().id() == ID_array)
-  {
-    // Do not replace constant arrays
-    return to_array_string_expr(
-      to_index_expr(to_address_of_expr(char_pointer).object()).array());
-  }
-  else if(char_pointer.id() == ID_address_of)
-  {
-    symbol_name = "char_array_of_address";
-  }
-  else if(char_pointer.id() == ID_if)
+
+  if(char_pointer.id() == ID_if)
   {
     const if_exprt &if_expr = to_if_expr(char_pointer);
     const array_string_exprt t =
       make_char_array_for_char_pointer(if_expr.true_case(), char_array_type);
     const array_string_exprt f =
       make_char_array_for_char_pointer(if_expr.false_case(), char_array_type);
-    array_typet array_type(
+    const array_typet array_type(
       char_array_type.subtype(),
       if_exprt(
         if_expr.cond(),
         to_array_type(t.type()).size(),
         to_array_type(f.type()).size()));
     return to_array_string_expr(if_exprt(if_expr.cond(), t, f, array_type));
   }
-  else if(char_pointer.id() == ID_symbol)
-    symbol_name = "char_array_symbol";
-  else if(char_pointer.id() == ID_member)
-    symbol_name = "char_array_member";
-  else if(
-    char_pointer.id() == ID_constant &&
-    to_constant_expr(char_pointer).get_value() == ID_NULL)
+  const bool is_constant_array =
+    char_pointer.id() == ID_address_of &&
+    (to_address_of_expr(char_pointer).object().id() == ID_index) &&
+    char_pointer.op0().op0().id() == ID_array;
+  if(is_constant_array)
   {
-    /// \todo Check if the case char_array_null occurs.
-    array_typet array_type(
-      char_array_type.subtype(),
-      from_integer(0, to_array_type(char_array_type).size().type()));
-    symbol_exprt array_sym = fresh_symbol("char_array_null", array_type);
-    return to_array_string_expr(array_sym);
+    return to_array_string_expr(
+      to_index_expr(to_address_of_expr(char_pointer).object()).array());
   }
-  else
-    symbol_name = "unknown_char_array";
-
-  array_string_exprt array_sym =
+  const std::string symbol_name = "char_array_" + id2string(char_pointer.id());
+  const auto array_sym =
     to_array_string_expr(fresh_symbol(symbol_name, char_array_type));
-  auto insert_result =
-    arrays_of_pointers.insert(std::make_pair(char_pointer, array_sym));
-  array_string_exprt result = to_array_string_expr(insert_result.first->second);
-  return result;
+  const auto insert_result =
+    arrays_of_pointers.insert({char_pointer, array_sym});
+  return  to_array_string_expr(insert_result.first->second);
 }
 
 void array_poolt::insert(

src/solvers/refinement/string_refinement_util.cpp

@@ -413,10 +413,15 @@ void string_dependenciest::for_each_dependency(
         stack.emplace_back(if_expr->true_case());
         stack.emplace_back(if_expr->false_case());
       }
-      else if(const auto string_node = node_at(to_array_string_expr(current)))
-        f(*string_node);
       else
-        UNREACHABLE;
+      {
+        const auto string_node = node_at(to_array_string_expr(current));
+        INVARIANT(
+          string_node,
+          "dependencies of the node should have been added to the graph at node creation "
+          + current.get().pretty());
+        f(*string_node);
+      }
     }
   }
 }

unit/Makefile

@@ -14,6 +14,7 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
        path_strategies.cpp \
+       solvers/refinement/array_pool/array_pool.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \

unit/solvers/refinement/array_pool/array_pool.cpp

@@ -0,0 +1,148 @@
+/*******************************************************************\
+
+ Module: Unit tests for array pool
+   solvers/refinement/string_constraint_generator.h
+
+ Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <solvers/refinement/string_constraint_generator.h>
+
+SCENARIO(
+  "array_pool", "[core][solvers][refinement][string_constraint_generator]")
+{
+  const std::size_t pointer_width = 16;
+  const auto char_type = unsignedbv_typet(8);
+  const auto length_type = signedbv_typet(32);
+  const auto pointer_type = pointer_typet(char_type, pointer_width);
+
+  GIVEN("An array pool")
+  {
+    symbol_generatort symbol_generator;
+    array_poolt pool(symbol_generator);
+
+    WHEN("Looking for a pointer symbol")
+    {
+      const symbol_exprt pointer("my_pointer", pointer_type);
+      const symbol_exprt pointer_length("my_pointer_length", length_type);
+      const array_string_exprt associated_array =
+        pool.find(pointer, pointer_length);
+
+      THEN("A second find give the same array")
+      {
+        const array_string_exprt second_lookup =
+          pool.find(pointer, pointer_length);
+
+        REQUIRE(second_lookup == associated_array);
+      }
+    }
+
+    WHEN("Looking for the address of the first element of a constant array")
+    {
+      const array_typet array_type(char_type, from_integer(3, length_type));
+      const exprt array = [array_type, char_type]{
+        array_exprt a(array_type);
+        a.operands().push_back(from_integer('f', char_type));
+        a.operands().push_back(from_integer('o', char_type));
+        a.operands().push_back(from_integer('o', char_type));
+        return a;
+      }();
+        const exprt first_element =
+          index_exprt(array, from_integer(0, length_type));
+      const exprt pointer = address_of_exprt(first_element, pointer_type);
+      const array_string_exprt associated_array =
+        pool.find(pointer, array_type.size());
+
+      THEN("The associated array should be the pointed array")
+      {
+        REQUIRE(associated_array == array);
+      }
+    }
+
+    WHEN("Looking for a null pointer")
+    {
+      const null_pointer_exprt null_pointer(pointer_type);
+      const symbol_exprt pointer_length("null_pointer_length", length_type);
+      const array_string_exprt associated_array =
+        pool.find(null_pointer, pointer_length);
+
+      THEN("`find` always gives the same array")
+      {
+        const symbol_exprt pointer_length2("null_pointer_length2", length_type);
+        const array_string_exprt second_lookup =
+          pool.find(null_pointer, pointer_length2);
+
+        REQUIRE(second_lookup == associated_array);
+      }
+    }
+
+    WHEN("Looking for an if-expression")
+    {
+      const exprt boolean_symbol = symbol_exprt("boolean", bool_typet());
+      const exprt true_case = symbol_exprt("pointer1", pointer_type);
+      const exprt false_case = symbol_exprt("pointer2", pointer_type);
+      const exprt if_expr = if_exprt(boolean_symbol, true_case, false_case);
+      const symbol_exprt pointer_length("pointer_length", length_type);
+
+      const array_string_exprt associated_array =
+        pool.find(if_expr, pointer_length);
+
+      THEN("Arrays associated to the subexpressions are the subexpressions of "
+           "the associated array")
+      {
+        const symbol_exprt pointer_length1("pointer_length1", length_type);
+        const array_string_exprt associated_to_true =
+          pool.find(true_case, pointer_length1);
+        const symbol_exprt pointer_length2("pointer_length2", length_type);
+        const array_string_exprt associated_to_false =
+          pool.find(false_case, pointer_length2);
+
+        const typet recomposed_type = array_typet(
+          char_type, if_exprt(boolean_symbol, pointer_length, pointer_length));
+        const exprt recomposed_array = if_exprt(
+          boolean_symbol,
+          associated_to_true,
+          associated_to_false,
+          recomposed_type);
+
+        REQUIRE(associated_array == recomposed_array);
+      }
+    }
+
+    WHEN("Looking for two pointer symbols")
+    {
+      const exprt true_case = symbol_exprt("pointer1", pointer_type);
+      const symbol_exprt pointer_length1("pointer_length1", length_type);
+      const exprt false_case = symbol_exprt("pointer2", pointer_type);
+      const symbol_exprt pointer_length2("pointer_length2", length_type);
+
+      const array_string_exprt associated_to_true =
+        pool.find(true_case, pointer_length1);
+      const array_string_exprt associated_to_false =
+        pool.find(false_case, pointer_length2);
+
+      THEN("Looking for an if-expression containing these two symbols")
+      {
+        const exprt boolean_symbol = symbol_exprt("boolean", bool_typet());
+        const exprt if_expr = if_exprt(boolean_symbol, true_case, false_case);
+        const symbol_exprt pointer_length("pointer_length", length_type);
+        const array_string_exprt associated_array =
+          pool.find(if_expr, pointer_length);
+
+        const typet recomposed_type = array_typet(
+          char_type,
+          if_exprt(boolean_symbol, pointer_length1, pointer_length2));
+        const exprt recomposed_array = if_exprt(
+          boolean_symbol,
+          associated_to_true,
+          associated_to_false,
+          recomposed_type);
+
+        REQUIRE(associated_array == recomposed_array);
+      }
+    }
+  }
+}