Abstract
A singleton abstraction occurs in a program analysis when some results of the analysis are known to be exact: an abstract binding corresponds to a single concrete binding. In this paper, we develop a novel approach to constructing singleton abstractions via relative store fragments. Each store fragment is a locally exact store abstraction in that it contains only those abstract variable bindings necessary to address a particular question at a particular program point; it is relative to that program point and the point of view may be shifted. We show how an analysis incorporating relative store fragments achieves flow-, context-, path- and must-alias sensitivity, and can be used as a basis for environment analysis, without any machinery put in place for those specific aims. We build upon recent advances in demand-driven higher-order program analysis to achieve this construction as it is fundamentally tied to demand-driven lookup of variable values.
Facchinetti is supported by a CAPES Fellowship, process number 13477/13-7.
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.
- 2.
regex is a regular expression engine using derivatives; rsa performs the RSA encryption algorithm; primtest is the Fermat primality testing algorithms; and deriv performs symbolic derivation of an equation.
- 3.
sat is a SAT solver, which stresses path- and context-sensitivity; cpstak is the TAK micro-benchmark in continuation-passing style, which stresses nested function calls and non-local lookups; and church tests the distributive property of multiplication over addition on Church numerals which includes polymorphic recursive functions and a massive number of function calls, stressing the function-wiring part of the analysis.
- 4.
Intel(R) Xeon(R) CPU E31220 @ 3.10Â GHz, 8Â GB of RAM, Debian GNU/Linux 8.8.
References
Agesen, O.: The cartesian product algorithm. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1995. LNCS, vol. 952, pp. 2–26. Springer, Heidelberg (1995). doi:10.1007/3-540-49538-X_2
BodÃk, R., Anik, S.: Path-sensitive value-flow analysis. In: POPL (1998)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). doi:10.1007/3-540-63141-0_10
Besson, F.: CPA beats \(\infty \)-CFA. In: Proceedings of the 11th International Workshop on Formal Techniques for Java-like Programs (2009)
Bergstrom, L., Fluet, M., Le, M., Reppy, J., Sandler, N.: Practical and effective higher-order optimizations. In: ICFP (2014)
Bourdoncle, F.: Abstract interpretation by dynamic partitioning. J. Funct. Program 2, 407–423 (1992)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: PLDI (1990)
Duesterwald, E., Gupta, R., Soffa, M.L.: A practical framework for demand-driven interprocedural data flow analysis. ACM Trans. Program. Lang. Syst. 19(6), 992–1030 (1997)
Das, M., Lerner, S., Mark Seigle, E.S.P.: Path-sensitive program verification in polynomial time. In: PLDI (2002)
Darais, D., Might, M., Van Horn, D.: Galois transformers and modular abstract interpreters. In: OOPSLA (2015)
Earl, C., Might, M., Van Horn, D.: Pushdown control-flow analysis of higher-order programs. In: Workshop on Scheme and Functional Programming (2010)
Fähndrich, M., Rehof, J., Das, M.: Scalable context-sensitive flow analysis using instantiation constraints. In: PLDI (2000)
Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: PLDI (1993)
Gilray, T., Lyde, S., Adams, M.D., Might, M., Van Horn, D.: Pushdown control-flow analysis for free. In: POPL (2016)
Germane, K., Might, M.: A posteriori environment analysis with pushdown Delta CFA. In: POPL (2017)
Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: Static Analysis Symposium (1998)
Heintze, N., Tardieu, O.: Demand-driven pointer analysis. In: PLDI (2001)
Johnson, J.I., Labich, N., Might, M., Van Horn, D.: Optimizing abstract abstract machines. In: ICFP (2013)
Johnson, J.I., Sergey, I., Earl, C., Might, M., Van Horn, D.: Pushdown flow analysis with abstract garbage collection. In: JFP (2014)
Jagannathan, S., Thiemann, P., Weeks, S., Wright, A.K.: Single and loving it: must-alias analysis for higher-order languages. In: POPL (1998)
Midtgaard, J.: Control-flow analysis of functional programs. ACM Comput. Surv. 44, 10:1–10:33 (2012)
Might, M.: Environment analysis of higher-order languages. PhD thesis, Georgia Institute of Technology (2007)
Might, M.: Abstract interpreters for free. In: Proceedings of the 17th International Conference on Static Analysis (2010)
Might, M.: Shape analysis in the absence of pointers and structure. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 263–278. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11319-2_20
Might, M., Shivers, O.: Environment analysis via \(\Delta \)CFA. In: POPL (2006)
Might, M., Shivers, O.: Improving flow analyses via \(\Gamma \)CFA: abstract garbage collection and counting. In: ICFP, Portland, Oregon (2006)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999)
Palmer, Z., Facchinetti, L.: DDPA implementation. https://github.com/JHU-PL-Lab/odefa/tree/sas2017-ddpa (2016)
Palmer, Z., Smith, S.: Higher-order demand-driven program analysis. In: ECOOP (2016)
Reps, T.: Demand interprocedural program analysis using logic databases. In: Application of Logic Databases (1994)
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)
Rehof, J., Fähndrich, M.: Type-base flow analysis: from polymorphic subtyping to CFL-reachability. In: POPL. Springer, New York (2001)
Späth, J., Do, L.N.Q., Ali, K., Bodden, E.: Demand-driven flow- and context-sensitive pointer analysis for Java. In: ECOOP, Boomerang (2016)
Sergey, I., Devriese, D., Might, M., Midtgaard, J., Darais, D., Clarke, D., Piessens, F.: Monadic abstract interpreters. In: PLDI (2013)
Shivers, O.: Control-flow analysis of higher-order languages. PhD thesis, Carnegie-Mellon University (1991). TR CMU-CS-91-145
Saha, D., Ramakrishnan, C.R.: Incremental and demand-driven points-to analysis using logic programming. In: PPDP (2005)
Steckler, P.A., Wand, M.: Lightweight closure conversion. ACM Trans. Program. Lang. Syst. 19, 48–86 (1997)
Tobin-Hochstadt, S., Felleisen, M.: Logical types for untyped languages. In: ICFP (2010)
Van Horn, D. Might, M.: Abstracting abstract machines. In: ICFP (2010)
Vardoulakis, D., Shivers, O.: CFA2: a context-free approach to control-flow analysis. In: European Symposium on Programming (2010)
Xie, Y., Chou, A., Engler, D.: Using symbolic, path-sensitive analysis to detect memory access errors. In: ESEC/FSE, Archer (2003)
Acknowledgments
The authors thank the anonymous reviewers for helpful suggestions which improved the final version of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Facchinetti, L., Palmer, Z., Smith, S.F. (2017). Relative Store Fragments for Singleton Abstraction. In: Ranzato, F. (eds) Static Analysis. SAS 2017. Lecture Notes in Computer Science(), vol 10422. Springer, Cham. https://doi.org/10.1007/978-3-319-66706-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-66706-5_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66705-8
Online ISBN: 978-3-319-66706-5
eBook Packages: Computer ScienceComputer Science (R0)