含有析取语义循环的不变式生成改进方法  

Improving Invariant Generation for Loops Containing Disjunctive Semantics

作　　者：潘建东[1,2] 陈立前[3] 黄达明[1,2] 孙浩[1,2] 曾庆凯[1,2] 

机构地区：[1]计算机软件新技术国家重点实验室(南京大学),江苏南京210023 [2]南京大学计算机科学与技术系,江苏南京210023 [3]并行与分布处理国防科技重点实验室(国防科学技术大学计算机学院),湖南长沙410073

出　　处：《软件学报》2016年第7期1741-1756,共16页Journal of Software

基　　金：国家自然科学基金(61170070;61572248;61431008;61321491);国家科技支撑计划(2012BAK26B01);国家高技术研究发展计划(863)(2011AA1A202)~~

摘　　要：抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.interpretation provides a general framework to generate program invariants automatically. However, most existing numerical abstract domains under this framework can only express constraint sets that are geometrically convex. Therefore, using convex abstract domains to analyze special program structures involving disjunctive semantics（whose constraint sets are non-convex） may lead to imprecise results. This paper presents a novel approach based on loop decomposition and deduction to improve invariant generation for loop structures with explicit and implicit disjunctive semantics. This approach can alleviate the problem of great semantic loss during abstract interpretation of loop structures with disjunctive semantics. Compared with existing approaches, experimental results show that the presented approach can generate more precise invariants for loop structures involving disjunctive semantics, which is also helpful for reasoning about certain security properties.

关 键 词：抽象解释 抽象域 不变式 析取语义 循环分解 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]