Expression-based aliasing for OO-languages

TL;DR

This paper extends alias analysis for object-oriented languages to handle unbounded executions, providing a sound over-approximation method implemented in the K-framework, with applications in concurrent programming models like SCOOP.

Contribution

It introduces an extension of alias calculus to infinite executions and implements it in K-framework, enabling sound over-approximation of aliasing in object-oriented programs.

Findings

The extended alias calculus handles infinite loops and recursion.

The K-framework implementation guarantees termination and soundness.

Application demonstrated in SCOOP concurrency model.

Abstract

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.