From 8ff892778dc640a88486e7b5820bfc8467ea721a Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Thu, 25 Jul 2019 14:04:54 +0100
Subject: [PATCH] Simplify and apply field sensitivity before value-set-deref

This means that any member-of-symbol constructs introduced by a nested dereference,
such as x->y ==> (x == &o1 ? o1 : o2).y, can be simplified to produce e.g.
(x == &o1 ? o1.y : o2.y) ==> (x == &o1 ? o1..y : o2..y). value_set_dereferencet will
then special-case the if-expression, dereferencing the inner o1..y and o2..y individually.
In the best case where each has a single possible alias, &o3 and &o4 respectively, we
end up with (x == &o1 ? &o3 : &o4), rather than the current result:
let p = (x == &o1 ? o1 : o2).y in (p == &o3 ? o3 : o4)
---
 .../double_deref_with_member.desc             |  4 ++--
 src/goto-symex/symex_dereference.cpp          | 24 +++++++++++++++----
 2 files changed, 22 insertions(+), 6 deletions(-)

diff --git a/regression/cbmc/double_deref/double_deref_with_member.desc b/regression/cbmc/double_deref/double_deref_with_member.desc
index e7256d946f2..85156557ba2 100644
--- a/regression/cbmc/double_deref/double_deref_with_member.desc
+++ b/regression/cbmc/double_deref/double_deref_with_member.desc
@@ -1,10 +1,10 @@
 CORE
 double_deref_with_member.c
 --show-vcc
-^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \(main::1::cptr!0@1#2 = address_of\(main::1::container[12]!0@1\) \? address_of\(symex_dynamic::dynamic_object[12]\) : address_of\(symex_dynamic::dynamic_object[12]\)\)
-^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[12]\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1\)
+^\{1\} \(main::1::cptr!0@1#2 = address_of\(main::1::container2!0@1\) \? main::argc!0@1#1 = 2 : main::argc!0@1#1 = 1\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
+derefd_pointer
 --
 See README for details about these tests
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 5489a8df717..bef9746738f 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -223,6 +223,26 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
     // first make sure there are no dereferences in there
     dereference_rec(tmp1, state, false);
 
+    // Depending on the nature of the pointer expression, the recursive deref
+    // operation might have introduced a construct such as
+    // (x == &o1 ? o1 : o2).field, in which case we should simplify to push the
+    // member operator inside the if, then apply field-sensitivity to yield
+    // (x == &o1 ? o1..field : o2..field). value_set_dereferencet can then
+    // apply the dereference operation to each of o1..field and o2..field
+    // independently, as it special-cases the ternary conditional operator.
+    do_simplify(tmp1);
+
+    if(symex_config.run_validation_checks)
+    {
+      // make sure simplify has not re-introduced any dereferencing that
+      // had previously been cleaned away
+      INVARIANT(
+        !has_subexpr(tmp1, ID_dereference),
+        "simplify re-introduced dereferencing");
+    }
+
+    tmp1 = state.field_sensitivity.apply(ns, state, std::move(tmp1), write);
+
     // we need to set up some elaborate call-backs
     symex_dereference_statet symex_dereference_state(state, ns);
 
@@ -241,10 +261,6 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
 
     // this may yield a new auto-object
     trigger_auto_object(expr, state);
-
-    // ...and may have introduced a member-of-symbol construct with a
-    // corresponding SSA symbol:
-    expr = state.field_sensitivity.apply(ns, state, std::move(expr), write);
   }
   else if(
     expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member &&