Merge pull request diffblue#951 from mgudemann/fix/bytecode_args_write_from_stack

Fix/bytecode args write from stack

Author: Daniel Kroening

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[0-9]+
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc-java/destructor1/test.desc

@@ -5,4 +5,4 @@ Break.class
 ^SIGNAL=0$
 dead i;
 --
-GOTO 10
+GOTO 11

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.

regression/cbmc-java/stack_var1/stack_test.class

@@ -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);
+  }
+}

regression/cbmc-java/stack_var1/stack_test.java

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

regression/cbmc-java/stack_var1/stack_var1.class

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

regression/cbmc-java/stack_var1/stack_var1.j

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

regression/cbmc-java/stack_var1/test.desc

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var10 s = new stack_var10();
+    int n = s.f();
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var10/README

@@ -0,0 +1,28 @@
+.class public stack_var10
+.super java/lang/Object
+
+.field private static n I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+
+   iconst_1
+   istore_1
+   iconst_0
+   istore_2
+   ;; lvar1 is 1, lvar2 is 0
+   iload_1
+   iload_2
+   ;; on stack 1, 0
+   istore_1
+   ;; store 0 into lvar1
+   ireturn
+.end method

regression/cbmc-java/stack_var10/stack_test.class

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

regression/cbmc-java/stack_var10/stack_test.java

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

regression/cbmc-java/stack_var10/stack_var10.class

@@ -0,0 +1,7 @@
+public class stack_test {
+  public static void main(String[] args) {
+    stack_var11 s = new stack_var11();
+    int n = s.f();
+    assert(n==0);
+  }
+}

regression/cbmc-java/stack_var10/stack_var10.j

@@ -0,0 +1,31 @@
+.class public stack_var11
+.super java/lang/Object
+
+.field private arr [I
+
+.method public <init>()V
+.limit stack 5
+   aload_0
+   invokenonvirtual java/lang/Object/<init>()V
+   aload_0
+   iconst_2
+   newarray int
+   putfield stack_var11/arr [I
+   return
+.end method
+
+.method public f()I
+   .limit stack 8
+   .limit locals 5
+   aload_0
+   getfield stack_var11/arr [I
+   iconst_0
+   iaload ;; put arr[0] on stack (currently 0)
+   aload_0
+   getfield stack_var11/arr [I
+   iconst_0
+   iconst_1
+   iastore ;; store 1 in arr[0],
+           ;; value on stack should not be touched
+   ireturn
+.end method

regression/cbmc-java/stack_var10/test.desc

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

regression/cbmc-java/stack_var11/README

@@ -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);
+  }
+}

regression/cbmc-java/stack_var11/stack_test.class

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

regression/cbmc-java/stack_var11/stack_test.java

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

regression/cbmc-java/stack_var11/stack_var11.class

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

regression/cbmc-java/stack_var11/stack_var11.j

@@ -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);
+  }
+}

regression/cbmc-java/stack_var2/README

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

regression/cbmc-java/stack_var2/stack_test.class

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

regression/cbmc-java/stack_var2/stack_test.java

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

regression/cbmc-java/stack_var2/stack_var2.class

@@ -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);
+  }
+}

regression/cbmc-java/stack_var2/stack_var2.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

regression/cbmc-java/stack_var2/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

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.

regression/cbmc-java/stack_var3/stack_test.class

@@ -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);
+  }
+}