Laure Gonnord_Research_ASPIC_benchs

Aspic tool implementation

Aspic is implemented over a fixpoint generic analyzer called Analyseur ([ANA]), developped by B. Jeannet at Inria. This tool performs a fixpoint analysis, provided an encoding of the control flow graph and an implementation of the abstract lattice of properties. We chose the polyhedral library NewPolka ([New]).

Aspic takes as input the textual automata input format of the tool Fast ([BFLP03]). A Fast file is composed of two parts : A “model”, which contains a textual description of a unique counter automaton: numerical vars, control points and transition functions consisting of a source, a destination, a numerical guard (possibly non convex) and an affine action over the numerical variables.

A “strategy”, which defines “regions”, and computation objectives. In contrast with the tool Fast itself, our tool only needs an initial region; an “error region” is only optionnal, and no additional information is required.

The Aspic tool makes a forward accessibility analysis, which aims at discovering some polyhedral invariants at each program control point. If an error region is defined (a formula over numerical variables and control points), the goal is transformed into a non accessibility problem by creating new bad states and new transitions; if, after convergence, all the bad states are associated an empty polyhedron, the goal is proved, otherwise the result is unconclusive.

The method used in aspic, called “Accelerated Linear Relation Analysis” is described in [Gon07] and [GH06].

Usage

The simplest way to use Aspic on the input.fst file is to use the command line :

./aspic input.fst [options]

with

• no option for lra+acceleration
• option -noaccel for classic LRA with classic limited widening.
• option -noaccel -nouptos for classic LRA with CH79 initial widening
• option -reps for lookahead widening.
• option -bruce for translating into StInG format

Toy examples

For the toy examples, we compared our method (comumn “Aspic”) with the following ones :

Classic Linear Relation Analysis, without widening upto, without the new path algorithm, with two widenings : the standard one ([Hal79]) and the one proposed in  [BHRZ03]. The first analysis is implemented in Aspic and the StInG tool ([StI]) can deal with both two. The results can be found in column Hal79/BHRZ03. On the toy examples, the invariants are indeed the same.

The algorithm [SSM04], which is implemented in StInG (column named “STING”). Aspic provides a translator from Fast language to the input grammar of StInG.

The classical LRA with or without widening upto, with the new path algorithm. It has been done with the Aspic tool (column Ch79-v2)

The LRA with “lookahead widening” ([GR06]) that we also implemented in Aspic. The results can be found in column called “lookahead”.

The Fast tool([FAS]), that implement the acceleration techniques we described in [Ler03]. The used Fast version does not give the fixpoint, it gives only some informaton on the accerated loops. The benchmarks give only an estimation of the computing time.

The description of the automata can be found in Aspic homepage. We present only the results obtained by the different methods on a relevant control point in Fig 1 and 2. No computation time is given because all these analysis are instantaneous, at the exception of the gas burner and the car analysis with the Fast tool (we stopped these two analysis after 15 min because the Presburger automata were too big at this time (more than 8000 states in each case).

On these examples, we can remark that Aspic manages to infer more complex invariants than the other tools. When the classic LRA (column CH79-v2) gives the same result, it needs the new path heuristic and the widening upto, and converge in more steps, as can be shown in Figure 3. In this last table, we used proof goals and compare the behaviour of classical LRA, Lookahead widening and LRA with acceleration. We indicate the minimum of delay used for prooving the goal, and the number of global iterations. This table shows the effectivity of aspic in terms of iteration number.

Sources

• Some of the Fast examples.
• Sting examples
• E. Goubault page
• personal debugging stuff
• wcet and scheduling examples from Paul Feautrier.

Acknowledgments

We would like to thank Paul Feautrier for his precious comments on polyhedra generation and for his benchmarks.

Références

[ANA]

ANALYSER. http://pop-art.inrialpes.fr/people/bjeannet/analyzer/index.html.

[BFLP03]

S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast: Fast acceleration of symbolic transition systems. In CAV’03, pages 118–121, Boulder (Colorado), July 2003. LNCS 2725, Springer-Verlag.

[BHRZ03]

R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337–354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.

[FAS]

FAST. http://www.lsv.ens-cachan.fr/fast/.

[GH06]

L. Gonnord and N. Halbwachs. Combining widening and acceleration in linear relation analysis. In 13th International Static Analysis Symposium, SAS’06, Seoul, Korea, August 2006.

[Gon07]

Laure Gonnord. Accélération abstraite pour l’amélioration de la précision en Analyse des Relations Linéaires. Thèse de doctorat, Université Joseph Fourier, Grenoble, October 2007.

[GR06]

D. Gopan and T. Reps. Lookahead widening. In CAV’06, Seattle, 2006.

[Hal79]

N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Thèse de troisième cycle, University of Grenoble, March 1979.

[Ler03]

J. Leroux. Algorithmique de la vérification des systèmes à compteurs – approximation et accélération – implémentation dans l’outil Fast. Phd thesis, Ecole Normale Supérieure de Cachan, December 2003.

[New]

NewPolka. http://pop-art.inrialpes.fr/people/bjeannet/newpolka/index.html.

[SSM04]

S. Sankaranarayanan, H. Sipma, and Z. Manna. Constraint-based linear relations analysis. In International Symposium on Static Analysis, SAS’2004, pages 53–68. LNCS 3148, Springer Verlag, 2004.

[StI]

StInG. http://theory.stanford.edu/~srirams/Software/sting.html.

---

Ce document a été traduit de L^AT_EX par H^EV^EA