Precise Widening Operators for Convex Polyhedra

TitlePrecise Widening Operators for Convex Polyhedra
Publication TypeJournal Article
Year of Publication2005
AuthorsBagnara R, Hill PM, Ricci E, Zaffanella E
JournalScience of Computer Programming
Volume58
Pagination28–56
ISSN0167-6423
Keywordsabstract interpretation, convex polyhedra, numerical properties, software verification, static analysis, widening operators
Abstract

In the context of static analysis via abstract interpretation, convex polyhedra constitute the most used abstract domain among those capturing numerical relational information. Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating the convergence of fixpoint computations. Widening operators provide a simple and general characterization for such mechanisms. For the domain of convex polyhedra, the original widening operator proposed by Cousot and Halbwachs amply deserves the name of standard widening since most analysis and verification tools that employ convex polyhedra also employ that operator. Nonetheless, there is an unfulfilled demand for more precise widening operators. In this paper, after a formal introduction to the standard widening where we clarify some aspects that are often overlooked, we embark on the challenging task of improving on it. We present a framework for the systematic definition of new widening operators that are never less precise than a given widening. The framework is then instantiated on the domain of convex polyhedra so as to obtain a new widening operator that improves on the standard widening by combining several heuristics. A preliminary experimental evaluation has yielded promising results. We also suggest an improvement to the well-known widening delay technique that allows to gain precision while preserving its overall simplicity.

DOI10.1016/j.scico.2005.02.003
File attachments: 

A Correct, Precise and Efficient Integration of Set-Sharing, Freeness and Linearity for the Analysis of Finite and Rational Tree Languages

TitleA Correct, Precise and Efficient Integration of Set-Sharing, Freeness and Linearity for the Analysis of Finite and Rational Tree Languages
Publication TypeJournal Article
Year of Publication2004
AuthorsHill PM, Zaffanella E, Bagnara R
JournalTheory and Practice of Logic Programming
Volume4
Pagination289–323
ISSN1471-0684
Keywordsabstract interpretation, abstract unification, freeness, linearity, logic programming, rational trees, set-sharing, software verification, static analysis
Abstract

It is well-known that freeness and linearity information positively interact with aliasing information, allowing both the precision and the efficiency of the sharing analysis of logic programs to be improved. In this paper we present a novel combination of set-sharing with freeness and linearity information, which is characterized by an improved abstract unification operator. We provide a new abstraction function and prove the correctness of the analysis for both the finite tree and the rational tree cases. Moreover, we show that the same notion of redundant information as identified in \cite{BagnaraHZ02TCS,ZaffanellaHB02TPLP} also applies to this abstract domain combination: this allows for the implementation of an abstract unification operator running in polynomial time and achieving the same precision on all the considered observable properties.

DOI10.1017/S1471068401001351
File attachments: 

Finite-Tree Analysis for Constraint Logic-Based Languages

TitleFinite-Tree Analysis for Constraint Logic-Based Languages
Publication TypeJournal Article
Year of Publication2004
AuthorsBagnara R, Gori R, Hill PM, Zaffanella E
JournalInformation and Computation
Volume193
Pagination84-116
ISSN0890-5401
Keywordsabstract interpretation, logic programming, occurs-check, rational unification, software verification, static analysis
Abstract

Logic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the safe omission of the occurs-check) and increased expressivity (cyclic terms can provide very efficient representations of grammars and other useful objects). Unfortunately, the use of infinite rational trees has problems. For instance, many of the built-in and library predicates are ill-defined for such trees and need to be supplemented by run-time checks whose cost may be significant. Moreover, some widely-used program analysis and manipulation techniques are correct only for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of the program variables (the finite variables) that, at the program points of interest, will always be bound to finite terms. For these reasons, we propose here a new data-flow analysis, based on abstract interpretation, that captures such information. We present a parametric domain where a simple component for recording finite variables is coupled, in the style of the open product construction of Cortesi et al., with a generic domain (the parameter of the construction) providing sharing information. The sharing domain is abstractly specified so as to guarantee the correctness of the combined domain and the generality of the approach. This finite-tree analysis domain is further enhanced by coupling it with a domain of Boolean functions, called finite-tree dependencies, that precisely captures how the finiteness of some variables influences the finiteness of other variables. We also summarize our experimental results showing how finite-tree analysis, enhanced with finite-tree dependencies, is a practical means of obtaining precise finiteness information.

DOI10.1016/j.ic.2004.04.005
File attachments: 

Checking and Bounding the Solutions of Some Recurrence Relations

TitleChecking and Bounding the Solutions of Some Recurrence Relations
Publication TypeMiscellaneous
Year of Publication2004
AuthorsBagnara R, Zaccagnini A
Abstract

Recurrence relations play an important role in the field of complexity analysis since complexity measures can often be elegantly expressed by systems of such relations. This justifies the interest in automatic, precise, efficient and correct systems able to solve or to approximate the solution of systems of recurrence relations. Assume such a system is built. Since closed-form solutions for recurrences of even modest complexity can be so big and complex to be unmanageable, how can confidence on such a system be gained? How can we quickly validate or perhaps disprove its results? And, in those cases where the exact solution is too complex to be of practical use, how can we trade precision for efficiency by approximating them from below and from above? We also concern ourselves with a problem related to the handling of sets of solutions of recurrence relations: how can we confine by means of a lower bound and an upper bound a set of such solutions? We provide some solutions to these problems where we are careful to rely, whenever possible, on fast integer computations and/or conditions that are easy to check in a completely automatic way. The ongoing experimental evaluation of these ideas is giving very promising results, showing order-of-magnitude speedups over the more traditional methods.

The Automatic Solution of Recurrence Relations. {I}. {Linear} Recurrences of Finite Order with Constant Coefficients

TitleThe Automatic Solution of Recurrence Relations. {I}. {Linear} Recurrences of Finite Order with Constant Coefficients
Publication TypeMiscellaneous
Year of Publication2003
AuthorsBagnara R, Zaccagnini A, Zolo T
Keywordscomplexity analysis, recurrence relations, software verification, static analysis
Abstract

We describe algorithmic techniques for the efficient solution of a wide class of linear recurrences of finite order with constant coefficients. We give an outline of the underlying theory both from an abstract and a more concrete point of view, in an attempt to convey the general principles as clearly as possible yet providing a well marked path for the implementation. In particular, the presentation is thorough and reasonably self-contained, covering topics such as the automatic solution of polynomial equations and efficient, exact symbolic summation of some special functions.

Set-Sharing is Redundant for Pair-Sharing

TitleSet-Sharing is Redundant for Pair-Sharing
Publication TypeJournal Article
Year of Publication2002
AuthorsBagnara R, Hill PM, Zaffanella E
JournalTheoretical Computer Science
Volume277
Pagination3–46
ISSN0304-3975
Keywordsabstract interpretation, domain decomposition, logic programming, sharing analysis, software verification, static analysis
Abstract

Although the usual goal of sharing analysis is to detect which pairs of variables share, the standard choice for sharing analysis is a domain that characterizes set-sharing. In this paper, we question, apparently for the first time, whether this domain is over-complex for pair-sharing analysis. We show that the answer is yes. By defining an equivalence relation over the set-sharing domain we obtain a simpler domain, reducing the complexity of the abstract unification procedure. We present experimental results showing that, in practice, our domain compares favorably with the set-sharing one over a wide range of benchmark and real programs.

DOI10.1016/S0304-3975(00)00312-1
File attachments: 

Soundness, Idempotence and Commutativity of Set-Sharing

TitleSoundness, Idempotence and Commutativity of Set-Sharing
Publication TypeJournal Article
Year of Publication2002
AuthorsHill PM, Bagnara R, Zaffanella E
JournalTheory and Practice of Logic Programming
Volume2
Pagination155–201
ISSN1471-0684
Keywordsabstract interpretation, logic programming, sharing analysis, software verification, static analysis
Abstract

It is important that practical data-flow analyzers are backed by reliably proven theoretical results. Abstract interpretation provides a sound mathematical framework and necessary generic properties for an abstract domain to be well-defined and sound with respect to the concrete semantics. In logic programming, the abstract domain Sharing is a standard choice for sharing analysis for both practical work and further theoretical study. In spite of this, we found that there were no satisfactory proofs for the key properties of commutativity and idempotence that are essential for Sharing to be well-defined and that published statements of the soundness of Sharing assume the occurs-check. This paper provides a generalization of the abstraction function for Sharing that can be applied to any language, with or without the occurs-check. Results for soundness, idempotence and commutativity for abstract unification using this abstraction function are proven.

DOI10.1017/S1471068401001338
File attachments: 

Foreign Language Interfaces for {Prolog}: A Terse Survey

TitleForeign Language Interfaces for {Prolog}: A Terse Survey
Publication TypeMiscellaneous
Year of Publication2002
AuthorsBagnara R, Carro M
Abstract

The availability of good foreign language interfaces is fundamental for the interoperability of different programming languages. While this observation is true for any language, it is especially important for non-mainstream languages such as Prolog, since they are likely to be discarded when shortcomings of the interfaces suggest the adoption of just one implementation language. In this paper we review some existing Prolog foreign language interfaces, trying to highlight both the important characteristics they share and the features that distinguish them from one another. We argue that even a basic, but standard Prolog foreign language interface could significantly contribute to increasing the adoption of Prolog for those subsystems where it is ‘‘the right language’’. Finally we suggest which steps could be taken in this direction.

Decomposing Non-Redundant {Sharing} by Complementation

TitleDecomposing Non-Redundant {Sharing} by Complementation
Publication TypeJournal Article
Year of Publication2002
AuthorsZaffanella E, Hill PM, Bagnara R
JournalTheory and Practice of Logic Programming
Volume2
Pagination233–261
ISSN1471-0684
Keywordsabstract interpretation, complementation, domain decomposition, logic programming, sharing analysis, software verification, static analysis
Abstract

Complementation, the inverse of the reduced product operation, is a technique for systematically finding minimal decompositions of abstract domains. Filé and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen’s set-sharing domain SH. However, since the result of this operation was still SH, they concluded that PS was too abstract for this. Here, we show that the source of this result lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, a proper decomposition is obtained if our non-redundant version of SH, PSD, is substituted for SH. To establish the results for PSD, we define a general schema for subdomains of SH that includes PSD and Def as special cases. This sheds new light on the structure of PSD and exposes a natural though unexpected connection between Def and PSD. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.

DOI10.1017/S1471068401001351
File attachments: 

A Foundation of Escape Analysis

TitleA Foundation of Escape Analysis
Publication TypeConference Paper
Year of Publication2002
AuthorsHill PM, Spoto F
EditorKirchner H, Ringeissen C
Conference NameAlgebraic Methodology and Software Technology; Proceedings of 9th International Conference, AMAST 2002
PublisherSpringer-Verlag
ISBN Number3-540-44144-1
Keywordsabstract interpretation, escape analysis, Java, object-oriented languages, software verification, static analysis
Abstract

Escape analysis of object-oriented languages allows us to stack allocate dynamically created objects and to reduce the overhead of synchronisation in Java-like languages. We formalise the escape property E, computed by an escape analysis, as an abstract interpretation of concrete states. We define the optimal abstract operations induced by E for a framework of analysis known as watchpoint semantics. The implementation of E inside that framework is a formally correct abstract semantics (analyser) for escape analysis. We claim that E is the basis for more refined and precise domains for escape analysis.

DOI10.1007/3-540-45719-4_26