使用Infer静态分析器查找程序间的bug

静态分析器在程序运行之前捕获错误的能力正在稳步提高。在Facebook使用Infer静态分析器（https://fbinfer.com/）的过程中，我们经常被问及Infer与其他开源分析工具（如Findbugs、错误倾向和Clang静态分析器）之间的差异。一个主要区别是程序间错误，或涉及多个程序之间交互的错误。

我们将看看Infer在Java和C中发现的两个程序间错误示例——一个来自开源DuckDuckGo Android应用程序，另一个来自OpenSSL C代码。上述工具无法发现这些错误，这些工具仅执行程序内分析，或者在Clang静态分析器的情况下，仅执行文件内分析（可能是程序间分析，但仅限于一个翻译单元中的程序，一个包含在内的文件）。

程序间错误是重要的，因为它们构成了Infer发现的几种类型的错误中的大多数。Facebook开发人员已经修复了数千个这样的bug，这表明静态分析发现它们可能会产生巨大影响；我们包括一些来自Infer在Facebook部署的程序间错误频率数据。正如我们所发现的，过程间分析可以部署到大型且快速变化的代码库中，这些代码库由数百万行代码组成，每天要进行数千次修改。

DuckDuckGo

面向隐私的互联网搜索引擎DuckDuckGo的Android应用程序代码在GitHub上提供。在Infer报告后，DuckDuckGo开发人员修复了应用程序早期版本的以下问题：

src/com/duckduckgo/mobile/android/activity/DuckDuckGo.java:867: error: NULL_DEREFERENCE
object `feedObject` last assigned on line 866 could be null and is dereferenced by call to `feedItemSelected(...)` at line 867.
    
864.
865. public void feedItemSelected(String feedId) {
866. FeedObject feedObject = DDGApplication.getDB().selectFeedById(feedId);
867. feedItemSelected(feedObject);

与此报告一起，Infer生成了一个由18个步骤组成的过程间错误跟踪，这些步骤通过过程getDB（）、selectFeedById（feedId）和feedItemSelected（feedObject）。有两个不同的feedItemSelected（）方法，一个接受FeedObject作为参数，另一个接受String。下面是第866行selectFeedById（feedId）调用访问的代码：

src/com/duckduckgo/mobile/android/db/DdgDB.java:483: start of procedure selectFeedById(...)
    
482.
483. public FeedObject selectFeedById(String id){
484. FeedObject out = null;
485. Cursor c = null;
486. try {
487.   c = this.db.query(FEED_TABLE, null, "_id=?", new String[]{id}, null, null, null);
488.   if (c.moveToFirst()) {
489.    out = getFeedObject(c);
490.   }
491.  } finally {
492.      if(c!=null) {
493.            c.close();
494.      }
495.  }
496.  return out;
497. }

selectFeedById（）有可能返回null，即当db.query（）在第487行返回的游标c为空游标时。第488行对c.moveToFirst（）的调用将返回false。

当分析feedItemSelected（）中标记了空问题的原始代码时，Infer需要在第866行意识到空是可能的。错误实际上在第867行报告，这是另一个方法调用，在本例中涉及以下方法：

src/com/duckduckgo/mobile/android/activity/DuckDuckGo.java:842: start of procedure feedItemSelected(...)
    
841.
842.  public void feedItemSelected(FeedObject feedObject) {
843. // keep a reference, so that we can reuse details while saving
844.    DDGControlVar.currentFeedObject = feedObject;
845.    DDGControlVar.mDuckDuckGoContainer.sessionType = SESSIONTYPE.SESSION_FEED;
846.
847     String url = feedObject.getUrl();

这里我们看到feedObject在第847行被取消引用。因此，如果feedObject为空，我们将有一个空指针取消引用。

我们有一个过程间错误，其中null的源在一个方法中，null的汇在第二个过程中，源和汇过程从第三个过程调用。我们需要程序间推理来发现这个问题，因为纯粹的程序内工具不会发现这个错误。

如果在代码中添加了关于可空性和不可空性的注释，Findbugs、易出错工具和其他工具可以发现此错误。然而，在编写的代码中发现bug需要过程间推理。

理论：规范和总结

Infer使用一种称为合成、基于摘要的分析的技术发现了DuckDuckGo问题。Infer不是每次遇到一个方法时都重新评估它，而是参考该方法可能做什么的摘要或近似值。组合分析器计算摘要而不查看方法的所有调用位置；Infer尝试在一次传递过程中计算尽可能的摘要。

Infer将其摘要表示为程序逻辑中的规范。更详细地说，规范是先决条件和后决条件的一对（前、后）（熟悉于霍尔逻辑或其更现代的化身，分离逻辑）。（pre，post）对意味着如果逻辑属性pre在执行过程之前保持，post将在执行过程之后保持。有时会使用几个帖子来表示帖子的分离（“或”）。摘要是前/后对的集合，其中一个前财产需要在调用位置匹配才能继续推理。

对于selectFeedById(String id)方法，Infer计算

PRE: this.db |→ - (db is non-null and points to a valid object)
    
POST1: return == null (we are returning a null feed object)
POST2: return |→ - (we are returning a valid, non-null feed object)

也就是说，在摘要中有一个单独的前/后对，其中后是析取POST1或POST2。原始过程feedItemSelected（StringfeedId）中的符号执行将在第866行考虑feedObject的两种情况：根据两个后置条件，null和非null情况。然后，对于第867行的下一条语句，我们必须考虑调用feedItemSelected（feedObject）的空参数。再次，我们通过查询feedItemSelected的计算前/后规范来处理这个问题。摘要有五个前/后规范，但它们都包含

PRE: feedObject |→ - (feedObject is a valid, non-null object)

Infer选择此作为前提条件，因为我们需要feedObject为非空；否则，将发生错误（NullPointerException）。现在，当符号执行尝试feedItemSelected（feedObject）但feedObject==null时，我们无法满足前提条件。正是在这一点上，我们试图构建一个逻辑证明，证明没有运行时错误，并报告错误。

重要的一点是关于代码的推理

864.
865.  public void feedItemSelected(String feedId) {
866. FeedObject feedObject = DDGApplication.getDB().selectFeedById(feedId);
867. feedItemSelected(feedObject)

可以只使用它调用的程序的摘要来完成，而不需要（再次）深入研究它们的身体。对于Infer的大规模操作，过程抽象原则的应用是至关重要的，因为它能够独立于调用站点构建摘要。

Infer的总结概念还有其他细微差别，它比前面提到的前/后规范更详细。为了让Infer报告错误的跟踪，除了前/后规范之外，它还记得在摘要中显示代码路径的跟踪信息。而且，前/后规范本身比上述规范更复杂，为了说明的目的，这些规范被手动简化。您可以在这里找到Infer为这些程序计算的详细规格。

OpenSSL

我们已经展示了基于摘要的组合程序分析如何在Java中有效地发现大规模的过程间错误。它也适用于C语言。例如，2014年，我们向GitHub提交了在OpenSSL中发现的15个空引用和内存泄漏Infer，该项目的核心开发人员之一解决了这一问题。一些空解引用相当复杂，这说明了我们想对误报率提出的一点，即在任何程序运行中都不会发生的错误。

以下是Infer的报告之一：

apps/ca.c:2780: error: NULL_DEREFERENCE
pointer `revtm` last assigned on line 2778 could be null and is dereferenced at line 2780, column 6
2778. revtm = X509_gmtime_adj(NULL, 0);
2779.
2780.  i = revtm→length + 1;

问题是过程X509_gmtime_adj（）在某些情况下可能返回null。总体而言，Infer发现的错误跟踪有61个步骤。此外，null的源（对X509_gmtime_adj的调用）在返回null之前在其子空间中有36个步骤；跟踪深入五个过程，最终在过程ASN1_TIME_adj（）的调用深度4处从文件crypto/ASN1/a_TIME.c返回null。

crypto/asn1/a_time.c:113:6: Condition is true
111.
112. ts=OPENSSL_gmtime(&t,&data);
113. if (ts == NULL)
114.   {
115.      ASN1err(ASN1_F_ASN1_TIME_ADJ, ASN1_R_ERROR_GETTING_TIME);
116.       return NULL;
117. }

X509_gmtime_adj（NULL，0）返回NULL的条件有些复杂，Infer无法确定它们肯定会在程序运行中发生。Infer不会在每次报告潜在错误时构造一个一直返回main（）的跟踪。相反，在试图构建逻辑证明的过程中，Infer有时会报告构建此类证明时遇到的困难。

在本例中，OpenSSL开发人员解决了这个问题。在代码库的其他地方，Infer报告被阻止，因为OPENSSL_gmtime（）附带了一个空检查，这进一步证实了这个问题值得提出。

我们还在OpenSSL上运行Clang静态分析器。它能够执行文件内分析，其中的一个子集可以是程序间的，但据我们所知，不能在文件之间进行。此示例需要文件间分析；事实上，当我们在OpenSSL-1.0h上运行CSA时，它没有发现错误。值得注意的是，CSA报告的错误集与Infer不同，因此在C代码上运行这两个分析器是有意义的，同样，为Java分析运行Findbugs和Error。

一个有趣的问题是，这份OpenSSL报告是假阳性还是真错误。即使过了几个小时，我们仍然不确定。在大规模使用静态分析时，这种情况并不罕见：对于大型代码，有时工具和人员都不确定是否会发生错误。这就是为什么在部署静态分析后，我们对假阳性率的概念的重视程度不如学习其原理时的重视程度。由于代码基数庞大且不断变化，对于所有实际目的来说，这个速率都是无法测量的。一个更为人所知的概念是修复率，它能更好地说明分析给程序员带来的价值：由于开发人员的代码更改而消除的分析器问题的比例。

速度和渐进主义

为了说明Infer在OpenSSL（一个由超过300000行代码和700个文件组成的代码库）上的性能，我们分析了代码，对其进行了修改以修复上述错误，然后以增量方式重新分析了它。

$ # compile to infer's intermediate language
$ time infer capture -- make
[...]
real 5m0.545s
user 4m10.563s
sys 1m3.104s
    
$ # analyze the entire OpenSSL project, using one CPU only
$ time infer -j 1 analyze
[...]
real 22m20.320s
user 20m24.831s
sys 1m31.722s

$ # fix the bug
$ vi apps/ca.c
[...]
    
$ # run infer incrementally, using one CPU only
$ time infer -j 1 run -reactive -- make 
[...]
real 0m41.296s
user 0m36.920s
sys 0m2.379s

Infer在代码更改上的运行速度比在整个项目上快得多。反应模式仅对更改的文件执行捕获和分析的翻译工作。OpenSSL开发人员给出的apps/ca.c中的代码修复涉及插入一个简单的空检查。

2778 revtm = X509_gmtime_adj(NULL, 0);
2779
2780 if (!revtm)
2781 return NULL;
2782
2783 i = revtm→length + 1;

这种更快的增量分析有助于Infer在Facebook的部署模型，它与代码审查系统集成在一起；如果在出现代码更改时必须对整个程序进行操作，那么即使是线性时间分析也会太慢。

程序间修复的频率

人们有时会问，程序间分析是否会捕捉到许多本地分析无法捕捉到的错误，以及我们是否需要程序间分析。毕竟，本地工具会跟踪我们在Infer中讨论的一些相同类别的错误（例如，空引用）。

我们查看了Facebook开发人员修复的100份最新Infer报告，分为几个错误类别。由于文件间错误必然被分类为程序间错误，请注意，程序间错误是下表中最右两列中的错误。

过程内意味着错误发生在单个函数的范围内。文件内但过程间意味着错误跟踪经过多个过程或函数，涉及多个过程，但支持跟踪和推理仅限于单个文件。Inter-file是一个跨多个文件的程序间错误。

我们发现，Java中修复的大多数空引用都是过程间的。在Objective-C中，更大的比例是程序内的。产生差异的部分原因是，我们已经实现了许多过程内检查，这些检查基于Facebook开发人员的输入来搜索ObjC特定的代码模式。程序间错误仍然占不可忽略的比例。

线程安全性是对用@ThreadSafe注释的Java类中方法之间的数据竞争的检查。同样，大多数是程序间的，甚至是文件间的。数据竞赛是对字段的访问或对容器的调用，这些字段和容器通常位于与注释的@ThreadSafe不同的类中。出于本表的目的，当我们有一个涉及两个过程的读/写竞争，但访问在过程本身内时，我们认为这是一个过程内竞争。发现它需要两个程序内推理，关于两个程序。

Allocates Memory是一种检查是否可以从注释为@NoAllocation的过程访问分配。

线程安全性和分配内存基于专门的过程间分析，不同于DuckDuckGo和OpenSSL的示例bug中提到的基于分离逻辑的分析。线程安全使用摘要的概念来记录访问和锁定信息。Allocates Memory是注释可达性分析器的一部分，其摘要存储跟踪信息。这两个分析器使用一个框架Infer.AI来编写Infer中的复合静态分析器。

Bad Pointer Comparison是Objective-C的一种lint检查，用于识别在比较中何时将NSNumber*等装箱基元类型强制为布尔值。它是用我们的AST语言AL编写的。我们将其作为不需要程序间推理的有用检查的一个例子，用于平衡。

结论

随着静态分析器越来越常见，它们通常用于执行简单的过程本地（过程内）检查。这些分析，例如开源工具Findbugs、Error-prone、ClangStaticAnalyzer和AndroidLint，部署相对广泛，并提供了积极的价值。例如，一个谷歌静态分析团队报告称，它广泛使用内部程序内检查，但避免大规模的程序间分析。Facebook在内部部署了几个linting和程序内分析解决方案，Infer在AL语言中包含了自己的解决方案。

相比之下，程序间分析似乎不太常用，但也有其他关键发展。两个重要的部署是Microsoft的前缀和静态驱动程序验证程序；静态驱动验证程序具有有限的扩展能力，而Prefix以自底向上的方式工作，就像早期版本的Infer一样，并且可以扩展到大型代码库。Coverity的专有静态分析器还支持程序间分析，使用一些与Infer相似的技术和其他不同的技术。这些努力提供了背景，但我们还没有进行详细的比较。一项对几种高级静态分析工具的独立研究发现，它们捕捉到了不同的错误集，这表明没有一种最好的分析器可以取代所有其他分析器。

因为Infer是合成的，这意味着过程的摘要是独立于调用上下文生成的，所以它可以扩展到大型代码库，并在频繁的代码修改上逐步工作。一般来说，我们觉得除了linting之外，高级静态分析技术还有很多潜力，比如检查程序间和其他更深层错误的技术。特别是，无论是在学术界还是在工业界，组合程序分析都将从进一步发展中受益。

原文地址：https://engineering.fb.com/2017/09/06/android/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer/