Top

Published in:

2019 | OriginalPaper | Chapter

Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis

Authors : Rémy Boutonnet, Nicolas Halbwachs

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Program analysis by abstract interpretation using relational abstract domains—like polyhedra or octagons—easily extends from state analysis (construction of reachable states) to relational analysis (construction of input-output relations). In this paper, we exploit this extension to enable interprocedural program analysis, by constructing relational summaries of procedures. In order to improve the accuracy of procedure summaries, we propose a method to refine them into disjunctions of relations, these disjunctions being directed by preconditions on input parameters.

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 Static Analysis of Binary Code with Memory Indirections Using Polyhedra

next chapter Exploiting Pointer Analysis in Memory Models for Deductive Verification

This change in the abstract equations could also be obtained by transforming each loop “while c do B” into “if c {do B while c}”, a transformation called “loop inversion” often applied by compilers.

sv-comp.sosy-lab.org/2018/benchmarks.php.

alice.cri.mines-paristech.fr/models.html.

www.mrtc.mdh.se/projects/wcet/benchmarks.html.

Allen, F.E.: Interprocedural analysis and the information derived by it. In: Hackl, C.E. (ed.) IBM 1974. LNCS, vol. 23, pp. 291–321. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07131-8_31CrossRef

Allen, F.E.: Interprocedural data flow analysis. In: IFIP Congress, pp. 398–402 (1974)

Ancourt, C., Coelho, F., Irigoin, F.: A modular static analysis approach to affine loop invariants detection. Electron. Notes Theor. Comput. Sci. 267(1), 3–16 (2010)CrossRef

Apinis, K., Seidl, H., Vojdani, V.: How to combine widening and narrowing for non-monotonic systems of equations. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, Seattle, WA, pp. 377–386, June 2013

Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45789-5_17CrossRef

Barth, J.M.: An interprocedural data flow analysis algorithm. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 119–131. ACM (1977)

Barvinok, A.I.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. Math. Oper. Res. 19(4), 769–779 (1994). https://doi.org/10.1287/moor.19.4.769. https://doi.org/10.1287/moor.19.4.769MathSciNetCrossRefMATH

Becchi, A., Zaffanella, E.: An efficient abstract domain for not necessarily closed polyhedra. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 146–165. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99725-4_11CrossRef

Bourdoncle, F.: Abstract interpretation by dynamic partitioning. J. Funct. Program. 2(4), 407–435 (1992)MathSciNetCrossRef

10.

Boutonnet, R., Asavoae, M.: The WCET analysis using counters - a preliminary assessment. In: Proceedings of 8th JRWRTC, in Conjunction with RTNS14, Versailles, France, October 2014

11.

Clauss, P.: Counting solutions to linear and nonlinear constraints through Ehrhart polynomials: applications to analyze and transform scientific programs. In: Proceedings of the 10th International Conference on Supercomputing, ICS 1996, Philadelphia, PA, USA, 25–28 May 1996, pp. 278–285 (1996). http://doi.acm.org/10.1145/237578.237617

12.

Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symposium on Principles of Programming Languages, POPL 1977, Los Angeles, January 1977

13.

Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conference on Formal Description of Programming Concepts, St. Andrews, NB, Canada. North-Holland Publishing Company (1977)

14.

Cousot, P., Cousot, R.: Relational abstract interpretation of higher order functional programs (extended abstract). In: Proceedings of Actes JTASPEFL 1991 (Bordeaux), Laboratoire Bordelais de Recherche en Informatique (LaBRI), October 1991, pp. 33–36 (1991)

15.

Cousot, P., Cousot, R.: Compositional separate modular static analysis of programs by abstract interpretation. In: Proceedings of SSGRR, pp. 6–10 (2001)

16.

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

17.

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 84–96. ACM (1978)

18.

Flexeder, A., Müller-Olm, M., Petter, M., Seidl, H.: Fast interprocedural linear two-variable equalities. ACM Trans. Programm. Lang. Syst. (TOPLAS) 33(6), 21 (2011)

19.

Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Programm. Lang. Syst. (TOPLAS) 20(5), 1067–1109 (1998)CrossRef

20.

Gulwani, S., Tiwari, A.: Computing procedure summaries for interprocedural analysis. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 253–267. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_18CrossRef

21.

Halbwachs, N.: Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Ph.D. thesis, Université Scientifique et Médicale de Grenoble (1979)

22.

Howe, J.M., King, A.: Polyhedral analysis using parametric objectives. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 41–57. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_6CrossRef

23.

Irigoin, F., Jouvelot, P., Triolet, R.: Semantical interprocedural parallelization: an overview of the pips project. In: ACM International Conference on Supercomputing 25th Anniversary Volume, pp. 143–150. ACM (2014)

24.

Jeannet, B.: Dynamic partitioning in linear relation analysis: application to the verification of reactive systems. Formal Methods Syst. Des. 23(1), 5–37 (2003)CrossRef

25.

Jeannet, B.: INTERPROC analyzer for recursive programs with numerical variables. INRIA. http://pop-art.inrialpes.fr/interproc/interprocweb.cgi. Accessed 06 Nov 2010

26.

Jeannet, B.: Relational interprocedural verification of concurrent programs. Softw. Syst. Model. 12(2), 285–306 (2013)CrossRef

27.

Jeannet, B., Gopan, D., Reps, T.: A relational abstraction for functions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 186–202. Springer, Heidelberg (2005). https://doi.org/10.1007/11547662_14CrossRef

28.

Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 39–50. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48294-6_3CrossRef

29.

Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_52CrossRef

30.

Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 258–273. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27815-3_22CrossRef

31.

Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega calculator and library, version 1.1. 0. College Park, MD 20742, 18 (1996)

32.

Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice. CRC Press, Boca Raton (2009)CrossRef

33.

Kranz, J., Simon, A.: Modular analysis of executables using on-demand heyting completion. Verification, Model Checking, and Abstract Interpretation. LNCS, vol. 10747, pp. 291–312. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_14CrossRef

34.

Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: Proceedings of the 2004 International Symposium on Code Generation and Optimization (CGO 2004), Palo Alto, California, March 2004

35.

Maisonneuve, V.: Convex invariant refinement by control node splitting: a heuristic approach. Electron. Notes Theor. Comput. Sci. 288, 49–59 (2012)CrossRef

36.

Maisonneuve, V., Hermant, O., Irigoin, F.: Computing invariants with transformers: experimental scalability and accuracy. Electron. Notes Theor. Comput. Sci. 307, 17–31 (2014)MathSciNetCrossRef

37.

Maréchal, A., Monniaux, D., Périn, M.: Scalable minimizing-operators on polyhedra via parametric linear programming. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 212–231. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66706-5_11CrossRef

38.

Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31987-0_2CrossRef

39.

Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE/IEEE CS Press, October 2001

40.

Müller-Olm, M., Rüthing, O., Seidl, H.: Checking herbrand equalities and beyond. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 79–96. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_6CrossRefMATH

41.

Müller-Olm, M., Seidl, H.: Computing interprocedurally valid relations in affine programs. Princ. Prog. Lang. (2004)

42.

Müller-Olm, M., Seidl, H., Steffen, B.: Interprocedural analysis (almost) for free. Univ. Dekanat Informatik (2004)

43.

Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77505-8_26CrossRef

44.

Popeea, C., Chin, W.N.: Dual analysis for proving safety and finding bugs. In: Proceedings of the 2010 ACM Symposium on Applied Computing, pp. 2137–2143. ACM (2010)

45.

Popeea, C., Chin, W.N.: Dual analysis for proving safety and finding bugs. Sci. Comput. Program. 78(4), 390–411 (2013)CrossRef

46.

Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 49–61. ACM (1995)

47.

Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. (TOPLAS) 29(5), 26 (2007)CrossRef

48.

Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. New York University, Courant Institute of Mathematical Sciences, Computer Science Department (1978)

49.

Singh, G., Püschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: POPL, pp. 46–59 (2017)

50.

Sotin, P., Jeannet, B.: Precise interprocedural analysis in the presence of pointers to the stack. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 459–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_24CrossRef

51.

Spillman, T.C.: Exposing side-effects in a PL/I optimizing compiler. In: IFIP Congress, vol. 1, pp. 376–381 (1971)

52.

Yorsh, G., Yahav, E., Chandra, S.: Generating precise and concise procedure summaries. In: ACM SIGPLAN Notices, vol. 43, pp. 221–234. ACM (2008)

53.

Zhang, X., Mangal, R., Naik, M., Yang, H.: Hybrid top-down and bottom-up interprocedural analysis. In: ACM SIGPLAN Notices, vol. 49, pp. 249–258. ACM (2014)CrossRef

Title: Disjunctive Relational Abstract Interpretation for Interprocedural Program Analysis
Authors: Rémy Boutonnet
Nicolas Halbwachs
Publisher: Springer International Publishing
Book: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-11244-8

Electronic ISBN: 978-3-030-11245-5

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-11245-5_7

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"

Premium Partner