Differential Evaluation of Fixpoints of Non-distributive Functions

摘要

We present a differential fixpoint computation method for program analyses based on abstract interpretation. An analysis of a program based on abstract interpretation can be expressed using a monotonic increasing function and a fixpoint of the function becomes an analysis result. To compute a fix-point, the function is applied repeatedly until the results become stable. This brings redundant computation because new results always include the former results. Differential methods try to avoid such redundancy by computing only the increment of each function application. Compared with other differential fixpoint evaluation methods, our method can deal with non-distributive functions which often occur in practical program analyses. To compute increments for non-distributive functions, we adapt an indirect way of using a differential evaluation rule for expressions which form function bodies. We have designed a differential worklist algorithm and applied the algorithm to implement an alias and constant propagation analysis. Experiments show that our method can avoid much redundant computation.