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

An abstract domain based on two-interval octagonal constraints

抽象解释静态程序分析技术用来发现运行时错误,保证程序正确性,已经被成功应用到工业界。抽象域是抽象解释理论中的一个重要方面,然而大部分已存在的数值抽象域无法表示程序的非凸性质,抽象域的这种凸性限制很多时候会影响数值分析的精度,甚至带来更多误报。基于两区间八边形约束,提出了一个新的数值抽象域,其约束形式为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.