We define a novel static analysis for Java bytecode, called definite expression aliasing. It infers, for each variable v at each program point p, a set of expressions whose value at p is equal to the value of v at p, for every possible execution of the program. Namely, it determines which expressions must be aliased to local variables and stack elements of the Java Virtual Machine. This is a useful piece of information for a static analyzer, such as Julia, since it can be used to refine other analyses at conditional statements or assignments. We formalize and implement a constraint-based analysis, defined and proved correct in the abstract interpretation framework. Moreover, we show the benefits of our definite expression aliasing analysis for nullness and termination analysis with Julia. © 2012 Springer-Verlag.
CITATION STYLE
Nikolić, D., & Spoto, F. (2012). Definite expression aliasing analysis for Java bytecode. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7521 LNCS, pp. 74–89). https://doi.org/10.1007/978-3-642-32943-2_6
Mendeley helps you to discover research relevant for your work.