Skip to content

Commit b90fc71

Browse files
authored
Merge pull request #5019 from smowton/smowton/fix/unpack-rec-max-bytes
byte-operators unpack_rec: enforce max-bytes if supplied
2 parents 063d80a + 478cc5c commit b90fc71

File tree

7 files changed

+55
-11
lines changed

7 files changed

+55
-11
lines changed

regression/cbmc/byte_update14/test.c

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int main(int argc, char **argv)
5+
{
6+
int array[10];
7+
char *ptr = argc % 2 ? (char *)&array[0] : (char *)&argc;
8+
ptr[argc] = 'a';
9+
ptr[1] = (char)argc;
10+
assert(ptr[1] == (char)argc);
11+
assert(array[1] == (char)argc);
12+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE broken-smt-backend
2+
test.c
3+
4+
^VERIFICATION FAILED$
5+
^\[main.assertion\.1\] line 10.*SUCCESS$
6+
^\[main.assertion\.2\] line 11.*FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$

regression/cbmc/dynamic_size1/stack_object.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
stack_object.c
33
--pointer-check
44
^EXIT=0$

regression/cbmc/pointer-function-parameters-struct-mutual-recursion/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
--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
44
^EXIT=0$

regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/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
--function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
44
^EXIT=0$

regression/cbmc/pointer-function-parameters-struct-simple-recursion/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
--function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
44
^EXIT=0$

src/solvers/lowering/byte_operators.cpp

Lines changed: 31 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -539,11 +539,24 @@ static exprt unpack_array_vector(
539539

540540
// recursively unpack each element so that we eventually just have an array
541541
// of bytes left
542-
exprt sub = unpack_rec(element, little_endian, {}, max_bytes, ns, true);
542+
543+
const optionalt<mp_integer> element_max_bytes =
544+
max_bytes
545+
? std::min(mp_integer{el_bytes}, *max_bytes - byte_operands.size())
546+
: optionalt<mp_integer>{};
547+
const std::size_t element_max_bytes_int =
548+
element_max_bytes ? numeric_cast_v<std::size_t>(*element_max_bytes)
549+
: el_bytes;
550+
551+
exprt sub =
552+
unpack_rec(element, little_endian, {}, element_max_bytes, ns, true);
543553
exprt::operandst sub_operands =
544-
instantiate_byte_array(sub, 0, el_bytes, ns);
554+
instantiate_byte_array(sub, 0, element_max_bytes_int, ns);
545555
byte_operands.insert(
546556
byte_operands.end(), sub_operands.begin(), sub_operands.end());
557+
558+
if(max_bytes && byte_operands.size() >= *max_bytes)
559+
break;
547560
}
548561

549562
const std::size_t size = byte_operands.size();
@@ -882,10 +895,21 @@ static exprt unpack_rec(
882895
// endianness
883896
auto bits_opt = pointer_offset_bits(src.type(), ns);
884897
DATA_INVARIANT(bits_opt.has_value(), "basic type should have a fixed size");
898+
885899
mp_integer bits = *bits_opt;
900+
mp_integer i = 0;
901+
902+
if(max_bytes.has_value())
903+
{
904+
const auto max_bits = *max_bytes * 8;
905+
if(little_endian)
906+
bits = std::min(bits, max_bits);
907+
else
908+
i = std::max(mp_integer{0}, bits - max_bits);
909+
}
886910

887911
exprt::operandst byte_operands;
888-
for(mp_integer i=0; i<bits; i+=8)
912+
for(; i < bits; i += 8)
889913
{
890914
extractbits_exprt extractbits(
891915
typecast_exprt::conditional_cast(
@@ -1004,7 +1028,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
10041028
src.id() == ID_byte_extract_big_endian);
10051029
const bool little_endian = src.id() == ID_byte_extract_little_endian;
10061030

1007-
// determine an upper bound of the number of bytes we might need
1031+
// determine an upper bound of the last byte we might need
10081032
auto upper_bound_opt = size_of_expr(src.type(), ns);
10091033
if(upper_bound_opt.has_value())
10101034
{
@@ -1041,6 +1065,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
10411065
if(element_bits.has_value() && *element_bits >= 1 && *element_bits % 8 == 0)
10421066
{
10431067
auto num_elements = numeric_cast<std::size_t>(array_type.size());
1068+
// XXX: This can't be right -- unpacked is a byte array, whereas array_type may have larger elements
10441069
if(!num_elements.has_value() && unpacked.op().id() == ID_array)
10451070
num_elements = unpacked.op().operands().size();
10461071

@@ -1221,11 +1246,10 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
12211246
size_bits = op0_bits;
12221247
}
12231248

1224-
mp_integer num_elements =
1225-
(*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
1249+
mp_integer num_bytes = (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
12261250

12271251
// get 'width'-many bytes, and concatenate
1228-
const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_elements);
1252+
const std::size_t width_bytes = numeric_cast_v<std::size_t>(num_bytes);
12291253
exprt::operandst op;
12301254
op.reserve(width_bytes);
12311255

0 commit comments

Comments
 (0)