Facebook 开源了适用于分析 C、Java 和 Objective-C 代码的静态分析工具 Infer 。
Infer 是 Facebook 的开发团队在代码提交内部评审时,用来执行增量分析的一款静态分析工具,在代码提交到代码库或者部署到用户的设备之前找出 bug。由 OCaml 语言编写的 Infer 目前能检测出空指针访问、资源泄露以及内存泄露,可对 C、Java 或 Objective-C 代码进行检测。Facebook 使用 Infer 自动验证 iOS 和安卓上的移动应用的代码,bug 报告的正确率达 80%。
Infer 通过捕获编译命令,把要被编译的文件转换为可用于分析潜在错误的中间语言格式。整个过程是增量进行的,意味着通常只有那些有修改过并提交编译的文件才会被 Infer 分析。Infer 还集成了大量的构建或编译工具,包括 Gradle、Maven、Buck、Xcodebuild、clang、make 和 javac。
有一些类型的错误能用 Infer 检测出,关于它们的更多细节内容可见此页。Infer 未来有望能加强对数组越界错误、转换异常和污染数据泄露的检测, Facebook 目前已开始着手开发这些功能,但暂不可用。
在被问及能否增强 Infer 的功能,以使其可找出其他错误,并能应用于其他语言编写的代码时,Facebook 的发言人答复 InfoQ:“我们认为,关于 Infer,这才只是一个开始,公司未来将持续致力于释放更多的价值给程序员”,并表示 Facebook 希望能与社区一起合作,来进一步完善 Infer:
Infer 做的不错,不过仍有许多跨工程组织的开放问题有待解决。一旦 Facebook 开源了 Infer,就可以同许多工程组织、研究组织和学术组织进行合作,通过社区的努力,有可能最终 Infer 会增加一些新特性,能用来发现新类型的 bug,甚至可以应用到新的语言上。
据 Facebook 透露,Infer 根植于两大基本理论之上,其一是霍尔逻辑,一种用于推理计算机程序正确性的形式系统,另一个是抽象解释,该理论用于测度程序语义的逼近结果,此外还涉及其它一些研究成果,例如 Separation Logic 和 Bi-abduction 。
Infer 的源代码可在GitHub 上获取。
查看英文原文: Facebook Open Sources Infer, a Static Analysis Tool
感谢邵思华对本文的审校。
给InfoQ 中文站投稿或者参与内容翻译工作,请邮件至 editors@cn.infoq.com 。也欢迎大家通过新浪微博( @InfoQ , @丁晓昀),微信(微信号: InfoQChina )关注我们,并与我们的编辑和其他读者朋友交流(欢迎加入 InfoQ 读者交流群)。
评论