A flow-insensitive-complete program representation. (English) Zbl 1498.68080
Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 197-218 (2022).
Summary: When designing a static analysis, choosing between a flow-insensitive or a flow-sensitive analysis often amounts to favor scalability over precision. It is well known than specific program representations can help to reconcile the two objectives at the same time. For example the SSA representation is used in modern compilers to perform a constant propagation analysis flow-insensitively without any loss of precision.
This paper proposes a provably correct program transformation that reconciles them for any analysis. We formalize the notion of Flow-Insensitive-Completeness with two collecting semantics and provide a program transformation that permits to analyze a program in a flow insensitive manner without sacrificing the precision we could obtain with a flow sensitive approach.
For the entire collection see [Zbl 1490.68015].
This paper proposes a provably correct program transformation that reconciles them for any analysis. We formalize the notion of Flow-Insensitive-Completeness with two collecting semantics and provide a program transformation that permits to analyze a program in a flow insensitive manner without sacrificing the precision we could obtain with a flow sensitive approach.
For the entire collection see [Zbl 1490.68015].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL (1988) |
| [2] | Andersen, L.O.: Program analysis and specialization for the C programming language. Ph.D. thesis. Datalogisk Institut (1994) |
| [3] | Bodík, R., Gupta, R., Sarkar, V.: ABCD: eliminating array bounds checks on demand. In: PLDI. ACM (2000) |
| [4] | Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference of POPL’78, pp. 84-96. ACM Press (1978) |
| [5] | Cytron, R.; Ferrante, J.; Rosen, BK; Wegman, MN; Zadeck, FK, Efficiently computing static single assignment form and the control dependence graph, ACM Trans. Program. Lang. Syst., 13, 4, 451-490 (1991) · doi:10.1145/115372.115320 |
| [6] | Gulwani, S.; Necula, GC; Giacobazzi, R., A polynomial-time algorithm for global value numbering, Static Analysis, 212-227 (2004), Heidelberg: Springer, Heidelberg · Zbl 1104.68019 · doi:10.1007/978-3-540-27864-1_17 |
| [7] | Hardekopf, B., Lin, C.: Flow-sensitive pointer analysis for millions of lines of code. In: Proceedings of CGO’11. ACM Press (2011) |
| [8] | Henry, J.; Monniaux, D.; Moy, M., PAGAI: a path sensitive static analyser, Electr. Notes Theor. Comput. Sci., 289, 15-25 (2012) · doi:10.1016/j.entcs.2012.11.003 |
| [9] | Hubert, L.; Beckert, B.; Marché, C., Sawja: static analysis workshop for java, Formal Verification of Object-Oriented Software, 92-106 (2011), Heidelberg: Springer, Heidelberg · Zbl 1308.68028 · doi:10.1007/978-3-642-18070-5_7 |
| [10] | Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of POPL’73, pp. 194-206. ACM Press (1973) · Zbl 0309.68020 |
| [11] | 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 |
| [12] | Logozzo, F.; Fähndrich, M., Pentagons: a weakly relational abstract domain for the efficient validation of array accesses, Sci. Comput. Program., 75, 9, 796-807 (2010) · Zbl 1197.68035 · doi:10.1016/j.scico.2009.04.004 |
| [13] | Maroneze, A.O.: Certified compilation and worst-case execution time estimation. Theses, Université Rennes 1 (2014). https://hal.archives-ouvertes.fr/tel-01064869 |
| [14] | Miné, A.: The octagon abstract domain. In: Proceedings of WCRE’01, p. 310. IEEE Computer Society (2001) · Zbl 1105.68069 |
| [15] | Mirliaz, S., Pichardie, D.: A flow-insensitive-complete program representation (2021). https://hal.archives-ouvertes.fr/hal-03384612. working paper or preprint |
| [16] | Nazaré, H.; Maffra, I.; Santos, W.; Barbosa, L.; Gonnord, L.; Quintão Pereira, FM, Validation of memory accesses through symbolic analyses, ACM SIGPLAN Not., 49, 10, 791-809 (2014) · doi:10.1145/2714064.2660205 |
| [17] | Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2004). https://books.google.fr/books?id=RLjt0xSj8DcC · Zbl 0932.68013 |
| [18] | Oh, H., Heo, K., Lee, W., Lee, W., Yi, K.: Design and implementation of sparse global analyses for C-like languages. In: Proceedings of PLDI’12. ACM Press (2012) |
| [19] | Pereira, F., Rastello, F.: Static Single Information form (2018). http://ssabook.gforge.inria.fr/latest/book.pdf. Chapter 11 in the SSA-book |
| [20] | Wegman, M.N., Zadeck, F.K.: Constant propagation with conditional branches. In: Proceedings of POPL’85, pp. 291-299. ACM Press (1985) |
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.
