计算机学报
計算機學報
계산궤학보
CHINESE JOURNAL OF COMPUTERS
2010年
3期
427-439
,共13页
值范围分析%静态分析%抽象解释%抽象域%区间分析
值範圍分析%靜態分析%抽象解釋%抽象域%區間分析
치범위분석%정태분석%추상해석%추상역%구간분석
value range analysis%static analysis%abstract interpretation%abstract domain%interval analysis
程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域--单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中.
程序變量的值範圍信息對于編譯器優化、程序分析與驗證等應用至關重要.抽象解釋理論提供瞭一種通用框架為程序變量計算近似的但是可靠的值範圍.然而該框架下已有的數值抽象域在錶達非凸性質方麵存在一定的跼限性,影響瞭值範圍分析的精度.文中基于抽象解釋理論,提齣一箇新的數值抽象域--單變量區間線性不等式抽象域.其主要思想是使用單變量區間線性不等式約束作為域元素的約束錶示方法.該抽象域的錶達能力彊于經典的區間抽象域,併允許錶達某類非凸、非連通性質.同時,其域操作存在高效的實現算法.該抽象域具有很彊的可擴展性,能夠應用在實際大規模的程序分析中.
정서변량적치범위신식대우편역기우화、정서분석여험증등응용지관중요.추상해석이론제공료일충통용광가위정서변량계산근사적단시가고적치범위.연이해광가하이유적수치추상역재표체비철성질방면존재일정적국한성,영향료치범위분석적정도.문중기우추상해석이론,제출일개신적수치추상역--단변량구간선성불등식추상역.기주요사상시사용단변량구간선성불등식약속작위역원소적약속표시방법.해추상역적표체능력강우경전적구간추상역,병윤허표체모류비철、비련통성질.동시,기역조작존재고효적실현산법.해추상역구유흔강적가확전성,능구응용재실제대규모적정서분석중.
The value range information of program variables is crucial for many applications,such as compiler optimization,program analysis and verification,etc.The theory of abstract interpretation provides a general framework to compute statically approximate but sound value ranges for program variables.However,most existing numerical abstract domains under the framework have limitations in expressing non-convex properties,which may lead to imprecision during the value range analysis.This paper proposes a new numerical abstract domain under the framework of abstract interpretation,namely an abstract domain of one-variable interval linear inequalities.The main idea is to use one-variable interval linear inequality constraints as the representation of domain elements.The new domain is more expressive than the classic interval abstract domain and allows expressing certain non-convex,unconnected properties.Moreover,its domain operations can be implemented via efficient algorithms.Thus,it has high scalability and can be applied in large-scale program analysis in practice.