Tighter Loop Bound Analysis (Technical report)

TL;DR

This paper introduces a new algorithm for computing tight upper bounds on instruction executions in programs, enabling more accurate loop bounds and outperforming existing tools in experimental evaluations.

Contribution

The paper presents a novel algorithm that produces tighter instruction and loop bounds, improving upon current loop bound analysis methods.

Findings

Algorithm often produces tighter bounds than existing tools

Experimental results validate the effectiveness of the approach

Bounds are expressed as functions of input values

Abstract

We present a new algorithm for computing upper bounds on the number of executions of each program instruction during any single program run. The upper bounds are expressed as functions of program input values. The algorithm is primarily designed to produce bounds that are relatively tight, i.e. not unnecessarily blown up. The upper bounds for instructions allow us to infer loop bounds, i.e.~upper bounds on the number of loop iterations. Experimental results show that the algorithm implemented in a prototype tool Looperman often produces tighter bounds than current tools for loop bound analysis.