diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 9c657af5678..abbc0de7d71 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/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(mp_array_size); array_exprt::operandst elements; @@ -628,7 +650,12 @@ bool field_sensitivityt::is_divisible( numeric_cast_v(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 diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index aad9ae75f69..825d476afaf 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/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()); diff --git a/unit/Makefile b/unit/Makefile index d4971c89bba..9e55c603f28 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/goto-symex/field_sensitivity.cpp b/unit/goto-symex/field_sensitivity.cpp new file mode 100644 index 00000000000..2b1162bd726 --- /dev/null +++ b/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 +#include +#include +#include +#include +#include +#include +#include +#include + +#include + +#include +#include +#include + +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 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); + } + } +} diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp index e15b29b6920..bf12859a2a0 100644 --- a/unit/pointer-analysis/value_set.cpp +++ b/unit/pointer-analysis/value_set.cpp @@ -10,6 +10,8 @@ Author: Diffblue Ltd. /// Unit tests for value_sett #include +#include +#include #include #include #include @@ -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); + } +}