你选择富于表达的还是纵容的编程语言？

你选择富于表达的还是纵容的编程语言？
——代码可分析的难易程度取决于你使用的编程语言

作者：Yannick Moy，2010年4月7日
原文：http://www.embedded.com/design/224200704
译者：logiciel，2010年4月17日

　　用C和Java的成熟的缺陷查找工具（包括诸如CoverityPrevent、GrammatechCodeSonar和FortifySCA）进行静态分析正在成为主流。由于这些工具的内在特性，它们把“噪音”（错误警告）限制到最低限度。但是，通过仔细挑选这些缺陷查找工具报告有问题的案例，它们大都不能确定程序的总体正确性。
　　为看到这一点，一般只要降低不报告问题的门限，立即返回一个极长的可能出现的问题的清单，这仅占所有潜在的问题的一小部分。在这里所谓“问题”是指任何软件错误，无论是在运行时可能发现（导致异常错误）的错误或程序员的意图与所获得的行为不匹配的错误。
　　作为一名开发人员和这些工具的用户，我多次尝试回答一个大多数用户都会问的经常性问题：如何才能使我的程序可分析？说实话，除了对编程语言避免使用某些功能和优先使用某些特性的少数技巧之外，通常不是可以做很多事情，因为有许多决定超出了程序员的控制，而是取决于编程语言本身的特点。
　　因此，真正的问题是：我应该选择哪种编程语言使我的程序可分析？这个问题可以重述为：什么样的编程语言给我“自由（for　free）”？这里自由的意思是我能得到来自源代码的可用信息，而没有进一步的分析信息，这些分析信息虽然没有严格要求表达功能的行为，但捕捉了程序员的意图的一部分。由于软件分析一直缺乏关于程序员意图的信息，来自一种“自由”的编程语言的信息是提供给分析器的最宝贵资产。按照这个准则，C的排名远低于Java，而JAVA远低于Ada。
　　当然，所有的语言工具努力恢复缺失的信息，但由于缺失的信息越积越高，工具难以恢复高层次的信息。例如，汇编语言程序分析工具基本上只限于恢复声明的类型和控制流，而C程序分析工具，更容易恢复上层信息，如类型安全和存储安全方面的特性。同样，Java程序分析工具除了可以恢复与C程序类似的那些特性外，通常还可以推断整数范围和指针是否为空。恢复“功能合约”是软件分析的最终目标，Ada程序分析工具在实现这个目标上是最佳的，因为它提供了大量的自由信息。
　　一个“功能合约”由一个先决条件和一个后置条件组成，一个函数的调用者应该在调用函数之前满足先决条件，该函数在返回之前应该满足后置条件。在一些先驱语言（特别是Eiffel）首先出现了用户定义的合约，现在各种广泛认可的环境中提供这种合约，如.NET平台（代码合约）及Ada语言的GNATGCC编译器。许多分析器在内部根据生成的合约，也称为功能概要，进行分析计算。
　　上面我说合约是最终目标，因为完整的合约允许独立地分析每一个函数,就像函数签名允许单独编译。但是，只有一个编程语言，SPARK，已经要求程序员提供合约。因此，在一般情况下,直到使用分析器时才生成合约。
　　现在一个编程语言的两个方面定义它能提供多少“自由”信息：表达性(expressiveness)和纵容性(permissiveness)。通常，这两个方面是混淆的，因为它们都似乎是指用许多不同的方式表达程序员意图的能力。但考虑到分析，他们有相当不同的含义，一个支持分析，而另一个损害分析。
　　一种语言是表达的，就是它可以让程序员轻松地转达他/她的意图,并尽早发现错误。相比于汇编语言，C允许约束变量持有特定类型的值，因此就这而言它的表达性较强。相比于C，Java允许测试一个值是否在一个数组a的长度a.length之内，因此就这而言它的表达性还要强。相比于Java，Ada语言允许约束一个标量变量持有特定范围内的值，因此就这而言它表达性最强。
一种语言是纵容的，就是它允许干扰程序的可靠性和可读性的结构。可通过强化的语义和限制来控制这种放任的程度。相比于汇编语言，C提供结构化的控制流语句（如-then-else的，循环），它防止任意地跳入或跳出函数，因此就这而言它是比较不纵容的。相比于C，Java提供了指针默认初始化为空，并且防止指针和整数之间的转换，因此就这而言它是更加不纵容的。相比于Java，Ada语言提供了子程序参数的模式（in/out/in-out），并在计算中检测是否出现整数溢出，因此就这而言它是最不纵容的。

用C/Java/Ada写的一个简单例子
　　为了观察一个表达性较强和纵容性较低的语言如何帮助分析一个软件片断，考虑一个很简单的例子，其中一个函数分配一个有N个结构的数组，其中N是在某个配置中定义的可用处理器的数量。

表1是用C，Java，Ada直接实现此功能的程序，其中没有详细的处理器结构类型和配置。



　　尽管这些实现在使用适当时是正确的，但由于调用者未能建立适当的环境，它们在执行时仍然可能出错。

　　在每种情况下，字段num_proc可能未初始化，这可能取一个任意大小的值。在C和Java程序中，conf可能是一个空指针，在这种情况下访问其字段num_proc将失败。在C中，通常报告一个段故障。在Java中，抛出一个NullPointerException异常。在Ada中，在源文本这一层次不把参数作为引用来传递，而编译器为了效率可以决定按引用传递，所以不会出现一个空的引用。
　　在C中，以字节为单位计算分配的大小可能溢出，结果是分配了一个非常小的数组，而不是一个非常大的。这是一个普遍的安全攻击的来源，数组访问可能超出数组的范围。在Java和Ada，运行时将确保有没有溢出。
　　在C中，conf可能是一个无效的指针，或者是因为它从来没有初始化，或者是因为它指向的位置被释放，或者超出范围。这通常会导致难以诊断的取决于编译器和程序的任意行为。在Java和Ada，语言规则确保指针默认初始化为null。
　　总结以上分析，C程序可能有五个错误，Java程序可能有三个错误，Ada程序可能有两个错误。这一切只是涉及一个非常简单的函数！现在对有复杂的交互操作的大型函数重复上述工作，你将发现C和Java程序比同等的Ada程序要抵制分析。
现在，从调用者的角度分析这些程序还提供什么可以自由分析？在C程序中，alloc_processors的结果类型是一个指针，它可能会或可能不会被初始化，可能为空或不为空，这可能是也可能不是指向一些有效的内存。在Java程序中，AllocProcessors的结果类型是一个指针，可能或可能不为空。在Ada程序中，Alloc_Processors的结果类型是一个非空指针，它可能只被初始化为一些非空的有效值。还有，Ada程序中参数Conf的in模式告诉我们，无论怎样传递它，它不会被Alloc_Processors的调用者修改。
2009年我在使用微软内部称为PREfix的分析器来查找一个大的微软的基础代码中的涉及安全的整数溢出漏洞时，多次遇到与这段代码对应的实际案例。由于基础代码用C编写，我通常很难依靠变量命名来判断工具检测的可能的整数溢出是否为安全漏洞：虽然num_proc不太可能非常大或被攻击者所控制，num_connections可以合法地被攻击者所控制。遗憾的是，依赖命名规则来检测安全漏洞是许多如C语言情况下的一个最佳手段。

整数和指针
前面的例子使用了编程语言中的两个关键类型：整数和指针。这并不奇怪，一种编程语言的表达性或纵容性在很大程度上与整数和指针的处理方式有关。
首先考虑的整数。在大多数编程语言（C、C++、Java、C＃）中，语言定义的整型与机器的整数直接映射。在移位与除法同义，或者负数当作正数时，这成为棘手的位向量操作的原因之一。在其他语言中，整数具有数学的强大力量，没有任何敏感的数量范围，甚至不是宇宙中原子的数量。
机器视角与数学视角都导致难以分析软件。程序中的整数是数量，既不是位向量也不是抽象的数字。为了分析，应适当限定数量，使之对应那些整数类型的有效范围，并让用户决定他们认为合适的界限。
这正是Ada的情况。Ada是表达的，它让程序员定义整数类型和约束。Ada不是纵容的，它要求在表达式中使用兼容的类型，或者使用适当的类型转换。
现在考虑指针。大多数编程语言只有一种通用的指针，这导致众所周知的编程危害。在C中，一个指针可指向栈或堆的位置、单个引用或一个数组，甚至一个数组的一部分。在Java中，一个引用可指向有非常不同生存周期的对象，它可以为null。
Ada仔细地区分了引用、数组、访问类型和地址等概念，并可以根据其使用进一步细分。当一个引用的模式为in，相应的过程仅能读取它，模式为out时相应的程序只能对它写，模式为in-out时相应的程序可以对它读和写。一个访问类型定义了它的作用范围内的存储池，使其他不同类型的指针不能使用别名，即使它们指向相同的基础类型。一个访问类型可能会被标记为非空，在这种情况下这种类型的值不可以为null。
我可以说出很多Ada对待整数和指针的精细程度，这使得它具有较强的表达力和较低的纵容度。但上面所述的应该够清楚了。

功能合约
SPARK是比Ada表达力更强和纵容度更低的一种语言。毫不奇怪，它的一部分建立在Ada之上。SPARK包括一个Ada子集，具有较强的语义和限制，用Ada 注释风格描述合约，这使得常规的Ada编译器可以编译SPARK的代码。Ada旨在促进程序分析，而SPARK旨在促进验证。
如表2中的例子所示，SPARK合约允许表达数据流（全局注释表达全局变量的读取和写入）、信息流（派生注释）、先决条件（预注释）和后置条件（后注释）。

　　在每种情况下，可能没有足够的内存来分配。在C程序中，malloc返回0，函数退出。在Java程序中，抛出一个OutOfMemoryError异常。在Ada程序中，引发异常Storage_Error。请注意，Ada程序中由Proc_Numbe类型限定了处理器的最大数量（64），而在C和Java程序中num_proc类型是一个预定义的整数类型，它的最大值可能是巨大的。



该合约规定，过程Linear_Search读取和写入全局变量Counter，每个输出（输出参数和Counter）的值决于其所有输入（输入参数和Counter）的值，只当Counter不是最大整数值时才可调用该程序，当所寻找的Value确实是在输入Table中下标为输出Index的位置时，该过程将返回Found为真，而Counter已在程序进入时的初值（记为Counter〜）基础上增加了1。

分析器允许静态地完全证明过程体遵守了合约，并且在执行过程中没有运行时错误。例如，SPARK的语义和限制确保分析器捕获所有对未初始化值的读取，并且不允许动态分配，因此在SPARK中不可能出现 Ada程序Alloc_Processors的错误。
由于这些限制，SPARK可能不适合所有场合。不过，对于其他编程语言，对功能合约的依赖可能是有价值的：
在你不能访问源代码时，合约使得分析一个库或一个使用库的程序成为可能；
l 合约允许把分析分成许多独立的小的分析，这样运行总共的花费将便宜得多，且不提在多核多处理器上并行运行的可能性；
l 由于合约允许验证独立功能，可以使用更强大的技术，例如现代SMT-证明器执行的基于SAT的勘探。
事实上，各种分析器提出自己的C和Java语言扩展来弥补这些语言的缺失，例如， Findbugs中的Java指针的非空注释，Splint中的C参数的输入/输出模式，PREfix中的C数组参数的尺寸标注，等等。这些语言扩展以用户友好的方式增加有限的功能合约。
由于SPARK的示范，在不久的将来，以合约为基础的分析将是使软件分析象编译那样普遍的最直接的方法。

提高信心
运用软件的静态分析是改善软件的正确性的一个肯定的方式，因为我们确实发现并纠正前进的道路上的错误。当所有发现的错误已经纠正，工具没有返回更多的（真）警告，这还有待观察是否能够提高我们关于该软件是正确的信心。
相对于进行分析程序的工具，答案更多地取决选择的编程语言。事实上，编程语言在方便分析的功能方面相差很大。Ada和SPARK比C和Java具有较强的表达力和较低的纵容度，因此大大方便分析。
根据Andy German在2003年做的关于代码规模在3000行到30万行的军用系统的一份研究报告，各种编程语言使编程人员每千行产生错误的数量是，SPARK平均是4，Ada是4.8到50，C是12.5到500（原文如此）[1]。还可以进一步阅读John Barnes的Ada2005介绍，其中深入阐述为什么表达力更强和纵容度更低的编程语言带来更好的软件[2]。

[1]. German, Andy. "Software Static Code Analysis Lessons Learned," CrossTalk, November 2003.

[2]. Barnes, John. "Safe and Secure Software," 2008, www.adacore.com/2008/04/08/gem-30/.