From 6f1322bc9204f4c894bb58239fd87aecd0f26da6 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 18 Jul 2022 19:27:29 +0100 Subject: [PATCH 1/5] Revert removal of `find_object_base_expression` test This test was removed due to incompatibility with new INVARIANT in the constuctor of member_exprt, which now checks that member is being accessed on a struct/union typed operand. This commit adds the test back as a precursor to making it compatible with the new INVARIANT. --- .../smt2_incremental/object_tracking.cpp | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 4617580ec4b..a958298472d 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -12,6 +12,36 @@ #include #include +TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") +{ + const typet base_type = pointer_typet{unsignedbv_typet{8}, 18}; + const symbol_exprt object_base{"base", base_type}; + const symbol_exprt index{"index", base_type}; + const pointer_typet pointer_type{base_type, 12}; + std::string description; + optionalt address_of; + using rowt = std::pair; + std::tie(description, address_of) = GENERATE_REF( + rowt{"Address of symbol", {object_base, pointer_type}}, + rowt{"Address of index", {index_exprt{object_base, index}, pointer_type}}, + rowt{ + "Address of struct member", + {member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}}, + rowt{ + "Address of index of struct member", + {index_exprt{member_exprt{object_base, "baz", base_type}, index}, + pointer_type}}, + rowt{ + "Address of struct member at index", + {member_exprt{ + index_exprt{object_base, index}, "baz", unsignedbv_typet{8}}, + pointer_type}}); + SECTION(description) + { + 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}; From 76915e35a146bab3bfbdbafa1a8ad959764736bf Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 19 Jul 2022 11:27:28 +0100 Subject: [PATCH 2/5] Refactor to replace `GENERATE` with separate `SECTION`s To fix this test, more appropriate type information needs to be added. This will result in differing object_base types for each check. This will be simpler to write in sections rather than `GENERATE` rows. --- .../smt2_incremental/object_tracking.cpp | 50 +++++++++++-------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index a958298472d..2bb4c70aad0 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -2,7 +2,6 @@ #include #include -#include #include #include @@ -18,27 +17,36 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") const symbol_exprt object_base{"base", base_type}; const symbol_exprt index{"index", base_type}; const pointer_typet pointer_type{base_type, 12}; - std::string description; - optionalt address_of; - using rowt = std::pair; - std::tie(description, address_of) = GENERATE_REF( - rowt{"Address of symbol", {object_base, pointer_type}}, - rowt{"Address of index", {index_exprt{object_base, index}, pointer_type}}, - rowt{ - "Address of struct member", - {member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}}, - rowt{ - "Address of index of struct member", - {index_exprt{member_exprt{object_base, "baz", base_type}, index}, - pointer_type}}, - rowt{ - "Address of struct member at index", - {member_exprt{ - index_exprt{object_base, index}, "baz", unsignedbv_typet{8}}, - pointer_type}}); - SECTION(description) + SECTION("Address of symbol") { - CHECK(find_object_base_expression(*address_of) == object_base); + const address_of_exprt address_of{object_base, pointer_type}; + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of index") + { + const address_of_exprt address_of{ + index_exprt{object_base, index}, pointer_type}; + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of struct member") + { + const address_of_exprt address_of{ + member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}; + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of index of struct member") + { + const address_of_exprt address_of{ + index_exprt{member_exprt{object_base, "baz", base_type}, index}, + pointer_type}; + CHECK(find_object_base_expression(address_of) == object_base); + } + SECTION("Address of struct member at index") + { + const address_of_exprt address_of{ + member_exprt{index_exprt{object_base, index}, "baz", unsignedbv_typet{8}}, + pointer_type}; + CHECK(find_object_base_expression(address_of) == object_base); } } From 0304a01b7cb997ccd51be57a9519ebf4d51c6ae7 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 19 Jul 2022 15:06:08 +0100 Subject: [PATCH 3/5] Add valid type information to test So that it is compatible with the new INVARIANT in the constructor of `member_exprt`. --- .../smt2_incremental/object_tracking.cpp | 45 ++++++++++++++----- 1 file changed, 35 insertions(+), 10 deletions(-) diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 2bb4c70aad0..635a70529d2 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -1,5 +1,6 @@ // Author: Diffblue Ltd. +#include #include #include #include @@ -13,39 +14,63 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") { - const typet base_type = pointer_typet{unsignedbv_typet{8}, 18}; - const symbol_exprt object_base{"base", base_type}; - const symbol_exprt index{"index", base_type}; - const pointer_typet pointer_type{base_type, 12}; + const std::size_t pointer_bits = 64; SECTION("Address of symbol") { - const address_of_exprt address_of{object_base, pointer_type}; + 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}}; CHECK(find_object_base_expression(address_of) == object_base); } SECTION("Address of 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}; CHECK(find_object_base_expression(address_of) == object_base); } SECTION("Address of struct member") { + 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", unsignedbv_typet{8}}, pointer_type}; + member_exprt{object_base, "baz", member_type}, + pointer_typet{member_type, pointer_bits}}; CHECK(find_object_base_expression(address_of) == object_base); } SECTION("Address of index of struct member") { + 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", base_type}, index}, - pointer_type}; + index_exprt{member_exprt{object_base, "baz", member_type}, index}, + pointer_typet{element_type, pointer_bits}}; CHECK(find_object_base_expression(address_of) == object_base); } SECTION("Address of struct member at index") { + 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}, "baz", unsignedbv_typet{8}}, - pointer_type}; + member_exprt{index_exprt{object_base, index}, "qux", member_type}, + pointer_typet{member_type, pointer_bits}}; CHECK(find_object_base_expression(address_of) == object_base); } } From b15fe4eaf8b6fffbdc104592e29c998ed89af097 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 19 Jul 2022 15:24:06 +0100 Subject: [PATCH 4/5] Add extra information to `find_object_base_expression` test To make it easier to debug. --- unit/solvers/smt2_incremental/object_tracking.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 635a70529d2..238dbbab8a8 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -21,6 +21,7 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") 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") @@ -33,6 +34,7 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") 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") @@ -43,6 +45,7 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") 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") @@ -58,6 +61,7 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") 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") @@ -71,6 +75,7 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") 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); } } From de250f9c955056a64b4209d70f53f5e330a8a810 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 19 Jul 2022 15:28:46 +0100 Subject: [PATCH 5/5] Add comment on constructed expression as C source expressions To make the intention of each test section clearer. --- unit/solvers/smt2_incremental/object_tracking.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp index 238dbbab8a8..69189591e66 100644 --- a/unit/solvers/smt2_incremental/object_tracking.cpp +++ b/unit/solvers/smt2_incremental/object_tracking.cpp @@ -17,6 +17,8 @@ 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{ @@ -26,6 +28,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") } 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)}; @@ -39,6 +43,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") } 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}; @@ -50,6 +56,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") } 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}; @@ -66,6 +74,8 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]") } 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)};