ETH LIbrary for Numerical Analysis

ELINA contains optimized implementations of popular numerical abstract domains such as Polyhedra, Octagon and Zones for static analysis. ELINA uses improved algorithms, online decomposition as well as state of the art performance optimizations from linear algebra such as vectorization, locality of reference, scalar replacement etc. to significantly improve the performance of static analysis with the numerical domains.

News

21 Mar 2018: Python Interface for the Octagon domain added.
15 Jan 2018: Limited support for Zonotope transformers added.
05 Dec 2017: Faster implementation of Polyhedra domain based on POPL'18 paper released.
24 Nov 2017: Added support for the Zones domain.
03 Aug 2017: Improved precision for Polyhedra transformers in case of integer overflow.
15 Feb 2017: Added Java interface based on APRON.
31 Jan 2017: Added OCaml interface based on APRON.
23 Jan 2017: Added support for APRON interface.
15 Jan 2017: Added support for fold and expand transformers for Polyhedra.
28 Nov 2016: Source code for Polyhedra and Octagon domain released.

Download

The source code for ELINA is available on Github using the link below.

Github

We also provide a tar file containing latest compressed source code here.

Documentation

Requirements

The installation is preferable for Linux 64-bit. Make sure you have latest version of gcc and g++. Install the following libraries.

GNU m4

  • sudo apt-get install m4
  • GMP

  • Download the tar file from https://gmplib.org/.
  • Extract the source.
  • Go to the gmp folder and run:
    • ./configure --enable-cxx
    • make
    • make check
    • sudo make install
  • This will install the gmp library in "/usr/local" folder.
  • GNU MPFR

  • Download the tar file from http://www.mpfr.org/
  • Extract the source.
  • Go to the mpfr folder and run:
    • ./configure
    • make
    • make check
    • sudo make install
  • This will install the mpfr library in "/usr/local" folder.
  • Compiling and installing

    ELINA uses Intel's Vector Instructions for improving the performance of the Octagon and Zones domain. ELINA also supports backward compatibility with APRON so that existing analyzers using APRON can benefit from ELINA with minimal changes. We also provide Python interface as well as OCaml and Java interface based on APRON. For Python interface, make sure you have at least Python 3.4.

  • Run "./configure". The ocaml and java support are disabled by default. Both are accessed using the APRON API. To use the apron API, specify "./configure -use-apron". To enable java and ocaml support, add "-use-ocaml" and "-use-java" options. Type "./configure -help" for more configuration options.
  • Check if your machine supports SSE or AVX as follows:
    • For Linux: Run "cat /proc/cpuinfo | grep "sse\|avx””, For Mac: Run “sysctl -a | grep machdep.cpu.features”.
    • Check for strings "sse", "avx" in output.
  • To compile the library:
    • If your computer supports AVX
      • run "make IS_VECTOR=-DVECTOR" to compile the source.
      • This will use AVX vectorized transformers for the Octagon and Zones domain.
    • Else if your computer supports SSE
      • run "make IS_VECTOR=-DVECTOR IS_SSE=-DSSE" to compile the source.
      • This will use SSE vectorized transformers for the Octagon and Zones domain.
    • Else run "make". This will use scalar transformers for the Octagon and Zones domain.
  • For 32-bit systems, disable the architecture specific flags (m64, march=native etc. ) and DTIMING in DFLAGS.
  • ELINA can be installed by running "sudo make install".
  • Running the Library

    The library can be used directly from C.

    Polyhedra

    Create the manager for the Polyhedra domain as follows:

                                    elina_manager_t * man = opt_pk_manager_alloc(false);

  • The file "elina_test_poly.c" contains examples for calling Polyhedra transformers such as Join, Meet and more. The file requires two integer arguments:
    • dim: number of variables in the created Octagons
    • nbcons: number of constraints used to create input Octagons for various transformers
  • The function "opt_pk_manager_alloc" in the file "opt_pk_internal.c" contains list of supported Polyhedra transformers.
  • Octagon

    Create the manager for the Octagon domain as follows:

                                    elina_manager_t * man = opt_oct_manager_alloc();

  • The file "elina_test_oct.c" contains examples for calling Octagon transformers such as Join, Meet and more. The file requires same arguments as for the Polyhedra domain.
  • The function "opt_oct_manager_alloc" in the file "opt_oct_representation.c" contains list of supported Octagon transformers.
  • Zones

    Create the manager for the Zones domain as follows:

                                    elina_manager_t * man = opt_zones_manager_alloc();

  • The function "opt_zones_manager_alloc" in the file "opt_zones_representation.c" contains list of supported Zones transformers.
  • OCaml interface

  • Make sure APRON's ocaml interface is installed.
  • We provide a test file "mlexample.ml" showing how to access the OCaml interface.
  • Type "ocamlrun mlexample.byte" to run the tests.
  • Java interface

  • Make sure APRON's java interface is installed.
  • We provide a test file "Test.java" showing how to access the Java interface.
  • Type "java -Djava.library.path=PATH_TO_INSTALLED.so elina.Test" to run the tests.
  • Python interface

  • We currently support Octagon domain with the Python interface.
  • We provide a test file "tests/elina_oct_test.py" showing how to access the Python interface.
  • Type "python elina_oct_test.py (dim) (nbcons) " to run the file. The two integer arguments have the same meaning as for the C interface.
  • Publications


    Fast Numerical Program Analysis with Reinforcement Learning
    Gagandeep Singh, Markus Püschel, Martin Vechev
    CAV 2018
    Paper
    A Practical Construction for Decomposing Numerical Abstract Domains
    Gagandeep Singh, Markus Püschel, Martin Vechev
    ACM POPL 2018
    Paper Talk
    Fast Polyhedra Abstract Domain
    Gagandeep Singh, Markus Püschel, Martin Vechev
    ACM POPL 2017
    Paper Slides Promo Talk
    Making Numerical Program Analysis Fast
    Gagandeep Singh, Markus Püschel, Martin Vechev
    ACM PLDI 2015
    PDFPaper Slides PDFPromo

    Performance

    We selected a number of realistic programs as benchmarks including linux device drivers from software verification competition. These benchmarks were analyzed using published analyzers including SeaHorn, DPS, TouchBoost, DIZY and CPAchecker. We compare speedup for ELINA over APRON for the end-to-end Octagon analysis. For the Polyhedra analysis, we compare ELINA against both APRON and Parma Polyhedra Library (PPL). PPL and APRON do not finish on some benchmarks either due to timeout after 4 hours or they run out of memory, we provide a conservative lower bound in such cases. The benchmarks which do not finish with APRON have ^ and those with PPL have * as superscript.

    Speedup for Octagon

    Speedup for Polyhedra

    Team


    Gagandeep Singh

    Gagandeep Singh

    PhD Student
    Department of Computer Science
    ETH Zurich
    Website

    Martin Vechev

    Martin Vechev

    Professor
    Department of Computer Science
    ETH Zurich
    Website

    Markus Puschel

    Markus Püschel

    Professor
    Department of Computer Science
    ETH Zurich
    Website