Incremental and modular context-sensitive analysis. (English) Zbl 1472.68035

Summary: Context-sensitive global analysis of large code bases can be expensive, which can make its use impractical during software development. However, there are many situations in which modifications are small and isolated within a few components, and it is desirable to reuse as much as possible previous analysis results. This has been achieved to date through incremental global analysis fixpoint algorithms that achieve cost reductions at fine levels of granularity, such as changes in program lines. However, these fine-grained techniques are neither directly applicable to modular programs nor are they designed to take advantage of modular structures. This paper describes, implements, and evaluates an algorithm that performs efficient context-sensitive analysis incrementally on modular partitions of programs. The experimental results show that the proposed modular algorithm shows significant improvements, in both time and memory consumption, when compared to existing non-modular, fine-grain incremental analysis techniques. Furthermore, thanks to the proposed intermodular propagation of analysis information, our algorithm also outperforms traditional modular analysis even when analyzing from scratch.


68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N17 Logic programming
Full Text: DOI arXiv


[1] Acar, U. A.2009. Self-adjusting computation: (an overview). In Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2009, Savannah, GA, USA, 19-20 January 2009, Puebla, G. and Vidal, G., Eds. ACM, 1-6.
[2] Albert, E., Arenas, P., Genaim, S., Puebla, G. and Zanardini, D.2012. Cost analysis of object-oriented bytecode programs. Theoretical Computer Science (Special Issue on Quantitative Aspects of Programming Languages)413, 1, 142-159. · Zbl 1236.68042
[3] Albert, E., Correas, J., Puebla, G. and Román-Díez, G.2012. Incremental resource usage analysis. In Proceedings of the 2012 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2012, Philadelphia, Pennsylvania, USA, 23-24 January 2012. ACM Press, 25-34.
[4] Albert, E., Gómez-Zamalloa, M., Hubert, L. and Puebla, G.2007. Verification of Java bytecode using analysis and transformation of logic programs. In Ninth International Symposium on Practical Aspects of Declarative Languages (PADL 2007), LNCS, vol. 4354. Springer-Verlag, 124-139.
[5] Apt, K. R.1990. Introduction to logic programming. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Elsevier, 493-576. · Zbl 0900.68136
[6] Arzt, S. and Bodden, E.2014. Reviser: Efficiently updating IDE-/IFDS-based data-flow analyses in response to incremental program changes. In 36th International Conference on Software Engineering, ICSE’14, Hyderabad, India - May 31-June 07, 2014, Jalote, P., Briand, L. C. and Van Der Hoek, A., Eds. ACM, 288-298.
[7] Banda, G. and Gallagher, J. P.2009. Analysis of linear hybrid systems in CLP. In Logic-Based Program Synthesis and Transformation, 18th International Symposium, LOPSTR 2008, Valencia, Spain, 17-18 July 2008, M. Hanus, Ed. Lecture Notes in Computer Science, vol. 5438. Springer, 55-70. · Zbl 1185.68406
[8] Bjørner, N., Gurfinkel, A., Mcmillan, K. L. and Rybalchenko, A.2015. Horn clause solvers for program verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Beklemishev, L. D., Blass, A., Dershowitz, N., Finkbeiner, B. and Schulte, W., Eds. Lecture Notes in Computer Science, vol. 9300. Springer, 24-51. · Zbl 1465.68044
[9] Bjørner, N., Mcmillan, K. L. and Rybalchenko, A.2013. On solving universally quantified Horn clauses. In SAS, Logozzo, F. and Fähndrich, M., Eds. LNCS, vol. 7935. Springer, 105-125.
[10] Bossi, A., Gabbrieli, M., Levi, G. and Meo, M.1994. A compositional semantics for logic programs. Theoretical Computer Science 122, 1, 2, 3-47. · Zbl 0801.68110
[11] Braem, C., Charlier, B. L., Modart, S. and Hentenryck, P. V.1994. Cardinality analysis of Prolog. In Proceedings of International Symposium on Logic Programming. MIT Press, Ithaca, NY, 457-471.
[12] Bruynooghe, M.1991. A practical framework for the abstract interpretation of logic programs. Journal of Logic Programming 10, 91-124. · Zbl 0717.68010
[13] Bueno, F., De La Banda, M. G., Hermenegildo, M. V., Marriott, K., Puebla, G. and Stuckey, P.2001. A model for inter-module analysis and optimizing compilation. In Logic-based Program Synthesis and Transformation. LNCS, vol. 2042. Springer-Verlag, 86-102. · Zbl 1018.68501
[14] Burke, M.1990. An interval-based approach to exhaustive and incremental interprocedural data-flow analysis. ACM Transactions on Programming Languages and Systems12, 3, 341-395.
[15] Calcagno, C. and Distefano, D.2011. Infer: An automatic program verifier for memory safety of C programs. In NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, 18-20 April 2011. Proceedings, Bobaru, M. G., Havelund, K., Holzmann, G. J. and Joshi, R., Eds. Lecture Notes in Computer Science, vol. 6617. Springer, 459-465.
[16] Carroll, M. and Ryder, B.1988. Incremental data flow analysis via dominator and attribute updates. In 15th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, 274-284.
[17] Codish, M., Debray, S. and Giacobazzi, R.1993. Compositional analysis of modular logic programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL’93. ACM, Charleston, South Carolina, 451-464.
[18] Conway, C. L., Namjoshi, K. S., Dams, D. and Edwards, S. A.2005. Incremental algorithms for inter-procedural analysis of safety properties. In Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, 6-10 July 2005, Etessami, K. and Rajamani, S. K., Eds. Lecture Notes in Computer Science, vol. 3576. Springer, 449-461. · Zbl 1081.68615
[19] Cooper, K. and Kennedy, K.1984. Efficient computation of flow insensitive interprocedural summary information. In ACM SIGPLAN Symposium on Compiler Construction (SIGPLAN Notices, vol. 19(6)). ACM Press, 247-258.
[20] Correas, J., Puebla, G., Hermenegildo, M. V. and Bueno, F.2006. Experiments in context-sensitive analysis of modular programs. In 15th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR’05). LNCS, vol. 3901. Springer-Verlag, 163-178.
[21] Cousot, P. and Cousot, R.1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Symposium on Principles of Programming Languages (POPL’77). ACM Press, 238-252.
[22] Cousot, P. and Cousot, R.2002. Modular static program analysis, invited paper. In Eleventh International Conference on Compiler Construction, CC 2002. LNCS, vol. 2304. Springer, 159-178. · Zbl 1051.68624
[23] Cousot, P., Cousot, R., Feret, J., Miné, A., Mauborgne, L. and Rival, X.2009. Why does Astrée scale up?Formal Methods in System Design (FMSD)35, 3, 229-264. · Zbl 1185.68241
[24] De Angelis, E., Fioravanti, F., Pettorossi, A. and Proietti, M.2014. VeriMAP: A tool for verifying programs through transformations. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, 5-13 April 2014. Proceedings, Ábrahám, E. and Havelund, K., Eds. Lecture Notes in Computer Science, vol. 8413. Springer, 568-574.
[25] De Moura, L. M. and Bjørner, N.2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Ramakrishnan, C. R. and Rehof, J., Eds. Lecture Notes in Computer Science, vol. 4963. Springer, 337-340.
[26] Debray, S., Lopez-Garcia, P. and Hermenegildo, M. V.1997. Non-failure analysis for logic programs. In 1997 International Conference on Logic Programming. MIT Press, Cambridge, MA, Cambridge, MA, 48-62.
[27] Dumortier, V., Janssens, G., Simoens, W. and Garca De La Banda, M.1993. Combining a definiteness and a freeness abstraction for CLP languages. In Workshop on Logic Program Synthesis and Transformation.
[28] Eichberg, M., Kahl, M., Saha, D., Mezini, M. and Ostermann, K.2007. Automatic Incrementalization of Prolog Based Static Analyses. Springer, Berlin, Heidelberg, 109-123.
[29] Fähndrich, M. and Logozzo, F.2011. Static contract checking with abstract interpretation. In Proceedings of the 2010 International Conference on Formal Verification of Object-oriented Software, FoVeOOS’10. Lecture Notes in Computer Science, vol. 6528. Springer-Verlag, Berlin, Heidelberg, 10-30. · Zbl 1308.68033
[30] Fedyukovich, G., Gurfinkel, A. and Sharygina, N.2016. Property directed equivalence via abstract simulation. In International Conference on Computer Aided Verification. Springer, 433-453. · Zbl 1411.68065
[31] Gallagher, J., Hermenegildo, M. V., Kafle, B., Klemen, M., Lopez-Garcia, P. and Morales, J.2020. From big-step to small-step semantics and back with interpreter specialization (invited paper). In Proceedings of the Eighth International Workshop on Verification and Program Transformation (VPT 2020). Electronic Proceedings in Theoretical Computer Science (EPTCS). Open Publishing Association (OPA), 50-65. Co-located with ETAPS 2020.
[32] Grebenshchikov, S., Gupta, A., Lopes, N. P., Popeea, C. and Rybalchenko, A.2012. HSF(C): A software verifier based on Horn clauses - (competition contribution). In TACAS, Flanagan, C. and König, B., Eds. LNCS, vol. 7214. Springer, 549-551.
[33] Gurfinkel, A., Kahsai, T., Komuravelli, A. and Navas, J. A.2015. The SeaHorn verification framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, 18-24 July 2015, Proceedings, Part I. LNCS, vol. 9206. Springer, 343-361. and Gallagher, J. P. 2006. Abstract interpretation of PIC programs through logic programming. In SCAM’06, Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation. IEEE Computer Society, 184-196.
[34] Hermenegildo, M. V., Bueno, F., Carro, M., Lopez-Garcia, P., Mera, E., Morales, J. and Puebla, G.2012. An overview of Ciao and its design philosophy. Theory and Practice of Logic Programming12, 1-2, 219-252. · Zbl 1244.68019
[35] Hermenegildo, M. V., Puebla, G., Bueno, F. and Lopez-Garcia, P.2005. Integrated program debugging, verification, and optimization using abstract interpretation (and the Ciao system preprocessor). Science of Computer Programming58, 1-2, 115-140. · Zbl 1076.68540
[36] Hermenegildo, M. V., Puebla, G., Marriott, K. and Stuckey, P.1995. Incremental analysis of logic programs. In International Conference on Logic Programming. MIT Press, 797-811.
[37] Hermenegildo, M. V., Puebla, G., Marriott, K. and Stuckey, P.2000. Incremental analysis of constraint logic programs. ACM Transactions on Programming Languages and Systems22, 2, 187-223.
[38] Jaffar, J. and Lassez, J.-L.1987. Constraint logic programming. In ACM Symposium on Principles of Programming Languages. ACM, 111-119.
[39] Jaffar, J., Murali, V., Navas, J. A. and Santosa, A. E.2012. TRACER: A symbolic execution tool for verification. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, 7-13 July 2012 Proceedings, Madhusudan, P. and Seshia, S. A., Eds. Lecture Notes in Computer Science, vol. 7358. Springer, 758-766.
[40] Kafle, B., Gallagher, J. P. and Morales, J. F.2016. RAHFT: A tool for verifying Horn clauses using abstract interpretation and finite tree automata. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, 17-23 July 2016, Proceedings, Part I,Chaudhuri, S. and Farzan, A., Eds. Lecture Notes in Computer Science, vol. 9779. Springer, 261-268.
[41] Kahn, G.1987. Natural semantics. In Brandenburg, F., Vidal-Naque, G. and Wirsing, M., Eds. Lecture Notes in Computer Science, vol. 247. Springer, 22-39. · Zbl 0635.68007
[42] Kelly, A., Marriott, K., Søndergaard, H. and Stuckey, P.1997. A generic object oriented incremental analyser for constraint logic programs. In Proceedings of the 20th Australasian Computer Science Conference, 92-101.
[43] Khedker, U. P. and Karkare, B.2008. Efficiency, precision, simplicity, and generality in interprocedural data flow analysis: Resurrecting the classical call strings method. In Compiler Construction, 17th International Conference, CC 2008, Budapest, Hungary, March 29-April 6, 2008, L. J. Hendren, Ed. Lecture Notes in Computer Science, vol. 4959. Springer, 213-228.
[44] King, A., Lu, L. and Genaim, S.2006. Detecting determinacy in Prolog programs. In Logic Programming, 22nd International Conference, ICLP 2006, Seattle, WA, USA, 17-20 August 2006, Proceedings, Etalle, S. and Truszczynski, M., Eds. Lecture Notes in Computer Science, vol. 4079. Springer, 132-147. · Zbl 1131.68380
[45] Krall, A. and Berger, T.1995a. Incremental global compilation of Prolog with the vienna abstract machine. In International Conference on Logic Programming. MIT Press.
[46] Krall, A. and Berger, T.1995b. The VAMAI - An abstract machine for incremental global dataflow analysis of Prolog. In ICLP’95 Post-Conference Workshop on Abstract Interpretation of Logic Languages, De La Banda, M. G., Janssens, G., and Stuckey, P., Eds. Science University of Tokyo, Tokyo, 80-91.
[47] Liqat, U., Georgiou, K., Kerrison, S., Lopez-Garcia, P., Hermenegildo, M. V., Gallagher, J. P. and Eder, K.2016. Inferring parametric energy consumption functions at different software levels: ISA vs. LLVM IR. In Foundational and Practical Aspects of Resource Analysis: 4th International Workshop, FOPARA 2015, London, UK, 11 April 2015. Revised Selected Papers, Eekelen, M. V. and Lago, U. D., Eds. Lecture Notes in Computer Science, vol. 9964. Springer, 81-100.
[48] Liqat, U., Kerrison, S., Serrano, A., Georgiou, K., Lopez-Garcia, P., Grech, N., Hermenegildo, M. V. and Eder, K.2014. Energy consumption analysis of programs based on XMOS ISA-level models. In Logic-Based Program Synthesis and Transformation, 23rd International Symposium, LOPSTR 2013, Revised Selected Papers, Gupta, G. and Peña, R., Eds. Lecture Notes in Computer Science, vol. 8901. Springer, 72-90.
[49] Lloyd, J.1987. Foundations of Logic Programming, 2nd extended edition. Springer. · Zbl 0668.68004
[50] Lopez-Garcia, P., Bueno, F. and Hermenegildo, M. V.2010. Automatic inference of determinacy and mutual exclusion for logic programs using mode and type analyses. New Generation Computing28, 2, 117-206. · Zbl 1192.68130
[51] Lopez-Garcia, P., Darmawan, L., Klemen, M., Liqat, U., Bueno, F. and Hermenegildo, M. V.2018. Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption. Theory and Practice of Logic Programming, Special Issue on Computational Logic for Verification18, 2, 167-223.arXiv:1803.04451. · Zbl 1478.68170
[52] Madsen, M., Yee, M. and Lhoták, O.2016. From Datalog to FLIX: A declarative language for fixed points on lattices. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, 13-17 June 2016, Krintz, C. and Berger, E., Eds. ACM, 194-208.
[53] Marlowe, T. and Ryder, B.1990. An efficient hybrid algorithm for incremental data flow analysis. In 17th ACM Symposium on Principles of Programming Languages (POPL). ACM Press, 184-196.
[54] Marriott, K. and Stuckey, P. J.1998. Programming with Constraints: an Introduction. MIT Press. · Zbl 0935.68098
[55] Méndez-Lojo, M., Navas, J. and Hermenegildo, M.2007. A flexible (C)LP-based approach to the analysis of object-oriented programs. In 17th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2007). Lecture Notes in Computer Science, vol. 4915. Springer-Verlag, 154-168. · Zbl 1179.68030
[56] Muthukumar, K. and Hermenegildo, M.1990. Deriving A Fixpoint Computation Algorithm for Top-down Abstract Interpretation of Logic Programs. Technical Report ACT-DC-153-90, Microelectronics and Computer Technology Corporation (MCC), Austin, TX 78759. April.
[57] Muthukumar, K. and Hermenegildo, M.1991. Combined determination of sharing and freeness of program variables through abstract interpretation. In International Conference on Logic Programming (ICLP 1991). MIT Press, 49-63.
[58] Muthukumar, K. and Hermenegildo, M.1992. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming13, 2/3, 315-347. · Zbl 0776.68032
[59] Navas, J., Méndez-Lojo, M. and Hermenegildo, M.2008. Safe upper-bounds inference of energy consumption for Java bytecode applications. In The Sixth NASA Langley Formal Methods Workshop (LFM 08), 29-32. Extended Abstract.
[60] Navas, J., Méndez-Lojo, M. and Hermenegildo, M. V.2007. An efficient, context and path sensitive analysis framework for Java programs. In 9th Workshop on Formal Techniques for Java-like Programs FTfJP 2007.
[61] Navas, J., Méndez-Lojo, M. and Hermenegildo, M. V.2009. User-definable resource usage bounds analysis for Java bytecode. In Proceedings of the Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE’09). Electronic Notes in Theoretical Computer Science, vol. 253. Elsevier - North Holland, 65-82.
[62] Perez-Carrasco, V., Klemen, M., Lopez-Garcia, P., Morales, J. and Hermenegildo, M. V.2020. Cost analysis of smart contracts via parametric resource analysis. In Proceedings of the 27th Static Analysis Symposium (SAS 2020). LNCS. Springer-Verlag.
[63] Plotkin, G.1981. A Structural Approach to Operational Semantics. Technical report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark.
[64] Plotkin, G. D.2004. A structural approach to operational semantics. The Journal of Logic and Algebraic Programming 60-61, 17-139.
[65] Pollock, L. and Soffa, M.1989. An incremental version of iterative data flow analysis. IEEE Transactions on Software Engineering15, 12, 1537-1549.
[66] Puebla, G., Correas, J., Hermenegildo, M. V., Bueno, F., Garca De La Banda, M., Marriott, K. and Stuckey, P. J.2004. A generic framework for context-sensitive analysis of modular programs. In Program Development in Computational Logic, A Decade of Research Advances in Logic-Based Program Development, Bruynooghe, M. and Lau, K., Eds. LNCS, vol. 3049. Springer-Verlag, Heidelberg, Germany, 234-261. · Zbl 1080.68557
[67] Puebla, G. and Hermenegildo, M. V.1996. Optimized algorithms for the incremental analysis of logic programs. In International Static Analysis Symposium (SAS 1996). Lecture Notes in Computer Science, vol. 1145. Springer-Verlag, 270-284.
[68] Ramalingam, G. and Reps, T.1993. categorized bibliography on incremental computation. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL’93. ACM, Charleston, South Carolina.
[69] Reps, T. W., Horwitz, S. and Sagiv, S.1995. Precise interprocedural dataflow analysis via graph reachability. In POPL, 49-61.
[70] Robinson, J. A.1965. machine oriented logic based on the resolution principle. Journal of the ACM12, 23, 23-41. · Zbl 0139.12303
[71] Rosen, B.1981. Linear cost is sometimes quadratic. In Eighth ACM Symposium on Principles of Programming Languages (POPL). ACM Press, 117-124.
[72] Rothenberg, B., Dietsch, D. and Heizmann, M.2018. Incremental verification using trace abstraction. In Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, 29-31 August 2018, A. Podelski, Ed. Lecture Notes in Computer Science, vol. 11002. Springer, 364-382.
[73] Ryder, B.1988. Incremental data-flow analysis algorithms. ACM Transactions on Programming Languages and Systems10, 1, 1-50.
[74] Ryder, B., Marlowe, T. and Paull, M.1988. Conditions for incremental iteration: Examples and counterexamples. Science of Computer Programming11, 1, 1-15. · Zbl 0661.68014
[75] Sery, O., Fedyukovich, G. and Sharygina, N.2012. Incremental upgrade checking by means of interpolation-based function summaries. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, 22-25 October 2012, Cabodi, G. and Singh, S., Eds. IEEE, 114-121.
[76] Sharir, M. and Pnueli, A.1978. Two Approaches to Interprocedural Data Flow Analysis. New York University. Courant Institute of Mathematical Sciences.
[77] Swift, T.2014. Incremental tabling in support of knowledge representation and reasoning. Theory and Practice of Logic Programming14, 4-5, 553-567. · Zbl 1307.68023
[78] Szabó, T., Erdweg, S. and Voelter, M.2016. Inca: A DSL for the definition of incremental program analyses. In Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, 3-7 September 2016, Lo, D., Apel, S. and Khurshid, S., Eds. ACM, 320-331.
[79] Thakur, M. and Nandivada, V. K.2020. Mix your contexts well: Opportunities unleashed by recent advances in scaling context-sensitivity. In Proceedings of the 29th International Conference on Compiler Construction. CC 2020. Association for Computing Machinery, New York, NY, USA, 27-38.
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.