Wiki » History » Revision 16
Revision 15 (Grigoriy Volkov, 09/17/2018 01:30 PM) → Revision 16/27 (Mikhail Mandrykin, 03/29/2019 06:04 PM)
h1. AstraVer Toolset AstraVer Toolset is built on top of 'Frama-C + AstraVer Jessie plugin + Why3' deductive verification toolchain, so it can be used to prove properties of Linux kernel code. *AstraVer* *Jessie2* is a successor fork of the "Jessie":http://krakatoa.lri.fr/ Jessie plug-in for "Frama-C":http://www.frama-c.com/ Frama-C that allows deductive verification of C programs annotated with "ACSL":http://frama-c.com/acsl.html and is primarily targeted at source code of Linux kernel modules. modules source code. It uses the language and tools of the "Why3 verification platform":http://why3.lri.fr/. Unlike original Jessie, AstraVer Jessie2 is not distributed as a part of the "Why2 verification platform":http://why.lri.fr/ and is compiled/installed separately. *Note*: This For now, this fork requires modified version of the __Frama-C__ source code analysis platform, that is based on the @Argon (18.0)@ @Chlorine 20180501@ version of the original platform. h2. Installation h3. Using OPAM * Install recommended OPAM external (system) dependencies — @gcc@, @m4@, @make@, @git@. For example, on Ubuntu: <pre><code class="bash"> sudo apt-get install gcc m4 make git </code></pre> * Install "OPAM":https://opam.ocaml.org/ as described in on the OPAM "documentation":https://opam.ocaml.org/doc/Install.html. For example (installing to @/usr/local/bin@ unsing the binary installer): <pre><code class="bash"> wget https://raw.githubusercontent.com/ocaml/opam/master/shell/install.sh https://raw.github.com/ocaml/opam/master/shell/opam_installer.sh sh install.sh chmod +x opam_installer.sh sudo ./opam_installer.sh /usr/local/bin </code></pre> * Initialize OPAM to use the OCaml @4.07.1@ compiler. On Ubuntu you can use @--disable-sandboxing@ to avoid installation of "bubblewrap":https://github.com/projectatomic/bubblewrap, although this is not recommended. 4.06.0 compiler: <pre><code class="bash"> opam init -c 4.07.1 --disable-sandboxing --comp 4.06.0 eval `opam config env` </code></pre> * Configure current shell environment to use the newly created OPAM switch (may not be needed if OPAM shell hooks were installed successfully during @opam init@): Install "Git":http://git-scm.com/. For example on Ubuntu: <pre><code class="bash"> eval $(opam env) sudo apt-get install git </code></pre> * Add ISPRAS OPAM repository at @https://forge.ispras.ru/git/astraver.opam-repository.git#astraver@ @https://forge.ispras.ru/git/astraver.opam-repository.git@ with AstraVer Jessie2 and modified Frama-C v18.0 Chlorine packages to the OPAM installation (@ispras@ is just an arbitrary name of the new repository): <pre><code class="bash"> opam repo add ispras https://forge.ispras.ru/git/astraver.opam-repository.git#astraver https://forge.ispras.ru/git/astraver.opam-repository.git opam update </code></pre> * Install OPAM @depext@ plug-in for easy extraction and installation of external (system) dependencies for OPAM packages: the Jessie2 and Frama-C build i.e. Autoconf, Gtk2 development files and M4. Ubuntu example: <pre><code class="bash"> opam sudo apt-get install depext $(opam install -e ubuntu jessie2) </code></pre> * Install external dependencies for (Temporary workaround) Build and install an older version of the AstraVer and Frama-C jingoo dependency to avoid a build e. g. Gtk2 development files: error: <pre><code class="bash"> opam depext astraver install -j 1 jingoo.1.2.17 </code></pre> * Build and install the AstraVer Jessie2 plugin for Frama-C with OPAM (the patched versions of Frama-C and Why3 platforms itself will be built and installed automatically). One can use the @-j@ option to speed-up compilation on a multi-core machine: <pre><code class="bash"> opam install astraver -j 1 jessie2 </code></pre> * Build and install either original or patched (search in task view, empty theory filtering) version of the Why3 verification platform: <pre><code class="bash"> sudo apt-get install $(opam install -e ubuntu why3) # Install GMP (external dependency) on Ubuntu opam install -j 4 why3 </code></pre> * The one using AstraVer Jessie would also likely need SMT solvers e.g. "Alt-Ergo":http://alt-ergo.ocamlpro.com/ (also "Z3":https://github.com/Z3Prover/z3, "CVC4":http://cvc4.cs.stanford.edu/web/ "CVC4":http://cvc4.cs.nyu.edu/web/ and others). Alt-Ergo can be installed via OPAM: <pre><code class="bash"> opam install alt-ergo altgr-ergo </code></pre> * The Why3 IDE should be configured initialized to detect available provers (and plugins): <pre><code class="bash"> why3 config --detect-provers --detect-plugins </code></pre> h2. Our Repositories * "AstraVer":/projects/astraver/repository "Jessie2":/projects/astraver/repository (@git clone https://forge.ispras.ru/git/astraver.git@) https://forge.ispras.ru/git/astraver.jessie2.git@) has the following branches: -- "@18.0@":/projects/astraver/repository/ "@20180501@":/projects/astraver/repository/jessie2?utf8=✓&rev=20180501 -- references the latest released version of the AstraVer Jessie2 plugin (currently `@alpha3.20180501@') * "QA":/projects/astraver/repository/qa (@git clone https://forge.ispras.ru/git/astraver.qa.git@) is a submodule of the "AstraVer":/projects/astraver/repository "Jessie2":/projects/astraver/repository repository. It contains several new test sets and the corresponding new testing script (in OCaml) that is based on the "Why3 proof replayer":http://why3.lri.fr/doc/manpages.html#sec62. replayer":http://why3.lri.fr/doc-0.87.2/manual007.html#sec56. * "Frama-C":/projects/astraver/repository/framac (@git clone https://forge.ispras.ru/git/astraver.frama-c.git@) has two branches: -- "@master@":/projects/astraver/repository/framac -- this is a dummy branch with each commit corresponding to an upstream release of Frama-C starting from "@Sodium 20150201@" (commit:framac|1db5542e) -- "@18.0@":/projects/astraver/repository/framac?utf8=✓&rev=18.0 "@20180501@":/projects/astraver/repository/framac?utf8=✓&rev=20180501 -- references patched version of Frama-C @Argon v18.0@ @Chlorine 20180501@ required by the latest AstraVer Jessie2 (@alpha3.20180501@) with some significant changes (wrap-around annotations and logic operations on bounded integers, annotation importing -- an order-independent merging of annotations from several C source files) * "Why3":/projects/astraver/repository/why3 (@git clone https://forge.ispras.ru/git/astraver.why3.git@) has two branches: -- "@master@":/projects/astraver/repository/why3 -- a periodically updated mirror of the INRIA official Why3 Git repository's "master branch":https://gitlab.inria.fr/why3/why3 branch":https://gforge.inria.fr/scm/browser.php?group_id=2990 -- "@bv_and_lemma_functions_stable-4.07@":/projects/astraver/repository/why3?utf8=✓&rev=bv_and_lemma_functions_stable-4.07 "@bv_and_lemma_functions_stable-4.06@":/projects/astraver/repository/why3?utf8=✓&rev=bv_and_lemma_functions_stable-4.06 -- patched version of the Why3 platform (version 0.87.3) with several small unmerged changes * "OPAM-repository":/projects/astraver/repository/opam-repository (@git clone https://forge.ispras.ru/git/astraver.opam-repository.git@) is the above mentioned OPAM repository