Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Astraver Toolset 1.0

  • Subject: [Frama-c-discuss] Astraver Toolset 1.0
  • From: khoroshilov at ispras.ru (Alexey Khoroshilov)
  • Date: Thu, 19 Mar 2015 12:21:03 +0300
Dear colleagues,

We have finally published our improvements in Frama-C-Jessie2-Why3
toolchain that were made within AstraVer project [1].
The purpose of the modifications is to be able to verify Linux kernel
space code.
The most of the improvements are in Jessie plugin and just a few of them
touches Frama-C or Why3.

Please find short description of the most important modifications 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.
-- The only other somewhat significant change to the Why3 platform is
modified label-to-VC-explanation matching. An example of a confusing
rendering of explanations is attached in file
"label_explanation_matching.mlw". The corresponding screenshot is
attached in "expls-original2.png". It shows that the explanation for the
first let construct was considered the explanation for the whole
explanation_matching_callee function and for the caller function the
user-provided explanation "Caller" was overridden by the standard
general explanation "VC for ...". The problem is that Why3 always used
just the last label providing some explanation among those in the set
attached to the corresponding VC term. For the callee function this
turned out to be the explanation attached to the let construct, and for
the caller function that received an additional general explanation in
addition to the one provided by the user, the general explanation
happend to be the last one. In our modification we merge all the
available explanations together still putting the last occurring one
first and separating them by dots, and also prevent propagation of
subterm explanations to the root (function) entries
("multiple_explanations.patch"). We also avoid adding general
explanations for VCs that already have user-provided ones
("redundant_explanations.patch"). This gives the result shown in
"expls-patched2.png". This modified explanations treatment are
especially useful for generated *.mlw files with lots of functions,
goals and corresponding explanations (e.g. "expls-patched3.png").

The current version of the modified tools can be installed either via
OPAM [2] or manually built from sources available in our public
repositories [3].

All the modifications are published under the same license as the
original tool has. Feel free to cherry-pick any or all of them.

[1] http://linuxtesting.org/astraver
[2] http://forge.ispras.ru/projects/astraver/wiki#Using-OPAM
[3] http://forge.ispras.ru/projects/astraver/wiki#Our-Repositories

--
Best regards,
Mikhail Mandrykin
Alexey Khoroshilov
Linux Verification Center, ISPRAS
web: http://linuxtesting.org

-------------- next part --------------
A non-text attachment was scrubbed...
Name: expls-original2.png
Type: image/png
Size: 423873 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150319/f848e631/attachment-0003.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: expls-patched2.png
Type: image/png
Size: 422941 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150319/f848e631/attachment-0004.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: expls-patched3.png
Type: image/png
Size: 545324 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150319/f848e631/attachment-0005.png>
-------------- next part --------------

module Explanation_matching
  use import ref.Ref
  use import int.Int

  let explanation_matching_callee "expl:Callee" (arg1 : int) (arg2 : int) : int
    requires { "expl:Requires"
                 ("expl:First conjunct" arg1 = 0) /\
                  "expl:Second conjunct" arg2 = 0 }
    ensures { "expl:Ensures"
                ("expl:First conjunct" result <= 0) /\
                 "expl:Second conjunct" result >= 0 }
  =
    let a = ref arg1 in
    "expl:Let"
    let b = ref arg2 in
    assert { "expl:Assertion"
               ("expl:First conjunct" !a = 0) /\
               ("expl:Second conjunct" !b <= 0) /\
                "expl:Third conjunct" !b >= 0 };
    !a


  let explanation_matching_caller "expl:Caller" (arg1 : int) : int
    requires { "expl:Requires"
                 ("expl:First conjunct" arg1 >= 0) /\
                  "expl:Second conjunct" arg1 <= 0 }
    ensures { "expl:Ensures"
                ("expl:First conjunct" result <= 0) /\
                 "expl:Second conjunct" result >= 0 }
  =
    explanation_matching_callee arg1 arg1
end
-------------- next part --------------
A non-text attachment was scrubbed...
Name: multiple_explanations.patch
Type: text/x-patch
Size: 2466 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150319/f848e631/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: reduntant_explanations.patch
Type: text/x-patch
Size: 2144 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150319/f848e631/attachment-0003.bin>