3.1 Abstract Interpreter

[Mathnerd314]

Desired function Provide a configurable abstract interpreter for safety and temporal properties over your IR, similar in spirit to CPAchecker but extended. arxiv Uses partial evaluation techniques (both online and offline) and constructs the control flow graph; resolves names and identifies static vs. dynamic parts; drives specialization, supercompilation, and optimization decisions. Implements the specializer (s) that builds residual programs (p_x) specialized on static input. Corresponds to the "fast-start abstract interpreter" tier. ar5iv.labs.arxiv Realizes the first Futamura projection: specialize programs, including the interpreter (i). courses.grainger.illinois

Inputs

• Target program (p) and data (d).
• Access to target (optional).
• BTA-annotated IR (2.1).
• Interpreter (i) and the graph engine (0.1–0.2).
• Static inputs (x) (configuration, compile-time files, etc.).
• Verification-ready IR (post-normalization/partial evaluation).
• Properties: safety, temporal formulas (including μ-calculus-style), concurrency properties. di.ens- assertions, bounds, finalizers, reachability, termination, dead code, security/safety properties, deadlock/race conditions using memory model and concurrency model

Processing

• Interpret (p) via the graph engine + mini-VM + runtime.
• Call into literal assembly interpreter for inline assembly.
• Offline mode:
  • Use BTA to guide specialization and drive supercompilation/partial evaluation.
• Online mode:
  • Run a “quick start” interpreter; specialize as static data is encountered; suspend when dynamic interaction is needed (via escape/download protocol).
• Policy for host file reads: read during specialization, cache contents, respect security policies.
• Integrate logic engine and term rewriting to drive choice and guard evaluation.
• Use IR normalization as needed to satisfy invariants during execution.
• Evaluate and optimize static portions to residual constants.
• Integrates with term rewriting and strategy module for language-semantics-defined reductions.
• Concurrent and incremental analysis

Outputs

• Result value or exception for (\mathrm{run}(p,d)).
• Profiling traces (if enabled).
• Residual programs (p_x) with static parts inlined and removed.
• Specialized hot-loop versions for JIT (via compiler).

Key references

• Abstract interpretation for verification. di.ens
• Partial evaluation and Futamura projections. gist.github

[Mathnerd314]

This is also just supercompilation: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/supercomp-by-eval.pdf / #2