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. 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. 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()); 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]")