Practical Memory Leak Detection using Guarded Value-Flow Analysis 论文阅读

本文于 2007 年投稿于 ACM-SIGPLAN 会议1

概述

指针在代码编写过程中可能出现以下两种问题:

  1. 存在一条执行路径,指针未成功释放(内存泄漏),如下面代码中注释部分所表明的:

    int foo()
    {int *p = malloc(4 * sizeof(int));if (p == NULL)return -1;int *q = malloc(4 * sizeof(int));if (q == NULL)return -1; // 注意这里,q为NULL时p一定不为NULL,但是函数直接返回,导致p所指向的区域未释放// some code to executefree(p);free(q);return 0;
    }
    
  2. 存在一条执行路径,指针被重复释放(未定义行为),如 free 一个空指针。

    	int *p = (int *)malloc(4 * sizeof(int));int *q = p;free(q);q = p;free(q);
    

最笨拙的方法是枚举每一条可能的路径,依次判断。但是这显然是不切实际的。因而本文的主要工作是提出一个能够发现未释放指针或重复释放指针的高效算法,并进行了代码实现,提示编写者具体可能的错误原因。即给定一个程序,找到其中可能存在的这种问题。

首先进行控制流图(Condition-Flow Graph,CFG)的约定:

  1. 赋值(运算节点): e = e ′ e=e' e=e
  2. 函数调用: e = f ( p 1 , p 2 , ⋯ , p m ) e=f(p_1,p_2,\cdots,p_m) e=f(p1,p2,,pm)
  3. 返回: return e \texttt{return}\ e return e
  4. 分支节点: switch e ( c 1 , n 1 ; c 2 , n 2 ; ⋯ ; c k , n k ; n t ) \texttt{switch}_e(c_1,n_1;c_2,n_2;\cdots;c_k,n_k;n_t) switche(c1,n1;c2,n2;;ck,nk;nt)。即一个节点根据表达式 e e e 的值不同可以有 k + 1 k+1 k+1 个分支跳转地址,分别记作 I n = { n 1 , n 2 , ⋯ , n k , n t } I_n=\{n_1,n_2,\cdots,n_k,n_t\} In={n1,n2,,nk,nt},最后一个为默认跳转地址。

此外,本文将问题进行了规约:定义 s o u r c e − s i n k [ n , m ] {\rm source-sink}[n,m] sourcesink[n,m] 问题为从 s r c \rm src src 会流入到 [ n , m ] [n,m] [n,m] s i n k \rm sink sink 的条件可满足性问题。对于未释放,则是 s o u r c e − s i n k [ 0 , 0 ] {\rm source-sink}[0,0] sourcesink[0,0] 问题,而多次释放则是 s o u r c e − s i n k [ 2 , ∞ ] {\rm source-sink}[2,\infty] sourcesink[2,] 问题,而合法性判断是 s o u r c e − s i n k [ 1 , 1 ] {\rm source-sink}[1,1] sourcesink[1,1] 问题。

算法流程

整体算法流程图如下所示:

在这里插入图片描述

  1. 利用编译器前端搭建 CFG。
  2. 到达定值点分析
  3. 值流图构建
  4. 无条件可达性分析,即不考虑具体控制流图上条件进行的分析
  5. 条件可达性分析,即考虑控制流图上条件进行的分析。

在实现该算法的同时还需要调用:

  1. 指针区域分析,即分析流图中每个指针所指向的内存区域。
  2. 条件分析。
  3. SAT(可满足性问题)解决器,即给定一组条件约束,返回一组可满足所有条件的初始值或报告无解。下文会将本论文中提出的问题规约到可满足性问题。

到达-定值分析(Reaching-Definition Analysis)

编译原理中经典的数据流分析方法。下文中用 p d o m ( x , n , m ) pdom(x,n,m) pdom(x,n,m) 来描述变量 x x x 能不能从 CFG 上流图节点 n n n 值不发生改变的到节点 m m m。论文中的 S S S 仅为一个记忆化的集合,不做具体参数使用。 p d o m pdom pdom 的计算使用逆向数据流分析方法:
p d o m ( x , n , m ) = { t r u e , m = n f a l s e , n 没有出边(返回节点) ⋀ i ∈ I n p d o m ( x , i , m ) ∧ ¬ d e f i n e ( x , i ) , 其他情况 pdom(x,n,m)= \begin{cases} true, m=n\\ false,\text{$n$ 没有出边(返回节点)}\\ \bigwedge_{i \in I_n} pdom(x,i,m) \wedge ^\lnot{define}(x,i),\text{其他情况} \end{cases} pdom(x,n,m)= true,m=nfalse,n 没有出边(返回节点)iInpdom(x,i,m)¬define(x,i),其他情况
其中 d e f i n e ( x , i ) define(x,i) define(x,i) 表示 i i i 节点没有进行对变量 x x x 的赋值操作。

构建值流图(Value-Flow Graph)

在构建值流图之前首先需要介绍 free 函数的工作原理或特性:

  1. 它释放传入参数给定的指针所指向的区域,也就是说它是针对内存区域而非指针的。例如下面的两个例子:

    1. 下面代码中 p1p2 指针所指向的区域都被释放了。

    下面代码中 p 指针指向区域并未完全释放——p 指针所指向的区域仍有一个 int 大小的空间未释放。

    	int *p = malloc(4 * sizeof(int));int *q = p + 1;free(q);
    

基于以上两个特性,构建如下的节点:

  1. 赋值(运算)节点。针对 CFG 上每个形如 x = y x=y x=y 形式的赋值语句都对应一个 VFG 的节点。

  2. 内存区域节点。由于 free 是针对区域而非指针型变量,因而需要用一个单独的节点描述它是否有被释放的途径。该部分节点用 n r n_r nr 表示,可以使用这篇论文2中的方法快速描述代码中每个指针可能对应的内存区域集合。

    这里还需要注意的是,由于指针存在加减法操作,因而这里需要额外使用一个偏移量来去衡量该内存地址的具体使用情况。

  3. 释放节点。每个 free 函数调用的节点都对应一个 VFG 上的汇(sink)点。

  4. 函数调用实参节点。由于进行函数调用,可以视为进行一次变量的值使用,记为 x @ n x_{@}n x@n

  5. 函数调用形参节点。在被调用函数(callee)中该函数作为新变量使用,同时它对应于调用函数(caller)的一个变量。为避免函数多次调用导致边关系混乱,因而新建一个形参节点以解决图过于混乱的问题,记为 [ p ] [p] [p]

  6. 函数返回节点。函数的返回值可能在 caller 中作为一个新变量继续存在,并涉及后续赋值和计算。

遍历 CFG,按如下规则建图(假设当前节点为 n n n):

  1. 赋值语句 y = x y=x y=x、释放节点 f r e e ( x ) free(x) free(x)、返回节点 r e t u r n ( x ) return(x) return(x):将所有 x x x 的定值点集合 n x n_x nx 建立一条边连到 n n n 节点。
  2. y = f ( x 1 , x 2 , ⋯ , x m ) y=f(x_1,x_2,\cdots,x_m) y=f(x1,x2,,xm):对于每个函数实参 x i x_i xi,首先将 x i x_i xi 的定值点集合连接一条边到对应的实参节点( n x i → x i @ n n_{x_i} \to {x_i}_@n nxixi@n),然后每个实参节点连接到形参节点 x i @ n → p i {x_i}_{@}n \to p_i xi@npi,最后将 callee 函数的返回节点 n r e t f n_{\rm ret}^f nretf 连接到当前函数调用节点(该语句可以视为一种特殊类型的赋值语句) n r e t f → n n_{\rm ret}^f \to n nretfn
  3. 对于赋值变量中 x x x y y y 不是一个有效节点的(如 malloc 函数返回的堆区域指针),调用内存区域查询函数返回对应的内存区域节点。

无条件可达性分析(Unguarded Reachability Detection)

该步骤中忽略了程序流图中的条件,即认为所有的边都是可走到的,在这种情况下先简单分析是否每个 malloc 函数都有至少一个 free 与之对应。

  1. 枚举一个起始点 s r c src src,首先找到 VFG 顺向流图中可到达节点集合 F s r c F_{src} Fsrc
  2. 找到 F s r c F_{src} Fsrc 中所有的 free 语句对应节点,记为 K K K
  3. 分类讨论:
    1. 如果 K K K 为空,则该 malloc 语句无对应 free 语句,直接报告内存泄漏。
    2. 如果从该 s r c src src 节点可以到达一个内存区域节点,则说明该代码片段中存在全局变量,暂时不继续分析该代码的内存泄漏问题,直接退出。
    3. 找到能从 s r c src src 到并且能到达 K K K 的集合 R R R,并将 R R R 集合传递到下一步继续分析。

条件可达性分析(Guarded Reachability Detection)

预处理

首先在 CFG 上进行条件分析。考虑每个分支节点 n n n 需要满足其分支出口唯一,即对于分支节点 n n n switch e ( c 1 , n 1 ; c 2 , n 2 ; c k , n k ; n t ) \texttt{switch}_e(c_1,n_1;c_2,n_2;c_k,n_k;n_t) switche(c1,n1;c2,n2;ck,nk;nt),需要满足:
C n = [ ⋁ i ( e = c i ) n ] ∧ [ ⋀ i ≠ j ( e = c i ) n ∧ ( e = c j ) n ‾ ] C_n=\left [\bigvee_{i}(e=c_i)_n\right] \wedge \left[\bigwedge_{i \ne j} \overline{(e=c_i)_n \wedge (e=c_j)_n}\right] Cn=[i(e=ci)n] i=j(e=ci)n(e=cj)n
即存在一条出路,且不存在一个条件同时满足两条出路。

定义函数 c g ( x , n , m ) cg(x,n,m) cg(x,n,m)(下简写成 c g u a r d ( n → m ) cguard(n \to m) cguard(nm),其中程序点 n n n 为形如 x = e x=e x=e 的赋值语句)表示变量 x x x 从程序点 n n n m m m 需要满足的输入条件集合,有如下递推:
c g ( x , n , m , E ) = { t r u e , 如果满足支配关系即 p d o m ( x , n , m ) c g ( x , n 1 , m , E ) , n 处无分支, n 1 为 n 语句的唯一后续语句 ⋁ i ∈ I n , x , E c o n d ( n , n i , E ) ∧ c g ( x , n i , m , E ∪ { ⟨ n , n i ⟩ } ) , 其他情况 cg(x,n,m,E)= \begin{cases} true,\texttt{如果满足支配关系即 $pdom(x,n,m)$}\\ cg(x,n_1,m,E),\texttt{$n$ 处无分支,$n_1$ 为 $n$ 语句的唯一后续语句}\\ \bigvee_{i \in I_{n,x,E}} cond(n,n_i,E) \wedge cg(x,n_i,m,E \cup \{\langle n,n_i\rangle\}),\texttt{其他情况} \end{cases} cg(x,n,m,E)= true,如果满足支配关系即 pdom(x,n,m)cg(x,n1,m,E),n 处无分支,n1  n 语句的唯一后续语句iIn,x,Econd(n,ni,E)cg(x,ni,m,E{⟨n,ni⟩}),其他情况
其中 I n , x , E I_{n,x,E} In,x,E 表示满足后续节点不是形如 d e f i n e ( n i , x ) define(n_i,x) define(ni,x) ⟨ n , n i ⟩ \langle n,n_i \rangle n,ni 不在 E E E 中的后续节点集合 { n i } \{n_i\} {ni} c o n d ( n , n i , E ) cond(n,n_i,E) cond(n,ni,E) 函数表示从 n n n 节点走到 n i n_i ni 节点所需要满足的条件,并且要求 n n n 节点后续不能有 E E E 中的边:
c o n d ( n , n i , E ) = { ( e = c i ) n , n 是一个分支节点,且 n 的后续集合不在 E 集合中 t r u e , 其他情况 cond(n,n_i,E)= \begin{cases} (e=c_i)_n,\texttt{$n$ 是一个分支节点,且 $n$ 的后续集合不在 $E$ 集合中}\\ true,\texttt{其他情况}\\ \end{cases} cond(n,ni,E)={(e=ci)n,n 是一个分支节点,且 n 的后续集合不在 E 集合中true,其他情况
这里 ( e = c i ) n (e=c_i)_n (e=ci)n 表示在程序分支判断点 n n n 处进行条件判断 e = c i e=c_i e=ci

这里加入 E E E 集合(已遍历的边集合)作为参数是方便代码实现上的,由于流图中可能有环存在,因而不能重复遍历同一条边,通过在状态中多维护一个 E E E 集合可以有效防止重复遍历到同一条边。在 c o n d cond cond 中,显然要进入循环然后退出该循环需要同时满足在循环的出口判断中 e = c i e=c_i e=ci e ≠ c i e \ne c_i e=ci,这显然是永假的。因而这里加入了边的限制条件以防止上述情况的出现。当然这里会存在一个小漏洞就是仅判断了循环入口点的条件,未判断出口点的。这里会对未释放问题的判定产生一定的影响,但是对多重释放不会。

接下来就是考虑利用这些条件在 VFG 上进行条件判断。同样定义 v g u a r d ( n , m ) = v g ( n , m ) vguard(n,m)=vg(n,m) vguard(n,m)=vg(n,m) 函数表示从 VFG 图上 n n n 节点走到 m m m 的约束条件集合,有:
v g ( n , m , E ) = { t r u e , n = m ⋁ n → n ′ ∈ E c g u a r d ( n → n ′ ) ∪ v g ( n ′ , m , E ∪ { n → n ′ } ) , 其他情况 vg(n,m,E)= \begin{cases} true,n=m\\ \bigvee_{n \to n' \in E} cguard(n \to n') \cup vg(n',m,E \cup \{n \to n'\}),\texttt{其他情况} \end{cases} vg(n,m,E)={true,n=mnnEcguard(nn)vg(n,m,E{nn}),其他情况
和在 CFG 上的情况类似,这里只需要在 VFG 图上再加入 CFG 上的信息即可。

分析过程

考虑对于一个确定的 s r c src src 节点和所有该指针的释放操作汇点 K K K,在 2.3 节中阐述的 R R R 集合上进行分析。定义 G k = v g u a r d ( s r c , k ) G_k=vguard(src,k) Gk=vguard(src,k) C C C R R R 上所有的分支节点需要满足的 C n C_n Cn 的与集合。此时就满足了一个 SAT 问题的框架:

  1. 如果此处存在一组初值指派满足 ∨ k ∈ K G k ‾ ∧ C \overline{\vee_{k \in K} {G_k}} \wedge C kKGkC,则表明存在某种初值指派,使得从该 s r c src src 语句无法走到任何一个汇点,即发生了内存泄漏。
  2. 如果存在一组初值指派,满足 ∃ i ≠ j , G i ∧ G j ∧ C \exists i \ne j,G_i \wedge G_j \wedge C i=j,GiGjC,则表明某组初值指派可以到达两个不同的 free 语句,进行多次释放操作,因而发生未定义行为(Undefined Behavior)。

可以注意到上述的操作时间复杂度是比较高的,特别是对于有大量 malloc 语句存在的时候。因而本文中仅对操作数不超过阈值 30 30 30 的代码进行分析。

本文同时实现了代码,将所有的错误种类分成以下几类:

  1. 从未释放。又分为:a)指针作为局部变量在 main 函数或其他函数未释放;b)指针作为全局变量或存在于数组等结构中未释放。
  2. 释放。又分为:a)一切条件下都能释放;b)某些情况下能释放,有些情况未释放。
  3. 不能判定,认为释放了。这种情况通常因为分析语句过多导致超过阈值停止分析。

  1. Cherem S, Princehouse L, Rugina R. Practical memory leak detection using guarded value-flow analysis[C]//Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2007: 480-491. ↩︎

  2. Bjarne Steensgaard. Points-to analysis in almost linear time. In Proceedings of the ACM Symposium on the Principles of Programming Languages, St. Petersburg Beach, FL, January 1996. ↩︎

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.hqwc.cn/news/130696.html

如若内容造成侵权/违法违规/事实不符,请联系编程知识网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

Matlab之查询子字符串在字符串中的起始位置函数strfind

一、功能 strfind函数用于在一个字符串中查找指定的子字符串,并返回子字符串在字符串中的起始位置。 二、语法 indices strfind(str, pattern) 其中,str是要进行查找的字符串,pattern是要查找的子字符串。 函数会返回一个由子字符串在字…

【Java 进阶篇】CSS语法格式详解

在前端开发中,CSS(层叠样式表)用于控制网页的样式和布局。了解CSS的语法格式是学习如何设计和美化网页的关键。本文将深入解释CSS的语法格式,包括选择器、属性和值等基本概念,同时提供示例代码以帮助初学者更好地理解。…

关于:未同意隐私政策,应用获取ANDROID ID问题

一、环境 Unity2018 4.21f1、Android Studio、Windows10 二、问题描述 我在提交华为应用时,总是提示【未同意隐私政策,应用获取ANDROID ID个人信息】,但是我已经全部去掉了,后面问了人工客服,反馈了如下信息 调用堆…

Linux 文件链接

Linux 下的文件链接有两类。一个是类似于 win 电脑的快捷方式,我们称为软链接,软链接也可以叫做符号链接。另一种是通过文件系统的 inode 连接来产生的,类似于 windows 电脑的复制,但是不产生新的文件,我们称为硬链接。…

UDP的报文结构和注意事项

前言 UDP(User Datagram Protocol)是一种无连接的传输层协议,它提供了一种简单的数据传输方式,适用于那些对可靠性要求不高的应用。本文将总结UDP的报文结构和一些使用UDP时需要注意的事项 UDP报文结构 UDP报文相对简单&#xf…

Mall脚手架总结(三) —— MongoDB存储浏览数据

前言 通过Elasticsearch整合章节的学习,我们了解SpringData框架以及相应的衍生查询的方式操作数据读写的语法。MongoDB的相关操作也同样是借助Spring Data框架,因此这篇文章的内容比较简单,重点还是弄清楚MongoDB的使用场景以及如何通过Sprin…

Potplayer结合cpolar内网穿透实现公网访问群晖WebDAV

把potplayer变成netflix需要几步? ​ 国内流媒体平台的内容让人一言难尽,就算是购买了国外的优秀作品,也总是在关键剧情上删删减减,就算是充了会员,效果如何? 广大网友不得不选择自己找资源下到本地&#x…

婚礼避坑指南(tips分享)

1️⃣自己买婚纱很可能比租的更省钱,更时髦。我是先去婚纱店看,玲琅满目的婚纱让我看花了眼,试穿了几件重工的婚纱感觉并不是自己喜欢的款式,穿着也不舒服,而且租金都要几千。自己在京东上400买的反倒特别满意。 2️…

Oracle 云服务即将支持 PostgreSQL!

2023 年 9 月 19 日,Oracle 产品团队发布了一篇文章,宣布 Oracle 云基础架构(OCI)开始提供 PostgreSQL 服务。目前支持的版本为 PostgreSQL 14.9,提供有限支持,12 月份将会提供正式版本。 众所周知&#x…

Citespace、vosviewer、R语言文献计量学 、SCI

​文献计量学是指用数学和统计学的方法,定量地分析一切知识载体的交叉科学。它是集数学、统计学、文献学为一体,注重量化的综合性知识体系。特别是,信息可视化技术手段和方法的运用,可直观的展示主题的研究发展历程、研究现状、研…

信息系统项目管理师第四版学习笔记——项目整合管理

管理基础 项目整合管理由项目经理负责,项目经理负责整合所有其他知识领域的成果,并掌握项目总体情况。项目整合管理的责任不能被授权或转移,项目经理必须对整个项目承担最终责任。 项目管理过程中,会使用并产生两大类文件&#…

Jetpack:004-如何使用文本组件

文章目录 1. 概念介绍2. 使用方法2.1 通用参数2.2 专用参数 3. 示例代码4. 内容总结 我们在上一章回中介绍了Jetpack组件在布局中的对齐方式,本章回中主要介绍文 本组件的使用方法。闲话休提,让我们一起Talk Android Jetpack吧 1. 概念介绍 我们在本章…