Skip to content

Commit 01cddb0

Browse files
committed
SMT2: fix pointer arithmetic
This fixes the encoding of pointer arithmetic in the SMT2 backend. Addition now no longer overflows from the offset into the object part.
1 parent e5f6077 commit 01cddb0

File tree

2 files changed

+21
-7
lines changed

2 files changed

+21
-7
lines changed

regression/cbmc/Pointer24/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--pointer-check
44
^EXIT=0$

src/solvers/smt2/smt2_conv.cpp

Lines changed: 20 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3645,21 +3645,35 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
36453645
element_size = *element_size_opt;
36463646
}
36473647

3648-
out << "(bvadd ";
3648+
// First convert the pointer operand
3649+
out << "(let ((?pointerop ";
36493650
convert_expr(p);
3650-
out << " ";
3651+
out << ")) ";
3652+
3653+
// The addition is done on the offset part only.
3654+
const std::size_t pointer_width = boolbv_width(p.type());
3655+
const std::size_t offset_bits =
3656+
pointer_width - config.bv_encoding.object_bits;
3657+
3658+
out << "(concat ";
3659+
out << "((_ extract " << pointer_width - 1 << ' ' << offset_bits
3660+
<< ") ?pointerop) ";
3661+
out << "(bvadd ((_ extract " << offset_bits - 1 << " 0) ?pointerop) ";
36513662

36523663
if(element_size >= 2)
36533664
{
3654-
out << "(bvmul ";
3665+
out << "(bvmul ((_ extract " << offset_bits - 1 << " 0) ";
36553666
convert_expr(i);
3656-
out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
3657-
<< "))";
3667+
out << ") (_ bv" << element_size << " " << offset_bits << "))";
36583668
}
36593669
else
3670+
{
3671+
out << "((_ extract " << offset_bits - 1 << " 0) ";
36603672
convert_expr(i);
3673+
out << ')'; // extract
3674+
}
36613675

3662-
out << ')';
3676+
out << ")))"; // bvadd, concat, let
36633677
}
36643678
else
36653679
{

0 commit comments

Comments
 (0)