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

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