From 074d3be717f1eee8eda1b135f96a6a8929a09a18 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 12 Apr 2022 15:58:19 +0100 Subject: [PATCH 1/8] Add extra test for address-of objects and pointer dereferencing to integers. --- .../cbmc-incr-smt2/pointers/pointers_simple.c | 14 ++++++++++++++ .../cbmc-incr-smt2/pointers/pointers_simple.desc | 12 ++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers/pointers_simple.c create mode 100644 regression/cbmc-incr-smt2/pointers/pointers_simple.desc diff --git a/regression/cbmc-incr-smt2/pointers/pointers_simple.c b/regression/cbmc-incr-smt2/pointers/pointers_simple.c new file mode 100644 index 00000000000..6cdeb4f1faa --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointers_simple.c @@ -0,0 +1,14 @@ +int main() +{ + int a = 10; + int *b = &a; + int c; + + *b = 12; + + __CPROVER_assert(a != *b, "a should be different than b"); + __CPROVER_assert(a == *b, "a should not be different than b"); + __CPROVER_assert( + *b != c, + "c can get assigned a value that makes it the same what b points to"); +} diff --git a/regression/cbmc-incr-smt2/pointers/pointers_simple.desc b/regression/cbmc-incr-smt2/pointers/pointers_simple.desc new file mode 100644 index 00000000000..2c5b645f7a3 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointers_simple.desc @@ -0,0 +1,12 @@ +CORE +pointers_simple.c +--trace +Passing problem to incremental SMT2 solving +\[main\.assertion.\d\] line \d a should be different than b: FAILURE +\[main\.assertion.\d\] line \d+ a should not be different than b: SUCCESS +\[main\.assertion.\d\] line \d+ c can get assigned a value that makes it the same what b points to: FAILURE +c=12 +^EXIT=10$ +^SIGNAL=0$ +-- +-- From 15423e346a31a79e99f56035ace616b35c29f8ef Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 12 Apr 2022 17:27:02 +0100 Subject: [PATCH 2/8] Add conversion of `pointer_object_exprt` and a regression test for that. --- .../cbmc-incr-smt2/pointers/pointer_object.c | 20 +++++++++++++ .../pointers/pointer_object.desc | 10 +++++++ .../smt2_incremental/convert_expr_to_smt.cpp | 30 +++++++++++++++++-- 3 files changed, 58 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_object.c create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_object.desc diff --git a/regression/cbmc-incr-smt2/pointers/pointer_object.c b/regression/cbmc-incr-smt2/pointers/pointer_object.c new file mode 100644 index 00000000000..18f9b76d650 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_object.c @@ -0,0 +1,20 @@ +int main() +{ + int a = 10; + int nondet_bool; + int flag = 1; + + int *b = &a; + int *c = nondet_bool ? &a : 0; + int *d = flag ? &a : 0; + int *e; + + // __CPROVER_same_object is True when + // `__CPROVER_pointer_object(a) == __CPROVER_pointer_object(b)` + __CPROVER_assert( + __CPROVER_same_object(b, c), "expected fail as c can be null"); + __CPROVER_assert( + __CPROVER_same_object(b, d), "expected success because d is &a"); + __CPROVER_assert( + __CPROVER_same_object(b, e), "expected fail as e can be null"); +} diff --git a/regression/cbmc-incr-smt2/pointers/pointer_object.desc b/regression/cbmc-incr-smt2/pointers/pointer_object.desc new file mode 100644 index 00000000000..a99baaa0482 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_object.desc @@ -0,0 +1,10 @@ +CORE +pointer_object.c +--trace --verbosity 10 +\[main\.assertion\.1\] line \d+ expected fail as c can be null: FAILURE +\[main\.assertion\.2\] line \d+ expected success because d is &a: SUCCESS +\[main\.assertion\.3\] line \d+ expected fail as e can be null: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 2594cf02446..dda265c2572 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1142,6 +1142,29 @@ static smt_termt convert_expr_to_smt( mult_overflow.pretty()); } +static smt_termt convert_expr_to_smt( + const pointer_object_exprt &pointer_object, + const sub_expression_mapt &converted) +{ + const auto type = + type_try_dynamic_cast(pointer_object.type()); + INVARIANT(type, "Pointer object should have a bitvector-based type."); + const auto converted_expr = converted.at(pointer_object.pointer()); + const std::size_t width = type->get_width(); + const std::size_t object_bits = config.bv_encoding.object_bits; + INVARIANT( + width >= object_bits, + "Width should be at least as big as the number of object bits."); + const std::size_t ext = width - object_bits; + const auto extract_op = smt_bit_vector_theoryt::extract( + width - 1, width - object_bits)(converted_expr); + if(ext > 0) + { + return smt_bit_vector_theoryt::zero_extend(ext)(extract_op); + } + return extract_op; +} + static smt_termt convert_expr_to_smt( const shl_overflow_exprt &shl_overflow, const sub_expression_mapt &converted) @@ -1437,10 +1460,13 @@ static smt_termt dispatch_expr_to_smt_conversion( else if(expr.id()==ID_pointer_offset) { } - else if(expr.id()==ID_pointer_object) +#endif + else if( + const auto pointer_object = + expr_try_dynamic_cast(expr)) { + return convert_expr_to_smt(*pointer_object, converted); } -#endif if( const auto is_dynamic_object = expr_try_dynamic_cast(expr)) From f02ee6a0cb2d5458bd498f5bdfa50bf948d085a5 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 19 Apr 2022 10:34:41 +0100 Subject: [PATCH 3/8] Add unit tests for pointer object expression conversion --- .../smt2_incremental/convert_expr_to_smt.cpp | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index b51909dac56..d9fdeec976e 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -8,6 +8,7 @@ #include #include #include +#include #include #include @@ -1186,3 +1187,58 @@ TEST_CASE( smt_bit_vector_constant_termt{0, 56}))); } } + +TEST_CASE( + "expr to smt conversion for pointer object expression", + "[core][smt2_incremental]") +{ + // The config lines are necessary to ensure that pointer width in configured. + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + config.bv_encoding.object_bits = 8; + + const auto pointer_type = pointer_typet(unsigned_int_type(), 64 /* bits */); + const pointer_object_exprt foo{ + symbol_exprt{"foo", pointer_type}, pointer_type}; + const pointer_object_exprt foobar{ + symbol_exprt{"foobar", pointer_type}, pointer_type}; + + SECTION("Pointer object expression") + { + const auto converted = convert_expr_to_smt(foo); + const auto expected = + smt_bit_vector_theoryt::zero_extend(56)(smt_bit_vector_theoryt::extract( + 63, 56)(smt_identifier_termt("foo", smt_bit_vector_sortt(64)))); + CHECK(converted == expected); + } + + SECTION("Invariant checks") + { + const cbmc_invariants_should_throwt invariants_throw; + SECTION("Pointer object's operand type should be a bitvector type") + { + auto copy_of_foo = foo; + copy_of_foo.type() = bool_typet{}; + REQUIRE_THROWS_MATCHES( + convert_expr_to_smt(copy_of_foo), + invariant_failedt, + invariant_failure_containing( + "Pointer object should have a bitvector-based type.")); + } + } + + SECTION("Comparison of pointer objects.") + { + const exprt comparison = notequal_exprt{foobar, foo}; + INFO("Expression " + comparison.pretty(1, 0)); + const auto converted = convert_expr_to_smt(comparison); + const auto bv1 = + smt_bit_vector_theoryt::zero_extend(56)(smt_bit_vector_theoryt::extract( + 63, 56)(smt_identifier_termt("foo", smt_bit_vector_sortt(64)))); + const auto bv2 = + smt_bit_vector_theoryt::zero_extend(56)(smt_bit_vector_theoryt::extract( + 63, 56)(smt_identifier_termt("foobar", smt_bit_vector_sortt(64)))); + const auto expected = smt_core_theoryt::distinct(bv2, bv1); + CHECK(converted == expected); + } +} From d4d3aa16882826d3aaf7483147bf46dc363efdad Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 20 Apr 2022 09:04:39 +0100 Subject: [PATCH 4/8] Add an extra test to the regression test suite, suggested by Thomas S. --- .../cbmc-incr-smt2/pointers/pointer_object2.c | 14 ++++++++++++++ .../pointers/pointer_object2.desc | 17 +++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_object2.c create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_object2.desc diff --git a/regression/cbmc-incr-smt2/pointers/pointer_object2.c b/regression/cbmc-incr-smt2/pointers/pointer_object2.c new file mode 100644 index 00000000000..503f9f32633 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_object2.c @@ -0,0 +1,14 @@ +#include +#include + +int main() +{ + int x; + int y; + int z; + bool nondet1; + bool nondet2; + int *a = nondet1 ? &x : &y; + int *b = nondet2 ? &y : &z; + __CPROVER_assert(!__CPROVER_same_object(a, b), "Can be violated."); +} diff --git a/regression/cbmc-incr-smt2/pointers/pointer_object2.desc b/regression/cbmc-incr-smt2/pointers/pointer_object2.desc new file mode 100644 index 00000000000..0d352f86e3d --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_object2.desc @@ -0,0 +1,17 @@ +CORE +pointer_object2.c +--trace --verbosity 10 +\[main\.assertion\.1\] line 13 Can be violated.: FAILURE +nondet1=FALSE +nondet2=TRUE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Ensure that two variables which can get assigned the address of the +same object satisfy the __CPROVER_same_object predicate. In the code +under test, we negate the predicate to be able to get a failure and a +trace which we can then match against expected values which guide +through the path that leads to the two variables getting assigned the +same object. From 061ce174a2e97bb41ec910fdff63fa0511f2b98a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 20 Apr 2022 09:24:47 +0100 Subject: [PATCH 5/8] Convert pointer_offset_exprt to SMT --- .../smt2_incremental/convert_expr_to_smt.cpp | 28 +++++++++++++++++-- 1 file changed, 25 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index dda265c2572..126c4285351 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1165,6 +1165,27 @@ static smt_termt convert_expr_to_smt( return extract_op; } +static smt_termt convert_expr_to_smt( + const pointer_offset_exprt &pointer_offset, + const sub_expression_mapt &converted) +{ + const auto type = + type_try_dynamic_cast(pointer_offset.type()); + INVARIANT(type, "Pointer offset should have a bitvector-based type."); + const auto converted_expr = converted.at(pointer_offset.pointer()); + const std::size_t width = type->get_width(); + std::size_t offset_bits = width - config.bv_encoding.object_bits; + if(offset_bits > width) + offset_bits = width; + const auto extract_op = + smt_bit_vector_theoryt::extract(offset_bits - 1, 0)(converted_expr); + if(width > offset_bits) + { + return smt_bit_vector_theoryt::zero_extend(width - offset_bits)(extract_op); + } + return extract_op; +} + static smt_termt convert_expr_to_smt( const shl_overflow_exprt &shl_overflow, const sub_expression_mapt &converted) @@ -1456,11 +1477,12 @@ static smt_termt dispatch_expr_to_smt_conversion( { return convert_expr_to_smt(*member_extraction, converted); } -#if 0 - else if(expr.id()==ID_pointer_offset) + else if( + const auto pointer_offset = + expr_try_dynamic_cast(expr)) { + return convert_expr_to_smt(*pointer_offset, converted); } -#endif else if( const auto pointer_object = expr_try_dynamic_cast(expr)) From ac0bb15dfe839615fdefaf74ab155b0e12abcc29 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Wed, 20 Apr 2022 09:41:40 +0100 Subject: [PATCH 6/8] Add unit tests for conversion of pointer_offset_exprt to SMT --- .../smt2_incremental/convert_expr_to_smt.cpp | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index d9fdeec976e..f73e98f8f39 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1242,3 +1242,39 @@ TEST_CASE( CHECK(converted == expected); } } + +TEST_CASE("pointer_offset_exprt to SMT conversion", "[core][smt2_incremental]") +{ + // The config lines are necessary to ensure that pointer width in configured. + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + config.bv_encoding.object_bits = 8; + + const auto pointer_type = pointer_typet(unsigned_int_type(), 64 /* bits */); + const pointer_offset_exprt pointer_offset{ + symbol_exprt{"foo", pointer_type}, pointer_type}; + + SECTION("simple pointer_offset_exprt conversion") + { + const auto converted = convert_expr_to_smt(pointer_offset); + const auto expected = + smt_bit_vector_theoryt::zero_extend(8)(smt_bit_vector_theoryt::extract( + 55, 0)(smt_identifier_termt("foo", smt_bit_vector_sortt(64)))); + CHECK(converted == expected); + } + + SECTION("Invariant checks") + { + const cbmc_invariants_should_throwt invariants_throw; + SECTION("pointer_offset_exprt's operand type should be a bitvector type") + { + auto pointer_offset_copy = pointer_offset; + pointer_offset_copy.type() = bool_typet{}; + REQUIRE_THROWS_MATCHES( + convert_expr_to_smt(pointer_offset_copy), + invariant_failedt, + invariant_failure_containing( + "Pointer offset should have a bitvector-based type.")); + } + } +} From e2dca8a711c18e6531ccb17dc74a0ecff8e72aeb Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 28 Apr 2022 11:44:32 +0100 Subject: [PATCH 7/8] Add regression test using __CPROVER_POINTER_OBJECT directly --- .../cbmc-incr-smt2/pointers/pointer_object3.c | 19 +++++++++++++++++++ .../pointers/pointer_object3.desc | 13 +++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_object3.c create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_object3.desc diff --git a/regression/cbmc-incr-smt2/pointers/pointer_object3.c b/regression/cbmc-incr-smt2/pointers/pointer_object3.c new file mode 100644 index 00000000000..019455cea7c --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_object3.c @@ -0,0 +1,19 @@ +#define NULL (void *)0 + +int main() +{ + int foo; + + // The identifiers are allocated deterministically, so we want to check the + // following properties hold: + + // The pointer object of NULL is always going to be zero. + __CPROVER_assert( + __CPROVER_POINTER_OBJECT(NULL) != 0, + "expected to fail with object ID == 0"); + // In the case where the program contains a single address of operation, + // the pointer object is going to be 1. + __CPROVER_assert( + __CPROVER_POINTER_OBJECT(&foo) != 1, + "expected to fail with object ID == 1"); +} diff --git a/regression/cbmc-incr-smt2/pointers/pointer_object3.desc b/regression/cbmc-incr-smt2/pointers/pointer_object3.desc new file mode 100644 index 00000000000..1c2ec66446c --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_object3.desc @@ -0,0 +1,13 @@ +CORE +pointer_object3.c + +\[main\.assertion\.1] line \d+ expected to fail with object ID == 0: FAILURE +\[main\.assertion\.2] line \d+ expected to fail with object ID == 1: FAILURE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Test that the assignment of object IDs to objects is deterministic: +* 0 for the NULL object, and +* 1 for the single object which is the result of an address of operation From e5f91f276360d27dd9d0bc55fc5cb2207a30f952 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 28 Apr 2022 16:48:40 +0100 Subject: [PATCH 8/8] Add regression test for __CPROVER_POINTER_OFFSET --- .../cbmc-incr-smt2/pointers/pointer_offset.c | 16 ++++++++++++++++ .../cbmc-incr-smt2/pointers/pointer_offset.desc | 16 ++++++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_offset.c create mode 100644 regression/cbmc-incr-smt2/pointers/pointer_offset.desc diff --git a/regression/cbmc-incr-smt2/pointers/pointer_offset.c b/regression/cbmc-incr-smt2/pointers/pointer_offset.c new file mode 100644 index 00000000000..a966465e426 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_offset.c @@ -0,0 +1,16 @@ +int main() +{ + int a; + int *p = &a; + int *q = &a; + + __CPROVER_assert( + __CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q), + "expected failure because offsets should be the same"); + + // TODO: Remove comments once pointer arithmetic works: + + // *q = p + 2; + + // __CPROVER_assert(__CPROVER_POINTER_OFFSET(p) != __CPROVER_POINTER_OFFSET(q), "expected failure"); +} diff --git a/regression/cbmc-incr-smt2/pointers/pointer_offset.desc b/regression/cbmc-incr-smt2/pointers/pointer_offset.desc new file mode 100644 index 00000000000..4bb21e3bf2d --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_offset.desc @@ -0,0 +1,16 @@ +CORE +pointer_offset.c +--trace +\[main\.assertion\.1\] line \d+ expected failure because offsets should be the same: FAILURE +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Test that the pointer offset bits of two pointers pointing to +the same object are equal. + +The test also contains a fragment of the test which doesn't work +for now, but would be good to be added as soon as we get pointer +arithmetic to work, so we can make sure that pointer offset fails +appropriately.