angr的强大能力不仅因为它是一个模拟器，还因为它能够使用我们称为“符号变量”的东西参与程序的执行。它可以使用一个符号，也就是一个名字，来代替程序执行中的确切数值。然后，在使用符号进行数学运算的过程中，将会产生一棵树(这棵树在编译理论中被称为抽象语法树或AST)。这些AST可以被解释为SMT解析器中的约束条件，就像Z3(另一个python的约束求解库)做的一样。为了回答这样一个问题：“已知经过一系列操作之后得到的输出，输入应该满足怎样的条件？”，在这里，你将会学习如何使用angr来解决这个问题。

使用位向量

让我们获取一个Project和state来开始和数字们玩耍吧！

markdown-img-paste-20180119095646948.png

一个位向量就是一个比特序列，可以解释为数学上的有界整数。让我们先生成一些位向量：

markdown-img-paste-20180119100158826.png

正如你看到的，你可以声明许多比特序列并且把他们称为位向量。你还可以对他们进行数学计算：

markdown-img-paste-20180119100524616.png

你不能做诸如one+weird_nine这样的操作。对不同长度的位向量做数学运算，将会导致一个类型错误。然而，你可以扩展这个weird_nine，让他具有合适的比特长度：

markdown-img-paste-2018011910103718.png

zero_extend将会用零扩展位向量的高位。为了在扩展时保持二进制补码表示的有符号整数的值，你还可以使用sign_extend来带符号扩展一个位向量

现在让我们混入一些符号参与计算：

markdown-img-paste-20180119102311524.png

x和y现在是“符号变量”，这跟咱们小学学的未知数是一个意思。注意，你提供的符号名（第一个参数）的后面被添加了一个递增的计数值。你可以对这些符号变量做数学计算，想做多少就做多少，但是你不会得到一个数值的结果，而是得到一个AST：

markdown-img-paste-20180119102407769.png

从技术概念上说x和y甚至one都是AST——即使只有一层。为了理解这一点，让我们学习如何处理AST。

每一个AST都有.op和一个.args。“op”是一个定义了要执行的运算的属性，“args”是参与运算的操作数。除非op是字符串"BVV"或"BVS"，所有的args都是AST。AST的终结节点是BVV或BVS。

译者注：对于AST的具体形式，上面文档中的解释很别扭，按照我的理解，当op是"BVV"或"BVS"时，args就代表了构成BVV和BVS的参数：值/符号，宽度。因此任意一个BVV或BVS对象都是一个有特殊op和args的AST。直接看下面的例子会比较好理解。

markdown-img-paste-2018011910574763.png

从现在开始，我们将会使用“位向量”这个词来表示一个最上层运算产生一个位向量的AST。通过AST还可以表示其他数据类型，包括浮点数和布尔类型(我们很快会看到)。

符号约束

将任意两个类型相似的AST进行比较操作将会产生一个新的AST——不是一个位向量，而是一个符号化的布尔类型:

markdown-img-paste-20180119111146877.png

从上述例子中你可以看出AST间的比较默认是无符号的。例子中的-5将会被包装为<BV64 0xfffffffffffffffb>，这个数被解释为无符号数之后，显然大于100 。如果你想让比较是带符号的，你可以使用one_hundred.SGT(-5)（SGT意思是“signed greater-than”）。在本章的最后可以找到完整的AST操作列表。

上面的例子还阐述了一个使用angr的要点——你不应该直接在一个if或while语句中使用两个变量的比较结果作为判断标准，因为这个比较结果可能不是一个确定的真值。即使比较的结果为真，if one > one_hundred将会产生异常。你应该使用solver.is_true和solver.is_false，它们将会测试出一个具体的真假值，而不执行约束求解。

markdown-img-paste-20180119114335393.png

译者注：如果使用在if语句中会报如下错误：

markdown-img-paste-20180119114509867.png

约束求解

你可以用加入一个约束条件到一个state中的方法（state.solver.add），将每一个符号化的布尔值作为一个关于符号变量合法性的断言。之后可以通过使用state.solver.eval(symbol)对各个断言进行评测来求出一个合法的符号值（若有多个合法值，返回其中的一个）。

一个例子可能会比文字更清楚：

markdown-img-paste-20180119115412786.png

通过添加这些约束到一个state中，我们已经迫使约束求解器考虑我们添加的断言，求解器返回的值必须满足这些断言。如果你运行上面的例子，你可能会得到x的不同值，但是这个值将必然大于3(因为y > 2且x >= y 且 x <= 10)。此外，如果你接着用state.solver.eval(y)求解y，你将会得到一个被之前求解出的x的值限制的y值。

译者注：比如例子中得到x为9，那么接着求解y，y的值就必须小于或等于9

如果在两次求解之间你没有添加任何其他的约束条件，那么两次求解的结果将会是一致的。

译者注：我理解是后求解的结果会被先求得的符号值约束，不知道文档中的“一致”是什么意思。

从现在开始，我们就明白了该如何解决本章开头提出的问题——找到一个产生指定输出的输入：

markdown-img-paste-20180120131104994.png

再次提醒，这样的求解方式只适用于位向量的语义下(也就是之前提到的AST)。如果我们在整数域上做上面的操作，将会是无解的。

译者注：这里有一点不解，如果是整数域上的求解，那需要求解的符号不也是用位向量来表示吗？文档并没有给出这种情况下无解的例子，故不知道怎么理解。

如果我们将两个互相矛盾或相反的约束加入一个state.solver中，比如没有一个值能够满足所有约束，那么这个state就变成了unsatisfiable，或者unsat，并且对这样的state求解会导致异常。你可以用state.satisfiable()检查一个state是否可解，接着上面的例子：

markdown-img-paste-2018012013223067.png

你还可以加入更复杂的表达式，而不仅是包含一个符号变量的表达式：

markdown-img-paste-20180120133439498.png

上面的测试发现这个eval解出的y居然是负数，且如果只给y < 0的约束来求解y，则会导致无解异常，待我问问作者。

这里我们可以看到，eval是一个通用的方法，它在考虑整个state(的约束)的情况下，将任意位向量转换为python基本类型。这也是为什么我们使用eval来将具体的位向量转换为python的int类型的原因。

没有给例子，不知道如何用eval完成位向量和int的转换

还需要注意的是符号变量x和y可以在新的state中被使用，尽管它在旧的state中被创建。符号变量不和state绑定，它们是自由存在的。

浮点数

z3(一个约束求解的python库)已经提供了对IEEE754浮点数标准的支持，并且因此angr也能够使用它们（因为angr集成了z3）。创建浮点数向量和创建一个向量主要的不同在于，浮点数向量的第二个参数不是位向量宽度，而是一个sort。你可以使用FPV和FPS来创建一个浮点值和符号。

markdown-img-paste-20180120160556970.png

有许多需要解释的东西——首先对于浮点数向量的显示并不是很好，但是抛开这个不谈，大多数的浮点数操作实际上都有第三个参数，它在你使用二进制运算符时被隐式地添加——这个参数是舍入模式。IEEE754定义了多个舍入模式(向最近的数舍入，向0舍入，舍入到正数等等)，所以z3必须支持它们。如果你想要对某个操作（比如solver.fpAdd）指定舍入模式，你就得在使用该操作时显示声明一个舍入模式(solver.fp.RM_*中的一个)作为参数。

浮点数符号的约束和求解工作按照和整型符号相同的方式工作，但是使用eval将会返回一个浮点值：

markdown-img-paste-20180120164212448.png

这很好，但是有时候我们需要能够直接和浮点数的位向量形式直接交互。你可以使用raw_to_bv和raw_to_fp将位向量解析为浮点数，反之亦可：

markdown-img-paste-20180120214915915.png

这些转换保留了位模式，就像把一个int指针转为浮点指针(或相反)一样。然而，如果你想尽量不丢失精度，当你想将一个浮点数转为int（或反过来）你可以使用另一组方法：val_to_fp和val_to_bv。由于浮点数的浮点特性，这些方法必须将目标值的位宽或种类作为参数：

markdown-img-paste-20180120220329560.png

这些方法还可以加一个signed参数，指定源或目的位向量是否是有符号的。

译者注：signed参数用法如下：

markdown-img-paste-20180120221119455.png

更多的解析方式

eval将会给出一个符合约束条件的可行解，但是如果你想要多个可行解时怎么办呢？你如何确定这个解是不是唯一的？解析器为你提供了一些通用的解决方案：

• solver.eval(expression) 将会解出一个可行解
• solver.eval_one(expression)将会给出一个表达式的可行解，若有多个可行解，则抛出异常。
• solver.eval_upto(expression, n)将会给出最多n个可行解，如果不足n个就给出所有的可行解。
• solver.eval_exact(expression, n)将会给出n个可行解，如果解的个数不等于n个，将会抛出异常。
• solver.min(expression)将会给出最小可行解
• solver.max(expression)将会给出最大可行解

另外，上述这些方法都可以接收如下关键字参数：

• extra_constraints可以传入元组形式的约束条件。这些约束将会在本次求解中被考虑，但是不加入state中。
• cast_to可以接收一个参数来指定把结果映射到哪种数据类型。目前这个参数只能是str，它将会以字符串形式展示返回的结果。例如：

markdown-img-paste-20180120233038900.png

小结

内容真多！读完本章之后，你应该能够创建和操作位向量、布尔值和浮点数来形成操作树，之后用附加在state上的约束求解器，根据约束条件集，求得一个（或多个）可行解。希望你读完本章能够体会到用AST来表示运算以及约束求解器的强大。

在附录中，你能够找到可以对AST进行的所有操作。