Commit b0622082 authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'blog-admit-check' into 'master'

[blog] new post about admit/check

See merge request !116
parents 01100b4b de0a434a
Pipeline #35728 passed with stage
in 1 minute and 54 seconds
---
layout: post
author: André Maroneze
date: 2021-06-10 11:00 +0100
categories: ACSL
title: "Admit and check annotations in ACSL"
---
In Frama-C 23 (Vanadium), two new kinds of ACSL annotations are available, to
complement `assert`: the `admit` and `check` annotations.
In a nutshell, `assert P` is equivalent to `check P; admit P`. The former
allows easier checking of the validity of predicates, while the latter
documents the introduction of external evidence into a proof.
In this blog post, we show a few examples where they may be useful, and
also a few pitfalls to avoid.
# `admit`: an `assert` that is *considered valid*
An `admit` annotation in ACSL is the same thing as an `assert` whose status
is *Considered valid* (blue/green bullet in the GUI). It is used in situations
where Frama-C's analyzers cannot prove a given property, such as:
- a proof performed by an external tool;
- a paper proof currently out of reach for Frama-C (e.g., complex mathematical
invariants on floating-point computations, such as some
[nonlinear filters](https://en.wikipedia.org/wiki/Nonlinear_filter));
- the behavior of hardware devices (e.g. registers accessed via absolute
addresses);
- the semantics of inline assembly code;
- the specification of complex external functions, whose behavior is more
easily modeled using a mix of C code and `admit` annotations.
Here's an example where `admit` is useful:
```
void main () {
int a = Frama_C_interval(-20000, 20000);
int b = Frama_C_interval(-20000, 20000);
int r = a*a - 2*a*b + b*b;
//@ admit r >= 0;
}
```
Eva cannot currently prove this property by itself; or, to be more precise:
Eva *can* prove it, using option `-eva-subdivide-non-linear` with a sufficiently
high value, but this might take a long time in practice.
The next best approach, until Frama-C 22, would be to add an `assert` with a
comment telling the user that the property does hold, even if not proven.
This generates unnecessary noise in reports.
With `admit`, the burden of the proof is shifted to the user; just like in Coq
and other tools related to formal proofs, the presence of `admit`s means the
stated property becomes part of the trusted computing base (TCB);
`admit` simply provides a way to clearly document this behavior.
# `check`: evaluate, but do not rely on it
A `check` is the contrapositive of an `admit`: it evaluates the predicate
validity and emits a status, but does *not* rely on it afterwards.
In Eva, for instance, this means the state is *not* reduced.
Therefore, unlike `assert`, `check` does *not* affect the evaluation and can
be inserted without interfering with any analyses.
As an example, consider the effect of adding `assert p != \null` in some code:
it may result in all traces after the `assert` ignoring the case `p == \null`.
While debugging WP proofs, in particular, such annotations may
interfere with the result and complicate understanding; removing them
afterwards can once again alter the result of the weakest precondition calculus.
With `check`s, this never happens; you can always include them during debugging,
to help understand what's going on during WP computation.
# `admit requires`, `admit ensures`, `check requires`, `check ensures`
Both `admit` and `check` can also be used as prefixes to `requires` and
`ensures` clauses; their behavior is changed in the same way as before.
In this case, `check` is used more often; but a clever developer did find
a use for [admit ensures](https://git.frama-c.com/pub/frama-c/-/blob/dc684f951165280d94d450de14e5eb8be7df1040/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.h#L60).
# When `admit` is not the right tool
Note that `admit` does nothing *more* than `assert`; in particular, it
does not allow *introducing* new states and values into an analysis.
For instance, an ACSL beginner's mistake is to try something like the
following code to obtain a non-deterministic range between `min` and `max`:
```
// (Should) return the range of integers between [min] and [max]
int nondet_interval(int min, int max) {
int random;
//@ admit \initialized(random) && min <= random <= max;
return random;
}
```
The reason it does not work is that, according to the semantics of C,
an uninitialized local variable has an indeterminate value which, in ACSL,
can be detected with the `\initialized` predicate. In the above example,
`\initialized(random)` is false, therefore the annotation is equivalent to
`//@ admit \false;`. The blocking semantics of `admit` results in an empty
state (e.g., `BOTTOM` in Eva).
If you want to emulate a function such as `Frama_C_interval` using `admit`,
you may start with a `volatile` variable; in Eva, the semantics of
`volatile int` is "contains any (initialized) integer". However,
the example below will *still* not work:
```
volatile int random;
int nondet_interval(int min, int max) {
//@ admit min <= random <= max;
return random;
}
```
The problem is unrelated to `admit`, however!
The issue is that `random` is still `volatile`, so even after the `admit`
constrained the set of states, the value of `random` may have been changed
(e.g., it could be a register receiving data from the network,
with new data arriving just after the evaluation of the `admit`).
Reading the variable again in the `return random` statement may thus produce
*any* value, including those outside `[min; max]`.
However, if we copy its value into a non-volatile variable, *then*
apply the `admit`, we'll get the desired behavior:
```
volatile int random;
int nondet_interval(int min, int max) {
int r = random;
//@ admit min <= r <= max;
return r;
}
```
This function does return a value between `min` and `max`, without emitting
any *Unknown* statuses. It's not very useful (you should prefer using
`Frama_C_interval` for such situations, since it is already provided in
Frama-C's `__fc_builtin.h` header), but it illustrates a use case for `admit`.
# Conclusion
The new ACSL annotations, `admit` and `check`, split `assert`'s functions
into fine-grained parts, allowing for better documentation of external
semantics and improving debugging of ACSL clauses.
The behavior of `assert` can be described as `check` + `admit`:
*to evaluate a predicate and emit a status* (`check`), and then *to reduce the
set of states after the annotation to those verifying the predicate* (`admit`).
They also work with `requires` and `ensures`: `requires` is equivalent to
`check requires` followed by `admit requires`; idem for `ensures`.
# Acknowledgments
This blog post incorporates suggestions and kind reviews by:
Michele Alberti, Patrick Baudin, David Bühler, Maxime Jacquemin,
Valentin Perrelle, Julien Signoles.
Markdown is supported
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