KLEE学习——实例1

下面开始根据KLEE官方给出的示例进行学习，闲话不多说，开始第一个示例的学习：Testing a small function
这个例子是引导我们熟悉使用klee测试简单函数所需的主要步骤，代码在/examples/get_sign目录下.
简单函数的代码如下，判断x的是0、正数、还是负数。

int get_sign(int x) {if (x == 0)return 0;if (x < 0)return -1;elsereturn 1;}

主要分为以下几个步骤：

1. 把输入符号化
为了使用KLEE测试这个函数，我们首先需要用符号化的输入去运行这个函数，klee提供了klee_make_symbolic()函数（定义在klee/klee.h中）将变量符号化，该函数接收3个参数：变量地址、变量大小、变量名（可以为任何值）。
下面是一个简单的例子，将变量a符号化并用它调用get_sign()：

int main() {int a;klee_make_symbolic(&a, sizeof(a), "a");return get_sign(a);}

2. 编译为LLVM位码
klee是基于LLVM位码的，因此我们首先需要将程序编译为LLVM位码，在klee_src/examples/get_sign目录下运行命令：

$ clang -I …/…/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c

解释一下命令的参数：
-I<dir>:添加目录到include搜索路径，这样我们的编译器才能找到klee/klee.h，里面定义了很多我们需要与klee虚拟机进行交互的内部函数，比如klee_make_symbolic.
-emit-llvm：对汇编程序和对象文件使用LLVM表示。
-c：只运行预处理、编译和汇编步骤。
-g：将调试信息添加到位代码文件中，以便之后使用该文件生成源代码行级别的统计信息。如果没有这个参数，将无法得到映射在源码层面的一些信息，不方便我们查看结果。
-O0 -Xclang -disable-O0-optnone：这个是一些优化相关的问题，具体暂时不做深入了解，具体的见：https://github.com/klee/klee/issues/902
以上及更多相关参数的了解可以通过以下命令自行查看：

$ clang --help

3. 运行KLEE
仍然在该目录下，直接执行命令：

$ klee get.sign.bc

我们能够得到输出如下：

通过输出，我们得到的信息是：我们一共有33条指令，3条路径，并生成了3个测试用例。
显然，3条路径分别是 a = 0, a < 0和 a >0.
其中，输出结果报告放在了 klee-out-0(或者klee-last)目录下(这里说明下，klee每执行一次都会生成一个klee-out-N，其中N是表示第几次的执行，这里我们只执行了一次，因此是0。除此之外，会生成一个klee-last的符号链接，指向最新生成的这个k查看lee-out-N)，我们查看下该目录：

关于生成的文件每个分别是什么，目前暂不需要深究，有需要可以参考详情见： http://klee.github.io/docs/files/

4. 利用KLEE生成测试用例
klee生成的测试用例都写在.ktest后缀的二进制文件中，可以通过ktest-tool工具查看:

这3个文件对应了我们之前得到输出的3个测试用例。
从这些文件里面，我们可以得到：
args: 调用程序时使用的参数,这个例子中只有程序名。
num objects: 符号对象在路径上的数量，在这个例子中只有1个。
object 0: name: 符号对面的名字
object 0 :int/uint: 符号对象实际的输入值（这里3个分别对应=0,>0,<0）

5. 重新使用测试用例运行程序
现在，我们可以用klee提供的库来将得到的测试用例作为输入来运行我们的程序。首先我们需要将我们的程序链接到klee提供的库libkleeRuntest：

$ export LD_LIBRARY_PATH=path-to-klee-build-dir/lib/:$LD_LIBRARY_PATH
$ gcc -I …/…/include -L path-to-klee-build-dir/lib/ get_sign.c -lkleeRuntest

注意，这里 path-to-klee-build-dir 是你自己klee_build的目录，这里我的是 /home/klee/klee_build。
因此，我需要输入的命令如下：

$ export LD_LIBRARY_PATH=/home/klee/klee_build/lib/:$LD_LIBRARY_PATH
$ gcc -I …/…/include -L /home/klee/klee_build/lib/ get_sign.c -lkleeRuntest

如果目录不对，将会报错如下：

接着，需要设置KTEST_FILE环境变量指向所需要测试的用例名：

$ KTEST_FILE=klee-last/test00000N.ktest ./a.out

这里，我们只有3个测试用例，我就全测了，结果如下：

可以看到，当我们用第一个用例测试，a=0，我们返回值也是0；第二个用例a=16843009,我们返回值为1；第三个用例a=-2147483648,返回值为-1（这里转换到了0-255范围，因此为255）。

总结：
用过这个例子，我们知道了用KLEE测试一个简单程序的整体流程（符号化输入）、编译为LLVM位码、用KLEE运行）和对结果的查看（主要信息在.ktest的几个文件），以及利用测试用例运行程序（链接klee提供的库）。

KLEE学习——实例1相关推荐

KLEE学习——实例3
说明: 这个例子展示了如何使用KLEE来寻找迷宫游戏的所有解决方案,是对如何使用符号执行来生成输入的一个很好的说明.示例官网原文见:Solving a maze with KLEE -实例中的迷宫大小 ...
KLEE学习——实例2
该例子通过符号化输入字符串来完成正则式匹配,实例来源见官网:Testing a Simple Regular Expression Library 1.编译生成LLVM位码源码所在目录为exampl ...
涵盖 14 大主题！最完整的 Python 学习实例集来了！
机器学习.深度学习最简单的入门方式就是基于 Python 开始编程实战.最近闲逛 GitHub,发现了一个非常不错的 Python 学习实例集,完全是基于 Python 来实现包括 ML.DL 等领域 ...
ajax请求返回json实例,Jquery Ajax 学习实例2 向页面发出请求返回JSon格式数据
一.AjaxJson.aspx 处理业务数据,产生JSon数据,供JqueryRequest.aspx调用,代码如下: protected void Page_Load(object sender, ...
php实训总结00字,说明的比较细的php 正则学习实例
说明的比较细的php 正则学习实例 "^The": 匹配以 "The"开头的字符串; "of despair$": 匹配以 "of ...
深度学习之生成对抗网络（1）博弈学习实例
深度学习之生成对抗网络(1)博弈学习实例博弈学习实例在生成对抗网络(Generative Adversarial Network,简称GAN)发明之前,变分自编码器被认为是理论完备,实现简单, ...
从入门到入土：Python爬虫学习|实例练手|爬取猫眼榜单|Xpath定位标签爬取|代码
此博客仅用于记录个人学习进度,学识浅薄,若有错误观点欢迎评论区指出.欢迎各位前来交流.(部分材料来源网络,若有侵权,立即删除) 本人博客所有文章纯属学习之用,不涉及商业利益.不合适引用,自当删除! 若 ...
从入门到入土：Python爬虫学习|实例练手|爬取百度翻译|Selenium出击|绕过反爬机制|
此博客仅用于记录个人学习进度,学识浅薄,若有错误观点欢迎评论区指出.欢迎各位前来交流.(部分材料来源网络,若有侵权,立即删除) 本人博客所有文章纯属学习之用,不涉及商业利益.不合适引用,自当删除! 若 ...
从入门到入土：Python爬虫学习|实例练手|爬取新浪新闻搜索指定内容|Xpath定位标签爬取|代码注释详解
此博客仅用于记录个人学习进度,学识浅薄,若有错误观点欢迎评论区指出.欢迎各位前来交流.(部分材料来源网络,若有侵权,立即删除) 本人博客所有文章纯属学习之用,不涉及商业利益.不合适引用,自当删除! 若 ...

KLEE学习——实例1

KLEE学习——实例1相关推荐

最新文章

热门文章