轻量级符号虚拟机，专为辅助求解器的宿主语言设计

文章预览

A Lightweight Symbolic Virtual Machinefor Solver-Aided Host Languages https://homes.cs.washington.edu/~bodik/ucb/Files/2014/rosette-pldi2014.pdf 摘要 求解器辅助的领域特定语言（SDSLs）是一类新兴的计算机辅助编程系统。它们通过使用可满足性求解器来自动化诸如验证、调试、合成和非确定性执行等任务，从而简化了程序的构建。然而，将编程任务简化为可满足性问题涉及将程序转换为逻辑约束，即使对于领域特定语言来说，这也是一个工程挑战。 我们之前已经证明，如果SDSLs通过（传统的）嵌入到一个本身是求解器辅助的宿主语言中来实现，就可以避免将程序转换为约束。本文描述了如何为这样的宿主语言实现一个符号虚拟机（SVM）。我们的符号虚拟机是轻量级的，因为它只将宿主语言的一小部分构造编译为约束，同时允许SDSL设计者使用整个语言，包括用于DSL嵌入的构造。这 ………………………………