Regular Path Clauses and Their Application in Solving Loops

TL;DR

This paper introduces a novel method using regular path expressions and loop counters to transform complex loops into simpler forms, enabling more effective recurrence solving for program analysis.

Contribution

It proposes a new transformation technique that simplifies multi-path and multi-argument recurrences, improving the ability to derive precise loop properties.

Findings

Transforms multi-path loops into single-path loops

Enables solving previously unsolvable recurrences

Achieves more precise analysis results

Abstract

A well-established approach to reasoning about loops during program analysis is to capture the effect of a loop by extracting recurrences from the loop; these express relationships between the values of variables, or program properties such as cost, on successive loop iterations. Recurrence solvers are capable of computing closed forms for some recurrences, thus deriving precise relationships capturing the complete loop execution. However, many recurrences extracted from loops cannot be solved, due to their having multiple recursive cases or multiple arguments. In the literature, several techniques for approximating the solution of unsolvable recurrences have been proposed. The approach presented in this paper is to define transformations based on regular path expressions and loop counters that (i) transform multi-path loops to single-path loops, giving rise to recurrences with a single recursive case, and (ii) transform multi-argument recurrences to single-argument recurrences, thus enabling the use of recurrence solvers on the transformed recurrences. Using this approach, precise solutions can sometimes be obtained that are not obtained by approximation methods.