CONTRACTS: dynamic frame condition checking for function contracts.

- Fixes #7197
- Fixes #7198
- Fixes #7206

Overview
---

The new features brought by the system are:
- Allow to use C functions to specify reusable/parametric assigns
  clauses and frees clauses in the contracts language;
- Allow function calls in pre- and post-conditions and check the
  absence of side-effects;
- Checking contracts on recursive functions (by assuming preconditions
  and asserting post conditions on the top level call and asserting
  pre conditions and assuming post conditions on the recursive call)
- The frame checks are fully dynamic and does not require inlining the
  program or unwinding loops a priori;
- The method is compatible with deferred resolution of function
  pointers calls during symex;
- All CPROVER library functions are supported;

In addition:
- The checks are implemented as C library
  `src/ansi-c/library/cprover_contracts.c`, the instrumentation insert
  calls to the library in the program;
- Contract checking and contract replacement mostly share the same
  code;
- The whole system's user documentation and developer documentation is
  written in the doxygen format and found in
  `src/goto-instrument/contracts/doc/`.

Limitations:
- loop contracts are not yet ported to the new framework;
- deferred function pointer resolution is not yet implemented,
  user-specified function pointer restriction is still required;
- havocing during contract replacement still relies on snapshots known
  to affect performance;
- more work is performed by symbolic execution which can be felt on
  runtime;

Method
---

Let’s call `f_top`​ the top-level function against which the contract
is being checked.

We assume `f_top`​ is itself called from a `harness` function, which
may call other functions besides `f_top`​.

Let’s consider a function `f` that is either `f_top​` or one of the
functions called (directly or indirectly) by `f_top`​. The goal is to
verify that `f` writes only to memory locations that are part of the
frame of the call to `f_top` but allowed by the contract or that were
allocated after entering `f_top`​ and are hence not part of the frame
of the call. To do that, we add ghost code to the program to build
representations the following sets of memory locations as the program
runs:

(`contract_assigns`, `contract_frees`, `allocated`, `deallocated`)

where:

- `contract_assigns` is the set of memory locations specified in the
  *assigns clause* of the contract being checked
- `contract_frees` is the set of pointers specified in the *frees
  clause* of the contract being checked
- `allocated` is the set objects identifiers allocated on the stack or
  the heap since entering `f_top`​
- `deallocated` is the set of heap objects identifiers deallocated
  since entering `f_top`​ (allows verification that an object was freed
  as a post-condition of the contract)
The instrumentation transforms all user-defined goto functions and
library functions:

```c
ret_t f(<parameters>);
```

Into functions accepting an extra parameter that is a pointer to a
dynamic representation of the sets introduced above:

```c
ret_t f(<parameters>,  __CPROVER_contracts_write_set_ptr_t write_set);
```

Function bodies is instrumented so that when the write_set pointer is
NULL no checks are performed, when it is not NULL the following checks
are performed:
- Assignments LHS are checked for inclusion in `contract_assigns` or
  `allocated`,
- DECL objects are recorded in `allocated`
- Dynamically allocated objects are recorded in `allocated`
- DEAD objects or objects assigned to `__CPROVER_dead_object` are
  removed from `allocated`
- dynamic objects deallocated with `__CPROVER_deallocate` are checked
  for inclusion in `contract_frees` or `allocated`, and recorded in
  `deallocated` (so that if needed we can check in post conditions
  that the function indeed deallocated the expected memory).
- The current write set is propagated to all functions calls or
  function pointer calls.

Since the write set is dynamically updated, a same function called at
different call sites can see a different write set.

Write sets are initialised from contracts descriptions and injected in
function calls that are checked against contracts, or used to perform
inclusion checks against write sets obtained from callers for
functions that are replaced by a contract.

Implementation
---

The class `dfcc_utilst` provides methods to
manipulate function symbols in the symbol table:
- create fresh local symbols
- create parameter symbols
- create static symbols
- clone and rename function symbols
- add function parameters
- rename function parameters

The file `cprover_contracts.c` defines:
- C types representing write sets
- C functions to create/populate/release write sets
- C functions to do write sets inclusion checks
- C functions implementing built-in predicates
 `__CPROVER_is_freeable`, `__CPROVER_was_freed`,
 `__CPROVER_is_fresh`

The class `dfcc_libraryt` provides a programmatic interface to load
and use the library-defined types and functions and perform some
optimisations like inlining or unwinding loops in library functions.

The class `dfcc_contract_modet` is an enum representing the CHECK and
REPLACE modes for contracts.

The class `dfcc_is_fresht` Rewrites calls to `__CPROVER_is_fresh` into
calls to the library implementation `__CPROVER_contracts_is_fresh`.

The class `dfcc_is_freeablet` rewrites calls to
`__CPROVER_is_freeable` into calls to the library implementation
`__CPROVER_contracts_is_freeable` and rewrites calls to
`__CPROVER_was_freed` into calls to the library implementation
`__CPROVER_contracts_was_freed`.

The class `goto_program_cfg_infot` extends `cfg_infot` and computes
the set of program-locals from DECLs found in the instruction
sequence. Contrary to the existing `function_cfg_infot` this new class
does consider parameters symbols as locals.

The class `dfcc_instrumentt` instruments GOTO functions with write-set
checks.  It also instruments proof harness functions and sub-sequences
of GOTO instructions extracted from larger GOTO programs.

The class `dfcc_spec_functionst` rewrites assigns clause and frees
clause specification functions into functions that populate a given
write-set, and can be checked for side-effects against a second
write-set.

The class `dfcc_contract_functionst` allows to translate the assigns
clause (or frees clause) of a contract expressed in DSL style into
GOTO a function describing the same set of targets as the clause. It
also allows to generate a havoc function from an assigns clause, that
havocs the targets described by the clause in a type-directed way.

The class `dfcc_dsl_wrapper_programt` generates a sequence of GOTO
instruction from a contract expressed in the DSL syntax.  The
instructions either encode a checked call to the function under
verification (CHECK mode) or an abstraction derived from the contract
(REPLACE mode). In CHECK mode, it generates GOTO instructions that
assume preconditions, snapshots history variables, creates a write set
instance, call the function under verification asserts the
postconditions, and returns the call's return value. In REPLACE mode,
it generates GOTO instructions encoding the nondeterministic
abstraction defined by the contract: assert preconditions, create and
havoc assigns clause targets, create a nondet return value for the
call, nondeterministically free frees clause targets, assume
postconditions, return a value that satisfies the post
conditions. These instructions are meant to be added to the GOTO
function that serves as a wrapper for the function under verification
or being replaced by the contract.

The class `dfcc_contract_handlert` is an abstract interface for
generating GOTO instructions from contracts for CHECK or REPLACE
modes. It delegates the actual generation to
`dfcc_dsl_wrapper_programt`.

The class `dfcc_swap_and_wrapt`, given a `function_id`, a
`contract_id`, a contract `mode`, and a `dfcc_contract_handlert` for
the contract, swaps the body of the function to a function with a
mangled name and instruments the mangled function for dynamic frame
condition checking using `dfcc_instrument`. The body of the original
function is then replaced with instructions generated by the contract
handler for the required contract mode (CHECK or REPLACE). To handle
recursive functions in contract checking mode, the body of the wrapper
function is generated in such a way the first invocation results in
checking the contract against the mangled function and recursive
invocations of the wrapper behave like the contract abstraction
(induction hypothesis for the recursive call).

The `dfcct` class receives the proof harness function, the map of
functions and contracts to check and the map of functions to replace
with contracts.  It instruments the proof harness, performs
swap-and-wrap operations for each of the checked and replaced
functions. It then instruments all other functions for DFCC.

Regression Tests
---

Regression tests are found in `regression/contracts-dfcc`. These
tests are ported from `regression/contracts` and only contain
tests for function contracts.

Author: Remi Delmas

doc/cprover-manual/contracts-requires-and-ensures.md

@@ -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

doc/man/goto-instrument.1

@@ -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/CMakeLists.txt

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

regression/Makefile

@@ -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/CMakeLists.txt

@@ -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/Makefile

@@ -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/main.c

@@ -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.