nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

An Efficient Abstract Domain for Not Necessarily Closed Polyhedra

verfasst von : Anna Becchi, Enea Zaffanella

Erschienen in: Static Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Extending Constraint-Only Representation of Polyhedra with Boolean Constraints

Nächstes Kapitel Modular Software Fault Isolation as Abstract Interpretation

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

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

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

\(\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.

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

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

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

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

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.

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

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.

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

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

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

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.

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

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

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_3CrossRef

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_19CrossRef

Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1–2), 28–56 (2005)MathSciNetCrossRef

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_13CrossRef

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

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

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

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

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

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_17CrossRef

12.

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

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]

14.

Birkhoff, G.: Lattice Theory, vol. 25. Colloquium Publications. American Mathematical Society, Providence (1967)

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)

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

17.

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

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)

19.

Cortesi, A., Zanioli, M.: Widening and narrowing operators for abstract interpretation. Comput. Lang. Syst. Struct. 37(1), 24–42 (2011)MATH

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)

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_142CrossRefMATH

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)

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

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)

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)

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

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_20CrossRefMATH

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_43CrossRef

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

30.

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

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_23CrossRef

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_52CrossRef

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

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_20CrossRef

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)

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_10CrossRef

37.

Miné, A.: The octagon abstract domain. In: Proceedings of the Eighth Working Conference on Reverse Engineering, pp. 310–319, Stuttgart, Germany (2001)

38.

Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique, Paris, France (2005)

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)

40.

Notani, V., Giacobazzi, R.: Learning based widening. In: 8th Workshop on Tools for Automatic Program Analysis (TAPAS 2017), New York, USA (2017)

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_2CrossRef

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)

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_7CrossRef

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)

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)

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)

47.

Zaffanella, E.: On the efficiency of convex polyhedra. Electr. Notes Theor. Comput. Sci. 334, 31–44 (2018)CrossRef

Titel: An Efficient Abstract Domain for Not Necessarily Closed Polyhedra
verfasst von: Anna Becchi
Enea Zaffanella
Verlag: Springer International Publishing
Buch: Static Analysis
Print ISBN: 978-3-319-99724-7

Electronic ISBN: 978-3-319-99725-4

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99725-4_11

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"