Facebook新推出AL语言,意在简化程序静态分析

  英文原文:Facebook’s New AL Language Aims to Simplify Static Program Analysis

  AL 是一种易用的声明式编程语言,适用于抽象语法树(AST)推理,使开发人员可以扩展 Facebook Infer 静态分析器的功能。

  Infer 采用 OCaml 编写,可标识 Null 指针访问、资源和内存泄漏,以及其它一些C、Java 和 Objective-C 代码中的可检测错误。据 Facebook 介绍,在他们的 iOS 和 Android 移动应用中,80% 的软件缺陷是由 Infer 正确地检测出的。

  AL 易于扩展,这克服了一个局限 Infer 的问题。实现扩展不仅需要具备静态分析的专门技能验,而且需要掌握 Infer 的内部机制。具体而言,AL 意在简化对过程内(Intra-procedural)软件缺陷新类型分析程序(Checker)的定义,即局限于过程代码内的软件缺陷。这类软件缺陷可使用更简单的分析手段检测到,包括借助于程序语法、通用语言习语和自定义约定。举个例子,在 Objective-C 中,为避免存留环路,对象的delegate通常不应做为strong引用。针对需求的分析程序可使用 AL 定义为:

DEFINE-CHECKER STRONG_DELEGATE_WARNING = {     LET name_contains_delegate =              declaration_has_name (REGEXP ("[dD]elegate"));     SET report_when =         WHEN            name_contains_delegate             AND is_strong_property ()         HOLDS-IN-NODE ObjCPropertyDecl;     SET message = "Property or ivar %decl_name% declared strong";     SET suggestion = "In general delegates should be declared weak or assign";   };

  在上面的 AL 代码中,亮点在report_when语句。该语句在ObjCPropertyDecl对象上定义了一个条件,声明为一个strong引用(is_strong_property)。ObjCPropertyDecl对象就是关联到 Objective-C 属性定义的 AST 节点。

  据 Facebook 介绍,通常使用数行 AL 代码就能新定义一个分析程序,并可立即投入使用,无需重新构建 Infer,确保了对新分析程序的快速反馈。AL 还支持定义基于时态逻辑模型的更复杂公式,其中一个 AST 节点可关联到时间上某一点,其所有的后代节点均看作是未来可验证的。例如,为保证程序的正确性,HOLDS-EVENTUALLY所关联的表达式可在未来某个时间点上得以验证。

  AL 是 Infer 的一个组成部分,已开源GitHub 上,适用于C、C++和 Objective-C。

PS:如果您想和业内技术大牛交流的话,请加qq群(527933790)或者关注微信公众 号(AskHarries),谢谢!

转载请注明原文出处:Harries Blog™ » Facebook新推出AL语言,意在简化程序静态分析

赞 (0)

分享到:更多 ()

评论 0

  • 昵称 (必填)
  • 邮箱 (必填)
  • 网址