一个基于两区间八边形约束的抽象域  

An abstract domain based on two-interval octagonal constraints

作　　者：丁泽文[1] 郭鸿昌 阚双龙[1] 张弛[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京210016 [2]东部战区空军装备部,江苏南京210018

出　　处：《计算机工程与科学》2017年第4期740-747,共8页Computer Engineering & Science

基　　金：国家863计划(2015AA015303);江苏省研究生培养创新工程(KYLX_0315);国家自然科学基金(61272038)

摘　　要：抽象解释静态程序分析技术用来发现运行时错误,保证程序正确性,已经被成功应用到工业界。抽象域是抽象解释理论中的一个重要方面,然而大部分已存在的数值抽象域无法表示程序的非凸性质,抽象域的这种凸性限制很多时候会影响数值分析的精度,甚至带来更多误报。基于两区间八边形约束,提出了一个新的数值抽象域,其约束形式为x±y∈[a,b]∪[c,d],其中x和y表示变量取值,a,b,c,d∈R。该抽象域的域元素是用两区间八边形约束表示,因此可以表达某类非凸性质,表达能力强于经典的八边形抽象域,并且相对于八边形抽象域,域操作的计算复杂度并没有提高太多。Static program analysis with abstract interpretation has been successfully applied to industry in order to avoid runtime errors and ensure the correctness of the software. Abstract domain is one of the important aspects in abstract interpretation theory. However, most of the existing numerical abstract domains cannot express non-convex properties. These limitations often affect the precision of numerical analysis and even lead to more false alarms.We propose a numerical abstract domain based on two-interval octagonal constraints. This abstract domain allows us to represent invariants of the form x±y∈［a,b］∪［c,d］, where x and y are variable values and a,b,c,d∈R. Domain elements in this abstract domain are represented by two-interval octagonal constraints, so the new abstract domain can express certain non-convex properties and is more expressive than the octagon abstract domain, with only a small overhead in the computational complexity of domain operation.

关 键 词：抽象解释 八边形抽象域 两区间 迁移函数 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]