Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Disjoint Polymorphism Read chapter Read first chapter

2017 | OriginalPaper | Chapter

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

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

Published in: Programming Languages and Systems

Publisher: Springer Berlin Heidelberg

Log in

Activate our intelligent search to find suitable subject content or patents.

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
previous chapter Commutative Semantics for Probabilistic Programming
next chapter A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Footnotes
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.
 
Literature
1.
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.
Bastani, O., Anand, S., Aiken, A.: Specification inference using context-free language reachability. In: Proceedings of POPL, pp. 553–566 (2015)
3.
4.
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.
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.
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.
Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Proceedings of PASTE, pp. 54–61 (2001)
8.
9.
10.
Kodumal, J., Aiken, A.: The set constraint/CFL reachability connection in practice. In: Proceedings of PLDI, pp. 207–218 (2004)
11.
Komondoor, R., Ramalingam, G.: Recovering data models via guarded dependences. In: Proceedings of WCRE, pp. 110–119 (2007)
12.
Kulkarni, S., Mangal, R., Zhang, X., Naik, M.: Accelerating program analyses by cross-program training. In: Proceedings of OOPSLA, pp. 359–377 (2016)
13.
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)
14.
15.
Lochbihler, A., Snelting, G.: On temporal path conditions in dependence graphs. ASE 16(2), 263–290 (2009)
16.
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.
18.
Milanova, A., Huang, W., Dong, Y.: CFL-reachability and context-sensitive integrity types. In: Proceedings of PPPJ, pp. 99–109 (2014)
19.
Naik, M., Aiken, A.: Conditional must not aliasing for static race detection. In: Proceedings of POPL, pp. 327–338 (2007)
20.
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.
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.
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.
Rehof, J., Fähndrich, M.: Type-based flow analysis: from polymorphic subtyping to CFL-reachability. In: Proceedings of POPL, pp. 54–66 (2001)
24.
Reps, T.: Shape analysis as a generalized path problem. In: Proceedings of PEPM, pp. 1–11 (1995)
25.
Reps, T.: Program analysis via graph reachability. Inf. Softw. Technol. 40(11–12), 701–726 (1998)CrossRef
26.
Reps, T.: Undecidability of context-sensitive data-dependence analysis. TOPLAS 22(1), 162–186 (2000)CrossRef
27.
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL, pp. 49–61 (1995)
28.
Reps, T., Horwitz, S., Sagiv, M., Rosay, G.: Speeding up slicing. In: Proceedings of FSE, pp. 11–20 (1994)
29.
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.
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.
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.
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.
34.
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.
Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. TOSEM 15(4), 410–457 (2006)CrossRef
36.
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.
Sridharan, M., Bodík, R.: Refinement-based context-sensitive points-to analysis for Java. In: Proceedings of PLDI, pp. 387–400 (2006)
38.
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.
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.
Tschantz, M.C., Wing, J.M.: Extracting conditional confidentiality policies. In: Proceedings of SEFM, pp. 107–116 (2008)
41.
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.
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.
Yannakakis, M.: Graph-theoretic methods in database theory. In: Proceedings of PODS, pp. 230–242 (1990)
44.
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.
Zhang, Q., Su, Z.: Context-sensitive data-dependence analysis via linear conjunctive language reachability. In: Proceedings of POPL, pp. 344–358 (2017)
46.
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.
Zheng, X., Rugina, R.: Demand-driven alias analysis for C. In: Proceedings of POPL, pp. 351–363 (2008)
48.
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
Metadata
Title
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Authors
Hao Tang
Di Wang
Yingfei Xiong
Lingming Zhang
Xiaoyin Wang
Lu Zhang
Copyright Year
2017
Publisher
Springer Berlin Heidelberg
Book
Programming Languages and Systems

Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-662-54434-1_33

Premium Partner

    Image Credits