这里是 2021-2022 年春季学期软件分析与验证课程大作业任务说明文档，本次课程大作业的目标是完成一个具有以下功能的程序验证工具：
- 对于给定的带有部分正确性验证标注的输入程序源码，能够返回其部分正确性验证的结果。
- 对于给定的带有部分正确性验证标注和秩函数的输入程序源码，能够返回其完全正确性验证的结果。
- 完成工具报告，大致描述你的实现过程、过程中遇到的问题以及解决方式。
推荐实现的验证算法为演绎验证，其在参考教材 The Calculus of Computation: Decision Procedures with Applications to Verification 的第五章 Program Correctness: Mechanics 中有详尽的介绍。
以下是对本次大作业所需实现的程序验证工具的输入和输出的描述。
一个符合语法规范的，带有前置条件、后置条件、循环不变式、断言以及秩函数等验证标注的，文本格式的 CMinor 语言的代码文件。
CMinor 语言的源程序部分大致是 C 语言的子集，验证标注部分大致是 ACSL 语言的子集。
注意：秩函数是一个整型表达式或整形表达式的元组，对于带有秩函数的源码文件，我们保证其文件中所有函数及循环都被标注了秩函数，且要么所有秩函数都是一个整形表达式、要么所有秩函数的元组长度均相同。
对于一个合法的输入，所实现的验证工具会在运行结束后，在其标准输出流中输出对应的验证结果。具体格式为：
VERIFIED：程序中所有验证标注均为有效的，即其部分正确（如果源码中没有秩函数）或者完全正确（如果源码中有秩函数）；UNVERIFIED：程序中并非所有验证标注都有效的，即其部分正确性（如果源码中没有秩函数）或者完全正确性（如果源码中有秩函数）不成立；UNKNOWN：程序中验证标注的有效性未知。
验证工具的实现框图如下图所示。它包含了从程序源码到验证结果的全部流程。其中，src 表示程序源代码，AST 表示抽象语法树（Abstract Syntax Tree），CFG 表示控制流图（Control-flow Graph），VC 表示验证条件（Verification Condition），solver 表示 SMT 求解器，res 表示需要输出的验证结果。其中，验证条件VC的生成，我们使用 ded-verif（deductive verification）验证算法。
在以下框图中，从源代码（src）到控制流图（CFG）的部分，和本课程教授的内容关系不大。因此，在本次作业任务中，这部分的实现，已经由助教完成，并以源码的形式给出，大家可以直接使用。而从 CFG 到验证结果（res）的部分，则是本课程所教授的核心内容，需要同学们自己独立完成。
parser | ded-verif solver
| | | |
src ---> AST ---> CFG -------> VCs ---> res
|
by TA | by 'yourself'
|验证工具输入的源代码 src 使用 CMinor 语言，一种面向教学的验证语言，其形式化语法文法如 ANTLR 文法文件 CMinorParser.g4 和 CMinorLexer.g4 中所示。
CMinor 语言支持两种 C 中的原子类型 int、float，支持这两种原子类型的定长的一维数组的定义和读写，也支持以这两种原则类型为成员的结构体（struct），同时也支持 C 语言中最基本的顺序、条件（if-then-else）和循环（while、for 和 do-while）语句，以及函数。
以下是一个使用 CMinor 语言描述的程序的例子。在函数 fun 中，变量 count 的值从 0 开始不断增大 1，直到其值不再小于 10。随后，该函数将返回 count。
int fun() {
int count = 0;
while (count < 10)
{
count = count + 1;
}
return count;
}由于 CMinor 语言是验证语言，所以还会额外支持用于程序验证的标注，这些标注是一种以 /*@ 或者 //@ 开头的特殊的注释。
对于 CMinor 语言中的任意一个函数，都必须使用一阶逻辑公式标注其前置条件（requires）和后置条件（ensures）。同时，在循环头位置，也必须标注对应位置的循环不变式。基于前置条件和后置条件的标注，形成了一个程序验证任务。即证明对于所有在初始情况下，满足前置条件的程序执行路径，在其“末端”后置条件也需要满足。
除了前置后置条件和循环不变式外，CMinor 语言还支持对断言的标注。并且对于除数、数组下标和数组长度，会自动生成运行时断言（runtime assertion）：“除数不为零”、“数组下标非负”、“数组下标小于数组长度”。
在验证标注中，CMinor 支持三种数学意义上的原子类型：integer、real 和 boolean，类型为 C 中的 int 或 float 的程序变量，在验证标注中会被提升成类型为 integer 或 real 的数学变量，也就是说我们在验证标注中无需考虑越界和取整的问题。所有标注的逻辑公式均使用一阶逻辑描述，即其可以被量词（\forall 和 \exists）限定。
以如下的程序为例，函数 fun 的前置条件 为 \true，后置条件 为 \result == 10，即返回值（return value）等于 10。那么，对于如下的输入，程序验证工具需要证明，函数 fun 在任何条件下（\true 表示始终满足），其返回值都满足 \result == 10。为证明该结论，需要使用循环不变式 count <= 10。
/*@ requires \true;
@ ensures \result == 10; */
int fun() {
int count = 0;
//@ loop invariant count <= 10;
while (count < 10)
{
count = count + 1;
}
return count;
}为了证明程序的完全正确性，还需要证明程序的终止性，即程序的执行路径都是有限的。为此，CMinor 语言还支持用于证明终止性的秩函数的标注。秩函数是一个整形表达式或整形表达式的元组，在函数头以 decreases 标出，在循环头以 loop variant 标出。所有有效的秩函数标注的值都是非负的。同时，对于程序中的任意一条基本路径，在路径头标注的秩函数的值，都严格大于路径尾标注的秩函数的值（对于元组而言，是字典序意义上的大于）。以此便可以证明程序的任意执行路径都是有限的。
以如下的程序为例，函数 fun 入口位置标注的秩函数表达式为 11，而在循环入口标注的秩函数表达式为 10 - count。从程序入口的 11 到循环头的 10 - count 的基本路径上，可以证明秩函数表达式的值是严格下降的。同时，从循环头的 10 - count 到其自身的基本路径上，由于经过了语句 count = count + 1，故秩函数表达式的值也是严格下降的。11 是一个自然数，由循环不变式 count <= 10 可知 10 - count 的非负性，所以全体秩函数也是非负的。因此，可以判定秩函数标注的有效性，即程序的终止性。
注：在本次作业的验证任务中，对于函数头的秩函数，我们要求其非负性可以被函数的前置条件所蕴含；对于循环头的秩函数，我们要求其非负性可以被循环不变式所蕴含。
/*@ requires \true;
@ decreases 11;
@ ensures \result == 10; */
int fun() {
int count = 0;
/*@ loop invariant count <= 10;
@ loop variant 10 - count; */
while (count < 10)
{
count = count + 1;
}
return count;
}程序分析和验证一般在程序的控制流图上进行。控制流图是程序的一种图形表示，它将程序的控制流结构，以有向图的形式表示出来。在控制流图上的每一个节点是一个基本代码块（Basic Block），简称为基本块。而连接各个基本块的有向边称为控制流边。在控制流图中，原程序中的所有控制流语句，如 if-then-else 和 while 等，都被替换为 assume 语句以及相应的控制流边。其中，assume 语句表达的含义是，在当前的执行路径中，若 assume 的条件被满足，则路径继续执行，否则，路径将阻塞，从而不再继续执行。
下图所示的是上一个例子中的 CMinor 源码的控制流图，其中总计有 7 个块。除了基本块外，_PRECOND#1 是整个控制流图的入口块，同时也用来表达函数的前置条件及秩函数，_POSTCOND#1 是整个控制流图的出口块，同时也用来表达函数的后置条件，_LOOPHEAD#1 是循环头的虚拟基本块。这个例子展示了出于验证需要，我们在常规的控制流图上，额外设计的三类虚拟块。
_PRECOND#1:
requires true
decreases 11
|
|
V
_BASIC#1:
count$1 = 0;
|
|<-------------------
V |
_LOOPHEAD#1: |
loop invariant (count$1 <= 10) |
loop variant (10 - count$1) |
_cond$1 = (count$1 < 10) |
| |
--------------------| |
| V |
_BASIC#3 _BASIC#2: |
assume !_cond$1 assume _cond$1 |
| count$1 = (count$1 + 1) |
| | |
| | |
| |--------------------
------------------->|
|
_BASIC#4:
\result$1 = count$1
|
|
V
_POSTCOND#1:
ensures (\result$1 == 10)
为了方便后续的验证，我们会对程序中的所有变量作 alpha conversion，即对变量重命名，保证所有变量不重名，比如上图中的 $1 即是通过 alpha conversion 所得。对于函数调用、实参、条件表达式、数组长度、数组下标和除数，我们会为其新建临时变量，比如上图中的 _cond$1。我们在数据流图这一层中间表示中不保留结构体的概念，结构体会被以类似于“元组”的形式处理，注意这也会导致函数调用时可能会有多个返回值。
在我们的控制流图中，有四类语句：
- assign：赋值语句，包括对变量的 assign 和对数组中元素的 assign 两种
- assert：程序断言
- assume：守卫（guard）条件，仅会出现在块首
- function call：函数调用，保证所有参数都是变量，并且可能有多个返回值
至此，从验证工具输入的源文件形式 CMinor 语言，到验证算法所依赖的程序控制流图，都已经有了一个大致的介绍。同时，在本次大作业所给出的初始代码中，也已经完成了对于以上内容的实现。同学们需要结合初始代码，以及课程所讲授的内容，完成本次课程大作业。
我们鼓励感兴趣的同学在学有余力的同时，完成一些更加进阶的验证算法。比如：
The Calculus of Computation: Decision Procedures with Applications to Verification