一句话：首个将 capability 语义纳入搜索空间与正确性模型的超级优化框架，在 CHERI 上同时提升性能与内存安全。
现有超级优化器假设指针与整数可互换，但这一假设在 CHERI 等内存安全增强架构上不再成立：指针是携带边界、权限与来源（provenance）元数据的 capability，语义变化使许多传统优化失效，迫使 CHERI 编译器采用保守策略，以性能换取安全。本文提出 CapOpt，首个把 capability 语义显式纳入搜索空间与正确性模型的超级优化框架。其核心是 Provenance-Guided Stratified Synthesis（PGSS）：围绕 capability 感知抽象组织搜索空间，并利用基于来源的推理剔除不安全变换。作者还定义了 capability 感知等价模型，在传统函数正确性之外加入元数据完整性。在基于 ARM 的 CHERI 硬件平台与 CHERI-RISC-V 模拟器上的实验表明，CapOpt 相比现有 CHERI-LLVM 工具链性能最高提升 4.1%，同时通过收紧指针边界与权限进一步增强了安全性。
Superoptimization is a powerful code optimization technique that generates optimized instruction sequences by exploring the space of instruction-level transformations. However, existing superoptimizers assume that pointers and integers are interchangeable, an assumption that no longer holds in memory-security-enhanced architectures like CHERI, where pointers are represented as metadata-rich capabilities with enforced bounds, permissions, and provenance. This semantic change breaks many traditional optimizations and forces CHERI compilers to adopt conservative strategies that sacrifice performance for safety. We present CapOpt, the first superoptimization framework that explicitly incorporates capability semantics into both its search space and correctness model. CapOpt introduces Provenance-Guided Stratified Synthesis (PGSS), a synthesis strategy that structures the search space around capability-aware abstractions and uses provenance-based reasoning to eliminate unsafe transformations. We also define a capability-aware equivalence model that extends conventional functional correctness to include metadata integrity. We evaluated CapOpt on an ARM-based CHERI hardware platform and the CHERI-RISC-V simulator. Experimental results show that CapOpt improves performance by up to 4.1% over the existing CHERI-LLVM toolchain, while strengthening security by tightening pointer bounds and permissions.
@article{paperbot12166,
title = {CapOpt: Capability-Aware Superoptimization for Secure and Provably Faster Code},
author = {Xiaoyang Sun and Dejice Jacob and Huanting Wang and Jeremy Singer and Zheng Wang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA2},
year = {2026},
doi = {10.1145/3839481}
}