From 2e4e0b5f42303f11653b4a414197ec3d7206bf85 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 18 May 2017 20:23:35 +0200
Subject: [PATCH 01/11] Introduce temporary stack variables for ?load / ?aload

---
 .../java_bytecode_convert_method.cpp          | 21 ++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 43a2ded0af1..3c8a2f739b8 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1363,15 +1363,26 @@ codet java_bytecode_convert_methodt::convert_instructions(
       typet element_type=data_ptr.type().subtype();
       dereference_exprt element(data_plus_offset, element_type);
 
-      c=get_array_bounds_check(deref, op[1], i_it->source_location);
+      const exprt tmp_var=tmp_variable("stack_array_elem", element_type);
+      c=code_blockt();
+      c.copy_to_operands(
+        get_array_bounds_check(deref, op[1], i_it->source_location));
+      c.copy_to_operands(
+        code_assignt(tmp_var, java_bytecode_promotion(element)));
       c.add_source_location()=i_it->source_location;
-      results[0]=java_bytecode_promotion(element);
+      results[0]=tmp_var;
     }
     else if(statement==patternt("?load"))
     {
-      // load a value from a local variable
-      results[0]=
-        variable(arg0, statement[0], i_it->address, CAST_AS_NEEDED);
+      const char char_type=statement[0];
+      const typet t=java_bytecode_promotion(java_type_from_char(char_type));
+
+      // create new stack variable to hold the value of the local variable
+      const exprt tmp_var=tmp_variable("stack_var", t);
+      c=code_assignt(
+        tmp_var,
+        variable(arg0, statement[0], i_it->address, CAST_AS_NEEDED));
+      results[0]=tmp_var;
     }
     else if(statement=="ldc" || statement=="ldc_w" ||
             statement=="ldc2" || statement=="ldc2_w")

From d9e3bbcbe1945f3ee484e8855ffb38c67112950c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 18 May 2017 20:28:26 +0200
Subject: [PATCH 02/11] Introduce temporary stack variables for `dup`,
 `dup_x1`, `dup_x2`

---
 .../java_bytecode_convert_method.cpp          | 21 ++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 3c8a2f739b8..a82575d92c0 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1742,19 +1742,34 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="dup")
     {
       assert(op.size()==1 && results.size()==2);
-      results[0]=results[1]=op[0];
+      // create new stack variable
+      const exprt tmp_var=
+        tmp_variable("stack_dup", op[0].type());
+      c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
+      results[0]=tmp_var;
+      results[1]=op[0];
     }
     else if(statement=="dup_x1")
     {
       assert(op.size()==2 && results.size()==3);
-      results[0]=op[1];
+      // create new stack variable
+      const exprt tmp_var=
+        tmp_variable("stack_dup_x1", op[1].type());
+      c=code_assignt(tmp_var, java_bytecode_promotion(op[1]));
+      // op1 is value1, op0 is value2
+      results[0]=tmp_var;
       results[1]=op[0];
       results[2]=op[1];
     }
     else if(statement=="dup_x2")
     {
       assert(op.size()==3 && results.size()==4);
-      results[0]=op[2];
+      // create new stack variable
+      const exprt tmp_var=
+        tmp_variable("stack_dup_x2", op[2].type());
+      c=code_assignt(tmp_var, java_bytecode_promotion(op[2]));
+      // op2 is value1, op1 is value2, op0 is value3
+      results[0]=tmp_var;
       results[1]=op[0];
       results[2]=op[1];
       results[3]=op[2];

From 319ff01014616d376cb6ebc68149edce7faa27fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 18 May 2017 20:36:36 +0200
Subject: [PATCH 03/11] Introduce temporary stack variable for `getfield`

---
 src/java_bytecode/java_bytecode_convert_method.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index a82575d92c0..ba1ee862f00 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1832,7 +1832,11 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="getfield")
     {
       assert(op.size()==1 && results.size()==1);
-      results[0]=java_bytecode_promotion(to_member(op[0], arg0));
+      // create a new stack variable to hold the value of the field
+      const exprt tmp_var=
+        tmp_variable("stack_field", java_bytecode_promotion(arg0.type()));
+      c=code_assignt(tmp_var, java_bytecode_promotion(to_member(op[0], arg0)));
+      results[0]=tmp_var;
     }
     else if(statement=="getstatic")
     {

From 75b770b8350ecd36496ac1d6f848e2bc07b6930f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 18 May 2017 20:37:32 +0200
Subject: [PATCH 04/11] Introduce temporary stack variable for `getstatic`

---
 src/java_bytecode/java_bytecode_convert_method.cpp | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index ba1ee862f00..b6dddc4d07e 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1849,11 +1849,21 @@ codet java_bytecode_convert_methodt::convert_instructions(
         lazy_methods->add_needed_class(
           to_symbol_type(arg0.type()).get_identifier());
       }
-      results[0]=java_bytecode_promotion(symbol_expr);
-
       // set $assertionDisabled to false
       if(field_name.find("$assertionsDisabled")!=std::string::npos)
+      {
         c=code_assignt(symbol_expr, false_exprt());
+        results[0]=java_bytecode_promotion(symbol_expr);
+      }
+      else
+      {
+        // create a new stack variable to hold the value of the field
+        const exprt tmp_var=tmp_variable(
+          "stack_static_field",
+          java_bytecode_promotion(arg0.type()));
+        c=code_assignt(tmp_var, symbol_expr);
+        results[0]=java_bytecode_promotion(tmp_var);
+      }
     }
     else if(statement=="putfield")
     {

From 35698063c301f5f941b4ea3eafa2730dc966c5b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 18 May 2017 20:37:52 +0200
Subject: [PATCH 05/11] Introduce temporary stack variables for `dup_2`,
 `dup2_x1`, `dup2_x2`

---
 .../java_bytecode_convert_method.cpp          | 71 ++++++++++++++++++-
 1 file changed, 68 insertions(+), 3 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index b6dddc4d07e..e5e402b2016 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1781,23 +1781,64 @@ codet java_bytecode_convert_methodt::convert_instructions(
       assert(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
-        op=pop(2);
+      {
+        op=pop(2); // op0 is value1 op1 is value2
+        const exprt tmp_var1=
+          tmp_variable("stack_dup2_1", op[0].type());
+        const exprt tmp_var2=
+          tmp_variable("stack_dup2_2", op[1].type());
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[0])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[1])));
+        results.push_back(tmp_var1);
+        results.push_back(tmp_var2);
+      }
       else
+      {
         op=pop(1);
+        const exprt tmp_var=
+          tmp_variable("stack_dup2", op[0].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
+        results.push_back(tmp_var);
+      }
 
       results.insert(results.end(), op.begin(), op.end());
-      results.insert(results.end(), op.begin(), op.end());
     }
     else if(statement=="dup2_x1")
     {
       assert(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
+      {
         op=pop(3);
+        const exprt tmp_var1=
+          tmp_variable("stack_dup2_x1_1", op[2].type());
+        const exprt tmp_var2=
+          tmp_variable("stack_dup2_x1_2", op[1].type());
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[2])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[1])));
+        results.push_back(tmp_var2);
+        results.push_back(tmp_var1);
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[2])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[1])));
+      }
       else
+      {
         op=pop(2);
+        const exprt tmp_var=
+          tmp_variable("stack_dup2_x1", op[1].type());
+        results.push_back(tmp_var);
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[1]));
+      }
 
-      results.insert(results.end(), op.begin()+1, op.end());
       results.insert(results.end(), op.begin(), op.end());
     }
     else if(statement=="dup2_x2")
@@ -1805,9 +1846,33 @@ codet java_bytecode_convert_methodt::convert_instructions(
       assert(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
+      {
         op=pop(2);
+        const exprt tmp_var1=
+          tmp_variable("stack_dup2_x2_1", op[1].type());
+        const exprt tmp_var2=
+          tmp_variable("stack_dup2_x2_2", op[0].type());
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[1])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[0])));
+        results.push_back(tmp_var2);
+        results.push_back(tmp_var1);
+        c=code_blockt();
+        c.copy_to_operands(
+          code_assignt(tmp_var1, java_bytecode_promotion(op[1])));
+        c.copy_to_operands(
+          code_assignt(tmp_var2, java_bytecode_promotion(op[0])));
+      }
       else
+      {
         op=pop(1);
+        const exprt tmp_var=
+          tmp_variable("stack_dup2_x2", op[0].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
+        results.push_back(tmp_var);
+      }
 
       assert(!stack.empty());
       exprt::operandst op2;

From 74ac6e13edc55d8a3d001d7e064f663786e702df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 17 May 2017 13:13:53 +0200
Subject: [PATCH 06/11] Adapt existing regression tests

---
 regression/cbmc-java/LocalVarTable5/test.desc | 2 +-
 regression/cbmc-java/destructor1/test.desc    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/cbmc-java/LocalVarTable5/test.desc b/regression/cbmc-java/LocalVarTable5/test.desc
index bfe77ab09ad..19f3ddab499 100644
--- a/regression/cbmc-java/LocalVarTable5/test.desc
+++ b/regression/cbmc-java/LocalVarTable5/test.desc
@@ -4,7 +4,7 @@ test.class
 dead anonlocal::1i
 dead anonlocal::2i
 dead anonlocal::3a
-dead new_tmp0
+dead new_tmp[0123456789]+
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/cbmc-java/destructor1/test.desc b/regression/cbmc-java/destructor1/test.desc
index 53856821b22..32dea0b83f5 100644
--- a/regression/cbmc-java/destructor1/test.desc
+++ b/regression/cbmc-java/destructor1/test.desc
@@ -5,4 +5,4 @@ Break.class
 ^SIGNAL=0$
 dead i;
 --
-GOTO 10
+GOTO 11

From 3f5dac89e1af5181c8f11027b5c322bf1bd29406 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 17 May 2017 18:44:12 +0200
Subject: [PATCH 07/11] Add regression tests for `iload`, `dup`, `dup_x1`,
 `dup_x2`

---
 .../cbmc-java/stack_var1/stack_test.class     | Bin 0 -> 603 bytes
 .../cbmc-java/stack_var1/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var1/stack_var1.class     | Bin 0 -> 205 bytes
 regression/cbmc-java/stack_var1/stack_var1.j  |  22 +++++++++++
 regression/cbmc-java/stack_var1/test.desc     |   9 +++++
 .../cbmc-java/stack_var2/stack_test.class     | Bin 0 -> 603 bytes
 .../cbmc-java/stack_var2/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var2/stack_var2.class     | Bin 0 -> 206 bytes
 regression/cbmc-java/stack_var2/stack_var2.j  |  25 ++++++++++++
 regression/cbmc-java/stack_var2/test.desc     |   9 +++++
 .../cbmc-java/stack_var3/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var3/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var3/stack_var3.class     | Bin 0 -> 210 bytes
 regression/cbmc-java/stack_var3/stack_var3.j  |  33 ++++++++++++++++
 regression/cbmc-java/stack_var3/test.desc     |   9 +++++
 .../cbmc-java/stack_var4/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var4/stack_test.java      |   7 ++++
 .../cbmc-java/stack_var4/stack_var4.class     | Bin 0 -> 214 bytes
 regression/cbmc-java/stack_var4/stack_var4.j  |  37 ++++++++++++++++++
 regression/cbmc-java/stack_var4/test.desc     |  10 +++++
 20 files changed, 182 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var1/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var1/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var1/stack_var1.class
 create mode 100644 regression/cbmc-java/stack_var1/stack_var1.j
 create mode 100644 regression/cbmc-java/stack_var1/test.desc
 create mode 100644 regression/cbmc-java/stack_var2/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var2/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var2/stack_var2.class
 create mode 100644 regression/cbmc-java/stack_var2/stack_var2.j
 create mode 100644 regression/cbmc-java/stack_var2/test.desc
 create mode 100644 regression/cbmc-java/stack_var3/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var3/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var3/stack_var3.class
 create mode 100644 regression/cbmc-java/stack_var3/stack_var3.j
 create mode 100644 regression/cbmc-java/stack_var3/test.desc
 create mode 100644 regression/cbmc-java/stack_var4/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var4/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var4/stack_var4.class
 create mode 100644 regression/cbmc-java/stack_var4/stack_var4.j
 create mode 100644 regression/cbmc-java/stack_var4/test.desc

diff --git a/regression/cbmc-java/stack_var1/stack_test.class b/regression/cbmc-java/stack_var1/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..2b723f49df870f126175f4745f10edd16c3ee9ff
GIT binary patch
literal 603
zcmYLG+e#xr5IvQd$t2@wV!XwBye&~d5qw)+6fYn|eMk`02k9iOw8qKOGx1;a2Yl8A
z1%=&r|7peQQInUdnyS<1oT_<yfB6ew6+b+9$h#Q!kU-vqku*{mbus24X(r<yCNSxu
zK<JwlVJLN^nnAd&LQ!qVI)P3I$u$+I=oi5%&L0u%t!7;kG9?wrgVuFb>WTsL;997F
zFjzb-U5XpA+z`RVayil}xcF%vc9$bjyV@7OV?5g;q}FPUFLJNkZ0VZZRfZ}P8t7Rh
z!)VEH`RGOu!TW6A2)*KC3e!Hi;1lv4xy|n#cC>El_6tMgV#dcT<_Osi{;+x}YZ32x
z&i;#g^Lwn_nQk@sCcIHyhDytNo17PkT0G!`oUo4+pBbQR-q_*F0xydmjv4+M=S-ZP
zg=f%%0V2yW88-=O^diT#fmZkzS)8X{kvM*aRa&&4V6Q*IxkF~`7G1AMa^L-DXc93^
z4mQ^od$3v2L4k?;xRVC`N5Mru9~lE}Gpn&G(3?v=A$<qezK3o7fzx69HfC5HB>W9y
Je=rst`T*Q;Z!iD=

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var1/stack_test.java b/regression/cbmc-java/stack_var1/stack_test.java
new file mode 100644
index 00000000000..cb404e89473
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var1 s = new stack_var1();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var1/stack_var1.class b/regression/cbmc-java/stack_var1/stack_var1.class
new file mode 100644
index 0000000000000000000000000000000000000000..67a2f73308153e8e628076a4f5bbcf0aa989b302
GIT binary patch
literal 205
zcmX^0Z`VEs1_nI_J}w3x1~x_pfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK!{z
zHk-`6%o00x1}+{376xuc1{UZ16reayaY<rwc6?c4k)d7|BLia^P#;2wk%3u5GmM>q
z38-GfQ`3_{k%1Lx9|$lp0L2)%fh0SSCkUh&fi$bub_T|cAbB8{lYtj1Eeur71QcVJ
SZee7UPFVw0zzn3B7&rhN*dQPP

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var1/stack_var1.j b/regression/cbmc-java/stack_var1/stack_var1.j
new file mode 100644
index 00000000000..a3736df18e2
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/stack_var1.j
@@ -0,0 +1,22 @@
+.class public stack_var1
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 2
+   .limit locals 2
+
+   ;; copy of arg on stack
+   iload_1
+   ;; increment arg
+   iinc 1 1
+   ;; incremented copy on stack
+   iload_1
+   isub
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var1/test.desc b/regression/cbmc-java/stack_var1/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/test.desc
@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var2/stack_test.class b/regression/cbmc-java/stack_var2/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..f26c64d43d442b1b3eb400c73afb3ddf95ec262d
GIT binary patch
literal 603
zcmYLG+e#xr5IvQd$t2@wV!XwBye&~dL3~?X6fYn|eMk`02k9iOw8qKOGx1;a2Yl8A
z1%=&r|7peQQInUdnyS<1oT_<yfB6ew6+b+9$h#Q!kU-vqku*{mbus24X(r<yCNSxu
zK<JwlVJLN^nnAd&LQ!qVI)P3I$u$+I=oi5%&L0u%t!7;kG9?wrgVuFb>WTsL;997F
zFjzb-U5XpA+z`RVayil}xcF%vc9$bjyV@7OV?5g;q}FPUFLJNkZ0VZZRfZ}P8t7Rh
z!)VEH`RGOu!TW6A2)*KC3e!Hi;1lv4xy|n#cC>El_6tMgV#dcT<_Osi{;+x}YZ32x
z&i;#g^Lwn_nQk@sCcIHyhDytNo17PkT0G!`oUo4+pBbQR-q_*F0xydmjv4+M=S-ZP
zg=f%%0V2yW88-=O^diT#fmZkzS)8X{kvM*aRa&&4V6Q*IxkF~`7G1AMa^L-DXc93^
z4mQ^od$3v2L4k?;xRVC`N5Mru9~lE}Gpn&G(3?v=A$<qezK3o7fzx69HfC5HB>W9y
Je=rst`T*VMZ!rJ>

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var2/stack_test.java b/regression/cbmc-java/stack_var2/stack_test.java
new file mode 100644
index 00000000000..822716f691c
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var2 s = new stack_var2();
+    int n = s.f(1);
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var2/stack_var2.class b/regression/cbmc-java/stack_var2/stack_var2.class
new file mode 100644
index 0000000000000000000000000000000000000000..6db13604864ab7dab67c972aee693ea014745c9c
GIT binary patch
literal 206
zcmX^0Z`VEs1_nI_J}w3x1~x_pfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK!{z
zHk-`6%o00x22LIZ76vXx1{UZ16rea`8c<<zNn&z#d|6_V5hDY$hGrNe0}nz-FN>Xl
z38-GfQ`3_{k%1Lx9|$lp0L2)%fFwJRCkUh&fi$bub_T|cAbB8{gMk++EyBPI)WE>N
VAsyMm$S9q%2C9M?NHZ~T0{|qPAbkJ;

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var2/stack_var2.j b/regression/cbmc-java/stack_var2/stack_var2.j
new file mode 100644
index 00000000000..e20a174070c
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/stack_var2.j
@@ -0,0 +1,25 @@
+.class public stack_var2
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(I)I
+   .limit stack 3
+   .limit locals 2
+
+   ;; push local var1
+   iload_1
+   ;; duplicate
+   dup
+   ;; increment local var1
+   iinc 1 1
+   ;; push local var1
+   iload_1
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var2/test.desc b/regression/cbmc-java/stack_var2/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/test.desc
@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var3/stack_test.class b/regression/cbmc-java/stack_var3/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..a42cc9101a1af73622c324983b4fb238d3d1d679
GIT binary patch
literal 601
zcmYLGT~8B16g{`Q+wE=_T3UrFg`#`}Fp&rQCK^qJgrvYjiHZ1NrtQ#7S+-<$%YTtS
z;Io>vi6r>$f6{nowe8EjGxwf3_nbSw{`|NHP{)=J9~Bpmd}L5D;jxDtmR(eRWKCzq
z$0}+r)(GVd5yw&|Y7oWmR4m$|>=Njlklk02N?sGJ?Va}oyD{iWLZPW5c{03eOMPa*
z+_(}dA}nryZ1%;C*b7C}+iN9SMZK5i;an>boy%i!o#I&*A-CTN|C9Tz!BBVPp)yp3
z*g!ueGESZwt^jkGC;0!$H$uM%@B~i-<Pi`mvvF@H9uBk~=;;eX<YGO*1~v)B8UD20
zmz{)tUZnPpc=W8<2ze!Js4HWoWp~QWK9V6fcpv91Bgb0?s8}&-_+){-VxD7xZ!4UM
zv$Hz}eKkN7IcC!$!NUSdd^XS)|B%Ib?GBj_V_3~+BiOIL!MR1D`Wg8<WV!7AG%T5v
zr39PL7E7>sq=Opsmbv1Aew%-Nz$?bXsg`;=6j&(bM(}Ro+FxK>-{H&{C%O!agG}(o
Ks9#J6F8u}Axo+P8

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var3/stack_test.java b/regression/cbmc-java/stack_var3/stack_test.java
new file mode 100644
index 00000000000..7ffc016070c
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var3 s = new stack_var3();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var3/stack_var3.class b/regression/cbmc-java/stack_var3/stack_var3.class
new file mode 100644
index 0000000000000000000000000000000000000000..9a3a0d6d370504ddb033f4faf67779296d1bff03
GIT binary patch
literal 210
zcmX^0Z`VEs1_nI_J}w3x26jdUfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK$uO
zE=C46o6Nk-5<5l)W(`eG9tKthZbk+c=lqmZMh3<-pz`99#N_Pwvcw`|u#zx#1|~)Z
z9)ze~7K0)K3(z_cU}9hdnE)g?fILAU%?PAfwYD=bZUo5#xtt7aP-#h^Qf8nSFN+Pc
Vt&DV33*-Orlr>OgAPFW0UI2KPA{+n!

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var3/stack_var3.j b/regression/cbmc-java/stack_var3/stack_var3.j
new file mode 100644
index 00000000000..f215d15b4bc
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/stack_var3.j
@@ -0,0 +1,33 @@
+.class public stack_var3
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 5
+   .limit locals 3
+
+   ;; 1->var1
+   ;; 0->var2
+   iconst_1
+   istore_1
+   iconst_0
+   istore_2
+   ;; push local var2 / var1
+   iload_2
+   iload_1
+   ;; dup var1
+   dup_x1
+   ;; sub one from var1
+   iinc 1 -1
+   ;; pop first var1
+   pop
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var3/test.desc b/regression/cbmc-java/stack_var3/test.desc
new file mode 100644
index 00000000000..3bf59401a5a
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/test.desc
@@ -0,0 +1,9 @@
+CORE
+stack_test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var4/stack_test.class b/regression/cbmc-java/stack_var4/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..cfbb80f78e82daf472877b6c3716d8ca38a8d564
GIT binary patch
literal 601
zcmYLG%T60X5Ulp@dhKPwuRt7LHctVO;Nlx3A|fCm88{drVGd|)4`_^8quDk80zbeR
zkgyb_<eq;DO3x<Pm+qPFn(C^a-)}#D0;piwgNLGvPaYB|nlPD03R5noJtR$M#=|U1
zF3N<$q6kB&Bh?MU?<y3Hj%*RAPDpO4Kt*2(*2?M$!QSb%Bq38(fjsP8H>5r`U~XIs
z6%Zy?&Z=#3D>gbJxZJ2kS_PMz=HX~963wdvaTDWN79q9O?EEM9YTcf0$~|SMGNFN<
zM>34o4VRBmj1jzl<y)aEKISm*V+1~-I2`xw-NUZdT|IbVh+HiASi}+`JH#I~+Oiq3
z&x_dJK93$YcRIWhHq?@#(y}$+W*<?H8@!J?%SiE-0m>GQ8a`QIuNdQ);oA&n;_R&T
zL5~KAEXQPAB&3l;p3eqa;~%m(mtT=M?Zc{meu4ev3C=w-({~toMUu<zFT;|ES@N*?
zY_SBJM>;4mZ-Fam&>!=!A9%$WA84t>LxEgA^@8+0T>AmG^$cgo_^!*aI7s;0M*T!Q
G@Z(?FE^goe

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var4/stack_test.java b/regression/cbmc-java/stack_var4/stack_test.java
new file mode 100644
index 00000000000..1088dd5ac2e
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var4 s = new stack_var4();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var4/stack_var4.class b/regression/cbmc-java/stack_var4/stack_var4.class
new file mode 100644
index 0000000000000000000000000000000000000000..782443dd6e37e3d94704b56bd085a5d86cb32c0b
GIT binary patch
literal 214
zcmX^0Z`VEs1_nI_J}w4c1`b9Bfvm)`ME#t^ymWp4q^#8B5=I8D;QZ2}<W#rJoK$uO
zZbk;4;*!MV?D(?8A``tVMg}&U%)HDJJ4Oa(4NXrT1~vvBMg|t={FGEi2F5g?ZiH&E
zk}!4#CI&?Y7NB(?z{CJFfq@4|asqjRK$;OqvubT;VB83j2XeU>*rC$046HznKxND}
bEVit6vNF=qEsTue;o)nbN|}K)69X#%T$3T#

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var4/stack_var4.j b/regression/cbmc-java/stack_var4/stack_var4.j
new file mode 100644
index 00000000000..99eecf3794a
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/stack_var4.j
@@ -0,0 +1,37 @@
+.class public stack_var4
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 5
+   .limit locals 4
+
+   ;; 0->var1
+   ;; 1->var2
+   ;; 2->var3
+   iconst_0
+   istore_1
+   iconst_1
+   istore_2
+   iconst_2
+   istore_3
+
+   ;; push local var3 / var2 / var1
+   iload_3
+   iload_2
+   iload_1
+   ;; push var1 in front of var3
+   dup_x2
+   ;; add one to local var 1
+   iinc 1 1
+   pop
+   pop
+   pop
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var4/test.desc b/regression/cbmc-java/stack_var4/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From 0aec9b1405c445e59c3de6a07ed61394f7c1c098 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Thu, 18 May 2017 12:47:59 +0200
Subject: [PATCH 08/11] Add regression tests for `dup2`, `dup2_x1` and
 `dup2_x2`

---
 .../cbmc-java/stack_var5/stack_test.class     | Bin 0 -> 602 bytes
 .../cbmc-java/stack_var5/stack_test.java      |   7 +++
 .../cbmc-java/stack_var5/stack_var5.class     | Bin 0 -> 209 bytes
 regression/cbmc-java/stack_var5/stack_var5.j  |  33 ++++++++++++++
 regression/cbmc-java/stack_var5/test.desc     |  10 ++++
 .../cbmc-java/stack_var6/stack_test.class     | Bin 0 -> 609 bytes
 .../cbmc-java/stack_var6/stack_test.java      |   7 +++
 .../cbmc-java/stack_var6/stack_var6.class     | Bin 0 -> 209 bytes
 regression/cbmc-java/stack_var6/stack_var6.j  |  25 ++++++++++
 regression/cbmc-java/stack_var6/test.desc     |  10 ++++
 .../cbmc-java/stack_var7/stack_test.class     | Bin 0 -> 602 bytes
 .../cbmc-java/stack_var7/stack_test.java      |   7 +++
 .../cbmc-java/stack_var7/stack_var7.class     | Bin 0 -> 223 bytes
 regression/cbmc-java/stack_var7/stack_var7.j  |  43 ++++++++++++++++++
 regression/cbmc-java/stack_var7/test.desc     |  10 ++++
 15 files changed, 152 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var5/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var5/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var5/stack_var5.class
 create mode 100644 regression/cbmc-java/stack_var5/stack_var5.j
 create mode 100644 regression/cbmc-java/stack_var5/test.desc
 create mode 100644 regression/cbmc-java/stack_var6/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var6/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var6/stack_var6.class
 create mode 100644 regression/cbmc-java/stack_var6/stack_var6.j
 create mode 100644 regression/cbmc-java/stack_var6/test.desc
 create mode 100644 regression/cbmc-java/stack_var7/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var7/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var7/stack_var7.class
 create mode 100644 regression/cbmc-java/stack_var7/stack_var7.j
 create mode 100644 regression/cbmc-java/stack_var7/test.desc

diff --git a/regression/cbmc-java/stack_var5/stack_test.class b/regression/cbmc-java/stack_var5/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..57cf43dac86c9be13b8ff00a1eb657c9b1e8c1b5
GIT binary patch
literal 602
zcmYLG$xh=y5PcQfabgS!Vau=#VHJx67dWwq5sQSBnK=X@0SDAc8q^_iP}|{SxNzhQ
zNFad(cm4@PwP#2!RpqMJuih)ae?GqgSi!6Z4|x|qJS31eVK|KxMqG?~NSeu*ho2aC
zQ6Th9i!hWrQq3UTQK2Z;WtBk3gygykRJ2L3=H?Fx_I9%>37Mh_<eyffEcJl_^PnMA
zKp31mDb~c5SgwoUe7O{96`Ze`hux(}R4#st%NWnH2&wf-{Xe-^YPNJm?kPi+2@Ui#
zl3}!DxO{Y@hv5BdUkSbHV*-;ty5JM?opryyJ?v`T)a@6B$i<Y8Y0MC^9sJ*NO;#fI
zc^2E-=hdCzcAZbchN?1DT2|ZK>?3ONfbVh4GE#hHfU<d`hARu~6+Ij?{58gzI6DhZ
zpgRLZmSZw*64K~Jj%x!w;6G$>o_Imx=m}PF@e%gMJ)CP~N9`MQy&%bb_s!5GVwxOm
zt}WJJ^G*i^Chp@-8uWpJi+;W_2HIj);;le$F7=4?HC+1^w)Fs~!}u-CusBHgTSoq1
Hym06XN3L%0

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var5/stack_test.java b/regression/cbmc-java/stack_var5/stack_test.java
new file mode 100644
index 00000000000..bfcbe79325d
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var5 s = new stack_var5();
+    int n = s.f();
+    assert(n==1);
+  }
+}
diff --git a/regression/cbmc-java/stack_var5/stack_var5.class b/regression/cbmc-java/stack_var5/stack_var5.class
new file mode 100644
index 0000000000000000000000000000000000000000..6230e78a9c70f9c25c79952cb347c499f2c7476e
GIT binary patch
literal 209
zcmX^0Z`VEs1_nI_J}w4c26jdUfvm)`ME#t^ymWp4q^#8B5_SeIMh33n{L-T2RJY8W
zR7M6io6Nk-5<5l)W(`eG9tKth9!3V9;*!MV?D(?8B2&FAMg|t={1l){E`%r}17jLk
zM;JQ;6N4fHGtfE^U}9hdnE)g?fjmJV%?PAfwYD=bZUo5#x!eqFP-zJU79eC`;9;?0
VwUv>MX<=kcSp!uC5@%xI004QJAkY8+

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var5/stack_var5.j b/regression/cbmc-java/stack_var5/stack_var5.j
new file mode 100644
index 00000000000..0871fb68e0b
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/stack_var5.j
@@ -0,0 +1,33 @@
+.class public stack_var5
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 4
+   .limit locals 4
+
+   ;; 1->var1
+   ;; 2->var2
+   iconst_1
+   istore_1
+   iconst_2
+   istore_2
+
+   ;; push local var2 / var1
+   iload_2
+   iload_1
+
+   ;; duplicate var2 / var1
+   dup2
+   ;; add one to local var 1
+   iinc 1 1
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var5/test.desc b/regression/cbmc-java/stack_var5/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var6/stack_test.class b/regression/cbmc-java/stack_var6/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..c5e765b667b216837c87a0f91d562994b70d598a
GIT binary patch
literal 609
zcmYLF%T60X5UjTM<z>NZI}j(~jX{P;a6!31A|gm6OHMdAig+B**dEY;y+*TZK88z<
zIYT6nKuYfUCs2AeU|+gtx~r?J`tRf2Zvg99^5LWG;+2mK$|k(d!NVIDlRg~Nnes7>
z85gsJQbokE)QRdv@s5f`vm@ICIv_ZkDpJV@Lbkg6onUSE+LDm3t4MzBcbigwGhl9X
zg^CCh)x-L!xDaa{5uL0x60M?>4Kp~}NJQ)Gi#Sj5EQ{c6wmMJbexujdE%{j)s(fsq
zM~RG+Rl^lv6k`PcfB8b_cLC-wA7BIlp*&po@!7*Ct$TVfVTfET1gKz<5DxLX%~RP*
z*yl0(tk!C^<r;4v_P0BH753DYvC^_Vpl2&dpBsFV16Jbkp#ciZMi9TUV7nOOnCIUV
zXX0$H+=8wQ5Ftk=EfR7lpvZ3n-Gjx$z~VhJ`?tu}-&(eN1MB@Y>`N3T!^a;Oxrf6&
z_m82<q*O&7Gh02*A#Aqkpv09N=m8ZMFZk3L9|&4cHv@&DcZ1v|T<a&S>@V0u#%FPc
P#YQIBG8QJ%g)jdBRe5m#

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var6/stack_test.java b/regression/cbmc-java/stack_var6/stack_test.java
new file mode 100644
index 00000000000..392d200d370
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var6 s = new stack_var6();
+    int n = s.f(1,2,4);
+    assert(n==-2);
+  }
+}
diff --git a/regression/cbmc-java/stack_var6/stack_var6.class b/regression/cbmc-java/stack_var6/stack_var6.class
new file mode 100644
index 0000000000000000000000000000000000000000..05223a9a3491806a31721a208b1f93e2b01c7847
GIT binary patch
literal 209
zcmX^0Z`VEs1_nI_J}w4c26jdUfvm)`ME#t^ymWp4q^#8B5_Sd-Mh33n{L-T2RJY8W
zR7M6i4Np%`O-~@hCNnRy#Eyr7je!TKrnn?AIXk{AvB->(fyFsL1*nuUjgf%|A+DFj
z$iS?j8OF}Q#GuH)473phm>7UYG4KFMP9RSZNHYRyR;}#}j2l7nKrR;pD^yyPfdj~9
XVBnONk&SI(VoX^BRl)+KnHabMum2%U

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var6/stack_var6.j b/regression/cbmc-java/stack_var6/stack_var6.j
new file mode 100644
index 00000000000..19108f70e36
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/stack_var6.j
@@ -0,0 +1,25 @@
+.class public stack_var6
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f(III)I
+   .limit stack 8
+   .limit locals 5
+
+   ;; push local var3 / var2 / var1
+   iload_1
+   iload_2
+   iload_3
+   dup2_x1
+   ;; add one to local var 2
+   iinc 2 1
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var6/test.desc b/regression/cbmc-java/stack_var6/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/stack_var7/stack_test.class b/regression/cbmc-java/stack_var7/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..21eabe9a02937bf489e793fa085732d5b0d3458a
GIT binary patch
literal 602
zcmYLG$xh=y5PcQfabgS!Vau=#VHJx67bFfWV#FdLWo8aRNWcMgk_L519MpFB7%m(+
z0}@Ce!JU5sQSBL$OI5k*^{e;F@1M`F09G*T!9(7~4-X0CO&Crig%KB{9+GA<=HVyC
zT@(m?(;^I|j#M)UcT_0Kby+3QF(J9G0u^l%thxC^g1z0WN<yZn0{N%aC`)}{z&vOO
z6%YpJPKq^gC6?<VIA1PBS_S88=3#d!5|xYJ;xfjwEJA9%QvXlxm6|PGk$cKeWkLfz
zjbs=t87?2)=plIj+E+ra`k26^k1qIxd}rOSZx6d#H+B1kA#yS0V;VDrYzP0hT$7cE
zeV)bk_IY(@xLxOyu%W69m6p{uH~WZMJm7mAvy2p98K7+5sNu>2dqoe&41bMrCeF^n
z6X?zWk>!|-n}jrak>lDx5BLvRoF`t8IC_FrTzrJRaS!Jj*-`rjT`x#--+ePQiI^q_
zn`?_T*u2w0fr<OLlLmdD;G&;zjDfb8m3S-An@c?+eGS*Xg>5~+=`el^Gb|1g{+5wH
I7%v?90!o^0@&Et;

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var7/stack_test.java b/regression/cbmc-java/stack_var7/stack_test.java
new file mode 100644
index 00000000000..b742878507e
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var7 s = new stack_var7();
+    int n = s.f();
+    assert(n==1);
+  }
+}
diff --git a/regression/cbmc-java/stack_var7/stack_var7.class b/regression/cbmc-java/stack_var7/stack_var7.class
new file mode 100644
index 0000000000000000000000000000000000000000..dcc6f0fc1b69c6dd2f0dcbdff3743f465247f4ce
GIT binary patch
literal 223
zcmX^0Z`VEs1_nI_J}w4c26lD^4n_unti-ZJ{hY+SbbbG%tkmQZMh33n{L-T2RJY8W
zR7M6io6Nk-5<5l)W(`eG9tKthZlHqVlEmcf__D+zb4CUh=lm3)I>t1xk}yUF9)zr3
z7CQqogCYYH&^i!cVqgTB03<nqJV7AM2&7rHwlgqp1jz%rTnubbX*C88pkf9FDHa=6
hTXs7E4l@=}7Fiil#<&(n#&94=Sp(I>0;HK3cmOiDBN_kz

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var7/stack_var7.j b/regression/cbmc-java/stack_var7/stack_var7.j
new file mode 100644
index 00000000000..e75f96b833d
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/stack_var7.j
@@ -0,0 +1,43 @@
+.class public stack_var7
+.super java/lang/Object
+
+.method public <init>()V
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   ;; 1->var1
+   ;; 2->var2
+   ;; 4->var3
+   ;; 8->var4
+   iconst_1
+   istore_1
+   iconst_2
+   istore_2
+   iconst_4
+   istore_3
+   bipush 8
+   istore 4
+   ;; push local var4 / var3 / var2 / var1
+   iload 4
+   iload_3
+   iload_2
+   iload 1
+   ;; push var2 / var1 in on head
+   dup2_x2
+   ;; add one to local var 1
+   iinc 1 1
+   pop
+   pop
+   pop
+   pop
+   ;; sub
+   isub
+   ;; incremented copy on stack
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var7/test.desc b/regression/cbmc-java/stack_var7/test.desc
new file mode 100644
index 00000000000..805e44acccd
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/test.desc
@@ -0,0 +1,10 @@
+CORE
+stack_test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^.*assertion at file stack_test.java line 5 function.*: SUCCESS
+$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From 8cacd7de064eadeb5b9cd65b8122812125dcc501 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 19 May 2017 08:25:04 +0200
Subject: [PATCH 09/11] Add regression test for `getfield`, `getstatic`

---
 .../cbmc-java/stack_var8/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var8/stack_test.java      |   7 +++++
 .../cbmc-java/stack_var8/stack_var8.class     | Bin 0 -> 238 bytes
 regression/cbmc-java/stack_var8/stack_var8.j  |  27 ++++++++++++++++++
 .../cbmc-java/stack_var9/stack_test.class     | Bin 0 -> 601 bytes
 .../cbmc-java/stack_var9/stack_test.java      |   7 +++++
 .../cbmc-java/stack_var9/stack_var9.class     | Bin 0 -> 235 bytes
 regression/cbmc-java/stack_var9/stack_var9.j  |  24 ++++++++++++++++
 8 files changed, 65 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var8/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var8/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var8/stack_var8.class
 create mode 100644 regression/cbmc-java/stack_var8/stack_var8.j
 create mode 100644 regression/cbmc-java/stack_var9/stack_test.class
 create mode 100644 regression/cbmc-java/stack_var9/stack_test.java
 create mode 100644 regression/cbmc-java/stack_var9/stack_var9.class
 create mode 100644 regression/cbmc-java/stack_var9/stack_var9.j

diff --git a/regression/cbmc-java/stack_var8/stack_test.class b/regression/cbmc-java/stack_var8/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..8ea61591cbc2c80a28ea0204557c61307a9141c5
GIT binary patch
literal 601
zcmYLG+e#xr5IvQd$t2@wV!Xv`)O8nk1%2^B@Pgt6gs2Y@L4A-;(i=J(Cri)7f6*WC
zSp@|JefOUft4B><s=BLApE{@d_5JY~z#@Km@Q`;g>>+`?2_tEwFzRB=L(+7{JxrkB
zVv^7|Bf?PXNHv3SONFA`kW~Vm5Rxk@P|+H}n*Du5us54kNyrpcAopA6WvLGhm>cIp
z1%$!b(_&p*h=qm-Y73=EtDv@Q9(I=^QTewg{>ONhMM$kw8eimIsoByMxuXnKCN$8q
zNQTk8;quXq9)kB-z7TrJ#}uZ0bipU&JL5LKJ#1^;)a@6B$i)vIGx$l!cJK$~x~xR(
z^KWc#mq&M+n+;wG8>-4sX<2P^vyZ674c^BI%SiE-0m|l$8a`QIujt{J;oCT8;_Uo+
z0NofMvK*6fk&s3&a(p(>6916JdGZN~;|Ey9xqH~Fw{WhI8M{Q+6OvqZUkpnkX34?k
zv&9l@9_gUKynS3rgWk-)_VbD{(AKgT4+VO2se7ca;M&))tvfg!#&2DQ#X-VfH|huD
GfkPkQ0&e60

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var8/stack_test.java b/regression/cbmc-java/stack_var8/stack_test.java
new file mode 100644
index 00000000000..3a288890e69
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var8 s = new stack_var8();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var8/stack_var8.class b/regression/cbmc-java/stack_var8/stack_var8.class
new file mode 100644
index 0000000000000000000000000000000000000000..5298a7d8c92c01f7cd2170ae34dac388e7042f0e
GIT binary patch
literal 238
zcmYMuKMR6j5C-t))clv3HMF;tgRTwH5(G{SL2JC3g(eDSeyWzB2pakTeW>V+sO9dS
zm){-l^L2j!@X$5kKqpv-QiS_eC5n-k5S&C*!cRrE^XKa%3QK~y$d5%B&Ehm7P)1P4
zaTb>of;<=o7F4tt{m)ovpiNMw`KDgje%#VP2PVfrgRH?opR>b1AxO37N#dDracy$y
j@hfpR-5bc2udvUYYHvaN8J$&aF0fsN&FO0t?h>Rov)Ur&

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var8/stack_var8.j b/regression/cbmc-java/stack_var8/stack_var8.j
new file mode 100644
index 00000000000..d5bec33279d
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/stack_var8.j
@@ -0,0 +1,27 @@
+.class public stack_var8
+.super java/lang/Object
+
+.field private n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   aload_0
+   iconst_0
+   putfield stack_var8/n I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   aload_0
+   getfield stack_var8/n I
+   aload_0
+   iconst_1
+   putfield stack_var8/n I
+
+   ireturn
+.end method
diff --git a/regression/cbmc-java/stack_var9/stack_test.class b/regression/cbmc-java/stack_var9/stack_test.class
new file mode 100644
index 0000000000000000000000000000000000000000..4f20f14f7d17dcc6fb4c1c15290f992bfca428ae
GIT binary patch
literal 601
zcmYLG+e#xr5IvQd$t2@wV!Xv`)O8nk1%2^Fyr6giA?ia!P#>g|^oGvH$<j0NU-Soj
zRzX2Q-~A`W>QR%Is_v@Or_QN<eSdrgu!vtCJmg&rdq^N}!bln^jJg=}kTjif4-+W3
zm?ZSgh%l5oQq3UTQlTg}WR*ZCgyf0}RJ2C0W`7?M?9FCX5;8><$o<xNS?WUr=Ek{D
z0by|Vv{)AxVxb{|+CnMPDyS`+hux(}RQ~OW|1q9r5mGCa#uvF)YPNJm?kGc*2@Uit
zl3_G&xO{Y@hv0pdFN9w5F@<R#UGNF{&bW<l58GNdb^C=Oa`D5*41N-_9sEJLE-MlH
z{2SZb<<XtyW`kG4hN?1DT2|ZK>?3M%gZFX5GE%%{fU<d`hEEpQD|$F)_%_a&I6HqH
zKsN@6EXQPAB&5-c9G?xe#6M(lo_s>$_yJaN?jH8)Eu1T4#xBwIgd~^U7sHZ>S#q%X
zY_SBJM>;4lZy#6Epf~fc{k&ofw6!e8LxJ90>K^GUxb`({>kdwb@mrT+aggxWjrzfO
G;Lr!*cW&hX

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var9/stack_test.java b/regression/cbmc-java/stack_var9/stack_test.java
new file mode 100644
index 00000000000..994e7974026
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/stack_test.java
@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var9 s = new stack_var9();
+    int n = s.f();
+    assert(n==0);
+  }
+}
diff --git a/regression/cbmc-java/stack_var9/stack_var9.class b/regression/cbmc-java/stack_var9/stack_var9.class
new file mode 100644
index 0000000000000000000000000000000000000000..1fa90019a0e1341eeef164c58df8b9db5ddc278c
GIT binary patch
literal 235
zcmYL@zY2nI6ot=K%RgCa)C06tgU&&;1c6gS&>FwYLK6iupQ@!Af`%TThl;KtwA}L@
z_zv9n=lKHQqHDl`POxK93NI1q!CP+QFenJdDm&*vxQLRFKq;X)jnb%?5#-^>Czz)~
z1jkJ&@`)R>{;wt)Xq!;bAt>`~SMB$|*_z4MVZ%_NsgN*WcK8$CS3Z-(%yYgiZhdCr
h)W;8ye1~=AQt2j|wbFye5}@5+DQsM7L*|sAegQN$B4q#o

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/stack_var9/stack_var9.j b/regression/cbmc-java/stack_var9/stack_var9.j
new file mode 100644
index 00000000000..aeee091def0
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/stack_var9.j
@@ -0,0 +1,24 @@
+.class public stack_var9
+.super java/lang/Object
+
+.field private static n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   iconst_0
+   putstatic stack_var9/n I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   getstatic stack_var9/n I
+   iconst_1
+   putstatic stack_var9/n I
+
+   ireturn
+.end method

From 52f522d375a967cb3996c830e2d62b7d925df038 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Fri, 19 May 2017 13:52:28 +0200
Subject: [PATCH 10/11] Add README to tests pointing to jasmin bytecode
 assembler

---
 regression/cbmc-java/stack_var1/README | 9 +++++++++
 regression/cbmc-java/stack_var2/README | 9 +++++++++
 regression/cbmc-java/stack_var3/README | 9 +++++++++
 regression/cbmc-java/stack_var4/README | 9 +++++++++
 regression/cbmc-java/stack_var5/README | 9 +++++++++
 regression/cbmc-java/stack_var6/README | 9 +++++++++
 regression/cbmc-java/stack_var7/README | 9 +++++++++
 regression/cbmc-java/stack_var8/README | 9 +++++++++
 regression/cbmc-java/stack_var9/README | 9 +++++++++
 9 files changed, 81 insertions(+)
 create mode 100644 regression/cbmc-java/stack_var1/README
 create mode 100644 regression/cbmc-java/stack_var2/README
 create mode 100644 regression/cbmc-java/stack_var3/README
 create mode 100644 regression/cbmc-java/stack_var4/README
 create mode 100644 regression/cbmc-java/stack_var5/README
 create mode 100644 regression/cbmc-java/stack_var6/README
 create mode 100644 regression/cbmc-java/stack_var7/README
 create mode 100644 regression/cbmc-java/stack_var8/README
 create mode 100644 regression/cbmc-java/stack_var9/README

diff --git a/regression/cbmc-java/stack_var1/README b/regression/cbmc-java/stack_var1/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var1/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var2/README b/regression/cbmc-java/stack_var2/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var2/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var3/README b/regression/cbmc-java/stack_var3/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var3/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var4/README b/regression/cbmc-java/stack_var4/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var4/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var5/README b/regression/cbmc-java/stack_var5/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var5/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var6/README b/regression/cbmc-java/stack_var6/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var6/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var7/README b/regression/cbmc-java/stack_var7/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var7/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var8/README b/regression/cbmc-java/stack_var8/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var8/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.
diff --git a/regression/cbmc-java/stack_var9/README b/regression/cbmc-java/stack_var9/README
new file mode 100644
index 00000000000..7a032cccbcd
--- /dev/null
+++ b/regression/cbmc-java/stack_var9/README
@@ -0,0 +1,9 @@
+This regression test is created from the .j file with the jasmin assembler.
+https://github.com/Sable/jasmin
+
+On Ubuntu, it is available as jasmin-sable. To convert a .j file, it is
+sufficient to do
+
+> jasmin $FILE.j
+
+and it will create the corresponding $FILE.class file.

From fc1a852049f2bfb7d75ff14730becda33e06e0c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Mon, 22 May 2017 09:30:24 +0200
Subject: [PATCH 11/11] Do not duplicate constant value as temporary variables

---
 .../java_bytecode_convert_method.cpp          | 49 ++++++++++++-------
 1 file changed, 32 insertions(+), 17 deletions(-)

diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index e5e402b2016..e49ba0264c7 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1742,34 +1742,49 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="dup")
     {
       assert(op.size()==1 && results.size()==2);
-      // create new stack variable
-      const exprt tmp_var=
-        tmp_variable("stack_dup", op[0].type());
-      c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
-      results[0]=tmp_var;
+      if(op[0].id()!=ID_constant)
+      {
+        // create new stack variable
+        const exprt tmp_var=
+          tmp_variable("stack_dup", op[0].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[0]));
+        results[0]=tmp_var;
+      }
+      else
+        results[0]=op[0];
       results[1]=op[0];
     }
     else if(statement=="dup_x1")
     {
       assert(op.size()==2 && results.size()==3);
-      // create new stack variable
-      const exprt tmp_var=
-        tmp_variable("stack_dup_x1", op[1].type());
-      c=code_assignt(tmp_var, java_bytecode_promotion(op[1]));
-      // op1 is value1, op0 is value2
-      results[0]=tmp_var;
+      if(op[1].id()!=ID_constant)
+      {
+        // create new stack variable
+        const exprt tmp_var=
+          tmp_variable("stack_dup_x1", op[1].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[1]));
+        // op1 is value1, op0 is value2
+        results[0]=tmp_var;
+      }
+      else
+        results[0]=op[1];
       results[1]=op[0];
       results[2]=op[1];
     }
     else if(statement=="dup_x2")
     {
       assert(op.size()==3 && results.size()==4);
-      // create new stack variable
-      const exprt tmp_var=
-        tmp_variable("stack_dup_x2", op[2].type());
-      c=code_assignt(tmp_var, java_bytecode_promotion(op[2]));
-      // op2 is value1, op1 is value2, op0 is value3
-      results[0]=tmp_var;
+      if(op[2].id()!=ID_constant)
+      {
+        // create new stack variable
+        const exprt tmp_var=
+          tmp_variable("stack_dup_x2", op[2].type());
+        c=code_assignt(tmp_var, java_bytecode_promotion(op[2]));
+        // op2 is value1, op1 is value2, op0 is value3
+        results[0]=tmp_var;
+      }
+      else
+        results[0]=op[2];
       results[1]=op[0];
       results[2]=op[1];
       results[3]=op[2];