Skip to content

Avoid crashing when applying trivial contracts #6255

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
feliperodri merged 6 commits into from
Jul 28, 2021
Merged

Avoid crashing when applying trivial contracts #6255

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
0c4574f
Removes get_namespace() from contracts module
feliperodri Jul 21, 2021
552beee
Consistent order of parameters across contracts functions
feliperodri Jul 27, 2021
61ea8ed
Avoid crashing when applying trivial contracts
feliperodri Jul 27, 2021
3a1b249
Removes unimplemented method from code_contractst
feliperodri Jul 27, 2021
a0646ec
Improves description of code_contractst methods
feliperodri Jul 27, 2021
2c32f86
Fixes typos across contracts manual
feliperodri Jul 28, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
111 changes: 56 additions & 55 deletions doc/cprover-manual/contracts-assigns.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
__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
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 either _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.
Expand All @@ -15,10 +15,11 @@ value(s) therein are not modified.

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,
their support would require changes to CBMC's memory model.

```c
int *err_signal; // Global variable
/* Examples */
int err_signal; // Global variable

int sum(const uint32_t a, const uint32_t b, uint32_t* out)
__CPROVER_assigns(*out)
Expand Down Expand Up @@ -49,10 +50,10 @@ 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;
const uint64_t result = ((uint64_t) a) + ((uint64_t) b);
if (result > UINT32_MAX) return FAILURE;
*out = (uint32_t) result;
return SUCCESS;
}
```

Expand All @@ -65,28 +66,28 @@ 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;
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;
int return_value_sum = __CPROVER_contracts_original_sum(a, b, out);
return return_value_sum;
}
```

Expand All @@ -101,7 +102,8 @@ 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 `<type>
x = <initial_value>`, `x` would be added to *free*. Assignment statements where the left-hand-side is in *free* are not instrumented with the above assertions.
x = <initial_value>`, `x` would be added to the *free* set. Assignment statements
where the left-hand-side is in the *free* set are not instrumented with the above assertions.

#### Replacement

Expand All @@ -112,7 +114,7 @@ Clauses](contracts-requires-and-ensures.md) - Replacement section, and it will a
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.
assuming the postconditions (i.e., requires clauses).
Copy link
Contributor

@SaswatPadhi SaswatPadhi Jul 28, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for fixing the docs! So many tiny errors (including errors in code examples) went unnoticed the last time!

Just one small issues: I think you meant "ensures" (not "requires") clauses in this sentence.


In our example, consider that a function `foo` may call `sum`.

Expand All @@ -126,21 +128,21 @@ __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;
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;
uint32_t a;
uint32_t b;
uint32_t out;
int rval = sum(a, b, &out);
if (rval == SUCCESS)
return out;
return rval;
}
```

Expand All @@ -150,26 +152,25 @@ wherever the function is called.
```c
int foo()
{
uint32_t a;
uint32_t b;
uint32_t out;
uint32_t a;
uint32_t b;
uint32_t out;

/* Function Contract Replacement */
/* Precondition */
__CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");

/* Function Contract Replacement */
/* Precondition */
__CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");
/* Writable Set */
*(&out) = nondet_uint32_t();

/* 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;
/* 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;
}
```
8 changes: 3 additions & 5 deletions doc/cprover-manual/contracts-history-variables.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,7 @@ _ensures_ clause.
### 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.

a parameter of the function. For now, only scalar or pointer types are supported.

### Semantics

Expand All @@ -24,13 +23,12 @@ 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)

int sum(const uint32_t a, const uint32_t b, uint32_t* out)
/* Postconditions */
__CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out)))
/* Writable Set */
__CPROVER_assigns(*out)
{
/* ... */
/* ... */
}
```
71 changes: 35 additions & 36 deletions doc/cprover-manual/contracts-memory-predicates.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,14 +1,13 @@
# 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).
external environment (in a precondition), or returning it to the calling context (in a postcondition).

### Parameters

Expand All @@ -33,12 +32,12 @@ __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;
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;
}
```

Expand All @@ -53,21 +52,21 @@ 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;
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;
__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;
}
```

Expand All @@ -80,11 +79,11 @@ int *err_signal; // Global variable

int foo()
{
uint32_t a;
uint32_t b;
uint32_t out;
sum(a, b, &out);
return *err_signal;
uint32_t a;
uint32_t b;
uint32_t out;
sum(a, b, &out);
return *err_signal;
}
```

Expand All @@ -98,21 +97,21 @@ int *err_signal; // Global variable

int foo()
{
uint32_t a;
uint32_t b;
uint32_t out;
uint32_t a;
uint32_t b;
uint32_t out;

/* Function Contract Replacement */
/* Precondition */
__CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause");
/* 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();
/* 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
/* Postconditions */
__CPROVER_assume(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))); // Assumes out is allocated

return *err_signal;
return *err_signal;
}
```
```
Loading