A Methodology for Avoiding Accumulated Imprecision in Program Analysis

We identify a phenomenon, called accumulated imprecision , that has escaped notice but is largely responsible for the difficu lty in design of accurate program analyses. Accumulated imprecis ion occurs because program analyses compute an abstract property aft every execution step and thus often lose track of crucial inf ormation during sequences of steps. For instance, a program that dest ructively swaps the children of a binary tree t preserves the property that t is a tree. However, there is an intermediate state during the swap in whicht’s left and right links point to the same subtree, and in that statet is not a tree. This intermediate state causes most program analyses to lose track of the shape of t. To address this problem, we introduce a language TR of transfer relations, written as conditional parallel assignments, for describing changes to the store. We show that TR is expressive enough to describe a wide variety of source-language features and i s closed under composition via an algorithm . To use transfer relations, the analysis designer first describes an operational semant ics of the source language with TR terms and then defines an abstraction of TR for the properties of interest. An analysis algorithm perfo rms a semantics-directed translation of a source program into TR, selectively applies to combine multiple execution steps and thus reduce accumulated imprecision, and applies a program anal ysis to the resulting multi-stepTR terms.