论文分享_08_02

通过路径依赖分析计算循环不变式

摘要

       对于程序分析来说，循环是非常难以处理的结构，特别是多种路径相互交错的复杂循环。
       文章首先基于在循环条件中的变量的更新和循环路径的执行顺序对多路径的循环进行分类，进而来理解循环的复杂性。
       之后，文章提出分析框架Proteus。该框架把循环和我们感兴趣的变量集合作为输入，然后通过分析，可以得到关于这些变量经过循环之后的变化情况的摘要。文章主要的贡献是利用路径依赖自动机(path dependency automaton, PDA)来捕获路径之间的执行依赖。然后利用DFS遍历PDA来对所有可行的执行路径的影响进行摘要。

三大应用：

  1. 能分析出比现有的循环边界分析技术更精确的循环边界
  2. 显著优于最先进的循环验证工具
  3. 在1秒钟内对非常深的循环产生测试样例，KLEE或者Pex面对这样的循环时可能会花费更多时间或者失败。

一、概览

1、相关定义

循环的流图，flowgraph of the loop
循环路径，loop path
归纳变量，induction variable
条件分类
循环执行，loop execution
循环分类，Loop classification
路径依赖自动机，Path Dependency Automaton

2、PDA构建算法

三、几种循环摘要

1、分离形式的循环摘要

2、对Type1型循环的摘要

3、环形摘要

4、对Type2,3,4类型的摘要

四、评价

五、结论