静态分析

什么是静态分析(SA)？好的，静态意味着“非动态”，即不在运行时或在运行期间。静态分析是在软件开发的上下文中在编译时或接近编译时完成的事情。但静态分析只是形式链的一部分，除了列车控制系统等关键系统外，通常不会充分利用它。

完整的形式化链条从形式化规范开始，形式化需求评估是形式化规范的一个重要前提，这一部分涉及的问题是“一些软件要做什么？”

下一步是正式的设计和建模，它处理软件是如何做的问题；通常这首先以正式的方式描述数据和算法，然后验证模型，最后(通常)用作框架并用于代码。这项工作的目标大致相当于Spark对于Ada的意义，即它允许NIM程序被正式验证其正确性。

要回答这个问题，我们必须首先通过拓宽视野，看看“软件开发”意味着什么，来了解上下文和全貌。软件开发可以被描述为一个有点奇怪的过程，它是翻译和理解一种语言，即客户用他们的语言思考，在他们的世界里，可能是天体物理、销售或制造。而且他们经常不提到他们认为是众所周知的东西。这就是“进来”的一面。

另一方面，“外发”的硬件，每个有经验的开发人员都知道，它有自己的危险之处。还有一个复杂的第三部分，因为我们通常建立的软件不是直接在硬件上运行的，而通常是在多个中间层上运行的，例如操作系统和库。

当某个项目非常关键时，我们肯定需要正式的规范，还包括与所需功能本身无关但对我们来说有价值甚至是关键的实用因素。一个明显的例子是代码必须在其上运行的操作系统和体系结构的列表。另一个不太明显的例子是代码将被观察的密切程度(例如日志文件)以及哪些失败响应是可接受的。

但请记住：我们的代码被证明是正确的声明是我们所能做出的最大声明，坦率地说，这是一个非常难以实现和非常罕见的声明，因为我们只控制了许多层中的一个，但需要与它们交互或依赖它们。

静态(程序)分析是我们作为软件开发人员最关心的形式链元素。

通常的“定义”，让我引用维基百科的话说，“静态程序分析是在没有实际执行程序…的情况下执行的计算机软件的分析”。是正确的，但同时也是完全不够的，几乎毫无用处。

为什么？因为我们必须区分编译器编写人员和开发人员，或者换句话说，必须区分“代码本身正确吗？”和“代码在逻辑上是正确的吗？”。从编译器的角度看，下面的代码：

var foo：uint32=0#init var var myArray：array[0..。511，uint32]#我们的数组#.。foo=myArray[100]#将一些元素分配给foo。

是正确的。类型匹配并且索引在边界内。这是编译器所关心的。

将myArray[100]赋给foo是否有意义并不是编译器关心的问题，但是您应该关注它。为什么？因为您希望并需要您的代码做一些有意义的事情以及它需要做什么，或者换句话说，您希望您的代码实现一些算法。

需要静态分析的基本上是检查算法的正确性-但如果实现了这一点，还可以利用这一能力将相当多的编译器工作卸载到静态分析上。

举个例子：Range，什么是Range，什么是Range，基本上等同于写var Month：uint8 invar 0<；Month<；=12，即带不变量的变量声明。

不变量是在与其相关的项(例如变量)的生命周期中必须为真的条件。大多数语言和SA工具都允许不变量在某些明确定义的条件下不成立。

事实上，上面的例子非常接近于现有的带有静态分析的模型检查器的表示法。现在，如果有一个带有月份名称的字符串数组，那么如果按照上面的方式声明月份数，那么按月数访问该数组将始终在限制之内。

更笼统地说：总是尽可能严格地确定您的类型。这条非常简单的规则是实现无错误代码的重要规则。

让我再给您举一个例子：NIM的低位和高位表示法，它提供数组(或序列)的最低和最高有效索引。它也可以被视为不变量，即loop_var.min<；=loop_var<；=loop_var.high。如果我想在C语言中获得相同的结果，我必须为FRAMA-C这样的静态验证器编写一组注释。这两个示例都处理在错误列表中排在前面的问题，这些错误会导致现实世界中的漏洞。

让我们看一个非常简单的函数，它只返回更低的参数值(两个参数的)，即min函数。这很简单，不是吗？嗯，它取决于一些因素，特别是参数类型。

如果我们像通常那样将其声明为func min(a：int，b：int)：int，那么我们可能会遇到问题，例如，在我们寻址的某些体系结构上，假设a是-128，b是0，int是8位，结果会是什么？可能是-128。

我们真正想做的是说结果实际上是提供的两个值中的最小值；但最小的两个数字是一个数学声明。我们的目标是数学性质的，我们真正想要实现的是这样的：“这个函数接受两个数字，并返回值较小的那个-这三个参数和返回值都是自然数集的元素，例如在-128和+127之间”。

函数min(a：int，b：int)：int=Required((int_min<；=a<；int_Max)and(int_min<；=b<；int_Max))确保((int_min<；=result<；int_Max)and((result==a and result<；b)or(result==b and result<；a))。

这看起来可能是一个像样的、合理的规范--但事实并非如此，主要有三个原因：

它过于依赖于具体环境(如字宽)，也就是说，它有时被称为“程序员规范”(与数学规范相反)，换言之，它只重复声明，

声明(代码)可能不够精确，即‘uintX’(例如，‘uint16’)可能会更好，并且会隐式地使规范更短，并且。

规格不是很清楚和完整，如果a==b怎么办？在这种情况下，后置条件将不成立。

函数min(a：int16，b：int16)：int16=确保((result==a and result<；=b)or(result==b and result<；=a))。

前置条件现在由编译器自动创建(基于精确的参数类型)，后置条件现在也更简单，还包括a==b的情况。

“但是我想要一个通用的MIN函数！”你说呢？那就把第一个版本放在上面，改正后置条件，但要三思而后行，看看这是否真的是你想要的。经验法则：把所有东西(比如类型)都钉得越紧越好。

然而，本例的要点有所不同，即后置条件(通常)应该做出与函数所做的事情相关的语句，与实现的算法相关。换句话说：观察者只需查看规范(而忽略函数体)就足以知道函数所做的事情。

说到这里，我将很快转向一个有时会在与SA相关的讨论中出现的问题：“我们为什么需要量化器，特别是EXISTS量化器？”为了回答这个问题，让我快速介绍另一个min函数，该函数适用于列表：

当我们甚至不知道函数将传递多少个值时，我们如何指定后置条件(同样：理想情况下，后置条件也会告诉我们函数做什么)？解决方案：我们提交参数列表中不存在小于Result的元素。

我们也可以使用All Quantor并将索引放入列表中，但这很快就会变得很糟糕。这样更容易，更重要的是，更清楚地声明类似于确保(值中不存在x：x<；result)之类的内容(读起来就像“列表值中没有小于结果的元素”)。

那么，这一切是如何工作的呢？有不同的方式，但至少现在几乎所有的静态分析器都使用Hoare三元组(通常也称为“契约式设计”(Design by Contract，DBC))作为基本框架。Hoare三元组有三个部分(这并不奇怪)，即前置条件、后置条件和可选的不变量。

描述它的一个典型且好的方法是DBC“教科书”解释：前置条件是调用者必须履行的承诺，后置条件是被调用者必须履行的承诺。或者说得非常简单：如果函数/过程是在状态(通常是参数)满足前置条件的情况下调用的，那么一旦完成(在函数退出时)，它肯定会满足后置条件。

小但重要的附注：大多数像样的静态分析器不会将前置条件和后置条件中的状态规范限制为参数和返回值，而是可以处理任何可达状态(例如全局变量)，尽管参数和返回值是经典和最常用的情况。

不幸的是，前置条件(通常写成“Required”)经常被误解和/或仅(Ab)用于简单的参数检查，例如为了避免空指针，这还算可以，但是前置条件可以做更多的事情。

举一个简单的例子，设想一个只处理奇数参数值的函数。素数可能是一个用例(2除外)。想象一下，我们想要一个只处理潜在素数的函数，可能是素数筛子中的提炼阶段。定义和前提条件可能如下所示：

函数某些Sieve(num：uint64)：bool=#素数不是负数，可以变大WHERE前提条件(lastDigit(Num)不在['；0'；，'；5'；]中)和(num>；2)和(num%2==1)#body

再次注意，这是在告诉函数本身、静态验证器和任何调用者，即num参数不能以0或5结尾(质数不能以0或5结尾)，大于2(我们不关心1和2)，是奇数(偶数>；2不能是素数)，并且is<；=MAX_UINT64(通过类型隐式)。

您注意到我使用lastDigit的小把戏了吗？实际上，它不是一个真正的把戏，而是一个方便的工具：lastDigit被称为“幻影函数”，它是一个仅在分析/验证时(但通常不是在运行时)存在的函数，但在其他方面的行为(几乎)就像任何函数一样。完整的事实是，幻影函数(在几乎所有提供它们的分析器中)是一个纯粹的数学(抽象)函数，有时被称为“引理”。有趣的是，幻影函数有两个用途：

做函数所做的事情，即可重用(某些条件元素在代码语料库中出现多次，因此可以方便地将它们放入虚幻函数中)；另外，它们在编译时消失。

后置条件(通常写为“确保”)做的事情与此完全相同，但在函数退出时，它们指定了函数保证保持的与状态相关的条件。

例如，如果我们声明给定函数从不返回负值或大于42的值，我们可以这样表示。

同样，请记住，我们做了一个数学陈述，尽管(通常)是与代码变量相关的。尽管应该注意，一个像样的静态分析器也会利用代码元素，例如变量声明，并将它们包括在其工作中。

让我们快速回到不变量，因为它们在控制机制中扮演着重要角色。静态分析中特别有趣的一点是确保循环正确终止。

在循环控制元素(例如，for(i=0；i<；42；i++)中的变量i)是只读的语言中，问题不那么严重，但是在像C这样的语言中，循环控制元素可以被分配并且可能相当多地“跳来跳去”，这可能会变得非常有问题。

输入循环不变量(其范围通常限于循环)。一个例子是所谓的“减量器”(编者注：不要与摄魂怪：混淆)，这是一种循环不变量，从某个值(例如，控制元素的最大值)开始，在每次循环迭代后倒计时一个。然后，分析器试图证明减量器最终达到零。

请记住，分析器从数学的角度看。IF(42)子句中i是1还是41对分析器来说几乎没有什么不同。它看到的是(假设我是uint16)i的域是0=i<；65536。如果(i<；42)子句中的i是1还是41对分析器来说几乎没有什么不同。它看到的是(假设我是uint16)i的域是0<；=i<；65536。请记住，在IF(i<；42)子句中，i是1还是41对分析器来说几乎没有什么不同。它看到的是(假设我是uint16)i的域是0<；=i<；65536。=i<；42和42<；=i<；65536，表示通往IF和ELSE部分的入口。

现在我们可以理解更多的东西，例如为什么有些分析器(如Spark)特别有用：这是因为它们与“宿主语言”(Ada)紧密交织在一起，因此可以理解编译器提供的大量信息(反之亦然)。基于LLVM的分析器可以发现一种更温和、更有限但有点类似的情况，因为它们也可以访问大量信息，尽管是在中间代码级别。

可能更重要的是，NIM分析不必基于某些中间表示(因此受限于例如LLVM)，但可以实现更类似于SPARK的解决方案。静态分析也将极大地帮助NIM的发展，因为例如我们可以使其成为一条仅充分地指定和成功验证它的规则。NIM分析也将极大地帮助NIM的开发，因为例如我们可以使其成为一条仅充分地指定和成功验证它的规则。NIM分析可能不是基于某种中间表示(因此像LLVM那样受限)，而是可以实现更类似于SPARK的解决方案。静态分析也将极大地帮助NIM的发展，因为例如我们可以使它成为一条仅充分地指定和成功验证它的规则。

求解不再是静态分析的问题，那么什么是静态分析器呢？它是代码和数学/求解之间的“桥梁”；它收集代码中包含的所有零碎信息，以及由“注释”代码的人提供的信息，并以有意义和相关的方式将其提供给求解器。

听起来很简单？嗯，是的，在理论上是的，但在现实生活中似乎是一项复杂而艰难的工作；事实上，只有极少数的语言提供了一些SA功能，而且SA主要只在相当少的几个非常敏感的项目中使用，这一事实有力地表明了SA并不是那么简单。另一个似乎也证实了这一观点的事实是，实际上只有十几到两个实际可用的和使用的静态分析器，对于大多数开发人员(包括经验丰富的开发人员)来说，所有这些都有一定的限制或过于复杂。

静态分析--我指的是与其“宿主语言”紧密耦合的SA--提供两大功能，即：

到目前为止，唯一已知的通过证明代码是无错误的来实现对代码的合理信任的方法，以及

对于普通开发人员来说，这是一种实际可用的、甚至相当方便的方式来实现这种信心。

需要注意的是：静态分析器不能创造奇迹；它在很大程度上只能证明您提供给它的东西是正确的。如果您不提供要验证的语句/条件，您将不会从中获得太多信息。

你可能听说过完全经过验证的seL4内核。嗯，他们确实采取了艰难的路线(当时他们不得不这样做)，他们花了大约十年的时间才完成了非常熟练的专家的工作。与Ada/Spark相比，(从几年前)可能还是一种编程语言的例子，它(实际上是相当紧密耦合的)静态分析器。我仍然记得我第一次使用它的经历。几乎是梦想成真，不仅因为它是一个没有博士学位就可以实际使用的东西，而且因为它的效率很高。我仍然记得我第一次使用它的经历。它几乎实现了一个梦想，不仅因为它是一个人不需要博士学位就可以实际使用的东西，还因为它的效率。我们通常不能在“注释”上投入比在编写代码上多得多的时间。

如果您应该从本文中带走一件事，那就是：用它的警告让您感到不安的编译器是您的朋友。SA是它的某种扩展版本。SA是您的朋友，而且是一个强大的朋友！做出您的选择：您可以让静态分析器向您指出问题所在，也可以让您的客户指出它们(并咒骂您)。

您应该注意的另一点是，SA是(基于)您正在编码的另一种规范。它不是缺点，而是一个优点，因为它不完全像您的代码/您的编程语言。它允许您用有点类似的符号来表示您的算法，但需要检查算法和程序实现。

事实上，我建议更进一步，将规范视为重要的部分，并将编码视为一些“次要工作”。编程“只是”实现“如何？”的一部分。事实上，在高度敏感的环境中，首先适当地(正式地)指定要做什么、必须满足什么条件以及某个模块或过程前后的状态是什么，而实际实现模块和/或过程只是倒数第二步(最后一步是验证和测试)，而实际实现模块和/或过程只是倒数第二步(最后一步是验证和测试)，而实际实现模块和/或过程只是倒数第二步(最后一步是验证和测试)。

还要注意这样做的一个特别有用和美丽的副作用：如果某个过程或模块需要更改，比如由于某些管理更改，只要规范(“注释”)足够完整和严密，则该更改不会对整个系统造成损害。

我希望将来的某个NIM版本X(具有不完整但合理的SA级别)将是一个可与Ada/Spark相媲美的飞跃，甚至可能是一个更重大的飞跃，因为NIM是一种比Ad.更常用(或很快将会)且更容易使用的语言.一旦有一个带a-d：Verify开关的NIM版本可用，我会高兴得跳起舞来.