Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Simulation and Invariance for Weak Consistency Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Exploiting Sparsity in Difference-Bound Matrices

verfasst von : Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Erschienen in: Static Analysis

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

Relational numeric abstract domains are very important in program analysis. Common domains, such as Zones and Octagons, are usually conceptualised with weighted digraphs and implemented using difference-bound matrices (DBMs). Unfortunately, though conceptually simple, direct implementations of graph-based domains tend to perform poorly in practice, and are impractical for analyzing large code-bases. We propose new DBM algorithms that exploit sparsity and closed operands. In particular, a new representation which we call split normal form reduces graph density on typical abstract states. We compare the resulting implementation with several existing DBM-based abstract domains, and show that we can substantially reduce the time to perform full DBM analysis, without sacrificing precision.

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 Securing a Compiler Transformation
Nächstes Kapitel Flow- and Context-Sensitive Points-To Analysis Using Generalized Points-To Graphs
Fußnoten
1
For presentation purposes, we assume all program states share a fixed set V of variables. In practice, this is unnecessarily expensive—we instead maintain vertices for only the variables that are in scope, and add or remove vertices as needed.
 
2
Our approach works for rational numbers as well. The implementation assumes 64-bit integers and does not currently take over-/under-flow into account.
 
3
This assumes \(\pi (\mathtt {S})\) is total. For a partial function like integer division we first close with respect to \(\mathtt {x}\), then enforce the remaining invariants.
 
4
It is not immediately clear how to extend this efficiently to an n-way meet, as a vertex may be reachable from some arbitrary subset of the operands.
 
5
This terminology may be confusing. The transitive reduction computes the greatest (by \({{\mathrm{\sqsubseteq }}}\)) equivalent representation of R, whereas the usual abstract-domain reduction corresponds to the transitive closure.
 
6
This assumes 16-bit vertex identifiers; if more than \(2^{16}\) variables are in scope at a program point, any dense-matrix approach is already impractical.
 
7
Code is available from the authors upon request.
 
8
We tried to stress test the DBM implementations by increasing the number of variables in scope through inlining. We inlined all function calls unless a called function was recursive or could not be resolved at compile time.
 
Literatur
1.
2.
Briggs, P., Torczon, L.: An efficient representation for sparse sets. ACM Lett. Program. Lang. Syst. 2(1–4), 59–69 (1993)CrossRef
3.
Chawdhary, A., Robbins, E., King, A.: Simple and efficient algorithms for octagons. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 296–313. Springer, Heidelberg (2014)
4.
5.
Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006)CrossRef
6.
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 ACM Symposium Principles of Programming Languages, pp. 238–252. ACM Press (1977)
7.
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Sixth ACM Symposium Principles of Programming Languages, pp. 269–282. ACM Press (1979)
8.
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? Formal Methods Syst. Des. 35(3), 229–264 (2009)CrossRefMATH
9.
Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: Proceedings of the Fifth ACM Symposium Principles of Programming Languages, pp. 84–97. ACM Press (1978)
10.
Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011)
11.
Feydy, T., Schutt, A., Stuckey, P.J.: Global difference constraint propagation for finite domain solvers. In: Proceedings of the 10th International ACM SIGPLAN Conference Principles and Practice of Declarative Programming, pp. 226–235. ACM Press (2008)
12.
Ford, L.R., Fulkerson, D.R.: Flows in Networks. Princeton University Press, Princeton (1962)MATH
13.
14.
Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: compact data structure and state-space reduction. In: Proceedings of the 18th International Symposium Real-Time Systems, pp. 14–24. IEEE Computer Society (1997)
15.
Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis and transformation. In: Proceedings of the International Symposium Code Generation and Optimization (CGO 2004), pp. 75–86. IEEE Computer Society (2004)
16.
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 Applied Computing, pp. 184–188. ACM Press (2008)
17.
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)CrossRef
18.
Miné, A.: The octagon abstract domain. High. Ord. Symbolic Comput. 19(1), 31–100 (2006)CrossRefMATH
19.
Okasaki, C., Gill, A.: Fast mergeable integer maps. In: Notes of the ACM SIGPLAN Workshop on ML, pp. 77–86, September 1998
20.
Singh, G., Püschel, M., Vechev, M.: Making numerical program analysis fast. In: Proceedings of the 36th ACM SIGPLAN Conference Programming Language Design and Implementation, pp. 303–313. ACM (2015)
21.
Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: Proceedings of the 25th ACM SIGPLAN Conference Programming Language Design and Implementation, pp. 231–242. ACM Press (2004)
22.
Venet, A.J.: The gauge domain: scalable analysis of linear inequality invariants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 139–154. Springer, Heidelberg (2012)CrossRef
Metadaten
Titel
Exploiting Sparsity in Difference-Bound Matrices
verfasst von
Graeme Gange
Jorge A. Navas
Peter Schachte
Harald Søndergaard
Peter J. Stuckey
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Static Analysis

Print ISBN: 978-3-662-53412-0

Electronic ISBN: 978-3-662-53413-7

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-662-53413-7_10