CINV
Library for Analysis of Programs with Dynamic Lists

Introduction
Examples
Download
Credits
References

Introduction

CINV is a tool for abstract reachability analysis of programs manipulating dynamic (singly linked) lists. It implements a generic abstract domain HS for reasoning about dynamic lists with unbounded data which includes an abstraction on the shape of the heap and which is parametrized by some abstract domain on finite sequences of data (a data words abstract domain, DW-domain for short). The DW-domain is intended to abstract the sequences of data in the lists by capturing relevant aspects such as their sizes, the sums or the multisets of their elements, or some class of constraints on their data at different (linearly ordered or successive) positions.

CINV provides currently three classes of DW-domains:

The first class, UCONS, relates data and lengths of lists segments through first-order formulas. These formulas have a special form: forall y. (P => U), where y is a vector of variables on the positions in the word, P is a constraint on the positions (seen as integers) associated with the y's, and U is a constraint on the data values at these positions, and possibly also on the positions when data are of numerical type.
The second class, LSUM, represents constraints relating data, length, and sums of data of list segments. In this class, several abstract domains can be obtained by varying the underlying numerical domain used (interval, octagons, polyhedra) and the kind (product or mixed) of relation allowed between the lengths and the sums of segments lists.
The third class, MSET, represents constraints relating data, length, and multisets of data of list segments. In this class, several abstract domains can be obtained by varying the underlying numerical domain used (interval, octagons, polyhedra) to represent data and length constraints. For the multiset constraints, we use the polyhedra domain with equality constraints.

For all these domains, CINV implements the APRON interface of abstract domains, uses the numerical domains provided by APRON and the fix point computation engines of INTERPROC.

CINV is now extended to:

inter-procedural analysis of C programs in CELIA.
deductive verification of programs on lists in Labs of CELIA.

Examples

We have applied CINV to a large class of programs manipulating lists. In particular, we have carried out the analysis of several sorting algorithms, of lists traversals with computation of complex arithmetical relations, etc.

For example, the following program sorts a list using an insertion sort algorithm which moves cells of the list instead of moving data.

C code Results of the analysis

C code	Results of the analysis
#include "intlist.h" /* acyclic(x) and l[x]==_l and data(x) */ intlist insertSortLst(intlist x) { intlist xi, y, yi, z, r; z = xi = yi = y = NULL; r = z = x; xi = x->next; while (xi != NULL) { yi = NULL; y = r; while (y != xi && y->data < xi->data) { yi = y; y = y->next; } if (yi == NULL) { z->next = xi->next; xi->next = r; r = xi; } else { z->next = xi->next; yi->next = xi; xi->next = y; } xi = NULL; xi = z->next; } return r; }	Using the `UCONS` domain with pattern forall y1,y2. y1 < y2, we obtain at the end of the main loop the ordering constraint on resulting list: forall y1,y2 in r. y1 < y2 => data(y1) <= data(y2) Moreover, with the pattern forall y. we obtain the constraint forall y in r. data(r) <= data(y). Using the `LSUM` domain, we obtain the preservation of data and length of the initial list at the end of the program as follows: acyclic(r) and length(r)=length(x)=_l and sum(r)=sum(x)=_S See the specific documentation of this example for details.

#include "intlist.h"

/* acyclic(x) and l[x]==_l and data(x) */
intlist insertSortLst(intlist x) {
  intlist xi, y, yi, z, r;
  z = xi = yi = y = NULL;
  r = z = x;
  xi = x->next;
  while (xi != NULL) {
    yi = NULL;
    y = r;
    while (y != xi && y->data < xi->data) {
      yi = y;
      y = y->next;
    }
    if (yi == NULL) {
      z->next = xi->next;
      xi->next = r;
      r = xi;
    }
    else {
      z->next = xi->next;
      yi->next = xi;
      xi->next = y;
    }
    xi = NULL;
    xi = z->next;
  }
  return r;
}

Using the UCONS domain with pattern forall y1,y2. y1 < y2, we obtain at the end of the main loop the ordering constraint on resulting list:
forall y1,y2 in r. y1 < y2 => data(y1) <= data(y2)
Moreover, with the pattern forall y. we obtain the constraint forall y in r. data(r) <= data(y).

Using the LSUM domain, we obtain the preservation of data and length of the initial list at the end of the program as follows:
acyclic(r) and length(r)=length(x)=_l and sum(r)=sum(x)=_S

See the specific documentation of this example for details.

Another example dealt by our tool is the intialisation of a list with the first elements of the Fibonacci sequence.

C code Results of the analysis

C code	Results of the analysis
#include "intlist.h" /* acyclic(x) and l[x]==_l and data(x) */ void initFibo(intlist x) { int m1 = 1; int m2 = 0; intlist xi = x; while (xi != NULL) { xi->data = m1+m2; m1 = m2; m2 = xi->data; xi = xi->next; } }	Using the `LSUM` domain, we obtain at the end of the program an invariant correspoding to a known identity of Fibonacci sequence: acyclic(x) and sum(x)=2m2+m1-2 Using the `UCONS` domain with pattern forall y1,y2. y1 < y2, we obtain at the end of the main loop the ordering constraint on resulting list: forall y1,y2 in x. y1 < y2 => data(y1) <= data(y2) Moreover, with the pattern forall y. we obtain the constraint forall y in x. y <= data(y) saying that the growing of the Fibonacci sequence is more than linear. See the specific documentation of this example for details.

#include "intlist.h"
/* acyclic(x) and l[x]==_l and data(x) */
void initFibo(intlist x) {
  int m1 = 1;
  int m2 = 0;
  intlist xi = x;
  while (xi != NULL) {
    xi->data = m1+m2;
    m1 = m2;
    m2 = xi->data;
    xi = xi->next;
  }
}

Using the LSUM domain, we obtain at the end of the program an invariant correspoding to a known identity of Fibonacci sequence:
acyclic(x) and sum(x)=2m2+m1-2

Using the UCONS domain with pattern forall y1,y2. y1 < y2, we obtain at the end of the main loop the ordering constraint on resulting list:
forall y1,y2 in x. y1 < y2 => data(y1) <= data(y2)
Moreover, with the pattern forall y. we obtain the constraint forall y in x. y <= data(y) saying that the growing of the Fibonacci sequence is more than linear.

See the specific documentation of this example for details.

The programs dealt currently by CINV are available on the distributed package (see Download, directory samples/src). A detailed presentation of results is given in the following documentation:

HTML version,
PDF version.

Download

CINV is a free software under LGPL license. The current version of CINV is 0.2.2. Older versions:

0.2.1
0.1

For installing CINV you need:

autoconf/automake.
An ANSI C compiler (only gcc with ansi option has been tested).
INTERPROC distribution which includes APRON and asks for downloading other tools or libraries (Ocaml, Camlidl, PPL).

Credits

Participants to the CINV project:

References

[BDERS10] A. Bouajjani, C. Dragoi, C. Enea, A. Rezine, and M. Sighireanu. Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. Long version of the CAV'2010 paper.

Last updated: Mon Oct 17 10:09:57 CEST 2011

CINV Library for Analysis of Programs with Dynamic Lists

Contents