From a3f473031ad66722e0453af21bf06defba7561d1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 1 Mar 2023 17:11:18 +0000 Subject: [PATCH] Byte-operator lowering: do not unconditionally insert bv cast In 848e633b6770d 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 https://github.com/model-checking/kani/issues/1978. --- src/util/lower_byte_operators.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index 02986e1442a4..1b3287578457 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -337,10 +337,7 @@ static exprt bv_to_expr( { PRECONDITION(can_cast_type(bitvector_expr.type())); - if( - can_cast_type(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 = @@ -348,6 +345,14 @@ static exprt bv_to_expr( return simplify_expr( typecast_exprt::conditional_cast(bv_expr, target_type), ns); } + else if( + can_cast_type(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) {