Annotation Generation

Purpose

Writing code without specifying its expected behavior is the best way to ensure unreliability and poor re-usability of the provided program.

Contracts have been introduced in order to provide a theoretical background for specification of programs. Contracts are mostly used for designing systems by giving its expected semantics. This semantics, while expressed using formal notations/languages, can be checked for correctness.

In our approach we generate implementation code from models. This code is highly idiomatic and we propose that as soon as we have a formal specification of the blocks, we can generate annotations in additions to the generated code in order to translate the block semantics into contracts on C code. These annotations will then be used for formal checking of the code correctness according to the provided specification.

Overview of the approach

ACSL annotations

The ACSL property specification language is a behavioral specification language for C programs. It is semantically close to JML and the CADUCEUS code analyser from the WHY project.

ACSL annotations are classical comments for C code where the starting characters ( // or /* ) are postfixed by an @ character.

Beside the fact that these annotations are in comments, they are based on a formal language and can be used by external programs. These annotations does not change the execution or the semantics of the original program.

Theoretical background

  • Hoare logic

Based on Hoare logic, ACSL annotations can be used as a language for specification of C code intended behavior.

Hoare logic is a set of formal rules for reasoning about the correctness of a computer program. The central construct used with Hoare logic is the Hoare triple. They are used in order to specify the memory modification implied by the computation of a block of code. Hoare triples are usually represented as

\[\{P\} C \{Q\}\]

P and Q are assertions and C is a command (block of code). This notation represent that if the memory state of the system is P (P assertion is evaluated to true) and the computation C is done (we execute C. Then the memory state of the system will be Q (Q is then evaluated to true). In the context of the computation C, P are pre-conditions and Q are post-conditions.

Hoare logic is a relational calculus where for each Q there are many possible P and for each P there are many possible Q.

\[\begin{split}&\exists n \in \mathbb{N}, \forall i \in [1..n], \{P_i\} \mathcal{C} \{Q\}\\ &\exists m \in \mathbb{N}, \forall j \in [1..m], \{P\} \mathcal{C}\{Q_j\}\end{split}\]
  • Weakest pre-condition calculus

Weakest Pre-condition (WP) is a functional calculus version of Hoare logic. For S and Q there is exactly one possible P and this P will imply all the others P seen in the Hoare logic part.

\[\begin{split}\exists n \in \mathbb{N}, \forall i \in [1..n], \{P_i\} \mathcal{C} \{Q\} &\land \exists p \in [1..n], \forall k \in [1..n] \land k\not=p,\\ \{P_k\} &\Rightarrow \{P_p\}\end{split}\]

The WP calculus is often written as \(P = wp(C,Q)\).

Tooling

  • Frama-C

The Frama-C tool is a framework made of plugins allowing to perform various source code analysis. These analysis are based on static analysis and allow to extract informations from the source code like metrics (control structure deepness, number of static allocations, ...), variables value origin analysis, dead code detection. A more detailed list of the tool provided analysis can be found on the editor web site.

This tool has the particularity of being correct and complete regarding its specification. Thanks to this, some of his extensions (plugins) allow to do formal verification on the code.

By using the WP plugin, we can analyse C code. This plugin implements a weakest pre-condition calculus based on ACSL annotations on a C code. It will generate proof obligations for each ACSL annotation that will be verified in proof assistants (Coq, ISABELLE or PVS) or automated tools supported by the WHY tool.

Using automated theorems provers, the user is not necessary a expert formal methodist but can therefore prove the correctness of a piece of code. This usage is well suited to our approach as we target users that do not have the knowledge or the time to learn to use tools like Coq.

GeneAuto prototype

An implementation of the approach has been prototyped and tested based on the GeneAuto automatic code generator. This experiment has been done in order to prove the feasibility of the approach on real (small scale for the moment) use cases.

Overview of the tool process

As in the original GeneAuto tool, for each block a backend must be provided in order to generate the statements for the block code generation. The GAVAMetamodel provides a new set of statements for annotation writing.

When the code generator developer codes its backend, he must provide the necessary annotation constructs. These annotations constructs are then processed by the verificationAnnotationGenerator tool.

GAVA metamodel

Documentation for the GAVA metamodel can be found on the GeneAuto metamodel with verification annotations documentation page.

Implementation

At first reading the section can be omitted as it contains only technical documentation about a prototype implementation.

These informations can be found on the GeneAuto annotation generation extension process page.

VerificationAnnotationGenerator tool

This tool will process the annotations provided in the backend. It will generate automatically certain idiomatic annotations (e.g. loop variants and invariants based on loops bounds).

This tool is also used for the processing of specific annotation purpose blocks.

Detailed informations can be found on the GeneAuto annotation generation extension process page.

AnnotationBlocks

Specific annotation simulink blocks have been conceived in order to manage high level annotations on systems.

  • VAMux block

    This block is used to declare annotation variables taking system variables as input. The output of this block will be a matrix of some elements (values) of the system to be used in annotations.

  • Ellipsoid block

    This block is used for expressing stability properties on the system. Typically, a set of values is taken from the system, grouped by using a VAMux block, and then processed in an ellipsoid calculus. This is based on the Lyapunov works on system stability. This is based on the Lyapunov stability work and is experimented by GeorgiaTech team.

For each of these blocks two classes have been written. One is a backend holding the annotation elements generated for each block ( geneauto.blocklibrary/src/geneauto.blocklibrary.backends.vabackends). The other is a typer holding type inference rules (geneauto.blocklibrary/src/geneauto.blocklibrary.typers.vatypers). More detailed documentation can be found on the GeneAuto annotation generation extension process page.

CPrinter

The printing tool provided in GeneAuto has been extended in order to print annotations on the code. This (mostly non-intrusive) modification is necessarily done on the printer tool as the printing of the annotations must be done -according to the annotation type- before or after the statement printing.

Mode informations can be found on the GeneAuto annotation generation extension process page.

Evolution of the approach

This approach was a first prototype. The next phase of the implementation relies on an abstraction of the annotation block principle by providing a specification of an annotation block by using the BlockLibrary specification approach documented in BlockLibrary Meta-model. This annotation block specification is given in the Annotation blocks transformation page.

Examples

We provide here an example of model for which we experiment the code generation. The model is here detailed and has been model using Simulink. The corresponding code was generated using GeneAuto extended with formal annotation generation.

For this example, we provide the simulink model, a graphical representation and the corresponding generated code.