Automatic Memory Management Based on Program Transformation Using Ownership

  • Tatsuya Sonobe
  • Kohei Suenaga
  • Atsushi Igarashi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8858)


We present a type-based program transformation for an imperative programming language with manual memory-management primitives (e.g., malloc and free in C). Our algorithm, given a program with potential memory leaks, inserts memory-deallocating instructions to the program so that the resulting program does not contain memory leaks. We design the algorithm as type reconstruction for an extension of the ownership-based type system by Suenaga and Kobayashi.


Memory leaks Type system Program transformation 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Ajiro, Y., Ueda, K., Cho, K.: Error-correcting source code. In: Maher, M.J., Puget, J.-F. (eds.) CP 1998. LNCS, vol. 1520, pp. 40–54. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  2. 2.
    Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  3. 3.
    Clarke, D.G., Potter, J., Noble, J.: Ownership types for flexible alias protection. In: Freeman-Benson, B.N., Chambers, C. (eds.) OOPSLA, pp. 48–64. ACM (1998)Google Scholar
  4. 4.
    Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  5. 5.
    de Kleer, J., Williams, B.C.: Diagnosing multiple faults. Artif. Intell. 32(1), 97–130 (1987)CrossRefzbMATHGoogle Scholar
  6. 6.
    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  7. 7.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Sarkar, V., Hall, M.W. (eds.) PLDI, pp. 213–223. ACM (2005)Google Scholar
  8. 8.
    Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. Technical Report MSR-TR-2007-39, Microsoft Research (2007)Google Scholar
  9. 9.
    Hastings, R., Joyce, B.: Purify: Fast detection of memory leaks and access errors. In: Proc. of the Winter 1992 USENIX Conference, San Francisco, California, pp. 125–138 (1991)Google Scholar
  10. 10.
    Heine, D.L., Lam, M.S.: A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In: Cytron, R., Gupta, R. (eds.) PLDI, pp. 168–181. ACM (2003)Google Scholar
  11. 11.
    Kernighan, B.W., Ritchie, D.: The C Programming Language, 2nd edn. Prentice-Hall (1988)Google Scholar
  12. 12.
    Khedker, U.P., Sanyal, A., Karkare, A.: Heap reference analysis using access graphs (2007)Google Scholar
  13. 13.
    Könighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: Bjesse, P., Slobodová, A. (eds.) FMCAD, pp. 91–100. FMCAD Inc. (2011)Google Scholar
  14. 14.
    Nethercote, N., Seward, J.: Valgrind: A framework for heavyweight dynamic binary instrumentation. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 89–100. ACM (2007)Google Scholar
  15. 15.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis (2. corr. print). Springer (2005)Google Scholar
  16. 16.
    Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Sen, K., Marinov, D., Agha, G.: CUTE: A concolic unit testing engine for C. In: Wermelinger, M., Gall, H. (eds.) ESEC/SIGSOFT FSE, pp. 263–272. ACM (2005)Google Scholar
  18. 18.
    Shaham, R., Kolodner, E.K., Sagiv, S.: Heap profiling for space-efficient java. In: Burke, M., Soffa, M.L. (eds.) PLDI, pp. 104–113. ACM (2001)Google Scholar
  19. 19.
    Shaham, R., Kolodner, E.K., Sagiv, S.: Estimating the impact of heap liveness information on space consumption in java. In: Boehm, H., Detlefs, D. (eds.) MSP/ISMM, pp. 171–182. ACM (2002)Google Scholar
  20. 20.
    Singh, R., Gulwani, S., Solar-Lezama, A.: Automated feedback generation for introductory programming assignments. In: Boehm, H.-J., Flanagan, C. (eds.) PLDI, pp. 15–26. ACM (2013)Google Scholar
  21. 21.
    Stroustrup, B.: The C++ programming language - special edition, 3rd edn. Addison-Wesley (2007)Google Scholar
  22. 22.
    Suenaga, K., Fukuda, R., Igarashi, A.: Type-based safe resource deallocation for shared-memory concurrency. In: Leavens, G.T., Dwyer, M.B. (eds.) OOPSLA, pp. 1–20. ACM (2012)Google Scholar
  23. 23.
    Suenaga, K., Kobayashi, N.: Fractional ownerships for safe memory deallocation. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 128–143. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  24. 24.
    Terauchi, T.: Checking race freedom via linear programming. In: Proc. of PLDI, pp. 1–10 (2008)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Tatsuya Sonobe
    • 1
  • Kohei Suenaga
    • 1
  • Atsushi Igarashi
    • 1
  1. 1.Kyoto UniversityKyotoJapan

Personalised recommendations