循环是一个多路径间不断迭代的结构，对循环进行分类以寻找可以解决的方案。 对循环的终止性分析，是寻找秩函数 ranking function，来判断循环的终止性，这个函数的寻找和验证很复杂，需要很多时间。

1, 多路径交错执行，变量在每条路径中变化不同，从而导致在多路径交错执行时，对该变量的分析变得困难。

现有方法是将多路径循环转换为多个单路径循环，然而当多路径交错迭代时，不能被转换为有限的单路径循环。

目前大部分方法都无法处理多路径循环。

2，变量不可归纳。

循环总结基于变量的可归纳性来计算循环结束后变量的结果。 当变量不可计算时，无法对其进行归纳。

变量在每条路径都可以归纳，但由于多路径的交错迭代使得其不可归纳。

目前大部分工作职能处理变量在循环每次迭代中变化为常量的情况。

3，终止性判定。

循环总结计算出输入与输出之间的关系，然而循环不终止时，则没有输出。

因此判定循环终止性是循环分析和与总结的基础问题。

终止性问题是一个经典的停机问题，其不可判定。

在循环分析时，如何对终止性进行快速判定是一个主要挑战。

4， 循环嵌套

提高分析的复杂度。

1）由于内外层循环嵌套，使得外层循环包含多路径，并且多路径间的交错执行复杂。 2）内外层循环的交错执行，使得外部循环的变量通常不可归纳。

当前的工作主要集中于非嵌套循环的分析，对嵌套循环无法处理或者得到的结果不准确。

---

循环的每一次迭代时循环内多个if-else分支的组合，通过cfg抽取循环内不同的迭代模式得到循环的可迭代路径。

自动机 path dependency automation 的每个状态对应循环的一条路径，状态间的转移表示路径间的依赖关系。

需要把循环进行分类，多路径交错执行方式和变量在每条路径的更新规律 是影响 迭代循环结果的两个主要因素。

分成4类。

disjunctive loop summary. 1) 识别可归纳变量 对每一条路径中这个变量计算在该路径执行后的结果

2）PDA中环的合并，将有周期的环合并成一个状态，从而将环约减少。

3）不可归纳变量的处理。 通过抽象和近似的策略将部分不可归纳变量转换成可归纳变量。

对多路径字符串循环，提出 conjunctive loop summary. 基于字符串求解器。

1）从CFG中得到循环的多条路径，每条路径将遍历字符串的部分元素。

2）对每条路径计算字符串索引变量与其他整型变量的关系，推断该路径所遍历的字符串范围。

3）基于每条路径上字符串约束条件以及范围生成相应的字符串约束条件。

循环终止性分析： 1）对循环每一条路径进行终止性分析

2）构建PDA以分析路径间的依赖关系

3）基于PDA对整个循环的终止性进行分析