goto-symex: support struct-keyed arrays (maps) in value materialisation

src/goto-symex/field_sensitivity.cpp

@@ -290,6 +290,21 @@ exprt field_sensitivityt::apply(
   return expr;
 }
 
+#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
+/// True if the array index type permits field-sensitive element enumeration
+/// via from_integer(i, index_type). Arrays keyed by a non-scalar type (e.g.
+/// Strata's `Map Ref _` heap, indexed by a struct reference) cannot be
+/// enumerated this way and must be handled monolithically. Boolean index types
+/// are deliberately excluded: from_integer(i, bool) collapses every i > 1 to
+/// `true`, so enumerating i = 0..size-1 would produce duplicate indices.
+static bool is_enumerable_array_index_type(const typet &index_type)
+{
+  const irep_idt &id = index_type.id();
+  return id == ID_unsignedbv || id == ID_signedbv || id == ID_bv ||
+         id == ID_integer || id == ID_c_enum || id == ID_c_enum_tag;
+}
+#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
+
 exprt field_sensitivityt::get_fields(
   const namespacet &ns,
   goto_symex_statet &state,
@@ -350,6 +365,13 @@ exprt field_sensitivityt::get_fields(
       return ssa_expr;
 
     const array_typet &type = to_array_type(ssa_expr.type());
+    // Element enumeration below builds integer indices via from_integer(i,
+    // index_type), so it only applies to arrays with an enumerable index type;
+    // arrays keyed by a non-scalar type (e.g. a map keyed by a struct
+    // reference, as in Strata's heap model `Map Ref _`) are treated
+    // monolithically.
+    if(!is_enumerable_array_index_type(type.index_type()))
+      return ssa_expr;
     const std::size_t array_size = numeric_cast_v<std::size_t>(mp_array_size);
 
     array_exprt::operandst elements;
@@ -628,7 +650,12 @@ bool field_sensitivityt::is_divisible(
     numeric_cast_v<mp_integer>(to_constant_expr(
       to_array_type(expr.type()).size())) <= max_field_sensitivity_array_size)
   {
-    return true;
+    // Only field-decompose arrays whose index type is enumerable (element
+    // enumeration builds from_integer(i, index_type)). Arrays keyed by a
+    // non-scalar type (e.g. Strata's `Map Ref _` heap, indexed by a struct
+    // reference) must be handled monolithically.
+    if(is_enumerable_array_index_type(to_array_type(expr.type()).index_type()))
+      return true;
   }
 #endif
 

src/pointer-analysis/value_set.cpp

@@ -1592,9 +1592,19 @@ void value_sett::assign(
     }
     else
     {
+      // For array assignments the indices were abstracted to
+      // exprt(ID_unknown, c_index_type()) above, so the array's index type
+      // does not affect materialisation here. We therefore require only the
+      // element types to match and intentionally ignore both the array size
+      // and the index type (the latter being what enables struct-keyed
+      // "map" arrays to be assigned).
       DATA_INVARIANT(
-        rhs.type() == lhs.type(),
-        "value_sett::assign types should match, got: "
+        rhs.type() == lhs.type() ||
+          (rhs.type().id() == ID_array && lhs.type().id() == ID_array &&
+           to_array_type(rhs.type()).element_type() ==
+             to_array_type(lhs.type()).element_type()),
+        "value_sett::assign types should match (for arrays, modulo array size "
+        "and index type, as array indices are abstracted here), got: "
         "rhs.type():\n" +
           rhs.type().pretty() + "\n" + "type:\n" + lhs.type().pretty());
 

unit/Makefile

@@ -82,6 +82,7 @@ SRC += analyses/ai/ai.cpp \
        goto-symex/apply_condition.cpp \
        goto-symex/complexity_limiter.cpp \
        goto-symex/expr_skeleton.cpp \
+       goto-symex/field_sensitivity.cpp \
        goto-symex/goto_symex_state.cpp \
        goto-symex/ssa_equation.cpp \
        goto-symex/is_constant.cpp \

unit/goto-symex/field_sensitivity.cpp

@@ -0,0 +1,104 @@
+/*******************************************************************\
+
+Module: Unit tests for field_sensitivityt
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for field_sensitivityt handling of arrays whose index type is
+/// not enumerable (e.g. struct-keyed "map" arrays as used by the Strata heap
+/// model `Map Ref _`). Such arrays must be treated monolithically: element
+/// enumeration builds indices via from_integer(i, index_type), which is only
+/// defined for integer/bitvector/enum index types.
+
+#include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/invariant.h>
+#include <util/magic.h>
+#include <util/namespace.h>
+#include <util/ssa_expr.h>
+#include <util/std_expr.h>
+#include <util/std_types.h>
+#include <util/symbol_table.h>
+
+#include <goto-programs/goto_program.h>
+
+#include <goto-symex/field_sensitivity.h>
+#include <goto-symex/goto_symex_state.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO(
+  "field sensitivity treats non-enumerable array index types monolithically",
+  "[core][goto-symex][field_sensitivity]")
+{
+  // Turn invariant violations into exceptions: without the enumerable-index
+  // guard, get_fields aborts inside from_integer (PRECONDITION) when it tries
+  // to build a struct-typed index constant. Throwing mode turns a regression
+  // into a clean test failure instead of killing the test binary.
+  const cbmc_invariants_should_throwt invariants_throw;
+
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+
+  const signedbv_typet int_type{32};
+
+  // A struct type used as an array index ("map key"), as produced by front
+  // ends that model heaps as struct-keyed maps.
+  struct_typet key_type{{{"id", int_type}}};
+  key_type.set_tag("key");
+
+  const field_sensitivityt field_sensitivity{
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE, false, irep_idt{}};
+
+  // Minimal symex state, required by the get_fields interface.
+  std::list<goto_programt::instructiont> target;
+  symex_targett::sourcet source{"fun", target.begin()};
+  guard_managert guard_manager;
+  std::size_t count = 0;
+  auto fresh_name = [&count](const irep_idt &) { return count++; };
+  goto_symex_statet state{
+    source,
+    DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE,
+    false,
+    irep_idt{},
+    guard_manager,
+    fresh_name};
+
+  GIVEN("a small array with an integer index type")
+  {
+    const array_typet array_type{int_type, from_integer(2, int_type)};
+    const ssa_exprt array_ssa{symbol_exprt{"some_array", array_type}};
+
+    THEN("it is divisible and get_fields enumerates its elements")
+    {
+      REQUIRE(field_sensitivity.is_divisible(array_ssa, true));
+
+      exprt fields;
+      REQUIRE_NOTHROW(
+        fields = field_sensitivity.get_fields(ns, state, array_ssa, true));
+      REQUIRE(fields.id() == ID_array);
+      REQUIRE(fields.operands().size() == 2);
+    }
+  }
+
+  GIVEN("a small array with a struct (map-key) index type")
+  {
+    array_typet map_type{int_type, from_integer(2, int_type)};
+    map_type.index_type_nonconst() = key_type;
+    const ssa_exprt map_ssa{symbol_exprt{"some_map", map_type}};
+
+    THEN("it is not divisible and get_fields leaves it unchanged")
+    {
+      REQUIRE(!field_sensitivity.is_divisible(map_ssa, true));
+
+      // Without the enumerable-index-type guard this aborts in
+      // from_integer(i, key_type).
+      exprt fields;
+      REQUIRE_NOTHROW(
+        fields = field_sensitivity.get_fields(ns, state, map_ssa, true));
+      REQUIRE(fields == map_ssa);
+    }
+  }
+}

unit/pointer-analysis/value_set.cpp

@@ -10,6 +10,8 @@ Author: Diffblue Ltd.
 /// Unit tests for value_sett
 
 #include <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/invariant.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/symbol_table.h>
@@ -433,3 +435,52 @@ SCENARIO(
     }
   }
 }
+
+TEST_CASE(
+  "value_sett::assign accepts arrays differing in size and index type",
+  "[core][pointer-analysis][value_set]")
+{
+  // Turn invariant violations into exceptions so that a regression of the
+  // relaxed type check shows up as a clean test failure.
+  const cbmc_invariants_should_throwt invariants_throw;
+
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  value_sett value_set;
+
+  const signedbv_typet int_type{32};
+
+  // A struct type used as an array index ("map key").
+  struct_typet key_type{{{"id", int_type}}};
+  key_type.set_tag("key");
+
+  // Two arrays sharing the element type: one indexed by the struct key (a
+  // "map", as used by the Strata heap model), one by the default index type.
+  // The sizes differ as well: the index-type annotation (#index_type) is an
+  // irept comment and hence invisible to type equality, so the size
+  // difference is what exercises the relaxed type check.
+  array_typet map_type{int_type, from_integer(2, int_type)};
+  map_type.index_type_nonconst() = key_type;
+  const array_typet array_type{int_type, from_integer(3, int_type)};
+
+  const symbol_exprt map_lhs{"map_lhs", map_type};
+  const symbol_exprt array_rhs{"array_rhs", array_type};
+
+  SECTION("differing size and index type, same element type")
+  {
+    // Array indices are abstracted to unknown on this path, so the index type
+    // does not affect materialisation and the assignment must be accepted.
+    REQUIRE_NOTHROW(value_set.assign(map_lhs, array_rhs, ns, false, false));
+  }
+
+  SECTION("differing element types are still rejected")
+  {
+    const array_typet other_element_type{
+      unsignedbv_typet{8}, from_integer(2, int_type)};
+    const symbol_exprt bytes_rhs{"bytes_rhs", other_element_type};
+
+    REQUIRE_THROWS_AS(
+      value_set.assign(map_lhs, bytes_rhs, ns, false, false),
+      invariant_failedt);
+  }
+}