Abstract
Interprocedural analyses are compositional when they compute over-approximations of procedures in a bottom-up fashion. These analyses are usually more scalable than top-down analyses, which compute a different procedure summary for every calling context. However, compositional analyses are rare in practice as it is difficult to develop them with enough precision.
We establish a connection between compositional analyses and modular lattices, which require certain associativity between the lattice join and meet operations, and use it to develop a compositional version of the connection analysis by Ghiya and Hendren. Our version is slightly more conservative than the original top-down analysis in order to meet our modularity requirement. When applied to real-world Java programs our analysis scaled much better than the original top-down version: The top-down analysis times out in the largest two of our five programs, while ours incurred only 2–5% of precision loss in the remaining programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
The subscripts p and g are used as mnemonics: \(d_p\) is used to partition a connection set and \(d_g\) to group two connection sets together.
- 2.
For example, let \(d_1 = \{\{x,z\},\{y\}\}\), \(d_2=\{\{x,y\},\{z\}\}\), and \(d_3=\{\{y,z\}, \{x\} \})\). Then \(d_1 \sqcap (d_2 \sqcup d_3) = d_1 \sqcap \{\{ x,y,z \} \} = d_1\), but \((d_1 \sqcap d_2) \sqcup (d_1 \sqcap d_3) = \{ \{ x\},\{y\}, \{z\} \}\).
- 3.
We analyze recursive procedures in a standard way using a fixpoint computation. As a result, a recursive procedure might be analyzed more than once. However, and unlike in top-down analyses, the procedure is analyzed only using a single input, namely \(\iota _{\mathsf {entry}}\), defined in Sect. 5.2.
- 4.
We note that if we only use elements in the analysis which are smaller than all the meet elements, then our analysis would become flow-insensitive. Let \(d,P_1,G_1,P_2,G_2\) be abstract elements such that \(P_1\) and \(P_2\) are modular elements, \(d \sqsubseteq P_1\), \(((d \sqcap P_1) \sqcup G_1) \sqsubseteq P_2\), \(((d \sqcap P_2) \sqcup G_2) \sqsubseteq P_1\). It holds that \(G_1 \sqsubseteq P_2\), \(G_2 \sqsubseteq P_1\), and thus \( (((d \sqcap P_1) \sqcup G_1) \sqcap P_2) \sqcup G_2 = (((d \sqcap P_1) \sqcap P_2) \sqcup G_1) \sqcup G_2 = (d \sqcap P_2 \sqcap P_1) \sqcup G_2 \sqcup G_1 = ((d \sqcap P_2) \sqcup G_2) \sqcap P_1) \sqcup G_1 \ . \) (This is in fact the case if the meet elements are \(\top \).) Note that this would imply that \({[\![{x=null}]\!]^\sharp } \circ {[\![{x = y}]\!]^\sharp } = {[\![{x = y}]\!]^\sharp }\circ {[\![{x=null}]\!]^\sharp }\), which is neither desired nor the case in our analysis.
References
Ball, T., Rajamani, S.: Bebop: a path-sensitive interprocedural dataflow engine. In: PASTE (2001)
Bodden, E.: Inter-procedural data-flow analysis with ifds/ide and soot. In: SOAP (2012)
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)
Castelnuovo, G.: Modular lattices for compositional interprocedural analysis. Master’s thesis, School of Computer Science, Tel Aviv University (2012)
Chatterjee, R., Ryder, B.G., Landi, W.: Relevant context inference. In: POPL (1999)
Codish, M., Debray, S., Giacobazzi, R.: Compositional analysis of modular logic programs. In: POPL (1993)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Formal Descriptions of Programming Concepts (1978)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)
Cousot, P., Cousot, R.: Modular static program analysis. In: CC (2002)
Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: PLDI (2011)
Dolby, J., Fink, S., Sridharan, M.: T. J. Watson Libraries for Analysis (2006)
Fischer, C.N., Cytron, R.K., LeBlanc, R.J.: Crafting A Compiler. Addison-Wesley, New York (2009)
Ghiya, R., Hendren, L.: Connection analysis: a practical interprocedural heap analysis for C. IJPP 24(6), 547–578 (1996)
Giacobazzi, R.: Abductive analysis of modular logic programs. JLP 8(4), 457–483 (1998)
Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. TCS 216(1), 159–211 (1999)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract domains condensing. TOCL 6(1), 33–60 (2005)
Giacobazzi, R., Scozzari, F.: A logical model for relational abstract domains. TOPLAS 20(5), 1067–1109 (1998)
Gratzer, G.: General Lattice Theory. Birkhauser Verlag, Berlin (1978)
Gulavani, B., Chakraborty, S., Ramalingam, G., Nori, A.: Bottom-up shape analysis using LISF. TOPLAS,33(5) (2011)
Jacobs, D., Langen, A.: Static analysis of logic programs for independent and parallelism. JLP 13(2–3), 291–314 (1992)
Livshits, V.B., Lam, M.S.: Finding security vulnerabilities in java applications with static analysis. In: USENIX Security (2005)
Madhavan, R., Ramalingam, G., Vaswani, K.: Purity analysis: an abstract interpretation formulation. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 7–24. Springer, Heidelberg (2011)
Marriott, K., Søndergaard, H.: Precise and efficient groundness analysis for logic programs. LOPLAS 2(1–4), 181–196 (1993)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)
Naik, M.: Chord: A program analysis platform for Java (2006)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL (1995)
Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. TCS 167(1), 131–170 (1996)
Sălcianu, A., Rinard, M.: Purity and side effect analysis for java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 199–215. Springer, Heidelberg (2005)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications (1981)
Simon, A.: Deriving a complete type inference for hindley-milner and vector sizes using expansion. In: PEPM (2013)
Whaley, J., Rinard, M.: Compositional pointer and escape analysis for java programs. In: OOPSLA (1999)
Acknowledgments
We thank the anonymous referees for their helpful comments. This work was supported by EU FP7 project ADVENT (308830), ERC grant agreement no. [321174-VSSC], Broadcom Foundation and Tel Aviv University Authentication Initiative, DARPA award #FA8750-12-2-0020 and NSF award #1253867.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Castelnuovo, G., Naik, M., Rinetzky, N., Sagiv, M., Yang, H. (2015). Modularity in Lattices: A Case Study on the Correspondence Between Top-Down and Bottom-Up Analysis. In: Blazy, S., Jensen, T. (eds) Static Analysis. SAS 2015. Lecture Notes in Computer Science(), vol 9291. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48288-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-662-48288-9_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48287-2
Online ISBN: 978-3-662-48288-9
eBook Packages: Computer ScienceComputer Science (R0)