SMT back-end: report too-many-addressed-objects

Fail generation of the SMT encoding with a meaningful error message
rather than generating invalid SMT-LIB output. The behaviour now matches
that of the SAT back-end.

Fixes: #7623

Author: tautschnig

regression/cbmc/address_space_size_limit1/test.desc

@@ -1,4 +1,4 @@
-CORE thorough-paths broken-smt-backend
+CORE thorough-paths
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects

src/solvers/smt2/smt2_conv.cpp

@@ -782,12 +782,21 @@ void smt2_convt::convert_address_of_rec(
     expr.id() == ID_symbol || expr.is_constant() ||
     expr.id() == ID_string_constant || expr.id() == ID_label)
   {
-    out
-      << "(concat (_ bv"
-      << pointer_logic.add_object(expr) << " "
-      << config.bv_encoding.object_bits << ")"
-      << " (_ bv0 "
-      << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
+    const std::size_t object_bits = config.bv_encoding.object_bits;
+    const std::size_t max_objects = std::size_t(1) << object_bits;
+    const mp_integer object_id = pointer_logic.add_object(expr);
+
+    if(object_id >= max_objects)
+    {
+      throw analysis_exceptiont{
+        "too many addressed objects: maximum number of objects is set to 2^n=" +
+        std::to_string(max_objects) +
+        " (with n=" + std::to_string(object_bits) + "); " +
+        "use the `--object-bits n` option to increase the maximum number"};
+    }
+
+    out << "(concat (_ bv" << object_id << " " << object_bits << ")"
+        << " (_ bv0 " << boolbv_width(result_type) - object_bits << "))";
   }
   else if(expr.id()==ID_index)
   {

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -854,15 +854,6 @@ static smt_termt convert_expr_to_smt(
   }
 }
 
-#ifndef CPROVER_INVARIANT_DO_NOT_CHECK
-static mp_integer power2(unsigned exponent)
-{
-  mp_integer result;
-  result.setPower2(exponent);
-  return result;
-}
-#endif
-
 /// \details
 /// This conversion constructs a bit vector representation of the memory
 /// address. This address is composed of 2 concatenated bit vector components.
@@ -884,16 +875,23 @@ static smt_termt convert_expr_to_smt(
     object != object_map.end(),
     "Objects should be tracked before converting their address to SMT terms");
   const std::size_t object_id = object->second.unique_id;
-  INVARIANT(
-    object_id < power2(config.bv_encoding.object_bits),
-    "There should be sufficient bits to encode unique object identifier.");
+  const std::size_t object_bits = config.bv_encoding.object_bits;
+  const std::size_t max_objects = std::size_t(1) << object_bits;
+  if(object_id >= max_objects)
+  {
+    throw analysis_exceptiont{
+      "too many addressed objects: maximum number of objects is set to 2^n=" +
+      std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
+      "); " +
+      "use the `--object-bits n` option to increase the maximum number"};
+  }
   const smt_termt object_bit_vector =
-    smt_bit_vector_constant_termt{object_id, config.bv_encoding.object_bits};
+    smt_bit_vector_constant_termt{object_id, object_bits};
   INVARIANT(
-    type->get_width() > config.bv_encoding.object_bits,
+    type->get_width() > object_bits,
     "Pointer should be wider than object_bits in order to allow for offset "
     "encoding.");
-  const size_t offset_bits = type->get_width() - config.bv_encoding.object_bits;
+  const size_t offset_bits = type->get_width() - object_bits;
   if(
     const auto symbol =
       expr_try_dynamic_cast<symbol_exprt>(address_of.object()))

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1525,23 +1525,17 @@ TEST_CASE(
       const address_of_exprt address_of_foo{foo};
       track_expression_objects(address_of_foo, ns, test.object_map);
       test.object_map.at(foo).unique_id = 256;
-      REQUIRE_THROWS_MATCHES(
-        test.convert(address_of_exprt{foo}),
-        invariant_failedt,
-        invariant_failure_containing("There should be sufficient bits to "
-                                     "encode unique object identifier."));
+      REQUIRE_THROWS_AS(
+        test.convert(address_of_exprt{foo}), analysis_exceptiont);
     }
     SECTION("Pointer should be wide enough to encode offset")
     {
       config.bv_encoding.object_bits = 64;
       const address_of_exprt address_of_foo{foo};
       track_expression_objects(address_of_foo, ns, test.object_map);
       test.object_map.at(foo).unique_id = 256;
-      REQUIRE_THROWS_MATCHES(
-        test.convert(address_of_exprt{foo}),
-        invariant_failedt,
-        invariant_failure_containing("Pointer should be wider than object_bits "
-                                     "in order to allow for offset encoding."));
+      REQUIRE_THROWS_AS(
+        test.convert(address_of_exprt{foo}), analysis_exceptiont);
     }
   }
   SECTION("Comparison of address of operations.")