How to Combine Widening and Narrowing for Non-monotonic Systems of Equations

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 widen-ing 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, possi-bly 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 it-eration, local, and side-effecting solving algorithms for the com-bined operator and prove that the resulting solvers always return sound results and are guaranteed to terminate for monotonic sys-tems whenever only finitely many unknowns (constraint variables) are encountered