diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp index ef6275963b4..4804fbfcdb7 100644 --- a/src/util/expr_initializer.cpp +++ b/src/util/expr_initializer.cpp @@ -12,12 +12,13 @@ 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" -template class expr_initializert { public: @@ -25,10 +26,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 +39,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,10 +61,12 @@ 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); + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -69,10 +75,12 @@ 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); + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -81,15 +89,17 @@ 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'); result = constant_exprt(value, type); } + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -97,17 +107,19 @@ 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 {}; 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; @@ -127,8 +139,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 +149,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 +171,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 +202,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 +229,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 +243,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 +256,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 +269,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,10 +282,12 @@ 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); + else + result = duplicate_per_byte(init_expr, type); result.add_source_location()=source_location; return result; @@ -292,7 +307,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 +323,91 @@ 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)); +} + +/// 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 `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) +{ + 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 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 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; + // 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( + casted_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 diff --git a/unit/util/expr_initializer.cpp b/unit/util/expr_initializer.cpp index efbda566997..f5f2d5e990c 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,45 +78,312 @@ 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(); + // 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 + 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); + 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") + { + 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( + "expr_initializer on variable-bit unsigned_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 = GENERATE(3, 8, 16, 20); + SECTION( + "Testing with expected type as unsigned_bv of size " + + std::to_string(input_type_size)) + { + 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(); @@ -114,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(); @@ -153,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(); @@ -182,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{ @@ -219,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(); @@ -248,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); + } }