ETH LIbrary for Numerical Analysis

ELINA contains optimized implementations of popular numerical abstract domains such as Polyhedra and Octagons 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

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 operators 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

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 domain. ELINA also supports backward compatibility with APRON so that existing analyzers using APRON can benefit from ELINA with minimal changes. Specify the install locations of GMP, MPFR and APRON (for APRON interface) libraries in Makefile.config.

    We also provide OCaml and Java interface based on APRON. For compiling the OCaml and Java interface with APRON, specify the location of APRON root directory in the APRON_SRCROOT variable in Makefile.config. For Ocaml interface set HAS_OCAML and HAS_OCAMLOPT flags in Makefile.config to 1. Similarly, for java interface set HAS_JAVA to 1. Additionally, specify the location of "jni.h" file in JNIINC variable in Makefile.config and the locations of "japron.jar" and "gmp.jar" in the CLASSPATH variable in java_interface/Makefile.

  • Check if your machine supports SSE or AVX as follows:
    • Run "cat /proc/cpuinfo | grep "sse\|avx"".
    • 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 operators for the Octagon domain.
    • Else if your computer supports SSE
      • run "make IS_VECTOR=-DVECTOR IS_SSE=-DSSE" to compile the source.
      • This will use SSE vectorized operators for the Octagon domain.
    • Else run "make". This will use scalar operators for the Octagon domain.
    • For APRON (OCaml, Java) interface, set IS_APRON=-DHAS_APRON in Makefile.config.
  • 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 library as follows:

                                    elina_manager_t * man = opt_pk_manager_alloc(false);

  • The file "elina_test_poly.c" contains examples for calling Polyhedra operators such as Join, Meet and more.
  • The function "opt_pk_manager_alloc" in the file "opt_pk_internal.c" contains list of Polyhedra operators.
  • Octagon

    Create the manager for the Octagon library as follows:

                                    elina_manager_t * man = opt_oct_manager_alloc();

  • The file "elina_test_oct.c" contains examples for calling Octagon operators such as Join, Meet and more.
  • The function "opt_oct_manager_alloc" in the file "opt_oct_representation.c" contains list of Octagon operators.
  • OCaml interface

  • We provide a test file "mlexample.ml" showing how to access the OCaml interface.
  • Type "ocamlrun mlexample.byte" to run the tests.
  • Java interface

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


    Fast Polyhedra Abstract Domain
    Gagandeep Singh, Markus Püschel, Martin Vechev
    ACM POPL 2017
    Slides
    Making Numerical Program Analysis Fast
    Gagandeep Singh, Markus Püschel, Martin Vechev
    ACM PLDI 2015
    PDF Slides PDF

    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 Octagons

    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