基于区间线性模版约束的程序分析

Program Analysis Based on Interval Linear Template Constraints

抽象解释是一种对程序语义进行可靠近似的通用理论,该理论在保证可靠性的前提下,可为程序变量的值范围分析提供一个通用的框架.抽象域是抽象解释框架的核心,在该框架下面向数值性质分析的数值抽象域得到了广泛的关注.其中,模板多面体抽象域的表达能力覆盖了程序分析中常用的弱关系型抽象域,如区间抽象域、八边形抽象域等.该文对经典的基于线性模版约束的模版多面体抽象域进行扩展,以支持区间线性模版约束,从而得到一个新的数值抽象域——区间线性模版约束抽象域,可以用来推导变量间形如"∑k[a_k,b_k]x_k≤c"的区间线性不等式关系(其中区间系数[a_k,b_k]为分析前预先确定的常量).该抽象域采用"弱解"作为区间线性约束的解语义,可以表达某类非凸(甚至非联通)性质,因而比经典的模版多面体抽象域表达能力更强.区间线性模板约束抽象域的域元素可以看作是一系列模版多面体的析取,几何上,其域元素与每个象限的交均是一个凸的模板多面体(可以为空).该文给出了区间线性模版约束抽象域的域表示和域操作,基于该抽象域的静态分析算法主要基于区间线性规划来实现.进一步,该文讨论了基于区间线性模版约束抽象域中区间线性模版的生成方法.最后,该文在开源数值抽象库APRON中实现了区间线性模版约束抽象域,并开展了程序分析实验.初步的实验结果表明区间线性模版约束抽象域可以有效地分析程序中的析取行为.

Abstract The problem of automatically inferring numerical invariants in a program has received wide attention in the analysis and verification of programs. Abstract interpretation is a general theory to soundly approximate program semantics. It provides a general framework to analyze value ranges of program variables, guaranteeing the soundness of the analysis. Abstract domain is key to the framework of abstract interpretation, which achieves a trade-off between efficiency and precision, and especially various numerical abstract domains have been proposed under this framework. In particular, the expressiveness of the template constraint matrix domain （TCM） subsumes most weakly relational abstract domains that are commonly used in practical programanalysis, for example, interval abstract domain （a≤x≤b）, octagon abstract domain （±x±y≤c）,etc. During the analysis and verification of real-life systems, due to uncertainty, the application data in the model or program may not be known exactly, which is then often provided or modelled in terms of intervals. Moreover, in practice, floating-point arithmetic and non-linear expressionsare often abstracted into linear expressions with interval coefficients. In other words, interval coefficients appear naturally during program analysis in practice. Hence, abstract domains that can infer interval linear relationships among variables are desired. This paper extends classical template constraint matrix domain which is based on linear template constraints, to support interval linear template constraints, and proposes a new numerical domain--interval template constraint matrix domain （itvTCM）, which could infer interval linear inequality relations among variables inthe program in the form of ＂∑k[ak,bk]xk≤c＂ （where the interval coefficient [ak, bk ] is determinedbefore analysis）, itvTCM makes use of ＂weak solution＂ as the semantics of the solution of interval linear constraints, which could represent certain non-convex （even non-connected） properties, and thus it is more expressive than TCM. Each itvTCM element could be considered as a disjunction of multiple TCMs but without using any explicit disjunctive operations. From the geometric point of view, each itvTCM element maps each orthant to a convex polyhedron （maybe an empty polyhedron）. This paper provides domain representation and domain operations （such as join, meet, widening, etc. ） of itvTCM, and most domain operations of itvTCM are implemented based on interval linear programming. Theoretically, the complexity of some domain operations of itvTCM is at worst exponential of that of the corresponding domain operations in classic TCM. However, in practice, we could alleviate this problem through restricting the number of interval coefficients. In this paper, we also discuss how to generate templates for itvTCM. Finally, we have implemented itvTCM in the numerical abstract domain library APRON, and conducted experiments. The preliminary experimental results show that itvTCM is useful to capture disjunctive behaviors of a program.