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

简介:

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。

本文转自d1net(转载)

相关文章
|
机器学习/深度学习 人工智能 语音技术
Facebook创造了两个会交流的神经网络来描述颜色,竟和人类语言惊人相似
你想过你是如何描述一个颜色的吗?最新研究表明人类使用离散符号来记录一个区域的颜色,在细化颜色过程中又增添其他信息。这背后有什么道理吗?Facebook用两个神经网络的实验现象告诉你。
Facebook创造了两个会交流的神经网络来描述颜色,竟和人类语言惊人相似
|
机器学习/深度学习 人工智能 自然语言处理
如何让AI理解数学?Facebook神经网络通过“语言翻译”求解数学难题
近年来,随着 AI 的崛起,神经网络一词也不断出现在人们的视线中。事实上,神经网络并不是什么新兴词汇。
|
人工智能 自然语言处理 机器人
两个Bot自创新语言!Facebook机器人纽约自由行导航定位碾压人类
在FAIR和蒙特利尔大学合作的最新研究中,研究人员首次将实验中将感知、行动和使用自然语言交互达成目标这三个任务结合在一起:让两个Bot使用自然语言对话,让“导游bot”将“游客bot”带到指定地点,而且导航成功率超越了人类。
1654 0
|
人工智能 机器人 机器学习/深度学习
x3d
|
PHP
Facebook的Hack语言三大看点
Hack语言主要有三大看点:类型化、异步、集合。 Hack最基础的特性就是类型标注。PHP5已经开始支持对象的类型化,PHP7也提供了标量类型化声明。Hack提供了全面的类型标注支持,与其typecher配合使用,还可以实现快速、前置静态类型验证。
x3d
792 0