From 71fc87db1a3e1ec53e6f3f4494e1a37c5cc58c4a Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 14 Dec 2018 16:43:14 +0000
Subject: [PATCH 1/3] get_subexpression_at_offset: use typecast_exprt for
 pointer-to-pointer casts

This signals that the cast is cleaner than a general byte-extract a little more clearly
---
 src/util/pointer_offset_size.cpp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 800cb58d8d1..a7d2af922b2 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -655,6 +655,13 @@ exprt get_subexpression_at_offset(
     return result;
   }
 
+  if(
+    offset_bytes == 0 && expr.type().id() == ID_pointer &&
+    target_type_raw.id() == ID_pointer)
+  {
+    return typecast_exprt(expr, target_type_raw);
+  }
+
   const typet &source_type = ns.follow(expr.type());
   const auto target_size_bits = pointer_offset_bits(target_type_raw, ns);
   if(!target_size_bits.has_value())

From c1314aec5807a80194b7e7f803d780fbe4269cb6 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 14 Dec 2018 16:44:47 +0000
Subject: [PATCH 2/3] Value-set: replace unsound typecast simplification with
 simplify_expr

Previously this would simplify ((struct A)x).y into x.y regardless of whether the two
structures both have a member y, or whether it is colocated in the two types. Now that
the simplifier can soundly simplify such an expression we should just use that instead.
---
 src/pointer-analysis/value_set.cpp | 35 ++++--------------------------
 1 file changed, 4 insertions(+), 31 deletions(-)

diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index f8ba7a82ce3..bfad48312d8 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -1630,37 +1630,10 @@ exprt value_sett::make_member(
   const struct_union_typet &struct_union_type=
     to_struct_union_type(ns.follow(src.type()));
 
-  if(src.id()==ID_struct ||
-     src.id()==ID_constant)
-  {
-    std::size_t no=struct_union_type.component_number(component_name);
-    assert(no<src.operands().size());
-    return src.operands()[no];
-  }
-  else if(src.id()==ID_with)
-  {
-    assert(src.operands().size()==3);
-
-    // see if op1 is the member we want
-    const exprt &member_operand=src.op1();
-
-    if(component_name==member_operand.get(ID_component_name))
-      // yes! just take op2
-      return src.op2();
-    else
-      // no! do this recursively
-      return make_member(src.op0(), component_name, ns);
-  }
-  else if(src.id()==ID_typecast)
-  {
-    // push through typecast
-    assert(src.operands().size()==1);
-    return make_member(src.op0(), component_name, ns);
-  }
-
-  // give up
   const typet &subtype = struct_union_type.component_type(component_name);
-  member_exprt member_expr(src, component_name, subtype);
+  exprt member_expr = member_exprt(src, component_name, subtype);
+
+  simplify(member_expr, ns);
 
-  return std::move(member_expr);
+  return member_expr;
 }

From 8d88c9776d3cb838ca1f209417f9c26bc9a09272 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 14 Dec 2018 16:51:39 +0000
Subject: [PATCH 3/3] Enable previously-failing test
 Linking7/member-name-mismatch

Now that value-set soundly simplifies member-of-cast-of-struct, this test works as expected.
This also improves the specificity of the two tests in this directory.

This is disabled under SMT2 for the same reason as the existing test.desc -- it involves a
struct-to-struct cast, which SMT2's `convert_typecast` doesn't handle yet.
---
 regression/cbmc/Linking7/member-name-mismatch.desc | 6 +++---
 regression/cbmc/Linking7/test.desc                 | 2 ++
 scripts/delete_failing_smt2_solver_tests           | 1 +
 3 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc
index ff30eee14c6..603d759e8d8 100644
--- a/regression/cbmc/Linking7/member-name-mismatch.desc
+++ b/regression/cbmc/Linking7/member-name-mismatch.desc
@@ -1,11 +1,11 @@
-KNOWNBUG
+CORE
 main.c
 module2.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.c == 41: FAILURE
 ^\*\* 1 of 2 failed
 --
 ^warning: ignoring
---
-This is either a bug in goto-symex or value_sett (where the invariant fails).
diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc
index 4eaef880405..7e8989049b8 100644
--- a/regression/cbmc/Linking7/test.desc
+++ b/regression/cbmc/Linking7/test.desc
@@ -5,5 +5,7 @@ module.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 ^\*\* 1 of 2 failed
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.b == 41: FAILURE
 --
 ^warning: ignoring
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
index f20aa252c73..1051bdc108d 100755
--- a/scripts/delete_failing_smt2_solver_tests
+++ b/scripts/delete_failing_smt2_solver_tests
@@ -36,6 +36,7 @@ rm Float6/test.desc
 rm Float8/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
+rm Linking7/member-name-mismatch.desc
 rm Malloc19/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc