转载

Facebook开源静态代码分析工具Infer

　　为了减少测试与人工代码检查的工作量，软件供应商一般利用静态代码分析工具来进行程序正确性和稳定性的检查。Monoidics 就是在 2009 年成立、专门设计代码分析工具的公司。该公司所开发的 Infer 静态代码分析工具提供了大规模代码检查的高效解决方案。2013 年 7 月，社交网站巨头 Facebook 收购了 Monoidics 公司，用来提升其大规模代码检查的效率。近日，Facebook 公开宣布开源 Infer 工具，为广大用户提供代码检查方面的便利。

　　静态代码分析是利用词法分析、语法分析、抽象语法树分析以及语义分析等手段，检查代码中潜在错误的过程。该过程与动态分析相对应，不需要执行应用程序，直接通过对代码扫描发现隐含的程序问题，并给出一定的修改建议。传统的静态代码分析是通过人工途径进行的。该方法既需要耗费大量的时间和人力，又很难保证检查结果的可信性。但是，软件的正确性和稳定性又十分重要。一旦发布后才发现 bug，应用程序就需要用户进行主动更新，会严重损害用户的使用体验。因此，自动化的代码检查工具就成为软件开发商所迫切需要的解决方案。

　　然而，自动化的静态代码分析并不容易。针对多达数百万行的代码进行语法、语义等分析，需要考虑到可能多达上千万种的可能性。而且，代码可能被多个开发人员进行高频率修改。以 Facebook 为例，在一天内，一个移动平台的程序代码可能会有超过一千处的修改。为了能够很好的与开发人员进行交互，分析工具就需要在若干分钟内完成大规模代码的分析工作，才能够不影响开发人员下一天的修改工作。

　　为此，Infer 采用了 Separation 逻辑和 bi-abduction 两种数学手段来提高代码分析的效率。Separation 逻辑是 Hoare 逻辑的扩展，主要用来程序中单独小段的分析。在每一步，Separation 逻辑保证了对每一个小段的分析有合理的，而且能够迅速完成。Bi-abduction 则是用来发现每个小段程序的行为属性。通过利用这两个技术，Infer 实现了增量分析，有效减少大规模代码修改过程中的分析时间。而且，Infer 会针对可疑的代码给出高质量的报告，帮助开发人员尽快确定 bug 是否存在或如何进行修改。

　　目前，Facebook 已经利用 Infer 来分析 Android 和 iOS 上的移动应用程序、Facebook Messenger 以及 Instagram 等。每个月，Infer 都会在开发人员正式提交代码之前发现数百个可能的 bug，有效减少了发现并解决 bug 的时间，提高了 Facebook 的产品开发效率。而且，Infer 所汇报的问题中 80% 都被开发人员所接受并进行解决，表现出很好的可信性。当前，Facebook 主要利用 Infer 进行 Android 平台和 iOS 平台 Objective-C 代码的分析。据透露，Infer 能够处理的语言还包括非 Android 平台的C语言和 Java 语言。未来，Facebook 表示会计划扩展 Infer 的能力，使其能够对更多语言进行分析。

正文到此结束