From 9fccd20468c0c672b79a8536685828e386c829a5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 26 May 2026 09:30:41 +0000 Subject: [PATCH] boolbv_let: pass lowered value to record_array_let_binding convert_let computes 'lowered_value' (the let's bound expression with byte_update / byte_extract operators rewritten away by lower_byte_operators) but then dropped it on the floor and passed the *un*-lowered 'pair.second' to record_array_let_binding. If the let-bound array value happens to contain a byte_update, the array theory's collect_arrays will see it and trip DATA_INVARIANT(false, "byte_update should be removed before collect_arrays") Fix: pass 'lowered_value' so the value handed to the array theory matches the lowering already done at the call site. The bug was introduced by commit 14105d503d7 ("Connect let-bound arrays to originals in array theory"), which added the byte-operator lowering computation but forgot to thread the result through to record_array_let_binding. That commit shipped in cbmc-6.9.0, so this is a release-shipped latent bug. No standard CBMC entry point currently funnels a byte-operator-bearing array expression into an array-typed let_exprt (SMT2 input has no byte_update; value_set_dereference produces pointer-typed lets; goto-symex's lift_let hoists lets out before they reach boolbvt), so there is no end-to-end regression test. The fix is pinned instead by a unit test in unit/solvers/flattening/boolbv.cpp that drives boolbvt directly with a let binding an unbounded-array symbol to a byte_update expression: it trips the DATA_INVARIANT above without this change and converts cleanly with it. While here, document record_array_let_binding's now load-bearing precondition (its value must be free of byte_update operators) in arrays.h. Co-authored-by: Kiro --- src/solvers/flattening/arrays.h | 2 ++ src/solvers/flattening/boolbv_let.cpp | 2 +- unit/solvers/flattening/boolbv.cpp | 50 +++++++++++++++++++++++++++ 3 files changed, 53 insertions(+), 1 deletion(-) diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index 1d2c4caccef..1ebb1a457cb 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -57,6 +57,8 @@ class arrayst:public equalityt /// array theory. For unbounded-array-typed bindings this connects the /// two expressions in the union-find so that element-wise constraints /// propagate correctly. + /// \pre \p value must be free of byte_update operators; lower them at the + /// call site (collect_arrays otherwise fails a DATA_INVARIANT). void record_array_let_binding(const symbol_exprt &symbol, const exprt &value); protected: diff --git a/src/solvers/flattening/boolbv_let.cpp b/src/solvers/flattening/boolbv_let.cpp index fb42d92cee9..e9fe4632967 100644 --- a/src/solvers/flattening/boolbv_let.cpp +++ b/src/solvers/flattening/boolbv_let.cpp @@ -80,7 +80,7 @@ bvt boolbvt::convert_let(const let_exprt &expr) const exprt lowered_value = has_byte_operator(pair.second) ? lower_byte_operators(pair.second, ns) : pair.second; - record_array_let_binding(pair.first, pair.second); + record_array_let_binding(pair.first, lowered_value); } } diff --git a/unit/solvers/flattening/boolbv.cpp b/unit/solvers/flattening/boolbv.cpp index 9f0bde9234a..58266a42a89 100644 --- a/unit/solvers/flattening/boolbv.cpp +++ b/unit/solvers/flattening/boolbv.cpp @@ -11,6 +11,9 @@ Author: Daniel Kroening #include #include +#include +#include +#include #include #include #include @@ -18,6 +21,7 @@ Author: Daniel Kroening #include #include #include +#include #include SCENARIO("boolbvt", "[core][solvers][flattening][boolbvt]") @@ -46,3 +50,49 @@ SCENARIO("boolbvt", "[core][solvers][flattening][boolbvt]") } } } + +SCENARIO( + "boolbvt convert_let with a byte_update in an unbounded array value", + "[core][solvers][flattening][boolbvt]") +{ + // A let-bound symbol of unbounded array type whose value still contains a + // byte_update operator must have that operator lowered before it is handed + // to the array theory: boolbvt::convert_let computes a lowered value but, + // before the fix, passed the un-lowered value to record_array_let_binding, + // tripping `DATA_INVARIANT(false, "byte_update should be removed before + // collect_arrays")` in collect_arrays. This pins that fix. + GIVEN("a let binding an unbounded array to a byte_update expression") + { + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + satcheckt satcheck{null_message_handler}; + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + boolbvt boolbv{ns, satcheck, null_message_handler}; + + const unsignedbv_typet u8{8}; + // non-constant size => unbounded array + const array_typet array_type{u8, symbol_exprt{"N", size_type()}}; + const symbol_exprt a{"a", array_type}; + const symbol_exprt x{"x", u8}; + + const symbol_exprt b{"b", array_type}; + const exprt array_value = byte_update_exprt{ + ID_byte_update_little_endian, + b, + from_integer(0, c_index_type()), + x, + /* bits_per_byte */ 8}; + + const let_exprt let{ + a, + array_value, + equal_exprt{index_exprt{a, from_integer(0, c_index_type())}, x}}; + + THEN("the let converts without tripping a DATA_INVARIANT") + { + boolbv << let; + REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE); + } + } +}