Memory snapshot support for pointers and structs [blocks: #4482]

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/memory-analyzer/pointer_to_struct_01/test.desc

@@ -2,8 +2,7 @@ CORE
 main.gb
 --breakpoint checkpoint --symbols p
 struct S tmp;
-tmp = \{ \.next=\(\(struct S \*\)(NULL|0)\) \};
-p = &tmp;
-p->next = &tmp;
+tmp = \{ \.next=\(\(struct S \*\)0\) \};
+p = \&tmp;
 ^EXIT=0$
 ^SIGNAL=0$

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