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

@@ -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()

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

regression/snapshot-harness/CMakeLists.txt

@@ -0,0 +1,7 @@
+add_test_pl_tests(
+  "../chain.sh \
+   $<TARGET_FILE:goto-cc> \
+   $<TARGET_FILE:goto-harness> \
+   $<TARGET_FILE:memory-analyzer> \
+   $<TARGET_FILE:cbmc> \
+   ../../../build/bin/goto-gcc")

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

regression/snapshot-harness/arrays_01/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+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);
+}

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

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

regression/snapshot-harness/pointer_01/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int x;
+int *p;
+
+void initialize()
+{
+  x = 3;
+  p = &x;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*p == x);
+}

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

regression/snapshot-harness/pointer_02/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+#include <malloc.h>
+
+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);
+}

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

regression/snapshot-harness/pointer_03/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int x;
+void *p;
+
+void initialize()
+{
+  x = 3;
+  p = (void *)&x;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*(int *)p == 3);
+
+  return 0;
+}

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

regression/snapshot-harness/pointer_04/main.c

@@ -0,0 +1,30 @@
+#include <assert.h>
+
+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;
+}

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

regression/snapshot-harness/pointer_05/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int x;
+int *p1;
+int *p2;
+
+void initialize()
+{
+  x = 3;
+  p1 = &x;
+  p2 = &x;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(*p1 == *p2);
+}

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

regression/snapshot-harness/pointer_06/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+#include <malloc.h>
+
+int *p;
+int *q;
+
+void initialize()
+{
+  p = malloc(sizeof(int));
+  q = p;
+}
+
+void checkpoint()
+{
+}
+
+int main()
+{
+  initialize();
+  checkpoint();
+
+  assert(p == q);
+}

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

regression/snapshot-harness/pointer_to_struct_01/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <malloc.h>
+
+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);
+}

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

regression/snapshot-harness/structs_01/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+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);
+}

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

regression/snapshot-harness/union_01/main.c

@@ -0,0 +1,31 @@
+#include <assert.h>
+
+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);
+}

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