Skip to main content
SpringerLink
Log in

Improving the results of program analysis by abstract interpretation beyond the decreasing sequence

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11

Similar content being viewed by others

Notes

  1. We use a form of CFG that should be self-explanatory. It is made precise in Sect. 4.2.

  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.

  3. 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”.

  4. 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.

  5. 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).

  6. 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].

  7. 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).

  8. www.mrtc.mdh.se/projects/wcet/benchmarks.html.

References

  1. Amato G, Scozzari F (2013) Localizing widening and narrowing. In: Static analysis international symposium, SAS 2013, Seattle, pp 25–42

  2. Amato G, Scozzari F, Seidl H, Apinis K, Vojdani V (2016) Efficiently intertwining widening and narrowing. Sci Comput Program 120:1–24

    Article  Google Scholar 

  3. 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

    Chapter  Google Scholar 

  4. 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

  5. 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

  6. 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

  7. 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

    Chapter  Google Scholar 

  8. 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

  9. 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

  10. 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

    Chapter  Google Scholar 

  11. Boussinot F, de Simone R (1991) The Esterel language. Proc IEEE 79(9):1293–1304

    Article  Google Scholar 

  12. Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: 2nd international symposium on programming. Dunod, Paris

  13. 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

  14. 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

    Chapter  Google Scholar 

  15. 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

  16. 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

  17. Cousot P (2015) Abstracting induction by extrapolation and interpolation. In: Verification. Model checking, and abstract interpretation, VMCAI 2015, Mumbai, India, pp 19–42

  18. Cortesi A, Zanioli M (2011) Widening and narrowing operators for abstract interpretation. Comput Lang Syst Struct 37(1):24–42

    MATH  Google Scholar 

  19. 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

  20. Gonnord L, Halbwachs N (2006) Combining widening and acceleration in linear relation analysis. In: Static analysis symposium, SAS 2006, Seoul, Korea, pp 144–160

    Chapter  Google Scholar 

  21. Goubault E (2001) Static analyses of the precision of floating-point operations. In: Static analysis symposium, SAS 2001, Paris, France, pp 234–259

  22. Gopan D, Reps T (2006) Lookahead widening. In: Computer aided verification, CAV 2006, Seattle, WA, pp 452–466

  23. 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

  24. Gopan D, Reps TW (2007) Guided static analysis. In: Static analysis symposium, SAS 2007, Kongens Lyngby, Denmark, pp 349–365

  25. Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: European symposium on programming, ESOP 2007, Braga, Portugal, pp 300–315

    Chapter  Google Scholar 

  26. Gonnord L, Schrammel P (2014) Abstract acceleration in linear relation analysis. Sci Comput Program 93:125–153

    Article  Google Scholar 

  27. Halbwachs N (1993) Delay analysis in synchronous programs. In: Computer-Aided Verification, CAV 1993, Elounda, Greece, pp 333–346

    Chapter  Google Scholar 

  28. Halbwachs N, Henry J (2012) When the decreasing sequence fails. In: Static analysis symposium, SAS 2012, Deauville, France, pp 198–213

    Chapter  Google Scholar 

  29. Henry J, Monniaux D, Moy M (2012) PAGAI: a path sensitive static analyzer. Electr Notes Theor Comput Sci 289:15–25

    Article  Google Scholar 

  30. Halbwachs N, Proy YE, Roumanoff P (1997) Verification of real-time systems using linear relation analysis. Form Methods Syst Des 11(2):157–185

    Article  Google Scholar 

  31. 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

    Chapter  Google Scholar 

  32. 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

    Google Scholar 

  33. 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

  34. 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

    Chapter  Google Scholar 

  35. Miné A (2001) The Octagon abstract domain. In: Eighth working conference on reverse engineering, WCRE 2001, Stuttgart, Germany, pp 310–319

  36. Miné A (2004) Weakly relational numerical abstract domains. PhD thesis, Ecole Polytechnique, Paris

  37. Monniaux D, Le Guen J (2012) Stratified static analysis based on variable dependencies. Electr Notes Theor Comput Sci 288:61–74

    Article  Google Scholar 

  38. 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

    Chapter  Google Scholar 

  39. Shamir A (1979) A linear time algorithm for finding minimum cutsets in reducible graphs. SIAM J Comput 8(4):645–655

    Article  MathSciNet  Google Scholar 

  40. Simon A, King A (2006) Widening polyhedra with landmarks. In: Asian symposium on programming languages and systems, APLAS 2006, Sydney, Australia, pp 166–182

    Chapter  Google Scholar 

  41. Sankaranarayanan S, Sipma H, Manna Z (2004) Constraint-based linear relations analysis. In: Static analysis symposium, SAS 2004, Verona, Italy, pp 53–68

    Chapter  Google Scholar 

  42. 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

  43. 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

    Chapter  Google Scholar 

  44. Tarjan RE (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1:146–160

    Article  MathSciNet  Google Scholar 

  45. Wolper P, Boigelot B (1998) Verifying systems with infinite but regular state spaces. In: Computer-aided verification, CAV’98, Vancouver, Canada, pp 88–97

  46. 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

Download references

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

  1. Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000, Grenoble, France

    Rémy Boutonnet & Nicolas Halbwachs

Authors
  1. Rémy Boutonnet
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nicolas Halbwachs
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Nicolas Halbwachs.

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

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

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

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-017-0310-y

Keywords

Search

Navigation