本文主要是介绍SAT、SMT、Z3和符号执行（2），希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！
符号执行（symbolic execution）是一种计算机科学领域的程序分析技术，通过采用抽象的符号代替精确值作为程序输入变量，得出每个路径抽象的输出结果。 这一技术在软件测试中有很重要的应用，能够有效地发现程序中的漏洞。本专栏中前面已经介绍过在angr中使用符号执行来解决CTF题目的例子。本文将通过几个例子来演示一下symbolic execution（或者SMT solver）在软件分析领域的应用。
一、程序等价性检验（Program Equivalence Checking）
这是《深入理解计算机系统》（参见【1】）中给出的一个问题。有一段计算机程序，在使用之前定义好的宏变量M和N后被编译成了二进制代码。由于编译器对程序中的乘法和除法运算做了一些优化，当把二进制代码反编译回C代码之后，对比两份源码，其实很难看出来它们是等价的（尽管它们确实是等价的）。现在的问题是，想求出：M和N的值到底是多少？
注意我们这里不会使用《深入理解计算机系统》中的分析方法（那个相当于是手工分析）。现在我们希望使用SMT solver来解决这个问题。
#!/usr/bin/env python3
from z3 这篇关于SAT、SMT、Z3和符号执行（2）的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！
