Lifting numeric relational domains to algebraic data types. (English) Zbl 1524.68198
Singh, Gagandeep (ed.) et al., Static analysis. 29th international symposium, SAS 2022, Auckland, New Zealand, December 5–7, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13790, 104-134 (2022).
Summary: We present RAND, an input-output relational abstract domain that expresses relations between values of non-recursive algebraic data types (ADTs), and numeric relations between their scalar parts. RAND is parametrised on a user-provided numeric relational domain, that we lift to pairs of variables and projection paths. It is constructed as a disjunctive completion of a reduced product of domains for numeric relations, for equalities, and for cases of variant constructors. Using RAND, we define a modular, inter-procedural, input-output relational analysis for a while language with ADTs and function calls. The analysis computes function summaries, that describe relations between the inputs of programs and their outputs.
For the entire collection see [Zbl 1515.68049].
For the entire collection see [Zbl 1515.68049].
MSC:
| 68Q65 | Abstract data types; algebraic specification |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Keywords:
static analysis; abstract interpretation; relational abstract domains; algebraic data types; input-output relations; function summariesReferences:
| [1] | Andreescu, OF; Jensen, T.; Lescuyer, S.; Montagu, B., Inferring frame conditions with static correlation analysis, POPL (2019) · doi:10.1145/3290360 |
| [2] | Bautista, S.; Jensen, T.; Montagu, B., Numeric domains meet algebraic data types, NSAD (2020) · doi:10.1145/3427762.3430178 |
| [3] | Bautista, S., Jensen, T., Montagu, B.: Artifact for the “Lifting Numeric Relational Domains to Algebraic Data Types” article of the SAS 2022 symposium (2022). doi:10.5281/zenodo.6977156 |
| [4] | Bautista, S., Jensen, T., Montagu, B.: Lifting Numeric Relational Domains to Algebraic Data Types (extended version) (2022). https://hal.inria.fr/hal-03765357 |
| [5] | Boutonnet, R.; Halbwachs, N., Disjunctive relational abstract interpretation for interprocedural program analysis, VMCAI (2019) · Zbl 1522.68146 · doi:10.1007/978-3-030-11245-5_7 |
| [6] | Chang, B.Y.E., Rival, X.: Modular construction of shape-numeric analyzers. Festschrift for Dave Schmidt (2013). https://hal.inria.fr/hal-00926948 · Zbl 1464.68072 |
| [7] | Comon, H., et al.: Tree Automata Techniques and Applications (2008). https://hal.inria.fr/hal-03367725 |
| [8] | Cousot, P., Constructive design of a hierarchy of semantics of a transition system by abstract interpretation (extended abstract), MFPS (1997) · Zbl 0911.68134 · doi:10.1016/s1571-0661(05)80168-9 |
| [9] | Cousot, P.: Principles of Abstract Interpretation. The MIT Press, Cambridge (2021) · Zbl 1494.68002 |
| [10] | Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977). doi:10.1145/512950.512973 · Zbl 1149.68389 |
| [11] | Cousot, P.; Cousot, R.; Horspool, RN, Modular static program analysis, Compiler Construction, 159-179 (2002), Heidelberg: Springer, Heidelberg · Zbl 1051.68624 · doi:10.1007/3-540-45937-5_13 |
| [12] | Dimovski, A.S.: Lifted static analysis using a binary decision diagram abstract domain. In: GPCE (2019). doi:10.1145/3357765.3359518 |
| [13] | Dimovski, A.S., Apel, S., Legay, A.: Several lifted abstract domains for static analysis of numerical program families. Sci. Comput. Program. 213 (2022). doi:10.1016/j.scico.2021.102725 |
| [14] | Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: FMCAD (2015). doi:10.1109/FMCAD.2015.7542253 · Zbl 1306.68013 |
| [15] | Filliâtre, J-C; Paskevich, A.; Felleisen, M.; Gardner, P., Why3 — where programs meet provers, Programming Languages and Systems, 125-128 (2013), Heidelberg: Springer, Heidelberg · Zbl 1435.68366 · doi:10.1007/978-3-642-37036-6_8 |
| [16] | Genet, T.; Le Gall, T.; Legay, A.; Murat, V.; Konstantinidis, S., A completion algorithm for lattice tree automata, Implementation and Application of Automata, 134-145 (2013), Heidelberg: Springer, Heidelberg · Zbl 1298.68135 · doi:10.1007/978-3-642-39274-0_13 |
| [17] | Genet, T., Le Gall, T., Legay, A., Murat, V.: Tree regular model checking for lattice-based automata. In: CIAA (2013). https://hal.inria.fr/hal-00924849 · Zbl 1298.68135 |
| [18] | Haudebourg, T., Genet, T., Jensen, T.P.: Regular language type inference with term rewriting. In: ICFP (2020). doi:10.1145/3408994 · Zbl 1504.68129 |
| [19] | Illous, H., Lemerre, M., Rival, X.: A relational shape abstract domain. In: NASA Formal Methods (2017). doi:10.1007/978-3-319-57288-8_15 · Zbl 1522.68156 |
| [20] | Illous, H.; Lemerre, M.; Rival, X.; Pichardie, D.; Sighireanu, M., Interprocedural shape analysis using separation logic-based transformer summaries, Static Analysis, 248-273 (2020), Cham: Springer, Cham · Zbl 1474.68054 · doi:10.1007/978-3-030-65474-0_12 |
| [21] | Jeannet, B.: The BDDAPRON logico-numerical abstract domains library (2009). https://pop-art.inrialpes.fr/ bjeannet/bjeannet-forge/bddapron/ |
| [22] | Jeannet, B.: Relational interprocedural verification of concurrent programs. Softw. Syst. Model. 12 (2013). doi:10.1007/s10270-012-0230-7 |
| [23] | Jeannet, B.; Loginov, A.; Reps, T.; Sagiv, M.; Giacobazzi, R., A relational approach to interprocedural shape analysis, Static Analysis, 246-264 (2004), Heidelberg: Springer, Heidelberg · Zbl 1104.68416 · doi:10.1007/978-3-540-27864-1_19 |
| [24] | Jeannet, B.; Miné, A., Apron: a library of numerical abstract domains for static analysis, CAV (2009) · doi:10.1007/978-3-642-02658-4\_52 |
| [25] | Journault, M.: Precise and modular static analysis by abstract interpretation for the automatic proof of program soundness and contracts inference. (Analyse statique modulaire précise par interprétation abstraite pour la preuve automatique de correction de programmes et pour l’inférence de contrats.). Ph.D. thesis, Sorbonne University, France (2019). https://tel.archives-ouvertes.fr/tel-02947214 |
| [26] | Journault, M.; Miné, A.; Ouadjaout, A.; Caires, L., An abstract domain for trees with numeric relations, Programming Languages and Systems, 724-751 (2019), Cham: Springer, Cham · Zbl 1524.68092 · doi:10.1007/978-3-030-17184-1_26 |
| [27] | Kim, S., Rival, X., Ryu, S.: A theoretical foundation of sensitivity in an abstract interpretation framework. In: TOPLAS (2018). doi:10.1145/3230624 |
| [28] | Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.: Compositional recurrence analysis revisited. In: PLDI (2017). doi:10.1145/3062341.3062373 |
| [29] | Klein, G., et al.: seL4: Formal verification of an OS kernel. In: SOSP (2009). doi:10.1145/1629575.1629596 |
| [30] | Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: POPL (2010). doi:10.1145/1706299.1706355 · Zbl 1312.68136 |
| [31] | Kozen, D.: Kleene algebra with tests. In: TOPLAS (1997). doi:10.1145/256167.256195 · Zbl 0882.03064 |
| [32] | Li, H., Berenger, F., Evan Chang, B., Rival, X.: Semantic-directed clumping of disjunctive abstract states. In: POPL (2017). doi:10.1145/3009837.3009881 · Zbl 1380.68129 |
| [33] | Liu, J.; Rival, X.; Feng, X.; Park, S., Abstraction of optional numerical values, Programming Languages and Systems, 146-166 (2015), Cham: Springer, Cham · Zbl 1329.68078 · doi:10.1007/978-3-319-26529-2_9 |
| [34] | Miné, A.: The octagon abstract domain. High. Order Symb. Comput. 19 (2006). doi:10.1007/s10990-006-8609-1 · Zbl 1105.68069 |
| [35] | Miné, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang. 4 (2017). doi:10.1561/2500000034 |
| [36] | Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: TOPLAS (2007). doi:10.1145/1275497.1275504 · Zbl 1108.68404 |
| [37] | Ong, C.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: POPL (2011). doi:10.1145/1926385.1926453 · Zbl 1284.68193 |
| [38] | Pierce, B., Advanced Topics in Types and Programming Languages (2005), Cambridge: MIT Press, Cambridge · Zbl 1080.68009 |
| [39] | Pierce, BC, Types and Programming Languages (2002), Cambridge: MIT Press, Cambridge · Zbl 0995.68018 |
| [40] | Rival, X., Yi, K.: Introduction to Static Analysis: An Abstract Interpretation Perspective. The MIT Press, Cambridge (2020) |
| [41] | Schrammel, P.; Jeannet, B.; Yahav, E., Logico-numerical abstract acceleration and application to the verification of data-flow programs, Static Analysis, 233-248 (2011), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-23702-7_19 |
| [42] | Sharma, T.; Reps, T., A new abstraction framework for affine transformers, Formal Methods Syst. Des., 54, 1, 110-143 (2018) · Zbl 1425.68084 · doi:10.1007/s10703-018-0325-z |
| [43] | Sotin, P.; Jeannet, B.; Barthe, G., Precise Interprocedural Analysis in the Presence of Pointers to the Stack, Programming Languages and Systems, 459-479 (2011), Heidelberg: Springer, Heidelberg · Zbl 1326.68107 · doi:10.1007/978-3-642-19718-5_24 |
| [44] | Tarski, A.: On the calculus of relations. J. Symbol. Logic 6 (1941). doi:10.2307/2268577 · JFM 67.0973.02 |
| [45] | Venet, A.; Cousot, R.; Schmidt, DA, Abstract cofibered domains: application to the alias analysis of untyped programs, Static Analysis, 366-382 (1996), Heidelberg: Springer, Heidelberg · Zbl 1482.68098 · doi:10.1007/3-540-61739-6_53 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
