Merge pull request #7015 from thomasspriggs/tas/fix_object_tracking_test

Fix SMT object tracking test

Author: thomasspriggs

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -1,8 +1,8 @@
 // Author: Diffblue Ltd.
 
+#include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/namespace.h>
-#include <util/optional.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -12,6 +12,84 @@
 #include <string>
 #include <utility>
 
+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};