Skip to content

Commit d9a5113

Browse files
tautschnigtautschnig
authored
Merge pull request #4438 from xbauch/feature/snapshot-pointers
Memory snapshot support for pointers and structs [blocks: #4482]
2 parents 8f4ca1d + e961c89 commit d9a5113

File tree

31 files changed

+678
-15
lines changed

31 files changed

+678
-15
lines changed

Diff for: ‎regression/CMakeLists.txt

+2-1
Original file line numberDiff line numberDiff line change
@@ -55,5 +55,6 @@ add_subdirectory(linking-goto-binaries)
5555
add_subdirectory(symtab2gb)
5656

5757
if(WITH_MEMORY_ANALYZER)
58-
add_subdirectory(memory-analyzer)
58+
add_subdirectory(snapshot-harness)
59+
add_subdirectory(memory-analyzer)
5960
endif()

Diff for: ‎regression/Makefile

+2-1
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,8 @@ ifeq ($(detected_OS),Linux)
4444
endif
4545

4646
ifeq ($(WITH_MEMORY_ANALYZER),1)
47-
DIRS += memory-analyzer
47+
DIRS += snapshot-harness \
48+
memory-analyzer
4849
endif
4950

5051
# Run all test directories in sequence

Diff for: ‎regression/memory-analyzer/pointer_to_struct_01/test.desc

+2-3
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,7 @@ CORE
22
main.gb
33
--breakpoint checkpoint --symbols p
44
struct S tmp;
5-
tmp = \{ \.next=\(\(struct S \*\)(NULL|0)\) \};
6-
p = &tmp;
7-
p->next = &tmp;
5+
tmp = \{ \.next=\(\(struct S \*\)0\) \};
6+
p = \&tmp;
87
^EXIT=0$
98
^SIGNAL=0$

Diff for: ‎regression/snapshot-harness/CMakeLists.txt

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
add_test_pl_tests(
2+
"../chain.sh \
3+
$<TARGET_FILE:goto-cc> \
4+
$<TARGET_FILE:goto-harness> \
5+
$<TARGET_FILE:memory-analyzer> \
6+
$<TARGET_FILE:cbmc> \
7+
../../../build/bin/goto-gcc")

Diff for: ‎regression/snapshot-harness/Makefile

+26
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
default: tests.log
2+
3+
MEMORY_ANALYZER_EXE=../../../src/memory-analyzer/memory-analyzer
4+
GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness
5+
CBMC_EXE=../../../src/cbmc/cbmc
6+
GOTO_CC_EXE=../../../src/goto-cc/goto-cc
7+
GOTO_GCC_EXE=../../../src/goto-cc/goto-gcc
8+
9+
test:
10+
@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(MEMORY_ANALYZER_EXE) $(CBMC_EXE) $(GOTO_GCC_EXE)"
11+
12+
tests.log: ../test.pl
13+
@../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(MEMORY_ANALYZER_EXE) $(CBMC_EXE) $(GOTO_GCC_EXE)"
14+
15+
show:
16+
@for dir in *; do \
17+
if [ -d "$$dir" ]; then \
18+
vim -o "$$dir/*.c" "$$dir/*.out"; \
19+
fi; \
20+
done;
21+
22+
clean:
23+
find -name '*.out' -execdir $(RM) '{}' \;
24+
find -name '*.gb' -execdir $(RM) '{}' \;
25+
find -name '*.json' -execdir $(RM) '{}' \;
26+
$(RM) tests.log

Diff for: ‎regression/snapshot-harness/arrays_01/main.c

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
#include <assert.h>
2+
3+
int array[] = {1, 2, 3};
4+
int *p;
5+
int *q;
6+
7+
void initialize()
8+
{
9+
p = &(array[1]);
10+
q = array + 1;
11+
array[0] = 4;
12+
}
13+
14+
void checkpoint()
15+
{
16+
}
17+
18+
int main()
19+
{
20+
initialize();
21+
checkpoint();
22+
23+
assert(p == &(array[1]));
24+
assert(p == q);
25+
assert(*p == *q);
26+
assert(array[0] != *p);
27+
*p = 4;
28+
assert(array[0] == *p);
29+
}

Diff for: ‎regression/snapshot-harness/arrays_01/test.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion p == \&\(array\[1\]\): SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion p == q: SUCCESS
8+
\[main.assertion.3\] line [0-9]+ assertion \*p == \*q: SUCCESS
9+
\[main.assertion.4\] line [0-9]+ assertion array\[0\] != \*p: SUCCESS
10+
\[main.assertion.5\] line [0-9]+ assertion array\[0\] == \*p: SUCCESS
11+
VERIFICATION SUCCESSFUL
12+
--
13+
^warning: ignoring

Diff for: ‎regression/snapshot-harness/chain.sh

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
goto_cc=$1
6+
goto_harness=$2
7+
memory_analyzer=$3
8+
cbmc=$4
9+
goto_gcc=$5
10+
entry_point='generated_entry_function'
11+
break_point='checkpoint'
12+
13+
name=${*:$#}
14+
name=${name%.c}
15+
memory_analyzer_symbols=$6
16+
goto_harness_args=${*:7:$#-7}
17+
18+
$goto_cc -o "${name}_cc.gb" "${name}.c"
19+
$goto_gcc -g -std=c11 -o "${name}_gcc.gb" "${name}.c"
20+
21+
$memory_analyzer --symtab-snapshot --json-ui --breakpoint $break_point --symbols ${memory_analyzer_symbols} "${name}_gcc.gb" > "${name}.json"
22+
23+
if [ -e "${name}-mod.gb" ] ; then
24+
rm -f "${name}-mod.gb"
25+
fi
26+
27+
$goto_harness "${name}_cc.gb" "${name}-mod.gb" --harness-function-name $entry_point --memory-snapshot "${name}.json" ${goto_harness_args}
28+
$cbmc --function $entry_point "${name}-mod.gb" \
29+
--pointer-check `# because we want to see out of bounds errors` \
30+
--unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
31+
--unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
32+
# cbmc args end

Diff for: ‎regression/snapshot-harness/pointer_01/main.c

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#include <assert.h>
2+
3+
int x;
4+
int *p;
5+
6+
void initialize()
7+
{
8+
x = 3;
9+
p = &x;
10+
}
11+
12+
void checkpoint()
13+
{
14+
}
15+
16+
int main()
17+
{
18+
initialize();
19+
checkpoint();
20+
21+
assert(*p == x);
22+
}

Diff for: ‎regression/snapshot-harness/pointer_01/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion \*p == x: SUCCESS
7+
VERIFICATION SUCCESSFUL
8+
--
9+
^warning: ignoring

Diff for: ‎regression/snapshot-harness/pointer_02/main.c

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
#include <assert.h>
2+
#include <malloc.h>
3+
4+
int x;
5+
int *p1;
6+
int *p2;
7+
int *p3;
8+
9+
void initialize()
10+
{
11+
x = 3;
12+
p1 = malloc(sizeof(int));
13+
p3 = malloc(sizeof(int));
14+
p2 = &x;
15+
}
16+
17+
void checkpoint()
18+
{
19+
}
20+
21+
int main()
22+
{
23+
initialize();
24+
checkpoint();
25+
26+
assert(*p2 == x);
27+
assert(p1 != p2);
28+
assert(p1 != p3);
29+
assert(*p1 == x);
30+
*p1 = x;
31+
assert(*p1 == x);
32+
}

Diff for: ‎regression/snapshot-harness/pointer_02/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion \*p2 == x: SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion p1 != p2: SUCCESS
8+
\[main.assertion.3\] line [0-9]+ assertion p1 != p3: SUCCESS
9+
\[main.assertion.4\] line [0-9]+ assertion \*p1 == x: FAILURE
10+
\[main.assertion.5\] line [0-9]+ assertion \*p1 == x: SUCCESS
11+
--
12+
^warning: ignoring

Diff for: ‎regression/snapshot-harness/pointer_03/main.c

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <assert.h>
2+
3+
int x;
4+
void *p;
5+
6+
void initialize()
7+
{
8+
x = 3;
9+
p = (void *)&x;
10+
}
11+
12+
void checkpoint()
13+
{
14+
}
15+
16+
int main()
17+
{
18+
initialize();
19+
checkpoint();
20+
21+
assert(*(int *)p == 3);
22+
23+
return 0;
24+
}

Diff for: ‎regression/snapshot-harness/pointer_03/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion \*\(int \*\)p == 3: SUCCESS
7+
--
8+
^warning: ignoring

Diff for: ‎regression/snapshot-harness/pointer_04/main.c

+30
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <assert.h>
2+
3+
int x;
4+
int *p1;
5+
int **p2;
6+
7+
void initialize()
8+
{
9+
x = 3;
10+
p1 = &x;
11+
p2 = &p1;
12+
}
13+
14+
void checkpoint()
15+
{
16+
}
17+
18+
int main()
19+
{
20+
initialize();
21+
checkpoint();
22+
23+
assert(&p1 == *p2);
24+
assert(*p2 == p1);
25+
assert(*p1 == 3);
26+
assert(*p2 == &x);
27+
assert(**p2 == x);
28+
29+
return 0;
30+
}

Diff for: ‎regression/snapshot-harness/pointer_04/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion \&p1 == \*p2: SUCCESS
7+
\[main.assertion.2\] line [0-9]+ assertion \*p2 == p1: SUCCESS
8+
\[main.assertion.3\] line [0-9]+ assertion \*p1 == 3: SUCCESS
9+
\[main.assertion.4\] line [0-9]+ assertion \*p2 == \&x: SUCCESS
10+
\[main.assertion.5\] line [0-9]+ assertion \*\*p2 == x: SUCCESS
11+
--
12+
^warning: ignoring

Diff for: ‎regression/snapshot-harness/pointer_05/main.c

+24
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
#include <assert.h>
2+
3+
int x;
4+
int *p1;
5+
int *p2;
6+
7+
void initialize()
8+
{
9+
x = 3;
10+
p1 = &x;
11+
p2 = &x;
12+
}
13+
14+
void checkpoint()
15+
{
16+
}
17+
18+
int main()
19+
{
20+
initialize();
21+
checkpoint();
22+
23+
assert(*p1 == *p2);
24+
}

Diff for: ‎regression/snapshot-harness/pointer_05/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion \*p1 == \*p2: SUCCESS
7+
VERIFICATION SUCCESSFUL
8+
--
9+
^warning: ignoring

Diff for: ‎regression/snapshot-harness/pointer_06/main.c

+23
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <assert.h>
2+
#include <malloc.h>
3+
4+
int *p;
5+
int *q;
6+
7+
void initialize()
8+
{
9+
p = malloc(sizeof(int));
10+
q = p;
11+
}
12+
13+
void checkpoint()
14+
{
15+
}
16+
17+
int main()
18+
{
19+
initialize();
20+
checkpoint();
21+
22+
assert(p == q);
23+
}

Diff for: ‎regression/snapshot-harness/pointer_06/test.desc

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
\[main.assertion.1\] line [0-9]+ assertion p == q: SUCCESS
7+
VERIFICATION SUCCESSFUL
8+
--
9+
^warning: ignoring

0 commit comments

Comments
 (0)