Advertisement

Effect-Driven Flow Analysis

  • Jens NicolayEmail author
  • Quentin StiévenartEmail author
  • Wolfgang De MeuterEmail author
  • Coen De RooverEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11388)

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.

Keywords

Program analysis Static analysis Abstract interpretation Effects 

Notes

Acknowledgments

Jens Nicolay is funded by the SeCloud project sponsored by Innoviris, the Brussels Institute for Research and Innovation.

References

  1. 1.
    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)Google Scholar
  2. 2.
    Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159–179. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45937-5_13CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Flanagan, C., Sabry, A., Duba, B., Felleisen, M.: The essence of compiling with continuations. ACM SIGPLAN Not. 28(6), 237–247 (1993)CrossRefGoogle Scholar
  5. 5.
    Fulgham, B., Gouy, I.: The computer language benchmarks game (2009). http://shootout.alioth.debian.org
  6. 6.
    Gabriel, R.P.: Performance and Evaluation of LISP Systems, vol. 263. MIT press, Cambridge (1985)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Johnson, J.I., Van Horn, D.: Abstracting abstract control. In: Proceedings of the 10th ACM Symposium on Dynamic languages, pp. 11–22. ACM (2014)Google Scholar
  11. 11.
    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)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Might, M., Manolios, P.: A posteriori soundness for non-deterministic abstract interpretations. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 260–274. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-93900-9_22CrossRefzbMATHGoogle Scholar
  13. 13.
    Might, M., Shivers, O.: Improving flow analyses via \(\gamma \)CFA: abstract garbage collection and counting. ACM SIGPLAN Not. 41, 13–25 (2006)CrossRefGoogle Scholar
  14. 14.
    Might, M., Van Horn, D.: A family of abstract interpretations for static analysis of concurrent higher-order programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 180–197. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-23702-7_16CrossRefGoogle Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    Nicolay, J., Stiévenart, Q., De Meuter, W., De Roover, C.: Purity analysis for JavaScript through abstract interpretation. J. Softw. Evol. Process (2017).  https://doi.org/10.1002/smr.1889Google Scholar
  19. 19.
    Nielson, F., Nielson, H.R., Hankin, C.: Algorithms. Principles of Program Analysis, pp. 365–392. Springer, Heidelberg (1999).  https://doi.org/10.1007/978-3-662-03811-6_6CrossRefzbMATHGoogle Scholar
  20. 20.
    Nielson, F., Nielson, H.R., Hankin, C.: Type and effect systems. Principles of Program Analysis, pp. 283–363. Springer, Heidelberg (1999).  https://doi.org/10.1007/978-3-662-03811-6_5CrossRefzbMATHGoogle Scholar
  21. 21.
    Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Technical report, New York University, Department of Computer Science (1978)Google Scholar
  22. 22.
    Shivers, O.: Control-flow analysis of higher-order languages. Ph.D. thesis, Carnegie Mellon University Pittsburgh, PA (1991)Google Scholar
  23. 23.
    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)Google Scholar
  24. 24.
    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)Google Scholar
  25. 25.
    Van Horn, D., Might, M.: Abstracting abstract machines. ACM SIGPLAN Not. 45, 51–62 (2010)CrossRefGoogle Scholar
  26. 26.
    Vardoulakis, D., Shivers, O.: CFA2: a context-free approach to control-flow analysis. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 570–589. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-11957-6_30CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Software Languages LabVrije Universiteit BrusselBrusselsBelgium

Personalised recommendations