CONTRACTS: Add test suite for DFCC

Tests are ported from regression/contracts.
They only include function contracts for now,
at the exclusion of loop contracts.

Author: Remi Delmas

regression/CMakeLists.txt

@@ -65,6 +65,7 @@ add_subdirectory(goto-analyzer-simplify)
 add_subdirectory(statement-list)
 add_subdirectory(systemc)
 add_subdirectory(contracts)
+add_subdirectory(contracts-dfcc)
 add_subdirectory(acceleration)
 add_subdirectory(k-induction)
 add_subdirectory(goto-harness)

regression/Makefile

@@ -38,6 +38,7 @@ DIRS = cbmc \
        statement-list \
        systemc \
        contracts \
+       contracts-dfcc \
        acceleration \
        k-induction \
        goto-harness \

regression/contracts-dfcc/CMakeLists.txt

@@ -0,0 +1,43 @@
+if(WIN32)
+  set(is_windows true)
+else()
+  set(is_windows false)
+endif()
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  set(gcc_only -X gcc-only)
+  set(gcc_only_string "-X;gcc-only;")
+else()
+  set(gcc_only "")
+  set(gcc_only_string "")
+endif()
+
+
+add_test_pl_tests(
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
+)
+
+## Enabling these causes a very significant increase in the time taken to run the regressions
+
+#add_test_pl_profile(
+#    "cbmc-z3"
+#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --z3' ${is_windows}"
+#    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-z3-backend;-X;thorough-z3-backend;${gcc_only_string}-s;z3"
+#    "CORE"
+#)
+
+#add_test_pl_profile(
+#    "cbmc-cprover-smt2"
+#    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> '$<TARGET_FILE:cbmc> --cprover-smt2' ${is_windows}"
+#    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt2-backend;-X;thorough-cprover-smt2-backend;${gcc_only_string}-s;cprover-smt2"
+#    "CORE"
+#)
+
+# solver appears on the PATH in Windows already
+#if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
+#  set_property(
+#    TEST "cbmc-cprover-smt2-CORE"
+#    PROPERTY ENVIRONMENT
+#      "PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
+#  )
+#endif()

regression/contracts-dfcc/Makefile

@@ -0,0 +1,42 @@
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+	exe=../../../src/goto-cc/goto-cl
+	is_windows=true
+	GCC_ONLY = -X gcc-only
+else
+	exe=../../../src/goto-cc/goto-cc
+	is_windows=false
+	GCC_ONLY =
+endif
+
+test:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' -X smt-backend $(GCC_ONLY)
+
+test-cprover-smt2:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --cprover-smt2" $(is_windows)' \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
+					  -s cprover-smt2 $(GCC_ONLY)
+
+test-z3:
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument "../../../src/cbmc/cbmc --z3" $(is_windows)' \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
+					  -s z3 $(GCC_ONLY)
+
+tests.log: ../test.pl test
+
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb *.smt2; \
+			cd ..; \
+		fi \
+	done

regression/contracts-dfcc/assigns-enforce-malloc-zero/main.c

@@ -0,0 +1,31 @@
+#include <stdlib.h>
+
+// returns the index at which the write was performed if any
+// -1 otherwise
+int foo(char *a, int size)
+  // clang-format off
+  __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
+  __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size))
+  __CPROVER_assigns(a: __CPROVER_object_whole(a))
+  __CPROVER_ensures(
+    a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
+// clang-format on
+{
+  if(!a)
+    return -1;
+  int i;
+  if(0 <= i && i < size)
+  {
+    a[i] = 0;
+    return i;
+  }
+  return -1;
+}
+
+int main()
+{
+  size_t size;
+  char *a;
+  foo(a, size);
+  return 0;
+}

regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
+^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that objects of size zero or __CPROVER_max_malloc_size
+do not cause spurious falsifications in assigns clause instrumentation
+in contract enforcement mode.

regression/contracts-dfcc/assigns-local-composite/main.c

@@ -0,0 +1,104 @@
+struct st1
+{
+  int a;
+  int arr[10];
+};
+
+struct st2
+{
+  int a;
+  struct st1 arr[10];
+};
+
+struct st3
+{
+  struct st1 *s1;
+  struct st2 *s2;
+  struct st1 arr1[10];
+  struct st2 arr2[10];
+};
+
+enum tagt
+{
+  CHAR,
+  INT,
+  CHAR_PTR,
+  INT_ARR,
+  STRUCT_ST1_ARR
+};
+
+// clang-format off
+struct taggedt {
+  enum tagt tag;
+  union {
+    struct{ char a; };
+    struct{ int b; };
+    struct{ char *ptr; };
+    struct{ int arr[10]; };
+    struct{ struct st1 arr1[10]; };
+  };
+};
+// clang-format on
+
+int foo(int i) __CPROVER_assigns()
+{
+  // all accesses to locals should pass
+  int arr[10];
+  struct st1 s1;
+  struct st2 s2;
+  struct st1 dirty_s1;
+  struct st3 s3;
+  s3.s1 = &dirty_s1;
+  s3.s2 = malloc(sizeof(struct st2));
+
+  if(0 <= i && i < 10)
+  {
+    arr[i] = 0;
+    s1.a = 0;
+    s1.arr[i] = 0;
+    s2.a = 0;
+    s2.arr[i].a = 0;
+    s2.arr[i].arr[i] = 0;
+    s3.s1->a = 0;
+    s3.s1->arr[i] = 0;
+    s3.s2->a = 0;
+    s3.s2->arr[i].a = 0;
+    s3.s2->arr[i].arr[i] = 0;
+    *(&(s3.s2->arr[i].arr[0]) + i) = 0;
+    (&(s3.arr1[0]) + i)->arr[i] = 0;
+    (&((&(s3.arr2[0]) + i)->arr[i]))->a = 0;
+  }
+
+  struct taggedt tagged;
+  switch(tagged.tag)
+  {
+  case CHAR:
+    tagged.a = 0;
+    break;
+  case INT:
+    tagged.b = 0;
+    break;
+  case CHAR_PTR:
+    tagged.ptr = 0;
+    break;
+  case INT_ARR:
+    if(0 <= i && i < 10)
+      tagged.arr[i] = 0;
+    break;
+  case STRUCT_ST1_ARR:
+    if(0 <= i && i < 10)
+    {
+      tagged.arr1[i].a = 0;
+      tagged.arr1[i].arr[i] = 0;
+    }
+    break;
+  }
+
+  return 0;
+}
+
+void main()
+{
+  int i;
+  foo(i);
+}

regression/contracts-dfcc/assigns-local-composite/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that assigns clause checking explicitly checks assignments to locally
+declared symbols with composite types, when they are dirty.
+Out of bounds accesses to locally declared arrays, structs, etc.
+will be detected by assigns clause checking.

regression/contracts-dfcc/assigns-replace-ignored-return-value/main.c

@@ -0,0 +1,37 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+int bar(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  return l + r;
+}
+
+int *baz(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    *__CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  int *res = malloc(sizeof(int));
+  *res = l + r;
+  return res;
+}
+
+int foo(int l, int r) __CPROVER_requires(0 <= l && l <= 10)
+  __CPROVER_requires(0 <= r && r <= 10) __CPROVER_assigns() __CPROVER_ensures(
+    __CPROVER_return_value == __CPROVER_old(l) + __CPROVER_old(r))
+{
+  bar(l, r);
+  bar(l, r);
+  baz(l, r);
+  baz(l, r);
+  return l + r;
+}
+
+int main()
+{
+  int l;
+  int r;
+  foo(l, r);
+  return 0;
+}

regression/contracts-dfcc/assigns-replace-ignored-return-value/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^\[.*assigns.*\].*ignored_return_value.*FAILURE
+--
+This test checks that when replacing a call by a contract for a call that
+ignores the return value of the function, the temporary introduced to 
+receive the call result does not trigger errors with assigns clause Checking
+in the function under verification.

regression/contracts-dfcc/assigns-replace-malloc-zero/main.c

@@ -0,0 +1,37 @@
+#include <stdlib.h>
+
+// returns the index at which the write was performed if any
+// -1 otherwise
+int foo(char *a, int size)
+  // clang-format off
+__CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
+__CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size))
+__CPROVER_assigns(__CPROVER_object_whole(a))
+__CPROVER_ensures(
+    a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
+// clang-format on
+{
+  if(!a)
+    return -1;
+  int i;
+  if(0 <= i && i < size)
+  {
+    a[i] = 0;
+    return i;
+  }
+  return -1;
+}
+
+int main()
+{
+  int size;
+  if(size < 0)
+    size = 0;
+  if(size > __CPROVER_max_malloc_size)
+    size = __CPROVER_max_malloc_size;
+  char *a = malloc(size * sizeof(*a));
+  int res = foo(a, size);
+  if(a && res >= 0)
+    __CPROVER_assert(a[res] == 0, "expecting SUCCESS");
+  return 0;
+}

regression/contracts-dfcc/assigns-replace-malloc-zero/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--dfcc main --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
+^EXIT=0$
+^SIGNAL=0$
+\[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+This test checks that objects of size zero or of __CPROVER_max_malloc_size
+do not cause spurious falsifications in assigns clause instrumentation
+in contract replacement mode.