From 7f358264d71fb4d939c93b6f0865f9e5efca0a1e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 27 Nov 2022 23:07:41 +0000 Subject: [PATCH 1/5] Refactor expr_initializer to take initialization expression We can now pass in 0 and nondet, and can then extend it to take more general initialization expressions. --- src/util/expr_initializer.cpp | 70 ++++++++++++++++++----------------- 1 file changed, 37 insertions(+), 33 deletions(-) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index ef6275963b4..6f6aa7d9db2 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "namespace.h" // IWYU pragma: keep #include "std_code.h" -template class expr_initializert { public: @@ -25,10 +24,12 @@ class expr_initializert { } - optionalt - operator()(const typet &type, const source_locationt &source_location) + optionalt operator()( + const typet &type, + const source_locationt &source_location, + const exprt &init_expr) { - return expr_initializer_rec(type, source_location); + return expr_initializer_rec(type, source_location, init_expr); } protected: @@ -36,13 +37,14 @@ class expr_initializert optionalt expr_initializer_rec( const typet &type, - const source_locationt &source_location); + const source_locationt &source_location, + const exprt &init_expr); }; -template -optionalt expr_initializert::expr_initializer_rec( +optionalt expr_initializert::expr_initializer_rec( const typet &type, - const source_locationt &source_location) + const source_locationt &source_location, + const exprt &init_expr) { const irep_idt &type_id=type.id(); @@ -57,9 +59,9 @@ optionalt expr_initializert::expr_initializer_rec( type_id==ID_fixedbv) { exprt result; - if(nondet) + if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else + else if(init_expr.is_zero()) result = from_integer(0, type); result.add_source_location()=source_location; @@ -69,9 +71,9 @@ optionalt expr_initializert::expr_initializer_rec( type_id==ID_real) { exprt result; - if(nondet) + if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else + else if(init_expr.is_zero()) result = constant_exprt(ID_0, type); result.add_source_location()=source_location; @@ -81,9 +83,9 @@ optionalt expr_initializert::expr_initializer_rec( type_id==ID_verilog_unsignedbv) { exprt result; - if(nondet) + if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else + else if(init_expr.is_zero()) { const std::size_t width = to_bitvector_type(type).get_width(); std::string value(width, '0'); @@ -97,12 +99,12 @@ optionalt expr_initializert::expr_initializer_rec( else if(type_id==ID_complex) { exprt result; - if(nondet) + if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else + else if(init_expr.is_zero()) { - auto sub_zero = - expr_initializer_rec(to_complex_type(type).subtype(), source_location); + auto sub_zero = expr_initializer_rec( + to_complex_type(type).subtype(), source_location, init_expr); if(!sub_zero.has_value()) return {}; @@ -127,8 +129,8 @@ optionalt expr_initializert::expr_initializer_rec( } else { - auto tmpval = - expr_initializer_rec(array_type.element_type(), source_location); + auto tmpval = expr_initializer_rec( + array_type.element_type(), source_location, init_expr); if(!tmpval.has_value()) return {}; @@ -137,7 +139,7 @@ optionalt expr_initializert::expr_initializer_rec( array_type.size().id() == ID_infinity || !array_size.has_value() || *array_size > MAX_FLATTENED_ARRAY_SIZE) { - if(nondet) + if(init_expr.id() == ID_nondet) return side_effect_expr_nondett(type, source_location); array_of_exprt value(*tmpval, array_type); @@ -159,8 +161,8 @@ optionalt expr_initializert::expr_initializer_rec( { const vector_typet &vector_type=to_vector_type(type); - auto tmpval = - expr_initializer_rec(vector_type.element_type(), source_location); + auto tmpval = expr_initializer_rec( + vector_type.element_type(), source_location, init_expr); if(!tmpval.has_value()) return {}; @@ -190,7 +192,8 @@ optionalt expr_initializert::expr_initializer_rec( DATA_INVARIANT( c.type().id() != ID_code, "struct member must not be of code type"); - const auto member = expr_initializer_rec(c.type(), source_location); + const auto member = + expr_initializer_rec(c.type(), source_location, init_expr); if(!member.has_value()) return {}; @@ -216,8 +219,8 @@ optionalt expr_initializert::expr_initializer_rec( if(!widest_member.has_value()) return {}; - auto component_value = - expr_initializer_rec(widest_member->first.type(), source_location); + auto component_value = expr_initializer_rec( + widest_member->first.type(), source_location, init_expr); if(!component_value.has_value()) return {}; @@ -230,7 +233,7 @@ optionalt expr_initializert::expr_initializer_rec( else if(type_id==ID_c_enum_tag) { auto result = expr_initializer_rec( - ns.follow_tag(to_c_enum_tag_type(type)), source_location); + ns.follow_tag(to_c_enum_tag_type(type)), source_location, init_expr); if(!result.has_value()) return {}; @@ -243,7 +246,7 @@ optionalt expr_initializert::expr_initializer_rec( else if(type_id==ID_struct_tag) { auto result = expr_initializer_rec( - ns.follow_tag(to_struct_tag_type(type)), source_location); + ns.follow_tag(to_struct_tag_type(type)), source_location, init_expr); if(!result.has_value()) return {}; @@ -256,7 +259,7 @@ optionalt expr_initializert::expr_initializer_rec( else if(type_id==ID_union_tag) { auto result = expr_initializer_rec( - ns.follow_tag(to_union_tag_type(type)), source_location); + ns.follow_tag(to_union_tag_type(type)), source_location, init_expr); if(!result.has_value()) return {}; @@ -269,9 +272,9 @@ optionalt expr_initializert::expr_initializer_rec( else if(type_id==ID_string) { exprt result; - if(nondet) + if(init_expr.id() == ID_nondet) result = side_effect_expr_nondett(type, source_location); - else + else if(init_expr.is_zero()) result = constant_exprt(irep_idt(), type); result.add_source_location()=source_location; @@ -292,7 +295,8 @@ optionalt zero_initializer( const source_locationt &source_location, const namespacet &ns) { - return expr_initializert(ns)(type, source_location); + return expr_initializert(ns)( + type, source_location, constant_exprt(ID_0, char_type())); } /// Create a non-deterministic value for type `type`, with all subtypes @@ -307,5 +311,5 @@ optionalt nondet_initializer( const source_locationt &source_location, const namespacet &ns) { - return expr_initializert(ns)(type, source_location); + return expr_initializert(ns)(type, source_location, exprt(ID_nondet)); } From fe6c7d7739b406dfcef63dc03d4f8b4310e8a866 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 27 Nov 2022 23:08:41 +0000 Subject: [PATCH 2/5] Extend expr_initializer to support byte-wise initialization Each byte of the expression is initialized to the given initialization expression. This building block will be required for the shadow memory implementation. --- src/util/expr_initializer.cpp | 76 +++++++++++++++++++++++++++++++++++ src/util/expr_initializer.h | 8 ++++ 2 files changed, 84 insertions(+) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 6f6aa7d9db2..4cccafb3d54 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -12,7 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr_initializer.h" #include "arith_tools.h" +#include "bitvector_expr.h" #include "c_types.h" +#include "config.h" #include "magic.h" #include "namespace.h" // IWYU pragma: keep #include "std_code.h" @@ -63,6 +65,8 @@ optionalt expr_initializert::expr_initializer_rec( result = side_effect_expr_nondett(type, source_location); else if(init_expr.is_zero()) result = from_integer(0, type); + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -75,6 +79,8 @@ optionalt expr_initializert::expr_initializer_rec( result = side_effect_expr_nondett(type, source_location); else if(init_expr.is_zero()) result = constant_exprt(ID_0, type); + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -92,6 +98,8 @@ optionalt expr_initializert::expr_initializer_rec( result = constant_exprt(value, type); } + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -110,6 +118,8 @@ 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.add_source_location()=source_location; return result; @@ -276,6 +286,8 @@ optionalt expr_initializert::expr_initializer_rec( result = side_effect_expr_nondett(type, source_location); else if(init_expr.is_zero()) result = constant_exprt(irep_idt(), type); + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -313,3 +325,67 @@ optionalt nondet_initializer( { return expr_initializert(ns)(type, source_location, exprt(ID_nondet)); } + +/// Create a value for type `type`, with all subtype bytes +/// initialized to the given value. +/// \param type: Type of the target expression. +/// \param source_location: Location to record in all created sub-expressions. +/// \param ns: Namespace to perform type symbol/tag lookups. +/// \param init_byte_expr: Value to be used for initialization. +/// \return An expression if a byte-initialized expression of the input type +/// can be built. +optionalt expr_initializer( + const typet &type, + const source_locationt &source_location, + const namespacet &ns, + const exprt &init_byte_expr) +{ + return expr_initializert(ns)(type, source_location, init_byte_expr); +} + +/// Builds an expression of the given output type with each of its bytes +/// initialized to the given initialization expression. +/// Integer bitvector types are currently supported. +/// For unsupported types the initialization expression is casted to the +/// output type. +/// \param init_byte_expr The initialization expression +/// \param output_type The output type +/// \return The built expression +exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type) +{ + if(output_type.id() == ID_unsignedbv || output_type.id() == ID_signedbv) + { + const size_t size = + to_bitvector_type(output_type).get_width() / config.ansi_c.char_width; + + // We've got a constant. So, precompute the value of the constant. + if(init_byte_expr.is_constant()) + { + const mp_integer value = + numeric_cast_v(to_constant_expr(init_byte_expr)); + mp_integer duplicated_value = value; + for(size_t i = 1; i < size; ++i) + { + duplicated_value = + bitwise_or(duplicated_value << config.ansi_c.char_width, value); + } + return from_integer(duplicated_value, output_type); + } + + // We haven't got a constant. So, build the expression using shift-and-or. + exprt::operandst values; + values.push_back(init_byte_expr); + for(size_t i = 1; i < size; ++i) + { + values.push_back(shl_exprt( + init_byte_expr, + from_integer(config.ansi_c.char_width * i, size_type()))); + } + if(values.size() == 1) + return values[0]; + return multi_ary_exprt(ID_bitor, values, output_type); + } + + // Anything else. We don't know what to do with it. So, just cast. + return typecast_exprt::conditional_cast(init_byte_expr, output_type); +} diff --git a/src/util/expr_initializer.h b/src/util/expr_initializer.h index 782778c68f7..2daf1bce6f1 100644 --- a/src/util/expr_initializer.h +++ b/src/util/expr_initializer.h @@ -27,4 +27,12 @@ optionalt nondet_initializer( const source_locationt &source_location, const namespacet &ns); +optionalt expr_initializer( + const typet &type, + const source_locationt &source_location, + const namespacet &ns, + const exprt &init_byte_expr); + +exprt duplicate_per_byte(const exprt &init_byte_expr, const typet &output_type); + #endif // CPROVER_UTIL_EXPR_INITIALIZER_H From 54efb47d613c28c109951870e444e222bf5903f0 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 18 Jul 2023 19:53:00 +0100 Subject: [PATCH 3/5] Improved checks and fixed duplicate_per_byte Function `duplicate_per_byte` now has a PRECONDITION checking that the `init_byte_expr` is either a boolean or a bitvector of maximum size 8. Also the computation of the number of duplication correctly accounts the case when the destination is not divisible by 8. In this case the input is duplicated one extra (including the sign bit if any) time and then truncated to the output size. --- src/util/expr_initializer.cpp | 52 +++++++++++++++++++++++++---------- 1 file changed, 37 insertions(+), 15 deletions(-) diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index 4cccafb3d54..4804fbfcdb7 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -346,39 +346,61 @@ optionalt expr_initializer( /// Builds an expression of the given output type with each of its bytes /// initialized to the given initialization expression. /// Integer bitvector types are currently supported. -/// For unsupported types the initialization expression is casted to the +/// For unsupported `output_type` the initialization expression is casted to the /// output type. /// \param init_byte_expr The initialization expression /// \param output_type The output type /// \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) { - if(output_type.id() == ID_unsignedbv || output_type.id() == ID_signedbv) + const auto init_type_as_bitvector = + type_try_dynamic_cast(init_byte_expr.type()); + // Fail if `init_byte_expr` is not a bitvector of maximum 8 bits or a boolean. + PRECONDITION( + (init_type_as_bitvector && + init_type_as_bitvector->get_width() <= config.ansi_c.char_width) || + init_byte_expr.type().id() == ID_bool); + if(const auto output_bv = type_try_dynamic_cast(output_type)) { - const size_t size = - to_bitvector_type(output_type).get_width() / config.ansi_c.char_width; + const auto out_width = output_bv->get_width(); + // Replicate `init_byte_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()) { - const mp_integer value = - numeric_cast_v(to_constant_expr(init_byte_expr)); - mp_integer duplicated_value = value; - for(size_t i = 1; i < size; ++i) - { - duplicated_value = - bitwise_or(duplicated_value << config.ansi_c.char_width, value); - } - return from_integer(duplicated_value, output_type); + const auto init_size = init_type_as_bitvector->get_width(); + const irep_idt init_value = to_constant_expr(init_byte_expr).get_value(); + + // Create a new BV od `output_type` size with its representation being the + // replication of the init_byte_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 + const auto source_index = index % config.ansi_c.char_width; + // If the modded i-th bit exists get it, otherwise add 0 padding. + return source_index < init_size && + get_bvrep_bit(init_value, init_size, source_index); + }); + + return constant_exprt{output_value, output_type}; } + const size_t size = + (out_width + config.ansi_c.char_width - 1) / config.ansi_c.char_width; + // We haven't got a constant. So, build the expression using shift-and-or. exprt::operandst values; - values.push_back(init_byte_expr); + // Let's cast init_byte_expr to output_type. + const exprt casted_init_byte_expr = + typecast_exprt::conditional_cast(init_byte_expr, output_type); + values.push_back(casted_init_byte_expr); for(size_t i = 1; i < size; ++i) { values.push_back(shl_exprt( - init_byte_expr, + casted_init_byte_expr, from_integer(config.ansi_c.char_width * i, size_type()))); } if(values.size() == 1) From fefeac27a6c510eab06685fe11a9d575f80bbbb6 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 18 Jul 2023 19:54:01 +0100 Subject: [PATCH 4/5] Added tests for duplicate_per_byte in the BV case --- unit/util/expr_initializer.cpp | 225 +++++++++++++++++++++++++++++++-- 1 file changed, 214 insertions(+), 11 deletions(-) diff --git a/unit/util/expr_initializer.cpp b/unit/util/expr_initializer.cpp index efbda566997..c797759dd19 100644 --- a/unit/util/expr_initializer.cpp +++ b/unit/util/expr_initializer.cpp @@ -1,15 +1,21 @@ // Author: Diffblue Ltd. #include +#include #include #include +#include #include #include #include #include +#include #include +#include +#include + /// Helper struct to hold useful test components. struct expr_initializer_test_environmentt { @@ -19,6 +25,10 @@ struct expr_initializer_test_environmentt static expr_initializer_test_environmentt make() { + // These config lines are necessary before construction because char size + // depend on the global configuration. + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); return {}; } @@ -68,24 +78,217 @@ create_tag_populate_env(const typet &type, symbol_tablet &symbol_table) UNREACHABLE; } -TEST_CASE("nondet_initializer boolean", "[core][util][expr_initializer]") +exprt replicate_expression( + const exprt &expr, + const typet &output_type, + std::size_t times) +{ + if(times == 1) + { + return expr; + } + exprt::operandst operands; + operands.push_back(expr); + for(std::size_t i = 1; i < times; ++i) + { + operands.push_back( + shl_exprt{expr, from_integer(config.ansi_c.char_width * i, size_type())}); + } + return multi_ary_exprt{ID_bitor, operands, output_type}; +} + +TEST_CASE( + "duplicate_per_byte precondition works", + "[core][util][duplicate_per_byte]") +{ + auto test = expr_initializer_test_environmentt::make(); + typet input_type = signedbv_typet{8}; + + SECTION("duplicate_per_byte fails when init type is not a bitvector") + { + const array_typet array_type{ + bool_typet{}, from_integer(3, signedbv_typet{8})}; + + const cbmc_invariants_should_throwt invariants_throw; + + REQUIRE_THROWS_MATCHES( + duplicate_per_byte(array_of_exprt{true_exprt{}, array_type}, input_type), + invariant_failedt, + invariant_failure_containing( + "Condition: (init_type_as_bitvector && " + "init_type_as_bitvector->get_width() <= config.ansi_c.char_width) || " + "init_byte_expr.type().id() == ID_bool")); + } + + SECTION( + "duplicate_per_byte fails when init type is a bitvector larger than " + "char_width bits") + { + const cbmc_invariants_should_throwt invariants_throw; + + REQUIRE_THROWS_MATCHES( + duplicate_per_byte(from_integer(0, unsignedbv_typet{10}), input_type), + invariant_failedt, + invariant_failure_containing( + "init_type_as_bitvector->get_width() <= config.ansi_c.char_width")); + } +} + +std::string to_hex(unsigned int value) +{ + std::stringstream ss; + ss << "0x" << std::hex << value; + return ss.str(); +} + +TEST_CASE( + "duplicate_per_byte on unsigned_bv with constant", + "[core][util][duplicate_per_byte]") +{ + auto test = expr_initializer_test_environmentt::make(); + // elements are init_expr_value, init_expr_size, output_expected_value, output_size + using rowt = std::tuple; + unsigned int init_expr_value, output_expected_value; + std::size_t output_size, init_expr_size; + std::tie( + init_expr_value, init_expr_size, output_expected_value, output_size) = + GENERATE( + rowt{0xFF, 8, 0xFF, 8}, // same-type constant + rowt{0x2, 2, 0x02, 8}, // smaller-type constant gets promoted + rowt{0x11, 5, 0x11, 5}, // same-type constant + rowt{0x21, 8, 0x01, 5}, // bigger-type constant gets truncated + rowt{0x2, 3, 0x02, 5}, // smaller-type constant gets promoted + rowt{0xAB, 8, 0xABAB, 16}, // smaller-type constant gets replicated + rowt{0xAB, 8, 0xBABAB, 20} // smaller-type constant gets replicated + ); + SECTION( + "Testing with output size " + std::to_string(output_size) + " init value " + + to_hex(init_expr_value) + " of size " + std::to_string(init_expr_size)) + { + 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); + const auto expected = + from_integer(output_expected_value, unsignedbv_typet{output_size}); + REQUIRE(result == expected); + + // 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); + REQUIRE(result_with_signed_init_type == result); + } +} + +TEST_CASE( + "duplicate_per_byte on unsigned_bv with non-constant expr", + "[core][util][duplicate_per_byte]") +{ + auto test = expr_initializer_test_environmentt::make(); + // elements are init_expr_size, output_size, replication_count + using rowt = std::tuple; + std::size_t init_expr_size, output_size, replication_count; + std::tie(init_expr_size, output_size, replication_count) = GENERATE( + rowt{8, 8, 1}, // same-type expr no-cast + rowt{2, 2, 1}, // same-type expr no-cast + rowt{3, 8, 1}, // smaller-type gets promoted + rowt{8, 2, 1}, // bigger type gets truncated + rowt{8, 16, 2}, // replicated twice + rowt{8, 20, 3}); // replicated three times and truncated + SECTION( + "Testing with output size " + std::to_string(output_size) + " init size " + + std::to_string(init_expr_size)) + { + typet output_type = signedbv_typet{output_size}; + + const auto init_expr = plus_exprt{ + from_integer(1, unsignedbv_typet{init_expr_size}), + from_integer(2, unsignedbv_typet{init_expr_size})}; + const auto result = duplicate_per_byte(init_expr, output_type); + + const auto casted_init_expr = + typecast_exprt::conditional_cast(init_expr, output_type); + const auto expected = + replicate_expression(casted_init_expr, output_type, replication_count); + + REQUIRE(result == expected); + } +} + +TEST_CASE("expr_initializer boolean", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); typet input = bool_typet{}; - const auto result = nondet_initializer(input, test.loc, test.ns); - REQUIRE(result.has_value()); - const auto expected = side_effect_expr_nondett{bool_typet{}, test.loc}; - REQUIRE(result.value() == expected); + SECTION("nondet_initializer") + { + const auto result = nondet_initializer(input, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = side_effect_expr_nondett{bool_typet{}, test.loc}; + REQUIRE(result.value() == expected); + } + SECTION("zero_initializer") + { + const auto result = zero_initializer(input, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = from_integer(0, bool_typet()); + ; + REQUIRE(result.value() == expected); + } + SECTION("expr_initializer with same-type constant") + { + const auto result = + expr_initializer(input, test.loc, test.ns, true_exprt{}); + REQUIRE(result.has_value()); + const auto expected = true_exprt{}; + REQUIRE(result.value() == expected); + } + SECTION("expr_initializer with other-type constant") + { + const auto result = expr_initializer( + input, test.loc, test.ns, from_integer(1, signedbv_typet{8})); + REQUIRE(result.has_value()); + const auto expected = + typecast_exprt{from_integer(1, signedbv_typet{8}), bool_typet{}}; + REQUIRE(result.value() == expected); + } + SECTION("expr_initializer with non-constant expr") + { + const auto result = expr_initializer( + input, test.loc, test.ns, or_exprt{true_exprt(), true_exprt{}}); + REQUIRE(result.has_value()); + const auto expected = or_exprt{true_exprt{}, true_exprt{}}; + REQUIRE(result.value() == expected); + } } -TEST_CASE("nondet_initializer signed_bv", "[core][util][expr_initializer]") +TEST_CASE( + "nondet_initializer 8-bit signed_bv", + "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); - typet input = signedbv_typet{8}; - const auto result = nondet_initializer(input, test.loc, test.ns); - REQUIRE(result.has_value()); - const auto expected = side_effect_expr_nondett{signedbv_typet{8}, test.loc}; - REQUIRE(result.value() == expected); + const std::size_t input_type_size = 8; + typet input_type = signedbv_typet{input_type_size}; + SECTION("nondet_initializer") + { + const auto result = nondet_initializer(input_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = + side_effect_expr_nondett{signedbv_typet{input_type_size}, test.loc}; + REQUIRE(result.value() == expected); + } + SECTION("zero_initializer") + { + const auto result = zero_initializer(input_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = from_integer(0, signedbv_typet{input_type_size}); + REQUIRE(result.value() == expected); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + // TODO: duplicate_per_byte is tested separately. Here we should check that + // expr_initializer calls duplicate_per_byte. + } } TEST_CASE("nondet_initializer c_enum", "[core][util][expr_initializer]") From e049de7a8cfa3115e098bb4dd510923759eb93c7 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 18 Jul 2023 19:54:47 +0100 Subject: [PATCH 5/5] Test for zero_initializer and expr_initializer --- unit/util/expr_initializer.cpp | 609 ++++++++++++++++++++++++++------- 1 file changed, 490 insertions(+), 119 deletions(-) diff --git a/unit/util/expr_initializer.cpp b/unit/util/expr_initializer.cpp index c797759dd19..f5f2d5e990c 100644 --- a/unit/util/expr_initializer.cpp +++ b/unit/util/expr_initializer.cpp @@ -146,21 +146,20 @@ TEST_CASE( "[core][util][duplicate_per_byte]") { auto test = expr_initializer_test_environmentt::make(); - // elements are init_expr_value, init_expr_size, output_expected_value, output_size + // values: init_expr_value, init_expr_size, output_expected_value, output_size using rowt = std::tuple; unsigned int init_expr_value, output_expected_value; std::size_t output_size, init_expr_size; std::tie( init_expr_value, init_expr_size, output_expected_value, output_size) = GENERATE( - rowt{0xFF, 8, 0xFF, 8}, // same-type constant - rowt{0x2, 2, 0x02, 8}, // smaller-type constant gets promoted - rowt{0x11, 5, 0x11, 5}, // same-type constant - rowt{0x21, 8, 0x01, 5}, // bigger-type constant gets truncated - rowt{0x2, 3, 0x02, 5}, // smaller-type constant gets promoted - rowt{0xAB, 8, 0xABAB, 16}, // smaller-type constant gets replicated - rowt{0xAB, 8, 0xBABAB, 20} // smaller-type constant gets replicated - ); + rowt{0xFF, 8, 0xFF, 8}, // same-type constant + rowt{0x2, 2, 0x02, 8}, // smaller-type constant gets promoted + rowt{0x11, 5, 0x11, 5}, // same-type constant + rowt{0x21, 8, 0x01, 5}, // bigger-type constant gets truncated + rowt{0x2, 3, 0x02, 5}, // smaller-type constant gets promoted + rowt{0xAB, 8, 0xABAB, 16}, // smaller-type constant gets replicated + rowt{0xAB, 8, 0xBABAB, 20}); // smaller-type constant gets replicated SECTION( "Testing with output size " + std::to_string(output_size) + " init value " + to_hex(init_expr_value) + " of size " + std::to_string(init_expr_size)) @@ -226,14 +225,19 @@ TEST_CASE("expr_initializer boolean", "[core][util][expr_initializer]") REQUIRE(result.has_value()); const auto expected = side_effect_expr_nondett{bool_typet{}, test.loc}; REQUIRE(result.value() == expected); + const auto expr_result = + expr_initializer(input, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); } SECTION("zero_initializer") { const auto result = zero_initializer(input, test.loc, test.ns); REQUIRE(result.has_value()); const auto expected = from_integer(0, bool_typet()); - ; REQUIRE(result.value() == expected); + const auto expr_result = expr_initializer( + input, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); } SECTION("expr_initializer with same-type constant") { @@ -263,53 +267,123 @@ TEST_CASE("expr_initializer boolean", "[core][util][expr_initializer]") } TEST_CASE( - "nondet_initializer 8-bit signed_bv", + "expr_initializer on variable-bit unsigned_bv", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); - const std::size_t input_type_size = 8; - typet input_type = signedbv_typet{input_type_size}; - SECTION("nondet_initializer") - { - const auto result = nondet_initializer(input_type, test.loc, test.ns); - REQUIRE(result.has_value()); - const auto expected = - side_effect_expr_nondett{signedbv_typet{input_type_size}, test.loc}; - REQUIRE(result.value() == expected); - } - SECTION("zero_initializer") - { - const auto result = zero_initializer(input_type, test.loc, test.ns); - REQUIRE(result.has_value()); - const auto expected = from_integer(0, signedbv_typet{input_type_size}); - REQUIRE(result.value() == expected); - } - SECTION("expr_initializer calls duplicate_per_byte") + const std::size_t input_type_size = GENERATE(3, 8, 16, 20); + SECTION( + "Testing with expected type as unsigned_bv of size " + + std::to_string(input_type_size)) { - // TODO: duplicate_per_byte is tested separately. Here we should check that - // expr_initializer calls duplicate_per_byte. + typet input_type = unsignedbv_typet{input_type_size}; + SECTION("nondet_initializer works") + { + const auto result = nondet_initializer(input_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = + side_effect_expr_nondett{unsignedbv_typet{input_type_size}, test.loc}; + REQUIRE(result.value() == expected); + const auto expr_result = + expr_initializer(input_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + } + SECTION("zero_initializer works") + { + const auto result = zero_initializer(input_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = from_integer(0, unsignedbv_typet{input_type_size}); + REQUIRE(result.value() == expected); + const auto expr_result = expr_initializer( + input_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0x0A, unsignedbv_typet{config.ansi_c.char_width}); + 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}); + REQUIRE(result.value() == expected); + } } } -TEST_CASE("nondet_initializer c_enum", "[core][util][expr_initializer]") +TEST_CASE( + "expr_initializer on c_enum and c_enum_tag", + "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); const unsignedbv_typet enum_underlying_type{8}; const auto enum_type = make_c_enum_type(enum_underlying_type); - const auto result = nondet_initializer(enum_type, test.loc, test.ns); - REQUIRE(result.has_value()); - const auto expected = side_effect_expr_nondett{enum_type, test.loc}; - REQUIRE(result.value() == expected); - // Repeat with the c_enum_tag_typet instead of the c_enum_typet it points to const auto c_enum_tag_type = create_tag_populate_env(enum_type, test.symbol_table); - const auto tag_result = - nondet_initializer(c_enum_tag_type, test.loc, test.ns); + SECTION("nondet_initializer works") + { + const auto result = nondet_initializer(enum_type, test.loc, test.ns); + const auto expected = side_effect_expr_nondett{enum_type, test.loc}; + REQUIRE(result.has_value()); + REQUIRE(result.value() == expected); + const auto expr_result = + expr_initializer(enum_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + + const auto tag_result = + nondet_initializer(c_enum_tag_type, test.loc, test.ns); + const auto tag_expected = + side_effect_expr_nondett{c_enum_tag_type, test.loc}; + REQUIRE(tag_result.has_value()); + REQUIRE(tag_result.value() == tag_expected); + const auto tag_expr_result = + expr_initializer(c_enum_tag_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(tag_expr_result == tag_result); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(enum_type, test.loc, test.ns); + const auto expected = from_integer(0, enum_type); + REQUIRE(result.has_value()); + REQUIRE(result.value() == expected); + const auto expr_result = expr_initializer( + enum_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + + const auto tag_result = + zero_initializer(c_enum_tag_type, test.loc, test.ns); + auto tag_expected = from_integer(0, enum_type); + tag_expected.type() = c_enum_tag_type; + REQUIRE(tag_result.has_value()); + REQUIRE(tag_result.value() == tag_expected); + const auto tag_expr_result = expr_initializer( + c_enum_tag_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(tag_expr_result == tag_result); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + 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); + 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); + tag_expected.type() = c_enum_tag_type; + REQUIRE(tag_result.has_value()); + REQUIRE(tag_result.value() == tag_expected); + } } TEST_CASE( - "nondet_initializer on fixed-size array of signed 8 bit elements", + "expr_initializer on fixed-size array of signed 8 bit elements", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); @@ -317,36 +391,109 @@ TEST_CASE( const std::size_t elem_count = 3; typet array_type = array_typet{inner_type, from_integer(elem_count, signedbv_typet{8})}; - const auto result = nondet_initializer(array_type, test.loc, test.ns); - REQUIRE(result.has_value()); - std::vector array_values{ - elem_count, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}; - const auto expected = array_exprt{ - array_values, - array_typet{ - signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; - REQUIRE(result.value() == expected); + + SECTION("nodet_initializer works") + { + const auto result = nondet_initializer(array_type, test.loc, test.ns); + REQUIRE(result.has_value()); + std::vector array_values{ + elem_count, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}; + const auto expected = array_exprt{ + array_values, + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; + REQUIRE(result.value() == expected); + const auto expr_result = + expr_initializer(array_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(array_type, test.loc, test.ns); + REQUIRE(result.has_value()); + std::vector array_values{elem_count, from_integer(0, inner_type)}; + const auto expected = array_exprt{ + array_values, + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; + REQUIRE(result.value() == expected); + const auto expr_result = expr_initializer( + array_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + } + + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); + const auto result = + 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)}; + const auto expected = array_exprt{ + array_values, + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; + REQUIRE(result.value() == expected); + } } TEST_CASE( - "nondet_initializer on array of nondet size", + "expr_initializer on array of nondet size", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); typet inner_type = signedbv_typet{8}; typet array_type = array_typet{ inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}; - const auto result = nondet_initializer(array_type, test.loc, test.ns); - REQUIRE(result.has_value()); - const auto expected = side_effect_expr_nondett{ - array_typet{ - inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}, - test.loc}; - REQUIRE(result.value() == expected); + + SECTION("nondet_initializer works") + { + const auto result = nondet_initializer(array_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = side_effect_expr_nondett{ + array_typet{ + inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}, + test.loc}; + REQUIRE(result.value() == expected); + const auto expr_result = + expr_initializer(array_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(array_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected = array_of_exprt{ + from_integer(0, inner_type), + array_typet{ + inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}}; + REQUIRE(result.value() == expected); + const auto expr_result = expr_initializer( + array_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + } + + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); + const auto result = + 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), + array_typet{ + inner_type, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}}; + REQUIRE(result.value() == expected); + } } TEST_CASE( - "nondet_initializer on fixed-size array of fixed-size arrays", + "expr_initializer on fixed-size array of fixed-size arrays", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); @@ -356,26 +503,78 @@ TEST_CASE( array_typet{inner_type, from_integer(elem_count, signedbv_typet{8})}; typet array_type = array_typet{inner_array_type, from_integer(elem_count, signedbv_typet{8})}; - const auto result = nondet_initializer(array_type, test.loc, test.ns); - REQUIRE(result.has_value()); - std::vector inner_array_values{ - elem_count, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}; - const auto inner_expected = array_exprt{ - inner_array_values, - array_typet{ - signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; - std::vector array_values{elem_count, inner_expected}; - const auto expected = array_exprt{ - array_values, - array_typet{ + + SECTION("nondet_initializer works") + { + const auto result = nondet_initializer(array_type, test.loc, test.ns); + REQUIRE(result.has_value()); + std::vector inner_array_values{ + elem_count, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}; + const auto inner_expected = array_exprt{ + inner_array_values, + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; + std::vector array_values{elem_count, inner_expected}; + const auto expected = array_exprt{ + array_values, + array_typet{ + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}, + from_integer(elem_count, signedbv_typet{8})}}; + REQUIRE(result.value() == expected); + const auto expr_result = + expr_initializer(array_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(array_type, test.loc, test.ns); + REQUIRE(result.has_value()); + std::vector inner_array_values{ + elem_count, from_integer(0, inner_type)}; + const auto inner_expected = array_exprt{ + inner_array_values, + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; + std::vector array_values{elem_count, inner_expected}; + const auto expected = array_exprt{ + array_values, array_typet{ - signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}, - from_integer(elem_count, signedbv_typet{8})}}; - REQUIRE(result.value() == expected); + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}, + from_integer(elem_count, signedbv_typet{8})}}; + REQUIRE(result.value() == expected); + const auto expr_result = expr_initializer( + array_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); + const auto result = + 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)}; + const auto inner_expected = array_exprt{ + inner_array_values, + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}}; + std::vector array_values{elem_count, inner_expected}; + const auto expected = array_exprt{ + array_values, + array_typet{ + array_typet{ + signedbv_typet{8}, from_integer(elem_count, signedbv_typet{8})}, + from_integer(elem_count, signedbv_typet{8})}}; + REQUIRE(result.value() == expected); + } } TEST_CASE( - "nondet_initializer nested struct type", + "expr_initializer on nested struct type", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); @@ -385,30 +584,98 @@ TEST_CASE( const struct_union_typet::componentst struct_components{ {"fizz", bool_typet{}}, {"bar", inner_struct_type}}; const struct_typet struct_type{struct_components}; - const auto result = nondet_initializer(struct_type, test.loc, test.ns); - REQUIRE(result.has_value()); - const exprt::operandst expected_inner_struct_fields{ - side_effect_expr_nondett{signedbv_typet{32}, test.loc}, - side_effect_expr_nondett{unsignedbv_typet{16}, test.loc}}; - const struct_exprt expected_inner_struct_expr{ - expected_inner_struct_fields, inner_struct_type}; - const exprt::operandst expected_struct_fields{ - side_effect_expr_nondett{bool_typet{}, test.loc}, - expected_inner_struct_expr}; - const struct_exprt expected_struct_expr{expected_struct_fields, struct_type}; - REQUIRE(result.value() == expected_struct_expr); - - const auto inner_struct_tag_type = - create_tag_populate_env(inner_struct_type, test.symbol_table); - const auto tag_result = - nondet_initializer(inner_struct_tag_type, test.loc, test.ns); - REQUIRE(tag_result.has_value()); - const struct_exprt expected_inner_struct_tag_expr{ - expected_inner_struct_fields, inner_struct_tag_type}; - REQUIRE(tag_result.value() == expected_inner_struct_tag_expr); + SECTION("nondet_initializer works") + { + const auto result = nondet_initializer(struct_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const exprt::operandst expected_inner_struct_fields{ + side_effect_expr_nondett{signedbv_typet{32}, test.loc}, + side_effect_expr_nondett{unsignedbv_typet{16}, test.loc}}; + const struct_exprt expected_inner_struct_expr{ + expected_inner_struct_fields, inner_struct_type}; + const exprt::operandst expected_struct_fields{ + side_effect_expr_nondett{bool_typet{}, test.loc}, + expected_inner_struct_expr}; + const struct_exprt expected_struct_expr{ + expected_struct_fields, struct_type}; + REQUIRE(result.value() == expected_struct_expr); + const auto expr_result = + expr_initializer(struct_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + + const auto struct_tag_type = + create_tag_populate_env(struct_type, test.symbol_table); + const auto tag_result = + nondet_initializer(struct_tag_type, test.loc, test.ns); + REQUIRE(tag_result.has_value()); + const struct_exprt expected_struct_tag_expr{ + expected_struct_fields, struct_tag_type}; + REQUIRE(tag_result.value() == expected_struct_tag_expr); + const auto tag_expr_result = + expr_initializer(struct_tag_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(tag_expr_result == tag_result); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(struct_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const exprt::operandst expected_inner_struct_fields{ + from_integer(0, signedbv_typet{32}), + from_integer(0, unsignedbv_typet{16})}; + const struct_exprt expected_inner_struct_expr{ + expected_inner_struct_fields, inner_struct_type}; + const exprt::operandst expected_struct_fields{ + from_integer(0, bool_typet{}), expected_inner_struct_expr}; + const struct_exprt expected_struct_expr{ + expected_struct_fields, struct_type}; + REQUIRE(result.value() == expected_struct_expr); + const auto expr_result = expr_initializer( + struct_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + + const auto struct_tag_type = + create_tag_populate_env(struct_type, test.symbol_table); + const auto tag_result = + zero_initializer(struct_tag_type, test.loc, test.ns); + REQUIRE(tag_result.has_value()); + const struct_exprt expected_struct_tag_expr{ + expected_struct_fields, struct_tag_type}; + REQUIRE(tag_result.value() == expected_struct_tag_expr); + const auto tag_expr_result = expr_initializer( + struct_tag_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(tag_expr_result == tag_result); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); + const auto result = + 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})}; + 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}; + const struct_exprt expected_struct_expr{ + expected_struct_fields, struct_type}; + REQUIRE(result.value() == expected_struct_expr); + + const auto struct_tag_type = + create_tag_populate_env(struct_type, test.symbol_table); + const auto tag_result = + expr_initializer(struct_tag_type, test.loc, test.ns, init_value); + REQUIRE(tag_result.has_value()); + const struct_exprt expected_struct_tag_expr{ + expected_struct_fields, struct_tag_type}; + REQUIRE(tag_result.value() == expected_struct_tag_expr); + } } -TEST_CASE("nondet_initializer union type", "[core][util][expr_initializer]") +TEST_CASE("expr_initializer on union type", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); const struct_union_typet::componentst inner_struct_components{ @@ -422,25 +689,77 @@ TEST_CASE("nondet_initializer union type", "[core][util][expr_initializer]") array_typet{signedbv_typet{8}, from_integer(8, signedbv_typet{8})}}, {"struct", inner_struct_type}}; const union_typet union_type{union_components}; - const auto result = nondet_initializer(union_type, test.loc, test.ns); - REQUIRE(result.has_value()); - const union_exprt expected_union{ - "foo", side_effect_expr_nondett{signedbv_typet{256}, test.loc}, union_type}; - REQUIRE(result.value() == expected_union); - - const auto union_tag_type = - create_tag_populate_env(union_type, test.symbol_table); - const auto tag_result = nondet_initializer(union_tag_type, test.loc, test.ns); - REQUIRE(tag_result.has_value()); - const union_exprt expected_union_tag{ - "foo", - side_effect_expr_nondett{signedbv_typet{256}, test.loc}, - union_tag_type}; - REQUIRE(tag_result.value() == expected_union_tag); + + SECTION("nondet_initializer works") + { + const auto result = nondet_initializer(union_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const union_exprt expected_union{ + "foo", + side_effect_expr_nondett{signedbv_typet{256}, test.loc}, + union_type}; + REQUIRE(result.value() == expected_union); + + const auto union_tag_type = + create_tag_populate_env(union_type, test.symbol_table); + const auto tag_result = + nondet_initializer(union_tag_type, test.loc, test.ns); + REQUIRE(tag_result.has_value()); + const union_exprt expected_union_tag{ + "foo", + side_effect_expr_nondett{signedbv_typet{256}, test.loc}, + union_tag_type}; + REQUIRE(tag_result.value() == expected_union_tag); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(union_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const union_exprt expected_union{ + "foo", from_integer(0, signedbv_typet{256}), union_type}; + REQUIRE(result.value() == expected_union); + const auto expr_result = expr_initializer( + union_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + + const auto union_tag_type = + create_tag_populate_env(union_type, test.symbol_table); + const auto tag_result = zero_initializer(union_tag_type, test.loc, test.ns); + REQUIRE(tag_result.has_value()); + const union_exprt expected_union_tag{ + "foo", from_integer(0, signedbv_typet{256}), union_tag_type}; + REQUIRE(tag_result.value() == expected_union_tag); + const auto tag_expr_result = expr_initializer( + union_tag_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(*tag_expr_result == *tag_result); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); + const auto result = + 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}; + REQUIRE(result.value() == expected_union); + + const auto union_tag_type = + create_tag_populate_env(union_type, test.symbol_table); + const auto tag_result = + expr_initializer(union_tag_type, test.loc, test.ns, init_value); + REQUIRE(tag_result.has_value()); + const union_exprt expected_union_tag{ + "foo", + duplicate_per_byte(init_value, signedbv_typet{256}), + union_tag_type}; + REQUIRE(tag_result.value() == expected_union_tag); + } } TEST_CASE( - "nondet_initializer union type with nondet sized array (fails)", + "expr_initializer on union type with nondet sized array (fails)", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); @@ -451,16 +770,68 @@ TEST_CASE( signedbv_typet{8}, side_effect_expr_nondett{signedbv_typet{8}, test.loc}}}}; const union_typet union_type{union_components}; - const auto result = nondet_initializer(union_type, test.loc, test.ns); - REQUIRE_FALSE(result.has_value()); + + SECTION("nondet_initializer fails correctly") + { + const auto result = nondet_initializer(union_type, test.loc, test.ns); + REQUIRE_FALSE(result.has_value()); + const auto expr_result = + expr_initializer(union_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(union_type, test.loc, test.ns); + REQUIRE_FALSE(result.has_value()); + const auto expr_result = expr_initializer( + union_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); + const auto result = + expr_initializer(union_type, test.loc, test.ns, init_value); + REQUIRE_FALSE(result.has_value()); + } } -TEST_CASE("nondet_initializer string type", "[core][util][expr_initializer]") +TEST_CASE("expr_initializer on string type", "[core][util][expr_initializer]") { auto test = expr_initializer_test_environmentt::make(); const string_typet string_type{}; - const auto result = nondet_initializer(string_type, test.loc, test.ns); - REQUIRE(result.has_value()); - const side_effect_expr_nondett expected_string{string_typet{}, test.loc}; - REQUIRE(result.value() == expected_string); + + SECTION("nondet_initializer works") + { + const auto result = nondet_initializer(string_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const side_effect_expr_nondett expected_string{string_typet{}, test.loc}; + REQUIRE(result.value() == expected_string); + const auto expr_result = + expr_initializer(string_type, test.loc, test.ns, exprt(ID_nondet)); + REQUIRE(expr_result == result); + } + + SECTION("zero_initializer works") + { + const auto result = zero_initializer(string_type, test.loc, test.ns); + REQUIRE(result.has_value()); + const auto expected_string = constant_exprt{irep_idt(), string_typet{}}; + REQUIRE(result.value() == expected_string); + const auto expr_result = expr_initializer( + string_type, test.loc, test.ns, constant_exprt(ID_0, char_type())); + REQUIRE(expr_result == result); + } + SECTION("expr_initializer calls duplicate_per_byte") + { + const exprt init_value = + from_integer(0xAB, signedbv_typet{config.ansi_c.char_width}); + 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); + REQUIRE(result.value() == expected_string); + } }