| Autor: |
Babu, Jasine, Krishnan, K. Murali, Paleri, Vineeth |
| Rok vydání: |
2017 |
| Předmět: |
|
| Druh dokumentu: |
Working Paper |
| Popis: |
The problem of determining Herbrand equivalence of terms at each program point in a data flow framework is a central and well studied question in program analysis. Most of the well-known algorithms for the computation of Herbrand equivalence in data flow frameworks proceed via iterative fix-point computation on some abstract lattice of short expressions relevant to the given flow graph. However the mathematical definition of Herbrand equivalence is based on a meet over all path characterization over the (infinite) set of all possible expressions. The aim of this paper is to develop a lattice theoretic fix-point formulation of Herbrand equivalence on the (infinite) concrete lattice defined over the set of all terms constructible from variables, constants and operators of a program. The present characterization uses an axiomatic formulation of the notion of Herbrand congruence and defines the (infinite) concrete lattice of Herbrand congruences. Transfer functions and non-deterministic assignments are formulated as monotone functions over this concrete lattice. 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. A re-formulation of the classical meet-over-all-paths definition of Herbrand equivalence in the above lattice theoretic framework is also presented and is proven to be equivalent to the new lattice theoretic fix-point characterization. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
