Add support for dynamic object sizes in old smt decision procedure

regression/cbmc/Malloc11/slice-formula.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend new-smt-backend
+CORE new-smt-backend
 main.c
 --pointer-check --slice-formula
 ^EXIT=0$

regression/cbmc/Malloc11/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend new-smt-backend
+CORE new-smt-backend
 main.c
 --pointer-check
 ^EXIT=0$

regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE smt-backend new-smt-backend
 original_repro.c
 --smt2
 ^EXIT=0$

regression/cbmc/pointer-predicates/at_bounds1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend new-smt-backend
+CORE new-smt-backend
 at_bounds1.c
 --pointer-primitive-check --malloc-fail-null
 ^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(q \+ (\(signed (long (long )?)?int\))?1, (\(unsigned (long (long )?)?int\))?0\): FAILURE$

regression/cbmc/simplify-array-size/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --malloc-may-fail --malloc-fail-null
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c

@@ -0,0 +1,89 @@
+// Code presented in https://github.com/diffblue/cbmc/issues/7690
+
+// clang-format off
+
+#include <stdlib.h>
+#include <stdint.h>
+
+extern size_t __CPROVER_max_malloc_size;
+int __builtin_clzll(unsigned long long);
+
+#define __nof_symex_objects                                                    \
+  ((size_t)(1ULL << __builtin_clzll(__CPROVER_max_malloc_size)))
+
+typedef struct {
+  size_t k;
+  void **ptrs;
+} smap_t;
+
+void smap_init(smap_t *smap, size_t k) {
+  *smap = (smap_t){
+      .k = k, .ptrs = __CPROVER_allocate(__nof_symex_objects * sizeof(void *), 1)};
+}
+
+void *smap_get(smap_t *smap, void *ptr) {
+  size_t id = __CPROVER_POINTER_OBJECT(ptr);
+  char *sptr = smap->ptrs[id];
+  if (!sptr) {
+    sptr = __CPROVER_allocate(smap->k * __CPROVER_OBJECT_SIZE(ptr), 1);
+    smap->ptrs[id] = sptr;
+  }
+  return sptr + smap->k * __CPROVER_POINTER_OFFSET(ptr);
+}
+
+typedef struct {
+  uint8_t key;
+  uint8_t value;
+} stk_elem_t;
+
+typedef struct {
+  int8_t top;
+  stk_elem_t *elems;
+} stk_t;
+
+size_t nondet_size_t();
+
+// Creates a fresh borrow stack
+stk_t *stk_new() {
+  stk_t *stk = __CPROVER_allocate(sizeof(stk_t), 1);
+  size_t stk_size = nondet_size_t();
+  __CPROVER_assume(UINT8_MAX <= stk_size && stk_size <= UINT8_MAX);
+  // works with
+  // __CPROVER_assume(stk_size == UINT8_MAX);
+  *stk = (stk_t){
+      .top = 0,
+      .elems = __CPROVER_allocate(sizeof(stk_elem_t) * stk_size, 1)};
+  return stk;
+}
+
+void stk_push(stk_t *stk, uint8_t key, uint8_t value) {
+  assert(stk->top < UINT8_MAX);
+  stk->elems[stk->top] = (stk_elem_t){.key = key, .value = value};
+  stk->top++;
+}
+
+stk_t *get_stk(smap_t *smap, void *ptr) {
+  stk_t **stk_ptr = (stk_t **) smap_get(smap, ptr);
+  if (!(*stk_ptr)) {
+    *stk_ptr = stk_new();
+  }
+  return *stk_ptr;
+}
+
+typedef struct {
+  int a;
+  int b;
+} my_struct_t;
+
+int main() {
+  smap_t smap;
+  smap_init(&smap, sizeof(stk_t*));
+  my_struct_t my_struct;
+  stk_t *stk_a = get_stk(&smap, &(my_struct.a));
+  stk_push(stk_a, 1, 1);
+  stk_t *stk_b = get_stk(&smap, &(my_struct.b));
+  assert(stk_b);
+  stk_push(stk_b, 1, 1);
+}
+
+// clang-format on

regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc

@@ -0,0 +1,9 @@
+CORE smt-backend
+singleton_interval_in_assume_7690.c
+--pointer-check
+^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed (long|long long) int\)stk-\>top\]: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--

src/solvers/smt2/smt2_conv.cpp

@@ -285,7 +285,6 @@ void smt2_convt::define_object_size(
   const object_size_exprt &expr)
 {
   const exprt &ptr = expr.pointer();
-  std::size_t size_width = boolbv_width(expr.type());
   std::size_t pointer_width = boolbv_width(ptr.type());
   std::size_t number = 0;
   std::size_t h=pointer_width-1;
@@ -295,23 +294,23 @@ void smt2_convt::define_object_size(
   {
     const typet &type = o.type();
     auto size_expr = size_of_expr(type, ns);
-    const auto object_size =
-      numeric_cast<mp_integer>(size_expr.value_or(nil_exprt()));
 
     if(
       (o.id() != ID_symbol && o.id() != ID_string_constant) ||
-      !size_expr.has_value() || !object_size.has_value())
+      !size_expr.has_value())
     {
       ++number;
       continue;
     }
 
+    find_symbols(*size_expr);
     out << "(assert (=> (= "
         << "((_ extract " << h << " " << l << ") ";
     convert_expr(ptr);
     out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
-        << "(= " << id << " (_ bv" << *object_size << " " << size_width
-        << "))))\n";
+        << "(= " << id << " ";
+    convert_expr(*size_expr);
+    out << ")))\n";
 
     ++number;
   }