Symex-dereference: simplify after deref

This is generally useful because it turns member-of-if into if-of-member, which
avoids repeatedly quoting large complex if expressions in a with_exprt, but it
is especially good for field sensitivity as it puts member expressions directly
on top of symbol expressions, which field sensitivity knows how to deal with.

Author: smowton

regression/cbmc/Pointer_byte_extract4/program-only.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+: dynamic_object1#\d+\) WITH
+--
+The above pattern makes sure we don't have a conditional choice of objects
+within a "with" expression. We avoid having this by running the simplifier after
+dereferencing.

src/goto-symex/symex_dereference.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/exception_utils.h>
+#include <util/expr_util.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 
@@ -389,4 +390,23 @@ void goto_symext::dereference(
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
   state.rename(expr, ns, goto_symex_statet::L1);
+
+  // dereferencing is likely to introduce new member-of-if constructs --
+  // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field"
+  // Simplify (which converts that to (x == &o1 ? o1.field : o2.field)) before
+  // applying field sensitivity, which can turn such field-of-symbol expressions
+  // into atomic SSA expressions, but would have to rewrite all of 'o1'
+  // otherwise.
+  // make the structure of the lhs as simple as possible to avoid,
+  // Similarly, (b ? s1 : s2).member=X results in
+  // (b ? s1 : s2)=(b ? s1 : s2) with member:=X and then
+  // s1=b ? ((b ? s1 : s2) with member:=X) : s1
+  // when all we need is
+  // s1=s1 with member:=X [and guard b]
+  // s2=s2 with member:=X [and guard !b]
+  do_simplify(expr);
+  // make sure simplify has not re-introduced any dereferencing that
+  // had previously been cleaned away
+  INVARIANT(
+    !has_subexpr(expr, ID_dereference), "simplify re-introduced dereferencing");
 }