From ebaabf9ea141f06648198aef43e76bc8bcb41a2b Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 31 May 2022 15:15:04 +0100 Subject: [PATCH 1/4] Add implementation for pointers relational operators support --- .../smt2_incremental/convert_expr_to_smt.cpp | 20 ++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 942be39192c..e74c1a5717d 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -530,13 +530,31 @@ static smt_termt convert_relational_to_smt( const auto &lhs = converted.at(binary_relation.lhs()); const auto &rhs = converted.at(binary_relation.rhs()); const typet operand_type = binary_relation.lhs().type(); - if(lhs.get_sort().cast()) + if(can_cast_type(operand_type)) + { + // The code here is operating under the assumption that the comparison + // operands have types for which the comparison makes sense. + + // We already know this is the case given that we have followed + // the if statement branch, but including the same check here + // for consistency (it's cheap). + const auto lhs_type_is_pointer = + can_cast_type(binary_relation.lhs().type()); + const auto rhs_type_is_pointer = + can_cast_type(binary_relation.rhs().type()); + INVARIANT( + lhs_type_is_pointer && rhs_type_is_pointer, + "pointer comparison requires that both operand types are pointers."); + return unsigned_factory(lhs, rhs); + } + else if(lhs.get_sort().cast()) { if(can_cast_type(operand_type)) return unsigned_factory(lhs, rhs); if(can_cast_type(operand_type)) return signed_factory(lhs, rhs); } + UNIMPLEMENTED_FEATURE( "Generation of SMT formula for relational expression: " + binary_relation.pretty()); From 7094f98092ec635a09aa81bc0c8a1ac36d2d1928 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 31 May 2022 15:15:51 +0100 Subject: [PATCH 2/4] Add two regression tests for pointer relational support --- .../pointers_stack_lessthan.c | 19 +++++++++++++++++++ .../pointers_stack_lessthan.desc | 15 +++++++++++++++ .../pointers_stack_malloc.c | 17 +++++++++++++++++ .../pointers_stack_malloc.desc | 13 +++++++++++++ 4 files changed, 64 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c create mode 100644 regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.desc create mode 100644 regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.c create mode 100644 regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.desc diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c new file mode 100644 index 00000000000..ff91413c7b3 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.c @@ -0,0 +1,19 @@ +#define NULL (void *)0 + +int main() +{ + int i = 12; + int *x = &i; + int *y = x + 1; + int *z = x - 1; + + // Assertions on y's relation to x + __CPROVER_assert(y != x, "y != x: expected successful"); + __CPROVER_assert(y > x, "y > x: expected successful"); + __CPROVER_assert(y < x, "y < x: expected failure"); + + // Assertions on z's relation to x + __CPROVER_assert(z != x, "z != x: expected successful"); + __CPROVER_assert(z > x, "z > x: expected failure"); + __CPROVER_assert(z < x, "z < x: expected success"); +} diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.desc b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.desc new file mode 100644 index 00000000000..23e7e398359 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_lessthan.desc @@ -0,0 +1,15 @@ +CORE +pointers_stack_lessthan.c +--trace +\[main\.assertion\.1] line \d+ y != x: expected successful: SUCCESS +\[main\.assertion\.2] line \d+ y > x: expected successful: SUCCESS +\[main\.assertion\.3] line \d+ y < x: expected failure: FAILURE +\[main\.assertion\.4] line \d+ z != x: expected successful: SUCCESS +\[main\.assertion\.5] line \d+ z > x: expected failure: FAILURE +\[main\.assertion\.6] line \d+ z < x: expected success: SUCCESS +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This is testing basic pointer relational operator support for three objects +defined in the function's stack frame. diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.c b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.c new file mode 100644 index 00000000000..2523c8ff807 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.c @@ -0,0 +1,17 @@ +#include + +int main() +{ + int *a = malloc(sizeof(int) * 5); + + for(int i = 0; i < 5; i++) + *(a + i) = i; + + for(int i = 0; i < 5; i++) + { + __CPROVER_assert(*(a + i) >= i, "*(a + i) >= i: expected successful"); + __CPROVER_assert(*(a + i) <= i, "*(a + i) <= i: expected successful"); + __CPROVER_assert(*(a + i) == i, "*(a + i) <= i: expected successful"); + __CPROVER_assert(*(a + i) != i, "*(a + i) <= i: expected failure"); + } +} diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.desc b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.desc new file mode 100644 index 00000000000..a98b92ff153 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_stack_malloc.desc @@ -0,0 +1,13 @@ +CORE +pointers_stack_malloc.c +--trace +\[main\.assertion\.1\] line \d+ \*\(a \+ i\) >= i: expected successful: SUCCESS +\[main\.assertion\.2\] line \d+ \*\(a \+ i\) <= i: expected successful: SUCCESS +\[main\.assertion\.3\] line \d+ \*\(a \+ i\) <= i: expected successful: SUCCESS +\[main\.assertion\.4\] line \d+ \*\(a \+ i\) <= i: expected failure: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This is testing the support for relational operators as applied to pointer objects +backed by a malloc and initialised to some values. From 582fe78178ae358edb874a06d10d24d4648b6fc4 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 6 Jun 2022 10:16:19 +0100 Subject: [PATCH 3/4] Add unit tests for relational operators on pointers in new SMT backend --- .../smt2_incremental/convert_expr_to_smt.cpp | 45 +++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 7b601df8641..ae324344237 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -327,6 +327,51 @@ TEST_CASE( } } +TEST_CASE( + "expr to smt conversion for relational operators as applied to pointers", + "[core][smt2_incremental]") +{ + auto test = expr_to_smt_conversion_test_environmentt::make(test_archt::i386); + // Pointer variables, used for comparisons + const std::size_t pointer_width = 32; + const auto pointer_type = pointer_typet(signedbv_typet{32}, pointer_width); + const symbol_exprt pointer_a("a", pointer_type); + const symbol_exprt pointer_b("b", pointer_type); + // SMT terms needed for pointer comparisons + const smt_termt smt_term_a = + smt_identifier_termt{"a", smt_bit_vector_sortt{pointer_width}}; + const smt_termt smt_term_b = + smt_identifier_termt{"b", smt_bit_vector_sortt{pointer_width}}; + + SECTION("Greater than on pointers") + { + CHECK( + test.convert(greater_than_exprt{pointer_a, pointer_b}) == + smt_bit_vector_theoryt::unsigned_greater_than(smt_term_a, smt_term_b)); + } + + SECTION("Greater than or equal on pointer operands") + { + CHECK( + test.convert(greater_than_or_equal_exprt{pointer_a, pointer_b}) == + smt_bit_vector_theoryt::unsigned_greater_than_or_equal( + smt_term_a, smt_term_b)); + } + SECTION("Less than on pointer operands") + { + CHECK( + test.convert(less_than_exprt{pointer_a, pointer_b}) == + smt_bit_vector_theoryt::unsigned_less_than(smt_term_a, smt_term_b)); + } + SECTION("Less than or equal on pointer operands") + { + CHECK( + test.convert(less_than_or_equal_exprt{pointer_a, pointer_b}) == + smt_bit_vector_theoryt::unsigned_less_than_or_equal( + smt_term_a, smt_term_b)); + } +} + TEST_CASE( "expr to smt conversion for arithmetic operators", "[core][smt2_incremental]") From 118b5b15a7a0ee8f546192b29863cc358838e18a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 6 Jun 2022 10:19:10 +0100 Subject: [PATCH 4/4] Add relational operators in assume context regression tests --- .../pointers_assume.c | 27 +++++++++++++++++++ .../pointers_assume.desc | 14 ++++++++++ 2 files changed, 41 insertions(+) create mode 100644 regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c create mode 100644 regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c new file mode 100644 index 00000000000..42e2cfbe407 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c @@ -0,0 +1,27 @@ +#include + +int main() +{ + int x; + int *y = &x; + int *z = &x; + + if(x) + { + y++; + } + else + { + z++; + } + + __CPROVER_assume(y >= z); + __CPROVER_assert(x != y, "x != y: expected successful"); + __CPROVER_assert(x == y, "x == y: expected failure"); + + __CPROVER_assume(z >= x); + + __CPROVER_assert(z >= x, "z >= x: expected successful"); + __CPROVER_assert(z <= y, "z <= y: expected successful"); + __CPROVER_assert(z <= x, "z <= x: expected failure"); +} diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc new file mode 100644 index 00000000000..d7c0a231f7c --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc @@ -0,0 +1,14 @@ +CORE +pointers_assume.c +--trace +\[main\.assertion\.1\] line \d+ x != y: expected successful: SUCCESS +\[main\.assertion\.2\] line \d+ x == y: expected failure: FAILURE +\[main\.assertion\.3\] line \d+ z >= x: expected successful: SUCCESS +\[main\.assertion\.4\] line \d+ z <= y: expected successful: SUCCESS +\[main\.assertion\.5\] line \d+ z <= x: expected failure: FAILURE +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This is testing basic pointer relational operator support for three objects +defined in the function's stack frame.