From bc47e4906eaef342bbfc10604080e532f2c391b1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 17 Sep 2019 14:04:29 +0100 Subject: [PATCH] Add regression test for static array propagation This checks that array cell sensitivity works fine for static arrays, whether we use the --static-values option or not. --- .../Test.class | Bin 0 -> 862 bytes .../Test.java | 36 ++++++++++++++++++ .../Util.class | Bin 0 -> 321 bytes .../static-values.json | 17 +++++++++ .../test-char-array-ref-static-values.desc | 13 +++++++ .../test-char-array-ref.desc | 13 +++++++ .../test-char-array-static-values.desc | 13 +++++++ .../test-char-array1.desc | 12 ++++++ 8 files changed, 104 insertions(+) create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/static-values.json create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc create mode 100644 jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..a41151d6a03b4e4b041718a03994d54bd215b4cd GIT binary patch literal 862 zcmZ9KOK;Oq5QWe6BTgK*b<#Esp-JciND870vaAqMC=!T=L|Y`v%CRrt5)x!PAXfa3 zZeYh2h(r-cu;)i1&UM=))RyO7AJ3inX2yU1{`du;g{wAfoX^3+vNBZ*H5lf# zX5f%c9kp=D!DTcoG#zZ({e%Tfq)v~u3zPyGhmj1%fk~eX`GJMA55`^+ z_5@5-14XlOhc&X{7H0zJ$SF+ja*70S%Zixq2ACfO+9KboTm@Hi;|SslH*7s^CKdBM zynsdSmFrs`RoC`cXgZ%vYme4&B^Uh=i%M>}!3X4j!gz87^Y^sg{!iCFGmw_1D#7Hw zNa}e~EuhJSZIpN`R;{^2h@~;a`w2wmEQCtm{)j@Fc5MQYVx8(!a8nR9whgGL-J{p=vatIXBf1&ZTaZe=M<>k^lez literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java new file mode 100644 index 0000000000..0d4ff9303a --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Test.java @@ -0,0 +1,36 @@ +class Util { + public static char[] chars(int count) { + char result[] = new char[count]; + for (int i = 0; i < count; ++i) { + result[i] = (char)((int)'a' + i); + } + return result; + } +} + +public class Test { + // static field which is initialized to a non-empty value + public static char[] staticCharArray = Util.chars(26); + // reference to the same array + public static char[] staticCharArrayRef = staticCharArray; + + public static char[] charArray() { + staticCharArray[0] = staticCharArray[3]; + staticCharArray[1] = 'e'; + assert staticCharArray[0] == 'd'; + assert staticCharArray[0] == 'A'; + return staticCharArray; + } + + public static char[] charArrayRef() { + staticCharArrayRef[0] = staticCharArray[3]; + staticCharArray[1] = 'e'; + if (staticCharArray[0] == 'A') { + assert false; + } else if (staticCharArray[0] == 'd') { + assert false; + } + + return staticCharArray; + } +} diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/Util.class new file mode 100644 index 0000000000000000000000000000000000000000..4eeec1101214289a09a31022d09de403d7ba6b19 GIT binary patch literal 321 zcmX9&%}T>y5S;yzG@7P1tsqz)5Oyc*kJIl=O?0)>bz601r-GPA>8&w;gptP5alk7lXG+So^Gnib&f@(Jz z$0v)MVLa>WVM@k|uJmk9Y#y}+fuPdMbaZ{Jr-g2#CUAO_#Vm>sle~YqAJ4O$k-pU~ zOjvXdvm_OGIn_z^__A|49K}&4P=f$lP`oOCiopT!G*+8LAzIrnkY^SGo4Hhw+=3;> ze{0CG++w5gW_68yzwv-t+xN78ejnZ`dHnrsKT%eN!5TM!?IwSj^(t|libK|g`bNn{ NS-w!Gxm!$C{s6BCG%WxC literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/static-values.json b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/static-values.json new file mode 100644 index 0000000000..9607ce108a --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/static-values.json @@ -0,0 +1,17 @@ +{ + "@type":"com.diffblue.retriever.StaticFieldMap", + "Test":{ + "@type":"com.diffblue.retriever.StaticFieldMap", + "staticCharArrayRef":{ + "@type":"[C", + "@ref": "id1" + }, + "staticCharArray":{ + "@type":"[C", + "@id": "id1", + "@items":[ + "abcAefghijklmnopqrstuvwxyz" + ] + } + } +} diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc new file mode 100644 index 0000000000..a7bb9e69ad --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc @@ -0,0 +1,13 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.2" --static-values static-values.json +Generated 0 VCC[(]s[)], 0 remaining after simplification +assertion at file Test.java line 31 .*: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Not that the json file has been modified on purpose so that this checks +that it is actually loaded and not retrieved by execution of the Util function. +This test does not work with symex-driven-lazy-loading because this option is +not compatible with --property. diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc new file mode 100644 index 0000000000..b1a08a7af1 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc @@ -0,0 +1,13 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.1" +Generated 0 VCC[(]s[)], 0 remaining after simplification +assertion at file Test.java line 29 .*: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Note that the json file has been modified on purpose so that this checks +that it is actually loaded and not retrieved by execution of the Util function. +This test does not work with symex-driven-lazy-loading because this option is +not compatible with --property. diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc new file mode 100644 index 0000000000..d00d568de8 --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc @@ -0,0 +1,13 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--function Test.charArray --property "java::Test.charArray:()[C.assertion.2" --static-values static-values.json +Generated 0 VCC[(]s[)], 0 remaining after simplification +assertion at file Test.java line 21 .*: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Note that the json file has been modified on purpose so that this checks +that it is actually loaded and not retrieved by execution of the Util function. +This test does not work with symex-driven-lazy-loading because this option is +not compatible with --property. diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc new file mode 100644 index 0000000000..e515604e4a --- /dev/null +++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc @@ -0,0 +1,12 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--function Test.charArray --property "java::Test.charArray:()[C.assertion.1" +Generated 0 VCC[(]s[)], 0 remaining after simplification +assertion at file Test.java line 20 .*: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Checks that constant propagation happens through static arrays. +This test does not work with symex-driven-lazy-loading because this option is +not compatible with --property.