Abstract
The classical method for program analysis by abstract interpretation consists in computing first an increasing sequence using an extrapolation operation, called widening, to correctly approximate the limit of the sequence. Then, this approximation is improved by computing a decreasing sequence without widening, the terms of which are all correct, more and more precise approximations. It is generally admitted that, when the decreasing sequence reaches a fixpoint, it cannot be improved further. As a consequence, most efforts for improving the precision of an analysis have been devoted to improving the limit of the increasing sequence. In a previous paper, we proposed a method to improve a fixpoint after its computation. This method consists in computing from the obtained solution a new starting value from which increasing and decreasing sequences are computed again. The new starting value is obtained by projecting the solution onto well-chosen components. The present paper extends and improves the previous paper: the method is discussed in view of some example programs for which it fails. A new method is proposed to choose the restarting value: the restarting value is no longer a simple projection, but is built by gathering and combining information backward the widening nodes in the basic solution. Experiments show that the new method properly solves all our examples, and improves significantly the results obtained on a classical benchmark.
Similar content being viewed by others
Notes
We use a form of CFG that should be self-explanatory. It is made precise in Sect. 4.2.
The table shows, at each iteration of the analysis and for each node of the graph, the value (i.e., the interval for i) attached to the node; since this value is computed only when the value of a preceding node changes, cells are left empty when their value is not computed.
These two programs could have been generated by compiling the Esterel programs [11] “every 60 tick do emit minute” and “every 60 s do emit minute”.
Defining the quality of a widening operator is difficult: since a widening is not monotone, by essence, a locally more precise widening is not guaranteed to lead to a more precise limit at the end of the sequence. This is why most proposed improvements are justified experimentally.
Notice that widening and narrowing are not dual. Following [17], widening is an extrapolation operator (its result is outside the range of its operands) while narrowing is an interpolation (its result is between its operands).
For simplicity, we consider only the case of monotone abstract functions. The extension to non-monotone functions could be considered, since such functions appear in some contexts—like analysis by induction on the syntax, or when using some partially reduced products of domains [5], or in context-sensitive interprocedural analysis [2,3,4].
The chain condition, imposed to a widening operator \(\nabla \), states that for any increasing sequence \(X_0\sqsubseteq X_1\sqsubseteq X_2\sqsubseteq \cdots \) of abstract values, the sequence \(Y_0=X_0\), \(Y_{n+1}=Y_n\nabla X_{n+1}\) is not strictly increasing (i.e., converges after a finite number of terms).
References
Amato G, Scozzari F (2013) Localizing widening and narrowing. In: Static analysis international symposium, SAS 2013, Seattle, pp 25–42
Amato G, Scozzari F, Seidl H, Apinis K, Vojdani V (2016) Efficiently intertwining widening and narrowing. Sci Comput Program 120:1–24
Apinis K, Seidl H, Vojdani V (2012) Side-effecting constraint systems: a swiss army knife for program analysis. In: Asian symposium on programming languages and systems, APLAS 2012, Kyoto, Japan, pp 157–172
Apinis K, Seidl H, Vojdani V (2013) How to combine widening and narrowing for non-monotonic systems of equations. In: Programming language design and implementation, PLDI 2013, Seattle, pp 377–386
Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2003) A static analyzer for large safety-critical software. In: Programming language design and implementation, PLDI 2003, San Diego, California, pp 196–207
Bardin S, Finkel A, Leroux J, Petrucci L (July 2003) Fast: fast acceleration of symbolic transition systems. In: Computer aided verification, CAV 2003, Boulder, Colorado, pp 118–121
Bultan T, Gerber R, Pugh W (1997) Symbolic model checking of infinite state systems using Presburger arithmetic. In: Computer aided verification, CAV 1997, Haifa, Israel, pp 400–411
Bagnara R, Hill PM, Ricci E, Zaffanella E (2003) Precise widening operators for convex polyhedra. In: Static analysis symposium, SAS 2003, San Diego, California, USA, pp 337–354
Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. In: Bjørner D, Broy M, Pottosin IV (eds) Formal methods in programming and their applications. Lecture notes in computer science, vol 735. Springer, Heidelberg
Bagnara R, Ricci E, Zaffanella E, Hill PM (2002) Possibly not closed convex polyhedra and the Parma Polyhedra Library. In: Static analysis symposium, SAS 2002, Madrid, Spain, pp 213–229
Boussinot F, de Simone R (1991) The Esterel language. Proc IEEE 79(9):1293–1304
Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: 2nd international symposium on programming. Dunod, Paris
Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of programming languages, POPL 1977, Los Angeles, California, pp 238–252
Costan A, Gaubert S, Goubault E, Martel M, Putot S (2005) A policy iteration algorithm for computing fixed points in static analysis of programs. In: Computer-aided verification, CAV 2005, Edinburgh, Scotland, pp 462–475
Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Principles of programming languages, POPL 1978, Tucson, Arizona, pp 84–96
Comon H, Jurski Y (June 1998) Multiple counters automata, safety analysis and Presburger arithmetic. In: Computer aided verification, CAV 1998, Vancouver, Canada, pp 268–279
Cousot P (2015) Abstracting induction by extrapolation and interpolation. In: Verification. Model checking, and abstract interpretation, VMCAI 2015, Mumbai, India, pp 19–42
Cortesi A, Zanioli M (2011) Widening and narrowing operators for abstract interpretation. Comput Lang Syst Struct 37(1):24–42
Gulavani BS, Chakraborty S, Nori AV, Rajamani SK (2008) Automatically refining abstract interpretations. In: Tools and algorithms for construction and analysis of systems, TACAS 2008, Budapest, Hungary, pp 443–458
Gonnord L, Halbwachs N (2006) Combining widening and acceleration in linear relation analysis. In: Static analysis symposium, SAS 2006, Seoul, Korea, pp 144–160
Goubault E (2001) Static analyses of the precision of floating-point operations. In: Static analysis symposium, SAS 2001, Paris, France, pp 234–259
Gopan D, Reps T (2006) Lookahead widening. In: Computer aided verification, CAV 2006, Seattle, WA, pp 452–466
Gulavani BS, Rajamani SK (2006) Counterexample driven refinement for abstract interpretation. In: Tools and algorithms for construction and analysis of systems, TACAS 2006, Vienna, Austria, pp 474–488
Gopan D, Reps TW (2007) Guided static analysis. In: Static analysis symposium, SAS 2007, Kongens Lyngby, Denmark, pp 349–365
Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: European symposium on programming, ESOP 2007, Braga, Portugal, pp 300–315
Gonnord L, Schrammel P (2014) Abstract acceleration in linear relation analysis. Sci Comput Program 93:125–153
Halbwachs N (1993) Delay analysis in synchronous programs. In: Computer-Aided Verification, CAV 1993, Elounda, Greece, pp 333–346
Halbwachs N, Henry J (2012) When the decreasing sequence fails. In: Static analysis symposium, SAS 2012, Deauville, France, pp 198–213
Henry J, Monniaux D, Moy M (2012) PAGAI: a path sensitive static analyzer. Electr Notes Theor Comput Sci 289:15–25
Halbwachs N, Proy YE, Roumanoff P (1997) Verification of real-time systems using linear relation analysis. Form Methods Syst Des 11(2):157–185
Jeannet B, Miné A (2009) Apron: a library of numerical abstract domains for static analysis. In: Computer aided verification, CAV 2009, Grenoble, France, pp 661–667
Karpenkov E, Monniaux D, Wendler P (2016) Program analysis with local policy iteration. In: Verification. Model checking, and abstract interpretation, VMCAI 2016, St Petersburg, Florida, pp 127–146
Lattner C, Adve V (2004) LLVM: a compilation framework for lifelong program analysis and transformation. In: Code generation and optimization, CGO 2004, Washington, DC, pp 75–86
Lakhdar-Chaouch L, Jeannet B, Girault A (2011) Widening with thresholds for programs with complex control graphs. In: Automated technology for verification and analysis, ATVA 2011, Taipei, Taiwan, pp 492–502
Miné A (2001) The Octagon abstract domain. In: Eighth working conference on reverse engineering, WCRE 2001, Stuttgart, Germany, pp 310–319
Miné A (2004) Weakly relational numerical abstract domains. PhD thesis, Ecole Polytechnique, Paris
Monniaux D, Le Guen J (2012) Stratified static analysis based on variable dependencies. Electr Notes Theor Comput Sci 288:61–74
Putot S, Goubault E, Martel M (2003) Static analysis-based validation of floating-point computations. In: Numerical software with result verification, international Dagstuhl seminar. LNCS 2991, Springer, Berlin, pp 306–313
Shamir A (1979) A linear time algorithm for finding minimum cutsets in reducible graphs. SIAM J Comput 8(4):645–655
Simon A, King A (2006) Widening polyhedra with landmarks. In: Asian symposium on programming languages and systems, APLAS 2006, Sydney, Australia, pp 166–182
Sankaranarayanan S, Sipma H, Manna Z (2004) Constraint-based linear relations analysis. In: Static analysis symposium, SAS 2004, Verona, Italy, pp 53–68
Sankaranarayanan S, Sipma H, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: Verification, model-checking, and abstract intepretation, VMCAI 2005, Paris, France, pp 25–41
Su Z, Wagner D (2004) A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In: Tools and algorithms for construction and analysis of systems, TACAS 2004, Barcelona, Spain, pp 280–295
Tarjan RE (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1:146–160
Wolper P, Boigelot B (1998) Verifying systems with infinite but regular state spaces. In: Computer-aided verification, CAV’98, Vancouver, Canada, pp 88–97
Wang C, Yang Z, Gupta A, Ivančić F (2007) Using counterexamples for improving the precision of reachability computation with polyhedra. In: Computer-aided verification, CAV 2007, Berlin, Germany, pp 352–365
Acknowledgements
Julien Henry implemented the first version of the select & project method in his analyzer Pagai. We are also indebted to the reviewers for their helpful comments.
Author information
Authors and Affiliations
Corresponding author
Additional information
This work has been partially supported by the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013)/ERC Grant Agreement nr. 306595 “STATOR”.
Rights and permissions
About this article
Cite this article
Boutonnet, R., Halbwachs, N. Improving the results of program analysis by abstract interpretation beyond the decreasing sequence. Form Methods Syst Des 53, 384–406 (2018). https://doi.org/10.1007/s10703-017-0310-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-017-0310-y