抽象解释静态分析：数学规划方法及其应用

理论计算机科学电子笔记267（2010）73-87www.elsevier.com/locate/entcs抽象解释静态分析：一种数学规划方法埃里克·古博特a，2，1，St'ephaneLeRouxb，3，JeremyLecontec，4，Leo Libertib，5和Fabrizio Marinellid，6aCEA Saclay，法国bLIX，E'colePolytechnique，91128Palaiseau，法国c信息，ENS，45 ruedDIIGA，大学Politecnica delle Marche，安科纳，意大利摘要通过抽象解释对计算机程序进行静态分析有助于证明程序的行为特性。程序是通过一个前向收集语义函数来定义的，在程序执行过程中的程序变量。语义函数的最小固定点是提供有关程序行为的有用信息的程序不变量。数学规划是一种用于描述和解决以非常一般的术语表达的优化问题的形式语言。本文通过提供一个数学程序来模拟寻找语义函数的最小不动点的问题，从而建立了这两个学科之间的联系。虽然我们将讨论限制在区间域上的整数算术语义，的数学规划工具有潜力丰富的静态分析相当。关键词：保证最小码不变，约束，双线性MINLP，策略迭代，分支定界。1介绍抽象解释静态分析（SAAI）由Cousot和Cousot在[9]和[10]中引入，并进一步发展，例如。[11]。它广泛应用于静态1我们感谢David Monniaux和Nicolas Halbwachs的许多启发性讨论和宝贵的建议。这项工作得到了一些人的支持：法国研究委员会（POST-D-OCTORALFALLOW-）船舶）、System@tic consortium（2电子邮件：eric. cea.fr3电子邮件：leroux@lix.polytechnique.fr4电子邮件：ens.fr5电子邮件：liberti@lix.polytechnique.fr6电子邮件：marinelli@diiga.univpm.it1571-0661 © 2010 Elsevier B.V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.09.00774E. Goubault等人理论计算机科学电子笔记267（2010）73∀ ∈∈对命令式程序的分析，以近似程序的行为，例如根据其可变环境。给定一个程序，构建一个前向收集语义函数，静态地表达给定控制点处的环境如何动态地依赖于其他控制点。这个函数有一个最小不动点（lfp），这是函数可能给出的“最佳”信息。节目计算lfp的基本方法包括增加欠近似序列（依赖于Kleene不动点定理），减少过近似序列（依赖于Tarski不动点定理），或两者结合（依赖于加宽）。 介绍了策略迭代（PI）方法 在[7]中，我们在[1]中进一步发展了区间域，并在[12，2]中推广到其它（关系）域。当语义函数在超范数中是非扩张的时，PI计算lfp，否则计算固定点。在[14]中描述了另一种区间PI方法，后来在[15]中推广到关系域计算语义函数的lfp很自然地是一个优化问题。 数学规划（MP）是一种描述非常一般的优化问题的解决方案的声明性语言[26]。 MP由一组参数（在求解过程之前对问题输入进行编码）、一组决策变量x ∈ Rn（在求解过程之后对问题输出进行编码）、一个目标函数f：Rn → R、一组等式和/或不等式约束g（x）≤ 0（其中g：Rn → Rm）、一组可变边界xL≤ x ≤ xU和一组整数约束jZxjZ[19]组成。MP根据解的性质被分类为：线性程序（LP）、非线性程序（NLP）、混合线性程序（MILP）、混合非线性程序（MINLP），每个类别具有专用的解算法。我们研究以下决策问题。统计分析的最佳解释问题（SAAIP）。给定一个用P语言编写的程序（定义在Sect. 2）它的语义功能（定义在节。3.1）有一个有限的LFP？SAAIP实际上是一个有问题的模式，因为它可以通过用于过度近似具体程序语义的抽象类型来参数化。本文的目的是建立一个强有力的联系，SAAI和MP正式搜索的LFP的MP制定的手段。当语义函数只包含整数凸算术时，MP是一个具有凸目标和约束的MINLP，且在最坏情况下总能在指数时间内得到最优解[4]。对于包括连续和/或非凸算术的语义函数，可以使用空间分支定界（sBB）算法[3]将所得MINLP求解为ε-近似MP标准工具箱还包括几种实用有效的启发式方法[5，21]，它们可以找到非最优但可行的解：在当前设置中，这些对应于不保证最小值的固定点，这可能提供有关程序的有用信息MP的可伸缩性很难被低估：变量关系，例如，简单地产生额外的约束，这些约束可以直接加入到当前的MP公式中。我们通过举例说明在SAAI中使用MP来设置框架，E. Goubault等人理论计算机科学电子笔记267（2010）7375非常经典的设置： 区间整环上的一个整数是一个整数算术。 虽然最近在P[13]中显示了相应SAAIP的特定情况，而我们的MP是通过最坏情况下的指数时间分支定界（BB）算法求解的，但[13]中提出的多项式算法的限制之一是所有交点必须涉及恒定的间隔，而我们的MP不一定在这个意义上受到限制。 换句话说，国会议员自然可以采取 考虑试验条件引起的变量关系。我们归纳地定义了一种命令式编程语言（第2节）及其前向收集区间域语义函数（第3节）。这使得能够对MP进行归纳定义（第4节），并证明语义函数有有限lfp当且仅当MP有解（第5节）。我们还使用著名的CPLEX求解器[17]（Sect.7）。我们注意到MP技术有时用于SAAI [23，8，6，14];更确切地说，LP技术被用作PI型算法到关系域的两个扩展中的运算符[12，15]。然而，据我们所知，通过MP对固定点方程进行建模是新的。2一种基本编程语言编程语言P的定义归纳如下。它的算术表达式涉及C中的常数（包括整数和实数中的常数），V ={v1，...，vn}，常数乘以变量，以及两个变量的加法。P中的程序和I中的指令由（互）归纳法定义。只有四个基本指令，即不做任何事情的指令，经典赋值，if-then-else分支和while循环。E：：=C| V| C E|E+ET：：=C ≤ V |V ≤ C | CgiJ（x）ei<$0）（b）i≤p（ei=0gi（x）giJ（x）ei<$1）(vi) 如果e<$=e，则以固定的pointx终止(vii) 设置e←e，并从步骤ii中重新开始。因此，PI算法在（1）的e-空间上执行局部搜索，而第7节中提到的算法探索整个e-空间，从而总是找到有保证的lfp。 相比之下，PI方法找到有保证的lfp的一个已知的充分条件是语义函数在超范数[7]中应该是非扩张的。7解数学规划给定一个程序P，相关MP的约束CP程序的大小P。这些约束涉及O（P）二进制变量。有2个O（|P|）这些变量的可能赋值。将二进制变量固定到这些分配之一会产生一个LP，它可以在实例大小的多项式时间内求解[18]（LP方法也可以证明不可行性和无界性）。如果对于所有可能的赋值，LP都没有解，这意味着FP的lfp不是有限的。 否则，根据引理5.8，任何有限解 都是FP的后定点。根据定理5.11，lfp是后动点之一，并且根据Tarski [25]，它是其中最小的。用于求解SAAIP的所提出的算法的实际复杂度可能接近其最坏情况的复杂度界限（指数），因此仅用于改进迄今为止SAAIP的最佳已知复杂度界限（没有加宽的Kleene我们可以使用MP方法来推导出一个实际适用的算法来求解稍微修改的SAAIP。通过假设一个任意大的界限，84E. Goubault等人理论计算机科学电子笔记267（2010）73T−| ·|不|不|不|T|变量值（这类似于强制所有盒子都在一个大的预定盒子中，类似于在加宽中所做的），我们能够精确地重新公式化（[20]，第179页）将MP中出现的决策变量之间的所有乘积转换为线性形式，产生一个MILP，我们使用基于BB的求解器CPLEX 11 [17]在具有8GB RAM的2.4GHz Intel XeonCPU上求解。注意，对于大多数实际情况，由于MILP的自动距离缩减技术可以提供相当大的帮助，因此大的界限不需要是任意的。基于上述分析，我们实现了一个C解析器（识别C的一个子集，该子集足够丰富，可以是图灵等价的），它输出相应的MP。我们的测试床由几个（小）C程序7组成，其中整数为整数a，b，c，a，b，c，d，e 我们将我们的结果与PI算法[7]的原型实现所获得的结果进行了比较;在这两种方法中，都设置为区间[5000，5000]。 在表1中，我们报告了：实例名称、代码行、变量总数（长度为n的数组计为n个变量）、用户CPU的秒数、lfp统计信息（所有间隔的宽度之和、间隔数、非间隔的宽度之和）.在所有的测试中，我们得到了宽度等于或小于PI得到的固定点，从而验证了该方法。例如MPPi名称线VarsCPU|·||不||T|CPU|·||不||T|短313230.00825000225202500232523短322030.02270077277702700772777短352230.02320283202803202832028短372530.0084200004200470000470短383530.12345013450103450134501元朗121340.76890000900.00490052952好221740.91680000800.0089000292长313040.64120426124260.064.36e+06436246长419540.4121200001200.008120002122长521640.7721100001100.0041200101210阵列2260.0430013930139----有趣的数组5360.0163000030----功能6270.112101190101190----地铁62349.252581.77e+071766675----表1MP和PI方法的比较。在我们的原型PI实现中，每当程序由于解析限制（数组，函数）而无法分析时，都标记为8结论我们展示了一个数学程序， 一个程序的语义函数与整数的一个递归算法，并继续表明，这产生了一个实际可行的方法计算lfps的程序。通过这个例子，我们希望通过抽象解释来强调标准的抽象编程工具箱在静态分析领域的有用性。未来的工作将扩展MP方法，以处理不同的域7http://www.lix.polytechnique.fr/~ liberti/nsad10-instances.zipE. Goubault等人理论计算机科学电子笔记267（2010）7385（特别是关系域）;我们还将采用其他方法，如策略迭代，作为用于解决问题（1）的标准分支定界方法中的上界过程。引用[1] Adje，A.，S. Gaubert和E. Goubault，Computing the smallest fixed point of nonexpansive mappingsarising in game theory and static analysis of programs（2008），发表于MTNS 2008，arXiv.org：0806.1160。[2] 我 是 A. ， S.Gau bert 和 E. Goubault ， 耦 合 policyiterationwithsemi-definiterelaxationtocalculateaccurate numerical invariants in static analysis，in：A. Gordon，editor，European Symposiumon Programming（2010），pp.23比42[3] 贝洛蒂山口，J. 利湖，澳-地 Li berti，F. 玛戈和达。 Wüachter，非凸MINLP的B ranching和bounds收紧技术，优化方法和软件24（2009），pp. 597-634[4] Bonami，P.，L. Biegler，A. Conn，G. 科尔努埃约斯岛格罗斯曼角，澳-地Laird，J. Lee，A. L o di，F. 玛戈特N. S awaya和A. Wüachter，一种用于凸混合整数非线性预处理的算法框架，技术报告RC23771，IBMCorporation（2005）。[5] Bonami，P.，G. Cor nu′ejols，A. L odi和F. Margot，Afabilitypumpformix eintegernonlinearprograms，Mathematical Programming 119（2009）.[6] 上校，M S. San karanar ayanan和H. Sipma，用非线性不变解方法求线性不变关系，在：W. Hunt，编辑，计算机辅助验证，LNCS2725（2003），pp.420-432[7] Costan ， A. ， S. Gaubert ， E. Goubault ， M. Martel 和 S. Putot ， A policy iteration algorithm forcomputing fixed points in static analysis of programs，in：K. Etessami和S. Rajamani，编辑，计算机辅助验证，LNCS3576（2005），pp.462-475[8] Cousot，P.，通过参数抽象、拉格朗日松弛和半有限规划证明程序不变性和终止性，在：R。Cousot，编辑，验证，模型检查和抽象解释，LNCS3385（2005），pp.十七比十九[9] Cousot ， P. and R. Cousot ， Static determination of dynamic properties of programs ， in ：Proceedings of the Second International Symposium on Programming（1976），pp. 106-130.[10] 库 索 山 口 和 R.Cousot ， Abstract interpretation ： A unified lattice model for static analysis ofprograms by construction of approximations of fixed points，Principles of Programming Languages 4（1977）.238-252。[11] 库索山口和R.Cousot，抽象解释框架，逻辑与计算杂志2（1992），pp. 511-547[12] Gaubert，S.，E. Goubault，A. Taly和S. Zennou，通过关系域上的策略迭代进行静态分析，在：R。D.Nicola，editor，European Symposium on Programming，LNCS4421（2007）. 237-252.[13] Gawlitza，T.，J. Leroux，J. Reineke，H. Seidl，G. Sutre和R.王文，多项式精细区间分析，载于：S. Albers ， H. Alt和S. Nüaher ， editors， FestschriftMehlhor n， LectureNotesinComputer Science 5760（2009），pp. 422-437.[14] Gawlitza，T.和H. Seidl，Precise fixpoint computation through strategy iteration，in：R. D. Nicola，editor，European Symposium on Programming，LNCS4421（2007）.三百到三百一十五[15] Gawlitza，T.和H.Seidl，通过策略迭代实现精确的关系不变量，在：J。Duparc和T. Henzinger，editors，Computer Science Logic，2007，pp. 23比40[16] Halbwachs，N.，Y.-- E. Proy和P. Roumano，使用线性关系分析的实时系统验证，系统设计中的形式化方法11（1997），pp.157-185[17] ZUAG，Gentilly，France（2008）.[18] Karmarkar，N.，一个新的多项式时间线性规划算法，Combinatorica4（1984），pp。373-395.[19] 利伯蒂湖数学规划中的重构：定义与系统学，RAIRO-RO86E. Goubault等人理论计算机科学电子笔记267（2010）7343（2009），pp. 55比86E. Goubault等人理论计算机科学电子笔记267（2010）7387≤∪W≤{ 联系我们←←[20] 利伯蒂湖S. Ca fieri和F. 数学规划中的重构：一种计算方法，在：A。Abraham，A. E. Hassanien，P.Siarry和A. Engelbrecht，editors，Foundations of Computational Intelligence Vol. 3，number 203 inStudies in Computational Intelligence，Springer，Berlin，2009 pp. 153-234。[21] 李伯提，L.，N. Mladen ov ic和G. Nannicini，Agood