From e52f05d8876fa8c4fe82760bb643093b87a579c5 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Wed, 9 Nov 2022 13:15:43 +0000 Subject: [PATCH] Add unit test of object size tracking Because we were previously missing unit tests for the tracking of object sizes. Note that this test includes tracking for when object sizes are based on symbols rather than statically defined. This is used for dynamically sized objects such as those pointed to by the return value of `malloc`. --- .../smt2_incremental/object_tracking.cpp | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 6ccb1b3ad1e..522fe102265 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -2,6 +2,7 @@ #include #include +#include #include #include #include @@ -157,3 +158,44 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]") CHECK(objects_are_already_tracked(compound_expression, object_map)); } } + +static symbolt make_size_variable() +{ + symbolt size_variable; + size_variable.name = "size_variable"; + size_variable.base_name = "size_variable"; + size_variable.type = size_type(); + return size_variable; +} + +TEST_CASE("Tracking object sizes.", "[core][smt2_incremental]") +{ + // Configuration needs to be performed before tracking because the size_type() + // width depends on the global configuration. + config.ansi_c.mode = configt::ansi_ct::flavourt::GCC; + config.ansi_c.set_arch_spec_x86_64(); + smt_object_mapt object_map = initial_smt_object_map(); + symbol_tablet symbol_table; + const symbolt size_variable = make_size_variable(); + symbol_table.insert(size_variable); + const symbol_exprt size_expr = size_variable.symbol_expr(); + namespacet ns{symbol_table}; + exprt base_object; + exprt expected_size; + using rowt = std::pair; + std::tie(base_object, expected_size) = GENERATE_REF( + rowt{from_integer(0, unsignedbv_typet{(8)}), from_integer(1, size_type())}, + rowt{from_integer(42, signedbv_typet{16}), from_integer(2, size_type())}, + rowt{from_integer(-24, signedbv_typet{32}), from_integer(4, size_type())}, + rowt{from_integer(2, unsignedbv_typet{64}), from_integer(8, size_type())}, + rowt{ + symbol_exprt{"array", array_typet{unsignedbv_typet{8}, size_expr}}, + size_expr}, + rowt{ + symbol_exprt{"array", array_typet{signedbv_typet{32}, size_expr}}, + mult_exprt{size_expr, from_integer(4, size_type())}}); + track_expression_objects(address_of_exprt{base_object}, ns, object_map); + const auto object = object_map.find(base_object); + REQUIRE(object != object_map.end()); + REQUIRE(object->second.size == expected_size); +}