×

Demand-driven interprocedural analysis for map-based abstract domains. (English) Zbl 1400.68054

Summary: Many data flow analysis problems can be succinctly formalized using constraint systems. For interprocedural analysis, the system may contain an infinite number of constraints, but it can still be solved using a local solver that evaluates the constraints in a demand-driven fashion. In this paper, we use local solvers to develop a compositional framework for interprocedural on-demand static analysis. We can integrate any map-based abstract domain into our framework, such as a points-to analysis that maps pointers to their possible target addresses. Driven by the local solving algorithm that tracks the required dependencies, only those points-to sets that are of interest to the user are computed. The approach is applicable whenever the keys of the map are efficiently comparable and the domain operations are applied pointwise; we place no additional restrictions on the value domain nor on the transfer functions of the analysis beyond the standard termination requirements of the solvers.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

Goblint; RELAY; Flix; ASTREE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amato, Gianluca; Scozzari, Francesca; Seidl, Helmut; Apinis, Kalmer; Vojdani, Vesal, Efficiently intertwining widening and narrowing, Sci. Comput. Program., 120, 1-24, (May 2016)
[2] Anand, Saswat; Godefroid, Patrice; Tillmann, Nikolai, Demand-driven compositional symbolic execution, (TACAS’08, Lect. Notes Comput. Sci., vol. 4963, (March 2008), Springer), 367-381 · Zbl 1134.68355
[3] Apinis, Kalmer; Seidl, Helmut; Vojdani, Vesal, Side-effecting constraint systems: a swiss army knife for program analysis, (APLAS, Lect. Notes Comput. Sci., vol. 7705, (2012), Springer), 157-172
[4] Apinis, Kalmer; Seidl, Helmut; Vojdani, Vesal, How to combine widening and narrowing for non-monotonic systems of equations, (Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, (2013), ACM), 377-386 · Zbl 1474.68043
[5] Bird, Richard; Wadler, Philip, Introduction to functional programming, vol. 1, (1988), Prentice Hall
[6] Blanchet, Bruno; Cousot, Patrick; Cousot, Radhia; Feret, Jérome; Mauborgne, Laurent; Miné, Antoine; Monniaux, David; Rival, Xavier, A static analyzer for large safety-critical software, (ACM SIGPLAN Not., vol. 38, (2003), ACM), 196-207 · Zbl 1026.68514
[7] Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (POPL, (1977)) · Zbl 0788.68094
[8] Cousot, Patrick; Cousot, Radhia, Static determination of dynamic properties of programs, (Robinet, B., Second International Symposium on Programming, Paris, France, (1976), Dunod Paris), 106-130 · Zbl 0393.68080
[9] Cousot, Patrick; Cousot, Radhia, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, (4th ACM Symp. on Principles of Programming Languages (POPL’77), (1977), ACM Press), 238-252 · Zbl 1149.68389
[10] Cousot, Patrick; Cousot, Radhia, Systematic design of program analysis frameworks, (Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’79, New York, NY, USA, (1979), ACM), 269-282 · Zbl 0413.06004
[11] Cousot, Patrick; Halbwachs, Nicolas, Automatic discovery of linear restraints among variables of a program, (POPL’78, (1978), ACM Press), 84-96
[12] Duesterwald, Evelyn; Gupta, Rajiv; Soffa, Mary Lou, A practical framework for demand-driven interprocedural data flow analysis, ACM Trans. Program. Lang. Syst., 19, 6, 992-1030, (November 1997)
[13] Fecht, Christian; Seidl, Helmut, A faster solver for general systems of equations, Sci. Comput. Program., 35, 2, 137-161, (1999) · Zbl 0948.68016
[14] Feng, Yu; Wang, Xinyu; Dillig, Isil; Lin, Calvin, EXPLORER: query- and demand-driven exploration of interprocedural control flow properties, (OOPSLA’15, (2015), ACM Press), 520-534
[15] Frielinghaus, Stefan Schulze; Seidl, Helmut; Vogler, Ralf, Enforcing termination of interprocedural analysis, (International Static Analysis Symposium, (2016), Springer), 447-468 · Zbl 1394.68086
[16] Fähndrich, Manuel; Logozzo, Francesco, Static contract checking with abstract interpretation, (FoVeOOS’10, Lect. Notes Comput. Sci., vol. 6528, (June 2010), Springer), 10-30 · Zbl 1308.68033
[17] Godefroid, Patrice; Nori, Aditya V.; Rajamani, Sriram K.; Tetali, Sai Deep, Compositional may-must program analysis: unleashing the power of alternation, (POPL’10, (2010), ACM Press), 43-56 · Zbl 1312.68057
[18] Granger, Philippe, Improving the results of static analyses of programs by local decreasing iterations, (Foundations of Software Technology and Theoretical Computer Science, (1992), Springer), 68-79
[19] Heintze, Nevin; Tardieu, Olivier, Demand-driven pointer analysis, (PLDI’01, (2001), ACM Press), 24-34
[20] Henning, John L., SPEC CPU2006 benchmark descriptions, SIGARCH Comput. Archit. News, 34, 4, 1-17, (September 2006)
[21] Hofmann, Martin; Karbyshev, Aleksandr; Seidl, Helmut, What is a pure functional?, (ICALP (2), Lect. Notes Comput. Sci., vol. 6199, (2010), Springer), 199-210 · Zbl 1288.68037
[22] Hughes, John; Launchbury, John, Reversing abstract interpretations, Sci. Comput. Program., 22, 3, 307-326, (June 1994) · Zbl 0810.68094
[23] Jones, Neil D.; Mycroft, Alan, Data flow analysis of applicative programs using minimal function graphs, (Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’86, New York, NY, USA, (1986), ACM), 296-306
[24] Kam, John B.; Ullman, Jeffrey D., Monotone data flow analysis frameworks, Acta Inform., 7, 3, 305-317, (1977) · Zbl 0375.68020
[25] Kildall, G. A., A unified approach to global program optimization, (POPL’73, (1973), ACM Press), 194-206 · Zbl 0309.68020
[26] Knoop, J.; Steffen, B., The interprocedural coincidence theorem, (Fourth International Conference on Compiler Construction, CC’92, Paderborn, Germany, Lect. Notes Comput. Sci., vol. 641, (1992), Springer-Verlag), 125-140
[27] Lam, Monica S.; Whaley, John; Livshits, V. Benjamin; Martin, Michael C.; Avots, Dzintars; Carbin, Michael; Unkel, Christopher, Context-sensitive program analysis as database queries, (PODS’05, (2005), ACM Press), 1-12 · Zbl 1159.68386
[28] Le Charlier, Baudouin; Van Hentenryck, Pascal, A universal top-down fixpoint algorithm, (1992), Institute of Computer Science, University of Namur Belgium, Technical Report 92-22
[29] Madsen, Magnus; Yee, Ming-Ho; Lhoták, Ondřej, From Datalog to flix: a declarative language for fixed points on lattices, (Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’16, New York, NY, USA, (2016), ACM), 194-208
[30] Manevich, Roman; Sridharan, Manu; Adams, Stephen; Das, Manuvir; Yang, Zhe, PSE: explaining program failures via postmortem static analysis, (PSE’12, (2004), ACM), 63-72
[31] Müller-Olm, Markus; Seidl, Helmut, Precise interprocedural analysis through linear algebra, (Jones, Neil D.; Leroy, Xavier, Principles of Programming Languages, Venice, Italy, (January 2004), ACM), 330-341 · Zbl 1325.68068
[32] Naeem, Nomair A.; Lhoták, Ondřej; Rodriguez, Jonathan, Practical extensions to the IFDS algorithm, (CC’10, (2010), Springer), 124-144
[33] Nielson, Flemming; Nielson, Hanne R.; Hankin, Chris, Principles of program analysis, (2015), Springer · Zbl 0932.68013
[34] Pratikakis, Polyvios; Foster, Jeffrey S.; Hicks, Michael, {\sclocksmith}: context-sensitive correlation analysis for detecting races, (PLDI’06, (2006), ACM Press), 320-331
[35] Reps, Thomas, Solving demand versions of interprocedural analysis problems, (Proceedings of the 5th International Conference on Compiler Construction, CC ’94, London, UK, UK, (1994), Springer-Verlag), 389-403
[36] Reps, Thomas; Horwitz, Susan; Sagiv, Mooly, Precise interprocedural dataflow analysis via graph reachability, (POPL’95, (1995), ACM Press), 49-61 · Zbl 0874.68133
[37] Rival, Xavier; Toubhans, Antoine; Chang, Bor-Yuh Evan, Construction of abstract domains for heterogeneous properties (position paper), (Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, (October 2014), Springer Berlin, Heidelberg), 489-492 · Zbl 1426.68066
[38] Sagiv, Mooly; Reps, Thomas; Horwitz, Susan, Precise interprocedural dataflow analysis with applications to constant propagation, Theor. Comput. Sci., 167, 1, 131-170, (January 1996) · Zbl 0874.68133
[39] Saha, Diptikalyan; Ramakrishnan, C. R., Incremental and demand-driven points-to analysis using logic programming, (PPDP’05, (2005), ACM Press), 117-128 · Zbl 1165.68377
[40] Seidl, Helmut; Vojdani, Vesal, Region analysis for race detection, (SAS’09, Lect. Notes Comput. Sci., vol. 5673, (2009), Springer), 171-187 · Zbl 1248.68152
[41] Seidl, Helmut; Vene, Varmo; Müller-Olm, Markus, Global invariants for analyzing multithreaded applications, Proc. Est. Acad. Sci., Phys. Math., 52, 4, 413-436, (2003) · Zbl 1091.68520
[42] Seidl, Helmut; Vojdani, Vesal; Vene, Varmo, A smooth combination of linear and Herbrand equalities for polynomial time must-alias analysis, (FM’09, Lect. Notes Comput. Sci., vol. 5850, (2009), Springer), 644-659
[43] Seidl, Helmut; Wilhelm, Reinhard; Hack, Sebastian, Compiler design: analysis and transformation, (2012), Springer Science & Business Media · Zbl 1257.68004
[44] Seo, Sunae; Yang, Hongseok; Yi, Kwangkeun; Han, Taisook, Goal-directed weakening of abstract interpretation results, ACM Trans. Program. Lang. Syst., 29, 6, (October 2007)
[45] Sharir, Micha; Pnueli, Amir, Two approaches to interprocedural data flow analysis, (Muchnick, S. S.; Jones, N. D., Program Flow Analysis: Theory and Application, (1981), Prentice-Hall), 189-233
[46] Sridharan, Manu; Gopan, Denis; Shan, Lexin; Bodík, Rastislav, Demand-driven points-to analysis for Java, (OOPSLA’05, (2005), ACM Press), 59-76
[47] Vojdani, Vesal, Static data race analysis of heap-manipulating C programs, (2010), University of Tartu, PhD thesis · Zbl 1360.68004
[48] Vojdani, Vesal; Apinis, Kalmer; Rõtov, Vootele; Seidl, Helmut; Vene, Varmo; Vogler, Ralf, Static race detection for device drivers: the goblint approach, (Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, (2016), ACM), 391-402
[49] Voung, Jan Wen; Jhala, Ranjit; Lerner, Sorin, RELAY: static race detection on millions of lines of code, (ESEC/FSE’07, (2007), ACM Press), 205-214
[50] Weiss, Cathrin; Rubio-González, Cindy; Liblit, Ben, Database-backed program analysis for scalable error propagation, (Bertolino, Antonia; Canfora, Gerardo; Elbaum, Sebastian G., 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, vol. 1, (2015), IEEE Computer Society), 586-597
[51] Zheng, Xin; Rugina, Radu, Demand-driven alias analysis for C, (POPL’08, (2008), ACM Press), 197-208
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.