Abstract
We propose a method that transforms a C program manipulating containers using low-level pointer statements into an equivalent program where the containers are manipulated via calls of standard high-level container operations like push_back or pop_front. The input of our method is a C program annotated by a special form of shape invariants which can be obtained from current automatic shape analysers after a slight modification. The resulting program where the low-level pointer statements are summarized into high-level container operations is more understandable and (among other possible benefits) better suitable for program analysis. We have implemented our approach and successfully tested it through a number of experiments with list-based containers, including experiments with simplification of program analysis by separating shape analysis from analysing data-related properties.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Hence, e.g., an implementation of a procedure inserting an element into a sorted list, which includes the search for the element, will not be understood as a single destructive container operation, but rather as a procedure that calls a container iterator in a loop until the right place for the inserted element is found, and then calls a destructive container operation that inserts the given region at a position passed to it as a parameter.
- 2.
In practice, there would typically be many more such statements, seemingly increasing the size of the case studies, but such statements are not an issue for our method.
References
Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)
Chilimbi, T.M., Hill, M.D., Larus, J.R.: Cache-conscious structure layout. In: Proceedings of PLDI 1999, pp. 1–12. ACM (1999)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977, pp. 238–252. ACM (1977)
Cozzie, A., Stratton, F., Xue, H., King, S.T.: Digging for data structures. In: Proceedings of USENIX 2008, pp. 255–266. USENIX Association (2008)
Dekker, R., Ververs, F.: Abstract data structure recognition. In: Proceedings of KBSE 1994, pp. 133–140 (1994)
Demsky, B., Ernst, M.D., Guo, P.J., McCamant, S., Perkins, J.H., Rinard, M.C.: Inference and enforcement of data structure consistency specifications. In: Proceedings of ISSTA 2006, pp. 233–244. ACM (2006)
Dudka, K., Holík, L., Peringer, P., Trtík, M., Vojnar, T.: From low-level pointers to high-level containers. Technical report FIT-TR-2015-03 arXiv:1510.07995, FIT BUT (2015). http://arxiv.org/abs/1510.07995
Dudka, K., Peringer, P., Vojnar, T.: Byte-precise verification of low-level list manipulation. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 215–237. Springer, Heidelberg (2013)
Habermehl, P., Holík, L., Rogalewicz, A., Simácek, J., Vojnar, T.: Forest automata for verification of heap manipulation. Formal Meth. Syst. Des. 41(1), 83–106 (2012)
Haller, I., Slowinska, A., Bos, H.: MemPick: high-level data structure detection in C/C++ binaries. In: Proceedings of WCRE 2013, pp. 32–41 (2013)
Hendren, L.J., Nicolau, A.: Parallelizing programs with recursive data structures. IEEE Trans. Parallel Distrib. Syst. 1(1), 35–47 (1990)
Jump, M., McKinley, K.S.: Dynamic shape analysis via degree metrics. In: Proceedings of ISMM 2009, pp. 119–128. ACM (2009)
Jung, C., Clark, N.: DDT: design and evaluation of a dynamic program analysis for optimizing data structure usage. In: Proceedings of MICRO 2009, pp. 56–66. ACM (2009)
O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)
Parízek, P.: J2BP. http://plg.uwaterloo.ca/~pparizek/j2bp
Parízek, P., Lhoták, O.: Predicate abstraction of java programs with collections. In: Proceedings of OOPSLA 2012, pp. 75–94. ACM (2012)
Pheng, S., Verbrugge, C.: Dynamic data structure analysis for java programs. In: Proceedings of ICPC 2006, pp. 191–201. IEEE Computer Society (2006)
Raman, E., August, D.I.: Recursive data structure profiling. In: Proceedings of MSP 2005, pp. 5–14. ACM (2005)
Raza, M., Calcagno, C., Gardner, P.: Automatic parallelization with separation logic. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 348–362. Springer, Heidelberg (2009)
Sagiv, S., Reps, T.W., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217–298 (2002)
Shaham, R., Kolodner, E.K., Sagiv, S.: On the Effectiveness of GC in Java. In: Proceedings of ISMM 2000, pp. 12–17. ACM (2000)
Vafeiadis, V.: RGSep action inference. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 345–361. Springer, Heidelberg (2010)
White, D.H., Lüttgen, G.: Identifying dynamic data structures by learning evolving patterns in memory. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 354–369. Springer, Heidelberg (2013)
Acknowledgement
This work was supported by the Czech Science Foundation project 14-11384S.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dudka, K., Holík, L., Peringer, P., Trtík, M., Vojnar, T. (2016). From Low-Level Pointers to High-Level Containers. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-662-49122-5_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-49121-8
Online ISBN: 978-3-662-49122-5
eBook Packages: Computer ScienceComputer Science (R0)