Analyzing programs with loops is a challenging task, suffering from potential issues such as indeterminate number of iterations and exponential growth of control flow complexity. Loop summarization, as a static analysis method for concrete semantic interpretation, receives increasing focuses. It produces symbolic expressions semantically equivalent to the loop program. However, current loop summarization methods are only suitable for single-branch loops or multi-branch loops with simple cycles, without supporting complex loops with irregular branch-to-branch transitions. In this paper, we proposed LoopSCC, a novel loop summarization technique, to achieve concrete semantic interpretation on complex loop. LoopSCC analyzes the control flow at the granularity of single-loop-path and applies the strongly connected components (SCC for short) for contraction and simplification, resulting in the contracted single-loop-path graph (CSG for short). Based on the control flow information provided by the CSG, we can convert the loop summary into a combination of SCC summaries. When an SCC contains irregular branch-to-branch transitions, we propose to explore a convergent range to identify the determinate cycles of different execution paths, referred as oscillatory interval. The loop summarization composed of both iteration conditions and execution operations can eventually be derived recursively. Extensive experiments compared to six state-of-the-art loop interpretation methods are conducted to evaluate the effectiveness of LoopSCC. From the results, LoopSCC outperforms comparative methods in both interpretation accuracy and application effectiveness. Especially, LoopSCC achieves a 100% interpretation accuracy on public common-used benchmark. A systematical study for loop properties on three large-scale programs illustrates that LoopSCC presents outstanding scalability for real-world loop programs.

翻译：分析包含循环的程序是一项具有挑战性的任务，常面临迭代次数不确定、控制流复杂度指数级增长等潜在问题。循环摘要作为一种面向具体语义解释的静态分析方法，正受到越来越多的关注。它能生成与循环程序语义等价的符号表达式。然而，现有的循环摘要方法仅适用于单分支循环或具有简单周期的多分支循环，无法支持存在不规则分支间转移的复杂循环。本文提出了一种新颖的循环摘要技术LoopSCC，以实现对复杂循环的具体语义解释。LoopSCC在单循环路径粒度上分析控制流，并应用强连通分量（简称SCC）进行收缩与简化，从而得到收缩后的单循环路径图（简称CSG）。基于CSG提供的控制流信息，我们可以将循环摘要转化为SCC摘要的组合。当某个SCC包含不规则的分支间转移时，我们提出通过探索收敛范围来识别不同执行路径的确定周期，称为振荡区间。最终可通过递归方式推导出由迭代条件和执行操作共同构成的循环摘要。我们进行了大量实验，与六种先进的循环解释方法进行比较，以评估LoopSCC的有效性。结果表明，LoopSCC在解释准确性和应用效果上均优于对比方法。特别是在公开常用基准测试集上，LoopSCC实现了100%的解释准确率。对三个大规模程序中循环特性的系统性研究表明，LoopSCC对实际循环程序展现出卓越的可扩展性。