diff --git a/CODEOWNERS b/CODEOWNERS index 6e9310ba6cf..93afa74e9a1 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -46,6 +46,7 @@ /src/goto-harness/ @martin-cs @chrisr-diffblue @peterschrammel /src/goto-instrument/ @martin-cs @chrisr-diffblue @peterschrammel /src/goto-instrument/code_contracts.* @tautschnig @feliperodri @SaswatPadhi +doc/cprover-manual/contracts* @tautschnig @feliperodri @SaswatPadhi /src/goto-diff/ @tautschnig @peterschrammel /src/jsil/ @kroening @tautschnig /src/memory-analyzer/ @tautschnig @chrisr-diffblue diff --git a/doc/cprover-manual/assigns-clause.md b/doc/cprover-manual/assigns-clause.md deleted file mode 100644 index e8e5dcb0ae2..00000000000 --- a/doc/cprover-manual/assigns-clause.md +++ /dev/null @@ -1,265 +0,0 @@ -# CBMC Assigns Clause - -## Introduction - -The _assigns_ clause allows the user to specify a list of memory -locations which may be written within a particular scope. While an assigns -clause may, in general, be interpreted with either _writes_ or _modifies_ -semantics, this design is based on the former. This means that memory not -captured by the assigns clause must not be written within the given scope, even -if the value(s) therein are not modified. - -Assigns clauses currently support simple variable types and their pointers, -structs, and arrays. Recursive pointer structures are left to future work, -as their support would require changes to CBMC's memory model. - - -## Syntax -A special construct is introduced to specify assigns clauses. Its syntax is -defined as follows. - -``` - := __CPROVER_assigns ( ) -``` -``` - := __CPROVER_nothing - | - | , -``` -``` - := - | [ array_index ] - | [ array_range ] - - := | - := , -``` -``` - := - | * -``` -``` - := - | . - | -> -``` -``` - := - | ( ) -``` - -The assigns clause identifies a list of targets, which may be an identifier -(e.g. `x`), a member of a struct (e.g. `myStruct.someMember` or -`myStructPtr->otherMember`), a dereferenced pointer (e.g. `*myPtr`), or an -array range (e.g. `myArr[5, lastIdx]`). The `` states that only -memory identified in the target list may be written within the function, as -described in the next section. - -For example, consider the following declarations. - -```c -struct pair -{ - int x; - int y; -}; - -void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx) -__CPROVER_assigns(*myInt1, myPair->y, myArr[5, lastIdx]); -``` - -This code declares a struct type, called `pair` with 2 members `x` and `y`, -as well as a function `foo` which takes two integer pointer arguments -`myInt1` and `myInt2`, one pair struct pointer `myPair`, and an array -argument `myArr` with an associated last index `lastIdx`. The assigns -clause attached to this definition states that most of the arguments -can be assigned. However, `myInt2`, `myPair->x`, and the first four -elements of `myArr` should not be assigned in the body of `foo`. - -## Semantics -The semantics of an assigns clause *c* of some function *f* can -be understood in two contexts. First, one may consider how the expressions in -*c* are treated when a call to *f* is replaced by its contract specification, -assuming the contract specification is a sound characterization of the behavior -of *f*. Second, one may consider how *c* is applied to the function body of *f* -in order to determine whether *c* is a sound characterization of the behavior of -*f*. To illustrate these two perspectives, consider the following definition of -`foo`. - - -```c -void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx) -{ - *myInt1 = 34; - myPair->y = 55; - myArr[5] = 89; -} -``` - -We begin by exploring these two perspectives with a formal definition, and then -an example. - -Let the ith expression in some assigns clause *c* be denoted -*exprs**c*[i], the jth formal parameter of some function -*f* be denoted *params**f*[j], and the kth argument passed -in a call to function *f* be denoted *args**f*[k] (an identifying -index may be added to distinguish a *particular* call to *f*, but for simplicity -it is omitted here). - -## Replacement -Assuming an assigns clause *c* is a sound characterization of -the behavior of the function *f*, a call to *f* may be replaced a series of -non-deterministic assignments. For each expression *e* ∈ -*exprs**c*, let there be an assignment ɸ := ∗, where -ɸ is *args**f*[i] if *e* is identical to some -*params**f*[i], and *e* otherwise. For array ranges, create an -assignment for each element in the array range. - -In the case where *f* is `foo`, and some function `bar` calls `foo` - -```c -void bar() -{ - int a, b; - int arr[8]; - struct pair p; - - foo(&a, &b, &p, arr, 7); -} -``` - -the call to `foo` is replaced by the following series of assignments. - -```c -void bar() -{ - int a, b; - int arr[10]; - struct pair p; - - a = *; - p.y = *; - arr[5] = *; - arr[6] = *; - arr[7] = *; -} -``` - -## Enforcement -In order to determine whether an assigns clause *c* is a -sound characterization of the behavior of a function *f*, the body of the -function is instrumented with assertion statements before each statement which -may write to memory (e.g. an assignment). These assertions are based on the -assignable targets *exprs**c* identified in the assigns clause. - -While sequentially traversing the function body, CBMC instruments statements -that might modify memory a preceding assertion to ensure that they only -modify assignable memory. These assertions consist of a disjunction -where each disjunct depends on the type of the assignable target. - -- For an assignable target expression *e* of scalar type: - -```c -__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&e) && -__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&e) -``` - -- For an assignable target expression *e* of struct type, a similar disjunct is - created, with an additional size comparison: - -```c -__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&e) && -__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&e) && -sizeof(lhs) == sizeof(e) -``` - -Additionally, for each member m of *e*, we add an extra disjunct: - -```c -__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&(e->m)) && -__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&(e->m)) && -sizeof(lhs) == sizeof(e->m) -``` - -This extension is performed recursively in the -case that some member of a struct is also a struct. - -- For an assignable target expression *e* of array range type, `a[lo, hi]`, a - disjunct is created using the array pointer `a` and the range bounds `lo` and -`hi`: - -```c -__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(a) && -__CPROVER_POINTER_OFFSET(&lhs) >= lo * sizeof(a[0]) && -__CPROVER_POINTER_OFFSET(&lhs) <= hi * sizeof(a[0]) -``` - -This effectively creates an assertion that the memory location being assigned -falls within the assignable memory identified by the assigns clause. In -practice, temporary variables are used to ensure that the assignable memory -doesn't change during function execution, but here we have used the assignable -targets directly for readability. Function calls are handled similarly, based -on the memory their assigns clause indicates that they can modify. -Additionally, for each function call without an assigns clause, we add an -assertion assert(*false*) to ensure that the assigns contract will only hold if -all called functions have an assigns clause which is compatible with that of the -calling function. - -For the earlier example, `foo` would be instrumented as follows: - - -```c -void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx) -{ - int *temp1 = myInt1; - int *temp2 = &(myPair->y); - int *temp3 = myArr; - int temp4 = 5 * sizeof(iint); - int temp5 = lastIdx * sizeof(int); - - assert((__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp1) && - __CPROVER_POINTER_OFFSET(myInt1) == __CPROVER_POINTER_OFFSET(temp1)) || - (__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp2) && - __CPROVER_POINTER_OFFSET(myInt1) == __CPROVER_POINTER_OFFSET(temp2)) || - (__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp3) && - __CPROVER_POINTER_OFFSET(myInt1) >= temp4 && - __CPROVER_POINTER_OFFSET(myInt1) <= temp5) - ); - *myInt1 = 34; - - assert((__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp1) && - __CPROVER_POINTER_OFFSET(&(myPair->y)) == __CPROVER_POINTER_OFFSET(temp1)) || - (__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp2) && - __CPROVER_POINTER_OFFSET(&(myPair->y)) == __CPROVER_POINTER_OFFSET(temp2)) || - (__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp3) && - __CPROVER_POINTER_OFFSET(&(myPair->y)) >= temp4 && - __CPROVER_POINTER_OFFSET(&(myPair->y)) <= temp5) - ); - myPair->y = 55; - - assert((__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp1) && - __CPROVER_POINTER_OFFSET(&(myArr[5])) == __CPROVER_POINTER_OFFSET(temp1)) || - (__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp2) && - __CPROVER_POINTER_OFFSET(&(myArr[5])) == __CPROVER_POINTER_OFFSET(temp2)) || - (__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp3) && - __CPROVER_POINTER_OFFSET(&(myArr[5])) >= temp4 && - __CPROVER_POINTER_OFFSET(&(myArr[5])) <= temp5) - ); - myArr[5] = 89; -} -``` - -Additionally, the set of assignable target expressions is updated while -traversing the function body when new memory is allocated. For example, the -statement `x = (int *)malloc(sizeof(int))` would create a pointer, stored in -`x`, to assignable memory. Since the memory is allocated within the current -function, there is no way an assignment to this memory can affect the memory of -the calling context. If memory is allocated for a struct, the subcomponents are -considered assignable as well. - -Finally, a set of freely-assignable symbols *free* is tracked during the -traversal of the function body. These are locally-defined variables and formal -parameters without dereferences. For example, in a variable declaration ` -x = `, `x` would be added to *free*. Assignment statements (i.e., -where the left-hand-side is in *free*) are not instrumented with -the above assertions. diff --git a/doc/cprover-manual/contracts-assigns.md b/doc/cprover-manual/contracts-assigns.md new file mode 100644 index 00000000000..ffec6fa373c --- /dev/null +++ b/doc/cprover-manual/contracts-assigns.md @@ -0,0 +1,175 @@ +# Assigns Clause + +### Syntax + +```c +__CPROVER_assigns(*identifier*, ...) +``` + +An _assigns_ clause allows the user to specify that a memory location may be written by a function. The set of locations writable by a function is the union of the locations specified by the assigns clauses, or the empty set of no _assigns_ clause is specified. While, in general, an _assigns_ clause could be interpreted with wither _writes_ or _modifies_ semantics, this +design is based on the former. This means that memory not captured by an +_assigns_ clause must not be written within the given function, even if the +value(s) therein are not modified. + +### Parameters + +An _assigns_ clause currently supports simple variable types and their pointers, +structs, and arrays. Recursive pointer structures are left to future work, as +their support would require changes to CBMC's memory model. For example, + +```c +int *err_signal; // Global variable + +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +__CPROVER_assigns(*out) + +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +__CPROVER_assigns(err_signal) + +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +__CPROVER_assigns(*out, err_signal) +``` + +### Semantics + +The semantics of an _assigns_ clause of a given function can be understood +in two contexts: enforcement and replacement. + +#### Enforcement + +In order to determine whether an _assigns_ clause is a sound abstraction of +the write set of a function *f*, the body of the function is instrumented with +assertion statements before each statement which may write to memory (e.g., an +assignment). These assertions are based on the writable locations identified by the _assigns_ clauses. + +For example, consider the following implementation of `sum` function. + +```c +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +/* Writable Set */ +__CPROVER_assigns(*out) +{ + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; +} +``` + +Assignable variables in the function are just those specified so with +`__CPROVER_assigns`, together with any local variables. +In the case of `sum` that is `*out` and `result`. Each assignment will be +instrumented with an assertion to check that the target of the assignment +is one of those options. + +```c +int __CPROVER_contracts_original_sum(const uint32_t a, const uint32_t b, uint32_t* out) +{ + const uint64_t result; + __CPROVER_assert((__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(out) && + __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(out)) || + (__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(&result) && + __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(&result)) + , "Check that result is assignable"); + result = ((uint64_t) *a) + ((uint64_t) *b); + if (result > UINT32_MAX) return FAILURE; + __CPROVER_assert((__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(out) && + __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(out)) || + (__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(&result) && + __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(&result)) + , "Check that result is assignable"); + *out = (uint32_t) result; + return SUCCESS; +} + +/* Function Contract Enforcement */ +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +{ + int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); + return return_value_sum; +} +``` + +Additionally, the set of assignable target expressions is updated while +traversing the function body when new memory is allocated. For example, the +statement `x = (int *)malloc(sizeof(int))` would create a pointer, stored in +`x`, to assignable memory. Since the memory is allocated within the current +function, there is no way an assignment to this memory can affect the memory of +the calling context. If memory is allocated for a struct, the subcomponents are +considered assignable as well. + +Finally, a set of freely-assignable symbols *free* is tracked during the +traversal of the function body. These are locally-defined variables and formal +parameters without dereferences. For example, in a variable declaration ` +x = `, `x` would be added to *free*. Assignment statements where the left-hand-side is in *free* are not instrumented with the above assertions. + +#### Replacement + +Assuming _assigns_ clauses are a sound abstraction of the write set for +a given function, CBMC will use the function contract in place of the function +implementation as described by [Requires \& Ensures +Clauses](contracts-requires-and-ensures.md) - Replacement section, and it will add +non-deterministic assignments for each object listed in the `__CPROVER_assigns` +clause. Since these objects might be modified by the function, CBMC uses +non-deterministic assignments to havoc them and restrict their values only by +assuming the postconditions. + +In our example, consider that a function `foo` may call `sum`. + +```c +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +/* Preconditions */ +__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) +/* Postconditions */ +__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE) +__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b))) +/* Writable Set */ +__CPROVER_assigns(*out) +{ + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; +} + +int foo() +{ + uint32_t a; + uint32_t b; + uint32_t out; + int rval = sum(a, b, &out); + if (rval == SUCCESS) + return out; + return rval; +} +``` + +CBMC will use the function contract in place of the function implementation +wherever the function is called. + +```c +int foo() +{ + uint32_t a; + uint32_t b; + uint32_t out; + + + /* Function Contract Replacement */ + /* Precondition */ + __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); + + /* Writable Set */ + *(&out) = nondet_uint32_t(); + + /* Postconditions */ + int return_value_sum = nondet_int(); + __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); + __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (*a + *b))); + + int rval = return_value_sum; + if (rval == SUCCESS) + return out; + return rval; +} +``` diff --git a/doc/cprover-manual/contracts-history-variables.md b/doc/cprover-manual/contracts-history-variables.md new file mode 100644 index 00000000000..90f3eaa5dda --- /dev/null +++ b/doc/cprover-manual/contracts-history-variables.md @@ -0,0 +1,36 @@ +# History Variables + +### Syntax + +```c +__CPROVER_old(*identifier*) +``` + +Refers to the value of a given object in the pre-state of a function within the +_ensures_ clause. + +**Important.** This function may be used only within the context of `__CPROVER_ensures`. + +### Parameters + +`__CPROVER_old` takes a single argument, which is the identifier corresponding to +a parameter of the function. For now, only scalar, structs, or pointer types are supported. + + +### Semantics + +To illustrate the behavior of `__CPROVER_old`, take a look at the example +bellow. If the function returns a failure code, the value of `*out` should not +have been modified. + +```c +int sum(uint32_t* a, uint32_t* b, uint32_t* out) + +/* Postconditions */ +__CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out))) +/* Writable Set */ +__CPROVER_assigns(*out) +{ + /* ... */ +} +``` diff --git a/doc/cprover-manual/contracts-memory-predicates.md b/doc/cprover-manual/contracts-memory-predicates.md new file mode 100644 index 00000000000..f1a9b9fcc5d --- /dev/null +++ b/doc/cprover-manual/contracts-memory-predicates.md @@ -0,0 +1,118 @@ +# Memory Predicates + + +### Syntax + +```c +bool __CPROVER_is_fresh(void *p, size_t size); +``` + +To specify memory footprint we use a special function called `__CPROVER_is_fresh `. The meaning of `__CPROVER_is_fresh` is that we are borrowing a pointer from the +external environment (in a precondition), or returning it to the calling context (in a postcondition). + +### Parameters + +`__CPROVER_is_fresh` takes two arguments: a pointer and an allocation size. +The first argument is the pointer to be checked for "freshness" (i.e., not previously +allocated), and the second is the expected size in bytes for the memory +available at the pointer. + +### Return Value + +It returns a `bool` value, indicating whether the pointer is fresh. + +### Semantics + +To illustrate the semantics for `__CPROVER_is_fresh`, consider the following implementation of `sum` function. + +```c +int *err_signal; // Global variable + +void sum(const uint32_t a, const uint32_t b, uint32_t* out) +__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) +__CPROVER_ensures(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))) +__CPROVER_assigns(*out, err_signal) +{ + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + err_signal = malloc(sizeof(*err_signal)); + if (!err_signal) return; + if (result > UINT32_MAX) *err_signal = FAILURE; + *out = (uint32_t) result; + *err_signal = SUCCESS; +} +``` + +#### Enforcement + +When checking the contract abstracts a function a `__CPROVER_is_fresh` +in a _requires_ clause will cause fresh memory to be allocated. +In an _ensures_ clause it will check that memory was freshly allocated. + +```c +int *err_signal; // Global variable + +int __CPROVER_contracts_original_sum(const uint32_t a, const uint32_t b, uint32_t* out) +{ + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + err_signal = malloc(sizeof(*err_signal)); + if (!err_signal) return; + if (result > UINT32_MAX) *err_signal = FAILURE; + *out = (uint32_t) result; + *err_signal = SUCCESS; +} + +/* Function Contract Enforcement */ +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +{ + __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); // Assumes out is freshly allocated + int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); + __CPROVER_assert(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)), "Check ensures clause"); + return return_value_sum; +} +``` + +#### Replacement + +In our example, consider that a function `foo` may call `sum`. + +```c +int *err_signal; // Global variable + +int foo() +{ + uint32_t a; + uint32_t b; + uint32_t out; + sum(a, b, &out); + return *err_signal; +} +``` + +When using a contract as an abstraction in place of a call to the function +a `__CPROVER_is_fresh` in a _requires_ clause will check that the argument +supplied is fresh and `__CPROVER_is_fresh` in an _ensures_ clause will +result in a fresh malloc. + +```c +int *err_signal; // Global variable + +int foo() +{ + uint32_t a; + uint32_t b; + uint32_t out; + + /* Function Contract Replacement */ + /* Precondition */ + __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); + + /* Writable Set */ + *(&out) = nondet_uint32_t(); + err_signal = nondet_int_pointer(); + + /* Postconditions */ + __CPROVER_assume(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))); // Assumes out is allocated + + return *err_signal; +} +``` \ No newline at end of file diff --git a/doc/cprover-manual/contracts-quantifiers.md b/doc/cprover-manual/contracts-quantifiers.md new file mode 100644 index 00000000000..19c4442d252 --- /dev/null +++ b/doc/cprover-manual/contracts-quantifiers.md @@ -0,0 +1,60 @@ +# Quantifiers + +### Syntax + +```c +__CPROVER_forall { *type* *identifier*; *boolean expression* } +__CPROVER_exists { *type* *identifier*; *boolean expression* } +``` + +While quantified expressions with arbitrary Boolean expressions are supported with an SMT backend, the SAT backend only supports bounded quantification under _constant_ lower & upper bounds. This is because the SAT backend currently expands a universal quantifier (`__CPROVER_forall`) to a conjunction and an existential quantifier (`__CPROVER_exists`) to a disjunction on each value within the specified bound. + +Concretely, with the SAT backend, the following syntax must be used for quantifiers within function contracts: + +``` +__CPROVER_forall { *id* *type*; *range* => *boolean expression* } +__CPROVER_exists { *id* *type*; *range* && *boolean expression* } +``` + +where `*range*` is an expression of the form + +``` +*lower bound* <= *id* && *id* <= *upper bound* +``` + +where `*lower bound*`and `*upper bound*` are constants. + + +### Semantics + +For `__CPROVER_forall` all `*type*` values for `*identifier*` must satisfy +`*boolean expression*`. + +```c +int foo(int *arr, int len) + /* ... */ + __CPROVER_ensures(__CPROVER_forall { + int i; + (0 <= i && i < len) ==> arr[i] == i + }) +{ + /* ... */ +} +``` + +For `__CPROVER_exists` some (at least one) `*type*` value for `*identifier*` +must satisfy `*boolean expression*`. + +```c +int bar(int *arr, int len) + __CPROVER_requires(__CPROVER_exists { + int i; + (0 <= i && i < len) && arr[i] == 1 + }) + /* ... */ +{ + /* ... */ +} +``` + +The examples above only work with the SMT backend, since `len` is not constant. \ No newline at end of file diff --git a/doc/cprover-manual/contracts-requires-and-ensures.md b/doc/cprover-manual/contracts-requires-and-ensures.md new file mode 100644 index 00000000000..5863ecd3286 --- /dev/null +++ b/doc/cprover-manual/contracts-requires-and-ensures.md @@ -0,0 +1,134 @@ +# Requires \& Ensures Clauses + + +### Syntax + +```c +__CPROVER_requires(bool cond) +``` + +A _requires_ clause specifies a precondition for a function, i.e., a property that must hold to properly execute the operation. Developers may see the _requires_ clauses of a function as obligations on the caller when invoking the function. The precondition of a function is the conjunction of the _requires_ clauses, or `true` if none are specified. + +```c +__CPROVER_ensures(bool cond) +``` + +An _ensures_ clause specifies a postcondition for a function, i.e., a property over arguments or global variables that the function guarantees at the end of the operation. Developers may see the _ensures_ clauses of a function as the obligations of that function to the caller. The postcondition of a function is the conjunction of the _ensures_ clauses, or `true` if none are specified. + + +### Parameters + +A _requires_ clause takes a Boolean expression over the arguments of +a function and/or global variables, including CBMC primitive functions (e.g., +[Memory Predicates](contracts-memory-predicates.md)). Similarly, _ensures_ clauses also accept Boolean +expressions and CBMC primitives, but also [History Variables](contracts-history-variables.md) and `__CPROVER_return_value`. + +**Important.** Developers may call functions inside _requires_ and _ensures_ +clauses to better write larger specifications (e.g., predicates). However, at +this point CBMC does not enforce such functions to be without side effects +(i.e., do not modify any global state). This will be checked in future +versions. + + +### Semantics + +The semantics of _ensures_ and _requires_ clauses can be understood in two +contexts: enforcement and replacement. To illustrate these two perspectives, +consider the following implementation of the `sum` function. + +```c +int sum(uint32_t a, uint32_t b, uint32_t* out) +/* Preconditions */ +__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) +/* Postconditions */ +__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE) +__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (*a + *b))) +{ + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; +} +``` + +#### Enforcement + +In order to determine whether _requires_ and _ensures_ clauses are a sound +abstraction of the behavior of a function *f*, CBMC will try to check them +as follows: + +1. Considers all arguments and global variables as non-deterministic values; +2. Assumes all preconditions specified in the `__CPROVER_requires` clauses; +4. Calls the implementation of function *f*; +5. Asserts all postconditions described in the `__CPROVER_ensures` clauses. + +In our example, the `sum` function will be instrumented as follows: + +```c +/* Function Contract Enforcement */ +int sum(uint32_t a, uint32_t b, uint32_t* out) +{ + __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); + + int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); + + __CPROVER_assert(return_value_sum == SUCCESS || return_value_sum == FAILURE, "Check ensures clause"); + __CPROVER_assert((return_value_sum == SUCCESS) ==> (*out == (a + b)), "Check ensures clause"); + + return return_value_sum; +} +``` + +#### Replacement + +Assuming _requires_ and _ensures_ clauses are a sound abstraction of the +behavior of the function *f*, CBMC will use the function contract in place of +the function implementation as follows: + +1. Adds assertions for all preconditions specified in the `__CPROVER_requires` + clauses; +2. Adds non-deterministic assignments for each symbol listed in the + `__CPROVER_assigns` clause (see [Assigns Clause](contracts-assigns.md) Section +for details); +3. Assumes all postconditions described in the `__CPROVER_ensures` clauses; + +In our example, consider that a function `foo` may call `sum`. + +```c +int foo() +{ + uint32_t a; + uint32_t b; + uint32_t out; + int rval = sum(a, b, &out); + if (rval == SUCCESS) + return out; + return rval; +} +``` + +CBMC will use the function contract in place of the function implementation +wherever the function is called. + +```c +int foo() +{ + uint32_t a; + uint32_t b; + uint32_t out; + + /* Function Contract Replacement */ + /* Precondition */ + __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); + + /* Postconditions */ + int return_value_sum = nondet_int(); + __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); + __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (*a + *b))); + + int rval = return_value_sum; + if (rval == SUCCESS) + return out; + return rval; +} +``` diff --git a/doc/cprover-manual/contracts.md b/doc/cprover-manual/contracts.md new file mode 100644 index 00000000000..8d86f43d7fb --- /dev/null +++ b/doc/cprover-manual/contracts.md @@ -0,0 +1,160 @@ +# Function Contracts + +CBMC offers support for function contracts, which includes three basic clauses: +_requires_, _ensures_, and _assigns_. +These clauses formally describe the specification of a function. CBMC +also provides a series of built-in constructs to be used with functions +contracts (e.g., _history variables_, _quantifiers_, and _memory predicates_). + +To learn more about contracts, take a look at the chapter [Design by +Contract](http://se.inf.ethz.ch/~meyer/publications/old/dbc_chapter.pdf) from +the book Object-Oriented Software Construction by Bertrand Meyer or read the +notes [Contract-based +Design](https://www.georgefairbanks.com/york-university-contract-based-design-2021) +by George Fairbanks. + +## Overview + +Take a look at the example below. + +```c +#include +#include + +#define SUCCESS 0 +#define FAILURE -1 + +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +{ + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; +} + +int foo() +{ + uint32_t a; + uint32_t b; + uint32_t out; + int rval = sum(a, b, &out); + if (rval == SUCCESS) + return out; + return rval; +} +``` + +Function `sum` writes the sum of `a` and `b` to `out`, and returns `SUCCESS`; +unless the result of the addition is too large to be represented as an `uint32_t`, in which case it returns `FAILURE`. Let's write +a function contract for this function. + +A function contract has three parts: + +- **Precondition** - describes what the function requires of the arguments + supplied by the caller and of global variables; +- **Postcondition** - describes the effect of the function; +- **Write Set** - describes the set of locations outside the function that + might be written to. + +In our example, the developer may require from the caller to properly allocate +all arguments, thus, pointers must be valid. We can specify the preconditions of +a function using `__CPROVER_requires` (see [Requires \& Ensures +Clauses](contracts-requires-and-ensures.md) Section for details) and we can +specify an allocated object using a predicate called `__CPROVER_is_fresh` (see +[Memory Predicate](contracts-memory-predicates.md) Section for details). Thus, for the `sum` function, the set +of preconditions are + +```c +/* Precondition */ +__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) +``` + +We can use `__CPROVER_ensures` to specify postconditions (see [Requires \& +Ensures Clauses](contracts-requires-and-ensures.md) Section for details). In our +example, developers can use the built-in construct `__CPROVER_return_value`, +which represents the return value of a function. As postconditions, one may list +possible return values (in this case, either `SUCCESS` or `FAILURE`) as well as +describe the main property of this function: if the function returns `SUCCESS`, +then `*out` stores the result of `*a + *b`. We can also check that the value in +`*out` will be preserved in case of failure by using `__CPROVER_old`, which +refers to the value of a given object in the pre-state of a function (see +[History Variables](contracts-history-variables.md) Section for details). Thus, for the `sum` function, the +set of postconditions are + + +```c +/* Postconditions */ +__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE) +__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b))) +__CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out))) +``` + +Finally, the _assigns_ clause allows developers to define a frame condition (see +[Assigns Clause](contracts-assigns.md) Section for details). +In general, systems for describing the frame condition of a function +use either writes or modifies semantics; this design is based on the former. +This means that memory not specified by the assigns clause must +not be written within the given function scope, even if the value(s) therein are +not modified. In our example, since we expect that only the value that +`out` points to may be modified, we annotate the function using `__CPROVER_assigns(*out)`. + +```c +/* Write Set */ +__CPROVER_assigns(*out) +``` + +Here is the whole function with its contract. + +```c +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +/* Precondition */ +__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) +/* Postconditions */ +__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE) +__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b))) +__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == __CPROVER_old(*out))) +/* Write Set */ +__CPROVER_assigns(*out) +{ + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; +} +``` + +First, we have to prove that the function satisfies the contract. + +```shell + goto-cc -o sum.goto *.c + goto-instrument --enforce-contract sum sum.goto sum-checking-contracts.goto + cbmc sum-checking-contracts.goto --function sum +``` + +The first command just compiles the GOTO program as usual, the second command +instruments the code to check the function satisfies the contract, +and the third one runs CBMC to do the checking. + +Now that we have proved that the function satisfies the contract, we can use the function +contract in place of the function implementation wherever the function is +called. + +```shell + goto-cc -o foo.goto *.c + goto-instrument --replace-call-with-contract foo foo.goto sum-using-contracts.goto + cbmc foo-using-contracts.goto --function foo +``` + +The first command just compiles the GOTO program as usual, the second command +instruments the code to use the function contract in place of the function +implementation wherever is invoked, and the third one runs CBMC to check the +program using contracts. + +## Additional Resources + +- [Requires \& Ensures Clauses](contracts-requires-and-ensures.md) +- [Assigns Clause](contracts-assigns.md) +- [Memory Predicates](contracts-memory-predicates.md) +- [History Variables](contracts-history-variables.md) +- [Quantifiers](contracts-quantifiers.md) +- [Loop Invariants \& Loop Variants]()