5.2.4 依赖循环的等值代码片段
在调研中发现,程序的控制流特征和数据流特征都会对路径的可达性产生影响,因此首先介绍控制流分析和数据流分析领域中的基本定义。
1.基本定义
当程序中包含循环结构时,其对应的控制流图是一个有向有环图。循环结构表示为L=(E L,N L,in L,out L),in L和out L分别是循环的入口节点和出口节点。
定义5-7(数据依赖) 令R和W表示对于一条节点上语句所进行的读操作和写操作的内存位置集合,如式(5-1)所示,节点ni和节点n j具有数据依赖,记为ni↔nj。数据依赖体现的是不同节点之间对相同内存位置的读写操作。
定义5-8(数据传播) 令n为一个赋值语句,将一个包含变量y的表达式赋值给变量v,此时称将y值传播给v,记为y→v。传播关系具有传递性,即y→v,v→z⇒y→z。
基于这些基本定义,给出如下定义。
定义5-9(条件依赖) ni和n j是控制流图G上两个表示条件语句的节点,令p是n i和n j之间的一条路径,当p中不包含赋值语句,并且R(ni)∩R(nj)=∅,或者p中包含赋值语句{n 1,n 1,…},并且x∈R(ni)∧y∈R(n j)时,ni和n j具有条件依赖关系。
数据依赖定义的是对同一内存位置读写操作之间的依赖关系。条件依赖关系描述了在不同的条件语句中出现了同一个内存位置的变量,导致变量具有多个约束的情况。条件依赖反映了不同位置的约束之间存在关联关系。
定义5-10(主宰循环) 令节点n的所有主宰节点集合为D(n)={d n 1,d n 2,…,d nm},若d ni和d nj是一个循环结构L的入口节点和出口节点,则称L为n的主宰循环。
节点n及其主宰循环L在控制流图上表现为L是n之前的完整循环,并且每一条从程序入口到n的路径都经过L。
定义5-11(独占节点) 令n是循环L={in L,out L}内的一个节点,若每一条从in L到n的路径都不经过任何循环(如图5-10(a)所示),或者同时包含另一个循环L′的入口节点和出口节点(如图5-10(b)所示),则n是L的独占节点。
定义5-12(等值判定条件) 令V(n)={v 1,v 2,…,v m}是条件节点n上出现的变量集合,若n的逻辑表达式φ中包含比较操作v 1=N,其中N是常量,那么n为等值判定条件。(https://www.daowen.com)
以C语言为例,包含等式操作符以及一个操作数是常量的条件语句等值判定条件,例如,条件语句“if(v==3)”的真分支在变量v的值为3时成立。在判定约束的可满足性时,许多约束求解器会对这种情况进行优化运算来提高判定效率。
程序中符合等值判定条件定义的情况不仅限于隐含的表达式符合等值判定条件,表5-1中列举了C语言中出现的等值判定条件表达式,这些情况都将被考虑到代码片段的识别中。
图5-10 两种n是L的独占节点情况举例
表5-1 C语言中等值判定条件的出现形式
2.依赖循环的等值代码片段
基于前面的基本定义,我们给出依赖循环的等值代码片段的定义。
定义5-13(依赖循环的等值代码片段) 令L是一个循环结构,n是一个等值判定条件节点,L是n的主宰循环或者n是L的独占节点,若L中存在节点n l与n有数据依赖或者条件依赖,那么L与n构成依赖循环的等值代码片段(Loop-Dependent Concrete Condition),简记为LDc2模式。
数据依赖和条件依赖在数据流上描述了不同节点之间条件的关联关系。主宰循环和独占节点描述了可达路径的可能性。需要注意的是,在循环中不能包含n中变量的重定义,这是因为对变量的重定义会为变量分配新的内存单元,违反了数据依赖的定义。图5-11给出了包含依赖循环的等值代码片段的形式,假设循环中都包含目标节点nc的数据依赖节点或条件依赖节点,满足LDc2的循环以√标注,否则以×表示。其中L 4和L 5不是nc的主宰循环,因此不构成依赖循环的等值代码片段。
猜测包含此代码片段的程序具有如下性质:等值判定条件n c的约束可能导致矛盾的路径条件,并且矛盾约束在nc下被触发。
图5-11 LDc2举例
