×

Improving the results of program analysis by abstract interpretation beyond the decreasing sequence. (English) Zbl 1425.68064

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

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

Aspic; LLVM; PPL; Dagger; ASTREE; FAST; Apron
PDFBibTeX XMLCite
Full Text: DOI HAL

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., Efficiently intertwining widening and narrowing, Sci Comput Program, 120, 1-24, (2016) · doi:10.1016/j.scico.2015.12.005
[3] Apinis, Kalmer; Seidl, Helmut; Vojdani, Vesal, Side-Effecting Constraint Systems: A Swiss Army Knife for Program Analysis, 157-172, (2012), Berlin, Heidelberg · doi:10.1007/978-3-642-35182-2_12
[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 · Zbl 1026.68514
[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, Tevfik; Gerber, Richard; Pugh, William, Symbolic model checking of infinite state systems using presburger arithmetic, 400-411, (1997), Berlin, Heidelberg · doi:10.1007/3-540-63166-6_39
[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 · Zbl 1067.68578
[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, Roberto; Ricci, Elisa; Zaffanella, Enea; Hill, Patricia M., Possibly Not Closed Convex Polyhedra and the Parma Polyhedra Library, 213-229, (2002), Berlin, Heidelberg · Zbl 1015.68215 · doi:10.1007/3-540-45789-5_17
[11] Boussinot, F.; Simone, R., The Esterel language, Proc IEEE, 79, 1293-1304, (1991) · doi:10.1109/5.97299
[12] Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: 2nd international symposium on programming. Dunod, Paris · Zbl 0393.68080
[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., A Policy Iteration Algorithm for Computing Fixed Points in Static Analysis of Programs, 462-475, (2005), Berlin, Heidelberg · Zbl 1081.68616 · doi:10.1007/11513988_46
[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 · Zbl 1432.68258
[18] Cortesi, A.; Zanioli, M., Widening and narrowing operators for abstract interpretation, Comput Lang Syst Struct, 37, 24-42, (2011) · Zbl 1218.68100
[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, Laure; Halbwachs, Nicolas, Combining Widening and Acceleration in Linear Relation Analysis, 144-160, (2006), Berlin, Heidelberg · Zbl 1225.68071 · doi:10.1007/11823230_10
[21] Goubault E (2001) Static analyses of the precision of floating-point operations. In: Static analysis symposium, SAS 2001, Paris, France, pp 234-259 · Zbl 0997.68518
[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 · Zbl 1180.68116
[24] Gopan D, Reps TW (2007) Guided static analysis. In: Static analysis symposium, SAS 2007, Kongens Lyngby, Denmark, pp 349-365 · Zbl 1211.68087
[25] Gawlitza, Thomas; Seidl, Helmut, Precise Fixpoint Computation Through Strategy Iteration, 300-315, (2007), Berlin, Heidelberg · Zbl 1187.68152 · doi:10.1007/978-3-540-71316-6_21
[26] Gonnord, L.; Schrammel, P., Abstract acceleration in linear relation analysis, Sci Comput Program, 93, 125-153, (2014) · doi:10.1016/j.scico.2013.09.016
[27] Halbwachs, Nicolas, Delay analysis in synchronous programs, 333-346, (1993), Berlin, Heidelberg · doi:10.1007/3-540-56922-7_28
[28] Halbwachs, Nicolas; Henry, Julien, When the Decreasing Sequence Fails, 198-213, (2012), Berlin, Heidelberg · doi:10.1007/978-3-642-33125-1_15
[29] Henry, J.; Monniaux, D.; Moy, M., PAGAI: a path sensitive static analyzer, Electr Notes Theor Comput Sci, 289, 15-25, (2012) · doi:10.1016/j.entcs.2012.11.003
[30] Halbwachs, N.; Proy, YE; Roumanoff, P., Verification of real-time systems using linear relation analysis, Form Methods Syst Des, 11, 157-185, (1997) · doi:10.1023/A:1008678014487
[31] Jeannet, Bertrand; Miné, Antoine, Apron: A Library of Numerical Abstract Domains for Static Analysis, 661-667, (2009), Berlin, Heidelberg · doi:10.1007/978-3-642-02658-4_52
[32] Karpenkov, Egor George; Monniaux, David; Wendler, Philipp, Program Analysis with Local Policy Iteration, 127-146, (2015), Berlin, Heidelberg · Zbl 1475.68092
[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, Lies; Jeannet, Bertrand; Girault, Alain, Widening with Thresholds for Programs with Complex Control Graphs, 492-502, (2011), Berlin, Heidelberg · Zbl 1348.68040 · doi:10.1007/978-3-642-24372-1_38
[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.; Guen, J., Stratified static analysis based on variable dependencies, Electr Notes Theor Comput Sci, 288, 61-74, (2012) · Zbl 1294.68063 · doi:10.1016/j.entcs.2012.10.008
[38] Putot, Sylvie; Goubault, Eric; Martel, Matthieu, Static Analysis-Based Validation of Floating-Point Computations, 306-313, (2004), Berlin, Heidelberg · Zbl 1126.65309 · doi:10.1007/978-3-540-24738-8_18
[39] Shamir, A., A linear time algorithm for finding minimum cutsets in reducible graphs, SIAM J Comput, 8, 645-655, (1979) · Zbl 0422.05029 · doi:10.1137/0208051
[40] Simon, Axel; King, Andy, Widening Polyhedra with Landmarks, 166-182, (2006), Berlin, Heidelberg · Zbl 1168.68365 · doi:10.1007/11924661_11
[41] Sankaranarayanan, Sriram; Sipma, Henny B.; Manna, Zohar, Constraint-Based Linear-Relations Analysis, 53-68, (2004), Berlin, Heidelberg · Zbl 1104.68023 · doi:10.1007/978-3-540-27864-1_7
[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 · Zbl 1111.68514
[43] Su, Zhendong; Wagner, David, A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings, 280-295, (2004), Berlin, Heidelberg · Zbl 1126.68358 · doi:10.1007/978-3-540-24730-2_23
[44] Tarjan, RE, Depth-first search and linear graph algorithms, SIAM J Comput, 1, 146-160, (1972) · Zbl 0251.05107 · doi:10.1137/0201010
[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 · Zbl 1135.68370
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.