TY - GEN

T1 - How to combine widening and narrowing for non-monotonic systems of equations

AU - Apinis, Kalmer

AU - Seidl, Helmut

AU - Vojdani, Vesal

PY - 2013

Y1 - 2013

N2 - Non-trivial analysis problems require complete lattices with infinite ascending and descending chains. In order to compute reasonably precise post-fixpoints of the resulting systems of equations, Cousot and Cousot have suggested accelerated fixpoint iteration by means of widening and narrowing [6, 7]. The strict separation into phases, however, may unnecessarily give up precision that cannot be recovered later. While widening is also applicable if equations are non-monotonic, this is no longer the case for narrowing. A narrowing iteration to improve a given post-fixpoint, additionally, must assume that all right-hand sides are monotonic. The latter assumption, though, is not met in presence of widening. It is also not met by equation systems corresponding to context-sensitive interprocedural analysis, possibly combining context-sensitive analysis of local information with flow-insensitive analysis of globals [1]. As a remedy, we present a novel operator that combines a given widening operator with a given narrowing operator. We present adapted versions of round-robin as well as of worklist iteration, local, and side-effecting solving algorithms for the combined operator and prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns (constraint variables) are encountered.

AB - Non-trivial analysis problems require complete lattices with infinite ascending and descending chains. In order to compute reasonably precise post-fixpoints of the resulting systems of equations, Cousot and Cousot have suggested accelerated fixpoint iteration by means of widening and narrowing [6, 7]. The strict separation into phases, however, may unnecessarily give up precision that cannot be recovered later. While widening is also applicable if equations are non-monotonic, this is no longer the case for narrowing. A narrowing iteration to improve a given post-fixpoint, additionally, must assume that all right-hand sides are monotonic. The latter assumption, though, is not met in presence of widening. It is also not met by equation systems corresponding to context-sensitive interprocedural analysis, possibly combining context-sensitive analysis of local information with flow-insensitive analysis of globals [1]. As a remedy, we present a novel operator that combines a given widening operator with a given narrowing operator. We present adapted versions of round-robin as well as of worklist iteration, local, and side-effecting solving algorithms for the combined operator and prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic systems whenever only finitely many unknowns (constraint variables) are encountered.

KW - Constraint Solving

KW - Fixpoint Iteration

KW - Static Program Analysis

UR - http://www.scopus.com/inward/record.url?scp=84883119385&partnerID=8YFLogxK

U2 - 10.1145/2462156.2462190

DO - 10.1145/2462156.2462190

M3 - Conference contribution

AN - SCOPUS:84883119385

SN - 9781450320146

T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

SP - 377

EP - 386

BT - PLDI 2013 - Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation

T2 - 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013

Y2 - 16 June 2013 through 19 June 2013

ER -