资源描述：
《多面体抽象域的整数实现方法及其在程序分析中的应用》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、多面体抽象域的整数实现方法及其在程序分析中的应用//.paper.edu.cn-1-中国科技论文在线多面体抽象域的整数实现方法及其在程序分析中的应用田楠，陈立前，王戟**作者简介：田楠（1988-），男，硕士研究生，程序分析通信联系人：王戟（1969-），男，教授，程序分析（国防科学技术大学计算机学院,长沙410073）5摘要：抽象解释理论为静态程序分析提供了一个通用框架.抽象域是该框架下的核心.多面体抽象域可用来产生线性不等式,是目前表达能力最强、应用最广泛的数值抽象域之一.现有的多面体抽象域实现一般采用多精度有理数,在实际应用中
2、可扩展性方面受到限制.本文采用多面体抽象域基于约束的表示方法,给出了多面体抽象域的一种基于机器整数的实现方法.10为了提高基于机器整数实现的多面体抽象域的可扩展性,本文提出了一些策略来限制约束系数的大小和约束的个数;另一方面,针对目标程序是整数程序的情况,本文根据变量的整数特点,提出了一些优化方法提高分析精度.实验表明,与基于多精度有理数实现的多面体抽象域相比,基于机器整数实现的多面体抽象域计算效率更高,并且更适合整数程序分析。关键词：抽象解释；机器整数；多面体抽象域15中图分类号：V19AMachine-IntegerImplem
3、entationforPolyhedraAbstractDomainanditsApplicationinProgramAnalysisTIANNan,CHENLiqian,WANGJi20(SchoolofComputerScience,NationalUniversityofDefenseTechnology,ChangSha410073)Abstract:Abstractinterpretationprovidesageneralframeworkforstaticprogramanalysis.Theabstractdoma
4、inisthecoreoftheframework.Polyhedronabstractdomainwhichisusedtogeneratelinearinvariantsisoneofthemostexpressiveandwidelyusedabstractdomains.Mostexistingimplementationsforpolyhedronabstractdomainwereusinggeneralmulti-precision25rational,andwerelimitedinscalabilityinprac
5、ticalapplications.Inthispaper,basedontheconstraint-basedrepresentation,wepresentedamachine-integerimplementationforpolyhedrondomain.Moreover,inordertoimprovethescalability,weproposesomestrategiestolimitthesizeoftheconstraintcoefficientsandthenumberofconstraints.Ontheot
6、herhand,whentheprogramtobeanalyzedisanintegerprogram,wepresentssomestrategiestoimproveprecision.30Experimentsshowthat,comparedwithmulti-precisionrationalimplementations,thepolyhedronabstractdomainbasedonmachineintegerismoreefficientandfitsmoretoanalyzeintegerprogram.Ke
7、ywords:abstractinterpretation;machine-integer;polyhedrondomain350引言抽象解释由P.Cousot和R.Cousot于1977年提出,是一种对程序语义进行可靠近似（或抽象）的通用理论[1][2].抽象解释的本质是在计算效率和计算精度之间进行折衷,通过牺牲部分计算精度来取得计算的可行性和一定的效率.目前,抽象解释在软硬件系统分析与验证领域取得了广泛的应用,其应用领域涉及静态分析、程序转换、模型检验、语法分析与解析等.40抽象解释理论为静态程序分析提供了一个通用的框架,用于构
8、造和逼近程序不动点.其中抽象解释的一个典型应用是数值程序分析,旨在发现程序中某个程序点的数值不变式,即每次程序执行均满足的数值变量间的关系.这些数值不变式可用于分析程序中是否有除零错、数//.paper.edu.cn-2-中国科技论文
