Abstract
A static shape analysis is presented that can prove the absence of NULL- and dangling pointer dereferences in standard algorithms on lists, trees and graphs. It is conceptually simpler than other analyses that use symbolically represented logic to describe the heap. Instead, it represents the heap as a single graph and a Boolean formula. The key idea is to summarize two nodes by calculating their common points-to information, which is done using the recently proposed fold and expand operations. The force of this approach is that both, fold and expand, retain relational information between points-to edges, thereby essentially inferring new shape invariants. We show that highly precise shape invariants can be inferred using off-the-shelf SAT-solvers. Cheaper approximations may augment standard points-to analysis used in compiler optimisations.
This work was supported by DFG Emmy Noether programme SI 1579/1.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Balakrishnan, G., Reps, T.: Recency-Abstraction for Heap-Allocated Storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006)
Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W., Wies, T., Yang, H.: Shape Analysis for Composite Data Structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 178–192. Springer, Heidelberg (2007)
Berndl, M., Lhoták, O., Qian, F., Hendren, L., Umanee, N.: Points-to analysis using BDDs. In: Programming Language Design and Implementation, pp. 103–114. ACM, San Diego (2003)
Boquist, U., Johnsson, T.: The Grin Project: A Highly Optimising Back end for Lazy Functional Languages. In: Kluge, W.E. (ed.) IFL 1996. LNCS, vol. 1268, pp. 58–84. Springer, Heidelberg (1997)
Brauer, J., King, A., Kriener, J.: Existential Quantification as Incremental SAT. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 191–207. Springer, Heidelberg (2011)
Brauer, J., Simon, A.: Inferring Definite Counterexamples through Under-Approximation. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 54–69. Springer, Heidelberg (2012)
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional Shape Analysis by means of Bi-Abduction. In: Principles of Programming Languages, Savannah, Georgia, USA, ACM (2009)
Chang, B.-Y.E., Rival, X.: Relational Inductive Shape Analysis. In: Principles of Programming Languages, pp. 247–260. ACM (2008)
Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: Principles of Programming Languages, pp. 269–282. ACM, San Antonio (1979)
Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Constraints among Variables of a Program. In: Principles of Programming Languages, Tucson, Arizona, USA, pp. 84–97. ACM (1978)
Hind, M., Pioli, A.: Which Pointer Analysis Should I Use? In: International Symposium on Software Testing and Analysis, Portland, Oregon, USA, pp. 113–123. ACM (2000)
McCloskey, B., Reps, T., Sagiv, M.: Statically Inferring Complex Heap, Array, and Numeric Invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 71–99. Springer, Heidelberg (2010)
McCloskey, B.: Practical Shape Analysis. PhD thesis, EECS Department, University of California, Berkeley (May 2010)
Nystrom, E.M., Kim, H.S., Hwu, W.W.: Importance of Heap Specialization in Pointer Analysis. In: Flanagan, C., Zeller, A. (eds.) Program Analysis for Software Tools and Engineering. ACM, Washington, DC (2004)
Podelski, A., Wies, T.: Boolean Heaps. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 268–283. Springer, Heidelberg (2005)
Reps, T., Sagiv, M., Loginov, A.: Finite Differencing of Logical Formulas for Static Analysis. Transactions on Programming Languages and Systems 32, 24:1–24:55 (2010)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Logic in Computer Science, Copenhagen, Denmark, pp. 55–74. IEEE (2002)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric Shape Analysis via 3-Valued Logic. Transactions on Programming Languages and Systems 24(3), 217–298 (2002)
Siegel, H., Simon, A.: Summarized Dimensions Revisited. In: Mauborgne, L. (ed.) Workshop on Numeric and Symbolic Abstract Domains, ENTCS, Venice, Italy. Springer (2011)
Simon, A.: Splitting the Control Flow with Boolean Flags. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 315–331. Springer, Heidelberg (2008)
Tsai, M.-C.: Categorization and Analyzing Linked Structures. PhD thesis, University of Illinois at Urbana-Champaign, Champaign, Illinois, USA (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Siegel, H., Simon, A. (2013). FESA: Fold- and Expand-Based Shape Analysis. In: Jhala, R., De Bosschere, K. (eds) Compiler Construction. CC 2013. Lecture Notes in Computer Science, vol 7791. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37051-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-37051-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37050-2
Online ISBN: 978-3-642-37051-9
eBook Packages: Computer ScienceComputer Science (R0)