Skip to main content

2017 | OriginalPaper | Buchkapitel

Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization

verfasst von : Hao Tang, Di Wang, Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, Lu Zhang

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

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

search-config
loading …

Abstract

Library summarization is an effective way to accelerate the analysis of client code. However, information about the client is unknown at the library summarization, preventing complete summarization of the library. An existing approach utilizes tree-adjoining languages (TALs) to provide conditional summaries, enabling the summarization of a library under certain premises. However, the use of TAL imposes several problems, preventing a complete summarization of a library and reducing the efficiency of the analysis.
In this paper we propose a new conditional summarization technique based on the context-free language (CFL) reachability analysis. Our technique overcomes the above two limitations of TAL, and is more accessible since CFL reachability is much more efficient and widely-used than TAL reachability. Furthermore, to overcome the high cost from premise combination, we also provide a technique to confine the number of premises while maintaining full summarization of the library.
We empirically compared our approach with the state-of-art TAL conditional summarization technique on 12 Java benchmark subjects from the SPECjvm2008 benchmark suite. The results demonstrate that our approach is able to significantly outperform TAL on both efficiency and 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!

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!

Fußnoten
4
Please note the statistics are different from the TALCRA paper [39] because that evaluation was performed on an early version of the TALCRA tool that built the graph differently.
 
Literatur
1.
Zurück zum Zitat Arzt, S., Bodden, E.: Stubdroid: automatic inference of precise data-flow summaries for the android framework. In: Proceedings of ICSE, pp. 725–735 (2016) Arzt, S., Bodden, E.: Stubdroid: automatic inference of precise data-flow summaries for the android framework. In: Proceedings of ICSE, pp. 725–735 (2016)
2.
Zurück zum Zitat Bastani, O., Anand, S., Aiken, A.: Specification inference using context-free language reachability. In: Proceedings of POPL, pp. 553–566 (2015) Bastani, O., Anand, S., Aiken, A.: Specification inference using context-free language reachability. In: Proceedings of POPL, pp. 553–566 (2015)
4.
Zurück zum Zitat Das, A., Lahiri, S.K., Lal, A., Li, Y.: Angelic verification: precise verification modulo unknowns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 324–342. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_19CrossRef Das, A., Lahiri, S.K., Lal, A., Li, Y.: Angelic verification: precise verification modulo unknowns. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 324–342. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-21690-4_​19CrossRef
5.
Zurück zum Zitat Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1995. LNCS, vol. 952, pp. 77–101. Springer, Heidelberg (1995). doi:10.1007/3-540-49538-X_5CrossRef Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Tokoro, M., Pareschi, R. (eds.) ECOOP 1995. LNCS, vol. 952, pp. 77–101. Springer, Heidelberg (1995). doi:10.​1007/​3-540-49538-X_​5CrossRef
6.
Zurück zum Zitat Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: Proceedings of PLDI, pp. 567–577 (2011) Dillig, I., Dillig, T., Aiken, A., Sagiv, M.: Precise and compact modular procedure summaries for heap manipulating programs. In: Proceedings of PLDI, pp. 567–577 (2011)
7.
Zurück zum Zitat Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Proceedings of PASTE, pp. 54–61 (2001) Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Proceedings of PASTE, pp. 54–61 (2001)
8.
Zurück zum Zitat Itzhaky, S., Bjørner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 35–51. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_3CrossRef Itzhaky, S., Bjørner, N., Reps, T., Sagiv, M., Thakur, A.: Property-directed shape analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 35–51. Springer, Heidelberg (2014). doi:10.​1007/​978-3-319-08867-9_​3CrossRef
9.
10.
Zurück zum Zitat Kodumal, J., Aiken, A.: The set constraint/CFL reachability connection in practice. In: Proceedings of PLDI, pp. 207–218 (2004) Kodumal, J., Aiken, A.: The set constraint/CFL reachability connection in practice. In: Proceedings of PLDI, pp. 207–218 (2004)
11.
Zurück zum Zitat Komondoor, R., Ramalingam, G.: Recovering data models via guarded dependences. In: Proceedings of WCRE, pp. 110–119 (2007) Komondoor, R., Ramalingam, G.: Recovering data models via guarded dependences. In: Proceedings of WCRE, pp. 110–119 (2007)
12.
Zurück zum Zitat Kulkarni, S., Mangal, R., Zhang, X., Naik, M.: Accelerating program analyses by cross-program training. In: Proceedings of OOPSLA, pp. 359–377 (2016) Kulkarni, S., Mangal, R., Zhang, X., Naik, M.: Accelerating program analyses by cross-program training. In: Proceedings of OOPSLA, pp. 359–377 (2016)
13.
Zurück zum Zitat Lattner, C., Lenharth, A., Adve, V.: Making context-sensitive points-to analysis with heap cloning practical for the real world. In: Proceedings of PLDI, pp. 278–289 (2007) Lattner, C., Lenharth, A., Adve, V.: Making context-sensitive points-to analysis with heap cloning practical for the real world. In: Proceedings of PLDI, pp. 278–289 (2007)
15.
Zurück zum Zitat Lochbihler, A., Snelting, G.: On temporal path conditions in dependence graphs. ASE 16(2), 263–290 (2009) Lochbihler, A., Snelting, G.: On temporal path conditions in dependence graphs. ASE 16(2), 263–290 (2009)
16.
Zurück zum Zitat Macedo, H.D., Touili, T.: Mining malware specifications through static reachability analysis. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 517–535. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40203-6_29CrossRef Macedo, H.D., Touili, T.: Mining malware specifications through static reachability analysis. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 517–535. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40203-6_​29CrossRef
17.
Zurück zum Zitat Madhavan, R., Ramalingam, G., Vaswani, K.: Modular heap analysis for higher-order programs. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 370–387. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33125-1_25CrossRef Madhavan, R., Ramalingam, G., Vaswani, K.: Modular heap analysis for higher-order programs. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 370–387. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-33125-1_​25CrossRef
18.
Zurück zum Zitat Milanova, A., Huang, W., Dong, Y.: CFL-reachability and context-sensitive integrity types. In: Proceedings of PPPJ, pp. 99–109 (2014) Milanova, A., Huang, W., Dong, Y.: CFL-reachability and context-sensitive integrity types. In: Proceedings of PPPJ, pp. 99–109 (2014)
19.
Zurück zum Zitat Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: Proceedings of POPL, pp. 327–338 (2007) Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: Proceedings of POPL, pp. 327–338 (2007)
20.
Zurück zum Zitat Pratikakis, P., Foster, J.S., Hicks, M.: Existential label flow inference via CFL reachability. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 88–106. Springer, Heidelberg (2006). doi:10.1007/11823230_7CrossRef Pratikakis, P., Foster, J.S., Hicks, M.: Existential label flow inference via CFL reachability. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 88–106. Springer, Heidelberg (2006). doi:10.​1007/​11823230_​7CrossRef
21.
Zurück zum Zitat Pratikakis, P., Foster, J.S., Hicks, M.W.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: Proceedings of PLDI, pp. 320–331 (2006) Pratikakis, P., Foster, J.S., Hicks, M.W.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: Proceedings of PLDI, pp. 320–331 (2006)
22.
Zurück zum Zitat Ravitch, T., Jackson, S., Aderhold, E., Liblit, B.: Automatic generation of library bindings using static analysis. In: Proceedings of PLDI, pp. 352–362 (2009) Ravitch, T., Jackson, S., Aderhold, E., Liblit, B.: Automatic generation of library bindings using static analysis. In: Proceedings of PLDI, pp. 352–362 (2009)
23.
Zurück zum Zitat Rehof, J., Fähndrich, M.: Type-based flow analysis: from polymorphic subtyping to CFL-reachability. In: Proceedings of POPL, pp. 54–66 (2001) Rehof, J., Fähndrich, M.: Type-based flow analysis: from polymorphic subtyping to CFL-reachability. In: Proceedings of POPL, pp. 54–66 (2001)
24.
Zurück zum Zitat Reps, T.: Shape analysis as a generalized path problem. In: Proceedings of PEPM, pp. 1–11 (1995) Reps, T.: Shape analysis as a generalized path problem. In: Proceedings of PEPM, pp. 1–11 (1995)
25.
Zurück zum Zitat Reps, T.: Program analysis via graph reachability. Inf. Softw. Technol. 40(11–12), 701–726 (1998)CrossRef Reps, T.: Program analysis via graph reachability. Inf. Softw. Technol. 40(11–12), 701–726 (1998)CrossRef
26.
Zurück zum Zitat Reps, T.: Undecidability of context-sensitive data-dependence analysis. TOPLAS 22(1), 162–186 (2000)CrossRef Reps, T.: Undecidability of context-sensitive data-dependence analysis. TOPLAS 22(1), 162–186 (2000)CrossRef
27.
Zurück zum Zitat Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL, pp. 49–61 (1995) Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL, pp. 49–61 (1995)
28.
Zurück zum Zitat Reps, T., Horwitz, S., Sagiv, M., Rosay, G.: Speeding up slicing. In: Proceedings of FSE, pp. 11–20 (1994) Reps, T., Horwitz, S., Sagiv, M., Rosay, G.: Speeding up slicing. In: Proceedings of FSE, pp. 11–20 (1994)
29.
Zurück zum Zitat Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 189–213. Springer, Heidelberg (2003). doi:10.1007/3-540-44898-5_11CrossRefMATH Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 189–213. Springer, Heidelberg (2003). doi:10.​1007/​3-540-44898-5_​11CrossRefMATH
30.
Zurück zum Zitat Rinetzky, N., Poetzsch-Heffter, A., Ramalingam, G., Sagiv, M., Yahav, E.: Modular shape analysis for dynamically encapsulated programs. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 220–236. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71316-6_16CrossRef Rinetzky, N., Poetzsch-Heffter, A., Ramalingam, G., Sagiv, M., Yahav, E.: Modular shape analysis for dynamically encapsulated programs. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 220–236. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-71316-6_​16CrossRef
31.
Zurück zum Zitat Rountev, A., Kagan, S., Marlowe, T.: Interprocedural dataflow analysis in the presence of large libraries. In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol. 3923, pp. 2–16. Springer, Heidelberg (2006). doi:10.1007/11688839_2CrossRef Rountev, A., Kagan, S., Marlowe, T.: Interprocedural dataflow analysis in the presence of large libraries. In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol. 3923, pp. 2–16. Springer, Heidelberg (2006). doi:10.​1007/​11688839_​2CrossRef
32.
Zurück zum Zitat Rountev, A., Ryder, B.G.: Points-to and side-effect analyses for programs built with precompiled libraries. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 20–36. Springer, Heidelberg (2001). doi:10.1007/3-540-45306-7_3CrossRef Rountev, A., Ryder, B.G.: Points-to and side-effect analyses for programs built with precompiled libraries. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 20–36. Springer, Heidelberg (2001). doi:10.​1007/​3-540-45306-7_​3CrossRef
33.
Zurück zum Zitat Rountev, A., Sharp, M., Xu, G.: IDE dataflow analysis in the presence of large object-oriented libraries. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 53–68. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78791-4_4CrossRef Rountev, A., Sharp, M., Xu, G.: IDE dataflow analysis in the presence of large object-oriented libraries. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 53–68. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-78791-4_​4CrossRef
34.
Zurück zum Zitat Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167(1–2), 131–170 (1996)MathSciNetCrossRef Sagiv, M., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167(1–2), 131–170 (1996)MathSciNetCrossRef
35.
Zurück zum Zitat Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. TOSEM 15(4), 410–457 (2006)CrossRef Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. TOSEM 15(4), 410–457 (2006)CrossRef
36.
Zurück zum Zitat Sridharan, M., Gopan, D., Shan, L., Bodík, R.: Demand-driven points-to analysis for Java. In: Proceedings of OOPSLA, pp. 57–76 (2005) Sridharan, M., Gopan, D., Shan, L., Bodík, R.: Demand-driven points-to analysis for Java. In: Proceedings of OOPSLA, pp. 57–76 (2005)
37.
Zurück zum Zitat Sridharan, M., Bodík, R.: Refinement-based context-sensitive points-to analysis for Java. In: Proceedings of PLDI, pp. 387–400 (2006) Sridharan, M., Bodík, R.: Refinement-based context-sensitive points-to analysis for Java. In: Proceedings of PLDI, pp. 387–400 (2006)
38.
Zurück zum Zitat Sukumaran, S., Sreenivas, A., Metta, R.: The dependence condition graph: precise conditions for dependence between program points. Comput. Lang. Syst. Struct. 36(1), 96–121 (2010)MATH Sukumaran, S., Sreenivas, A., Metta, R.: The dependence condition graph: precise conditions for dependence between program points. Comput. Lang. Syst. Struct. 36(1), 96–121 (2010)MATH
39.
Zurück zum Zitat Tang, H., Wang, X., Zhang, L., Xie, B., Zhang, L., Mei, H.: Summary-based context-sensitive data-dependence analysis in presence of callbacks. In: Proceedings of POPL, pp. 83–95 (2015) Tang, H., Wang, X., Zhang, L., Xie, B., Zhang, L., Mei, H.: Summary-based context-sensitive data-dependence analysis in presence of callbacks. In: Proceedings of POPL, pp. 83–95 (2015)
40.
Zurück zum Zitat Tschantz, M.C., Wing, J.M.: Extracting conditional confidentiality policies. In: Proceedings of SEFM, pp. 107–116 (2008) Tschantz, M.C., Wing, J.M.: Extracting conditional confidentiality policies. In: Proceedings of SEFM, pp. 107–116 (2008)
41.
Zurück zum Zitat Xu, G., Rountev, A.: Merging equivalent contexts for scalable heap-cloning-based context-sensitive points-to analysis. In: Proceedings of ISSTA, pp. 225–235 (2008) Xu, G., Rountev, A.: Merging equivalent contexts for scalable heap-cloning-based context-sensitive points-to analysis. In: Proceedings of ISSTA, pp. 225–235 (2008)
42.
Zurück zum Zitat Xu, G., Rountev, A., Sridharan, M.: Scaling CFL-reachability-based points-to analysis using context-sensitive must-not-alias analysis. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 98–122. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03013-0_6CrossRef Xu, G., Rountev, A., Sridharan, M.: Scaling CFL-reachability-based points-to analysis using context-sensitive must-not-alias analysis. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 98–122. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-03013-0_​6CrossRef
43.
Zurück zum Zitat Yannakakis, M.: Graph-theoretic methods in database theory. In: Proceedings of PODS, pp. 230–242 (1990) Yannakakis, M.: Graph-theoretic methods in database theory. In: Proceedings of PODS, pp. 230–242 (1990)
44.
Zurück zum Zitat Zhang, Q., Lyu, M.R., Yuan, H., Su, Z.: Fast algorithms for Dyck-CFL reachability with applications to alias analysis. In: Proceedings of PLDI, pp. 435–446 (2013) Zhang, Q., Lyu, M.R., Yuan, H., Su, Z.: Fast algorithms for Dyck-CFL reachability with applications to alias analysis. In: Proceedings of PLDI, pp. 435–446 (2013)
45.
Zurück zum Zitat Zhang, Q., Su, Z.: Context-sensitive data-dependence analysis via linear conjunctive language reachability. In: Proceedings of POPL, pp. 344–358 (2017) Zhang, Q., Su, Z.: Context-sensitive data-dependence analysis via linear conjunctive language reachability. In: Proceedings of POPL, pp. 344–358 (2017)
46.
Zurück zum Zitat Zhang, X., Mangal, R., Naik, M., Yang, H.: Hybrid top-down and bottom-up interprocedural analysis. In: Proceedings of PLDI, pp. 249–258 (2014) Zhang, X., Mangal, R., Naik, M., Yang, H.: Hybrid top-down and bottom-up interprocedural analysis. In: Proceedings of PLDI, pp. 249–258 (2014)
47.
Zurück zum Zitat Zheng, X., Rugina, R.: Demand-driven alias analysis for C. In: Proceedings of POPL, pp. 351–363 (2008) Zheng, X., Rugina, R.: Demand-driven alias analysis for C. In: Proceedings of POPL, pp. 351–363 (2008)
48.
Zurück zum Zitat Zhu, H., Dillig, T., Dillig, I.: Automated inference of library specifications for source-sink property verification. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 290–306. Springer, Heidelberg (2013). doi:10.1007/978-3-319-03542-0_21CrossRef Zhu, H., Dillig, T., Dillig, I.: Automated inference of library specifications for source-sink property verification. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 290–306. Springer, Heidelberg (2013). doi:10.​1007/​978-3-319-03542-0_​21CrossRef
Metadaten
Titel
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
verfasst von
Hao Tang
Di Wang
Yingfei Xiong
Lingming Zhang
Xiaoyin Wang
Lu Zhang
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-54434-1_33