Expression-based aliasing for OO-languages
This work addresses alias analysis challenges for verification and optimization in object-oriented programming, particularly for concurrent models like SCOOP, but it is incremental as it builds on prior calculus.
The authors tackled the undecidability of alias analysis in object-oriented languages by extending an existing alias calculus to handle unbounded program executions like infinite loops and recursive calls, and they implemented it in the K-framework to ensure termination and sound over-approximation of aliasing information.
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 s.a. infinite loops and recursive calls. Moreover, we devise a corresponding executable specification in the 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 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; K-definitions can be compiled into Maude for execution.