Three improvements to the top-down solver

The local solver TD is a generic fixpoint engine which explores a given system of equations on demand. It has been successfully applied to the interprocedural analysis of procedural languages. The solver TD gains efficiency by detecting variable dependencies on the fly. This algorithm has been recently extended to deal with widening and narrowing as well. In particular, it has been equipped with an automatic detection of widening and narrowing points. That version, however, is only guaranteed to terminate under two conditions: only finitely many variables are encountered, and all right-hand sides are monotonic. While the first condition is unavoidable, the second limits the applicability of the solver. Another limitation is that the solver maintains the current abstract values of all encountered variables in one data-structure — thus prohibiting interprocedural analyses to scale to larger programs.

In the present paper, we therefore extend the top-down solver TD in three ways. First, we indicate how the restriction to monotonic right-hand sides can be lifted. Then we show how the solver can be tuned to store abstract values only when it turns out to be inevitable. Finally, we also show how the solver can be extended to side-effecting equation systems, which have successfully been applied to seamlessly combine context-sensitive with flow-insensitive analyses.