Advertisement

An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints

  • Mathias Péron
  • Nicolas Halbwachs
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4349)

Abstract

Knowing that two numerical variables always hold different values, at some point of a program, can be very useful, especially for analyzing aliases: if i ≠ j, then A[i] and A[j] are not aliased, and this knowledge is of great help for many other program analyses. Surprisingly, disequalities are seldom considered in abstract interpretation, most of the proposed numerical domains being restricted to convex sets. In this paper, we propose to combine simple ordering properties with disequalities. “Difference-bound matrices” (or DBMs) is a domain proposed by David Dill, for expressing relations of the form “x − y ≤ c” or “c 1 ≤ x ≤ c 2”. We define dDBMs (“disequalities DBMs”) as conjunctions of DBMs with simple disequalities of the form “x ≠ y” or “x ≠ 0”. We give algorithms on dDBMs, for deciding the emptiness, computing a normal form, and performing the usual operations of an abstract domain. These algorithms have the same complexity (O(n 3), where n is the number of variables) than those for classical DBMs, if the variables are considered to be valued in a dense set (ℝ or ℚ). In the arithmetic case, the emptiness decision is NP-complete, and other operations run in O(n 5).

Keywords

abstract domains alias analysis difference-bound matrices disequalities static analysis 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information and Computation 104(1), 2–34 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  2. Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: PLDI’93, pp. 46–55. ACM, New York (1993)Google Scholar
  3. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: 2nd Int. Symp. on Programming, pp. 106–130. Dunod, Paris (1976)Google Scholar
  4. Clarisó, R.C., Cortadella, J.: Verification of parametric timed circuits using octahedra. In: Designing correct circuits, DCC’04, Barcelona (2004)Google Scholar
  5. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL’78, pp. 84–96 (January 1978)Google Scholar
  6. Cormen, T.H., et al.: Introduction to Algorithms. The MIT Press, Cambridge (1990)Google Scholar
  7. Deutsch, A.: Interprocedural may-alias analysis for pointers: beyond k-limiting. In: PLDI’94, pp. 230–241 (1994)Google Scholar
  8. Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)Google Scholar
  9. Goralciková, A., Koubek, V.: A reduct-and-closure algorithm for graphs. In: Becvar, J. (ed.) Mathematical Foundations of Computer Science 1979. LNCS, vol. 74, pp. 301–307. Springer, Heidelberg (1979)Google Scholar
  10. CAAP 1991 and TAPSOFT 1991.
    Granger, P.: Static analysis of linear congruence equalities among variables of a program. In: Abramsky, S. (ed.) CAAP 1991 and TAPSOFT 1991. LNCS, vol. 493, pp. 169–192. Springer, Heidelberg (1991)Google Scholar
  11. Harvey, W., Stuckey, P.J.: A unit two variable per inequality integer constraint solver for constraint logic programming. In: Twentieth Australasian Computer Science Conference, ACSC’97, pp. 102–111 (February 1997)Google Scholar
  12. Harvey, W., Stuckey, P.J.: Improving linear constraint propagation by changing constraint representation. Constraints 8(2), 173–207 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  13. Imbert, J.-L.: Variable elimination for generalized linear constraints. In: ICLP’93, pp. 499–516 (1993)Google Scholar
  14. Jeannet, B.: The NBAC verification/slicing tool, http://www.inrialpes.fr/pop-art/people/bjeannet/nbac/
  15. SAS 1999.
    Jeannet, B., Halbwachs, N., Raymond, P.: Dynamic partitioning in analyses of numerical properties. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, Springer, Heidelberg (1999)CrossRefGoogle Scholar
  16. Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)zbMATHCrossRefMathSciNetGoogle Scholar
  17. Lassez, J.-L., McAloon, K.: A canonical form for generalized linear constraints. J. Symb. Comput. 13(1), 1–24 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  18. Larsen, K.G., et al.: Clock difference diagrams. Nordic J. of Computing 6(3), 271–298 (1999)zbMATHMathSciNetGoogle Scholar
  19. Masdupuy, F.: Semantic analysis of interval congruences. In: International Conference on Formal Methods in Programming and Their Applications, pp. 142–155 (1993)Google Scholar
  20. Miné, A.: The octagon abstract domain. In: AST 2001 in WCRE 2001, pp. 310–319. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar
  21. Miné, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117–132. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  22. CSL 1999.
    Møller, J.B., et al.: Difference decision diagrams. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 111–125. Springer, Heidelberg (1999)Google Scholar
  23. ESOP 2005.
    Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, Springer, Heidelberg (2005)Google Scholar
  24. Puget, J.-F.: A fast algorithm for the bound consistency of alldiff constraints. In: Mittal, V.O., et al. (eds.) Assistive Technology and Artificial Intelligence. LNCS (LNAI), vol. 1458, pp. 359–366. Springer, Heidelberg (1998)Google Scholar
  25. Pugh, W., Wonnacott, D.: Constraint-based array dependence analysis. TOPLAS 20(3), 635–678 (1998)CrossRefGoogle Scholar
  26. Rosenkrantz, D.J., Hunt III, H.B.: Processing conjunctive predicates and ueries. In: VLDB, pp. 64–72 (1980)Google Scholar
  27. ESA 1993.
    Simon, K., Crippa, D., Collenberg, F.: On the distribution of the transitive closure in a random acyclic digraph. In: Lengauer, T. (ed.) ESA 1993. LNCS, vol. 726, pp. 345–356. Springer, Heidelberg (1993)Google Scholar
  28. Simon, K.: An improved algorithm for transitive closure on acyclic digraphs. TCS 58(1-3), 325–346 (1988)zbMATHCrossRefGoogle Scholar
  29. SAS 2006.
    Sankaranarayanan, S., et al.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  30. LCPC 2002.
    Seater, R., Wonnacott, D.: Efficient Manipulation of Disequalities During Dependence Analysis. In: Pugh, B., Tseng, C.-W. (eds.) LCPC 2002. LNCS, vol. 2481, pp. 295–308. Springer, Heidelberg (2005)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Mathias Péron
    • 1
  • Nicolas Halbwachs
    • 1
  1. 1.Vérimag, GrenobleFrance

Personalised recommendations