Abstract
A function-modular analysis is presented that computes precise function summaries in the presence of pointers and indirect calls. Our approach computes several summaries for a function, each specialized to a particular input property. A call site combines the effect of several summaries, based on what properties hold. The key novelty is that the properties are tailored to the function being analyzed. Moreover, they are represented in a domain-agnostic way by using Herbrand terms with variables. Callers instantiate these variables, based on their state. For each variable instantiation, a new summary is computed. Since the computed summaries are exact with respect to the property, our fixpoint computation resembles the process of Heyting completion where a domain is iteratively refined to be complete wrt. the intersection with a property. Our approach combines the advantages of a modular analysis, such as scalability and context-sensitivity, with the ability to compute meaningful summaries for functions that call other functions via pointers that were passed as arguments. We illustrate our framework in the context of inferring indirect callees in x86 executables.
Access provided by CONRICYT-eBooks. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Amato, G., Scozzari, F., Seidl, H., Apinis, K., Vojdani, V.: Efficiently intertwining widening and narrowing. Sci. Comput. Program. 120, 1–24 (2016)
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation, San Diego, California, USA. ACM, June 2003
Brauer, J., King, A.: Automatic abstraction for intervals using boolean formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 167–183. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15769-1_11
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, Los Angeles, California, USA, pp. 238–252. ACM, January 1977
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages , San Antonio, Texas, USA, pp.269–282. ACM, January 1979
Cousot, Patrick, Cousot, Radhia: Modular static program analysis. In: Horspool, R.Nigel (ed.) CC 2002. LNCS, vol. 2304, pp. 159–179. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_13
Cousot, P., Cousot, R., Fähndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 128–148. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_10
Das, A., Lahiri, S.K., Lal, A., Li, Y.: Angelic verification: precise verification modulo unknowns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 324–342. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_19
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making Abstract Domains Condensing. Trans. Comput. Log. 6(1), 33–60 (2005)
Giacobazzi, R., Scozzari, F.: A Logical Model for Relational Abstract Domains. Transactions on Programming Languages and Systems 20(5), 1067–1109 (1998)
Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_20
Kranz, J., Sepp, A., Simon, A.: GDSL: A universal toolkit for giving semantics to machine language. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 209–216. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03542-0_15
Kranz, J., Simon, A. : Structure-preserving compilation: efficient integration of functional DSLs into legacy systems. In: Principles and Practice of Declarative Programming. ACM, September 2014
Marriott, K., Søndergaard, H.: Precise and Efficient Groundness Analysis for Logic Programs. ACM Lett. Program. Lang. Syst. 2, 181–196 (1993)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Principles of Programming Languages, pp. 330–341. ACM, January 2004
Reps, T., Horwitz, S., Sagiv, M. : Precise interprocedural dataflow analysis via graph reachability. In Principles of Programming Languages, San Francisco, California, USA, pp. 49–61. ACM (1995)
Sharir, M., Pnueli, A.: Two Approaches to Interprocedural Data Flow Analysis, ch. 7, pp. 189–234. Prentice-Hall, Englewood Cliffs, NJ (1981)
Shivers, O.: Control-Flow Analysis of Higher-Order Languages. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1991
Siegel, H., Simon, A.: FESA: fold- and expand-based shape analysis. In: Jhala, R., De Bosschere, K. (eds.) CC 2013. LNCS, vol. 7791, pp. 82–101. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37051-9_5
Simon, A.: Deriving a Complete Type Inference for Hindley-Milner and Vector Sizes using Expansion. Science of Computer Programming 95(pt. 2), 254–271 (2014)
Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174–192. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_17
Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 366–382. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61739-6_53
Xu, Z., Reps, T., Miller, B.P.: Typestate checking of machine code. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 335–351. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45309-1_22
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
Kranz, J., Simon, A. (2018). Modular Analysis of Executables Using On-Demand Heyting Completion. In: Dillig, I., Palsberg, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2018. Lecture Notes in Computer Science(), vol 10747. Springer, Cham. https://doi.org/10.1007/978-3-319-73721-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-73721-8_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-73720-1
Online ISBN: 978-3-319-73721-8
eBook Packages: Computer ScienceComputer Science (R0)