1 介绍

  • Daikon是一个动态检测不变量的工具

  • 不变量是程序中某个特定点上保持为真的属性，这些通常出现在断言语句，文档和形式化规范中。

  • 不变量在程序理解和其它许多应用中都非常有用，例如，不变量可以是

    • x.field > abs(y)
    • y = 2 * x + 3
    • 数组a是有序的
    • 对于所有的列表对象lst，kst.next.prev = lst
    • 等等，用户可以扩展Daikon以添加新的属性

  • 动态不变量检测通过运行程序，观察程序计算的值，然后报告在观察到的执行过程中始终为真的属性。

    • Daikon可以在C、C++、C#、Eiffel、F#、Java、Perl和Visual Basic程序中检测属性
    • 在spreedsheet文件中
    • 以及其它数据源中（动态不变量监测是一种可以应用于任意数据的机器学习技术）

  • Daikon完全开源

  • Daikon详情参考daion用户手册

  • 本文记录本人使用daikon过程

2 下载Daikon

  • 照着用户手册下载即可
  • 注意daikon需要的shell环境变量
export DAIKONDIR=daikonparent/daikon-5.8.18 # daikon的安装目录
source $DAIKONDIR/scripts/daikon.bashrc

3 使用案例

C/C++

  1. 需要使用 gcc 和 编译选项 -gdwarf-2 -no-pie产生可执行文件
    • 对于通过./configure生成的Makefile,在./configure前加入CC=gcc CFLAGS="-gdwarf-2 -no-pie"即可
  2. 使用 kvasir 前端产生daikon需要的文件，对于单次运行，只需要在正常运行指令前加上 kvasir-dtrace即可，示例
    • kvasir-dtrace ./wordplay -f words.txt 'Daikon Dynamic Invariant Detector'
  3. 随后使用daikon进行分析
java -cp $DAIKONDIR/daikon.jar daikon.Daikon \
    daikon-output/wordplay.decls daikon-output/wordplay.dtrace

程序多次运行轨迹

  • 对于多次运行的程序，需要将多次运行的轨迹合并，此时可以将各个轨迹分开，或者合成一个轨迹文件
  • 分开轨迹文件（此种写法更好一些）
kvasir-dtrace --dtrace-file=daikon-output/wordplay1.dtrace \
    ./wordplay -f words.txt 'daikon dynamic invariant detector'
kvasir-dtrace --no-dyncomp --dtrace-file=daikon-output/wordplay2.dtrace \
    ./wordplay -f words.txt 'better results from multiple runs'
kvasir-dtrace --no-dyncomp --dtrace-file=daikon-output/wordplay3.dtrace \
    ./wordplay -f words.txt 'more testing equals better testing'
java -Xmx3600m -cp $DAIKONDIR/daikon.jar daikon.Daikon \  # 这里-Xmx3600m是为了增加java的堆栈大小,在大数据量的情况下需要
    daikon-output/wordplay*.dtrace daikon-output/wordplay.decls # 这里的*是通配符
  • 合并轨迹文件
kvasir-dtrace --dtrace-file=daikon-output/wordplay-all.dtrace \
    ./wordplay -f words.txt 'daikon dynamic invariant detector'
kvasir-dtrace --no-dyncomp --dtrace-append \
    --dtrace-file=daikon-output/wordplay-all.dtrace \
    ./wordplay -f words.txt 'better results from multiple runs'
kvasir-dtrace --no-dyncomp --dtrace-append \
    --dtrace-file=daikon-output/wordplay-all.dtrace \
    ./wordplay -f words.txt 'more testing equals better testing'
java -Xmx3600m -cp $DAIKONDIR/daikon.jar daikon.Daikon \
    daikon-output/wordplay-all.dtrace daikon-output/wordplay.decls

注意事项

  • 在示例中，很重要的一个示范是
java -cp $DAIKONDIR/daikon.jar daikon.Daikon \
     --config_option daikon.derive.Derivation.disable_derived_variables=true \
     daikon-output/wordplay.decls daikon-output/wordplay.dtrace
  • 这里通过配置选项禁止派生变量的生成，大大减少了运算时间，而这派生变量许多都是无用的，这在第五部分Daikon输出中会有所说明

4 运行Daikon

  • 运行Daikon使用以下命令：
java -jar daikon.jar --input=<dtrace文件路径> <其他选项>
  • 其中<dtrace文件路径>是你要分析的.dtrace文件的路径
  • <其他选项>是可选的命令行参数，用于配置Daikon的行为。例如，你可以使用–output=<输出文件路径>选项来指定输出文件的路径，或者使用–help选项来查看所有可用的命令行选项。
  • 各Daikon的前端使用各不相同，详见手册
  • spinfo文件是用于检测条件不变量（Conditional invariants）的分割信息文件。这些文件是可选的，可以自动创建或手动创建。

4.1 控制Daikon输出的选项

  • –help
  • -o inv_file:将序列化的不变量输出到指定文件，默认生成与dtrace文件同名的.inv.gz文件
  • –no_text_output:不将不变量作为文本输出
  • –format name：以给定格式生成输出，有关Daikon支持的输出列表参阅invariant语法
  • –show_progress/–no_show_progress:打印或不打印执行Daikon主要部分的时间信息
  • –show_detail_progress:同上，还包括不变量的详细信息
  • –noversion:禁止打印版本信息
  • –output_num_samples:输出不变量和程序点的数值和样本数量，这是一个调试选项，帮助理解Daikon产生了怎样的输出
  • –files_from filename：从给定的文本文件中读取一系列.decls、.dtrace或.spinfo文件名，作为在命令行上提供文件名的替代方法
  • –server dirname：Daikon的服务器模式，在该模式下，它会读取dirname中的文件（按字典顺序排序），直到找到一个以“.end”结尾的文件，然后计算并输出不变量

4.2 控制不变量探测的选项

  • –conf_limit val：是一个命令行选项，用于设置Daikon在证明不变量的置信度限制。只有当给定的不变量置信度大于这个值Daikon才会输出
    • val在0到1之间，.99为默认值，越大的值过滤越强
    • 每种类型的不变量都有自己确定置信度的方法，参见Java 源代码中的 invariant 的 computeConfidence 方法。
    • 考虑不变量a，有两种打印不变量置信度的方法
      • 使用Diff（参见invariant Diff） java -cp $DAIKONDIR/daikon.jar daikon.diff.Diff MyFile.inv.gz
      • 使用PrintInvariants (参见 Printing invariants)java -cp $DAIKONDIR/daikon.jar daikon.PrintInvariants --dbg daikon.PrintInvariants.repr \ MyFile.inv.gz
    • 要打印被丢弃的每个不变量的置信度，请使用 --disc_reason all 命令行选项运行 Daikon（参见 Daikon Daikon debugging options）
  • –list_type classname:表示给定的类实现了java.util.List接口。See ListImplementors declaration
  • –user-defined-invariant classname:使用在给定类中定义的用户定义的不变量，而不是内置在Daikon中的不变量。
  • –disable-all-invariants：禁用所有已知的不变量：那些内置在Daikon中的不变量，以及到目前为止通过–user-defined-invariant指定的所有不变量。在此选项指定后，可以重新启用某个不变量，参见启用/禁用特定不变量的选项。
  • –nohierarchy：避免在数据流层次结构中连接程序点。
  • –suppress_redundant：使用Simplify自动定理证明器抑制逻辑上多余的不变量的显示。

4.3 操作部分trace文件

  • –ppt-select-pattern=ppt_regexp：仅处理名称与正则表达式匹配的程序点。–ppt-omit-pattern参数优先于此参数
  • –ppt-omit-pattern=ppt_regexp：不处理名称与正则表达式匹配的程序点。此参数优先于–ppt-select-pattern参数
  • –var-select-pattern=var_regexp：仅处理名称与正则表达式匹配的变量（无论是在跟踪文件还是在派生中）。–var-omit-pattern参数优先于此参数。
  • –var-omit-pattern=var_regexp：忽略名称与正则表达式匹配的变量（无论是在跟踪文件还是在派生中）。此参数优先于–var-select-pattern参数。
  • 将以上命令传给前端工具，可以让目标程序运行得更快，跟踪文件更小

4.4 Daikon配置选项

  • –config filename: 从指定的文件中读取配置选项。更多信息参见 Configuration options
  • –config_option name=value:指定一个配置选项

4.5 Daikon调试选项

  • 更多参见后续 Debugging options
  • –dbg category 和 --debug：这两个选项用于启用特定部分的Daikon的调试输出（日志输出）。可以通过多次指定–dbg category来实现对调试输出的细粒度控制。–debug选项会打开所有调试标志，这会产生很多输出！
  • –track class<var1,var2,var3>@ppt：此选项用于在指定的类、变量和程序点上启用调试信息。
  • –disc_reason inv_class<var1,var2,…>@ppt：此选项打印指定程序点处被丢弃的inv_class类的不变量，以及简短的原因和解释为什么它们不值得打印。
  • –mem_stat：此选项将内存使用情况统计信息打印到当前目录中名为stat.out的文件中

5 Daikon输出