diff --git a/regression/cbmc-incr-smt2/pointers/pointer_values.c b/regression/cbmc-incr-smt2/pointers/pointer_values.c new file mode 100644 index 00000000000..ea3eecb4874 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_values.c @@ -0,0 +1,12 @@ +int main() +{ + int *a; + int *b = 0; + int *c; + __CPROVER_assume(c != 0); + + __CPROVER_assert( + a != b, "should fail because a can be any pointer val, including NULL"); + __CPROVER_assert( + a != c, "should fail because a and c can point to same object"); +} diff --git a/regression/cbmc-incr-smt2/pointers/pointer_values.desc b/regression/cbmc-incr-smt2/pointers/pointer_values.desc new file mode 100644 index 00000000000..a521f9b7c61 --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_values.desc @@ -0,0 +1,12 @@ +CORE +pointer_values.c +--trace +\[main\.assertion\.1\] line \d+ should fail because a can be any pointer val, including NULL: FAILURE +\[main\.assertion\.2\] line \d+ should fail because a and c can point to same object: FAILURE +a=\(\(signed int \*\)NULL\) +c=\(signed int \*\)1 +^EXIT=10$ +^SIGNAL=0$ +-- +-- +Test printing of NULL pointer values in trace. diff --git a/regression/cbmc-incr-smt2/pointers/pointer_values_2.c b/regression/cbmc-incr-smt2/pointers/pointer_values_2.c new file mode 100644 index 00000000000..5016b57b2dd --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_values_2.c @@ -0,0 +1,8 @@ +int main() +{ + int *a; + int *b; + __CPROVER_assume(a == 0xDEADBEEF); + + __CPROVER_assert(a != b, "should fail as b can also be assigned 0xDEADBEEF"); +} diff --git a/regression/cbmc-incr-smt2/pointers/pointer_values_2.desc b/regression/cbmc-incr-smt2/pointers/pointer_values_2.desc new file mode 100644 index 00000000000..da75fa6938d --- /dev/null +++ b/regression/cbmc-incr-smt2/pointers/pointer_values_2.desc @@ -0,0 +1,12 @@ +CORE +pointer_values_2.c +--trace --slice-formula +\[main\.assertion\.1\] line \d should fail as b can also be assigned 0xDEADBEEF: FAILURE +a=\(signed int \*\)3735928559 +b=\(signed int \*\)3735928559 +^EXIT=10$ +^SIGNAL=0$ +-- +-- +3735928559 is the decimal value of the hex constant 0xDEADBEEF that +the pointer is assumed to point to in this example. diff --git a/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp index 415db4cd583..560df31c7c2 100644 --- a/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp +++ b/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp @@ -1,15 +1,15 @@ // Author: Diffblue Ltd. -#include - -#include - #include #include +#include #include #include #include +#include +#include + class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort { private: @@ -37,13 +37,35 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override { + const auto sort_width = bit_vector_constant.get_sort().bit_width(); + if( + const auto pointer_type = + type_try_dynamic_cast(type_to_construct)) + { + INVARIANT( + pointer_type->get_width() == sort_width, + "Width of smt bit vector term must match the width of pointer type."); + if(bit_vector_constant.value() == 0) + { + result = null_pointer_exprt{*pointer_type}; + } + else + { + // The reason we are manually constructing a constant_exprt here is a + // limitation in the design of `from_integer`, which only allows it to + // be used with pointer values of 0 (null pointers). + result = constant_exprt{ + integer2bvrep(bit_vector_constant.value(), sort_width), + *pointer_type}; + } + return; + } if( const auto bitvector_type = type_try_dynamic_cast(type_to_construct)) { INVARIANT( - bitvector_type->get_width() == - bit_vector_constant.get_sort().bit_width(), + bitvector_type->get_width() == sort_width, "Width of smt bit vector term must match the width of bit vector " "type."); result = from_integer(bit_vector_constant.value(), type_to_construct); diff --git a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp index 9ebaa612856..d0a570277ce 100644 --- a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp +++ b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp @@ -68,6 +68,16 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]") rowt{smt_bool_literal_termt{false}, false_exprt{}}, rowt{smt_bit_vector_constant_termt{0, 8}, from_integer(0, c_bool_typet(8))}, rowt{smt_bit_vector_constant_termt{1, 8}, from_integer(1, c_bool_typet(8))}, + rowt{ + smt_bit_vector_constant_termt{0, 64}, + from_integer(0, pointer_typet(void_type(), 64 /* bits */))}, + // The reason for the more intricate elaboration of a pointer with a value + // of 12 is a limitation in the design of from_integer, which only handles + // pointers with value 0 (null pointers). + rowt{ + smt_bit_vector_constant_termt{12, 64}, + constant_exprt( + integer2bvrep(12, 64), pointer_typet(void_type(), 64 /* bits */))}, UNSIGNED_BIT_VECTOR_TESTS(8), SIGNED_BIT_VECTOR_TESTS(8), UNSIGNED_BIT_VECTOR_TESTS(16), @@ -96,23 +106,31 @@ TEST_CASE( using rowt = std::tuple; std::tie(input_term, input_type, invariant_reason) = GENERATE( - rowt{smt_bool_literal_termt{true}, - unsignedbv_typet{16}, - "Bool terms may only be used to construct bool typed expressions."}, - rowt{smt_identifier_termt{"foo", smt_bit_vector_sortt{16}}, - unsignedbv_typet{16}, - "Unexpected conversion of identifier to value expression."}, + rowt{ + smt_bool_literal_termt{true}, + unsignedbv_typet{16}, + "Bool terms may only be used to construct bool typed expressions."}, + rowt{ + smt_identifier_termt{"foo", smt_bit_vector_sortt{16}}, + unsignedbv_typet{16}, + "Unexpected conversion of identifier to value expression."}, rowt{ smt_bit_vector_constant_termt{0, 8}, unsignedbv_typet{16}, "Width of smt bit vector term must match the width of bit vector type."}, - rowt{smt_bit_vector_constant_termt{0, 8}, - empty_typet{}, - "construct_value_expr_from_smt for bit vector should not be applied " - "to unsupported type empty"}, - rowt{smt_core_theoryt::make_not(smt_bool_literal_termt{true}), - unsignedbv_typet{16}, - "Unexpected conversion of function application to value expression."}); + rowt{ + smt_bit_vector_constant_termt{0, 8}, + empty_typet{}, + "construct_value_expr_from_smt for bit vector should not be applied " + "to unsupported type empty"}, + rowt{ + smt_core_theoryt::make_not(smt_bool_literal_termt{true}), + unsignedbv_typet{16}, + "Unexpected conversion of function application to value expression."}, + rowt{ + smt_bit_vector_constant_termt{0, 16}, + pointer_typet{unsigned_int_type(), 0}, + "Width of smt bit vector term must match the width of pointer type"}); SECTION(invariant_reason) { const cbmc_invariants_should_throwt invariants_throw;