Skip to main content

2019 | OriginalPaper | Buchkapitel

Effect-Driven Flow Analysis

verfasst von : Jens Nicolay, Quentin Stiévenart, Wolfgang De Meuter, Coen De Roover

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

Traditional machine-based static analyses use a worklist algorithm to explore the analysis state space, and compare each state in the worklist against a set of seen states as part of their fixed-point computation. This may require many state comparisons, which gives rise to a computational overhead. Even an analysis with a global store has to clear its set of seen states each time the store updates because of allocation or side-effects, which results in more states being reanalyzed and compared.
In this work we present a static analysis technique, Modf, that does not rely on a set of seen states, and apply it to a machine-based analysis with global-store widening. Modf analyzes one function execution at a time to completion while tracking read, write, and call effects. These effects trigger the analysis of other function executions, and the analysis terminates when no new effects can be discovered.
We compared Modf to a traditional machine-based analysis implementation on a set of 20 benchmark programs and found that Modf is faster for 17 programs with speedups ranging between 1.4x and 12.3x. Furthermore, Modf exhibits similar precision as the traditional analysis on most programs and yields state graphs that are comparable in size.

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!

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!

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!

Literatur
1.
Zurück zum Zitat Andreasen, E.S., Møller, A., Nielsen, B.B.: Systematic approaches for increasing soundness and precision of static analyzers. In: Proceedings of the 6th ACM SIGPLAN International Workshop on State of the Art in Program Analysis, SOAP@PLDI 2017, pp. 31–36 (2017) Andreasen, E.S., Møller, A., Nielsen, B.B.: Systematic approaches for increasing soundness and precision of static analyzers. In: Proceedings of the 6th ACM SIGPLAN International Workshop on State of the Art in Program Analysis, SOAP@PLDI 2017, pp. 31–36 (2017)
3.
Zurück zum Zitat Earl, C., Might, M., Van Horn, D.: Pushdown control-flow analysis of higher-order programs. In: Proceedings of the 2010 Workshop on Scheme and Functional Programming (Scheme 2010) (2010) Earl, C., Might, M., Van Horn, D.: Pushdown control-flow analysis of higher-order programs. In: Proceedings of the 2010 Workshop on Scheme and Functional Programming (Scheme 2010) (2010)
4.
Zurück zum Zitat Flanagan, C., Sabry, A., Duba, B., Felleisen, M.: The essence of compiling with continuations. ACM SIGPLAN Not. 28(6), 237–247 (1993)CrossRef Flanagan, C., Sabry, A., Duba, B., Felleisen, M.: The essence of compiling with continuations. ACM SIGPLAN Not. 28(6), 237–247 (1993)CrossRef
6.
Zurück zum Zitat Gabriel, R.P.: Performance and Evaluation of LISP Systems, vol. 263. MIT press, Cambridge (1985) Gabriel, R.P.: Performance and Evaluation of LISP Systems, vol. 263. MIT press, Cambridge (1985)
7.
Zurück zum Zitat Gilray, T., Adams, M.D., Might, M.: Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, 18–22 September 2016, pp. 407–420 (2016) Gilray, T., Adams, M.D., Might, M.: Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, 18–22 September 2016, pp. 407–420 (2016)
8.
Zurück zum Zitat Gilray, T., Lyde, S., Adams, M.D., Might, M., Horn, D.V.: Pushdown control-flow analysis for free. In: Proceedings of the 43th Annual ACM Symposium on the Principles of Programming Languages (POPL 2016) (2016) Gilray, T., Lyde, S., Adams, M.D., Might, M., Horn, D.V.: Pushdown control-flow analysis for free. In: Proceedings of the 43th Annual ACM Symposium on the Principles of Programming Languages (POPL 2016) (2016)
9.
Zurück zum Zitat Johnson, J.I., Labich, N., Might, M., Van Horn, D.: Optimizing abstract abstract machines. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, USA, 25–27 September 2013, pp. 443–454 (2013) Johnson, J.I., Labich, N., Might, M., Van Horn, D.: Optimizing abstract abstract machines. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Boston, MA, USA, 25–27 September 2013, pp. 443–454 (2013)
10.
Zurück zum Zitat Johnson, J.I., Van Horn, D.: Abstracting abstract control. In: Proceedings of the 10th ACM Symposium on Dynamic languages, pp. 11–22. ACM (2014) Johnson, J.I., Van Horn, D.: Abstracting abstract control. In: Proceedings of the 10th ACM Symposium on Dynamic languages, pp. 11–22. ACM (2014)
11.
Zurück zum Zitat Liang, S., Might, M., Horn, D.V.: Anadroid: Malware analysis of android with user-supplied predicates. Electr. Notes Theor. Comput. Sci. 311, 3–14 (2015)MathSciNetCrossRef Liang, S., Might, M., Horn, D.V.: Anadroid: Malware analysis of android with user-supplied predicates. Electr. Notes Theor. Comput. Sci. 311, 3–14 (2015)MathSciNetCrossRef
13.
Zurück zum Zitat Might, M., Shivers, O.: Improving flow analyses via \(\gamma \)CFA: abstract garbage collection and counting. ACM SIGPLAN Not. 41, 13–25 (2006)CrossRef Might, M., Shivers, O.: Improving flow analyses via \(\gamma \)CFA: abstract garbage collection and counting. ACM SIGPLAN Not. 41, 13–25 (2006)CrossRef
15.
Zurück zum Zitat Nguyen, P.C., Gilray, T., Tobin-Hochstadt, S., Horn, D.V.: Soft contract verification for higher-order stateful programs. PACMPL 2(POPL), 51:1–51:30 (2018) Nguyen, P.C., Gilray, T., Tobin-Hochstadt, S., Horn, D.V.: Soft contract verification for higher-order stateful programs. PACMPL 2(POPL), 51:1–51:30 (2018)
16.
Zurück zum Zitat Nicolay, J., Noguera, C., Roover, C.D., Meuter, W.D.: Determining dynamic coupling in JavaScript using object type inference. In: Proceedings of the Thirteenth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2013), pp. 126–135 (2013) Nicolay, J., Noguera, C., Roover, C.D., Meuter, W.D.: Determining dynamic coupling in JavaScript using object type inference. In: Proceedings of the Thirteenth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2013), pp. 126–135 (2013)
17.
Zurück zum Zitat Nicolay, J., Spruyt, V., De Roover, C.: Static detection of user-specified security vulnerabilities in client-side JavaScript. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 3–13. ACM (2016) Nicolay, J., Spruyt, V., De Roover, C.: Static detection of user-specified security vulnerabilities in client-side JavaScript. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 3–13. ACM (2016)
21.
Zurück zum Zitat Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Technical report, New York University, Department of Computer Science (1978) Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Technical report, New York University, Department of Computer Science (1978)
22.
Zurück zum Zitat Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, Carnegie Mellon University Pittsburgh, PA (1991) Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, Carnegie Mellon University Pittsburgh, PA (1991)
23.
Zurück zum Zitat Stievenart, Q., Nicolay, J., De Meuter, W., De Roover, C.: Detecting concurrency bugs in higher-order programs through abstract interpretation. In: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, pp. 232–243. ACM (2015) Stievenart, Q., Nicolay, J., De Meuter, W., De Roover, C.: Detecting concurrency bugs in higher-order programs through abstract interpretation. In: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, pp. 232–243. ACM (2015)
24.
Zurück zum Zitat Stiévenart, Q., Nicolay, J., De Meuter, W., De Roover, C.: Mailbox abstractions for static analysis of actor programs. In: 31st European Conference on Object-Oriented Programming, ECOOP 2017, pp. 25:1–25:30 (2017) Stiévenart, Q., Nicolay, J., De Meuter, W., De Roover, C.: Mailbox abstractions for static analysis of actor programs. In: 31st European Conference on Object-Oriented Programming, ECOOP 2017, pp. 25:1–25:30 (2017)
25.
Zurück zum Zitat Van Horn, D., Might, M.: Abstracting abstract machines. ACM SIGPLAN Not. 45, 51–62 (2010)CrossRef Van Horn, D., Might, M.: Abstracting abstract machines. ACM SIGPLAN Not. 45, 51–62 (2010)CrossRef
Metadaten
Titel
Effect-Driven Flow Analysis
verfasst von
Jens Nicolay
Quentin Stiévenart
Wolfgang De Meuter
Coen De Roover
Copyright-Jahr
2019
DOI
https://doi.org/10.1007/978-3-030-11245-5_12