Advertisement

Inferring Grammatical Summaries of String Values

  • Se-Won Kim
  • Wooyoung Chin
  • Jimin Park
  • Jeongmin Kim
  • Sukyoung Ryu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)

Abstract

We present a new kind of static analysis that infers grammatical summaries of string values. We are given a context-free grammar and a program which contains string expressions whose values should be partial sentences of the grammar. A grammatical summary of an expression is a vocabulary string of the grammar that derives all the possible string values of the expression. Our analysis automatically finds out such grammatical summaries. We design the analysis using abstract interpretation framework making it pluggable into conventional data-flow analysis frameworks.

In addition to the theoretical foundation of the analysis, we present how we make the analysis computable and tractable. While inferring grammatical summaries of a string expression often results in an infinite number of summaries, we make the inference computable by using a CFL-reachability algorithm and finite state automata representation. Additionally, we make the analysis more tractable by several optimization techniques such as keeping only relevant summaries and using two-level grammars. These techniques achieve huge speedup in our experiments.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1–18. Springer, Heidelberg (2003), http://www.brics.dk/JSA/ CrossRefGoogle Scholar
  2. 2.
    Cook., W.R., Rai, S.: Safe query objects: Statically typed objects as remotely executable queries. In: Proceedings of the 27th International Conference on Software Engineering (2005)Google Scholar
  3. 3.
    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 4th ACM Symposium on Principles of Programming Languages (1977)Google Scholar
  4. 4.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM Symposium on Principles of Programming Languages (1979)Google Scholar
  5. 5.
    Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Doh, K.-G., Kim, H., Schmidt, D.A.: Abstract parsing: Static analysis of dynamically generated string output using LR-parsing technology. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 256–272. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  7. 7.
    Gould, C., Su, Z., Devanbu, P.T.: Static checking of dynamically generated queries in database applications. In: Proceedings of the 26th International Conference on Software Engineering (2004)Google Scholar
  8. 8.
    Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238–255. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  9. 9.
    PLRG @ KAIST. SAFE: Scalable Analysis Framework for ECMAScript, http://safe.kaist.ac.kr
  10. 10.
    Kim, S.-W., Choe, K.-M.: String analysis as an abstract interpretation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 294–308. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 11.
    Kirkegaard, C., Møller, A.: Static Analysis for Java Servlets and JSP. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 336–352. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  12. 12.
    Lee, H., Won, S., Jin, J., Cho, J., Ryu, S.: SAFE: Formal specification and implementation of a scalable analysis framework for ECMAScript. In: Proceedings of the 2012 International Workshop on Foundations of Object-Oriented Languages (2012)Google Scholar
  13. 13.
    Minamide, Y.: Static approximation of dynamically generated web pages. In: Proceedings of the 14th International Conference on World Wide Web (2005)Google Scholar
  14. 14.
    Minamide, Y., Tozawa, A.: XML validation for context-free grammars. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 357–373. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Møller, A., Schwarz, M.: HTML validation of context-free languages. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 426–440. Springer, Heidelberg (2011)Google Scholar
  16. 16.
    Reps, T.W., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of the 22nd ACM Symposium on Principles of Programming Languages (1995)Google Scholar
  17. 17.
    Thiemann, P.: Grammar-based analysis of string expressions. In: Proceedings of the 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (2005)Google Scholar
  18. 18.
    Valiant, L.G.: General context-free recognition in less than cubic time. J. Comput. Syst. Sci. 10(2), 308–315 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Wassermann, G., Gould, C., Su, Z., Devanbu, P.T.: Static checking of dynamically generated queries in database applications. ACM Trans. Softw. Eng. Methodol. 16(4) (2007)Google Scholar
  20. 20.
    Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (2007)Google Scholar
  21. 21.
    Yu, F., Alkhalaf, M., Bultan, T.: Stranger: An automata-based string analysis tool for PHP. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 154–157. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  22. 22.
    Yu, F., Bultan, T., Cova, M., Ibarra, O.H.: Symbolic string verification: An automata-based approach. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 306–324. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Yu, F., Bultan, T., Hardekopf, B.: String abstractions for string verification. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 20–37. Springer, Heidelberg (2011)Google Scholar
  24. 24.
    Yu, F., Bultan, T., Ibarra, O.H.: Symbolic string verification: Combining string analysis and size analysis. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 322–336. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  25. 25.
    Yu, F., Bultan, T., Ibarra, O.H.: Relational string verification using multi-track automata. In: Domaratzki, M., Salomaa, K. (eds.) CIAA 2010. LNCS, vol. 6482, pp. 290–299. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Se-Won Kim
    • 1
  • Wooyoung Chin
    • 1
  • Jimin Park
    • 1
  • Jeongmin Kim
    • 1
  • Sukyoung Ryu
    • 1
  1. 1.Department of Computer ScienceKAISTDaejeonSouth Korea

Personalised recommendations