Skip to content

Commit

Permalink
Byte-operator lowering: do not unconditionally insert bv cast
Browse files Browse the repository at this point in the history
In 848e633 a cast to bv was inserted to block interpreting floatbv
type casts from taking place. It was unnecessarily inserted for all
bitvector types. While this does not result in wrong semantics, it may
block simplification for happening when we end up (via other simplifier
rules) creating a bv (and not (un)signed bv) typed constant. All of
these transformations are correct, but we may end up with an equality
over pointer-typed constants where the underlying constant is a(n)
(un)signed bv on one side, and a bv on the other side. The bit patterns
match, so the back-end will correctly solve this, but the simplifier
cannot.

Observed when studying
model-checking/kani#1978.
  • Loading branch information
tautschnig committed Mar 1, 2023
1 parent 1efed70 commit a3f4730
Showing 1 changed file with 9 additions and 4 deletions.
13 changes: 9 additions & 4 deletions src/util/lower_byte_operators.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -337,17 +337,22 @@ static exprt bv_to_expr(
{
PRECONDITION(can_cast_type<bitvector_typet>(bitvector_expr.type()));

if(
can_cast_type<bitvector_typet>(target_type) ||
target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
target_type.id() == ID_string)
if(target_type.id() == ID_floatbv)
{
std::size_t width = to_bitvector_type(bitvector_expr.type()).get_width();
exprt bv_expr =
typecast_exprt::conditional_cast(bitvector_expr, bv_typet{width});
return simplify_expr(
typecast_exprt::conditional_cast(bv_expr, target_type), ns);
}
else if(
can_cast_type<bitvector_typet>(target_type) ||
target_type.id() == ID_c_enum || target_type.id() == ID_c_enum_tag ||
target_type.id() == ID_string)
{
return simplify_expr(
typecast_exprt::conditional_cast(bitvector_expr, target_type), ns);
}

if(target_type.id() == ID_struct)
{
Expand Down

0 comments on commit a3f4730

Please sign in to comment.