Skip to content

Commit a54bc5b

Browse files
Enrico SteffinlongoNlightNFotis
Enrico Steffinlongo
authored andcommitted
Fix duplicate_per_byte when init_expr is signed
When using duplicate_per_byte with signed bv, if the bv was casted to a bigger unsigned bv the sign-extension was performed, so the obtained bv was non-zero on the least significant part and interfeering with the replicated value.
1 parent c435f43 commit a54bc5b

File tree

2 files changed

+22
-17
lines changed

2 files changed

+22
-17
lines changed

src/util/expr_initializer.cpp

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -427,19 +427,19 @@ exprt duplicate_per_byte(
427427
// We haven't got a constant. So, build the expression using shift-and-or.
428428
exprt::operandst values;
429429

430-
typet operation_type = output_type;
431-
if(const auto ptr_type = type_try_dynamic_cast<pointer_typet>(output_type))
432-
{
433-
operation_type = unsignedbv_typet{ptr_type->get_width()};
434-
}
435-
if(
436-
const auto float_type = type_try_dynamic_cast<floatbv_typet>(output_type))
437-
{
438-
operation_type = unsignedbv_typet{float_type->get_width()};
439-
}
440-
// Let's cast simplified_init_expr to output_type.
441-
const exprt casted_init_byte_expr =
442-
typecast_exprt::conditional_cast(init_byte_expr, operation_type);
430+
// When doing the replication we extend the init_expr to the output size to
431+
// compute the bitwise or. To avoid that the sign is extended too we change
432+
// the type of the output to an unsigned bitvector with the same size as the
433+
// output type.
434+
typet operation_type = unsignedbv_typet{output_bv->get_width()};
435+
// To avoid sign-extension during cast we first cast to an unsigned version
436+
// of the same bv type, then we extend it to the output type (adding 0
437+
// padding).
438+
const exprt casted_init_byte_expr = typecast_exprt::conditional_cast(
439+
typecast_exprt::conditional_cast(
440+
init_byte_expr, unsignedbv_typet{init_type_as_bitvector->get_width()}),
441+
operation_type);
442+
443443
values.push_back(casted_init_byte_expr);
444444
for(size_t i = 1; i < size; ++i)
445445
{

unit/util/expr_initializer.cpp

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -311,10 +311,15 @@ TEST_CASE(
311311

312312
const auto result = duplicate_per_byte(init_expr, output_type, test.ns);
313313

314-
const auto casted_init_expr =
315-
typecast_exprt::conditional_cast(init_expr, output_type);
316-
const auto expected =
317-
replicate_expression(casted_init_expr, output_type, replication_count);
314+
const auto operation_type = unsignedbv_typet{output_size};
315+
const auto casted_init_expr = typecast_exprt::conditional_cast(
316+
typecast_exprt::conditional_cast(
317+
init_expr, unsignedbv_typet{init_expr_size}),
318+
operation_type);
319+
const auto expected = typecast_exprt::conditional_cast(
320+
replicate_expression(
321+
casted_init_expr, operation_type, replication_count),
322+
output_type);
318323

319324
REQUIRE(result == expected);
320325
}

0 commit comments

Comments
 (0)