Value set dereferencing: do not treat struct prefixes as equal

Two distinct struct types cannot be cast between, even when one is a
prefix of the other. Value set dereferencing taking this approach just
resulted in propositional encoding producing a warning about invalid
type casts.

Author: tautschnig

jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc

@@ -0,0 +1,24 @@
+struct T
+{
+  // intentionally empty to trigger is_prefix_of code (empty structs, however,
+  // are a GCC-only feature)
+};
+
+struct S
+{
+  struct T t;
+  int other;
+};
+
+void foo(struct S s2)
+{
+  struct T *p = &s2.t;
+  struct T t2 = *p;
+  __CPROVER_assert(0, "");
+}
+
+int main()
+{
+  struct S s;
+  foo(s);
+}

regression/cbmc/struct2/main.c

@@ -0,0 +1,11 @@
+CORE gcc-only no-new-smt
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test must not generate a warning about typecasts (between different struct
+types) being ignored.

regression/cbmc/struct2/test.desc

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+struct a
+{
+  int x;
+};
+struct b
+{
+  struct a p;
+  int y;
+};
+
+int f00(struct a *ptr)
+{
+  return ptr->x;
+}
+
+int main()
+{
+  struct b z = {{1}, 2};
+
+  assert(&z == &(z.p));
+  assert(&z == &(z.p.x));
+
+  assert(f00(&z) == z.p.x);
+
+  return 0;
+}

regression/cbmc/struct5/main.c

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/struct5/test.desc

@@ -71,6 +71,34 @@ bool is_object_field_element(const exprt &expr)
     return false;
 }
 
+/// Returns true if struct \p a is a prefix of \p b, i.e., if this struct has
+/// n components then the component types and names of this struct must match
+/// the first n components of \p b.
+/// \param a: Struct type that may be a prefix.
+/// \param b: Struct type to compare with.
+static bool struct_is_prefix_of(const struct_typet &a, const struct_typet &b)
+{
+  const struct_typet::componentst &ot_components = b.components();
+  const struct_typet::componentst &tt_components = a.components();
+
+  if(ot_components.size() < tt_components.size())
+    return false;
+
+  struct_typet::componentst::const_iterator ot_it = ot_components.begin();
+
+  for(const auto &tt_c : tt_components)
+  {
+    if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
+    {
+      return false; // they just don't match
+    }
+
+    ot_it++;
+  }
+
+  return true; // ok, a is a prefix of b
+}
+
 bool prefix_of(const typet &a, const typet &b, const namespacet &ns)
 {
   if(a == b)
@@ -88,7 +116,8 @@ bool prefix_of(const typet &a, const typet &b, const namespacet &ns)
   const auto &a_struct = to_struct_type(a);
   const auto &b_struct = to_struct_type(b);
 
-  return a_struct.is_prefix_of(b_struct) || b_struct.is_prefix_of(a_struct);
+  return struct_is_prefix_of(a_struct, b_struct) ||
+         struct_is_prefix_of(b_struct, a_struct);
 }
 
 static std::optional<object_address_exprt> find_object(const exprt &expr)

src/cprover/may_alias.cpp

@@ -372,22 +372,6 @@ bool value_set_dereferencet::dereference_type_compare(
   if(object_type == dereference_type)
     return true; // ok, they just match
 
-  // check for struct prefixes
-  const typet &ot_base = object_type.id() == ID_struct_tag
-                           ? ns.follow_tag(to_struct_tag_type(object_type))
-                           : object_type;
-  const typet &dt_base = dereference_type.id() == ID_struct_tag
-                           ? ns.follow_tag(to_struct_tag_type(dereference_type))
-                           : dereference_type;
-
-  if(ot_base.id()==ID_struct &&
-     dt_base.id()==ID_struct)
-  {
-    if(to_struct_type(dt_base).is_prefix_of(
-         to_struct_type(ot_base)))
-      return true; // ok, dt is a prefix of ot
-  }
-
   // we are generous about code pointers
   if(dereference_type.id()==ID_code &&
      object_type.id()==ID_code)

src/pointer-analysis/value_set_dereference.cpp

@@ -112,35 +112,6 @@ struct_typet::get_base(const irep_idt &id) const
   return {};
 }
 
-/// Returns true if the struct is a prefix of \a other, i.e., if this struct
-/// has n components then the component types and names of this struct must
-/// match the first n components of \a other struct.
-/// \param other: Struct type to compare with.
-bool struct_typet::is_prefix_of(const struct_typet &other) const
-{
-  const componentst &ot_components=other.components();
-  const componentst &tt_components=components();
-
-  if(ot_components.size()<
-     tt_components.size())
-    return false;
-
-  componentst::const_iterator
-    ot_it=ot_components.begin();
-
-  for(const auto &tt_c : tt_components)
-  {
-    if(ot_it->type() != tt_c.type() || ot_it->get_name() != tt_c.get_name())
-    {
-      return false; // they just don't match
-    }
-
-    ot_it++;
-  }
-
-  return true; // ok, *this is a prefix of ot
-}
-
 /// Returns true if the type is a reference.
 bool is_reference(const typet &type)
 {

src/util/std_types.cpp

@@ -239,8 +239,6 @@ class struct_typet:public struct_union_typet
   {
   }
 
-  bool is_prefix_of(const struct_typet &other) const;
-
   /// A struct may be a class, where members may have access restrictions.
   bool is_class() const
   {