低级中间表示中的所有权
Ownership in low-level intermediate representation
AI总结：
针对低级程序验证中所有权信息缺失、指针无法用FOL抽象的问题，为类LLVM低级中间表示设计所有权语义，通过指针缓存减少地址映射维护，在SEABMC中实现后，C程序验证的SMT求解速度提升1.3x-5x。
摘要：
高级语言中的所有权概念可帮助程序员和编译器推理内存操作的有效性。此前，所有权语义已成功应用于高级自动程序验证，通过数据的一阶逻辑（FOL）表示来建模数据引用，而非维护地址映射。然而，所有权语义尚未应用于低级程序验证，我们发现了两大挑战：其一，程序编译为低级中间表示（如LLVM IR）时所有权信息会丢失；其二，低级程序中的指针通过地址映射指向字节（如在unsafe Rust中），因此验证条件（VC）无法始终将指针替换为其FOL抽象。\n为解决这一问题，我们为类LLVM的低级中间表示设计了所有权语义。借助这些语义，验证条件可通过直接访问存储数据字节表示的指针缓存，机会性地对部分内存访问建模。该方案减少了必须维护地址映射的场景，尤其适用于遵循所有权语义的大体安全的程序。对于不安全功能，内存访问通过地址映射上的操作建模，我们还提供了保持地址映射与指针缓存同步的机制。\n我们在SEABMC（一款针对LLVM的位精确有界模型检验器）中实现了这些语义。评估阶段假设源程序用C语言编写，由于C语言本身不内置所有权机制，我们添加了合适的宏，在将程序翻译为类LLVM中间表示以进行验证的过程中引入并保留所有权。我们在成熟的开源C代码上评估了该方法，在手工构建的基准测试和实际程序中，均观察到SMT求解阶段实现了1.3倍至5倍的速度提升。
英文摘要：
The concept of ownership in high level languages can aid both the programmer and the compiler to reason about the validity of memory operations. Previously, ownership semantics has been used successfully in high level automatic program verification to model a reference to data by a first order logic (FOL) representation of data instead of maintaining an address map. However, ownership semantics is not used in low level program verification. We have identified two challenges. First, ownership information is lost when a program is compiled to a low level intermediate representation (e.g., in LLVM IR). Second, pointers in low level programs point to bytes using an address map (e.g., in unsafe Rust) and thus the verification condition (VC) cannot always replace a pointer by its FOL abstraction. To remedy the situation, we develop ownership semantics for an LLVM like low level intermediate representation. Using these semantics, the VC can opportunistically model some memory accesses by a direct access of a pointer cache that stores byte representation of data. This scheme reduces instances where an address map must be maintained, especially for mostly safe programs that follow ownership semantics. For unsafe functionality, memory accesses are modelled by operations on an address map and we provide mechanisms to keep the address map and pointer cache in sync. We implement these semantics in SEABMC, a bit precise bounded model checker for LLVM. For evaluation, the source programs are assumed to be written in C. Since C does not have ownership built in, suitable macros are added that introduce and preserve ownership during translation to LLVM like IR for verification. This approach is evaluated on mature open source C code. For both handcrafted benchmarks and practical programs, we observe a speedup of $1.3x-5x$ during SMT solving.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
