源码地址：vigor_github
论文地址：vigor_paper
幻灯片地址：vigor_slide

环境搭建

代码中提供了setup.sh，可一键完成环境下载和配置。此外readme.md中提到的为了提高性能，配置hugepage=2M*4096，可使用命令echo 4096 > /sys/kernel/mm/hugepages/hugepages-2048kB/nr_hugepages完成（默认hugepagesz=2M）

但是在运行setup.sh过程中，因为实验室网络的原因，有很多配置如DPDK安装包和ocaml包等等下载不了。
于是我选择了作者提供的第二套方案——docker。此时如果单纯的运行Docker_build.sh，其实就是重新构造一个vigor的image，这时还是跟宿主机一个网络，同样还是不能完成下载。
然后我选择直接docker pull dslabepfl/vigor，用别人配置好的docker环境。pull完之后再运行setup.sh就可以完成环境配置。

代码阅读

框架

先选个NF如vignat，进到对应目录。根据readme.md所说，输入make symbex validate完成对vignat的验证，观察运行结果。

观察vignat/Makefile，发现并没有目标文件，而是去包含了上级Makefile文件。

include $(abspath $(dir $(lastword $(MAKEFILE_LIST))))/../Makefile

跟着向上翻，发现按照我们的输入make参数，是会去继续包含Makefile.dpdk

ifeq (click,$(findstring click,$(shell pwd)))
# Click baselines
include $(SELF_DIR)/Makefile.click
else ifeq (nfos-,$(findstring nfos-,$(MAKECMDGOALS)))
# NFOS-related targets
include $(SELF_DIR)/Makefile.nfos
else ifeq (,$(findstring moonpol,$(abspath $(NF_DIR))))
# DPDK-based NFs
include $(SELF_DIR)/Makefile.dpdk
endif

跟着翻，发现有symbex和validate目标，参数都可以在上述三个文件找到。

symbex validate 其中clean目标在原本文件中，autogen目标在根目录的Makefile中 autogen

主要是validate目标中执行的命令是切换到validator/目录去执行Makefile，跟着看看。发现vig%目标，其中%是通配符，$@表示目标文件，在图中代表vignat。

validator/Makefile

这样再加上时间的输出结果，就可以发现我们以上的流程跟之前图示的输出结果基本一致，这样就大概能明白程序的流程，接下来就是一部分一部分代码深入去阅读。

Validator

参考论文中提到的验证的四个关键步骤，其中Validator完成了2,3,4三步。

在validator目录中完成的大部分都是定理生成和定理证明的事情，所以需要用到更为专业的语言来完成工作，vigor中使用的就是OCaml函数式语言(VeriFast也是用了该语言)。第一次接触这种函数式语言，简单学习了一下

https://riptutorial.com/zh-CN/ocaml
https://ocaml.org/learn/tutorials/index.zh.html

观察validator/validator.ml文件。因为实在不熟悉OCaml，所以大部分情况都是靠猜，然后看了一下代码，觉得Verifier.verify_ir函数看起来像是在验证某些东西。

  match Verifier.verify_ir
          ir verifast_bin intermediate_fout
          verify_out_fname proj_root lino_fname
  with
  | Verifier.Valid -> printf "Valid.\n"
  | Verifier.Inconsistent -> printf "Inconsistent.\n"
  | Verifier.Invalid_seq -> printf "Invalid.\n"
  | Verifier.Invalid_rez _ -> printf "Invalid output.\n"

根据OCaml的命名规则，Verifier.verify_ir调用的是verifier.ml中的verify_ir函数（ml文件命名首字母小写，调用的时候大写）。vefirier.ml还是比较好看懂的，代码量也少，大概的意思就是完成上述步骤4的工作，调用verifast工具验证每条trace。

首先第一行命令调用了Render.render_ir函数，其中~表示的是标签参数，即render_assertions这个参数复制为true，跟进看一下。
第一行let ir = discard_redundant_preconditions ir in根据命名猜一下，该函数的作用应该是去除多余的前置条件，再跟进。
其中~f的是~f:f的简写，具体如下：
跟进Ir.term_eq，发现个模式匹配，关键里面有一堆看不懂的函数，如Bop之类
搜一下，发现是个类似宏定义的存在，如Bop就是bop、tterm、tterm三个参数组成，其中bop可以是各种运算，tterm是由递归定义完成，从而可以完成嵌套运算。
那么刚才的term_eq函数就可以，算了，我还是没看懂term_eq干了啥，那不妨猜一下吧，filter_redundant_preconditions函数可能是根据前后条件匹配关系，过滤掉了缺少后置条件的那些“多余”的前置条件。

未完待续