Abstract
Writing heap manipulating programs is hard. Even though the high-level algorithms may be simple, it is often tedious to express them using low-level operations. We present a new tool — Synlip — that uses expression of intent in the form of concrete examples drawn using box-and-arrow diagrams to synthesize heap-manipulations automatically. Instead of modeling the concrete examples in a monolithic manner, Synlip attempts to extract a set of patterns of manipulation that can be applied repeatedly to construct such programs. It, then, attempts to infer these patterns as linear transformations, leveraging the power of ILP solvers for program synthesis.
In contrast to many current tools, Synlip does not need a bound on the number of statements and the number of temporaries to be used in the desired program. Also, it is almost insensitive to the size of the concrete examples and, thus, tends to be scalable. Synlip was found to be quite fast; it takes less than 10 seconds for most of our benchmark tasks spanning data-structures like singly and doubly linked-lists, AVL trees and binary search trees.
The first author is now with Flipkart, India.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
GNU Octave. https://www.gnu.org/software/octave/
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)
Ganapathy, V., Jha, S., Chandler, D., Melski, D., Vitek, D.: Buffer overrun detection using linear programming and static analysis. In: CCS 2003, pp. 345–354 (2003)
Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. Int. J. Softw. Tools Technol. Transf. 15, 455–474 (2013)
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL 2004, pp. 330–341 (2004)
Roy, S.: From concrete examples to heap manipulating programs. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 126–149. Springer, Heidelberg (2013)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: POPL 1999 (1999)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)
Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 574–592. Springer, Heidelberg (2013)
Singh, R., Solar-Lezama, A.: Synthesizing data structure manipulations from storyboards. In: ESEC/FSE 2011, pp. 289–299 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garg, A., Roy, S. (2015). Synthesizing Heap Manipulations via Integer Linear Programming. In: Blazy, S., Jensen, T. (eds) Static Analysis. SAS 2015. Lecture Notes in Computer Science(), vol 9291. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48288-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-662-48288-9_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48287-2
Online ISBN: 978-3-662-48288-9
eBook Packages: Computer ScienceComputer Science (R0)