diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 4617580ec4b..69189591e66 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -1,8 +1,8 @@ // Author: Diffblue Ltd. +#include #include #include -#include #include #include @@ -12,6 +12,84 @@ #include #include +TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") +{ + const std::size_t pointer_bits = 64; + SECTION("Address of symbol") + { + // Constructed address of expression should be equivalent to the following + // C expression - `&base`. + const typet base_type = unsignedbv_typet{8}; + const symbol_exprt object_base{"base", base_type}; + const address_of_exprt address_of{ + object_base, pointer_typet{base_type, pointer_bits}}; + INFO("Address of expression is: " + address_of.pretty(2, 0)); + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of index") + { + // Constructed address of expression should be equivalent to the following + // C expression - `&(base[index])`. + const unsignedbv_typet element_type{8}; + const signedbv_typet index_type{pointer_bits}; + const array_typet base_type{element_type, from_integer(42, index_type)}; + const symbol_exprt object_base{"base", base_type}; + const symbol_exprt index{"index", index_type}; + const pointer_typet pointer_type{element_type, pointer_bits}; + const address_of_exprt address_of{ + index_exprt{object_base, index}, pointer_type}; + INFO("Address of expression is: " + address_of.pretty(2, 0)); + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of struct member") + { + // Constructed address of expression should be equivalent to the following + // C expression - `&(base.baz)`. + const struct_tag_typet base_type{"structt"}; + const symbol_exprt object_base{"base", base_type}; + const unsignedbv_typet member_type{8}; + const address_of_exprt address_of{ + member_exprt{object_base, "baz", member_type}, + pointer_typet{member_type, pointer_bits}}; + INFO("Address of expression is: " + address_of.pretty(2, 0)); + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of index of struct member") + { + // Constructed address of expression should be equivalent to the following + // C expression - `&(base.baz[index])`. + const struct_tag_typet base_type{"structt"}; + const symbol_exprt object_base{"base", base_type}; + + const unsignedbv_typet element_type{8}; + const signedbv_typet index_type{pointer_bits}; + const array_typet member_type{element_type, from_integer(42, index_type)}; + const symbol_exprt index{"index", index_type}; + + const address_of_exprt address_of{ + index_exprt{member_exprt{object_base, "baz", member_type}, index}, + pointer_typet{element_type, pointer_bits}}; + INFO("Address of expression is: " + address_of.pretty(2, 0)); + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of struct member at index") + { + // Constructed address of expression should be equivalent to the following + // C expression - `&(base[index].qux)`. + const struct_tag_typet element_type{"struct_elementt"}; + const signedbv_typet index_type{pointer_bits}; + const array_typet base_type{element_type, from_integer(42, index_type)}; + const symbol_exprt object_base{"base", base_type}; + const symbol_exprt index{"index", index_type}; + const unsignedbv_typet member_type{8}; + const address_of_exprt address_of{ + member_exprt{index_exprt{object_base, index}, "qux", member_type}, + pointer_typet{member_type, pointer_bits}}; + INFO("Address of expression is: " + address_of.pretty(2, 0)); + CHECK(find_object_base_expression(address_of) == object_base); + } +} + TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]") { const typet base_type = pointer_typet{signedbv_typet{16}, 18};