论文标题
翻新符号孔为LLVM IR
Retrofitting Symbolic Holes to LLVM IR
论文作者
论文摘要
符号孔是求解器和互动编程的基本构建块之一。未知的值可以将不明的值集成到程序中，并且可以使用自动化工具（例如SAT求解器）来证明包含它们的程序的属性。但是，在编程语言中支持符号孔具有挑战性。指定孔与类型系统和执行语义的相互作用需要仔细设计。 本文激发并介绍了符号孔的实施，该符号孔具有未知类型的LLVM IR，这是一种强大的编译器中间语言。我们描述了如何通过在新的原始IR操纵背后抽象不健全和类型的不安全细节来安全地实现此类漏洞。我们的实施与现有功能（例如类型和依赖性检查）合作。最后，我们强调了使用我们的实施来调查的潜在富有成果的领域。
Symbolic holes are one of the fundamental building blocks of solver-aided and interactive programming. Unknown values can be soundly integrated into programs, and automated tools such as SAT solvers can be used to prove properties of programs containing them. However, supporting symbolic holes in a programming language is challenging; specifying interactions of holes with the type system and execution semantics requires careful design. This paper motivates and introduces the implementation of symbolic holes with unknown type to LLVM IR, a strongly-typed compiler intermediate language. We describe how such holes can be implemented safely by abstracting unsound and type-unsafe details behind a new primitive IR manipulation. Our implementation co-operates well with existing features such as type and dependency checking. Finally, we highlight potentially fruitful areas for investigation using our implementation.
