From e961c89b9f14fbc0acd1c61948615031c2017e87 Mon Sep 17 00:00:00 2001 From: Petr Bauch Date: Thu, 16 May 2019 15:41:53 +0100 Subject: [PATCH] Add regression tests for snapshot-harness These call memory-analyzer to produce the JSON snapshots and then build the harness similarly to how goto-harness tests work. We currently tests structs, unions, arrays and pointers to all of those. --- regression/CMakeLists.txt | 3 +- regression/Makefile | 3 +- regression/snapshot-harness/CMakeLists.txt | 7 ++++ regression/snapshot-harness/Makefile | 26 ++++++++++++++ regression/snapshot-harness/arrays_01/main.c | 29 ++++++++++++++++ .../snapshot-harness/arrays_01/test.desc | 13 +++++++ regression/snapshot-harness/chain.sh | 32 +++++++++++++++++ regression/snapshot-harness/pointer_01/main.c | 22 ++++++++++++ .../snapshot-harness/pointer_01/test.desc | 9 +++++ regression/snapshot-harness/pointer_02/main.c | 32 +++++++++++++++++ .../snapshot-harness/pointer_02/test.desc | 12 +++++++ regression/snapshot-harness/pointer_03/main.c | 24 +++++++++++++ .../snapshot-harness/pointer_03/test.desc | 8 +++++ regression/snapshot-harness/pointer_04/main.c | 30 ++++++++++++++++ .../snapshot-harness/pointer_04/test.desc | 12 +++++++ regression/snapshot-harness/pointer_05/main.c | 24 +++++++++++++ .../snapshot-harness/pointer_05/test.desc | 9 +++++ regression/snapshot-harness/pointer_06/main.c | 23 +++++++++++++ .../snapshot-harness/pointer_06/test.desc | 9 +++++ .../pointer_to_struct_01/main.c | 34 +++++++++++++++++++ .../pointer_to_struct_01/test.desc | 12 +++++++ regression/snapshot-harness/structs_01/main.c | 32 +++++++++++++++++ .../snapshot-harness/structs_01/test.desc | 12 +++++++ regression/snapshot-harness/union_01/main.c | 31 +++++++++++++++++ .../snapshot-harness/union_01/test.desc | 11 ++++++ 25 files changed, 457 insertions(+), 2 deletions(-) create mode 100644 regression/snapshot-harness/CMakeLists.txt create mode 100644 regression/snapshot-harness/Makefile create mode 100644 regression/snapshot-harness/arrays_01/main.c create mode 100644 regression/snapshot-harness/arrays_01/test.desc create mode 100755 regression/snapshot-harness/chain.sh create mode 100644 regression/snapshot-harness/pointer_01/main.c create mode 100644 regression/snapshot-harness/pointer_01/test.desc create mode 100644 regression/snapshot-harness/pointer_02/main.c create mode 100644 regression/snapshot-harness/pointer_02/test.desc create mode 100644 regression/snapshot-harness/pointer_03/main.c create mode 100644 regression/snapshot-harness/pointer_03/test.desc create mode 100644 regression/snapshot-harness/pointer_04/main.c create mode 100644 regression/snapshot-harness/pointer_04/test.desc create mode 100644 regression/snapshot-harness/pointer_05/main.c create mode 100644 regression/snapshot-harness/pointer_05/test.desc create mode 100644 regression/snapshot-harness/pointer_06/main.c create mode 100644 regression/snapshot-harness/pointer_06/test.desc create mode 100644 regression/snapshot-harness/pointer_to_struct_01/main.c create mode 100644 regression/snapshot-harness/pointer_to_struct_01/test.desc create mode 100644 regression/snapshot-harness/structs_01/main.c create mode 100644 regression/snapshot-harness/structs_01/test.desc create mode 100644 regression/snapshot-harness/union_01/main.c create mode 100644 regression/snapshot-harness/union_01/test.desc diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index fd75d83a4d..b47c8e5d6b 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -55,5 +55,6 @@ add_subdirectory(linking-goto-binaries) add_subdirectory(symtab2gb) if(WITH_MEMORY_ANALYZER) -add_subdirectory(memory-analyzer) + add_subdirectory(snapshot-harness) + add_subdirectory(memory-analyzer) endif() diff --git a/regression/Makefile b/regression/Makefile index 2624eb9942..3742ce83e4 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -44,7 +44,8 @@ ifeq ($(detected_OS),Linux) endif ifeq ($(WITH_MEMORY_ANALYZER),1) - DIRS += memory-analyzer + DIRS += snapshot-harness \ + memory-analyzer endif # Run all test directories in sequence diff --git a/regression/snapshot-harness/CMakeLists.txt b/regression/snapshot-harness/CMakeLists.txt new file mode 100644 index 0000000000..e4247acf55 --- /dev/null +++ b/regression/snapshot-harness/CMakeLists.txt @@ -0,0 +1,7 @@ +add_test_pl_tests( + "../chain.sh \ + $ \ + $ \ + $ \ + $ \ + ../../../build/bin/goto-gcc") diff --git a/regression/snapshot-harness/Makefile b/regression/snapshot-harness/Makefile new file mode 100644 index 0000000000..8bb6a0c5c5 --- /dev/null +++ b/regression/snapshot-harness/Makefile @@ -0,0 +1,26 @@ +default: tests.log + +MEMORY_ANALYZER_EXE=../../../src/memory-analyzer/memory-analyzer +GOTO_HARNESS_EXE=../../../src/goto-harness/goto-harness +CBMC_EXE=../../../src/cbmc/cbmc +GOTO_CC_EXE=../../../src/goto-cc/goto-cc +GOTO_GCC_EXE=../../../src/goto-cc/goto-gcc + +test: + @../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(MEMORY_ANALYZER_EXE) $(CBMC_EXE) $(GOTO_GCC_EXE)" + +tests.log: ../test.pl + @../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_HARNESS_EXE) $(MEMORY_ANALYZER_EXE) $(CBMC_EXE) $(GOTO_GCC_EXE)" + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + find -name '*.json' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/snapshot-harness/arrays_01/main.c b/regression/snapshot-harness/arrays_01/main.c new file mode 100644 index 0000000000..60700a22f3 --- /dev/null +++ b/regression/snapshot-harness/arrays_01/main.c @@ -0,0 +1,29 @@ +#include + +int array[] = {1, 2, 3}; +int *p; +int *q; + +void initialize() +{ + p = &(array[1]); + q = array + 1; + array[0] = 4; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p == &(array[1])); + assert(p == q); + assert(*p == *q); + assert(array[0] != *p); + *p = 4; + assert(array[0] == *p); +} diff --git a/regression/snapshot-harness/arrays_01/test.desc b/regression/snapshot-harness/arrays_01/test.desc new file mode 100644 index 0000000000..e89b75dbb1 --- /dev/null +++ b/regression/snapshot-harness/arrays_01/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +array,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion p == \&\(array\[1\]\): SUCCESS +\[main.assertion.2\] line [0-9]+ assertion p == q: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \*p == \*q: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion array\[0\] != \*p: SUCCESS +\[main.assertion.5\] line [0-9]+ assertion array\[0\] == \*p: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/chain.sh b/regression/snapshot-harness/chain.sh new file mode 100755 index 0000000000..b5b5d6957e --- /dev/null +++ b/regression/snapshot-harness/chain.sh @@ -0,0 +1,32 @@ +#!/bin/bash + +set -e + +goto_cc=$1 +goto_harness=$2 +memory_analyzer=$3 +cbmc=$4 +goto_gcc=$5 +entry_point='generated_entry_function' +break_point='checkpoint' + +name=${*:$#} +name=${name%.c} +memory_analyzer_symbols=$6 +goto_harness_args=${*:7:$#-7} + +$goto_cc -o "${name}_cc.gb" "${name}.c" +$goto_gcc -g -std=c11 -o "${name}_gcc.gb" "${name}.c" + +$memory_analyzer --symtab-snapshot --json-ui --breakpoint $break_point --symbols ${memory_analyzer_symbols} "${name}_gcc.gb" > "${name}.json" + +if [ -e "${name}-mod.gb" ] ; then + rm -f "${name}-mod.gb" +fi + +$goto_harness "${name}_cc.gb" "${name}-mod.gb" --harness-function-name $entry_point --memory-snapshot "${name}.json" ${goto_harness_args} +$cbmc --function $entry_point "${name}-mod.gb" \ + --pointer-check `# because we want to see out of bounds errors` \ + --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \ + --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \ + # cbmc args end diff --git a/regression/snapshot-harness/pointer_01/main.c b/regression/snapshot-harness/pointer_01/main.c new file mode 100644 index 0000000000..3c04349bbf --- /dev/null +++ b/regression/snapshot-harness/pointer_01/main.c @@ -0,0 +1,22 @@ +#include + +int x; +int *p; + +void initialize() +{ + x = 3; + p = &x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*p == x); +} diff --git a/regression/snapshot-harness/pointer_01/test.desc b/regression/snapshot-harness/pointer_01/test.desc new file mode 100644 index 0000000000..4e6490db71 --- /dev/null +++ b/regression/snapshot-harness/pointer_01/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*p == x: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_02/main.c b/regression/snapshot-harness/pointer_02/main.c new file mode 100644 index 0000000000..13502cae8f --- /dev/null +++ b/regression/snapshot-harness/pointer_02/main.c @@ -0,0 +1,32 @@ +#include +#include + +int x; +int *p1; +int *p2; +int *p3; + +void initialize() +{ + x = 3; + p1 = malloc(sizeof(int)); + p3 = malloc(sizeof(int)); + p2 = &x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*p2 == x); + assert(p1 != p2); + assert(p1 != p3); + assert(*p1 == x); + *p1 = x; + assert(*p1 == x); +} diff --git a/regression/snapshot-harness/pointer_02/test.desc b/regression/snapshot-harness/pointer_02/test.desc new file mode 100644 index 0000000000..5e6f5fdf76 --- /dev/null +++ b/regression/snapshot-harness/pointer_02/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +x,p1,p2,p3 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=10$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*p2 == x: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion p1 != p2: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion p1 != p3: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion \*p1 == x: FAILURE +\[main.assertion.5\] line [0-9]+ assertion \*p1 == x: SUCCESS +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_03/main.c b/regression/snapshot-harness/pointer_03/main.c new file mode 100644 index 0000000000..44c9edf6aa --- /dev/null +++ b/regression/snapshot-harness/pointer_03/main.c @@ -0,0 +1,24 @@ +#include + +int x; +void *p; + +void initialize() +{ + x = 3; + p = (void *)&x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*(int *)p == 3); + + return 0; +} diff --git a/regression/snapshot-harness/pointer_03/test.desc b/regression/snapshot-harness/pointer_03/test.desc new file mode 100644 index 0000000000..1f29edb3df --- /dev/null +++ b/regression/snapshot-harness/pointer_03/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +x,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*\(int \*\)p == 3: SUCCESS +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_04/main.c b/regression/snapshot-harness/pointer_04/main.c new file mode 100644 index 0000000000..29950c318a --- /dev/null +++ b/regression/snapshot-harness/pointer_04/main.c @@ -0,0 +1,30 @@ +#include + +int x; +int *p1; +int **p2; + +void initialize() +{ + x = 3; + p1 = &x; + p2 = &p1; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(&p1 == *p2); + assert(*p2 == p1); + assert(*p1 == 3); + assert(*p2 == &x); + assert(**p2 == x); + + return 0; +} diff --git a/regression/snapshot-harness/pointer_04/test.desc b/regression/snapshot-harness/pointer_04/test.desc new file mode 100644 index 0000000000..c4025bb0f9 --- /dev/null +++ b/regression/snapshot-harness/pointer_04/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \&p1 == \*p2: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \*p2 == p1: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \*p1 == 3: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion \*p2 == \&x: SUCCESS +\[main.assertion.5\] line [0-9]+ assertion \*\*p2 == x: SUCCESS +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_05/main.c b/regression/snapshot-harness/pointer_05/main.c new file mode 100644 index 0000000000..8edd9810a2 --- /dev/null +++ b/regression/snapshot-harness/pointer_05/main.c @@ -0,0 +1,24 @@ +#include + +int x; +int *p1; +int *p2; + +void initialize() +{ + x = 3; + p1 = &x; + p2 = &x; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(*p1 == *p2); +} diff --git a/regression/snapshot-harness/pointer_05/test.desc b/regression/snapshot-harness/pointer_05/test.desc new file mode 100644 index 0000000000..5fbe74f96a --- /dev/null +++ b/regression/snapshot-harness/pointer_05/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +x,p1,p2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion \*p1 == \*p2: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_06/main.c b/regression/snapshot-harness/pointer_06/main.c new file mode 100644 index 0000000000..af0e19c96f --- /dev/null +++ b/regression/snapshot-harness/pointer_06/main.c @@ -0,0 +1,23 @@ +#include +#include + +int *p; +int *q; + +void initialize() +{ + p = malloc(sizeof(int)); + q = p; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p == q); +} diff --git a/regression/snapshot-harness/pointer_06/test.desc b/regression/snapshot-harness/pointer_06/test.desc new file mode 100644 index 0000000000..70452f9ad8 --- /dev/null +++ b/regression/snapshot-harness/pointer_06/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion p == q: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/pointer_to_struct_01/main.c b/regression/snapshot-harness/pointer_to_struct_01/main.c new file mode 100644 index 0000000000..8238f850be --- /dev/null +++ b/regression/snapshot-harness/pointer_to_struct_01/main.c @@ -0,0 +1,34 @@ +#include +#include + +struct S +{ + struct S *next; +}; + +struct S st; +struct S *p; +struct S *q; + +void initialize() +{ + st.next = &st; + p = &st; + q = malloc(sizeof(struct S)); +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(p == &st); + assert(p->next == &st); + assert(p != q); + q->next = &st; + assert(p == q->next); +} diff --git a/regression/snapshot-harness/pointer_to_struct_01/test.desc b/regression/snapshot-harness/pointer_to_struct_01/test.desc new file mode 100644 index 0000000000..7574b74154 --- /dev/null +++ b/regression/snapshot-harness/pointer_to_struct_01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +st,p,q --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion p == \&st: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion p-\>next == \&st: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion p \!= q: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion p == q-\>next: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/structs_01/main.c b/regression/snapshot-harness/structs_01/main.c new file mode 100644 index 0000000000..462006577d --- /dev/null +++ b/regression/snapshot-harness/structs_01/main.c @@ -0,0 +1,32 @@ +#include + +struct S +{ + int c1; + int c2; +} st; + +int *p; + +void initialize() +{ + st.c1 = 1; + st.c2 = 3; + p = &(st.c2); +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(st.c1 + 2 == st.c2); + assert(st.c1 + 2 == *p); + assert(*p == st.c2); + *p = st.c2 + 1; + assert(*p == st.c2); +} diff --git a/regression/snapshot-harness/structs_01/test.desc b/regression/snapshot-harness/structs_01/test.desc new file mode 100644 index 0000000000..887f6a4448 --- /dev/null +++ b/regression/snapshot-harness/structs_01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +st,p --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion st.c1 \+ 2 == st.c2: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion st.c1 \+ 2 == \*p: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \*p == st.c2: SUCCESS +\[main.assertion.4\] line [0-9]+ assertion \*p == st.c2: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/union_01/main.c b/regression/snapshot-harness/union_01/main.c new file mode 100644 index 0000000000..127ea571b3 --- /dev/null +++ b/regression/snapshot-harness/union_01/main.c @@ -0,0 +1,31 @@ +#include + +union Un { + int i; + float f; +} un; + +int *ip; +float *fp; + +void initialize() +{ + un.i = 1; + ip = &un.i; + fp = &un.f; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(ip == &un.i); + assert(*ip == un.i); + *fp = 2.0f; + assert(un.f == 2.0f); +} diff --git a/regression/snapshot-harness/union_01/test.desc b/regression/snapshot-harness/union_01/test.desc new file mode 100644 index 0000000000..beefc7d3d7 --- /dev/null +++ b/regression/snapshot-harness/union_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +un,ip,fp --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion ip == \&un.i: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \*ip == un.i: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion un.f == 2.0f: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring