Abstract
We propose a technique to describe properties of numerical stores with optional values, that is, where some variables may have no value. Properties of interest include numerical equalities and inequalities. Our approach lifts common linear inequality based numerical abstract domains into abstract domains describing stores with optional values. This abstraction can be used in order to analyze languages with some form of option scalar type. It can also be applied to the construction of abstract domains to describe complex memory properties that introduce symbolic variables, e.g., in order to summarize unbounded sets of program variables, and where these symbolic variables may be undefined, as in some array or shape analyses. We describe the general form of abstract states, and propose sound and automatic static analysis algorithms. We evaluate our construction in the case of an array abstract domain.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Mayas are among the civilizations believed to have independently invented number “zero”.
References
Chen, L., Liu, J., Miné, A., Kapur, D., Wang, J.: An abstract domain to infer octagonal constraints with absolute value. In: Müller-Olm, M., Seidl, H. (eds.) Static Analysis. LNCS, vol. 8723, pp. 101–117. Springer, Heidelberg (2014)
Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. ENTS 6, 77–102 (1997)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL (2011)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978)
Cox, A., Chang, B.-Y.E., Sankaranarayanan, S.: QUIC graphs: relational invariant generation for containers. In: VMCAI (2015)
Ghorbal, K., Ivančić, F., Balakrishnan, G., Maeda, N., Gupta, A.: Donut domains: efficient non-convex domains for abstract interpretation. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 235–250. Springer, Heidelberg (2012)
Gopan, D., DiMaio, F., Dor, N., Reps, T., Sagiv, M.: Numeric domains with summarized dimensions. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 512–529. Springer, Heidelberg (2004)
Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: PLDI (2008)
Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)
Karr, M.: Affine relationships among the variables of a program. Acta Informatica 6(2), 133–151 (1976)
Liu, J., Rival, X.: Abstraction of arrays based on non contiguous partitions. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 282–299. Springer, Heidelberg (2015)
Miné, A.: The octagon abstract domain. HOSC 19(1), 31–100 (2006)
Miné, A.: Relational domains for the detection of floating point run-time errors. In: ESOP (2004)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL (1999)
Siegel, H., Mihaila, B., Simon, A.: The undefined domain: precise relational information for entities that do not exist. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 74–89. Springer, Heidelberg (2013)
Siegel, H., Simon, A.: Summarized dimensions revisited. In: NSAD (2012)
Siegel, H., Simon, A.: FESA: fold- and expand-based shape analysis. In: Jhala, R., Bosschere, K. (eds.) Compiler Construction. LNCS, vol. 7791, pp. 82–101. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Liu, J., Rival, X. (2015). Abstraction of Optional Numerical Values. In: Feng, X., Park, S. (eds) Programming Languages and Systems. APLAS 2015. Lecture Notes in Computer Science(), vol 9458. Springer, Cham. https://doi.org/10.1007/978-3-319-26529-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-26529-2_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-26528-5
Online ISBN: 978-3-319-26529-2
eBook Packages: Computer ScienceComputer Science (R0)