Merge pull request #7479 from peterschrammel/shadow-memory-tests

Tests for future shadow memory feature

Author: peterschrammel

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