Interprocedural Dataflow Analysis over Weight Domains with Infinite Descending Chains

TL;DR

This paper introduces an efficient algorithm for fixed-point analysis over semirings with infinite descending chains, extending previous methods limited to bounded semirings, with applications in interprocedural dataflow analysis.

Contribution

It presents a novel approach to fixed-point equations over semirings without boundedness restrictions, applicable to interprocedural dataflow analysis.

Findings

Algorithm detects stabilization of Kleene's iterations in infinite chains

Application to weighted pushdown automata reachability problems

Demonstrated usability through multiple applications

Abstract

We study generalized fixed-point equations over idempotent semirings and provide an efficient algorithm for the detection whether a sequence of Kleene's iterations stabilizes after a finite number of steps. Previously known approaches considered only bounded semirings where there are no infinite descending chains. The main novelty of our work is that we deal with semirings without the boundedness restriction. Our study is motivated by several applications from interprocedural dataflow analysis. We demonstrate how the reachability problem for weighted pushdown automata can be reduced to solving equations in the framework mentioned above and we describe a few applications to demonstrate its usability.