Widening Operators for Weakly-Relational Numeric Abstractions
(Extended Abstract)1

Roberto Bagnara, Department of Mathematics, University of Parma, Italy
  Patricia M. Hill, School of Computing, University of Leeds, UK
  Elena Mazzi, Department of Mathematics, University of Parma, Italy
  Enea Zaffanella, Department of Mathematics, University of Parma, Italy

1  Introduction

In recent years there has been a lot of interest in the definition of so-called weakly-relational numeric domains, whose complexity and precision are in between the (non-relational) abstract domain of intervals [9] and the (relational) abstract domain of convex polyhedra [10]. The first weakly-relational domain proposed in the literature is based on systems of constraints of the form x - y <= c and ± x <= c, typically represented by Difference-Bound Matrices (DBMs). Even though DBMs have a long tradition in Computer Science, their use in the Abstract Interpretation field is quite recent. The idea of defining an abstract domain of DBMs was put forward in [1], where these constraints were called bounded differences. An independent application can be found in [19], where an abstract domain of transitively closed DBMs is defined. In this case, the transitive closure requirement was meant as a simple and well understood way to obtain a canonical form for the domain elements, so as to abstract away from merely syntactic differences. In [19] the specification of all the required abstract semantics operators is provided, including an operator that is meant to match the standard widening operator defined on the domain of convex polyhedra [10]. Unfortunately, as pointed out in [14, 15], this operator is not a widening since it does not provide a convergence guarantee for the abstract iteration sequence.

The abstract domain of (not necessarily transitively closed) DBMs is considered in [14]. In this more concrete, syntactic domain the transitive closure operator behaves as a kernel operator (monotonic, idempotent and reductive) mapping each DBM into the smallest DBM (with respect to the component-wise ordering) encoding the same geometric shape. As done in [19], a widening operator is also defined in [14] and it is observed that this widening ``has some intriguing interactions'' with transitive closure, therefore identifying the divergence issue faced in [19]. This observation has led to the conclusion that ``fixpoint computations must be performed'' in the lattice of DBMs, without enforcing transitive closure [14].

2  Difference-Bound Shapes

While the analysis of the divergence problem is absolutely correct, the solution identified in [14] is sub-optimal since, as is usually the case, resorting to a syntactic domain (such as the one of DBMs) has a number of negative consequences. To identify a simpler, more natural solution, we first have to acknowledge that an element of this abstract domain should be a geometric shape, rather than (any) one of its matrix representations. To stress this concept, such an element will be called a Difference-Bound Shape (DBS). A DBS corresponds to the equivalence class of all the DBMs representing it. The implementation of the abstract domain can freely choose between these possible representations, switching at will from one to the other, as long as the semantic operators are implemented as expected. The other step towards the solution of the divergence problem is the simple observation that a DBS is a convex polyhedron and the set of all DBSs is closed under the application of the standard widening on polyhedra. Thus, no divergence problem can be incurred when applying the standard widening to an increasing sequence of DBSs.

On the other hand, the domain of DBSs is isomorphic to the domain of transitively closed DBMs considered in [19], which suffers from an actual divergence problem. A closer inspection reveals that these two observations are not in contradiction, because the widening operator defined in [19] is not equivalent to the standard widening for convex polyhedra. In fact, a key requirement in the specification of the standard widening is that the first argument is described by a non-redundant system of constraints.2 Thus, using transitively closed DBMs does not work because they typically contain redundant constraints. What is needed for a correct implementation of the standard widening is a minimization procedure mapping a DBM representation into (any) one of the maximal elements in the corresponding equivalence class: such a procedure was defined in [13] and called transitive reduction.

In summary, the solution to the divergence problem for DBSs is to apply the standard widening of [10] to a transitively reduced DBM representation of the first argument. It is worth stressing that, from the point of view of the user, this is a transparent implementation detail: on the domain of DBSs, transitive reduction is the identity function, as was the case for transitive closure.

2.1  On the Precision of the Standard Widening

The standard widening on DBSs could result, if used without any precaution, in poorer precision with respect to its counterpart defined on the syntactic domain of DBMs. The specification of [14] prescribes, for maximum precision, two constraints on the abstract iteration sequence: the first one restricts the application of the standard widening to a transitively closed representation for the second argument (note that, in this case, no divergence problem can arise); the second one demands that the first DBM of the iteration sequence M0, M1, ..., Mi, ...is transitively closed. The effects of both improvements can be obtained also with the semantic domain of DBSs. As for the first one, this can be applied as is (since transitive closure is just an implementation detail). The other improvement can be achieved by applying the well-known `widening up to' technique defined in [11, 12] or its variation called `staged widening with thresholds' [6, 7, 17]: in practice, it is sufficient to add to the set of `up to' thresholds all the constraints of M0 that are redundant for the representation of the corresponding DBS (i.e., those constraints that are removed by the transitive reduction algorithm).

Further precision improvements can be obtained by applying any delay strategy and/or the framework defined in [2, 3]. In particular, by providing the widening on DBSs with a finite convergence certificate, it is possible to lift it to a corresponding widening on the finite powerset of DBSs [4]. It should be stressed that, in this case, using the syntactic domain of DBMs may have drawbacks: since different DBMs may represent the same DBS, the presence of these ``duplicates'' in a finite powerset element may have a negative effect on both efficiency and precision (e.g., when considering a cardinality-based widening operator). Also note that, in general, the systematic removal of these duplicates would interfere with widenings, possibly compromising the convergence guarantee.

3  Octagonal Shapes and Beyond

The abstract domain of DBMs has been generalized in [15] so as to allow for the manipulation of constraints of the form a x + b y <= c, where a,b in {-1,0,+1}, leading to the definition of the octagon abstract domain (octagons were called simple sections in [5]). Each octagon is represented by using a coherent DBM and the transitive closure algorithm is specialized into a strong closure procedure. All the previous reasoning can be repeated, leading to the definition of the semantic abstract domain of octagonal shapes together with a correct implementation of the standard widening. In this case, the transitive reduction algorithm defined in [13] does not eliminate all redundancies: we will describe a new minimization procedure that takes into account all the constraint inferences performed by the strong closure algorithm.

Other examples of weakly-relational numeric domains include the `two variables per inequality' abstract domain [20], the octahedron abstract domain [8], and the abstract domain of template constraint matrices [18], as well as the abstract domain of bounded quotients [1] and the zone congruence abstract domain [16]. As long as their implementation is based on (extensions of) the transitive closure algorithm, it is possible to define the corresponding syntactic and semantic versions. The choice between the two versions mainly depends on the availability of a reasonably efficient minimization procedure: in our opinion, all the rest being equal, the semantic versions should be preferred for their greater elegance and the more natural integration with domain constructions such as the finite powerset operator.

References

[1]
R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, March 1997. Printed as Report TD-1/97.

[2]
R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337--354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.

[3]
R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Science of Computer Programming, 2005. To appear.

[4]
R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. In B. Steffen and G. Levi, editors, Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004), volume 2937 of Lecture Notes in Computer Science, pages 135--148, Venice, Italy, 2003. Springer-Verlag, Berlin.

[5]
V. Balasundaram and K. Kennedy. A technique for summarizing data access and its use in parallelism enhancing transformations. In B. Knobe, editor, Proceedings of the ACM SIGPLAN'89 Conference on Programming Language Design and Implementation (PLDI), volume 24(7) of ACM SIGPLAN Notices, pages 41--53, Portland, Oregon, USA, 1989. ACM Press.

[6]
B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In T. Æ. Mogensen, D. A. Schmidt, and I. Hal Sudborough, editors, The Essence of Computation, volume 2566 of Lecture Notes in Computer Science, pages 85--108. Springer-Verlag, Berlin, 2002.

[7]
B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI'03), pages 196--207, San Diego, California, USA, 2003. ACM Press.

[8]
R. Clarisó and J. Cortadella. The octahedron abstract domain. In R. Giacobazzi, editor, Static Analysis: Proceedings of the 11th International Symposium, volume 3148 of Lecture Notes in Computer Science, pages 312--327, Verona, Italy, 2004. Springer-Verlag, Berlin.

[9]
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238--252, New York, 1977. ACM Press.

[10]
P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84--96, Tucson, Arizona, 1978. ACM Press.

[11]
N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In B. Le Charlier, editor, Static Analysis: Proceedings of the 1st International Symposium, volume 864 of Lecture Notes in Computer Science, pages 223--237, Namur, Belgium, 1994. Springer-Verlag, Berlin.

[12]
N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157--185, 1997.

[13]
K. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient verification of real-time systems: Compact data structure and state-space reduction. In Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS'97), pages 14--24, San Francisco, CA, 1997. IEEE Computer Society Press.

[14]
A. Miné. A new numerical abstract domain based on difference-bound matrices. In O. Danvy and A. Filinski, editors, Proceedings of the 2nd Symposium on Programs as Data Objects (PADO 2001), volume 2053 of Lecture Notes in Computer Science, pages 155--172, Aarhus, Denmark, 2001. Springer-Verlag, Berlin.

[15]
A. Miné. The octagon abstract domain. In Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), pages 310--319, Stuttgart, Germany, 2001. IEEE Computer Society Press.

[16]
A. Miné. A few graph-based relational numerical abstract domains. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 117--132, Madrid, Spain, 2002. Springer-Verlag, Berlin.

[17]
A. Miné. Relational abstract domains for the detection of floating-point run-time errors. In D. Schmidt, editor, Programming Languages and Systema: Proceedings of the 13th European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, pages 3--17, Barcelona, Spain, 2004. Springer-Verlag, Berlin.

[18]
S. Sankaranarayanan, H. Sipma, and Z. Manna. Scalable analysis of linear systems using mathematical programming. In R. Cousot, editor, Proceedings of the Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2005), volume 3385 of Lecture Notes in Computer Science, Paris, France, 2004. Springer-Verlag, Berlin. To appear.

[19]
R. Shaham, E. K. Kolodner, and S. Sagiv. Automatic removal of array memory leaks in Java. In D. A. Watt, editor, Proceedings of the 9th International Conference on Compiler Construction (CC 2000), volume 1781 of Lecture Notes in Computer Science, pages 50--66. Springer-Verlag, Berlin, 2000.

[20]
A. Simon, A. King, and J. M. Howe. Two variables per linear inequality as an abstract domain. In M. Leuschel, editor, Logic Based Program Synthesis and Tranformation, 12th International Workshop, volume 2664 of Lecture Notes in Computer Science, pages 71--89, Madrid, Spain, 2002. Springer-Verlag, Berlin.

1
This work has been partly supported by projects ``Constraint Based Verification of Reactive Systems'' and ``AIDA --- Abstract Interpretation Design and Applications'' and by the Royal Society International Joint Project --- 2004/R1 Europe (ESEP).
2
This requirement was sometimes neglected in recent papers describing the standard widening; it was recently recalled and exemplified in [2, 3].

This document was translated from LATEX by HEVEA.