ELINA: ETH LIbrary for Numerical Analysis

News

25 Jul 2018: Version 1.1 with various bugfixes released.
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.

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 AVX as follows:

For Linux: Run "cat /proc/cpuinfo | grep "avx””, For Mac: Run “sysctl -a | grep machdep.cpu.features”.
Check for the string "avx" in output.

If your machine support AVX instructions, then ELINA can be configured using "./configure -use-vector". This will enable ELINA to benefit from AVX instructions for making the Octagon and Zones domain implementation faster.

For 32-bit systems, disable the architecture specific flags (m64, march=native etc. ) and DTIMING in DFLAGS.

ELINA can be compiled and installed by running "make" and then "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

Slides
A Practical Construction for Decomposing Numerical Abstract Domains
Gagandeep Singh, Markus Püschel, Martin Vechev
ACM POPL 2018

Paper

Slides

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

Paper

Slides

Promo

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.