18-Feb-2015: The first public release of Astraver Toolset

user warning: Got error 28 from storage engine query: SELECT t.*,v.weight AS v_weight_unused FROM term_node r INNER JOIN term_data t ON r.tid = t.tid INNER JOIN vocabulary v ON t.vid = v.vid WHERE r.vid = 247 ORDER BY v.weight, t.weight, t.name in /opt/drupal-6.38/modules/taxonomy/taxonomy.module on line 640.
Submitted by Mikhail Mandrykin on Wed, 18/02/2015 - 14:30

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). (*)

(*)The main purpose of implementing support for these features was the ability to use the tools on our target code without the need for its significant preliminary modification. As a result the support is not complete enough to be usable for verification of code that significantly relies on these features. For instance:

  • memset() function is used only for zero initialization and the resulting VCs can be incomplete (e.g. for structures with final flexible array members);
  • there is an assumption that function pointer variables can only have values from the set of all functions declared in the context of analysis (like in a properly registered kernel module), otherwise some proof obligations can become unprovable;
  • support for verification of variadic functions can be incomplete or very awkward in some cases (in our code such functions are used for debug printing and logging purposes only, so we mostly ignore them for now);
  • inline assembly should only be present in actually unused or unreachable code, or for purposes that are not currently subject to verification (e.g. memory barriers or atomic blocks).

ACSL Extensions

  • 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.

Jessie Improvements

  • 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).

Bugs Fixes

  • 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.

Scalability

  • 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.

Jessie2 Refactoring

  • 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).

Why3 Improvements

  • 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).