This tutorial is about infra-structures for general-purpose interprocedural analyses. It consists of two parts. The first part, following the lines of [2], argues that side-effecting constraint systems may serve as kind of swiss army knife for specifying analyses, while the second part provides an overview on solving techniques for such systems. Side-effecting constraint systems were originally introduced for the analysis of multi-threaded code by Müller-Olm, Seidl and Vene in [41]. Here, we explain how this formalism provides a unified framework for realizing efficient interprocedural analyses of programs, possibly with dynamic function calls, where the amount of context-sensitivity can be tweaked and where the context-sensitive analyses of local properties can be combined with flow-insensitive analyses of global properties, e.g., about the heap. One infrastructure realizing this intermediate format, is the analyzer generator GOBLINT, which we use to practically evaluate this approach on real-world examples.

The second part, following [3], reports on techniques for solving side-effecting constraint systems. One major issue here is that 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 to accelerate fixpoint iteration by means of widening and narrowing [10, 14]. The strict separation into a widening phase followed by a narrowing phase, 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 constraint systems corresponding to context-sensitive interprocedural analyses, possibly combining context-sensitive analysis of local information with flow-insensitive analysis of globals. 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 and priorities are respected by side-effects.