为 LLVM IR 改造符号孔
编程语言
2020-06-11 v1
摘要
符号孔是求解器辅助与交互式编程的基本构建块之一。未知值可被可靠地集成到程序中，且可使用 SAT 求解器等自动化工具证明含此类值的程序性质。然而，在编程语言中支持符号孔具有挑战性；规定孔与类型系统及执行语义的交互需要细致设计。本文动机并介绍了将具未知类型的符号孔引入 LLVM IR（一种强类型编译器中间语言）的实现。我们描述了如何通过在新原语 IR 操作之后抽象出不健全和类型不安全的细节，来安全地实现此类孔。我们的实现与类型检查和依赖检查等现有特性良好协作。最后，我们强调了使用我们的实现可能富有成果的研究方向。
引用
@article{arxiv.2006.05875,
title = {Retrofitting Symbolic Holes to LLVM IR},
author = {Bruce Collie and Michael O'Boyle},
journal= {arXiv preprint arXiv:2006.05875},
year = {2020}
}
备注
Accepted to TyDe 2020