P14
2021-05-05 12:15:07 1 举报AI智能生成
南大软件分析P14
作者其他创作
大纲/内容
Motivation
Imperative vs Declarative（命令式与声明式）
目标：从人群中选择成年人
Imperative//命令式：怎么做（〜实现）
Declarative//声明式：该做什么（〜规格）
如何进行程序分析？
规则
指向分析，命令式实现
指针分析，声明式实现（通过Datalog）
•简洁
•可读（基于逻辑的规范）
•易于实施
•可读（基于逻辑的规范）
•易于实施
Introduction to Datalog
Datalog
Datalog是一种声明性逻辑编程语言，是Prolog的子集。
它作为一种数据库语言出现（1980年代中期）
现在它有各种各样的应用
•程序分析
•声明式网络
• 大数据
• 云计算
•…
•声明式网络
• 大数据
• 云计算
•…
•无副作用
•无控制流
•无函数
•图灵不完整
•无控制流
•无函数
•图灵不完整
Predicates (Data)//谓词（数据）
在数据记录中，谓词（关系）是一组语句
本质上，谓词是数据表
一个事实（fact）断言一个特定的元组（一行）属于一个关系（一个表），即它表示谓词对于特定的值组合为true。
Atoms（原子）
原子是数据记录的基本元素，代表形式的谓词。
Terms（条目）
Variables（变量）：代表任何值
Constants（常数）
例子
Atoms (Cont.)//原子（续）
P（X1，X2，…，Xn）被称为关系原子（relational atom）
当谓词P包含由X1，X2，…，Xn描述的元组时，P（X1，X2，…，Xn）计算为true。
除了关系原子之外，Datalog还具有算术原子（arithmetic atoms）
Datalog Rules (Logic)//Datalog规则（逻辑）
规则是表达逻辑推理的一种方式
规则还用于指定如何推论事实
规则的形式是
Datalog Rules (Cont.)//Datalog规则（续）
“，”可以读为（逻辑and），即对于主体B1，B2，…，Bn，如果所有子目标B1，B2，...和Bn均为true，则为true。
例如，我们可以通过Datalog规则推导出成年人：
如何解释规则？
考虑子目标中变量值的所有可能组合。
如果组合使所有子目标为真，则头部原子（具有相应的值）也为真。
头谓词由所有真实原子组成。
规则解释的一个例子
Datalog program = Facts + Rules
EDB和IDB谓词
按照惯例，Datalog中的谓词分为两种：
EDB (extensional database)//扩展数据库
•先验中定义的谓词
•关系是一成不变的
•可以看作是输入关系
•关系是一成不变的
•可以看作是输入关系
IDB (intensional database)
•仅由规则建立的谓词
•关系是由规则推断的
•可以看作是输出关系
•关系是由规则推断的
•可以看作是输出关系
Logical Or（逻辑或）
在Datalog中，有两种表达逻辑或的方法
1.用相同的头写多个规则
2.使用逻辑或运算符“;”
“;”的优先级 （或）小于“，”（和），因此析取可以用括号括起来，例如H <-A，（B; C）。
Negation（否定）
在Datalog规则中，子目标可以是否定的原子，这会否定其含义。
否定的子目标写为！B（…），读为非B（…）
例如，要计算需要参加补考的学生，我们可以编写
Student存储所有学生的位置，PassedStd存储通过考试的学生的位置。
Recursion（递归）
Datalog支持递归规则，该规则允许从其自身（直接/间接）推导IDB谓词。
例如，我们可以使用递归规则来计算图的可达性信息（即，传递闭合）：
其中Edge（a，b）表示图具有从节点a到节点b的边，而Reach（a，b）表示b是从a可达的。
没有递归，Datalog只能表达基本关系代数的查询。
基本上是带有SELECT-FROM-WHERE的SQL
通过递归，Datalog变得更加强大，并且能够表达复杂的程序分析，例如指向分析。
规则安全
对于这两个规则，x的无穷大值都可以满足该规则，这使得A为无穷关系。
•如果每个变量都出现在至少一个非负相关原子中，则规则是安全的。
•以上两个规则是不安全的。
•在Datalog中，仅允许使用安全规则。
•以上两个规则是不安全的。
•在Datalog中，仅允许使用安全规则。
Recursion and Negation
该规则是矛盾的，没有道理。
在Datalog中，原子的递归和负数必须分开。 否则，规则可能包含矛盾，并且推论无法收敛。
执行Datalog程序
Datalog引擎根据给定的规则和EDB谓词推论事实，直到无法推论出新事实为止。
一些现代的Datalog引擎
LogicBlox, Soufflé, XSB, Datomic, Flora-2, …
单调性
数据记录是单调的，因为无法删除事实。
终止
Datalog程序总是终止，因为：
1）数据记录是单调的
2）IDB谓词的可能值是有限的（规则安全性）
2）IDB谓词的可能值是有限的（规则安全性）
Pointer Analysis via Datalog
Pointer Analysis via Datalog
EDB
可以从程序中语法提取与指针相关的信息。
IDB
指向分析结果。
Rules
指向分析规则。
用于指向分析的Datalog模型
一个例子
基础语句
调用语句
全程序分析
Taint Analysis via Datalog
指向分析之上的EDB/IDB谓词
处理source（生成污染数据）
处理sink（生成污染流信息）
基于Datalog的程序分析的优缺点
优点
简洁易读
易于实施
受益于现成的优化数据记录引擎
缺点
受限制的表达方式，即表达某些逻辑是不可能或不便的
无法完全控制性能
0 条评论
下一页
