The Calculus of Abstract Dependencies

By: Isabella Mastroeni and Damiano Zanardini

Damiano Zanardini
Fac. de Informatica
Univ. Politecnica de Madrid
damiano@clip.dia.fi.upm.es

Isabella Mastroeni
Dip. di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2
I-37134 Verona, Italy
mastroeni@sci.univr.it

Abstract:

We propose an algorithm to over-approximate data dependencies with respect to abstract properties of data, described as abstract domains. To the best of our knowledge, no other explicit calculi of abstract dependencies exist in the literature. In our setting, relevant variables are those which may affect abstract properties of expressions they occur in. Unlike its non-abstracted counterpart, the calculus of abstract dependencies is forced to rely on semantics: the syntactic occurrence of a variable is not sufficient to decide whether an expression depends on it. The algorithm computes the set of relevant variables for an expression, w.r.t. an abstract domain; it is proved to be sound, that is, the computed set is an over approximation of truly (semantically) relevant variables. We exploit static analysis techniques, together with our knowledge of the structure of expressions and domains, in order to improve efficiency. Applications to program slicing (w.r.t. abstract properties) and to abstract non-interference are discussed; moreover, we propose a domain transformer which approximates the most precise domain ruling out a given set of dependencies.