首页  思维导图  详情

P15

2021-05-05 12:15:39   3  举报





AI智能生成

南大软件分析P15

程序分析

作者其他创作

大纲/内容

Feasible and Realizable Paths（可行和可实现的路径）

JDK中一个方法的控制流图

所有这些路径都可执行吗？
不可行的路径：CFG中与实际执行不对应的路径。
我们希望程序分析结果不会被不可行的路径污染，或者被尽可能少的污染。
但是，给定一条路径，通常无法确定是否可行。

一个例子

例子

//注：Enter main底下对应的应该是Exit main，PPT有误，下面的图也是。

Inevitable（不可避免的）

Avoidable（可避免的）

Realizable Paths（可实现的路径）

“returns”与相应的“calls”相匹配的路径。

可实现的路径可能无法执行，但是不可实现的路径一定不能执行。

我们的目标是识别可实现的路径（realizable paths），以便避免沿无法实现的路径（unrealizable paths）得到的污染分析的结果。

如何识别可实现的路径

如何系统地识别可实现的路径？

CFL-Reachability（CFL-可达性）

上下午无关语言CFL

仅当路径的边上的标签（labels）的串联（concatenation）是指定上下文无关语言（context-free language）中的单词时，
才认为一条路径连接了两个节点A和B，或者从A可以到达B。

L语言的有效句子必须遵循L的语法。

上下文无关的语言是由上下文无关的语法（context-free grammar）（CFG）生成的语言。

CFG是一种形式语法（formal grammar），其中的每一种production都具有以下形式：

其中S是单个非终结符（nonterminal），而a可以是一连串的终结符 and/or 非终结符，或者为空。

where S is a single nonterminal and
a could be a string of terminals and/or nonterminals, or empty.

上下文无关意味着S可以在任何地方被aSb / kong取代，无论S出现在何处。//【注】processon无法复制希腊字母会出现乱码，暂时用kong表示空字符。

Partially Balanced-Parenthesis Problem via CFL

每个右括号“)i”都由前面的左括号“(i”平衡，但是反之则不必成立。

对于每个调用点i，将其调用边标记为“(i”，将返回边标记为 ")i”。

用符号“ e”标记所有其他边。

路径是可实现的路径，前提是该路径的单词使用语言L（realizable）。

Overview of IFDS

IFDS定义

Precise Interprocedural Dataflow Analysis via Graph Reachability
//通过图可达性进行精确的过程间数据流分析

//IFDS(过程间，有限，分布式，子集问题)

IFDS用于过程间数据流分析，具有有限域上的分布式流函数。

Provide meet-over-all-realizable-paths (MRP) solution.
//提供全部实现路径（MRP）解决方案。

Meet-Over-All-Realizable-Paths (MRP)

MOP

路径p的路径函数（表示为pfp），是p上所有边（有时是节点）的流动函数的组合。

Meet-Over-All-Paths (MOP)

对于每个节点n，MOPn提供“所有路径”的解决方案，
其中Paths（start，n）表示CFG中从起始节点到n的路径集。

MRP

Meet-Over-All-Realizable-Paths (MRP)

对于每个节点n，MRPn提供“所有实现路径”的解决方案，
其中RPaths（start，n）表示从起始节点到n的可实现路径的集合。
（路径的单词满足语言L（可实现））

MRP与MOP的关系

MRPn偏序于MOPn。

IFDS的过程

给定程序P和数据流分析问题Q。

（1）构建supergraph G*

为P建立一个超图（supergraph）G *，并基于Q为G *中的边定义流函数（flow functions）。

（2）构建exploded supergraph G#

通过将流函数转换为表示关系（representation relations）（图形）来为P构建分解的超级图（exploded supergraph）G＃。

（3）应用Tabulation algorithm

通过在G＃上应用制表算法（Tabulation algorithm），可以解决Q作为图形可达性问题（找出MRP解决方案）的问题。

设n为程序点，如果存在G＃中从<smain，0>到<n，d>的可实现路径，则数据事实（data fact）d∈MRPn。

疑问：d∈MRPn？d不是路径吧？

Supergraph and Flow Functions

Supergraph

在IFDS中，程序由称为超图的G * =（N *，E *）表示。

G *由流图G1，G2 ...（每个过程一个）的集合组成。

每个流图Gp具有唯一的开始节点sp和唯一的退出节点ep。

过程调用由调用节点Callp和返回站点节点Retp表示。

对于每个过程调用，G *具有三种边：

从Callp到Retp的过程内的call-to-return-site 边。

从Callp到被调用程序的sp的过程间的call-to-start 边。

从被调用程序的ep到Retp的过程间exit-to-return-site 边。

Design Flow Functions

“可能未初始化的变量（“Possibly-uninitialized variables）”

对于每个节点n∈N *，确定在执行达到n之前可能未初始化的变量集。

一个例子

具体过程和细节详见pdf。

两个注意点

λ S.S-{g}//g是整个程序的全局变量

“call-to-return-site”边允许传播本地变量信息

S- {g}有助于减少误报（不会损害健全性）。

λ S.S-{a}//a是被调用方法p的局部变量

//因为对于main方法而言，没有本地变量a，
//而当程序进入p方法时S可能会增加p的本地变量a，
//如果p方法中变量a没有初始化，则a会跟随S传出p方法，
//导致main方法的S中出现了a（实际上main方法并没有本地变量a）。
//所以在exit-to-return-site 边上，应该把a从S中删除。

Exploded Supergraph and Tabulation Algorithm

Build Exploded Supergraph

通过将流函数转换为表示关系（图形），为程序构建分解的超图形G＃。

每个流函数可以表示为具有2（D + 1）个节点（最多（D + 1）2个边）的图，其中D是数据流事实（dataflow facts）的有限集合。
//注：（D+1）2是（D+1）的二次方

流函数f的表示关系，Rf⊆（D∪0）×（D∪0），是定义如下的二进制关系（或图）：

Exploded Supergraph G#

上图G *中的每个节点n被“分解”为G＃中的D + 1个节点，G *中的每条边n1⟶n2被“分解”为与G＃中的n1⟶n2相关的流函数的表示关系。

为什么我们需要表示0⟶0的边？

在传统的数据流分析中，要查看数据事实a是否在程序点p成立，我们在分析完成后检查a是否在OUT [n4]中

数据事实是通过流函数的组成传播的。在这种情况下，直接从OUT [n4]的最终结果中检索“可达性”。

对于相同情况，在IFDS中，数据事实a是否保持在p，取决于是否存在从<smain，0>到<n4，a>的路径。
通过连接在“pasted” representation relations上的边（找出路径）来检索“可达性”。

λS. {a}表示与输入S无关的p处的保持有a；
但是，如果没有边0⟶0，
每条边的表示关系无法连接或“pasted”在一起，就像在传统数据流分析中无法将流函数组合在一起一样。
因此，IFDS无法通过这种分离的表示关系来产生正确的解决方案。