From 257088b57304303aff6de100ba6e14b71a2996c0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 27 May 2026 09:45:12 +0000 Subject: [PATCH] Handle empty type in incremental SMT2 decision procedure Skip zero-width-typed leaves (typically void) in gather_dependent_expressions so that we never attempt to call convert_type_to_smt_sort on them, which would hit UNIMPLEMENTED_FEATURE. Handle the only top-level consumer that could legitimately involve such a leaf -- equality of two zero-width-typed operands -- by short-circuiting set_to: for value == true the equality is vacuously satisfied (no command emitted); for value == false we send `(assert false)` directly. This matches the end-to-end behaviour of the non-incremental SMT2 backend, which converts equal_exprt over a zero-width type to true_exprt and then negates. Both filter sites use the shared is_zero_width predicate (now exposed via util/pointer_offset_size.h) rather than a narrow ID_empty check, so they stay correct even if struct_encoding's pre-pass ever stops normalising other zero-width forms. The set_to short-circuit handles only the top-level equality. Nested cases such as and_exprt{equal_exprt{x_void, y_void}, other} would still reach convert_expr_to_smt and trip UNIMPLEMENTED_FEATURE; CBMC's GOTO programs do not produce such nested shapes today, but pushing the short-circuit into the equal_exprt overload of convert_expr_to_smt (mirroring smt2_conv.cpp's structure more closely) is left as a follow-up. Add a focused unit test in unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp covering both set_to(equal_exprt{void_x, void_y}, true) (no extra commands sent) and set_to(..., false) (a single `(assert false)`). Remove the no-new-smt exclusion tag from havoc_slice_checks and memset_null regression tests since they now pass with the incremental SMT2 backend. Fixes: #8077 Co-authored-by: Kiro --- regression/cbmc/havoc_slice_checks/test.desc | 2 +- regression/cbmc/memset_null/test.desc | 2 +- .../smt2_incremental_decision_procedure.cpp | 40 +++++++++++++++++-- .../smt2_incremental_decision_procedure.cpp | 32 +++++++++++++++ 4 files changed, 70 insertions(+), 6 deletions(-) diff --git a/regression/cbmc/havoc_slice_checks/test.desc b/regression/cbmc/havoc_slice_checks/test.desc index 42b6f11e2c3..b5d12522d0a 100644 --- a/regression/cbmc/havoc_slice_checks/test.desc +++ b/regression/cbmc/havoc_slice_checks/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^\[main\.assertion\.\d+\] line 9 assertion havoc_slice W_OK.*: FAILURE$ diff --git a/regression/cbmc/memset_null/test.desc b/regression/cbmc/memset_null/test.desc index 6984ae9e29d..bef94363c5e 100644 --- a/regression/cbmc/memset_null/test.desc +++ b/regression/cbmc/memset_null/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^\[main.precondition_instance.1\] line .* memset destination region writeable: FAILURE$ diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 2817ba012fe..e85a0b766ef 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -6,6 +6,7 @@ #include #include #include +#include #include #include #include @@ -71,7 +72,8 @@ get_problem_messages(const smt_responset &response) /// returned by this`gather_dependent_expressions` function. /// \details `symbol_exprt`, `array_exprt` and `nondet_symbol_exprt` add /// dependant expressions. -static std::vector gather_dependent_expressions(const exprt &root_expr) +static std::vector +gather_dependent_expressions(const exprt &root_expr, const namespacet &ns) { std::vector dependent_expressions; @@ -89,7 +91,13 @@ static std::vector gather_dependent_expressions(const exprt &root_expr) can_cast_expr(expr_node) || can_cast_expr(expr_node)) { - dependent_expressions.push_back(expr_node); + // Skip zero-width-typed leaves: they have no SMT representation + // (convert_type_to_smt_sort would hit UNIMPLEMENTED_FEATURE on + // empty_typet), and the only top-level consumer that could + // legitimately involve such a leaf -- equality of two void-typed + // operands -- is short-circuited in `set_to` below. + if(!is_zero_width(expr_node.type(), ns)) + dependent_expressions.push_back(expr_node); } // The decision procedure does not depend on the values inside address of // code typed expressions. We can build the address without knowing the @@ -193,7 +201,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions( std::stack to_be_defined; const auto push_dependencies_needed = [&](const exprt &expr) { bool result = false; - for(const auto &dependency : gather_dependent_expressions(expr)) + for(const auto &dependency : gather_dependent_expressions(expr, ns)) { if(!seen_expressions.insert(dependency).second) continue; @@ -598,7 +606,7 @@ exprt smt2_incremental_decision_proceduret::get(const exprt &expr) const return identifier_descriptor; } const exprt lowered = lower(expr); - if(gather_dependent_expressions(lowered).empty()) + if(gather_dependent_expressions(lowered, ns).empty()) { INVARIANT( objects_are_already_tracked(lowered, object_map), @@ -653,6 +661,30 @@ void smt2_incremental_decision_proceduret::set_to( << in_expr.pretty(2, 0) << messaget::eom; }); const exprt lowered_expr = lower(in_expr); + // Equality of two zero-width-typed (typically void) operands is + // vacuously true. For value == true we therefore have nothing to + // assert; for value == false we send `(assert false)` directly, + // matching the end-to-end behaviour of the non-incremental SMT2 + // backend (smt2_conv.cpp), which converts `equal_exprt` over a + // zero-width type to `true_exprt` and then negates. + // + // Limitation: only the *top-level* equality is intercepted here. + // A nested case such as `set_to(and_exprt{equal_exprt{x_void, + // y_void}, other}, true)` would still descend into + // `convert_expr_to_smt`, which has no handling for void operands + // and would trip UNIMPLEMENTED_FEATURE in `convert_type_to_smt_sort`. + // CBMC's GOTO programs do not produce such nested shapes today, + // but a future refactor pushing this short-circuit into the + // `equal_exprt` overload of `convert_expr_to_smt` would handle the + // nested case for free. + if( + lowered_expr.id() == ID_equal && + is_zero_width(to_equal_expr(lowered_expr).lhs().type(), ns)) + { + if(!value) + solver_process->send(smt_assert_commandt{smt_bool_literal_termt{false}}); + return; + } PRECONDITION(can_cast_type(lowered_expr.type())); define_dependent_functions(lowered_expr); diff --git a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 5fd0a855875..c17145f6361 100644 --- a/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -1136,6 +1136,38 @@ TEST_CASE( CHECK(test.sent_commands == expected_get_commands); } +TEST_CASE( + "smt2_incremental_decision_proceduret set_to over empty type", + "[core][smt2_incremental]") +{ + // Equality of two empty-typed (void) operands is vacuously true. The + // decision procedure should therefore short-circuit set_to without + // descending into convert_expr_to_smt (which has no SMT sort for + // empty_typet) and without declaring the void-typed leaves: for + // value == true nothing extra is sent; for value == false a single + // `(assert false)` is sent. + auto test = decision_procedure_test_environmentt::make(); + const symbolt x{"x", empty_typet{}, ID_C}; + test.symbol_table.insert(x); + const symbolt y{"y", empty_typet{}, ID_C}; + test.symbol_table.insert(y); + + INFO("Sanity checking decision procedure and flushing size definitions"); + test.mock_responses.push_front(smt_check_sat_responset{smt_sat_responset{}}); + CHECK(test.procedure() == decision_proceduret::resultt::D_SATISFIABLE); + test.sent_commands.clear(); + + INFO("set_to(equal_exprt{x, y}, true) sends no extra commands"); + test.procedure.set_to(equal_exprt{x.symbol_expr(), y.symbol_expr()}, true); + CHECK(test.sent_commands == std::vector{}); + + INFO("set_to(equal_exprt{x, y}, false) sends a single `(assert false)`"); + test.procedure.set_to(equal_exprt{x.symbol_expr(), y.symbol_expr()}, false); + const std::vector expected_commands{ + smt_assert_commandt{smt_bool_literal_termt{false}}}; + CHECK(test.sent_commands == expected_commands); +} + TEST_CASE( "smt2_incremental_decision_proceduret getting value of struct-symbols with " "value in the symbol table",