Tiny

TINY stands for Tiny Is Not Yasa (Yet Another Static Analyzer).

Tiny is a simple abstract interpretation based static analyzer for a small imperative language. It was first written for abstract interpretation tutorials (typically by making the students write simple non relational abstract domains) and was primarily intended to remain small and simple. It now provides:

• non-relational numerical domains: constants (Kildall), parity, signs, intervals (integers, rationals, doubles, with rounding errors), small floats, affine forms, and their reductions;
• relational numerical domains through Apron: polyhedra, octagons, boxes;
• boolean partitioning of any numerical domain;
• loop unrolling and finite-horizon (simulation) analyses;
• an OCaml library, used by the lustrec compiler to analyze Lustre models (lustrev -tiny).

Work in progress. Tiny is a research and teaching tool under active development: interfaces and results may change without notice. The BddApron domains (lib/domains/bddapronWrapper.ml) are currently not built: they require the bddapron library, only tested with OCaml 4.07.

Quick start

opam pin add tiny git+https://github.com/Embedded-SW-VnV/tiny.git
tiny -a polka examples/int/ex01.tiny

tiny -help lists the options and the available abstract domains.

User guide

You can either install tiny as an opam package or in a docker container. We advised you to install it with OPAM because it makes using tiny easier.

OPAM installation

Dependencies

You need to have OPAM the OCaml Package Manager installed. You will find instruction on how to install opam on your system at https://opam.ocaml.org/doc/Install.html

You also need to install rsync.

Other packages will be required. The list of the required system package is system-dependent. But don't worry OPAM is able to determine which packages to install.

For information only (no need to install them manually) on a fresh debian-based system the following packages are required : ̀libgmp-dev libmpfr-dev m4 perl

Install

Clone this project with git and open a terminal in the root of the project then run :

opam pin -n -y . # Add tiny in opam
opam depext tiny # Install the required system dependencies
opam install tiny # Install Tiny

You can then use tiny from the command line. Running tiny without any input will show the usage instructions.

$ tiny
tiny: No input file provided.
Usage: tiny [options] <input_filename>
  --abstract-domain <domain>  Use abstract domain <domain> (dummyInt (default), kildall_int, kildall_real, parity, signes_real, signes_int, intervals_infint, intervals_rat, intervals_double, signes_int_parity_red_1, intervals_double_err, affine, polka, oct)
...

Uninstall

Just run opam unpin tiny

Docker installation

Dependencies

The only dependency here is docker.

Install

In a shell with the root of this project as current directory run : sudo docker build --tag tiny . in order to build the docker image

For convenience we will define the tiny-docker alias. alias tiny-docker='sudo docker run --rm -v $(pwd):/workdir -w /workdir --entrypoint "/tiny/bin/tiny" tiny' You can add the line above to your .bashrc

Use

tiny-docker -a signes_int examples/int/ex01.tiny

NB: the docker container only has access to your current directory so path to the file to analyze should be relative and under the current directory.

Uninstall

Just run : sudo docker image rm tiny

Developer guide

Abreviation

asn : assignement
asrt : assertion
nop : no - op (dummy statement)
stm : statement
env : environment
expr : expression
u- (prefix) : (usually) untyped

Build

This project uses dune build system.

The bin/ folder contains three files :

• main.ml which is the entry point of the tiny executable
• main_nn.ml, the entry point of the tiny-nn executable
• test_domain.ml which defines an executable to test domains The /lib folder defines a private library containing internal tiny modules.

Build and run executable

dune exec ./bin/main.exe
dune exec ./bin/test_domain.exe

Generating the documentation

dune build @doc-private

The documentation is generated to ̀_build/default/_doc/_html/tiny@XXXXXXXX/Tiny/index.html`

Something strange ?

Clean old builds with : dune clean

Managing depencies

Depencies are managed with dune if you need to add or change a depency just edit the dune-project config file at the root of the repository. The depencies are listed as s-expressions such as :

(package 
 (depends
  (opam_package_name1 (>= minimal_version))
  (opam_package_name1 (>= minimal_version))
 )
)

Authors

Tiny is developed by

• Pierre Roux — original author (2012): the language, its parser and type checker, the analyzer (fixpoint iteration with widening and descending iterations), the non-relational domains and the Apron wrapper.
• Pierre-Loïc Garoche — maintainer; boolean partitioning domains (BoolPartition, BoolActivate), loop unrolling and finite-horizon analysis, the API used by lustrec, packaging.

Contributors

• Corentin Lauverjat (2020) — migration to dune, opam and Docker packaging, C-compatible boolean operators, JSON export of abstract values, error reporting of the menhir parser.
• Alexandre Gleize-Pons (2021) — BddApron domains, Apron box and octagon domains, rand_int inputs, widening on intervals, examples and the benchmarking script timetab.sh.
• Julien Rodrigues (2022) — connection with the analysis of Lustre models: node-by-node analysis and per-node results, used by lustrec's tiny plugin.

License

GPL-3.0-or-later, see LICENSE.