Abstract Interpretation Framework

[samuel-malec]

Overview

A static program analysis framework for GraalVM Native Image that uses abstract interpretation to discover compile-time optimizations.

Quick Start

Enable with a single flag (runs intraprocedural analysis by-default):

native-image -H:+RunAbstractInterpretation MyApp

Enable interprocedural analysis:

native-image -H:+RunAbstractInterpretation -H:+InterproceduralAnalysis MyApp

Key Classes for Code Review

Entry Points (Start Here)

1. AbstractInterpretationDriver.java - Configures and launches the framework
2. AbstractInterpretationEngine.java - Orchestrates analysis execution
3. AIFOptions.java - All configuration options

Analysis Engine

4. IntraProceduralAnalyzer.java - Single-method analysis
5. InterProceduralAnalyzer.java - Cross-method context-sensitive analysis

Abstract Domains (The Math)

6. AbstractDomain.java - Lattice operations interface
7. AbstractMemory.java - Main domain combining environment + store
8. IntInterval.java - Integer interval domain [lower, upper]

Transfer Functions (The Logic)

9. DataFlowIntervalAbstractInterpreter.java - Interprets some Graal IR node types and performs numerical dataflow analysis

Optimization Discovery

10. ConstantValueChecker.java - Finds constant values
11. IfConditionChecker.java - Finds dead branches

Fixpoint Algorithm

12. FixpointIterator.java - Iterates until stable solution
13. WeakTopologicalOrdering.java - Efficient CFG traversal for loops

Method Summaries (Performance)

14. SummaryManager.java: Method summary cache

• Stores analysis results for reuse across call sites
• Context-sensitive: different summaries for different calling contexts
• Subsumption checking: reuse summaries when applicable

15. Summary.java: Encapsulates method behavior

• Pre-condition: abstract state at method entry
• Post-condition: abstract state at return
• Parameter bindings and return value abstractions

16. SummaryFactory.java: Factory for creating summaries

• Pluggable design allows different summary strategies
• DataFlowIntervalAnalysisSummaryFactory for interval-based summaries

[oracle-contributor-agreement]

Thank you for your pull request and welcome to our community! To contribute, please sign the Oracle Contributor Agreement (OCA).
The following contributors of this PR have not signed the OCA:

• PR author: samuel-malec
• malec293@gmail.com (@samuel-malec)

To sign the OCA, please create an Oracle account and sign the OCA in Oracle's Contributor Agreement Application.

When signing the OCA, please provide your GitHub username. After signing the OCA and getting an OCA approval from Oracle, this PR will be automatically updated.

If you are an Oracle employee, please make sure that you are a member of the main Oracle GitHub organization, and your membership in this organization is public.

[gergo-]

Hi @samuel-malec , could you provide some context on this PR? Is this work coordinated with someone in the GraalVM compiler or native image team? Is there a writeup on the general design of this framework and the kinds of results it achieves?

[samuel-malec]

Hi,
This is a project that I worked on alongiside @d-kozak.

This work builds on my previous research on integrating abstract interpretation into GraalVM Native Image (done as part of my bachelor’s thesis. The goal of this framework is to enable static analyses that can operate directly within the Native Image analysis pipeline.

The design is currently exploratory and aimed at evaluating what kinds of analyses (e.g., dataflow analyses, bounds checking, resource leaks tracking, etc...) can be expressed and made practical in this setting.

I’m working on a more complete write-up of the architecture and intended use-cases, which I’m happy to share once it’s in a presentable state. Right now I created this pr so that @d-kozak can look more in-depth into the implementation.

Hi @samuel-malec , could you provide some context on this PR? Is this work coordinated with someone in the GraalVM compiler or native image team? Is there a writeup on the general design of this framework and the kinds of results it achieves?

[smarr]

Hi David @d-kozak and Samuel @samuel-malec, Christoph (@00asdf) has been working on something somewhat similar. @d-kozak I believe you two talked about it in Vienna at some point. We have a draft write up describing it an could probably share it offline.