写点什么

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

2015 年 6 月 19 日

为了减少测试与人工代码检查的工作量,软件供应商一般利用静态代码分析工具来进行程序正确性和稳定性的检查。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 的能力,使其能够对更多语言进行分析。


感谢徐川对本文的审校。

给InfoQ 中文站投稿或者参与内容翻译工作,请邮件至 editors@cn.infoq.com 。也欢迎大家通过新浪微博( @InfoQ @丁晓昀),微信(微信号: InfoQChina )关注我们,并与我们的编辑和其他读者朋友交流(欢迎加入 InfoQ 读者交流群InfoQ 好读者)。

2015 年 6 月 19 日 06:486610
用户头像

发布了 268 篇内容, 共 102.8 次阅读, 收获喜欢 19 次。

关注

评论

发布
暂无评论
发现更多内容

【架构师训练营 1 期】第十周学习总结

诺乐

Week_10 总结

golangboy

极客大学架构师训练营

10 模块分解课后练习

ABS

第十周学习总结

solike

架构师训练营第六周作业

xiaomao

week6 技术选型(二) 作业和学习总结

杨斌

目标检测之WBF(Weighted Boxes Fusion)

Dreamer

目标检测

第 6 周作业

Steven

极客大学架构师训练营

git 在未保存,add,commit,push下撤销的方法?收藏后再也不用找了

小松漫步

学习总结之分布式数据库

幸福小子

架构师训练营第十周学习笔记

一马行千里

学习 极客大学架构师训练营

架构师训练营第十一周作业

Geek_4c1353

极客大学架构师训练营

架构师训练营第2期 第六周课后练习

月下独酌

极客大学架构师训练营

架构师训练营 - week10 - 作业

lucian

极客大学架构师训练营

第10周作业

paul

腾讯云轻量应用服务器 SSH 配置

邵俊达

SSH 轻服务器

week6-命题作业

未来已来

架构师训练营第 10 周课后练习

叶纪想

极客大学架构师训练营

模块分解

wing

极客大学架构师训练营

架构师训练营第十周命题作业

一马行千里

极客大学架构师训练营 命题作业

架构第十周作业

Geek_Gu

极客大学架构师训练营

第十周 模块分解总结

钟杰

极客大学架构师训练营

极客时间架构 1 期:第 10 周 模块分解 - 学习总结

Null

极客时间架构 1 期:第 10 周 模块分解 - 命题作业

Null

与前端训练营的日子 --Week05

SamGo

学习

9 性能优化(三)课后练习

ABS

架构第十周总结

Geek_Gu

极客大学架构师训练营

第十周作业

solike

Effective go 笔记-01

邵俊达

golang Effective-go

架构师训练营2期 第六周总结

月下独酌

极客大学架构师训练营

CAP原理

幸福小子

分布式 CAP原理

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