diff --git a/regression/cbmc/Malloc11/slice-formula.desc b/regression/cbmc/Malloc11/slice-formula.desc index fc9450935d6..7e1503c5880 100644 --- a/regression/cbmc/Malloc11/slice-formula.desc +++ b/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$ diff --git a/regression/cbmc/Malloc11/test.desc b/regression/cbmc/Malloc11/test.desc index 0f3c3b19726..f2d081192ad 100644 --- a/regression/cbmc/Malloc11/test.desc +++ b/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$ diff --git a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc b/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc index 1f09f9e1000..808836019d7 100644 --- a/regression/cbmc/issue_5952_soundness_bug_smt_encoding/test_original.desc +++ b/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$ diff --git a/regression/cbmc/pointer-predicates/at_bounds1.desc b/regression/cbmc/pointer-predicates/at_bounds1.desc index 5cbaf19b023..ab59233baf9 100644 --- a/regression/cbmc/pointer-predicates/at_bounds1.desc +++ b/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$ diff --git a/regression/cbmc/simplify-array-size/test.desc b/regression/cbmc/simplify-array-size/test.desc index b06cb557a6d..9a12d1c23c9 100644 --- a/regression/cbmc/simplify-array-size/test.desc +++ b/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$ diff --git a/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c new file mode 100644 index 00000000000..37a264e7d63 --- /dev/null +++ b/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 +#include + +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 diff --git a/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc b/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc new file mode 100644 index 00000000000..bcd5f334075 --- /dev/null +++ b/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$ +-- +-- diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index b4312756dec..6cd0cea82ef 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/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(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; }