Skip to content

Commit e3dd810

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #6831 from NlightNFotis/pointer_val_in_trace_fix
Fix for getting values of pointers in traces in new SMT backend
2 parents d7e8c4d + 691a3df commit e3dd810

File tree

6 files changed

+103
-19
lines changed

6 files changed

+103
-19
lines changed

‎regression/cbmc-incr-smt2/pointers/pointer_values.c‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
int main()
2+
{
3+
int *a;
4+
int *b = 0;
5+
int *c;
6+
__CPROVER_assume(c != 0);
7+
8+
__CPROVER_assert(
9+
a != b, "should fail because a can be any pointer val, including NULL");
10+
__CPROVER_assert(
11+
a != c, "should fail because a and c can point to same object");
12+
}

‎regression/cbmc-incr-smt2/pointers/pointer_values.desc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
pointer_values.c
3+
--trace
4+
\[main\.assertion\.1\] line \d+ should fail because a can be any pointer val, including NULL: FAILURE
5+
\[main\.assertion\.2\] line \d+ should fail because a and c can point to same object: FAILURE
6+
a=\(\(signed int \*\)NULL\)
7+
c=\(signed int \*\)1
8+
^EXIT=10$
9+
^SIGNAL=0$
10+
--
11+
--
12+
Test printing of NULL pointer values in trace.

‎regression/cbmc-incr-smt2/pointers/pointer_values_2.c‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
int *a;
4+
int *b;
5+
__CPROVER_assume(a == 0xDEADBEEF);
6+
7+
__CPROVER_assert(a != b, "should fail as b can also be assigned 0xDEADBEEF");
8+
}

‎regression/cbmc-incr-smt2/pointers/pointer_values_2.desc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
pointer_values_2.c
3+
--trace --slice-formula
4+
\[main\.assertion\.1\] line \d should fail as b can also be assigned 0xDEADBEEF: FAILURE
5+
a=\(signed int \*\)3735928559
6+
b=\(signed int \*\)3735928559
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
--
11+
3735928559 is the decimal value of the hex constant 0xDEADBEEF that
12+
the pointer is assumed to point to in this example.

‎src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp‎

Lines changed: 28 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
// Author: Diffblue Ltd.
22

3-
#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
4-
5-
#include <solvers/smt2_incremental/smt_terms.h>
6-
73
#include <util/arith_tools.h>
84
#include <util/bitvector_types.h>
5+
#include <util/pointer_expr.h>
96
#include <util/std_expr.h>
107
#include <util/std_types.h>
118
#include <util/type.h>
129

10+
#include <solvers/smt2_incremental/construct_value_expr_from_smt.h>
11+
#include <solvers/smt2_incremental/smt_terms.h>
12+
1313
class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
1414
{
1515
private:
@@ -37,13 +37,35 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
3737

3838
void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override
3939
{
40+
const auto sort_width = bit_vector_constant.get_sort().bit_width();
41+
if(
42+
const auto pointer_type =
43+
type_try_dynamic_cast<pointer_typet>(type_to_construct))
44+
{
45+
INVARIANT(
46+
pointer_type->get_width() == sort_width,
47+
"Width of smt bit vector term must match the width of pointer type.");
48+
if(bit_vector_constant.value() == 0)
49+
{
50+
result = null_pointer_exprt{*pointer_type};
51+
}
52+
else
53+
{
54+
// The reason we are manually constructing a constant_exprt here is a
55+
// limitation in the design of `from_integer`, which only allows it to
56+
// be used with pointer values of 0 (null pointers).
57+
result = constant_exprt{
58+
integer2bvrep(bit_vector_constant.value(), sort_width),
59+
*pointer_type};
60+
}
61+
return;
62+
}
4063
if(
4164
const auto bitvector_type =
4265
type_try_dynamic_cast<bitvector_typet>(type_to_construct))
4366
{
4467
INVARIANT(
45-
bitvector_type->get_width() ==
46-
bit_vector_constant.get_sort().bit_width(),
68+
bitvector_type->get_width() == sort_width,
4769
"Width of smt bit vector term must match the width of bit vector "
4870
"type.");
4971
result = from_integer(bit_vector_constant.value(), type_to_construct);

‎unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp‎

Lines changed: 31 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,16 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]")
6868
rowt{smt_bool_literal_termt{false}, false_exprt{}},
6969
rowt{smt_bit_vector_constant_termt{0, 8}, from_integer(0, c_bool_typet(8))},
7070
rowt{smt_bit_vector_constant_termt{1, 8}, from_integer(1, c_bool_typet(8))},
71+
rowt{
72+
smt_bit_vector_constant_termt{0, 64},
73+
from_integer(0, pointer_typet(void_type(), 64 /* bits */))},
74+
// The reason for the more intricate elaboration of a pointer with a value
75+
// of 12 is a limitation in the design of from_integer, which only handles
76+
// pointers with value 0 (null pointers).
77+
rowt{
78+
smt_bit_vector_constant_termt{12, 64},
79+
constant_exprt(
80+
integer2bvrep(12, 64), pointer_typet(void_type(), 64 /* bits */))},
7181
UNSIGNED_BIT_VECTOR_TESTS(8),
7282
SIGNED_BIT_VECTOR_TESTS(8),
7383
UNSIGNED_BIT_VECTOR_TESTS(16),
@@ -96,23 +106,31 @@ TEST_CASE(
96106

97107
using rowt = std::tuple<smt_termt, typet, std::string>;
98108
std::tie(input_term, input_type, invariant_reason) = GENERATE(
99-
rowt{smt_bool_literal_termt{true},
100-
unsignedbv_typet{16},
101-
"Bool terms may only be used to construct bool typed expressions."},
102-
rowt{smt_identifier_termt{"foo", smt_bit_vector_sortt{16}},
103-
unsignedbv_typet{16},
104-
"Unexpected conversion of identifier to value expression."},
109+
rowt{
110+
smt_bool_literal_termt{true},
111+
unsignedbv_typet{16},
112+
"Bool terms may only be used to construct bool typed expressions."},
113+
rowt{
114+
smt_identifier_termt{"foo", smt_bit_vector_sortt{16}},
115+
unsignedbv_typet{16},
116+
"Unexpected conversion of identifier to value expression."},
105117
rowt{
106118
smt_bit_vector_constant_termt{0, 8},
107119
unsignedbv_typet{16},
108120
"Width of smt bit vector term must match the width of bit vector type."},
109-
rowt{smt_bit_vector_constant_termt{0, 8},
110-
empty_typet{},
111-
"construct_value_expr_from_smt for bit vector should not be applied "
112-
"to unsupported type empty"},
113-
rowt{smt_core_theoryt::make_not(smt_bool_literal_termt{true}),
114-
unsignedbv_typet{16},
115-
"Unexpected conversion of function application to value expression."});
121+
rowt{
122+
smt_bit_vector_constant_termt{0, 8},
123+
empty_typet{},
124+
"construct_value_expr_from_smt for bit vector should not be applied "
125+
"to unsupported type empty"},
126+
rowt{
127+
smt_core_theoryt::make_not(smt_bool_literal_termt{true}),
128+
unsignedbv_typet{16},
129+
"Unexpected conversion of function application to value expression."},
130+
rowt{
131+
smt_bit_vector_constant_termt{0, 16},
132+
pointer_typet{unsigned_int_type(), 0},
133+
"Width of smt bit vector term must match the width of pointer type"});
116134
SECTION(invariant_reason)
117135
{
118136
const cbmc_invariants_should_throwt invariants_throw;

0 commit comments

Comments
 (0)