This is a summary of the group meeting on 10 March 2021

An Applied Quantum Hoare Logic (PLDI ’19)

这篇论文是应明生老师团队19年发表在PLDI上的，是关于用projection-based方法定义的新型量子霍尔逻辑。（待补充） 符号执行技术基本知识的介绍

---

符号执行技术的动机是用来自动生成违反某些性质的输入样例。

经典的符号执行将输入对应为符号值，同时模拟程序运行的每个分支，根据输入映射的符号值将程序中的变量映射为输入符号值以及具体值上（这里指可以通过静态分析确定的值）的表达式，在这个过程中对程序的所有分支都进行跟踪，并维护当前路径的分支条件（即所经路径条件的合取）。最后利用约束求解器来判断是否有违反性质的输入的具体值（比如在遇到assertion时，同时判断assertion中的内容是否被违背，且该路径是否是有效的（即当前路径的分支条件是否可满足），如果可以找到同时满足路径的分支条件且违背assertion的解时，就表明程序性质在该输入上被违反）。

经典的符号执行是sound和complete的，前者指的是所有违反性质的输入都能被找到，这得益于经典符号执行的穷举探索；后者指的是找到的输入都一定违反了性质，如果约束求解器足够精确，这是显然的。但经典符号执行也面临许多问题，比如在内存建模上（即对指针，数组，复杂的数据结构的建模，一个很重要的问题就是符号表达式出现在指针上，这可能会使该指针可以指向任意对象）；在程序间的交互的建模上（比如如何建模程序对文件的读写操作）；如何解决状态空间爆炸问题（即路径爆炸问题，这是由于在循环或者函数调用中出现的大量程序分支导致的路径数上的指数爆炸）；如何更好的解决与约束求解器的融合。

更进一步的，在经典符号执行的基础上，后来的工作者提出了混合执行，即将符号执行和具体执行结合起来，牺牲一部分经典符号执行的好的性质（soundness和completeness）来获得在实际应用上更好的表现。混合执行可以分为动态符号执行和选择性符号执行两类。

动态符号执行的思路如下，先是随机选择一组输入值，根据具体的输入值，探索该路径上是否会违背性质，在这部分状态空间探索完毕后，采用一些路径选择的策略，根据已经探索过的路径，选择其它未被探索的路径进行探索。此外，动态符号执行还可以采用“用具体值简化约束求解”的策略，来部分解决经典符号执行无法解决的“程序中存在外部代码”的问题。动态符号执行是unsound的，但仍是complete的。

选择性符号执行是在程序空间的探索过程中，有选择的使用符号执行和具体执行，这样可以将有限的资源更好的集中在探索某些重要的代码部分上。当然，选择性符号执行也会对soundness和completeness带来影响。