CONTRACTS: Dynamic frame condition checking

doc/man/goto-instrument.1

@@ -1003,6 +1003,12 @@ replace calls to \fIfun\fR with \fIfun\fR's contract
 .TP
 \fB\-\-enforce\-contract\fR \fIfun\fR
 wrap \fIfun\fR with an assertion of its contract
+.TP
+\fB\-\-enforce\-contract\-rec\fR \fIfun\fR
+wrap \fIfun\fR with an assertion of its contract that can handle recursive calls
+.TP
+\fB\-\-dfcc\fR \fIfun\fR
+instrument dynamic frame condition checks method using \fIfun\fR as entry point
 .SS "User-interface options:"
 .TP
 \fB\-\-flush\fR

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.