18-Feb-2015: The first public release of Astraver Toolset
We are happy to announce the first public release of Astraver Toolset 1.0 that is built on top of the 'Frama-C + Jessie + Why3 IDE' deductive verification toolchain. The toolchain was adapted, so it can be used to specify and prove properties of Linux kernel code. The most of our modifications go to the Jessie plugin, while the Frama-C front-end and the Why3 platform have got just minor fixes or improvements. Some of our modifications were already applied upstream, while the rest is available in our public repositories.
The most important modifications are described below.
C Language Support
- Low-level reinterpret type casts between pointers to integral types. This feature required modification of the Jessie memory model as described in our paper "Extended High-Level C-Compatible Memory Model with Limited Low-Level Pointer Cast Support for Jessie Intermediate Language". The overall idea can be summarized as an ability to do certain ghost re-allocations of memory blocks in explicitly specified points in order to transform arrays of allocated objects (structures) from one type to another. WARNING. Discriminated unions support is not yet fully adapted to the modified memory model.
- Prefix type casts between outer structures and their corresponding first substructures (through field inlining and structure inheritance relation in Jessie).
- Kernel memory (de)allocating functions kmalloc()/kzalloc(), kfree().
- Builtin C99 __Bool type.
- Standard library functions memcpy(), memmove(), memcmp() and memset(). The support for these functions is implemented through type-based specialization of several pre-defined pattern specifications. (*)
- Function pointers (through exhaustive may-aliases checking). (*)
- Variadic functions (through additional array argument). (*)
- Inline assembly (through undefined function calls). (*)
- Jessie-specific \offset_min() and \offset_max() constructions support.
- Proxy variables for string literals (with the corresponding invariants on the contents).
- Jessie pragma code annotation for specifying explicit pointer reinterpretations.
To implement support for these small extensions to the ACSL specification language modifications in both Frama-C and Jessie were introduced.
- Composite terms expansion in \assigns clause, i.e. /*@ assigns s;*/, where s has a composite (structure or union) type, is expanded to /*@ assigns s.a, s.b, s.c; */, where a, b and c are the members of the composite type. Similar expansion is also applied to arrays of constant size.
- Weakened precondition of safe pointer comparison for equality: now it requires both pointers to be either in the same block or valid.
- Strengthened precondition of the deallocation function (free): now it requires the argument to have \offset_min == 0.
- Special debugging printers for Jc OO internal representation (work with OCaml debugger). The normal printing functions will fail with segmentation fault due to method invocations (i.e. function pointer calls).
- Different values of sizeof in code vs annotations due to embedded fields transformation.
- Incomplete post- and frame conditions for memory allocation/deallocation operations.
- Incomplete translation of allocates clauses.
- Assigns clause translation for global references.
- Excess dereferences on local immutable variables.
- \valid(p+(a..b)) translation not conformant to the corresponding ACSL specification.
- [Frama-C] "void (*) (void)" type parsing in logic.
- [Frama-C] typeof applied to an expression of a function type (was always treated as function pointer, but should also be compatible with function type).
- [Frama-C] goto statements in complex compound initializers caused failures due to initialization debugging enabled by default (fixed upstream in Neon, but will still likely fail in debug mode).
- [Frama-C] Location information for cast expressions (was missing due to CIL's mkCast without location argument).
- [Frama-C] We treat zero-sized arrays in structures as flexible array members (with no size specified) whereas current Cabs2Cil considers zero array length as an error (although not a fatal one) and recovers from it by setting the length to 1.
- A lot of minor bug fixes.
- We also made some efforts to improve the tool scalability on very large programs (> 10 000 LoC) where only a relatively small part of the original program is actually analyzed (e.g. if a lot of code arises after headers expansion). The scalability is achieved through the elimination of irrelevant globals and unused composite type declarations before applying any Jessie-specific transformations.
- There was also some refactoring of both the Jessie plugin and the Jessie translator. Common module in the Jessie plugin and Why/Why3 output modules (now separated) in the Jessie translator were touched the most. Modified Jessie is built using Ocamlbuild and uses OCaml 4.02 type-level module aliases (instead of packing) to form a library module (Jc).
- Assumption highlighting (different colors for true and false assumptions) that improves usability of the tool. We use heuristic implementation based on location information. When a boolean negation expression has no location information, but the subexpression under the negation does, we consider such expression a negative assumption and highlight it in red (or any other configurable color). This allows better condition highlighting in if, while, and switch statements.
- Another somewhat significant change to the Why3 platform is modified label-to-VC-explanation matching. The problem was that Why3 always used just the last label providing some explanation among those in the set attached to the corresponding VC term. There was, for instance, a sample Why module where the callee function got the explanation attached to its outermost let construct, and the caller function received the (quite meaningless) default general explanation while it already had one provided by the user (in this case the general explanation happened to be the last one). In our modification we merge all the available explanations together still putting the last occurring one first (for compatibility) and separating them by dots. We also also prevent propagation of subterm explanations to the root (function) entries and avoid adding general explanations for VCs that already have user-provided ones. This modified explanations treatment is especially useful for generated *.mlw files with lots of functions, goals and corresponding explanations.
The current release can be installed either via OPAM or manually built from sources available in our public repositories. All the modifications are published under the licenses applicable to their corresponding original files (or in case of newly created files, the tools they were added to).