Commit 8f2a7ad8 authored by cqs7520's avatar cqs7520
Browse files

Adds cheat sheet.

parents
# VCC Cheat Sheet
for Applied Verification of C Programs
by Julius Tonner
Version 0.1 - May 28, 2021
---
## Common Mistakes
- Are your pointers disjoint?
- Have you ensured postconditions for all possible results?
- Have you ensured postconditions for data you are not modifying?
- Do you have stated all loop invariants?
## Logic
### `\true`, `\false`
Boolean literals.
### `&&`, `||`, `!`
Conjunction (and), Disjunction (or), Negation (not).
### `==>`
Logical implication.
```
\false ==> 0 == 1
```
### `<==>`
Logical equivalence.
```
12 > 7 <==> 7 < 12
```
### `\forall type a, b; condition`
Universal quantification.
Is true when `condition` is true for all valuations of the declared variables.
```
\forall unsigned i; i > 0
```
```
\forall int p, q; p == q <==> p >= q && p <= q
```
### `\exists type a, b; condition`
Existential quantification.
Is true when `condition` is true for at least one valuation of the declared variables.
```
\exists unsigned i; i == 42
```
```
\exists short s, t; s - t < 0
```
## Contracts
### `_(assert condition)`
Assertion.
Verification fails when `condition` does not hold.
If `condition` holds, the verifier can use it to verify subsequent code.
```
void foo()
{
_(assert 0 <= d && d < 10)
}
```
### `_(assume condition)`
Assumption.
Lets the verifier use `condition` to verify subsequent code even though the condition might not actually be true.
Assuming a contradictory condition (e.g. `\false`) will let all subsequent code pass verification.
```
void foo()
{
time_t t = time();
struct tm *ti = localtime(&t);
int y = ti->tm_year + 1900;
_(assume 1900 <= y && y < 2000)
// We'll never need more than two digits to store the year part of a date.
}
```
### `_(invariant condition)` (Loop Invariant)
Verification fails if `condition` does not hold at the beginning of at least one of the loop runs.
If a variable is changed in the loop, the loop invariants are the only things the verifier knows about it in and after the loop.
```
int arr[10];
for (unsigned i; i < 10; i++)
_(invariant \forall unsigned j; j < i ==> arr[j] == 42)
{
arr[i] = 42;
}
_(assert \forall unsigned j; j < 10 ==> arr[j] == 42)
```
### `_(requires condition)`
Precondition.
Verification fails if `condition` is not true when the function is called.
Lets the verifier use `condition` to verify subsequent code.
```
int abs(int i)
_(requires i != INT_MIN)
{
return i >= 0 ? i : -i;
}
void foo()
{
abs(-42); // Cool.
abs(-2147483647) // Not cool.
}
```
### `_(ensures condition)`
Postcondition.
Verification fails if `condition` does not hold at the end of the function.
Lets the verifier use `condition` after the function has been called.
```
int positive()
_(ensures \result > 0)
{
return 5;
}
void foo()
{
int i = positive();
_(assert i >= 1)
}
```
### `_(maintains condition)`
Equivalent to `_(requires condition) _(ensures condition)`.
### `\result`
Refers to the return value of a function.
```
_(ensures \result == 42)
```
### `_(returns x)`
Equivalent to `_(ensures \result == x)`.
### `\old(x)`
Refers to the value of `x` when the function was called.
```
void foo(int x)
// [...]
{
x++;
_(assert x == \old(x) + 1)
}
```
### `\same(x)`
Equivalent to `x == \old(x)`.
## Assisting Verification
### `_(ghost statement)`
`statement` is executed by the verifier only, not during runtime of the compiled program.
It is used to calculate "meta"-information for reasoning about the code.
"Real" code can influence ghost code but not vice versa.
```
int i = 21;
_(ghost int I = i)
_(ghost I *= 2)
_(assert I == 42 && i == 21)
```
### `_(unchecked)(expression)`
Ignores arithmetic overflows in `expression`.
Usually, a programs' correctness depends on computer arithmetic behaving exactly like ordinary arithmetic, but in some special cases (e.g. hash computation), overflow is desired.
```
unsigned zero = _(unchecked)(UINT_MAX + 1);
```
## Framing, Type Invariants, Ownership
### `_(writes x)`
States that a function wants to write to the contents of the set of pointers `x`.
Can also be used with multiple arguments: `_(writes x, y, z)`.
```
void set_zero(int *p)
_(writes p)
// [...]
{
*p = 0;
}
```
### `_(pure)`
States that a function does not modify the heap (i.e. does not have side effects, is a pure function).
The result of the function only changes if the inputs or the values the function reads change.
```
_(pure) int max(int a, int b)
{
return a > b ? a : b;
}
```
### `_(reads x)`
States that a _pure_ function wants to read the contents of the pointers x and y (on the heap) and therefore might change its value when the contents of x or y change.
Can also be used with multiple arguments: `_(reads x, y, z)`.
Does not apply to non-pure functions.
```
_(pure) bool value_equal(Foo *a, Foo *b)
_(reads a, b)
// [...]
{
return a->value == b->value;
}
```
### `\array_range(array, length)`
Refers to all the `length` elements of `array` as a set of pointers. Equivalent to `&array[0], &array[1], ..., &array[length - 1]`.
```
void foo(int *arr, unsigned len)
_(writes \array_range(arr, len))
{
// [...]
}
```
### `\disjoint(x, y)`
Holds if `x` and `y` are non-overlapping sets of pointers.
```
\disjoint(\array_range(a, n), \array_range(b, m))
```
### `_(invariant condition)` (Type Invariant)
Verification fails if `condition` does not hold when the struct object is wrapped.
If the struct object is known to be in the wrapped state, its invariants hold.
```
struct Amount
{
int amount;
_(invariant LOWER_LIMIT <= amount && amount <= UPPER_LIMIT)
};
```
### `\inv(x)`
Refers to the type invariant of `x`.
```
void wrap(Foo *foo)
_(requires \inv(foo))
// [...]
{
_(wrap foo)
}
```
### [`\mine(x)`](https://knowyourmeme.com/memes/mine-mine-mine-seagulls)
Holds if the current struct owns `x`.
Required for admissibility if a type invariant depends on the contents of `x`.
```
typedef struct _Foo {
int *p;
_(invariant \mine(p))
_(invariant 0 <= *p && *p <= 42)
} Foo;
```
### `\this`
Refers to the struct object within a type invariant.
```
typedef struct _Foo {
int value;
_(invariant \this->value == 42)
} Foo;
```
### `\owns`
Refers to the set of structs a struct owns.
Use `=`, `+=` and `-=` to modify the set.
### `_(wrap x)`
Transfers `x` from mutable to wrapped state.
The type invariants of `x` are checked and will hold subsequently.
```
Foo *new_foo(int value)
// [...]
{
Foo *foo = (Foo*) malloc(sizeof(Foo));
// [...]
foo->value = value;
_(wrap foo)
return foo;
}
```
### `_(unwrap x)`
Transfers `x` from wrapped to mutable state.
The type invariants of `x` do not need to hold anymore.
```
void change_value(Foo *foo, int value)
// [...]
{
_(unwrap foo)
foo->value = value;
}
```
### `_(unwrapping x) { statements }`
Equivalent to `_(unwrap x) { statements } _(wrap x)`.
### `\thread_local(x)`
Holds if the current thread owns `x`.
The contents of `x` can safely be read only if `\thread_local(x)` holds.
```
unsigned is_zero(int *p)
_(requires \thread_local(p))
{
return *p == 0;
}
```
### `\wrapped(x)`
Holds if `x` is owned by the current thread (implies `\thread_local(x)`) and its type invariants hold.
```
void foo(Bar *bar)
_(requires \wrapped(bar))
{
// [...]
}
```
### `\mutable(x)`
Holds if `x` is owned by the current thread (implies `\thread_local(x)`) and is mutable (the type invariants of `x` do _not_ need to hold).
```
void foo(int *p)
_(requires \mutable(p))
// [...]
{
*p = 42;
}
```
### `\mutable_array(array, length)`
Holds if `array` points to memory for `length` elements of its element type.
```
void set_zero(int *arr, unsigned len)
_(requires \mutable_array(arr, len))
// [...]
{
for (unsigned idx = 0; idx < len; idx++)
arr[idx] = 0;
}
```
### `\nested(x)`
Holds if `x` is not owned by the current thread.
The type invariants of `x` hold.
In a sequential program, `x` cannot change.
### `\fresh(x)`
Holds if `x` did not exist on the heap prior the calling the function.
```
int *new_int()
_(ensures \fresh(p))
{
int* p = (int*) malloc(sizeof(int));
// [...]
return p;
}
```
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment