操作系统形式化验证实践教程(4) - 工具环境

如前面我们所了解的，Isabelle/HOL是套相当复杂的系统，它的底层基于Standard ML语言，它自己使用HOL和Isar语言，它可以生成ocaml，haskell和scala的代码，它有要使用到很多的自动定理证明工具。

除了相当强大的IDE环境，Isabelle也提供了命令行工具和大量的配置。

Isabelle环境

可以通过isabelle getenv -a命令获取Isabelle的详细配置信息：

我们分类列举一些常见的配置项，通过这些大家可以理解到Isabelle/HOL底层的架构：

• 基本参数
  • ISABELLE_HOME=/workspace/xulun/Isabelle2020
  • ISABELLE_ROOT=/workspace/xulun/Isabelle2020
  • ISABELLE_PLATFORM64=x86_64-linux
  • ISABELLE_PLATFORM_FAMILY=linux
  • ISABELLE_COMPONENTS_BASE=/home/ziying.liuziying/.isabelle/contrib
  • ISABELLE_HEAPS=/home/ziying.liuziying/.isabelle/Isabelle2020/heaps
  • ISABELLE_FILE_FORMATS=isabelle.Bibtex$File_Format
  • ISABELLE_DOCS=/workspace/xulun/Isabelle2020/doc:/workspace/xu - lun/Isabelle2020/src/Tools/jEdit/dist/doc
  • ISABELLE_LOGIC=HOL
• Standard ML相关
  • ML_SYSTEM=polyml-5.8.1
  • ML_PLATFORM=x86_64_32-linux
  • ML_OPTIONS=--minheap 500
  • ML_IDENTIFIER=polyml-5.8.1_x86_64_32-linux
  • ML_SOURCES=/workspace/xulun/Isabelle2020/contrib/polyml-5.8.1-20200228/src
  • ML_HOME=/workspace/xulun/Isabelle2020/contrib/polyml-5.8.1-20200228/x86_64_32-linux
  • POLYML_HOME=/workspace/xulun/Isabelle2020/contrib/polyml-5.8.1-20200228
• Java相关
  • ISABELLE_JAVA_PLATFORM=x86_64-linux
  • ISABELLE_JAVA_SYSTEM_OPTIONS=-server -Dfile.encoding=UTF-8 -Disabelle.threads=0 -Djdk.gtk.version=2.2
  • ISABELLE_TOOL_JAVA_OPTIONS=-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss16m
  • SCALA_HOME=/workspace/xulun/Isabelle2020/contrib/scala-2.12.10
  • ISABELLE_SCALA_SCRIPT=/workspace/xulun/Isabelle2020/bin/isabelle_scala_script
• ocaml相关
  • ISABELLE_OCAML_VERSION=ocaml-base-compiler.4.05.0
• Haskell相关
  • ISABELLE_STACK_ROOT=/home/ziying.liuziying/.stack
  • ISABELLE_GHC_VERSION=ghc-8.6.4
• 自动定理证明相关
  • ISABELLE_ATP=/workspace/xulun/Isabelle2020/src/HOL/Tools/ATP
  • Z3_HOME=/workspace/xulun/Isabelle2020/contrib/z3-4.4.0pre-3/x86_64-linux
  • VAMPIRE_HOME=/workspace/xulun/Isabelle2020/contrib/vampire-4.2.2/x86_64-linux
  • CVC4_HOME=/workspace/xulun/Isabelle2020/contrib/cvc4-1.5-5/x86_64-linux
  • CVC4_INSTALLED=yes
  • E_HOME=/workspace/xulun/Isabelle2020/contrib/e-2.0-3/x86_64-linux
  • VAMPIRE_VERSION=4.2.2pre
  • CVC4_SOLVER=/workspace/xulun/Isabelle2020/contrib/cvc4-1.5-5/x86_64-linux/cvc4
  • Z3_SOLVER=/workspace/xulun/Isabelle2020/contrib/z3-4.4.0pre-3/x86_64-linux/z3
  • Z3_VERSION=4.4.0pre
• 编辑器相关
  • JEDIT_HOME=/workspace/xulun/Isabelle2020/src/Tools/jEdit
  • JEDIT_SETTINGS=/home/ziying.liuziying/.isabelle/Isabelle2020/jedit
• LaTeX相关
  • ISABELLE_LATEX=latex -file-line-error
  • ISABELLE_PDFLATEX=pdflatex -file-line-error

Isabelle会话

证明是一个复杂的系统，涉及到很多库和文档等的协作。所以除了每个定理文件之外，我们还需要一个类似于Makefile一样的工程组织文件，在Isabelle中被称为会话ROOT规范。文件名就叫ROOT。

我们就不像规范一样描述结构了，直接上个真实的例子，这个例子来源于seL4的C-parser：

chapter "C-Parser"

session "Simpl-VCG" = Word_Lib +
  sessions
    "HOL-Statespace"
  theories
    "Simpl/Vcg"

session CParser = "Simpl-VCG" +
  sessions
    "HOL-Library"
    "HOL-Word"
    "Lib"
  theories
    "CTranslation"

Chapter

首先一个ROOT可以有个Chapter来描述下这个规范的名字，将来用于生成browse info时使用，如果没有指定的话默认为：“Unsorted”。总之就是个名字，没有形式化的含义。

session

session来定义一个会话单元，可以像面向对象编程一样继承自某个父会话。
格式为：

session 会话名 = 父会话名 + 
sessions
引用的会话列表
theories
定理列表

session中还可以指定路径，用in表示。另外还可以指定options。不谈语法，我们还是例子说话：

session AsmRefineTest in "testfiles" = AsmRefine +
  options [threads = 1] (* use of unsync references in test files *)
  sessions
    CParser
  theories
    "global_asm_stmt_gref"
    "inf_loop_gref"
    "global_array_swap_gref"

document_files

除了会话和定理之外，文档生成也是定理证明的重要部分。可以在options中指定输出的文档类型，然后通过document_files区段来指定文档要引用的文件。document_files也可以通过in来指定路径。我们还是看个例子：

session ASpecDoc in "abstract" = Word_Lib +
  options [document=pdf]
  sessions
    "HOL-Library"
    Lib
    ExecSpec
  theories
    "Intro_Doc"
  theories
    "Syscall_A"
    "Glossary_Doc"
    (* "KernelInit_A" *)
  document_files
    "VERSION"    (* generated by `make ASpec` *)
    "gitrev.tex" (* generated by `make ASpec` *)
    "root.tex"
    "root.bib"
    "defs.bib"
    "ulem.sty"
    "imgs/CDT.pdf"
    "imgs/seL4-background_01.pdf"
    "imgs/seL4-background_03.pdf"
    "imgs/seL4-background_04.pdf"
    "imgs/sel4objects_01.pdf"
    "imgs/sel4objects_05.pdf"
    "imgs/sel4_internals_01.pdf"
  document_files (in "document/$L4V_ARCH")
    "ARCH.tex"

小结

环境配好，ROOT文件写好，我们就可以通过isabelle build命令去执行编译和文档生成的命令了。

下一步，我们就直击一个形式化验证操作系统的现场，去看看seL4是如何进行形式化验证的。需要的基础后面用到我们会慢慢展开。