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.

Author: petr-bauch

regression/CMakeLists.txt

@@ -53,5 +53,6 @@ add_subdirectory(goto-harness)
 add_subdirectory(goto-cc-file-local)
 
 if(WITH_MEMORY_ANALYZER)
-add_subdirectory(memory-analyzer)
+  add_subdirectory(snapshot-harness)
+  add_subdirectory(memory-analyzer)
 endif()

regression/Makefile

@@ -24,17 +24,20 @@ DIRS = cbmc \
        cbmc-cpp \
        goto-cc-goto-analyzer \
        systemc \
-       contracts \
-       memory-analyzer
+       contracts
        # Empty last line
 
+ifeq ($(WITH_MEMORY_ANALYZER),1)
+  DIRS += snapshot-harness \
+          memory-analyzer
+          # Empty last line
+endif
+
 # Run all test directories in sequence
 .PHONY: test
 test:
 	@for dir in $(DIRS); do \
-	  if [ "$$dir" != memory-analyzer -o "$WITH_MEMORY_ANALYZER" = 1 ]; then \
 		$(MAKE) "$$dir" || exit 1; \
-	  fi \
 	done;
 
 # Pattern to execute a single test suite directory

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);
+}