Top

Published in:

2020 | OriginalPaper | Chapter

Incremental Abstract Interpretation

Authors : Helmut Seidl, Julian Erhard, Ralf Vogler

Published in: From Lambda Calculus to Cybersecurity Through Program Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Non-incremental static analysis by abstract interpretation has to be rerun every time the code to be analyzed changes. For large code bases, this incurs a significant overhead, in particular, if the individual changes to the code are small. In order to accelerate the analysis on changing code bases, incremental static analysis reuses analysis results computed for earlier versions of the source code where possible. We show that this behavior can seamlessly be achieved for the analysis of C programs if a local generic solver such as the top-down solver is used as the fixed-point engine. This solver maintains a set of stable unknowns for which fixpoint iteration has already stabilized and it recursively destabilizes dependent unknowns on change. We indicate how this machinery can be applied to selectively invalidate results for those unknowns that may be directly or indirectly affected by program changes. We also explain the technical difficulties faced when realizing this basic idea within an analysis infra-structure such as Goblint. We also report the results of a preliminary experimental evaluation concerning the impact of incrementalization on analysis performance.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Galois Connections for Recursive Types

next chapter Correctly Slicing Extended Finite State Machines

http://www.figlet.org/.

https://github.com/cmatsuoka/figlet.

Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing. Sci. Comput. Program. 120, 1–24 (2016). https://doi.org/10.1016/j.scico.2015.12.005CrossRef

Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a swiss army knife for program analysis. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 157–172. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35182-2_12CrossRef

Apinis, K., Seidl, H., Vojdani, V.: Enhancing top-down solving with widening and narrowing. In: Probst, C.W., Hankin, C., Hansen, R.R. (eds.) Semantics, Logics, and Calculi. LNCS, vol. 9560, pp. 272–288. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-27810-0_14CrossRefMATH

Arzt, S., Bodden, E.: Reviser: efficiently updating IDE-/IFDS-based data-flow analyses in response to incremental program changes. In: Jalote, P., Briand, L.C., van der Hoek, A. (eds.) 36th International Conference on Software Engineering, ICSE 2014, Hyderabad, India, 31 May –07 June 2014, pp. 288–298. ACM (2014). https://doi.org/10.1145/2568225.2568243

Bolduc, C.: Lessons learned: using a static analysis tool within a continuous integration system. In: 2016 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), pp. 37–40. IEEE (2016)

Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive programs. In: Neuhold, E. (ed.) Formal Descriptions of Programming Concepts, pp. 237–277. North-Holland Publishing Company, Amsterdam (1977)MATH

Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55844-6_142CrossRefMATH

Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159–179. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_13CrossRef

Emanuelsson, P., Nilsson, U.: A comparative study of industrial static analysis tools. Electron. Notes Theor. Comput. Sci. 217, 5–21 (2008)CrossRef

10.

Frielinghaus, S.S., Seidl, H., Vogler, R.: Enforcing termination of interprocedural analysis. Formal Methods Syst. Design 53(2), 313–338 (2018). https://doi.org/10.1007/s10703-017-0288-5CrossRefMATH

11.

Garcia-Contreras, I., Morales, J.F., Hermenegildo, M.V.: Towards incremental and modular context-sensitive analysis. In: Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). OpenAccess Series in Informatics (OASIcs). Dagstuhl Press, July 2018. (Extended Abstract)

12.

Hermenegildo, M.V., Puebla, G., Marriott, K., Stuckey, P.: Incremental analysis of constraint logic programs. ACM Trans. Program. Lang. Syst. 22(2), 187–223 (2000)CrossRef

13.

Jones, N.D., Muchnick, S.S.: A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In: DeMillo, R.A. (ed.) Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 1982, pp. 66–74. ACM Press (1982). https://doi.org/10.1145/582153.582161

14.

Muthukumar, K., Hermenegildo, M.: 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, April 1990

15.

Karbyshev, A.: Monadic parametricity of second-order functionals. Ph.D. thesis, Technical University Munich (2013). http://nbn-resolving.de/urn:nbn:de:bvb:91-diss-20130923-1144371-0-6

16.

Le Charlier, B., Van Hentenryck, P.: A universal top-down fixpoint algorithm. Technical report CS-92-25. CS Department, Brown University (1992)

17.

Liqat, U., et al.: Energy consumption analysis of programs based on XMOS ISA-level models. In: Gupta, G., Peña, R. (eds.) LOPSTR 2013. LNCS, vol. 8901, pp. 72–90. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-14125-1_5CrossRef

18.

O’Hearn, P.W.: Continuous reasoning: scaling the impact of formal methods. In: Dawar, A., Grädel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09–12 July 2018, pp. 13–25. ACM (2018). https://doi.org/10.1145/3209108.3209109

19.

Puebla, G., Hermenegildo, M.: Optimized algorithms for incremental analysis of logic programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 270–284. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61739-6_47CrossRef

20.

Ramalingam, G., Reps, T.W.: A categorized bibliography on incremental computation. In: Deusen, M.S.V., Lang, B. (eds.) Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, pp. 502–510. ACM Press (1993). https://doi.org/10.1145/158511.158710

21.

Ramalingam, G., Reps, T.W.: An incremental algorithm for a generalization of the shortest-path problem. J. Algorithms 21(2), 267–305 (1996). https://doi.org/10.1006/jagm.1996.0046MathSciNetCrossRefMATH

22.

Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Cytron, R.K., Lee, P. (eds.) Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, 23–25 January 1995, pp. 49–61. ACM Press (1995). https://doi.org/10.1145/199448.199462

23.

Seidl, H., Vogler, R.: Three improvements to the top-down solver. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, 03–05 September 2018, pp. 21:1–21:14. ACM (2018). https://doi.org/10.1145/3236950.3236967

24.

Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, pp. 189–233. Prentice-Hall, Englewood Cliffs (1981)

25.

Vojdani, V., Apinis, K., Rõtov, V., Seidl, H., Vene, V., Vogler, R.: Static race detection for device drivers: the Goblint approach. In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, pp. 391–402. ACM (2016). https://doi.org/10.1145/2970276.2970337

Title: Incremental Abstract Interpretation
Authors: Helmut Seidl
Julian Erhard
Ralf Vogler
Publisher: Springer International Publishing
Book: From Lambda Calculus to Cybersecurity Through Program Analysis
Print ISBN: 978-3-030-41102-2

Electronic ISBN: 978-3-030-41103-9

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-41103-9_5

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"