符号执行可以被用于生成测试输入，以下为论文《Symbolic Execution for Software Testing: Three Decades Later》的阅读笔记
把符号输入进程序里（而不是输入实际的数据），把程序中的函数变成符号表达式。程序的输出值也是输入符号表达式。
一个程序的执行路径可以表示为ture和false的序列，在序列的第i个位置为true则表示第i个条件判断语句执行then分支，若为false则执行else分支。
一个程序的所有的执行路径可以被表示成一颗执行树。
符号执行的过程中，一直存有一个符号状态集合
它是映射的集合，这里的映射是指把一个符号变量通过符号表达式变成另外一个符号变量。
符号执行的过程中，还有一个符号路径约束PC，这是符号表达式上的一个无量词的一阶式。
在每条路径开始执行前，都初始化这两个变量为，
符号执行阶段，这两个值会变化。
在一条执行路径结束的时候，会调用约束求解器去求解PC，从而生成真正的input values.如果程序用这个input values去执行，它的执行路径会跟符号执行的路径一致。
这就是符号执行的基本概念。
如上图，当程序执行到16，17行时，
其中x_0，y_0是两个初始的无约束符号值。
当执行到v=e这种赋值语句时，例如第6行代码时。符号状态会变为:
当执行到条件语句如：
如果PC可以满足对符号值的某些分配，那么符号执行继续沿着then这条分支执行下去，且符号状态为σ和符号路径约束为PC。
同样，如果PC'可满足，PC‘则使用符号状态σ和符号路径约束PC’创建另一个符号执行的实例，并沿着“else”分支继续执行；
如在第7行，会有两个路径约束被创建，分别对应于
在第8行，会有两个路径约束被创建，分别对应于
如果符号执行实例遇到了退出语句或错误（例如，程序崩溃或违反了断言），则终止符号执行的当前实例，并使用现成的约束求解器生成对当前符号路径约束得到真正的input datas.
则
PC的前面是若干个ture,最后一个是false.
在实践中，需要对路径搜索进行限制，例如，限制时间，限制路径的数量、限制路径的深度
若把上面的twice替换如下
则执行到twice时，会产生两个路径约束：
此时常规的约束求解器是不能求解这个非线性表达式的。
如果我们连twice的源码都得不到呢，
则会有以下两个路径约束
此时常规的约束求解器还是无法求解。
符号执行的概念早在1975年就提出了，但是真正得到实用，却是在一种方式提出之后，即结合实际执行和符号化执行的一种方法：concolic execution，是真正意义上的动态符号执行。
Concolic Execution是把实际执行和符号执行结合的一种方法，以下称为混合执行。
混合执行的输入是随机生成的或者给定的一个具体的值，在执行过程中收集条件语句中的符号约束，然后对此约束取反，使用约束求解器来求解当前输入的变体，以便引导程序的下一次执行转向另一个执行路径
我们依旧以上面那个程序的例子来说明
先产生一些随机输入，例如{x=22, y=7}
同时实际地和符号化地执行程序。这个实际执行会走到第7行的else分支，符号化执行会在实际执行路径生成路径约束
然后混合执行会将路径约束的连接词取反，求解
得到一个测试输入{x=2, y=1}，
注意到，这里使用“以深度优先”的搜索策略来探索所有的执行路径；但是，我们可以使用其他策略来探索不同顺序的路径。
这一部分没读太懂，所以下面的内容读懂了再做补充吧。
EGT方法由EXE和KLEE工具扩展组合成，它工作通过区分程序的具体状态和符号状态来完成。
EGT在每次操作之前动态检查操作所涉及的值是否都是具体的。如果操作的值是具体的，则该操作将与原始程序中一样执行。否则，如果至少有一个值是符号值，则通过更新当前路径的路径条件，然后符号地执行该操作。
例如，如果图1中的第17行更改为y=10，那么第6行将用具体参数20调用函数twice()，调用将像原始程序一样执行。然后，第7行上的分支将成为如果(20==x)，符号执行会往两个方向执行，在“then”方向(会添加x=20的路径约束)，以及“else”方向(会添加了x=20的约束)。注意，在“then”路径上，第8行变成了if(x>20)，因此在“then”边是不可行的，因为x被约束等于20了。
参考文献：
https://zhuanlan.zhihu.com/p/26927127
\delta
\delta = 空集
PC = ture
1 int twice (int v) {
2 return 2∗v;
3 }
4
5 void testme (int x, int y) {
6 z = twice (y);
7 if (z == x) {
8 if (x > y+10)
9 ERROR;
10 }
11 }
12 }
13
14 /∗ simple driver exercising testme () with sym inputs ∗/
15 int main() {
16 x = sym input();
17 y = sym input();
18 testme (x, y );
19 return 0;
20 }
1 int twice (int v) {
2 return 2∗v;
3 }
4
5 void testme (int x, int y) {
6 z = twice (y);
7 if (z == x) {
8 if (x > y+10)
9 ERROR;
10 }
11 }
12 }
13
14 /∗ simple driver exercising testme () with sym inputs ∗/
15 int main() {
16 x = sym input();
17 y = sym input();
18 testme (x, y );
19 return 0;
20 }
\delta = \{x \rightarrow x_0,y \rightarrow y_0\}
\delta = \{x \rightarrow x_0,y \rightarrow y_0\}
\delta = \{x \rightarrow x_0,y \rightarrow y_0\,z \rightarrow 2y_0\}
\delta = \{x \rightarrow x_0,y \rightarrow y_0\,z \rightarrow 2y_0\}
if(e) S1 else S2
PC会被更新(then语句)，
PC = PC \cap \delta(e)
然后还会生成一个新的路径约束 (else语句)，
PC^{’} = PC \cap \lnot\delta(e)
PC会被更新(then语句)，
PC = PC \cap \delta(e)
然后还会生成一个新的路径约束 (else语句)，
PC^{’} = PC \cap \lnot\delta(e)
x0 = 2y_0 ，
x0 \neq 2y_0
(x0 = 2y_0)\cap(x_0>y_0+10) ，
(x0 = 2y_0)\cap(x_0 \leq y_0+10)
(x0 = 2y_0)\cap(x_0>y_0+10) ，
[注意]传递专业知识、拓宽行业人脉——看雪讲师团队等你加入！
