From abda36564322dfba788c8411f060821810b9fa35 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jun 2026 20:06:40 +0000 Subject: [PATCH] goto-symex: support struct-keyed arrays (maps) in value materialisation Field-sensitivity and the value-set assume array indices are integer-typed. For arrays keyed by a struct (used to model heaps as Map Ref Struct), the from_integer-based index construction aborts. Gate is_divisible/get_fields to integer/bitvector/enum index types, and relax value_sett::assign array type-equality to allow arrays with the same element type but differing size (unbounded heap maps). Co-authored-by: Kiro --- src/goto-symex/field_sensitivity.cpp | 29 +++++++++++++++++++++++++++- src/goto-symex/field_sensitivity.h | 4 ++++ src/pointer-analysis/value_set.cpp | 7 +++++-- 3 files changed, 37 insertions(+), 3 deletions(-) diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index 9c657af5678..5de851fa653 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -350,6 +350,21 @@ 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). If the index type is not an integer/bitvector/enum (e.g. a + // map keyed by a struct reference, as in Strata's heap model `Map Ref _`), + // we cannot enumerate elements this way; treat the array monolithically. + { + const typet &idx_t = type.index_type(); + if( + idx_t.id() != ID_unsignedbv && idx_t.id() != ID_signedbv && + idx_t.id() != ID_bv && idx_t.id() != ID_integer && + idx_t.id() != ID_c_enum && idx_t.id() != ID_c_enum_tag && + idx_t.id() != ID_c_bool && idx_t.id() != ID_bool) + { + return ssa_expr; + } + } const std::size_t array_size = numeric_cast_v(mp_array_size); array_exprt::operandst elements; @@ -628,7 +643,19 @@ 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 an integer/bitvector/enum + // (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. + const typet &idx_t = to_array_type(expr.type()).index_type(); + if( + idx_t.id() == ID_unsignedbv || idx_t.id() == ID_signedbv || + idx_t.id() == ID_bv || idx_t.id() == ID_integer || + idx_t.id() == ID_c_enum || idx_t.id() == ID_c_enum_tag || + idx_t.id() == ID_c_bool || idx_t.id() == ID_bool) + { + return true; + } } #endif diff --git a/src/goto-symex/field_sensitivity.h b/src/goto-symex/field_sensitivity.h index 12606321ce0..b394a8ee158 100644 --- a/src/goto-symex/field_sensitivity.h +++ b/src/goto-symex/field_sensitivity.h @@ -204,6 +204,10 @@ class field_sensitivityt [[nodiscard]] bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const; + /// Whether field sensitivity is currently enabled (can be temporarily + /// disabled for quantifier bodies to preserve algebraic structure). + bool enabled = true; + private: const std::size_t max_field_sensitivity_array_size; diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index aad9ae75f69..3b16285978b 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -1593,8 +1593,11 @@ void value_sett::assign( else { 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 (modulo array size), got: " "rhs.type():\n" + rhs.type().pretty() + "\n" + "type:\n" + lhs.type().pretty());