Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2018: Static Analysis pp 146–165Cite as

An Efficient Abstract Domain for Not Necessarily Closed Polyhedra

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    We assume some familiarity with the basic notions of lattice theory [14].

  2. 2.

    Note that we abuse notation by adopting the usual set operator and relation symbols to denote the corresponding component-wise extensions on systems.

  3. 3.

    The opposite conversion works in the same way, exploiting duality.

  4. 4.

    \(\beta \in \mathcal {C}\) is redundant in \(\mathcal {C}\) if \(\mathop {\mathrm {con}}\nolimits (\mathcal {C}) = \mathop {\mathrm {con}}\nolimits (\mathcal {C}\setminus \{\beta \})\); similarly for generators.

  5. 5.

    In the figures, the (strict) inequality constraints are denoted by (dashed) lines and the (closure) points are denoted by (unfilled) circles.

  6. 6.

    \(\mathop {\uparrow }\nolimits S\) denotes the smallest upward closed set containing S.

  7. 7.

    Recall that \( ns _g = \{c_0, c_1\}\) is the support describing the materialization \(p_1\).

  8. 8.

    It is meant, with respect to those available for \(\epsilon \)-representations.

  9. 9.

    The first parameter \(\beta \) of strict-on-eq-points seems to require a geometrical constraint, but this is not really the case; the parameter is only used to check the constraint kind (equality, non-strict inequality or strict inequality): in the special case of a non-skeleton element \( ns \), we always have a strict inequality.

  10. 10.

    For all widenings ‘\(\nabla \)’, we implicitly specify that \(\emptyset \nabla \mathcal {P}_2 = \mathcal {P}_2\) .

  11. 11.

    We write \(\mathop {\mathrm {ineqs}}\nolimits (\mathcal {C})\) to denote the constraint system obtained by splitting each equality in \(\mathcal {C}\) into a pair of non-strict inequalities.

  12. 12.

    As an example, \(f_0\) is the number of strict inequality constraints cutting only a vertex from the topological closure of the polyhedron.

  13. 13.

    Note that for all \(k \le j \le n-1\), we have \(f_j = f'_j = 0\).

  14. 14.

    The efficiency gains have been confirmed when adopting the PPLite implementation.

  15. 15.

    All experiments have been performed on a laptop with an Intel Core i7-3632QM CPU, 16 GB of RAM and running GNU/Linux 4.13.0-36.

  16. 16.

    We only show those tests where the time spent by pplite_poly is above 0.5 s.

References

  1. Amato, G., Scozzari, F.: The abstract domain of parallelotopes. Electr. Notes Theor. Comput. Sci. 287, 17–28 (2012)

    Article  Google Scholar 

  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_3

    Chapter  Google Scholar 

  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_19

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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_13

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  7. Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. Softw. Tools for Technol. Transf. 8(4/5), 449–466 (2006)

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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)

    Article  Google Scholar 

  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_17

    Chapter  Google Scholar 

  12. Becchi, A., Zaffanella, E.: A conversion procedure for NNC polyhedra. CoRR, abs/1711.09593 (2017)

    Google Scholar 

  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. Birkhoff, G.: Lattice Theory, vol. 25. Colloquium Publications. American Mathematical Society, Providence (1967)

    Google Scholar 

  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. 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)

    Article  MathSciNet  Google Scholar 

  17. Clarisó, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program. 64(1), 115–139 (2007)

    Article  MathSciNet  Google Scholar 

  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. Cortesi, A., Zanioli, M.: Widening and narrowing operators for abstract interpretation. Comput. Lang. Syst. Struct. 37(1), 24–42 (2011)

    MATH  Google Scholar 

  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. 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_142

    Chapter  MATH  Google Scholar 

  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. Fulara, J., Durnoga, K., Jakubczyk, K., Schubert, A.: Relational abstract domain of weighted hexagons. Electr. Notes Theor. Comput. Sci. 267(1), 59–72 (2010)

    Article  Google Scholar 

  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. 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. 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)

    Article  Google Scholar 

  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_20

    Chapter  MATH  Google Scholar 

  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_43

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  30. Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electr. Notes Theor. Comput. Sci. 289, 15–25 (2012)

    Article  Google Scholar 

  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_23

    Chapter  Google Scholar 

  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_52

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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_20

    Chapter  Google Scholar 

  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. 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_10

    Chapter  Google Scholar 

  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. Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique, Paris, France (2005)

    Google Scholar 

  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. 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. 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_2

    Chapter  Google Scholar 

  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. 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_7

    Chapter  Google Scholar 

  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. 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. 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. Zaffanella, E.: On the efficiency of convex polyhedra. Electr. Notes Theor. Comput. Sci. 334, 31–44 (2018)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Udine, Udine, Italy

    Anna Becchi

  2. University of Parma, Parma, Italy

    Enea Zaffanella

Authors
  1. Anna Becchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Enea Zaffanella
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Enea Zaffanella .

Editor information

Editors and Affiliations

  1. Universität Freiburg, Freiburg, Germany

    Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Becchi, A., Zaffanella, E. (2018). An Efficient Abstract Domain for Not Necessarily Closed Polyhedra. In: Podelski, A. (eds) Static Analysis. SAS 2018. Lecture Notes in Computer Science(), vol 11002. Springer, Cham. https://doi.org/10.1007/978-3-319-99725-4_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-99725-4_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-99724-7

  • Online ISBN: 978-3-319-99725-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation