Skip to content

Commit bb9c198

Browse files
committed
Encode integer addresses together with pointer object/offset
Instead of encoding pointers with the same bit width a pointer on a given platform has, just widen the bit-blasted encoding to include both the previous object/offset encoding as well as an (integer) address. The encoding is thus also trivially extended to handle larger numbers of objects and offsets of the same width as the address. Furthermore clean up the code to encapsulate encoding properly, and make in-code layout of pointer encoding more natural (it's now object, offset, integer-address). Fixes: #436 Fixes: #311 Fixes: #94
1 parent 726a92f commit bb9c198

File tree

11 files changed

+512
-182
lines changed

11 files changed

+512
-182
lines changed
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
1-
CORE
1+
THOROUGH
22
main.i
33
--32 --little-endian
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
88
^warning: ignoring
9+
--
10+
Takes around 2 minutes to run.

regression/cbmc/Pointer_Arithmetic13/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=0$

regression/cbmc/Pointer_Arithmetic18/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--32
44
^EXIT=0$

regression/cbmc/Pointer_comparison1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33

44
^EXIT=10$

regression/cbmc/address_space_size_limit1/test.c

-16
This file was deleted.

regression/cbmc/address_space_size_limit1/test.desc

-7
This file was deleted.

regression/cbmc/address_space_size_limit3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
THOROUGH
22
main.i
33
--32 --little-endian --object-bits 25 --pointer-check
44
^EXIT=10$

src/solvers/flattening/boolbv_width.cpp

+4-6
Original file line numberDiff line numberDiff line change
@@ -27,15 +27,12 @@ boolbv_widtht::~boolbv_widtht()
2727

2828
std::size_t boolbv_widtht::get_object_width(const pointer_typet &type) const
2929
{
30-
return config.bv_encoding.object_bits;
30+
return type.get_width();
3131
}
3232

3333
std::size_t boolbv_widtht::get_offset_width(const pointer_typet &type) const
3434
{
35-
const std::size_t pointer_width = type.get_width();
36-
const std::size_t object_width = get_object_width(type);
37-
PRECONDITION(pointer_width >= object_width);
38-
return pointer_width - object_width;
35+
return type.get_width();
3936
}
4037

4138
std::size_t boolbv_widtht::get_address_width(const pointer_typet &type) const
@@ -203,8 +200,9 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
203200
}
204201
else if(type_id==ID_pointer)
205202
{
203+
const pointer_typet &t = type_checked_cast<pointer_typet>(type);
206204
entry.total_width =
207-
get_address_width(type_checked_cast<pointer_typet>(type));
205+
get_address_width(t) + get_object_width(t) + get_offset_width(t);
208206
DATA_INVARIANT(entry.total_width != 0, "pointer must have width");
209207
}
210208
else if(type_id==ID_struct_tag)

0 commit comments

Comments
 (0)