Program Analyses using Newton's Method
Thomas Reps
Esparza et al. generalized Newton's method—a numerical-analysis
algorithm for finding roots of real-valued functions—to a method
for finding fixed-points of systems of equations over semirings. Their
method provides a new way to solve interprocedural dataflow-analysis
problems. As in its real-valued counterpart, each iteration of their
method solves a simpler ``linearized'' problem.
Because essentially all fast iterative numerical methods are forms of
Newton's method, this advance is exciting because it may provide the
key to creating faster program-analysis algorithms. However, there is
an important difference between the dataflow-analysis and
numerical-analysis contexts: when Newton's method is used in numerical
problems, commutativity of multiplication is relied on to rearrange an
expression of the form ``a * Y * b + c * Y * d'' into ``(a * b + c * d) * Y.''
Equations with such expressions correspond to path problems described
by regular languages. In contrast, when Newton's method is used for
interprocedural dataflow analysis, the ``multiplication'' operation
involves function composition, and hence is non-commutative:
``a * Y * b + c * Y * d'' cannot be rearranged into ``(a * b + c * d) * Y.''
Equations with the former expressions correspond to path problems
described by linear context-free languages (LCFLs).
The invited talk that this paper accompanies presented a method that
we developed in 2015 for solving the LCFL sub-problems produced during
successive rounds of Newton's method.
It uses some algebraic slight-of-hand to turn a class of LCFL path
problems into regular-language path problems.
This result is surprising because a reasonable sanity
check---formal-language theory---suggests that it should be
impossible:
after all, the LCFL languages are a strict superset of the regular
languages.
The talk summarized several concepts and prior results on which
that result is based.
The method described applies to predicate abstraction, on which most of today's
software model checkers rely, as well as to other abstract domains
used in program analysis.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)
University of Wisconsin