Deep Static Modeling of invokedynamic
George Fourtounis, Yannis Smaragdakis

TL;DR
This paper presents a static analysis technique that accurately models Java's invokedynamic and lambda features, eliminating unsoundness and improving analysis precision without sacrificing efficiency.
Contribution
It introduces a static modeling approach for invokedynamic and lambdas that integrates with existing analysis tools to ensure soundness and completeness.
Findings
Successfully models invokedynamic and lambdas in static analysis
Uncovers previously unreachable code due to unsoundness
Achieves high efficiency in analysis process
Abstract
Java 7 introduced programmable dynamic linking in the form of the invokedynamic framework. Static analysis of code containing programmable dynamic linking has often been cited as a significant source of unsoundness in the analysis of Java programs. For example, Java lambdas, introduced in Java 8, are a very popular feature, which is, however, resistant to static analysis, since it mixes invokedynamic with dynamic code generation. These techniques invalidate static analysis assumptions: programmable linking breaks reasoning about method resolution while dynamically generated code is, by definition, not available statically. In this paper, we show that a static analysis can predictively model uses of invokedynamic while also cooperating with extra rules to handle the runtime code generation of lambdas. Our approach plugs into an existing static analysis and helps eliminate all unsoundness…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Model-Driven Software Engineering Techniques
