Merge pull request #3725 from tautschnig/simplify-after-deref

Symex-dereference: simplify after deref [blocks: #2574, #4056]

Author: tautschnig

jbmc/regression/jbmc-generics/constant_propagation/Generic.class

@@ -0,0 +1,27 @@
+public class Test {
+  public static void main() {
+    Generic<Integer> g = new GenericSub<Integer>();
+
+    int x = 0;
+    for(int i = 0; i < 1000; ++i)
+      x += g.get();
+
+    assert x == 0;
+  }
+}
+
+class Generic<T> {
+  T key;
+  int x;
+
+  public int get() { return 0; }
+
+  public Generic() {
+    key = null;
+    x = 5;
+  }
+}
+
+class GenericSub<S> extends Generic<S> {
+  public int get() { return x; }
+}

jbmc/regression/jbmc-generics/constant_propagation/GenericSub.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.main --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+^\{-\d+\} symex_dynamic::dynamic_object1#3 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object1#4 = \{ \{ \{ "java::GenericSub" \}, NULL, 5 \} \}$
+--
+byte_extract_(big|little)_endian
+--
+The use of generics should not result in any byte_extract operations being
+generated for this test.

jbmc/regression/jbmc-generics/constant_propagation/Test.class

@@ -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.

jbmc/regression/jbmc-generics/constant_propagation/Test.java

@@ -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>
 
@@ -363,4 +364,30 @@ void goto_symext::dereference(exprt &expr, statet &state)
   // dereferencing may introduce new symbol_exprt
   // (like __CPROVER_memory)
   expr = state.rename<L1>(std::move(l1_expr), ns);
+
+  // Dereferencing is likely to introduce new member-of-if constructs --
+  // for example, "x->field" may have become "(x == &o1 ? o1 : o2).field."
+  // Run expression simplification, which converts that to
+  // (x == &o1 ? o1.field : o2.field))
+  // before applying field sensitivity. Field sensitivity can then turn such
+  // field-of-symbol expressions into atomic SSA expressions instead of having
+  // to rewrite all of 'o1' otherwise.
+  // Even without field sensitivity this can be beneficial: for example,
+  // "(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);
+
+  if(symex_config.run_validation_checks)
+  {
+    // 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");
+  }
 }