From 76634fefadfae8fda4a97503b9bb44107a6bc450 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 15 Jun 2023 18:42:35 +0100 Subject: [PATCH 1/4] Add support for dynamic object sizes in the old SMT backend The old SMT backend simply ignored the sizes of dynamically sized objects instead of actually defining the size. This allowed the solver to just choose whichever size it liked in order to reach an outcome of SAT, rather than applying any bounds which had been applied to the size. Actually translating the size where the expression is non-constant should fix various observable behaviors related to object sizes and bounds. --- src/solvers/smt2/smt2_conv.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) 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; } From bed6839b548bd31372b59657b2eef0153e06196b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 8 Jun 2023 11:51:15 +0100 Subject: [PATCH 2/4] Add test for issue 7690 --- .../singleton_interval_in_assume_7690.c | 89 +++++++++++++++++++ .../test_smt2.desc | 9 ++ 2 files changed, 98 insertions(+) create mode 100644 regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c create mode 100644 regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc 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$ +-- +-- From 5da3a04ddc2c0e9cb58dfa5f3ad489a8bae0ba8e Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 15 Jun 2023 20:07:01 +0100 Subject: [PATCH 3/4] Switch on KNOWNBUG test from issue 5952 original example This is also fixed by support for dynamic object sizes. --- .../issue_5952_soundness_bug_smt_encoding/test_original.desc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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$ From 2fdec1adf5ef5709074688daa90e8f1fccd76b7b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 15 Jun 2023 21:19:49 +0100 Subject: [PATCH 4/4] Switch on existing tests fixed by adding dynamic size support --- regression/cbmc/Malloc11/slice-formula.desc | 2 +- regression/cbmc/Malloc11/test.desc | 2 +- regression/cbmc/pointer-predicates/at_bounds1.desc | 2 +- regression/cbmc/simplify-array-size/test.desc | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) 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/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$