Merge pull request #4949 from smowton/smowton/feature/more-accurate-member-deref

Simplify and apply field sensitivity before value-set-deref

Author: smowton

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

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 &&