From f14572bdcad8d8a7075eb966049bf20ca9090dc5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 1 Mar 2021 12:20:54 +0000
Subject: [PATCH] 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.
---
 .../test_no_simplify_vccs.desc                | 11 -------
 regression/cbmc/struct2/main.c                | 24 +++++++++++++++
 regression/cbmc/struct2/test.desc             | 11 +++++++
 .../value_set_dereference.cpp                 | 13 ---------
 src/util/std_types.cpp                        | 29 -------------------
 src/util/std_types.h                          |  2 --
 6 files changed, 35 insertions(+), 55 deletions(-)
 delete mode 100644 jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc
 create mode 100644 regression/cbmc/struct2/main.c
 create mode 100644 regression/cbmc/struct2/test.desc

diff --git a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc b/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc
deleted file mode 100644
index 74fb1af96136..000000000000
--- a/jbmc/regression/jbmc/simplify-classid-of-interface/test_no_simplify_vccs.desc
+++ /dev/null
@@ -1,11 +0,0 @@
-CORE
-Test
---function Test.main --no-simplify --unwind 10 --show-vcc
-^EXIT=0$
-^SIGNAL=0$
-"java::Impl1" = cast\(\{ \{ "java::Impl1" \}, 0 \}, struct (\{ struct \{ string @class_identifier \} @java.lang.Object \}|java::Intf)\)\.@java.lang.Object\.@class_identifier
---
-^warning: ignoring
---
-This checks that the test generates the VCC testing the class-id that we're
-intending to simplify away in the main test.
diff --git a/regression/cbmc/struct2/main.c b/regression/cbmc/struct2/main.c
new file mode 100644
index 000000000000..0f2c38670328
--- /dev/null
+++ b/regression/cbmc/struct2/main.c
@@ -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);
+}
diff --git a/regression/cbmc/struct2/test.desc b/regression/cbmc/struct2/test.desc
new file mode 100644
index 000000000000..f46890667749
--- /dev/null
+++ b/regression/cbmc/struct2/test.desc
@@ -0,0 +1,11 @@
+CORE gcc-only broken-smt-backend
+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.
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 0e994f8ba4d3..0f66829b17da 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -359,19 +359,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=ns.follow(object_type),
-              dt_base=ns.follow(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)
diff --git a/src/util/std_types.cpp b/src/util/std_types.cpp
index 62c7c72a3f5d..72cb782d4217 100644
--- a/src/util/std_types.cpp
+++ b/src/util/std_types.cpp
@@ -114,35 +114,6 @@ optionalt<struct_typet::baset> 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)
 {
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 8641c0aee721..e639a8644e1e 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -234,8 +234,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
   {