Daikon简介

来自官方的翻译

Daikon 是动态检测可能不变量的一种实现;也就是说,Daikon不变量检测器会报告程序中可能存在的不变量。不变量是程序在某个点或某些点上所持有的性质;它们通常出现在断言语句、文档和形式规范中。不变量可用于程序理解和许多其他应用。例如:'x.field > abs(y)'; 'y = 2*x+3'; '数组 a 是有序的'; 对于所有列表对象 lst,'lst.next.prev = lst'; 对于所有树节点对象 n,'n.left.value < n.right.value'; 'p != null => p.content in myArray';等等。

这样的解释可能有点太晦涩，下面是省流版

Daikon是一个工具,它可以通过观察程序运行时的数据,自动发现一些潜在的规律或模式,我们把这些规律或模式称为不变量。比如说,你写了一个程序对一组数字从小到大排序。在排序之后,数组中的元素肯定是按升序排列的,即array[i] <= array[i+1]。这就是一个不变量,无论输入数据是什么,只要排序成功,这个性质总是成立。再举一个例子,如果一个程序购物车的代码,不变量可能是”购物车不为空,则必须有商品被添加”。

Daikon可以自动分析程序运行轨迹,发现诸如”数组是排序的”、”购物车非空必有商品”这样的不变量规律,并将它们报告给程序员,供他们理解程序、检查错误或声明一些规范性的性质。

安装Daikon

安装Daikon所需环境

首先需要安装JDK，如果使用的是Centos 7自带的，则使用不了javac等命令，需要参考javac命令报错bash:javac:command not found这篇博客进行修改

安装JDK可以参考CentOS7 安装jdk8教程这篇文章

下载Daikon

# 找一个位置新建一个daikonparent文件夹，假设建立在home目录下
mkdir daikonparent
# 移动到daikonparent文件夹
cd daikonparent
# 下载
wget http://plse.cs.washington.edu/daikon/download/daikon-5.8.18.tar.gz
# 解压
sudo tar zxf daikon-5.8.18.tar.gz

tips：如果下载太慢，如果是虚拟机的话可以用下载到本机上，利用VMware Tools之类的工具拷到虚拟机上（移动后一定检查文件完整不！！！这没弄好导致卡了我半天）。如果不是虚拟机，可以试试wget换源的操作，如果还不行，最好使用magic了

配置Daikon

# 转到用户根目录
cd ~
# 打开配置文件.bashrc
sudo vim .bashrc

然后在.bashrc文件最下面加入下面两句话（按下I键进入插入模式，在最下面粘贴完下面两句话后，按下ESC，然后输入:wq保存并退出）

# 你自己的Daikon绝对路径，以刚刚建立在home下daikonparent文件夹的为例
export DAIKONDIR=daikonparent/daikon-5.8.18
source $DAIKONDIR/scripts/daikon.bashrc

然后应用设定

source .bashrc

编译 Daikon 并构建其他工具

# 安装make工具
sudo yum install make

sudo make -C $DAIKONDIR rebuild-everything
make -C $DAIKONDIR compile
make -C $DAIKONDIR daikon.jar

之后会编译一段时间就安装完成了，编译完成后是支持Java语言的

验证安装

这里使用Daikon自带的测试用例

# 进入测试用例目录
cd $DAIKONDIR/examples/java-examples/QueueAr
# 编译Java文件
sudo javac -g DataStructures/QueueArTester.java
# 对QueueArTester程序进行监控和追踪执行
sudo java -cp .:$DAIKONDIR/daikon.jar daikon.DynComp DataStructures.QueueArTester
# 运行QueueArTester程序，并生成一个声明文件，其中包含了程序中变量的类型信息等
sudo java -cp .:$DAIKONDIR/daikon.jar daikon.Chicory --daikon --comparability-file=QueueArTester.decls-DynComp DataStructures.QueueArTester
# 与第3条类似，仅仅运行程序并使用之前生成的声明文件
sudo java -cp .:$DAIKONDIR/daikon.jar daikon.Chicory --comparability-file=QueueArTester.decls-DynComp DataStructures.QueueArTester
# 运行Daikon不变量检测器,输入之前生成的追踪文件
sudo java -cp $DAIKONDIR/daikon.jar daikon.Daikon QueueArTester.dtrace.gz

如果能生成QueueArTester.dtrace.gz文件，则说明安装成功，这里是仅支持Java的，如果想支持C++还需要安装kvasir

image-20240511230506582