A Fix-Point Characterization of Herbrand Equivalence of Expressions in Data Flow Frameworks

摘要

Computing Herbrand equivalences of terms in data flow frameworks is well studied in program analysis. While algorithms use iterative fix-point computation on some abstract lattice of expressions relevant to the flow graph, the definition of Herbrand equivalences is based on an equivalence over all program paths formulation, on the (infinite) set of all expressions. The aim of this paper is to develop a lattice theoretic fix-point formulation of Herbrand equivalence on a concrete lattice defined over the set of all terms constructible from variables, constants and operators of a program. This new formulation makes explicit the underlying lattice framework as well as the monotone function involved in computing Herbrand equivalences. We introduce the notion of Herbrand congruence and define an (infinite) concrete lattice of Herbrand congruences. Herbrand equivalence is defined as the maximum fix-point of a composite transfer function defined over an appropriate product lattice of the above concrete lattice. We then reformulate the traditional meet over all paths definition in our lattice theoretic framework, and prove that the maximum fix-point (MFP) and the meet-over-all-paths (MOP) formulations coincide as expected.