Handle empty type in incremental SMT2 decision procedure

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$

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$

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -6,6 +6,7 @@
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/pointer_offset_size.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
@@ -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<exprt> gather_dependent_expressions(const exprt &root_expr)
+static std::vector<exprt>
+gather_dependent_expressions(const exprt &root_expr, const namespacet &ns)
 {
   std::vector<exprt> dependent_expressions;
 
@@ -89,7 +91,13 @@ static std::vector<exprt> gather_dependent_expressions(const exprt &root_expr)
       can_cast_expr<nondet_symbol_exprt>(expr_node) ||
       can_cast_expr<string_constantt>(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<exprt> 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<bool_typet>(lowered_expr.type()));
 
   define_dependent_functions(lowered_expr);

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<smt_commandt>{});
+
+  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<smt_commandt> 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",