Incremental SMT2: Add size limit to array element retrieval

regression/cbmc/pointer-offset-01/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --no-malloc-may-fail --trace
 ^\s*ub.*=(\(char \*\)&)?dynamic_object \+ \d+

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -26,6 +26,12 @@
 #include <stack>
 #include <unordered_set>
 
+/// Maximum number of array elements to retrieve from the solver during
+/// trace generation. Arrays larger than this threshold will not have
+/// their values retrieved element by element, as doing so would be
+/// prohibitively slow or cause out-of-memory issues.
+static const std::size_t MAX_TRACE_ARRAY_SIZE = 1000;
+
 /// Issues a command to the solving process which is expected to optionally
 /// return a success status followed by the actual response of interest.
 static smt_responset get_response_to_command(
@@ -438,6 +444,13 @@ std::optional<exprt> smt2_incremental_decision_proceduret::get_expr(
   INVARIANT(
     size,
     "Size of array must be convertible to std::size_t for getting array value");
+  if(*size > MAX_TRACE_ARRAY_SIZE)
+  {
+    log.warning() << "cannot retrieve array of size " << *size
+                  << " from SMT solver due to size limit of "
+                  << MAX_TRACE_ARRAY_SIZE << messaget::eom;
+    return {};
+  }
   std::vector<exprt> elements;
   const auto index_type = type.index_type();
   elements.reserve(*size);

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -1197,3 +1197,38 @@ TEST_CASE(
 
   CHECK(test.sent_commands == expected_commands);
 }
+
+TEST_CASE(
+  "smt2_incremental_decision_proceduret get_expr returns empty for large "
+  "arrays.",
+  "[core][smt2_incremental]")
+{
+  auto test = decision_procedure_test_environmentt::make();
+  const auto index_type = signedbv_typet{32};
+  const auto value_type = signedbv_typet{8};
+  // Create an array type with a size exceeding MAX_TRACE_ARRAY_SIZE (1000).
+  const auto large_array_type =
+    array_typet{value_type, from_integer(1001, index_type)};
+  const symbolt large_array = make_test_symbol("large_array", large_array_type);
+  const smt_identifier_termt large_array_term{
+    "large_array",
+    smt_array_sortt{smt_bit_vector_sortt{32}, smt_bit_vector_sortt{8}}};
+
+  test.sent_commands.clear();
+  test.procedure.set_to(
+    equal_exprt{large_array.symbol_expr(), large_array.symbol_expr()}, true);
+
+  // Solve to put procedure in suitable state.
+  test.mock_responses.push_back(smt_check_sat_responset{smt_sat_responset{}});
+  test.procedure();
+
+  // Mock the response for getting the array size.
+  test.mock_responses.push_back(smt_get_value_responset{
+    {{{smt_bit_vector_constant_termt{1001, 32}},
+      smt_bit_vector_constant_termt{1001, 32}}}});
+
+  // get_expr should return empty optional for the large array.
+  const auto result =
+    test.procedure.get_expr(large_array_term, large_array_type);
+  REQUIRE_FALSE(result.has_value());
+}