Add regression tests for dup2, dup2_x1 and dup2_x2

Author: Matthias Güdemann

regression/cbmc-java/stack_var5/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);
+  }
+}

regression/cbmc-java/stack_var5/stack_test.java

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

regression/cbmc-java/stack_var5/stack_var5.class

@@ -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_var5/stack_var5.j

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

regression/cbmc-java/stack_var5/test.desc

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

regression/cbmc-java/stack_var6/stack_test.class

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

regression/cbmc-java/stack_var6/stack_var6.class

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

regression/cbmc-java/stack_var6/stack_var6.j

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