Skip to main content

2017 | OriginalPaper | Buchkapitel

Conjunctive Abstract Interpretation Using Paramodulation

verfasst von : Or Ozeri, Oded Padon, Noam Rinetzky, Mooly Sagiv

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Scaling static analysis is one of the main challenges for program verification in general and for abstract interpretation in particular. One way to compactly represent a set of states is using a formula in conjunctive normal form (CNF). This can sometimes save exponential factors. Therefore, CNF formulae are commonly used in manual program verification and symbolic reasoning. However, it is not used in abstract interpretation, due to the complexity of reasoning about the effect of program statements when the states are represented this way.
We present algorithms for performing abstract interpretation on CNF formulae recording equality and inequalities of ground terms. Here, terms correspond to the values of variables and of addresses and contents of dynamically allocated memory locations, and thus, a formula can represent pointer equalities and inequalities. The main idea is the use of the rules of paramodulation as a basis for an algorithm that computes logical consequences of CNF formulae, and the application of the algorithm to perform joins and transformers.
The algorithm was implemented and used for reasoning about low level programs. We also show that our technique can be used to implement best transformers for a variant of Connection Analysis via a non-standard interpretation of equality.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Fußnoten
1
Function congruence means that if x and y are equal then, for any function \(f(\cdot )\), so are f(x) and f(y). Congruence naturally generalizes to functions with multiple arguments.
 
2
Our analysis does not prove memory safety. Thus, our results can be adapted to the case where such an operation leads to an error state in the following way: The properties we infer hold unless the program performs a memory error, e.g., dereferencing a null-valued pointer or accessing an unallocated memory address.
 
3
A ground formula is a formula which does not contain free variables.
 
4
We assume the reader is familiar with the notions of well-formedness, ranking and meaning of terms in FOL, and do not formalize them here. For a formal definition, see, e.g., [15, Chap. 7].
 
5
\({\text {remSym}}( SR (\cdot ,\mathcal {F})\) is the obvious extension of the symbol elimination function \({\text {remSym}}(\cdot ,v)\), described in Sect. 4, from a single symbol v to the removal of all symbols coming from \(\mathcal {F}\).
 
Literatur
1.
Zurück zum Zitat Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1988)MATH Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques and Tools. Addison-Wesley, Reading (1988)MATH
2.
Zurück zum Zitat Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). doi:10.1007/11804192_17 CrossRef Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). doi:10.​1007/​11804192_​17 CrossRef
3.
Zurück zum Zitat Castelnuovo, G., Naik, M., Rinetzky, N., Sagiv, M., Yang, H.: Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 252–274. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48288-9_15 CrossRef Castelnuovo, G., Naik, M., Rinetzky, N., Sagiv, M., Yang, H.: Modularity in lattices: a case study on the correspondence between top-down and bottom-up analysis. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 252–274. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-48288-9_​15 CrossRef
4.
Zurück zum Zitat Codish, M., Demoen, B.: Analyzing logic programs using "PROP"-ositional logic programs and a magic wand. J. Log. Program. 25(3), 249–274 (1995)MathSciNetCrossRefMATH Codish, M., Demoen, B.: Analyzing logic programs using "PROP"-ositional logic programs and a magic wand. J. Log. Program. 25(3), 249–274 (1995)MathSciNetCrossRefMATH
5.
Zurück zum Zitat Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixed points. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252 (1977) Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixed points. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252 (1977)
6.
Zurück zum Zitat Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 269–282. ACM Press, New York (1979) Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 269–282. ACM Press, New York (1979)
7.
Zurück zum Zitat del Val, A.: A new method for consequence finding and compilation in restricted languages. In: Hendler, J., Subramanian, D. (eds.) Proceedings of 16th National Conference on Artificial Intelligence and 11th Conference on Innovative Applications of Artificial Intelligence, 18–22 July 1999, Orlando, Florida, USA, pp. 259–264. AAAI Press/The MIT Press (1999) del Val, A.: A new method for consequence finding and compilation in restricted languages. In: Hendler, J., Subramanian, D. (eds.) Proceedings of 16th National Conference on Artificial Intelligence and 11th Conference on Innovative Applications of Artificial Intelligence, 18–22 July 1999, Orlando, Florida, USA, pp. 259–264. AAAI Press/The MIT Press (1999)
8.
Zurück zum Zitat Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006). doi:10.1007/11691372_19 CrossRef Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006). doi:10.​1007/​11691372_​19 CrossRef
9.
Zurück zum Zitat Ghiya, R., Hendren, L.J.: Connection analysis: a practical interprocedural heap analysis for C. In: Huang, C.-H., Sadayappan, P., Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1995. LNCS, vol. 1033, pp. 515–533. Springer, Heidelberg (1996). doi:10.1007/BFb0014221 CrossRef Ghiya, R., Hendren, L.J.: Connection analysis: a practical interprocedural heap analysis for C. In: Huang, C.-H., Sadayappan, P., Banerjee, U., Gelernter, D., Nicolau, A., Padua, D. (eds.) LCPC 1995. LNCS, vol. 1033, pp. 515–533. Springer, Heidelberg (1996). doi:10.​1007/​BFb0014221 CrossRef
10.
Zurück zum Zitat Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theoret. Comput. Sci. 216(1–2), 159–211 (1999)MathSciNetCrossRefMATH Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theoret. Comput. Sci. 216(1–2), 159–211 (1999)MathSciNetCrossRefMATH
11.
Zurück zum Zitat Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst. 20(5), 1067–1109 (1998)CrossRef Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. ACM Trans. Program. Lang. Syst. 20(5), 1067–1109 (1998)CrossRef
12.
Zurück zum Zitat Inoue, K.: Consequence-finding based on ordered linear resolution. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of 12th International Joint Conference on Artificial Intelligence, 24–30 August 1991, Sydney, Australia, pp. 158–164. Morgan Kaufmann (1991) Inoue, K.: Consequence-finding based on ordered linear resolution. In: Mylopoulos, J., Reiter, R. (eds.) Proceedings of 12th International Joint Conference on Artificial Intelligence, 24–30 August 1991, Sydney, Australia, pp. 158–164. Morgan Kaufmann (1991)
13.
Zurück zum Zitat Marriott, K., Søndergaard, H.: Precise and efficient groundness analysis for logic programs. LOPLAS 2(1–4), 181–196 (1993)CrossRefMATH Marriott, K., Søndergaard, H.: Precise and efficient groundness analysis for logic programs. LOPLAS 2(1–4), 181–196 (1993)CrossRefMATH
15.
Zurück zum Zitat Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 1. Elsevier Science Publishers B. V., Amsterdam (2001)MATH Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning, vol. 1. Elsevier Science Publishers B. V., Amsterdam (2001)MATH
18.
Zurück zum Zitat Simon, L., del Val, A.: Efficient consequence finding. In: Nebel, B. (ed.) Proceedings of 17th International Joint Conference on Artificial Intelligence, IJCAI 2001, 4–10 August 2001, Seattle, Washington, USA, pp. 359–370. Morgan Kaufmann (2001) Simon, L., del Val, A.: Efficient consequence finding. In: Nebel, B. (ed.) Proceedings of 17th International Joint Conference on Artificial Intelligence, IJCAI 2001, 4–10 August 2001, Seattle, Washington, USA, pp. 359–370. Morgan Kaufmann (2001)
19.
Zurück zum Zitat Smaragdakis, Y., Balatsouras, G.: Pointer analysis. Found. Trends Program. Lang. 2(1), 1–69 (2015)CrossRef Smaragdakis, Y., Balatsouras, G.: Pointer analysis. Found. Trends Program. Lang. 2(1), 1–69 (2015)CrossRef
Metadaten
Titel
Conjunctive Abstract Interpretation Using Paramodulation
verfasst von
Or Ozeri
Oded Padon
Noam Rinetzky
Mooly Sagiv
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-52234-0_24