Skip to content

Commit 69bf02d

Browse files
smowtonsmowton
authored
Merge pull request #5057 from smowton/romain/feature/array-cell-sensitivity
Array-cell sensitivity
2 parents e7f2930 + 123a68e commit 69bf02d

File tree

78 files changed

+1021
-52
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

78 files changed

+1021
-52
lines changed

‎jbmc/regression/jbmc/array-cell-sensitivity1/Test.class

642 Bytes
Binary file not shown.

‎jbmc/regression/jbmc/array-cell-sensitivity1/Test.java

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
public class Test {
2+
3+
public static void main(int unknown) {
4+
5+
int[] x = new int[10];
6+
x[unknown] = 1;
7+
x[1] = unknown;
8+
assert (x[1] == unknown);
9+
}
10+
}

‎jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
Test.class
3+
--function Test.main --show-vcc --max-field-sensitivity-array-size 10
4+
symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
5+
symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
6+
symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
7+
symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
8+
symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
9+
symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
10+
symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
11+
symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
12+
symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
13+
symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
14+
symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
15+
^EXIT=0$
16+
^SIGNAL=0$
17+
--
18+
--
19+
This checks that field sensitvity is still applied to an array of size 10
20+
when the max is set to 10.

‎jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
Test.class
3+
--function Test.main --show-vcc --max-field-sensitivity-array-size 9
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
symex_dynamic::dynamic_2_array#[0-9]\[1\]
7+
--
8+
symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
9+
--
10+
This checks that field sensitvity is not applied to an array of size 10
11+
when the max is set to 9.

‎jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
Test.class
3+
--function Test.main --show-vcc --no-array-field-sensitivity
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
symex_dynamic::dynamic_2_array#[0-9]\[1\]
7+
--
8+
symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
9+
--
10+
This checks that field sensitvity is not applied to arrays when
11+
no-array-field-sensitivity is used.

‎jbmc/regression/jbmc/array-cell-sensitivity1/test.desc

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
CORE
2+
Test.class
3+
--function Test.main --show-vcc
4+
symex_dynamic::dynamic_2_array#2\[\[0\]\] = symex_dynamic::dynamic_2_array#2\[0\]
5+
symex_dynamic::dynamic_2_array#2\[\[1\]\] = symex_dynamic::dynamic_2_array#2\[1\]
6+
symex_dynamic::dynamic_2_array#2\[\[2\]\] = symex_dynamic::dynamic_2_array#2\[2\]
7+
symex_dynamic::dynamic_2_array#2\[\[3\]\] = symex_dynamic::dynamic_2_array#2\[3\]
8+
symex_dynamic::dynamic_2_array#2\[\[4\]\] = symex_dynamic::dynamic_2_array#2\[4\]
9+
symex_dynamic::dynamic_2_array#2\[\[5\]\] = symex_dynamic::dynamic_2_array#2\[5\]
10+
symex_dynamic::dynamic_2_array#2\[\[6\]\] = symex_dynamic::dynamic_2_array#2\[6\]
11+
symex_dynamic::dynamic_2_array#2\[\[7\]\] = symex_dynamic::dynamic_2_array#2\[7\]
12+
symex_dynamic::dynamic_2_array#2\[\[8\]\] = symex_dynamic::dynamic_2_array#2\[8\]
13+
symex_dynamic::dynamic_2_array#2\[\[9\]\] = symex_dynamic::dynamic_2_array#2\[9\]
14+
symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
15+
^EXIT=0$
16+
^SIGNAL=0$
17+
--
18+
symex_dynamic::dynamic_2_array#3\[\[[023456789]\]\] =
19+
--
20+
This checks that a write to a Java array with an unknown index uses a whole-array
21+
write followed by array-cell expansion, but one targeting a constant index uses
22+
a single-cell symbol without expansion.

‎jbmc/regression/jbmc/array-cell-sensitivity2/Test.class

1.15 KB
Binary file not shown.

‎jbmc/regression/jbmc/array-cell-sensitivity2/Test.java

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
public class Test {
2+
3+
public int data;
4+
public Test[] children = new Test[2];
5+
6+
public static void main(int unknown) {
7+
8+
Test[] root = new Test[2];
9+
Test node1 = new Test();
10+
Test node2 = new Test();
11+
root[0] = node1;
12+
root[1] = node2;
13+
node1.children[0] = unknown % 2 == 0 ? node1 : node2;
14+
node1.children[1] = unknown % 3 == 0 ? node1 : node2;
15+
node2.children[0] = unknown % 5 == 0 ? node1 : node2;
16+
node2.children[1] = unknown % 7 == 0 ? node1 : node2;
17+
int idx1 = 0, idx2 = 1, idx3 = 1, idx4 = 0;
18+
root[idx1].children[idx2].children[idx3].children[idx4].data = 1;
19+
assert (node1.data == 1);
20+
}
21+
}

‎jbmc/regression/jbmc/array-cell-sensitivity2/test.desc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
Test.class
3+
--function Test.main --show-vcc
4+
symex_dynamic::dynamic_object6#3\.\.data =
5+
symex_dynamic::dynamic_object3#3\.\.data =
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
symex_dynamic::dynamic_object6#3\.\.data = symex_dynamic::dynamic_object6#3\.data
10+
symex_dynamic::dynamic_object3#3\.\.data = symex_dynamic::dynamic_object3#3\.data
11+
--
12+
This checks that a write using a mix of field and array accessors uses a field-sensitive
13+
symbol (the data field of the possible ultimate target objects) rather than using
14+
a whole-struct write followed by an expansion.

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,25 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
135135
parse_java_language_options(cmdline, options);
136136
parse_java_object_factory_options(cmdline, options);
137137

138+
if(cmdline.isset("max-field-sensitivity-array-size"))
139+
{
140+
options.set_option(
141+
"max-field-sensitivity-array-size",
142+
cmdline.get_value("max-field-sensitivity-array-size"));
143+
}
144+
145+
if(cmdline.isset("no-array-field-sensitivity"))
146+
{
147+
if(cmdline.isset("max-field-sensitivity-array-size"))
148+
{
149+
log.error()
150+
<< "--no-array-field-sensitivity and --max-field-sensitivity-array-size"
151+
<< " must not be given together" << messaget::eom;
152+
exit(CPROVER_EXIT_USAGE_ERROR);
153+
}
154+
options.set_option("no-array-field-sensitivity", true);
155+
}
156+
138157
if(cmdline.isset("show-symex-strategies"))
139158
{
140159
log.status() << show_path_strategies() << messaget::eom;

‎regression/cbmc-concurrency/norace_array1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
CORE pthread
22
main.c
33

44
^EXIT=0$

‎regression/cbmc-concurrency/norace_array2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG pthread
1+
CORE pthread
22
main.c
33

44
^EXIT=0$

‎regression/cbmc-concurrency/struct_and_array1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE pthread
22
main.c
33

44
^EXIT=0$

‎regression/cbmc/Multi_Dimensional_Array3/test.desc

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,11 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33

44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$
77
--
88
^warning: ignoring
9+
--
10+
With the SMT backend this incorrect result because of the bug documented here:
11+
https://github.com/diffblue/cbmc/issues/4749

‎regression/cbmc/address_space_size_limit3/main.i

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,11 @@ void f__L_0x3c6_0()
9292

9393
int main()
9494
{
95+
int unknown;
96+
// Avoid constant propagation solving for pointer-offsets of esp,
97+
// which prevent demonstrating the object-size limitation this test
98+
// intends to exhibit:
99+
esp -= (unknown & 1);
95100
L_0x3fe_0: esp-=0x4;
96101
L_0x3fe_1: *(uint32_t*)(esp)=ebp;
97102
L_0x3ff_0: ebp=esp;

‎regression/cbmc/array-cell-sensitivity1/test.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char **argv)
4+
{
5+
int array[10];
6+
array[argc] = 1;
7+
array[1] = argc;
8+
assert(array[1] == argc);
9+
}

‎regression/cbmc/array-cell-sensitivity1/test.desc

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
CORE
2+
test.c
3+
--show-vcc
4+
main::1::array!0@1#2\[\[1\]\] = main::1::array!0@1#1\[1\]
5+
main::1::array!0@1#2\[\[2\]\] = main::1::array!0@1#1\[2\]
6+
main::1::array!0@1#2\[\[3\]\] = main::1::array!0@1#1\[3\]
7+
main::1::array!0@1#2\[\[4\]\] = main::1::array!0@1#1\[4\]
8+
main::1::array!0@1#2\[\[5\]\] = main::1::array!0@1#1\[5\]
9+
main::1::array!0@1#2\[\[6\]\] = main::1::array!0@1#1\[6\]
10+
main::1::array!0@1#2\[\[7\]\] = main::1::array!0@1#1\[7\]
11+
main::1::array!0@1#2\[\[8\]\] = main::1::array!0@1#1\[8\]
12+
main::1::array!0@1#2\[\[9\]\] = main::1::array!0@1#1\[9\]
13+
main::1::array!0@1#3\[\[1\]\] =
14+
^EXIT=0$
15+
^SIGNAL=0$
16+
--
17+
main::1::array!0@1#[2-9]\[[0-9]+\]
18+
--
19+
This checks that a write with a non-constant index leads to a whole-array
20+
operation followed by expansion into individual array cells, while a write with
21+
a constant index leads to direct use of a single cell symbol

‎regression/cbmc/array-cell-sensitivity1/test_execution.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
4+
^VERIFICATION SUCCESSFUL$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
--
9+
The real test is in test.desc; this is a companion to check that the program under
10+
test actually behaves as expected.

‎regression/cbmc/array-cell-sensitivity10/test.c

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#include <assert.h>
2+
3+
struct A
4+
{
5+
int x;
6+
int y;
7+
};
8+
9+
int main(int argc, char **argv)
10+
{
11+
struct A array[10];
12+
struct A other[2];
13+
struct A *ptr = argc % 2 ? &other : &array[0];
14+
ptr[argc].x = 1;
15+
ptr[1].x = argc;
16+
assert(ptr[1].x == argc);
17+
assert(array[1].x == argc);
18+
}

‎regression/cbmc/array-cell-sensitivity10/test.desc

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
CORE
2+
test.c
3+
--show-vcc
4+
main::1::array!0@1#2\[\[0\]\]..x = main::1::array!0@1#1\[0\].x
5+
main::1::array!0@1#2\[\[1\]\]..x = main::1::array!0@1#1\[1\].x
6+
main::1::array!0@1#2\[\[2\]\]..x = main::1::array!0@1#1\[2\].x
7+
main::1::array!0@1#2\[\[3\]\]..x = main::1::array!0@1#1\[3\].x
8+
main::1::array!0@1#2\[\[4\]\]..x = main::1::array!0@1#1\[4\].x
9+
main::1::array!0@1#2\[\[5\]\]..x = main::1::array!0@1#1\[5\].x
10+
main::1::array!0@1#2\[\[6\]\]..x = main::1::array!0@1#1\[6\].x
11+
main::1::array!0@1#2\[\[7\]\]..x = main::1::array!0@1#1\[7\].x
12+
main::1::array!0@1#2\[\[8\]\]..x = main::1::array!0@1#1\[8\].x
13+
main::1::array!0@1#2\[\[9\]\]..x = main::1::array!0@1#1\[9\].x
14+
main::1::array!0@1#3\[\[1\]\]..x =
15+
main::1::array!0@1#2\[\[0\]\]..y = main::1::array!0@1#1\[0\].y
16+
main::1::array!0@1#2\[\[1\]\]..y = main::1::array!0@1#1\[1\].y
17+
main::1::array!0@1#2\[\[2\]\]..y = main::1::array!0@1#1\[2\].y
18+
main::1::array!0@1#2\[\[3\]\]..y = main::1::array!0@1#1\[3\].y
19+
main::1::array!0@1#2\[\[4\]\]..y = main::1::array!0@1#1\[4\].y
20+
main::1::array!0@1#2\[\[5\]\]..y = main::1::array!0@1#1\[5\].y
21+
main::1::array!0@1#2\[\[6\]\]..y = main::1::array!0@1#1\[6\].y
22+
main::1::array!0@1#2\[\[7\]\]..y = main::1::array!0@1#1\[7\].y
23+
main::1::array!0@1#2\[\[8\]\]..y = main::1::array!0@1#1\[8\].y
24+
main::1::array!0@1#2\[\[9\]\]..y = main::1::array!0@1#1\[9\].y
25+
^EXIT=0$
26+
^SIGNAL=0$
27+
--
28+
--
29+
This checks that a write with a non-constant index leads to a whole-array
30+
operation followed by expansion into individual array cells, while a write with
31+
a constant index leads to direct use of a single cell symbol, for the case where
32+
the array element is struct-typed and accessed via a pointer.

‎regression/cbmc/array-cell-sensitivity10/test_execution.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
test.c
3+
4+
^VERIFICATION FAILED$
5+
^\[main.assertion\.1\] line 16.*SUCCESS$
6+
^\[main.assertion\.2\] line 17.*FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
--
11+
The real test is in test.desc; this is a companion to check that the program under
12+
test actually behaves as expected.

‎regression/cbmc/array-cell-sensitivity11/test.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
struct A
4+
{
5+
int x;
6+
int y;
7+
};
8+
9+
int main(int argc, char **argv)
10+
{
11+
struct A array[10];
12+
int *ptr = argc % 2 ? &argc : &array[0].y;
13+
*ptr = argc;
14+
assert(*ptr == argc);
15+
assert(array[1].y == argc);
16+
}

‎regression/cbmc/array-cell-sensitivity11/test.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
test.c
3+
--show-vcc
4+
main::1::array!0@1#2\[\[0\]\]..y =
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
main::1::array!0@1#[2-9]\[\[[1-9]\]\]
9+
main::1::array!0@1#[3-9]\[\[[0-9]\]\]
10+
--
11+
This checks that an array access made via a pointer to a member of the array's
12+
element struct type is executed using a field-sensitive symbol.

‎regression/cbmc/array-cell-sensitivity11/test_execution.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
test.c
3+
4+
^VERIFICATION FAILED$
5+
^\[main.assertion\.1\] line 14.*SUCCESS$
6+
^\[main.assertion\.2\] line 15.*FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
--
11+
The real test is in test.desc; this is a companion to check that the program under
12+
test actually behaves as expected.

‎regression/cbmc/array-cell-sensitivity12/test.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
#include <assert.h>
2+
3+
struct A
4+
{
5+
int x;
6+
int y;
7+
};
8+
9+
int main(int argc, char **argv)
10+
{
11+
struct A array[10];
12+
int *ptr = argc % 2 ? &array[0].x : &array[0].y;
13+
*ptr = argc;
14+
assert(*ptr == argc);
15+
assert(array[0].y == argc);
16+
}

‎regression/cbmc/array-cell-sensitivity12/test.desc

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
FUTURE
2+
test.c
3+
--show-vcc
4+
main::1::array!0@1#2\[\[0\]\]..x =
5+
main::1::array!0@1#2\[\[0\]\]..y =
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
main::1::array!0@1#[2-9]\[\[[1-9]\]\]
10+
main::1::array!0@1#[3-9]\[\[[0-9]\]\]
11+
--
12+
Ideally we should handle accesses to a pointer with a finite set of possible
13+
referents precisely, but because value_sett regards &array[0].x and &array[0].y
14+
as two different offsets into the same allocation and discards the precise offsets
15+
they point to, this is currently handled imprecisely with a byte_update operation.

‎regression/cbmc/array-cell-sensitivity12/test_execution.desc

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
test.c
3+
4+
^VERIFICATION FAILED$
5+
^\[main.assertion\.1\] line 14.*SUCCESS$
6+
^\[main.assertion\.2\] line 15.*FAILURE$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
--
11+
The real test is in test.desc; this is a companion to check that the program under
12+
test actually behaves as expected.

0 commit comments

Comments
 (0)