Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LoopSCC: Towards Summarizing Multi-branch Loops within Determinate Cycles

Kai Zhu, Chenkai Guo, Kuihao Yan, Xiaoqi Jia, Haichao Du, Qingjia Huang, Yamin Xie, Jing Tang

TL;DR

This paper proposes LoopSCC, a novel loop summarization technique, to achieve concrete semantic interpretation on complex loop and achieves a 100% interpretation accuracy on public common-used benchmark.

Abstract

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: Towards Summarizing Multi-branch Loops within Determinate Cycles

TL;DR

This paper proposes LoopSCC, a novel loop summarization technique, to achieve concrete semantic interpretation on complex loop and achieves a 100% interpretation accuracy on public common-used benchmark.

Abstract

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.

Paper Structure

This paper contains 35 sections, 2 theorems, 19 figures, 2 tables, 3 algorithms.

Table of Contents

  1. Introduction
  2. Motivation
  3. Preliminaries
  4. SCC-based Loop Summarization
  5. Overview
  6. SCC-based Flow Analysis
  7. Transformation of Nested Loop
  8. Construction of CSG
  9. Loop Summarization
  10. Summarization for 1-order SCC
  11. Summarization for High-order SCC
  12. Evaluation
  13. RQ1: Accuracy of LoopSCC.
  14. Benchmark
  15. Experimental Settings
  16. ...and 20 more sections

Key Result

Theorem 1

If the oscillatory interval $O$ of a high-order SCC, $O$ contains all the J-Intervals and can be divided into a finite number of periodic subintervals,, then the summarization of $scc$ can be converted into a summarization of low-order SCC.

Figures (19)

  • Figure 1: Acyclic Multi-branch Loop
  • Figure 2: Cyclic Multi-branch Loop
  • Figure 3: Inductiveness Trap
  • Figure 4: Connected Cycles
  • Figure 6:
  • ...and 14 more figures

Theorems & Definitions (12)

  • Definition 1
  • Definition 2
  • Definition 3
  • Definition 4
  • Definition 5
  • Definition 6
  • Definition 7
  • Definition 8
  • Definition 9
  • Definition 10
  • ...and 2 more