From 73fadb3c9af7040b23bb56673423df61baf361e9 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 21 Dec 2018 18:07:19 +0000
Subject: [PATCH 1/2] 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.
---
 .../Pointer_byte_extract4/program-only.desc   | 12 +++++++++
 src/goto-symex/symex_dereference.cpp          | 27 +++++++++++++++++++
 2 files changed, 39 insertions(+)
 create mode 100644 regression/cbmc/Pointer_byte_extract4/program-only.desc

diff --git a/regression/cbmc/Pointer_byte_extract4/program-only.desc b/regression/cbmc/Pointer_byte_extract4/program-only.desc
new file mode 100644
index 00000000000..7b738a3b40b
--- /dev/null
+++ b/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.
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 20f65da8854..0a7fd38f956 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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");
+  }
 }

From 0b09ffa61bae058358f94f5e1beaeb5e3b53ece5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 6 Mar 2019 23:06:36 +0000
Subject: [PATCH 2/2] Test to make sure generics do not result in constant
 propagation failure

This was fine with develop with and without simplification after dereferencing,
but would break if removing base_type_eq without adding the simplification step.
---
 .../constant_propagation/Generic.class        | Bin 0 -> 407 bytes
 .../constant_propagation/GenericSub.class     | Bin 0 -> 311 bytes
 .../constant_propagation/Test.class           | Bin 0 -> 615 bytes
 .../constant_propagation/Test.java            |  27 ++++++++++++++++++
 .../constant_propagation/test.desc            |  12 ++++++++
 5 files changed, 39 insertions(+)
 create mode 100644 jbmc/regression/jbmc-generics/constant_propagation/Generic.class
 create mode 100644 jbmc/regression/jbmc-generics/constant_propagation/GenericSub.class
 create mode 100644 jbmc/regression/jbmc-generics/constant_propagation/Test.class
 create mode 100644 jbmc/regression/jbmc-generics/constant_propagation/Test.java
 create mode 100644 jbmc/regression/jbmc-generics/constant_propagation/test.desc

diff --git a/jbmc/regression/jbmc-generics/constant_propagation/Generic.class b/jbmc/regression/jbmc-generics/constant_propagation/Generic.class
new file mode 100644
index 0000000000000000000000000000000000000000..aa709de18f189883cdb7bf65a250ab7c66796dbf
GIT binary patch
literal 407
zcmZWkJx{_=6g`(hOKTOVfXd{E9c0i+35$uwgy=xy-qx3<h$Shl(f{P)KujF`0sbiC
zc{Op6;huNzdFR}ZukVjf0H+u@XrO1Kj=qLH3;Pxh1jd7U5qQ&i_!N#7VU~<;qq&NU
zbAdfelPoOCTu~MTWaOD~%_>m^ad^bMezCl#pfyc1byGe@Di6YFLB<@XSz1gg-JM`K
z4$d~GOg1TjGh3E<tS(dC#tzh~IM(aAXrtr8gyq7)mcY7Fnaa~x(Eh(Z4tZpQm)96{
zK+vozn@Dq&3tVjTXNT2*uV~hICGsAkSuq_V2NSjKgdMf6<-bFGS)=AR*D&7xOdbaV
UyTmSR^l0kS@;lrkuUG2+0K&LJxc~qF

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc-generics/constant_propagation/GenericSub.class b/jbmc/regression/jbmc-generics/constant_propagation/GenericSub.class
new file mode 100644
index 0000000000000000000000000000000000000000..208befc45c16beecd25a6bca582b7d2a58a11325
GIT binary patch
literal 311
zcmZ9HKTE_w5XIjl@nT~1&VPl1U}2#aUSnlK8bLV-T5Pc2#3Af)?m^s$AIe4$1Peca
zAL?*&T%*OjnSJ|v!|u=G>l?r&_G1JXM({BTu^nQEFvyHGE+_b>XAgwndj80SVPP!a
zbx#$yrLJb;_zk-yG$BOFG*-K=75^ktSH)Dn=<!V3W_({wxprw@+_L4?)LE(0JSD_x
z-nBK~n0{AO^0T|>LkZR}NU)1NK~@pfRfKSLAkeGS1jq8|Kt2I@Qj&r|G95{$-Z}pS
jy~{vY7wxZs1JMYv=wI{$-rGO)Q1)(!=OMx7vTywY?a4E(

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc-generics/constant_propagation/Test.class b/jbmc/regression/jbmc-generics/constant_propagation/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..c339d158cf7f461d0a7a3183dbd99502620fccd4
GIT binary patch
literal 615
zcmYLG&rcIU6#m{$cc&ee{-6q#0)iqS2T7D;H5vp$Ks~fEk(1l)q?uB-W_PRqfd7OX
zy>M0&NF>p_e~CBm9?&-%XfN~Tz4yKEec#Nl%kMt`Y+_YGVMd~+;9y4K7G?{`qb@P0
z;MvZ+!UAqfEE1~AL6Yb=HG?R5Zjzwg*Bt^K61;|qO!|Z%*6zP1<hBMKO(-3hNWUB&
zw{_gIU~U`-CL&BW(;z&05xmRF5=(@9BkW&ssODf8hkD1@i9$;!>4RSIKJYP#B0=ry
zNXI5@4%<BF;|}inn1D~HS=2^9h`Jlku61t5@gU~CmPKOO$33hN%46iKc29>XL0-|a
zg|6nDjqI_5F>tHT<_XgsotRj6MjO~lI^+fq9Ab&zPVvK1xn?!-O@Qs9$Y+VOd5*-<
zT|WnXu|Smh^s*wGMP&s2z#k&G_vix7n{$YL(GZX4D&qHNl<Vtf$h~cRbm;WopRaIF
zP^y2z#05M?%Ac0l$%q#q`7T(M%ep*NIiKaY$g3W5Ws18+h)ehqRieMBRv3F@Bw{lY
i22`f<XDFON=1!3l-{6i{Tx+*fE*$@<b$ByVF#R8CKW%jY

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc-generics/constant_propagation/Test.java b/jbmc/regression/jbmc-generics/constant_propagation/Test.java
new file mode 100644
index 00000000000..2c71fc754a0
--- /dev/null
+++ b/jbmc/regression/jbmc-generics/constant_propagation/Test.java
@@ -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; }
+}
diff --git a/jbmc/regression/jbmc-generics/constant_propagation/test.desc b/jbmc/regression/jbmc-generics/constant_propagation/test.desc
new file mode 100644
index 00000000000..31756c1b722
--- /dev/null
+++ b/jbmc/regression/jbmc-generics/constant_propagation/test.desc
@@ -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.