Tests for future shadow memory feature

regression/CMakeLists.txt

@@ -38,6 +38,7 @@ add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
 add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
+add_subdirectory(cbmc-shadow-memory)
 add_subdirectory(cbmc-output-file)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)

regression/Makefile

@@ -1,7 +1,8 @@
 # For the best possible utilisation of multiple cores when
 # running tests in parallel, it is important that these directories are
 # listed with decreasing runtimes (i.e. longest running at the top)
-DIRS = cbmc \
+DIRS = cbmc-shadow-memory \
+       cbmc \
        cbmc-library \
        cprover \
        crangler \

regression/cbmc-shadow-memory/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc>"
+)

regression/cbmc-shadow-memory/Makefile

@@ -0,0 +1,22 @@
+default: tests.log
+
+test:
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+
+test-cprover-smt2:
+	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
+
+tests.log: ../test.pl
+	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+
+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 '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests.log

regression/cbmc-shadow-memory/char1/main.c

@@ -0,0 +1,59 @@
+#include <assert.h>
+
+// Add some string constants to confuse the value sets.
+const char *x1 = "This is a short string constant";
+const char *x2 = "This is a loooooooooooooonger string constant";
+const char *x3 = "And yet another string constant";
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  // Add some string constants to confuse the value sets.
+  const char *y1 = "Yes, this is a short string constant";
+  const char *y2 = "Yes, this is a loooooooooooooonger string constant";
+  const char *y3 = "Yes, and yet another string constant";
+
+  char *a;
+  assert(__CPROVER_get_field(a, "field1") == 0);
+  assert(__CPROVER_get_field(&a, "field1") == 0);
+  // Cannot set because a doesn't point anywhere.
+  __CPROVER_set_field(a, "field1", 1);
+  // Hence, the value is still 0.
+  assert(__CPROVER_get_field(a, "field1") == 0);
+  assert(__CPROVER_get_field(&a, "field1") == 0);
+
+  __CPROVER_set_field(a, "field1", 0);
+  __CPROVER_set_field(&a, "field1", 1);
+  assert(__CPROVER_get_field(a, "field1") == 0);
+  assert(__CPROVER_get_field(&a, "field1") == 1);
+
+  char *b = (char *)0;
+  assert(__CPROVER_get_field(b, "field1") == 0);
+  assert(__CPROVER_get_field(&b, "field1") == 0);
+  // Cannot set because b points to NULL.
+  __CPROVER_set_field(b, "field1", 1);
+  // Hence, the value is still 0.
+  assert(__CPROVER_get_field(b, "field1") == 0);
+  assert(__CPROVER_get_field(&b, "field1") == 0);
+
+  __CPROVER_set_field(b, "field1", 0);
+  __CPROVER_set_field(&b, "field1", 1);
+  assert(__CPROVER_get_field(b, "field1") == 0);
+  assert(__CPROVER_get_field(&b, "field1") == 1);
+
+  static char *c;
+  assert(__CPROVER_get_field(c, "field1") == 0);
+  assert(__CPROVER_get_field(&c, "field1") == 0);
+  // Cannot set because c doesn't point anywhere.
+  __CPROVER_set_field(c, "field1", 1);
+  // Hence, the value is still 0.
+  assert(__CPROVER_get_field(c, "field1") == 0);
+  assert(__CPROVER_get_field(&c, "field1") == 0);
+
+  __CPROVER_set_field(c, "field1", 0);
+  __CPROVER_set_field(&c, "field1", 1);
+  assert(__CPROVER_get_field(c, "field1") == 0);
+  assert(__CPROVER_get_field(&c, "field1") == 1);
+}

regression/cbmc-shadow-memory/char1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-shadow-memory/constchar-param1/main.c

@@ -0,0 +1,53 @@
+#include <assert.h>
+
+void test(const char *str)
+{
+  // Set shadow memory for some characters
+  for(int i = 1; i < 6; ++i)
+  {
+    __CPROVER_set_field(&str[i], "field1", 1);
+  }
+
+  // Copy string constant into buffer
+  char buffer[10];
+  for(int i = 0; i < 7; ++i)
+  {
+    buffer[i] = str[i];
+    __CPROVER_set_field(
+      &buffer[i], "field1", __CPROVER_get_field(&str[i], "field1"));
+  }
+
+  // Check that shadow memory has not been copied
+  for(int i = 0; i < 7; ++i)
+  {
+    assert(__CPROVER_get_field(&buffer[0], "field1") == 0);
+  }
+
+  // Copy shadow memory
+  for(int i = 0; i < 7; ++i)
+  {
+    __CPROVER_set_field(
+      &buffer[i], "field1", __CPROVER_get_field(&str[i], "field1"));
+  }
+
+  // Check that shadow memory has been copied
+  assert(__CPROVER_get_field(&buffer[0], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[1], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[2], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[3], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[4], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[5], "field1") == 1);
+  assert(__CPROVER_get_field(&buffer[6], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[7], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[8], "field1") == 0);
+  assert(__CPROVER_get_field(&buffer[9], "field1") == 0);
+}
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  // Needed because the string constant is in the global pool.
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  test("!Hello!");
+}

regression/cbmc-shadow-memory/constchar-param1/test.desc

@@ -0,0 +1,9 @@
+FUTURE
+main.c
+--unwind 11
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^Generated 11 VCC\(s\), 0 remaining after simplification$
+--
+^warning: ignoring

regression/cbmc-shadow-memory/constchar-pointers1/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  // Needed because the string constant is in the global pool.
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  const char *str = "!Hello!";
+
+  // Set shadow memory for some characters
+  for(int i = 1; i < 6; ++i)
+  {
+    __CPROVER_set_field(&str[i], "field1", 1);
+  }
+
+  // Populate with pointers into string constant
+  char *pointers[10];
+  for(int i = 0; i < 7; ++i)
+  {
+    pointers[i] = &str[i];
+  }
+
+  // Check that we can read the string constant's shadow memory
+  // through the pointers.
+  assert(__CPROVER_get_field(pointers[0], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[1], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[2], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[3], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[4], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[5], "field1") == 1);
+  assert(__CPROVER_get_field(pointers[6], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[7], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[8], "field1") == 0);
+  assert(__CPROVER_get_field(pointers[9], "field1") == 0);
+}

regression/cbmc-shadow-memory/constchar-pointers1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+--unwind 11
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-shadow-memory/custom-init1/main.c

@@ -0,0 +1,95 @@
+#include <assert.h>
+#include <stdlib.h>
+
+struct STRUCTNAME
+{
+  int x1;
+  int B1[3];
+};
+
+// Test initialization of various data types with custom values
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)1);
+  __CPROVER_field_decl_local("field2", (unsigned __CPROVER_bitvector[6])33);
+  __CPROVER_field_decl_global("field1", (_Bool)1);
+  __CPROVER_field_decl_global("field2", (unsigned __CPROVER_bitvector[6])33);
+
+  int y;
+  assert(__CPROVER_get_field(&y, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&y) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&y) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&y) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&y, "field1") == 1);
+  assert(__CPROVER_get_field(&y, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&y) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&y) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&y) + 3, "field2") == 33);
+
+  int A[5];
+  assert(__CPROVER_get_field(&A[2], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&A[2], "field1") == 1);
+  assert(__CPROVER_get_field(&A[2], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&A[2]) + 3, "field2") == 33);
+
+  struct STRUCTNAME m;
+  assert(__CPROVER_get_field(&m.B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&m.B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(&m.B1[1], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&m.B1[1]) + 3, "field2") == 33);
+
+  struct STRUCTNAME n[3];
+  assert(__CPROVER_get_field(&n[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&n[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(&n[2].x1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&n[2].x1) + 3, "field2") == 33);
+
+  short *z = malloc(10 * sizeof(short));
+  assert(__CPROVER_get_field(&z[7], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&z[7]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(&z[7], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&z[7]) + 1, "field2") == 33);
+
+  struct STRUCTNAME *p = malloc(sizeof(struct STRUCTNAME));
+  assert(__CPROVER_get_field(&p->B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&p->B1[1], "field1") == 1);
+  assert(__CPROVER_get_field(&p->B1[1], "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&p->B1[1]) + 3, "field2") == 33);
+
+  struct STRUCTNAME *u = malloc(3 * sizeof(struct STRUCTNAME));
+  assert(__CPROVER_get_field(&u[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 1, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 2, "field1") == 1);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 3, "field1") == 1);
+  assert(__CPROVER_get_field(&u[2].x1, "field1") == 1);
+  assert(__CPROVER_get_field(&u[2].x1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 1, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 2, "field2") == 33);
+  assert(__CPROVER_get_field(((char *)&u[2].x1) + 3, "field2") == 33);
+
+  const char *w = "A string constant";
+  assert(__CPROVER_get_field(&w[0], "field1") == 1);
+  assert(__CPROVER_get_field(&w[5], "field1") == 1);
+  assert(__CPROVER_get_field(&w[0], "field2") == 33);
+  assert(__CPROVER_get_field(&w[5], "field2") == 33);
+}

regression/cbmc-shadow-memory/custom-init1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-shadow-memory/errno1/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <errno.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (_Bool)0);
+  __CPROVER_field_decl_global("field1", (_Bool)0);
+
+  int *error = __errno();
+
+  assert(__CPROVER_get_field(error, "field1") == 0);
+
+  __CPROVER_set_field(error, "field1", 1);
+  assert(__CPROVER_get_field(error, "field1") == 1);
+}

regression/cbmc-shadow-memory/errno1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-shadow-memory/float1/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main()
+{
+  __CPROVER_field_decl_local("field1", (unsigned __CPROVER_bitvector[7])0);
+
+  float x;
+
+  // Check that shadow memory has been initialized to zero.
+  assert(!__CPROVER_get_field(&x, "field1"));
+
+  // Check that shadow memory has been set to the chosen
+  // nondeterministic value.
+  unsigned __CPROVER_bitvector[7] v;
+  __CPROVER_set_field(&x, "field1", v);
+  assert(__CPROVER_get_field(&x, "field1") == v);
+}

regression/cbmc-shadow-memory/float1/test.desc

@@ -0,0 +1,8 @@
+FUTURE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-shadow-memory/getenv1/main.c

@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+void main()
+{
+  __CPROVER_field_decl_global("dr_write", (_Bool)0);
+
+  char *env = getenv("PATH");
+  __CPROVER_assume(env != NULL);
+  assert(!__CPROVER_get_field(env, "dr_write"));
+
+  __CPROVER_set_field(env, "dr_write", 1);
+  assert(__CPROVER_get_field(env, "dr_write"));
+}