diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 2d6847950e6..d0a7fecf744 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "config.h" #include "magic.h" #include "namespace.h" // IWYU pragma: keep +#include "simplify_expr.h" #include "std_code.h" #include "symbol_table.h" @@ -68,7 +69,7 @@ optionalt expr_initializert::expr_initializer_rec( else if(init_expr.is_zero()) result = from_integer(0, type); else - result = duplicate_per_byte(init_expr, type); + result = duplicate_per_byte(init_expr, type, ns); result.add_source_location()=source_location; return result; @@ -82,7 +83,7 @@ optionalt expr_initializert::expr_initializer_rec( else if(init_expr.is_zero()) result = constant_exprt(ID_0, type); else - result = duplicate_per_byte(init_expr, type); + result = duplicate_per_byte(init_expr, type, ns); result.add_source_location()=source_location; return result; @@ -101,7 +102,7 @@ optionalt expr_initializert::expr_initializer_rec( result = constant_exprt(value, type); } else - result = duplicate_per_byte(init_expr, type); + result = duplicate_per_byte(init_expr, type, ns); result.add_source_location()=source_location; return result; @@ -121,7 +122,7 @@ optionalt expr_initializert::expr_initializer_rec( result = complex_exprt(*sub_zero, *sub_zero, to_complex_type(type)); } else - result = duplicate_per_byte(init_expr, type); + result = duplicate_per_byte(init_expr, type, ns); result.add_source_location()=source_location; return result; @@ -289,7 +290,7 @@ optionalt expr_initializert::expr_initializer_rec( else if(init_expr.is_zero()) result = constant_exprt(irep_idt(), type); else - result = duplicate_per_byte(init_expr, type); + result = duplicate_per_byte(init_expr, type, ns); result.add_source_location()=source_location; return result; @@ -373,10 +374,14 @@ static exprt cast_or_reinterpret(const exprt &expr, const typet &out_type) /// output type. /// \param init_byte_expr The initialization expression /// \param output_type The output type +/// \param ns Namespace to perform type symbol/tag lookups /// \return The built expression /// \note `init_byte_expr` must be a boolean or a bitvector and must be of at /// most `size <= config.ansi_c.char_width` -exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type) +exprt duplicate_per_byte( + const exprt &init_byte_expr, + const typet &output_type, + const namespacet &ns) { const auto init_type_as_bitvector = type_try_dynamic_cast(init_byte_expr.type()); @@ -385,20 +390,25 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type) (init_type_as_bitvector && init_type_as_bitvector->get_width() <= config.ansi_c.char_width) || init_byte_expr.type().id() == ID_bool); + // Simplify init_expr to enable faster duplication when simplifiable to a + // constant expr + const auto simplified_init_expr = simplify_expr(init_byte_expr, ns); if(const auto output_bv = type_try_dynamic_cast(output_type)) { const auto out_width = output_bv->get_width(); - // Replicate `init_byte_expr` enough times until it completely fills + // Replicate `simplified_init_expr` enough times until it completely fills // `output_type`. // We've got a constant. So, precompute the value of the constant. - if(init_byte_expr.is_constant()) + if(simplified_init_expr.is_constant()) { const auto init_size = init_type_as_bitvector->get_width(); - const irep_idt init_value = to_constant_expr(init_byte_expr).get_value(); + const irep_idt init_value = + to_constant_expr(simplified_init_expr).get_value(); // Create a new BV of `output_type` size with its representation being the - // replication of the init_byte_expr (padded with 0) enough times to fill. + // replication of the simplified_init_expr (padded with 0) enough times to + // fill. const auto output_value = make_bvrep(out_width, [&init_size, &init_value](std::size_t index) { // Index modded by 8 to access the i-th bit of init_value @@ -427,7 +437,7 @@ exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type) { operation_type = unsignedbv_typet{float_type->get_width()}; } - // Let's cast init_byte_expr to output_type. + // Let's cast simplified_init_expr to output_type. const exprt casted_init_byte_expr = typecast_exprt::conditional_cast(init_byte_expr, operation_type); values.push_back(casted_init_byte_expr); diff --git a/src/util/expr_initializer.h b/src/util/expr_initializer.h index 2daf1bce6f1..f9421ef56e5 100644 --- a/src/util/expr_initializer.h +++ b/src/util/expr_initializer.h @@ -33,6 +33,9 @@ optionalt expr_initializer( const namespacet &ns, const exprt &init_byte_expr); -exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type); +exprt duplicate_per_byte( + const exprt &init_byte_expr, + const typet &output_type, + const namespacet &ns); #endif // CPROVER_UTIL_EXPR_INITIALIZER_H diff --git a/unit/util/expr_initializer.cpp b/unit/util/expr_initializer.cpp index deadc4d90bb..f297892e32a 100644 --- a/unit/util/expr_initializer.cpp +++ b/unit/util/expr_initializer.cpp @@ -113,7 +113,8 @@ TEST_CASE( const cbmc_invariants_should_throwt invariants_throw; REQUIRE_THROWS_MATCHES( - duplicate_per_byte(array_of_exprt{true_exprt{}, array_type}, input_type), + duplicate_per_byte( + array_of_exprt{true_exprt{}, array_type}, input_type, test.ns), invariant_failedt, invariant_failure_containing( "Condition: (init_type_as_bitvector && " @@ -128,7 +129,8 @@ TEST_CASE( const cbmc_invariants_should_throwt invariants_throw; REQUIRE_THROWS_MATCHES( - duplicate_per_byte(from_integer(0, unsignedbv_typet{10}), input_type), + duplicate_per_byte( + from_integer(0, unsignedbv_typet{10}), input_type, test.ns), invariant_failedt, invariant_failure_containing( "init_type_as_bitvector->get_width() <= config.ansi_c.char_width")); @@ -170,7 +172,8 @@ TEST_CASE( typet output_type = unsignedbv_typet{output_size}; const auto result = duplicate_per_byte( from_integer(init_expr_value, unsignedbv_typet{init_expr_size}), - output_type); + output_type, + test.ns); const auto expected = from_integer(output_expected_value, unsignedbv_typet{output_size}); REQUIRE(result == expected); @@ -178,7 +181,8 @@ TEST_CASE( // Check that signed-bv values are replicated including the sign bit. const auto result_with_signed_init_type = duplicate_per_byte( from_integer(init_expr_value, signedbv_typet{init_expr_size}), - output_type); + output_type, + test.ns); REQUIRE(result_with_signed_init_type == result); } @@ -187,7 +191,8 @@ TEST_CASE( typet output_type = signedbv_typet{output_size}; const auto result = duplicate_per_byte( from_integer(init_expr_value, unsignedbv_typet{init_expr_size}), - output_type); + output_type, + test.ns); const auto expected = from_integer(output_expected_value, signedbv_typet{output_size}); REQUIRE(result == expected); @@ -195,7 +200,8 @@ TEST_CASE( // Check that signed-bv values are replicated including the sign bit. const auto result_with_signed_init_type = duplicate_per_byte( from_integer(init_expr_value, signedbv_typet{init_expr_size}), - output_type); + output_type, + test.ns); REQUIRE(result_with_signed_init_type == result); } @@ -205,7 +211,8 @@ TEST_CASE( const pointer_typet output_type{bool_typet{}, output_size}; const auto result = duplicate_per_byte( from_integer(init_expr_value, signedbv_typet{init_expr_size}), - output_type); + output_type, + test.ns); auto expected = from_integer(output_expected_value, unsignedbv_typet{output_size}); // Forcing the type to be pointer_typet otherwise from_integer fails when @@ -219,11 +226,13 @@ TEST_CASE( // Check that replicating to a float_value is same as unsigned_bv. const auto result = duplicate_per_byte( from_integer(init_expr_value, unsignedbv_typet{init_expr_size}), - float_type()); + float_type(), + test.ns); const auto expected_unsigned_value = expr_try_dynamic_cast(duplicate_per_byte( from_integer(init_expr_value, unsignedbv_typet{init_expr_size}), - unsignedbv_typet{float_type().get_width()})); + unsignedbv_typet{float_type().get_width()}, + test.ns)); REQUIRE(expected_unsigned_value); const auto expected = constant_exprt{expected_unsigned_value->get_value(), float_type()}; @@ -232,6 +241,50 @@ TEST_CASE( } } +TEST_CASE( + "duplicate_per_byte calls simplify", + "[core][util][duplicate_per_byte]") +{ + auto test = expr_initializer_test_environmentt::make(); + // elements are init_expr, expected_value + using rowt = std::tuple; + exprt init_expr; + std::size_t expected_value; + std::tie(init_expr, expected_value) = GENERATE( + rowt{ + from_integer(0xAB, char_type()), 0xABAB}, // char type, no simplification + rowt{ + typecast_exprt::conditional_cast( + from_integer(0xAAB, unsignedbv_typet{24}), char_type()), + 0xABAB}, // cast to smaller type (truncating + rowt{ + typecast_exprt::conditional_cast( + from_integer(0xA, unsignedbv_typet{4}), unsignedbv_typet(8)), + 0x0A0A}, // cast to bigger type (zero-extended) + rowt{ + plus_exprt{ + from_integer(0x0B, char_type()), from_integer(0xA0, char_type())}, + 0xABAB}, // arithmetic operation on char type + rowt{ + typecast_exprt::conditional_cast( + plus_exprt{ + from_integer(0x0B, unsignedbv_typet{24}), + from_integer(0xAA0, unsignedbv_typet(24))}, + char_type()), + 0xABAB}); // arithmetic operation with narrowing cast to char type + + SECTION("Testing with expression") + { + const auto output_type = unsignedbv_typet{config.ansi_c.char_width * 2}; + + const auto result = duplicate_per_byte(init_expr, output_type, test.ns); + + const auto expected = from_integer(expected_value, output_type); + + REQUIRE(result == expected); + } +} + TEST_CASE( "duplicate_per_byte on unsigned_bv with non-constant expr", "[core][util][duplicate_per_byte]") @@ -250,13 +303,13 @@ TEST_CASE( SECTION("Testing with init size " + std::to_string(init_expr_size)) { const auto init_expr = plus_exprt{ - from_integer(1, unsignedbv_typet{init_expr_size}), + symbol_exprt{"a_symbol", unsignedbv_typet{init_expr_size}}, from_integer(2, unsignedbv_typet{init_expr_size})}; SECTION("filling signedbv of size " + std::to_string(output_size)) { typet output_type = signedbv_typet{output_size}; - const auto result = duplicate_per_byte(init_expr, output_type); + const auto result = duplicate_per_byte(init_expr, output_type, test.ns); const auto casted_init_expr = typecast_exprt::conditional_cast(init_expr, output_type); @@ -269,7 +322,7 @@ TEST_CASE( SECTION("filling unsignedbv of size " + std::to_string(output_size)) { typet output_type = unsignedbv_typet{output_size}; - const auto result = duplicate_per_byte(init_expr, output_type); + const auto result = duplicate_per_byte(init_expr, output_type, test.ns); const auto casted_init_expr = typecast_exprt::conditional_cast(init_expr, output_type); @@ -284,7 +337,7 @@ TEST_CASE( // Check that replicating a pointer_value is same as unsigned_bv modulo a // byte_extract outside. const pointer_typet output_type{bool_typet{}, output_size}; - const auto result = duplicate_per_byte(init_expr, output_type); + const auto result = duplicate_per_byte(init_expr, output_type, test.ns); const auto unsigned_corr_type = unsignedbv_typet{output_size}; const auto unsigned_init_expr = typecast_exprt::conditional_cast(init_expr, unsigned_corr_type); @@ -306,7 +359,7 @@ TEST_CASE( const std::size_t float_replication_count = (float_type().get_width() + config.ansi_c.char_width - 1) / config.ansi_c.char_width; - const auto result = duplicate_per_byte(init_expr, float_type()); + const auto result = duplicate_per_byte(init_expr, float_type(), test.ns); const auto unsigned_corr_type = unsignedbv_typet{float_type().get_width()}; const auto unsigned_init_expr = @@ -412,8 +465,8 @@ TEST_CASE( const auto result = expr_initializer(input_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); - const auto expected = - duplicate_per_byte(init_value, unsignedbv_typet{input_type_size}); + const auto expected = duplicate_per_byte( + init_value, unsignedbv_typet{input_type_size}, test.ns); REQUIRE(result.value() == expected); } } @@ -460,7 +513,7 @@ TEST_CASE( expr_initializer(input_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); const auto expected = duplicate_per_byte( - init_value, pointer_typet{bool_typet{}, input_type_size}); + init_value, pointer_typet{bool_typet{}, input_type_size}, test.ns); REQUIRE(result.value() == expected); } } @@ -499,7 +552,8 @@ TEST_CASE("expr_initializer on float type", "[core][util][expr_initializer]") const auto result = expr_initializer(input_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); - const auto expected = duplicate_per_byte(init_value, float_type()); + const auto expected = + duplicate_per_byte(init_value, float_type(), test.ns); REQUIRE(result.value() == expected); } } @@ -562,13 +616,13 @@ TEST_CASE( from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); const auto result = expr_initializer(enum_type, test.loc, test.ns, init_value); - const auto expected = duplicate_per_byte(init_value, enum_type); + const auto expected = duplicate_per_byte(init_value, enum_type, test.ns); REQUIRE(result.has_value()); REQUIRE(result.value() == expected); const auto tag_result = expr_initializer(c_enum_tag_type, test.loc, test.ns, init_value); - auto tag_expected = duplicate_per_byte(init_value, enum_type); + auto tag_expected = duplicate_per_byte(init_value, enum_type, test.ns); tag_expected.type() = c_enum_tag_type; REQUIRE(tag_result.has_value()); REQUIRE(tag_result.value() == tag_expected); @@ -624,7 +678,7 @@ TEST_CASE( expr_initializer(array_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); std::vector array_values{ - elem_count, duplicate_per_byte(init_value, inner_type)}; + elem_count, duplicate_per_byte(init_value, inner_type, test.ns)}; const auto expected = array_exprt{ array_values, array_typet{ @@ -678,7 +732,7 @@ TEST_CASE( expr_initializer(array_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); const auto expected = array_of_exprt{ - duplicate_per_byte(init_value, inner_type), + duplicate_per_byte(init_value, inner_type, test.ns), array_typet{ inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}}; REQUIRE(result.value() == expected); @@ -750,7 +804,7 @@ TEST_CASE( expr_initializer(array_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); std::vector inner_array_values{ - elem_count, duplicate_per_byte(init_value, inner_type)}; + elem_count, duplicate_per_byte(init_value, inner_type, test.ns)}; const auto inner_expected = array_exprt{ inner_array_values, array_typet{ @@ -847,12 +901,13 @@ TEST_CASE( expr_initializer(struct_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); const exprt::operandst expected_inner_struct_fields{ - duplicate_per_byte(init_value, signedbv_typet{32}), - duplicate_per_byte(init_value, unsignedbv_typet{16})}; + duplicate_per_byte(init_value, signedbv_typet{32}, test.ns), + duplicate_per_byte(init_value, unsignedbv_typet{16}, test.ns)}; const struct_exprt expected_inner_struct_expr{ expected_inner_struct_fields, inner_struct_type}; const exprt::operandst expected_struct_fields{ - duplicate_per_byte(init_value, bool_typet{}), expected_inner_struct_expr}; + duplicate_per_byte(init_value, bool_typet{}, test.ns), + expected_inner_struct_expr}; const struct_exprt expected_struct_expr{ expected_struct_fields, struct_type}; REQUIRE(result.value() == expected_struct_expr); @@ -935,7 +990,9 @@ TEST_CASE("expr_initializer on union type", "[core][util][expr_initializer]") expr_initializer(union_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); const union_exprt expected_union{ - "foo", duplicate_per_byte(init_value, signedbv_typet{256}), union_type}; + "foo", + duplicate_per_byte(init_value, signedbv_typet{256}, test.ns), + union_type}; REQUIRE(result.value() == expected_union); const auto union_tag_type = @@ -945,7 +1002,7 @@ TEST_CASE("expr_initializer on union type", "[core][util][expr_initializer]") REQUIRE(tag_result.has_value()); const union_exprt expected_union_tag{ "foo", - duplicate_per_byte(init_value, signedbv_typet{256}), + duplicate_per_byte(init_value, signedbv_typet{256}, test.ns), union_tag_type}; REQUIRE(tag_result.value() == expected_union_tag); } @@ -1024,7 +1081,8 @@ TEST_CASE("expr_initializer on string type", "[core][util][expr_initializer]") const auto result = expr_initializer(string_type, test.loc, test.ns, init_value); REQUIRE(result.has_value()); - const auto expected_string = duplicate_per_byte(init_value, string_type); + const auto expected_string = + duplicate_per_byte(init_value, string_type, test.ns); REQUIRE(result.value() == expected_string); } }