一句话：提出 SuperStack，用贪心、MaxSAT 与领域约束加速栈字节码超优化，找到更优等价指令序列。
给定无循环指令序列，超优化利用约束求解器寻找满足目标的最优等价序列，但其搜索空间随解长度指数增长，长序列难以处理。本文面向栈字节码提出 SuperStack，包含三个组件：贪心算法逐步收紧最优解长度上界；将优化问题表示为 MaxSAT 中的加权软子句；引入领域特定的支配约束与冗余约束来削减搜索空间。工具支持 WebAssembly 和 Ethereum 字节码的最优代码翻译。在超过 500,000 个序列上的实验表明，贪心、约束与 SAT 的结合显著提升现有超优化器的优化收益，并将优化时间至少缩短为原来的四分之一。
Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is optimal for a desired objective. The complexity of the search grows exponentially with the length of the solution being constructed and the problem becomes intractable for large sequences of instructions. This paper presents a new approach to superoptimizing stack-bytecode via three novel components: (1) a greedy algorithm to refine the bound on the length of the optimal solution; (2) a new representation of the optimization problem as a set of weighted soft clauses in MaxSAT; (3) a series of domain-specific dominance and redundant constraints to reduce the search space for optimal solutions. We have developed a tool, named S uper S tack , which can be used to find optimal code translations of modern stack-based bytecode, namely WebAssembly or Ethereum bytecode. Experimental evaluation on more than 500,000 sequences shows the proposed greedy, constraint-based and SAT combination is able to greatly increase optimization gains achieved by existing superoptimizers and reduce to at least a fourth the optimization time.
@article{AlbertBHIRS24,
title = {SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques},
author = {Elvira Albert and Maria Garcia de la Banda and Alejandro Hernández-Cerezo and Alexey Ignatiev and Albert Rubio and Peter J. Stuckey},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656435}
}