×

Expression-based aliasing for OO-languages. (English) Zbl 1328.68043

Artho, Cyrille (ed.) et al., Formal techniques for safety-critical systems. Third international workshop, FTSCS 2014, Luxembourg, November 6–7, 2014. Revised selected papers. Cham: Springer (ISBN 978-3-319-17580-5/pbk; 978-3-319-17581-2/ebook). Communications in Computer and Information Science 476, 47-61 (2015).
Summary: Alias analysis has been an interesting research topic in verification and optimization of programs. The undecidability of determining whether two expressions in a program may reference to the same object is the main source of the challenges raised in alias analysis. In this paper we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions such as infinite loops and recursive calls. Moreover, we devise a corresponding executable specification in the \(\mathbb K\)-framework. An important property of our extension is that, in a non-concurrent setting, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to show that the associated \(\mathbb K\)-machinery implements an algorithm that always stops and provides a sound over-approximation of the “may aliasing” information, where soundness stands for the lack of false negatives. As a case study, we analyze the integration and further applications of the alias calculus in SCOOP. The latter is an object-oriented programming model for concurrency, recently formalized in Maude; \(\mathbb K\) definitions can be compiled into Maude for execution.
For the entire collection see [Zbl 1316.68001].

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N15 Theory of programming languages

Software:

Maude; K-Maude; Eiffel
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Cavalcanti, A.; Dams, DR, Field-sensitive value analysis by field-insensitive analysis, FM 2009: Formal Methods, 370-386 (2009), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-05089-3_24
[2] Asavoae, IM, Abstract semantics for alias analysis in K, Electr. Notes Theor. Comput. Sci., 304, 97-110 (2014) · doi:10.1016/j.entcs.2014.05.005
[3] Bouajjani, A.; Esparza, J.; Maler, O.; Mazurkiewicz, A.; Winkowski, J., Reachability analysis of pushdown automata: application to model-checking, CONCUR 1997: Concurrency Theory, 135-150 (1997), Heidelberg: Springer, Heidelberg · Zbl 1512.68135
[4] Burke, M.; Carini, P.; Choi, J-D; Hind, M.; Pingali, K.; Banerjee, U.; Gelernter, D.; Nicolau, A.; Padua, D., Flow-insensitive interprocedural alias analysis in the presence of pointers, Languages and Compilers for Parallel Computing, 234-250 (1995), Berlin Heidelberg: Springer, Berlin Heidelberg · doi:10.1007/BFb0025882
[5] Caltais, G.: Expression-based aliasing for OO-languages. CoRR, abs/1409.7509 (2014) · Zbl 1328.68043
[6] Chase, D.R.., Wegman, M.N., Zadeck, F.K.: Analysis of pointers and structures. In: PLDI, pp. 296-310 (1990)
[7] Choi, J.-D., Burke, M., Carini, P.: Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects. In: Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1993, pp. 232-245. ACM, New York, NY, USA (1993)
[8] Cousot, P.; Cousot, R., Abstract interpretation and application to logic programs, J. Log. Program., 13, 2-3, 103-179 (1992) · Zbl 0776.68024 · doi:10.1016/0743-1066(92)90030-7
[9] Diwan, A.; McKinley, KS; Moss, JEB, Type-based alias analysis, SIGPLAN Not., 33, 5, 106-117 (1998) · doi:10.1145/277652.277670
[10] Emami, M., Ghiya, R., Hendren, L.J.: Context-sensitive interprocedural points-to analysis in the presence of function pointers. In: Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, PLDI 1994, pp. 242-256. ACM, New York, NY, USA (1994)
[11] Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: PASTE, pp. 54-61 (2001)
[12] Hind, M.; Burke, M.; Carini, P.; Choi, J-D, Interprocedural pointer alias analysis, ACM Trans. Program. Lang. Syst., 21, 4, 848-894 (1999) · doi:10.1145/325478.325519
[13] Hoare, CART; Möller, B.; Struth, G.; Wehrman, I.; Bravetti, M.; Zavattaro, G., Concurrent Kleene algebra, CONCUR 2009 - Concurrency Theory, 399-414 (2009), Heidelberg: Springer, Heidelberg · Zbl 1254.68172 · doi:10.1007/978-3-642-04081-8_27
[14] Kleene, SC; Shannon, C.; McCarthy, J., Representation of events in nerve nets and finite automata, Automata Studies, 3-41 (1956), Princeton: Princeton University Press, Princeton
[15] Kogtenkov, A., Meyer, B., Velder, S.: Alias and change calculi, applied to frame inference. CoRR, abs/1307.3189 (2013)
[16] Landi, W., Undecidability of static analysis, ACM Lett. Program. Lang. Syst., 1, 4, 323-337 (1992) · doi:10.1145/161494.161501
[17] Landi, W., Ryder, B.G:. Pointer-induced aliasing: a problem classification. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1991, pp. 93-103. ACM, New York, NY, USA (1991)
[18] Larus, J.R., Hilfinger, P.N.: Detecting conflicts between structure accesses. In: PLDI, pp. 21-34. ACM, New York (1988)
[19] Meseguer, J.; Roşu, G.; Owe, O.; Steffen, M.; Telle, JA, The rewriting logic semantics project: a progress report, Fundamentals of Computation Theory, 1-37 (2011), Heidelberg: Springer, Heidelberg · Zbl 1342.68198 · doi:10.1007/978-3-642-22953-4_1
[20] Meyer, B., Eiffel: The Language (1991), Englewood Cliffs: Prentice-Hall, Englewood Cliffs · Zbl 0779.68013
[21] Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Proceedings of the 2006 ACM SIGPLAN/SIGBED Conference on Language, Compilers, and Tool Support for Embedded Systems, LCTES 2006, pp. 54-63. ACM, New York, NY, USA (2006)
[22] Morandi, B., Schill, M., Nanz, S., Meyer, B.: Prototyping a concurrency model. In: ACSD, pp. 170-179 (2013)
[23] Myers. E.M.: A precise inter-procedural data flow algorithm. In: Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1981, pp. 219-230. ACM, New York, NY, USA (1981)
[24] Nienaltowski, P.: Practical Framework for Contract-based Concurrent Object-oriented Programming, ETH (2007)
[25] Rabin, MO; Scott, D., Finite automata and their decision problems, IBM J. Res. Dev., 3, 2, 114-125 (1959) · Zbl 1461.68105 · doi:10.1147/rd.32.0114
[26] Robert, V.; Leroy, X.; Hawblitzel, C.; Miller, D., A formally-verified alias analysis, Certified Programs and Proofs, 11-26 (2012), Heidelberg: Springer, Heidelberg · Zbl 1383.68015 · doi:10.1007/978-3-642-35308-6_5
[27] Rosu, G., Serbanuta, T.F.: K overview and SIMPLE case study. In Proceedings of International K Workshop (K 2011), ENTCS. Elsevier (2013) (to appear)
[28] Şerbănuţă, TF; Roşu, G.; Ölveczky, PC, K-Maude: a rewriting based tool for semantics of programming languages, Rewriting Logic and Its Applications, 104-122 (2010), Heidelberg: Springer, Heidelberg · Zbl 1306.68088 · doi:10.1007/978-3-642-16310-4_8
[29] Sridharan, M.; Chandra, S.; Dolby, J.; Fink, SJ; Yahav, E.; Clarke, D.; Noble, J.; Wrigstad, T., Alias analysis for object-oriented programs, Aliasing in Object-Oriented Programming, 196-232 (2013), Heidelberg: Springer, Heidelberg
[30] Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for C programs. In: Proceedings of the ACM SIGPLAN 1995 Conference on Programming Language Design and Implementation, PLDI 1995, pp. 1-12. ACM, New York, NY, USA (1995)
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.