No CrossRef data available.
Article contents
Incremental and Modular Context-sensitive Analysis
Published online by Cambridge University Press: 19 January 2021
Abstract
Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.
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.
Keywords
Information
- Type
- Original Article
- Information
- Copyright
- © The Author(s), 2021. Published by Cambridge University Press
Footnotes
*
Research partially funded by MINECO MICINN PID2019-108528RB-C21 ProCode project, FPU grant 16/04811, and the Madrid M141047003 N-GREENS and P2018/TCS-4339 BLOQUES-CM programs. We are also grateful to the anonymous reviewers, editors, and to Ignacio Fábregas for their comments.
References
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
Apt, K. R. 1990. Introduction to logic programming. In Handbook of Theoretical Computer Science, J. van Leeuwen, Ed. Elsevier, 493–576.Google Scholar
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.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
Bossi, A., Gabbrieli, M., Levi, G. and Meo, M. 1994. A compositional semantics for logic programs. Theoretical Computer Science 122, 1, 2, 3–47.CrossRefGoogle Scholar
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.Google Scholar
Bruynooghe, M. 1991. A practical framework for the abstract interpretation of logic programs. Journal of Logic Programming 10, 91–124.CrossRefGoogle Scholar
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.CrossRefGoogle Scholar
Burke, M. 1990. An interval-based approach to exhaustive and incremental interprocedural data-flow analysis. ACM Transactions on Programming Languages and Systems 12, 3, 341–395.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
Eichberg, M., Kahl, M., Saha, D., Mezini, M. and Ostermann, K. 2007. Automatic Incrementalization of Prolog Based Static Analyses. Springer, Berlin, Heidelberg, 109–123.Google Scholar
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.Google Scholar
Fedyukovich, G., Gurfinkel, A. and Sharygina, N. 2016. Property directed equivalence via abstract simulation. In International Conference on Computer Aided Verification. Springer, 433–453.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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 Programming 12, 1–2, 219–252.CrossRefGoogle Scholar
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 Programming 58, 1–2, 115–140.CrossRefGoogle Scholar
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.Google Scholar
Hermenegildo, M. V., Puebla, G., Marriott, K. and Stuckey, P. 2000. Incremental analysis of constraint logic programs. ACM Transactions on Programming Languages and Systems 22, 2, 187–223.CrossRefGoogle Scholar
Jaffar, J. and Lassez, J.-L. 1987. Constraint logic programming. In ACM Symposium on Principles of Programming Languages. ACM, 111–119.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
Krall, A. and Berger, T. 1995a. Incremental global compilation of Prolog with the vienna abstract machine. In International Conference on Logic Programming. MIT Press.Google Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
Lloyd, J. 1987. Foundations of Logic Programming, 2nd extended edition. Springer.CrossRefGoogle Scholar
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 Computing 28, 2, 117–206.CrossRefGoogle Scholar
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 Verification 18, 2, 167–223.arXiv:1803.04451.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Marriott, K. and Stuckey, P. J. 1998. Programming with Constraints: an Introduction. MIT Press.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
Muthukumar, K. and Hermenegildo, M. 1992. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming 13, 2/3, 315–347.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
Plotkin, G. 1981. A Structural Approach to Operational Semantics. Technical report DAIMI FN-19, Computer Science Department, Aarhus University, Denmark.Google Scholar
Plotkin, G. D. 2004. A structural approach to operational semantics. The Journal of Logic and Algebraic Programming 60–61, 17–139.Google Scholar
Pollock, L. and Soffa, M. 1989. An incremental version of iterative data flow analysis. IEEE Transactions on Software Engineering 15, 12, 1537–1549.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
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.CrossRefGoogle Scholar
Reps, T. W., Horwitz, S. and Sagiv, S. 1995. Precise interprocedural dataflow analysis via graph reachability. In POPL, 49–61.Google Scholar
Robinson, J. A. 1965. machine oriented logic based on the resolution principle. Journal of the ACM 12, 23, 23–41.CrossRefGoogle Scholar
Rosen, B. 1981. Linear cost is sometimes quadratic. In Eighth ACM Symposium on Principles of Programming Languages (POPL). ACM Press, 117–124.Google Scholar
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.Google Scholar
Ryder, B. 1988. Incremental data-flow analysis algorithms. ACM Transactions on Programming Languages and Systems 10, 1, 1–50.CrossRefGoogle Scholar
Ryder, B., Marlowe, T. and Paull, M. 1988. Conditions for incremental iteration: Examples and counterexamples. Science of Computer Programming 11, 1, 1–15.CrossRefGoogle Scholar
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.Google Scholar
Sharir, M. and Pnueli, A. 1978. Two Approaches to Interprocedural Data Flow Analysis. New York University. Courant Institute of Mathematical Sciences.Google Scholar
Swift, T. 2014. Incremental tabling in support of knowledge representation and reasoning. Theory and Practice of Logic Programming 14, 4–5, 553–567.CrossRefGoogle Scholar
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.Google Scholar
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.Google Scholar
Garcia-Contreras et al. supplementary material
Garcia-Contreras et al. supplementary material
PDF
1.3 MB
You have
Access
- 12
- Cited by