Skip to content

Commit 72fb131

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #7479 from peterschrammel/shadow-memory-tests
Tests for future shadow memory feature
2 parents 5cabd3b + 2a78b3d commit 72fb131

File tree

68 files changed

+2233
-1
lines changed

Some content is hidden

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

68 files changed

+2233
-1
lines changed

‎regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,7 @@ add_subdirectory(cbmc-cover)
3838
add_subdirectory(cbmc-incr-oneloop)
3939
add_subdirectory(cbmc-incr-smt2)
4040
add_subdirectory(cbmc-incr)
41+
add_subdirectory(cbmc-shadow-memory)
4142
add_subdirectory(cbmc-output-file)
4243
add_subdirectory(cbmc-with-incr)
4344
add_subdirectory(array-refinement-with-incr)

‎regression/Makefile

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
11
# For the best possible utilisation of multiple cores when
22
# running tests in parallel, it is important that these directories are
33
# listed with decreasing runtimes (i.e. longest running at the top)
4-
DIRS = cbmc \
4+
DIRS = cbmc-shadow-memory \
5+
cbmc \
56
cbmc-library \
67
cprover \
78
crangler \

‎regression/cbmc-shadow-memory/CMakeLists.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
add_test_pl_tests(
2+
"$<TARGET_FILE:cbmc>"
3+
)

‎regression/cbmc-shadow-memory/Makefile

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
default: tests.log
2+
3+
test:
4+
@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
5+
6+
test-cprover-smt2:
7+
@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
8+
9+
tests.log: ../test.pl
10+
@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
11+
12+
show:
13+
@for dir in *; do \
14+
if [ -d "$$dir" ]; then \
15+
vim -o "$$dir/*.c" "$$dir/*.out"; \
16+
fi; \
17+
done;
18+
19+
clean:
20+
find -name '*.out' -execdir $(RM) '{}' \;
21+
find -name '*.smt2' -execdir $(RM) '{}' \;
22+
$(RM) tests.log

‎regression/cbmc-shadow-memory/char1/main.c

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
#include <assert.h>
2+
3+
// Add some string constants to confuse the value sets.
4+
const char *x1 = "This is a short string constant";
5+
const char *x2 = "This is a loooooooooooooonger string constant";
6+
const char *x3 = "And yet another string constant";
7+
8+
int main()
9+
{
10+
__CPROVER_field_decl_local("field1", (_Bool)0);
11+
__CPROVER_field_decl_global("field1", (_Bool)0);
12+
13+
// Add some string constants to confuse the value sets.
14+
const char *y1 = "Yes, this is a short string constant";
15+
const char *y2 = "Yes, this is a loooooooooooooonger string constant";
16+
const char *y3 = "Yes, and yet another string constant";
17+
18+
char *a;
19+
assert(__CPROVER_get_field(a, "field1") == 0);
20+
assert(__CPROVER_get_field(&a, "field1") == 0);
21+
// Cannot set because a doesn't point anywhere.
22+
__CPROVER_set_field(a, "field1", 1);
23+
// Hence, the value is still 0.
24+
assert(__CPROVER_get_field(a, "field1") == 0);
25+
assert(__CPROVER_get_field(&a, "field1") == 0);
26+
27+
__CPROVER_set_field(a, "field1", 0);
28+
__CPROVER_set_field(&a, "field1", 1);
29+
assert(__CPROVER_get_field(a, "field1") == 0);
30+
assert(__CPROVER_get_field(&a, "field1") == 1);
31+
32+
char *b = (char *)0;
33+
assert(__CPROVER_get_field(b, "field1") == 0);
34+
assert(__CPROVER_get_field(&b, "field1") == 0);
35+
// Cannot set because b points to NULL.
36+
__CPROVER_set_field(b, "field1", 1);
37+
// Hence, the value is still 0.
38+
assert(__CPROVER_get_field(b, "field1") == 0);
39+
assert(__CPROVER_get_field(&b, "field1") == 0);
40+
41+
__CPROVER_set_field(b, "field1", 0);
42+
__CPROVER_set_field(&b, "field1", 1);
43+
assert(__CPROVER_get_field(b, "field1") == 0);
44+
assert(__CPROVER_get_field(&b, "field1") == 1);
45+
46+
static char *c;
47+
assert(__CPROVER_get_field(c, "field1") == 0);
48+
assert(__CPROVER_get_field(&c, "field1") == 0);
49+
// Cannot set because c doesn't point anywhere.
50+
__CPROVER_set_field(c, "field1", 1);
51+
// Hence, the value is still 0.
52+
assert(__CPROVER_get_field(c, "field1") == 0);
53+
assert(__CPROVER_get_field(&c, "field1") == 0);
54+
55+
__CPROVER_set_field(c, "field1", 0);
56+
__CPROVER_set_field(&c, "field1", 1);
57+
assert(__CPROVER_get_field(c, "field1") == 0);
58+
assert(__CPROVER_get_field(&c, "field1") == 1);
59+
}

‎regression/cbmc-shadow-memory/char1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-shadow-memory/constchar-param1/main.c

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
#include <assert.h>
2+
3+
void test(const char *str)
4+
{
5+
// Set shadow memory for some characters
6+
for(int i = 1; i < 6; ++i)
7+
{
8+
__CPROVER_set_field(&str[i], "field1", 1);
9+
}
10+
11+
// Copy string constant into buffer
12+
char buffer[10];
13+
for(int i = 0; i < 7; ++i)
14+
{
15+
buffer[i] = str[i];
16+
__CPROVER_set_field(
17+
&buffer[i], "field1", __CPROVER_get_field(&str[i], "field1"));
18+
}
19+
20+
// Check that shadow memory has not been copied
21+
for(int i = 0; i < 7; ++i)
22+
{
23+
assert(__CPROVER_get_field(&buffer[0], "field1") == 0);
24+
}
25+
26+
// Copy shadow memory
27+
for(int i = 0; i < 7; ++i)
28+
{
29+
__CPROVER_set_field(
30+
&buffer[i], "field1", __CPROVER_get_field(&str[i], "field1"));
31+
}
32+
33+
// Check that shadow memory has been copied
34+
assert(__CPROVER_get_field(&buffer[0], "field1") == 0);
35+
assert(__CPROVER_get_field(&buffer[1], "field1") == 1);
36+
assert(__CPROVER_get_field(&buffer[2], "field1") == 1);
37+
assert(__CPROVER_get_field(&buffer[3], "field1") == 1);
38+
assert(__CPROVER_get_field(&buffer[4], "field1") == 1);
39+
assert(__CPROVER_get_field(&buffer[5], "field1") == 1);
40+
assert(__CPROVER_get_field(&buffer[6], "field1") == 0);
41+
assert(__CPROVER_get_field(&buffer[7], "field1") == 0);
42+
assert(__CPROVER_get_field(&buffer[8], "field1") == 0);
43+
assert(__CPROVER_get_field(&buffer[9], "field1") == 0);
44+
}
45+
46+
int main()
47+
{
48+
__CPROVER_field_decl_local("field1", (_Bool)0);
49+
// Needed because the string constant is in the global pool.
50+
__CPROVER_field_decl_global("field1", (_Bool)0);
51+
52+
test("!Hello!");
53+
}

‎regression/cbmc-shadow-memory/constchar-param1/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
FUTURE
2+
main.c
3+
--unwind 11
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
^Generated 11 VCC\(s\), 0 remaining after simplification$
8+
--
9+
^warning: ignoring

‎regression/cbmc-shadow-memory/constchar-pointers1/main.c

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
__CPROVER_field_decl_local("field1", (_Bool)0);
6+
// Needed because the string constant is in the global pool.
7+
__CPROVER_field_decl_global("field1", (_Bool)0);
8+
9+
const char *str = "!Hello!";
10+
11+
// Set shadow memory for some characters
12+
for(int i = 1; i < 6; ++i)
13+
{
14+
__CPROVER_set_field(&str[i], "field1", 1);
15+
}
16+
17+
// Populate with pointers into string constant
18+
char *pointers[10];
19+
for(int i = 0; i < 7; ++i)
20+
{
21+
pointers[i] = &str[i];
22+
}
23+
24+
// Check that we can read the string constant's shadow memory
25+
// through the pointers.
26+
assert(__CPROVER_get_field(pointers[0], "field1") == 0);
27+
assert(__CPROVER_get_field(pointers[1], "field1") == 1);
28+
assert(__CPROVER_get_field(pointers[2], "field1") == 1);
29+
assert(__CPROVER_get_field(pointers[3], "field1") == 1);
30+
assert(__CPROVER_get_field(pointers[4], "field1") == 1);
31+
assert(__CPROVER_get_field(pointers[5], "field1") == 1);
32+
assert(__CPROVER_get_field(pointers[6], "field1") == 0);
33+
assert(__CPROVER_get_field(pointers[7], "field1") == 0);
34+
assert(__CPROVER_get_field(pointers[8], "field1") == 0);
35+
assert(__CPROVER_get_field(pointers[9], "field1") == 0);
36+
}

‎regression/cbmc-shadow-memory/constchar-pointers1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
main.c
3+
--unwind 11
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-shadow-memory/custom-init1/main.c

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
struct STRUCTNAME
5+
{
6+
int x1;
7+
int B1[3];
8+
};
9+
10+
// Test initialization of various data types with custom values
11+
int main()
12+
{
13+
__CPROVER_field_decl_local("field1", (_Bool)1);
14+
__CPROVER_field_decl_local("field2", (unsigned __CPROVER_bitvector[6])33);
15+
__CPROVER_field_decl_global("field1", (_Bool)1);
16+
__CPROVER_field_decl_global("field2", (unsigned __CPROVER_bitvector[6])33);
17+
18+
int y;
19+
assert(__CPROVER_get_field(&y, "field1") == 1);
20+
assert(__CPROVER_get_field(((char *)&y) + 1, "field1") == 1);
21+
assert(__CPROVER_get_field(((char *)&y) + 2, "field1") == 1);
22+
assert(__CPROVER_get_field(((char *)&y) + 3, "field1") == 1);
23+
assert(__CPROVER_get_field(&y, "field1") == 1);
24+
assert(__CPROVER_get_field(&y, "field2") == 33);
25+
assert(__CPROVER_get_field(((char *)&y) + 1, "field2") == 33);
26+
assert(__CPROVER_get_field(((char *)&y) + 2, "field2") == 33);
27+
assert(__CPROVER_get_field(((char *)&y) + 3, "field2") == 33);
28+
29+
int A[5];
30+
assert(__CPROVER_get_field(&A[2], "field1") == 1);
31+
assert(__CPROVER_get_field(((char *)&A[2]) + 1, "field1") == 1);
32+
assert(__CPROVER_get_field(((char *)&A[2]) + 2, "field1") == 1);
33+
assert(__CPROVER_get_field(((char *)&A[2]) + 3, "field1") == 1);
34+
assert(__CPROVER_get_field(&A[2], "field1") == 1);
35+
assert(__CPROVER_get_field(&A[2], "field2") == 33);
36+
assert(__CPROVER_get_field(((char *)&A[2]) + 1, "field2") == 33);
37+
assert(__CPROVER_get_field(((char *)&A[2]) + 2, "field2") == 33);
38+
assert(__CPROVER_get_field(((char *)&A[2]) + 3, "field2") == 33);
39+
40+
struct STRUCTNAME m;
41+
assert(__CPROVER_get_field(&m.B1[1], "field1") == 1);
42+
assert(__CPROVER_get_field(((char *)&m.B1[1]) + 1, "field1") == 1);
43+
assert(__CPROVER_get_field(((char *)&m.B1[1]) + 2, "field1") == 1);
44+
assert(__CPROVER_get_field(((char *)&m.B1[1]) + 3, "field1") == 1);
45+
assert(__CPROVER_get_field(&m.B1[1], "field1") == 1);
46+
assert(__CPROVER_get_field(&m.B1[1], "field2") == 33);
47+
assert(__CPROVER_get_field(((char *)&m.B1[1]) + 1, "field2") == 33);
48+
assert(__CPROVER_get_field(((char *)&m.B1[1]) + 2, "field2") == 33);
49+
assert(__CPROVER_get_field(((char *)&m.B1[1]) + 3, "field2") == 33);
50+
51+
struct STRUCTNAME n[3];
52+
assert(__CPROVER_get_field(&n[2].x1, "field1") == 1);
53+
assert(__CPROVER_get_field(((char *)&n[2].x1) + 1, "field1") == 1);
54+
assert(__CPROVER_get_field(((char *)&n[2].x1) + 2, "field1") == 1);
55+
assert(__CPROVER_get_field(((char *)&n[2].x1) + 3, "field1") == 1);
56+
assert(__CPROVER_get_field(&n[2].x1, "field1") == 1);
57+
assert(__CPROVER_get_field(&n[2].x1, "field2") == 33);
58+
assert(__CPROVER_get_field(((char *)&n[2].x1) + 1, "field2") == 33);
59+
assert(__CPROVER_get_field(((char *)&n[2].x1) + 2, "field2") == 33);
60+
assert(__CPROVER_get_field(((char *)&n[2].x1) + 3, "field2") == 33);
61+
62+
short *z = malloc(10 * sizeof(short));
63+
assert(__CPROVER_get_field(&z[7], "field1") == 1);
64+
assert(__CPROVER_get_field(((char *)&z[7]) + 1, "field1") == 1);
65+
assert(__CPROVER_get_field(&z[7], "field2") == 33);
66+
assert(__CPROVER_get_field(((char *)&z[7]) + 1, "field2") == 33);
67+
68+
struct STRUCTNAME *p = malloc(sizeof(struct STRUCTNAME));
69+
assert(__CPROVER_get_field(&p->B1[1], "field1") == 1);
70+
assert(__CPROVER_get_field(((char *)&p->B1[1]) + 1, "field1") == 1);
71+
assert(__CPROVER_get_field(((char *)&p->B1[1]) + 2, "field1") == 1);
72+
assert(__CPROVER_get_field(((char *)&p->B1[1]) + 3, "field1") == 1);
73+
assert(__CPROVER_get_field(&p->B1[1], "field1") == 1);
74+
assert(__CPROVER_get_field(&p->B1[1], "field2") == 33);
75+
assert(__CPROVER_get_field(((char *)&p->B1[1]) + 1, "field2") == 33);
76+
assert(__CPROVER_get_field(((char *)&p->B1[1]) + 2, "field2") == 33);
77+
assert(__CPROVER_get_field(((char *)&p->B1[1]) + 3, "field2") == 33);
78+
79+
struct STRUCTNAME *u = malloc(3 * sizeof(struct STRUCTNAME));
80+
assert(__CPROVER_get_field(&u[2].x1, "field1") == 1);
81+
assert(__CPROVER_get_field(((char *)&u[2].x1) + 1, "field1") == 1);
82+
assert(__CPROVER_get_field(((char *)&u[2].x1) + 2, "field1") == 1);
83+
assert(__CPROVER_get_field(((char *)&u[2].x1) + 3, "field1") == 1);
84+
assert(__CPROVER_get_field(&u[2].x1, "field1") == 1);
85+
assert(__CPROVER_get_field(&u[2].x1, "field2") == 33);
86+
assert(__CPROVER_get_field(((char *)&u[2].x1) + 1, "field2") == 33);
87+
assert(__CPROVER_get_field(((char *)&u[2].x1) + 2, "field2") == 33);
88+
assert(__CPROVER_get_field(((char *)&u[2].x1) + 3, "field2") == 33);
89+
90+
const char *w = "A string constant";
91+
assert(__CPROVER_get_field(&w[0], "field1") == 1);
92+
assert(__CPROVER_get_field(&w[5], "field1") == 1);
93+
assert(__CPROVER_get_field(&w[0], "field2") == 33);
94+
assert(__CPROVER_get_field(&w[5], "field2") == 33);
95+
}

‎regression/cbmc-shadow-memory/custom-init1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-shadow-memory/errno1/main.c

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
#include <assert.h>
2+
#include <errno.h>
3+
4+
int main()
5+
{
6+
__CPROVER_field_decl_local("field1", (_Bool)0);
7+
__CPROVER_field_decl_global("field1", (_Bool)0);
8+
9+
int *error = __errno();
10+
11+
assert(__CPROVER_get_field(error, "field1") == 0);
12+
13+
__CPROVER_set_field(error, "field1", 1);
14+
assert(__CPROVER_get_field(error, "field1") == 1);
15+
}

‎regression/cbmc-shadow-memory/errno1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-shadow-memory/float1/main.c

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
__CPROVER_field_decl_local("field1", (unsigned __CPROVER_bitvector[7])0);
6+
7+
float x;
8+
9+
// Check that shadow memory has been initialized to zero.
10+
assert(!__CPROVER_get_field(&x, "field1"));
11+
12+
// Check that shadow memory has been set to the chosen
13+
// nondeterministic value.
14+
unsigned __CPROVER_bitvector[7] v;
15+
__CPROVER_set_field(&x, "field1", v);
16+
assert(__CPROVER_get_field(&x, "field1") == v);
17+
}

‎regression/cbmc-shadow-memory/float1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
FUTURE
2+
main.c
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc-shadow-memory/getenv1/main.c

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
#include <stdlib.h>
2+
3+
void main()
4+
{
5+
__CPROVER_field_decl_global("dr_write", (_Bool)0);
6+
7+
char *env = getenv("PATH");
8+
__CPROVER_assume(env != NULL);
9+
assert(!__CPROVER_get_field(env, "dr_write"));
10+
11+
__CPROVER_set_field(env, "dr_write", 1);
12+
assert(__CPROVER_get_field(env, "dr_write"));
13+
}

0 commit comments

Comments
 (0)