package absolute

AbSolute

AbSolute is a constraint solver based on abstract domains from the theory of abstract interpretation. It implements the solving method presented in: "A Constraint Solver Based on Abstract Domains".

This repository provides code for two packages: the AbSolute solver and the libabsolute library. You can use the later from you OCaml programs, its documentation is available here.

AbSolute is still in developpement, and have not been fully tested. Feel free to fill an issue or contact any member of the developpement team if you want to report a bug or suggest a feature.

Contributors: Marie Pelleau, Ghiles Ziat, Alexandre Marechal, Pierre Talbot, Antoine Miné, Charlotte Truchet. Supported by ANR CoVerif.

The AbSolute Solver

introductory example

In AbSolute, you first declare your variables in the init section, and then the constraints on these variables in the constraints section:

/* simple example with sinus and cosinus */
init{
  real x = [-10;10];
  real y = [-5;5];
}

constraints{
  y < sin(x) + 1;
  y > cos(x) - 1;
}

This model is saved into a file that can be fed into the AbSolute solver. You can checkout our Emacs mode for a more convenient use¹. We also have nice graphics showing how the problem was solved:

You can see other examples of problems in the problems directory. Please also consult our documentation for more information.

Getting Started

The installation process should be easy, if you have any problem, see the Section Troubleshooting, fill an issue or email us directly.

Installation

The easiest way to install AbSolute is through the OCaml package manager opam. You will have to install it if you do not have it. For example:

apt-get install opam # on Debian, see opam documentation for other distributions.
opam init --comp 4.09.0 # Initialize ~/.opam with a freshly compiled OCaml 4.09.0

The next step is to download and build AbSolute. If you intent to modify the source code and possibly contribute to the project, jump to the "Developpers" section. Otherwise, you can install it from opam:

opam repo add absolute https://raw.githubusercontent.com/mpelleau/AbSolute/master
opam install absolute
# Retrieve a model file
wget https://raw.githubusercontent.com/mpelleau/AbSolute/master/problems/booth.abs
# Test the file with your fresh installation
absolute booth.abs
# Display solver options
absolute --help

Developpers

See the CONTIBUTING.md

Results

Beside the ouptut, AbSolute uses the following return code to describe the results.

• 1 for an internal error

• 2 misuse of options

• 3 the problem is unsatisfiable

• 4 the problem may admit solutions but the solver failed to find one

• 5 the problem is satisfiable

Troubleshooting

1. For some reason, having both packages libapron and libapron-dev installed will make the building of AbSolute fail. Therefore, the easiest way to deal with apron is to install it with and only with opam : https://opam.ocaml.org/packages/

Citing AbSolute:

@inproceedings{DBLP:conf/vmcai/PelleauMTB13,
  author    = {Marie Pelleau and
               Antoine Min{\'{e}} and
               Charlotte Truchet and
               Fr{\'{e}}d{\'{e}}ric Benhamou},
  title     = {A Constraint Solver Based on Abstract Domains},
  booktitle = {Verification, Model Checking, and Abstract Interpretation, 14th International
               Conference, {VMCAI} 2013, Rome, Italy, January 20-22, 2013. Proceedings},
  pages     = {434--454},
  year      = {2013},
  crossref  = {DBLP:conf/vmcai/2013},
  url       = {https://doi.org/10.1007/978-3-642-35873-9\_26},
  doi       = {10.1007/978-3-642-35873-9\_26},
  timestamp = {Wed, 24 May 2017 08:30:31 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/vmcai/PelleauMTB13},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

1. A simple emacs mode for editing AbSolute problem description files↩:

You can simply add the following to your .emacs:

(require 'generic-x) ;; you will need this

(define-generic-mode 'absolute-mode          ;; name of the mode
  '("/*" "*/")                               ;; comments start with '/*' and end with '*/'
  '("init" "constraints" "solutions"
    "real" "int" "in" "notin")               ;; keywords
  '(("\\(?:cos\\|exp\\|s\\(?:in\\|qrt\\)\\)"
     . 'font-lock-function-name-face))       ;; function names
  '("\\.abs$")                               ;; files for which to activate this mode
  nil                                        ;; other actions to perform
  "A mode for AbSolute files"                ;; doc string
  )