Computing Stack Maps with Interfaces

8 years 12 months ago
Computing Stack Maps with Interfaces
Abstract. Lightweight bytecode verification uses stack maps to annotate Java bytecode programs with type information in order to reduce the verification to type checking. This paper describes an improved bytecode analyser together with algorithms for optimizing the stack maps generated. The analyser is simplified in its treatment of base values (keeping only the necessary information to ensure memory safety) and enriched in its representation of interface types, using the Dedekind-MacNeille completion technique. The computed interface information allows to remove the dynamic checks at interface method invocations. We prove the memory safety property guaranteed by the bytecode verifier using an operational semantics whose distinguishing feature is the use of untagged 32-bit values. For bytecode typable without sets of types we show how to prune the fix-point to obtain a stack map that can be checked without computing with sets of interfaces i.e., lightweight verification is not made mor...
Frédéric Besson, Thomas P. Jensen, T
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Authors Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin
Comments (0)