From 227e83de4ebf6dce4e10f63f03bd786ee9bbfe37 Mon Sep 17 00:00:00 2001
From: svorenova <maria.svorenova@diffblue.com>
Date: Thu, 26 Apr 2018 14:13:07 +0100
Subject: [PATCH] Adding regression tests for multi-dimensional arrays

Connected to TG-1121 - crash for multidim arrays with non-const size and
non-const element access, and variations of the example.
---
 .../array_nonconstsize_nonconstaccess/A.class | Bin 0 -> 244 bytes
 .../array_nonconstsize_nonconstaccess/A.java  |   3 +++
 .../FloatMultidim1.class                      | Bin 0 -> 508 bytes
 .../FloatMultidim1.java                       |  17 +++++++++++++++++
 .../FloatMultidim2.class                      | Bin 0 -> 510 bytes
 .../FloatMultidim2.java                       |  17 +++++++++++++++++
 .../RefMultidim1.class                        | Bin 0 -> 555 bytes
 .../RefMultidim1.java                         |  18 ++++++++++++++++++
 .../RefMultidim2.class                        | Bin 0 -> 555 bytes
 .../RefMultidim2.java                         |  18 ++++++++++++++++++
 .../RefMultidimConstsize.class                | Bin 0 -> 487 bytes
 .../RefMultidimConstsize.java                 |   8 ++++++++
 .../RefSingledim.class                        | Bin 0 -> 544 bytes
 .../RefSingledim.java                         |  18 ++++++++++++++++++
 .../test_float_multidim_1.desc                |  12 ++++++++++++
 .../test_float_multidim_2.desc                |   8 ++++++++
 .../test_ref_multidim_1.desc                  |  12 ++++++++++++
 .../test_ref_multidim_2.desc                  |  12 ++++++++++++
 .../test_ref_multidim_constsize.desc          |   6 ++++++
 .../test_ref_singledim.desc                   |   8 ++++++++
 20 files changed, 157 insertions(+)
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.class
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.java
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.class
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.class
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.java
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc
 create mode 100644 regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.class
new file mode 100644
index 0000000000000000000000000000000000000000..e31a62ef61b4c664bcd57cbc53f87bef3a770201
GIT binary patch
literal 244
zcmXYry$ZrW5QJxAel*74H?UI+)7U9O5K;v#6#Gj&^du$_6W_~9u<!wVC~;3x>@f4~
z4tJmL>kVLzp^FB34*CuT1QI+U!CtCNl`BGHJUI}|b$*nDUZgU)sjjgs_99N145K^|
z=|L1q=Ng*jS>3oA1q*_^%c~-hq0;AeFuRDm@L<E?hXO)hXFnC$$=}8onUom8;2#0J
ohY728T;SZ~<o`E-HGP5}3=FhbZN|FfvU-1Sq0LUS4y%Fg58tIHO8@`>

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java
new file mode 100644
index 00000000000..da813a5f3de
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/A.java
@@ -0,0 +1,3 @@
+public class A {
+  public float a;
+}
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.class
new file mode 100644
index 0000000000000000000000000000000000000000..f894ebdb1e03d34c2b5dedb798fb8f3847506794
GIT binary patch
literal 508
zcmY*VO-lk%6g_ulY|PBBGAk>{T4+dOxGUTQf}lkdZCX8Ts<BbS#-KmbB7!z8Y!$SK
zHf{Pxfkfx2n+EQE@1A?lIq%N*@B0UU5|%=+uwWx@BV}VzFtz7)T)!+Zv$<1&wckB=
z1ksw?aSr<JhSNJy4Ub5o)@>^9RP|h4Pe9ARa&HB(TE*)szuxzJ_uOq4cLj1m>1;K3
zc2;50VpIi&D$-{R-3w-qebv0KtDA{h=(yYOHJys9{pS8lZnxB(3L}6iLF9jn{<>N4
zROhmA*l0OTAL}r=r~V9xW-;5W3Ot2pVCxO?I%)@*bsLOn=J0p`A<T@hFlLEp^2<at
zmwv!TI{1jSbl?kyQBPY>2wLT51k7@Nb;k-H<p=T!V?dG#ZIBsdlLi)Iv`bQOnbitS
zGPK-8WMp3ATT|pj5M_>Go)PB`E98$cAUAoMz9l%ve?<q*53y{+7((QS@<Os+KlumO
Ct4~`1

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java
new file mode 100644
index 00000000000..b631e2e7617
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim1.java
@@ -0,0 +1,17 @@
+public class FloatMultidim1 {
+  public float[][] f(int y) {
+    if (y > 0 && y < 5) {
+      float[][] a1 = new float[y][2];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j][1] = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.class
new file mode 100644
index 0000000000000000000000000000000000000000..4d40ffc37417eb12b337bd1e8bc679df2cb0c195
GIT binary patch
literal 510
zcmY*VJxc>Y6r8==croV7`0c4+w1`FwN;)Nt5D*eYlr&bG%c&PHiNuTGpRo|ZPP7s%
z>}>o;LJ(&!*SPTB?wj{!W_Q1TKRyAJv5<hotc6Jna~9?W#`e9g7gPky!bU?t9`stS
zK&Iw(-J?OL>Gsc5(<hRv^&I6lRNvEe1j^vbyA{aRs(w!e^?@IFEw8h?Cm=2;T{zr0
zKd-WAGY$m|wL_l~bT5!P4U}_TS2vMb;<PvDJ8sp}epCM?x7+GYB@x4zK>B}+{<>N6
zRrj)V+-$o}fK`}$r(OnxW-(i=O56qa*ycOLTiA{>>oyqU%*oLJ5|{|FBvM2)`6Uu9
z+7DQ><BwR0*<Ub>x-Fj&mz8J4%*vMBT~3~Cy-KNDucVpK7Wpunw2;WsaE6kLtd?k#
zr|CM<p?#URog*iW409IKj7h#?iTn`;6r;=OQ;u`|Ejn<1h(!y=5JLP=UXZLmVCD~Y
C%1?9v

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java
new file mode 100644
index 00000000000..6d80d3b38c5
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/FloatMultidim2.java
@@ -0,0 +1,17 @@
+public class FloatMultidim2 {
+  public float[][] f(int y) {
+    if (y > 0 && y < 5) {
+      float[][] a1 = new float[2][y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[1][j] = 1.0f;
+      return a1;
+    } else {
+      return new float[1][1];
+    }
+  }
+}
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.class
new file mode 100644
index 0000000000000000000000000000000000000000..4102562d05f53b2876a84b9e00ae79c0eae02778
GIT binary patch
literal 555
zcmYjNO-my|5PdZtnIw)HKjKFw?kWpQ6g4DzSWp5Y2twk*W)T)oojC4JjETgF;Ggjz
zg4cKu!3Fi=#eXCO@pX(~H(g!z`c>8IdVamT2e69SI2=qn7<Z70!^Cuq#&eK%Fe8Yp
z2aO;s2+Yj<uE5%C?)!q_V$kq++D8??^;=cyL`I9vs;cj*R-ofPXodfR6TwjNmw!-d
z*TY~xILfUF<UkP3Y|roQ6*qKP<JlG%Dkrc%z%#*MIaJldk~;3!i<g`2R@L7MbjOj;
zMVD*pRJn*E#!?$DzTm6C{mc*~G$&hEjlbESm6~4-NmV>sm_vj!(8~aoAx0Z#l;thF
z?S)&&b?<qAHqrxGpT7G}z#xVgaWY8I>f{Gl+`td-9C<H#fhEs=f?<?A>k?6`a0S~e
zEY9Su|1kgD!YXS&@7};(?8qaG4s%WDe%~ob`!Uu_uzQkXQ;gDl%}_y(-B;LI>sf`3
uNpeRpN}IqpjA5MLN)vs@sHm@2dr9&H6U-cj*+t5M(S^thAz_N1$kZE{<5Ua)

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.java
new file mode 100644
index 00000000000..58ed13eaaa4
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim1.java
@@ -0,0 +1,18 @@
+public class RefMultidim1 {
+  public A[][] f(int y) {
+    if (y > 0 && y < 5) {
+      A[][] a1 = new A[y][2];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j][1] = new A();
+      a1[j][1].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.class
new file mode 100644
index 0000000000000000000000000000000000000000..fa85a072b9f289ec63d816343f866116cb8762ec
GIT binary patch
literal 555
zcmYjNTWeZD5dP*|JZg`Z+}i5VUI+v&NhCH8ffhju0YMvxMJRb%^&~mgOEAYk{!AW9
zA+O0p2{h35r7!(Q1u6a3Sa6q}o%!~gnQ!O!-*4Xm?BYcn4l)i_9c1G$k%`fG4ss6i
zg2>xo7=#spStzyy*1J*H7o_UJ(0@M}wEgi1)$S8nu8%sZ-%{g1$8*pMPlIzovVQ0v
zHzxfs=mvxG8-W}PqJ>)V=%`-RVUMRKFw~B~{tsRX63tL`J~h<Yyk5LHnv6UCexN%p
zEf(GGsSD*IiWo~(T|C2cfxE~Mq&271SHqLiLA&R7LQ)maK3*ci8R%tz$`GTCGb-^G
z-uA0I$nEU;5p84!vOazHfq(>(j5ryjX?5}sSlqy#cZISS{fsT!`vt>jc-9w0t;#iQ
zv$AQG^Y<`6-oa{WzwCa6y?G-)Vcam+gzmRNLE4Y8UYgz4C^pL|$JYWC?6CW5cGh}!
wVdDw8OIW5&V;w74<+pM~A22GKtJU5bd4k8xOu?KY>%f>o<PRZXik`^Rf1I{d4*&oF

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java
new file mode 100644
index 00000000000..ae5be7d1ecd
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidim2.java
@@ -0,0 +1,18 @@
+public class RefMultidim2 {
+  public A[][] f(int y) {
+    if (y > 0 && y < 5) {
+      A[][] a1 = new A[2][y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[1][j] = new A();
+      a1[1][j].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.class
new file mode 100644
index 0000000000000000000000000000000000000000..c474465f50d05b7d9dcdf10cc5cfef773c1f0e77
GIT binary patch
literal 487
zcmZuuT}uK%6g_u8+}yS@Gt<hXH<L(`-U>kkL0Ahigz#z9wMN!m(6y+4)k6pcz4g+M
ziteb;i!;ofxgY18%blO!k1qfh$lI`xv5>NmwV@*uXR~kNz``LRb|nKDRS0_Fq)jkt
zVc#Qcxiavsr=zYnz7t)aBS|;x3BN7IQu)iE5k1NYA?@CJgXYwaWM7VIVK9j%^3}T}
z(0~~W4Mj{Zd>RBzoD<AW$E~XTkYKmM>A2_BrBcbRB03w2C*fcXaYj@f<Zwhtt*Rs>
zRBg!@!9(e$JM?-HLj<2XjuGQIsHK4v8C#pZ65qtPS)761=IM2|v3Zc-@Y`7wU;~@%
z@pO=2tH94NcmsLU{D!7Ajml}RY<xn$pTTIUciDM|`A?gM$>lnCVsHm0c3J3%Jtb3I
fP%UMc6x&F$5dR)_kmA1MNHZeIcpf?<H0=EWFu+av

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java
new file mode 100644
index 00000000000..90692e0392a
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefMultidimConstsize.java
@@ -0,0 +1,8 @@
+public class RefMultidimConstsize {
+  public void f(int y) {
+    A[][] a1 = new A[2][2];
+    int j = 1;
+    a1[j][1] = new A();
+    a1[j][1].a = 1.0f;
+  }
+}
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.class b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.class
new file mode 100644
index 0000000000000000000000000000000000000000..741443d1e2d27d55e857a922be25eed2a6bea976
GIT binary patch
literal 544
zcmYjN%Syvg5IvKmO^s2j^-+!W0phb-6n9EN1VN|@Rs?Z%+om<Orc$fm&$tl5tu9nh
z^aK1OLBw-w7be`9JCpO6$>-1O2Y^*fIEZ4{#)tz0!yOEsjZqsZL3BL`gJxD>&dwbQ
ztj&7K7xd(U(BHj0EBK8ARj9Gkm#Y_5?NBuWUALQ7^CY+sbm#W{ay|$vHNO;`tqG(o
zuxGdDj&mEjs`6|L47E&ycJErym2axz>5e*Yso6*foP7PVQS`S0ZQ1)@b*ZYZlnWa%
zify<U!??ixj}XK)CR0;kC9_wk`o$)pif0Rxi0}{S#{fq|jIo1NhFO>+^DmIc)@O$?
z+G+|qd3XN+%w4RwEP5C<`56{pig-6jd$C*0c<(TFJnIfID|?TKnN6qOU>v=`%%@W;
z?h~x^gFKL8LfcHYWK2ejvQZ>BS(4QVji+e1K+8qi=`mKh!2o%2^fGp19DT$a#3tH3
ez0Kc{`qodJkOA_|ZzOFDenaGoG{F$t29m$8G*TY`

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.java b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.java
new file mode 100644
index 00000000000..1237623d6f5
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/RefSingledim.java
@@ -0,0 +1,18 @@
+public class RefSingledim {
+  public A[] f(int y) {
+    if (y > 0 && y < 5) {
+      A[] a1 = new A[y];
+      int j;
+      if (y > 1) {
+        j = 1;
+      } else {
+        j = 0;
+      }
+      a1[j] = new A();
+      a1[j].a = 1.0f;
+      return a1;
+    } else {
+      return null;
+    }
+  }
+}
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc
new file mode 100644
index 00000000000..54c7ed67f46
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_1.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+FloatMultidim1.class
+--function FloatMultidim1.f --cover location --unwind 3
+\d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This crashes during symex, with error 'cannot unpack array of nonconst size'
+when trying to access the element of the array. Symex uses byte_extract_little
+_endian to access the element which does not get simplified (it seems the
+problem is that the types in the instruction do not match). TG-1121
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc
new file mode 100644
index 00000000000..9f1c5d4581b
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_float_multidim_2.desc
@@ -0,0 +1,8 @@
+CORE
+FloatMultidim2.class
+--function FloatMultidim2.f --cover location --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+y=1$
+y=[2-4]$
+y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc
new file mode 100644
index 00000000000..f96f028e32f
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_1.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+RefMultidim1.class
+--function RefMultidim1.f --cover location --unwind 3
+\d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This crashes during symex, with error 'cannot unpack array of nonconst size'
+when trying to access the element of the array. Symex uses byte_extract_little
+_endian to access the element which does not get simplified (it seems the
+problem is that the types in the instruction do not match). TG-1121
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc
new file mode 100644
index 00000000000..190b154c371
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_2.desc
@@ -0,0 +1,12 @@
+KNOWNBUG
+RefMultidim2.class
+--function RefMultidim2.f --cover location --unwind 3
+\d+ of \d+ covered
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This crashes during symex, with error 'cannot unpack array of nonconst size'
+when trying to access the element of the array. Symex uses byte_extract_little
+_endian to access the element which does not get simplified (it seems the
+problem is that the types in the instruction do not match). TG-1121
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc
new file mode 100644
index 00000000000..eeb64c3e6b1
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_multidim_constsize.desc
@@ -0,0 +1,6 @@
+CORE
+RefMultidimConstsize.class
+--function RefMultidimConstsize.f --cover location --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+y=-*[0-9]+$
diff --git a/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc
new file mode 100644
index 00000000000..84db685c705
--- /dev/null
+++ b/regression/cbmc-java/array_nonconstsize_nonconstaccess/test_ref_singledim.desc
@@ -0,0 +1,8 @@
+CORE
+RefSingledim.class
+--function RefSingledim.f --cover location --unwind 3
+^EXIT=0$
+^SIGNAL=0$
+y=1$
+y=[2-4]$
+y=([05-9]|[1-9][0-9]+|-[1-9][0-9]*)$