We introduce Stencil-Lifting, a novel system for automatically converting stencil kernels written in low-level languages within legacy code into semantically equivalent Domain-Specific Language (DSL) implementations. Targeting the efficiency bottlenecks of existing verified lifting systems, Stencil-Lifting achieves scalable stencil kernel abstraction through two key innovations. First, we propose a hierarchical recursive lifting theory that represents stencil kernels, structured as nested loops, using invariant subgraphs, which are customized data dependency graphs capturing loop-carried computations and structural invariants. Each vertex in the invariant subgraph is associated with a predicate-based summary that encodes its computational semantics. Enforcing self-consistency across these summaries enables a derivation of correct loop invariants and postconditions, without the need for external verification. Second, we design a hierarchical recursive lifting algorithm that guarantees termination through a convergent recursive process, avoiding the inefficiencies of search-based synthesis while efficiently deriving valid summaries with formally proven completeness. We evaluate Stencil-Lifting on diverse stencil benchmarks from real-world applications. Experiment results demonstrate that Stencil-Lifting achieves 31.6× and 5.8× speedups compared to the state-of-the-art verified lifting systems STNG and Dexter, respectively. Our work significantly improves the efficiency of translating stencil kernels into DSL implementations, effectively bridging the gap between legacy code and modern DSL-based paradigms.

@article{paperbot2957,
  title = {Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes},
  author = {Mingyi Li and Junmin Xiao and Siyan Chen and Hui Ma and Xi Chen and Peihua Bao and Liang Yuan and Guangming Tan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763159}
}