Advertisement

An Efficient Abstract Domain for Not Necessarily Closed Polyhedra

  • Anna Becchi
  • Enea ZaffanellaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

We present a construction of the abstract domain of NNC (not necessarily topologically closed) polyhedra based on a recently introduced variant of the double description representation and conversion procedure. We describe the implementation of the operators needed to interface the new abstract domain with commonly available static analysis tools, highlighting the efficiency gains enabled by the new representation. We also reconsider the widening operator for NNC polyhedra, proposing a more appropriate specification based on the semantics of the domain elements, rather than their low level representation details. Finally, we provide an experimental evaluation comparing the efficiency of the new abstract domain with respect to more classical implementations.

References

  1. 1.
    Amato, G., Scozzari, F.: The abstract domain of parallelotopes. Electr. Notes Theor. Comput. Sci. 287, 17–28 (2012)CrossRefGoogle Scholar
  2. 2.
    Bagnara, R., Hill, P.M., Mazzi, E., Zaffanella, E.: Widening operators for weakly-relational numeric abstractions. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 3–18. Springer, Heidelberg (2005).  https://doi.org/10.1007/11547662_3CrossRefGoogle Scholar
  3. 3.
    Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337–354. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-44898-5_19CrossRefGoogle Scholar
  4. 4.
    Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1–2), 28–56 (2005)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 135–148. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24622-0_13CrossRefGoogle Scholar
  6. 6.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Formal Asp. Comput. 17(2), 222–257 (2005)CrossRefGoogle Scholar
  7. 7.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. Softw. Tools for Technol. Transf. 8(4/5), 449–466 (2006)CrossRefGoogle Scholar
  8. 8.
    Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Applications of polyhedral computations to the analysis and verification of hardware and software systems. Theor. Comput. Sci. 410(46), 4672–4691 (2009)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Formal Meth. Syst. Des. 35(3), 279–323 (2009)CrossRefGoogle Scholar
  11. 11.
    Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.M.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45789-5_17CrossRefGoogle Scholar
  12. 12.
    Becchi, A., Zaffanella, E.: A conversion procedure for NNC polyhedra. CoRR, abs/1711.09593 (2017)Google Scholar
  13. 13.
    Becchi, A., Zaffanella, E.: A direct encoding for NNC polyhedra. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification, pp. 230–248, Cham, 2018. Springer International Publishing. An extended version with proofs is available as [12]Google Scholar
  14. 14.
    Birkhoff, G.: Lattice Theory, vol. 25. Colloquium Publications. American Mathematical Society, Providence (1967)Google Scholar
  15. 15.
    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), pp. 196–207, San Diego, USA (2003)Google Scholar
  16. 16.
    Chernikova, N.V.: Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities. U.S.S.R. Comput. Math. Math. Phys. 5(2), 228–233 (1965)MathSciNetCrossRefGoogle Scholar
  17. 17.
    Clarisó, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program. 64(1), 115–139 (2007)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Cortesi, A.: Widening operators for abstract interpretation. In: Sixth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2008), pp. 31–40, Cape Town, South Africa (2008)Google Scholar
  19. 19.
    Cortesi, A., Zanioli, M.: Widening and narrowing operators for abstract interpretation. Comput. Lang. Syst. Struct. 37(1), 24–42 (2011)zbMATHGoogle Scholar
  20. 20.
    Cousot, P., Cousot, R.: 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, pp. 238–252, Los Angeles, USA (1977)Google Scholar
  21. 21.
    Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55844-6_142CrossRefzbMATHGoogle Scholar
  22. 22.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pp. 84–96, Tucson, USA (1978)Google Scholar
  23. 23.
    Fulara, J., Durnoga, K., Jakubczyk, K., Schubert, A.: Relational abstract domain of weighted hexagons. Electr. Notes Theor. Comput. Sci. 267(1), 59–72 (2010)CrossRefGoogle Scholar
  24. 24.
    Genov, B.: The convex hull problem in practice: improving the running time of the double description method. Ph.D. thesis, University of Bremen, Germany (2014)Google Scholar
  25. 25.
    Halbwachs, N.: Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme. Thèse de 3ème cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France (1979)Google Scholar
  26. 26.
    Halbwachs, N., Merchat, D., Gonnord, L.: Some ways to reduce the space dimension in polyhedra computations. Formal Meth. Syst. Des. 29(1), 79–95 (2006)CrossRefGoogle Scholar
  27. 27.
    Halbwachs, N., Merchat, D., Parent-Vigouroux, C.: Cartesian factoring of polyhedra in linear relation analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 355–365. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-44898-5_20CrossRefzbMATHGoogle Scholar
  28. 28.
    Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Le Charlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223–237. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58485-4_43CrossRefGoogle Scholar
  29. 29.
    Halbwachs, N., Proy, Y.-E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Meth. Syst. Des. 11(2), 157–185 (1997)CrossRefGoogle Scholar
  30. 30.
    Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electr. Notes Theor. Comput. Sci. 289, 15–25 (2012)CrossRefGoogle Scholar
  31. 31.
    Howe, J.M., King, A.: Logahedra: a new weakly relational domain. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 306–320. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04761-9_23CrossRefGoogle Scholar
  32. 32.
    Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_52CrossRefGoogle Scholar
  33. 33.
    Kaibel, V., Pfetsch, M.E.: Computing the face lattice of a polytope from its vertex-facet incidences. Comput. Geom. 23(3), 281–290 (2002)MathSciNetCrossRefGoogle Scholar
  34. 34.
    Laviron, V., Logozzo, F.: SubPolyhedra: a (More) scalable approach to infer linear inequalities. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 229–244. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-93900-9_20CrossRefGoogle Scholar
  35. 35.
    Logozzo, F., Fähndrich, M.: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In: Proceedings of the 2008 ACM Symposium on Applied Computing, pp. 184–188, Fortaleza, Brazil (2008)Google Scholar
  36. 36.
    Miné, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155–172. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44978-7_10CrossRefGoogle Scholar
  37. 37.
    Miné, A.: The octagon abstract domain. In: Proceedings of the Eighth Working Conference on Reverse Engineering, pp. 310–319, Stuttgart, Germany (2001)Google Scholar
  38. 38.
    Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique, Paris, France (2005)Google Scholar
  39. 39.
    Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Contributions to the Theory of Games - Volume II, Number 28 in Annals of Mathematics Studies, pp. 51–73, Princeton, USA (1953)Google Scholar
  40. 40.
    Notani, V., Giacobazzi, R.: Learning based widening. In: 8th Workshop on Tools for Automatic Program Analysis (TAPAS 2017), New York, USA (2017)Google Scholar
  41. 41.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-30579-8_2CrossRefGoogle Scholar
  42. 42.
    Shaham, R., Kolodner, E.K., Sagiv, S.: Heap profiling for space-efficient Java. In: Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 104–113, Snowbird, USA (2001)Google Scholar
  43. 43.
    Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 71–89. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-45013-0_7CrossRefGoogle Scholar
  44. 44.
    Singh, G., Püschel, M., Vechev, M.T.: Making numerical program analysis fast. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 303–313, Portland, USA (2015)Google Scholar
  45. 45.
    Singh, G., Püschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 46–59, Paris, France (2017)Google Scholar
  46. 46.
    Singh, G., Püschel, M., Vechev, M.T.: A practical construction for decomposing numerical abstract domains. PACMPL, 2(POPL), 55:1–55:28 (2018)Google Scholar
  47. 47.
    Zaffanella, E.: On the efficiency of convex polyhedra. Electr. Notes Theor. Comput. Sci. 334, 31–44 (2018)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of UdineUdineItaly
  2. 2.University of ParmaParmaItaly

Personalised recommendations