BT

如何利用碎片时间提升技术认知与能力? 点击获取答案

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

| 作者 张天雷 关注 4 他的粉丝 发布于 2015年6月20日. 估计阅读时间: 4 分钟 | QCon上海2018 关注大数据平台技术选型、搭建、系统迁移和优化的经验。

为了减少测试与人工代码检查的工作量,软件供应商一般利用静态代码分析工具来进行程序正确性和稳定性的检查。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好读者)。

评价本文

专业度
风格

您好,朋友!

您需要 注册一个InfoQ账号 或者 才能进行评论。在您完成注册后还需要进行一些设置。

获得来自InfoQ的更多体验。

告诉我们您的想法

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我
社区评论

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

允许的HTML标签: a,b,br,blockquote,i,li,pre,u,ul,p

当有人回复此评论时请E-mail通知我

讨论

登陆InfoQ,与你最关心的话题互动。


找回密码....

Follow

关注你最喜爱的话题和作者

快速浏览网站内你所感兴趣话题的精选内容。

Like

内容自由定制

选择想要阅读的主题和喜爱的作者定制自己的新闻源。

Notifications

获取更新

设置通知机制以获取内容更新对您而言是否重要

BT