On the application of substitution algebra to program unification
Abstract
Many problems in software engineering such as program refactoring, deobfuscation, vulnerability detection, require an efficient toolset for detecting pieces of code that have similar behavior. Current state of art in software clone detection makes it possible to find out only those pieces of code which have the same syntactic structure since. A more profound analysis of functional properties of programs encounters with undecidability of equivalence checking problem for Turing-complete models of computation. To overcome this principal deficiency of modern clone detection techniques we suggest to use equivalence relations on programs that are more strong than functional equivalence. One of such equivalences is a so called logic&term program equivalence introduced by V.E. Itkin in 1972 г. In this paper we build a new algorithm for checking logic&term equivalence of programs. This algorithm is based on the operations for computing the least upper bound and the greatest upper bound in the lattice of finite substitutions. Using this algorithm we also develop a procedure for solving the unification problem for sequential programs, i.e. the problem of computing the most general common instance (specialization) of a given pair of programs (pieces of code).
About the Authors
V. A. Zakharov
ISP RAS, Moscow
Russian Federation
Russian Federation
T. A. Novikova
Faculty of Computational Mathematics and Cybernetics, Lomonosov Moscow State University, Moscow
Russian Federation
Russian Federation
References
1. Lague B., Proulx D., Mayrand J. et al. Assessing the benefits of incorporating function clone detection in a development process // Proceedings of the International Conference on Software Maintenance. — Washington, DC, USA: IEEE Computer Society, 1997.— p. 314–321.
2. Baker B. S. On finding duplication and near-duplication in large software systems // Proceedings of the Second Working Conference on Reverse Engineering. — Washington, DC, USA: IEEE Computer Society, 1995. — p. 86–95.
3. Kontogiannis K. A., Demori R., Merlo E. et al. Pattern matching for clone and concept detection // Journal of Automated Software Engineering.— 1996.— Vol. 3.— p. 108 -125.
4. Li Z., Lu S., Myagmar S., Zhou Y.. Cp-miner: Finding copy-paste and related bugs in large-scale software code // IEEE Transactions on Software Engineering. — 2006. — v. 32, N 3.— p. 176–192.
5. Johnson J. H. Identifying redundancy in source code using fingerprints // Proceedings of the Conference Centre for Advanced Studies on Collaborative research (CASCON). — IBM Press, 1993.— p. 171–183.
6. Фаулер М. Рефакторинг. Улучшение существующего кода. — Символ-Плюс, 2008. — 432 c.
7. Komondoor R., Horwitz S. Using slicing to identify duplication in source code // Proceedings of the 8th International Symposium on Static Analysis. — Springer-Verlag, 2001. — p. 40–56.
8. Roy C. K., Cordy J. R. A survey on software clone detection research // Technical report TR 2007-541, School of Computing, Queen’s University. — 2007. — v. 115.
9. Robinson J.A. A machine-oriented logic based on the resolution principle // Journal of the ACM. — 1965. — v. 12, N 1 — p. 23_41.
10. Baader F., Snyder W. Unification theory. — Handbook of Automated Reasoning, v. I, Elsevier Science Publishers, 2001. — p. 447–533.
11. Yelick K.A. Generalized approach to equational unification // Technical Report, Massachusetts Institute of Technology Cambridge, MA, USA, 1990.
12. Luckham D.C., Park D.M., Paterson M.S., On formalized computer programs // Journal of Computer and System Science — 1970. — v.4, N 3. — p. 220-249.
13. Itkin V.E., Zwinogrodski Z. On program schemata equivalence // Journal of Computer and System Science. — 1972. — v. 6, N 1. — p. 88-101.
14. Иткин В.Э. Логико-термальная эквивалентность схем программ // Кибернетика. — 1972. — N 1. — с. 5-27.
15. Sabelfeld V.K. The logic-termal equivalence is polynomial-time decidable // Information Processing Letters. — 1980 — v. 10, N 2. — p. 57-62.
16. Eder E. Properties of substitutions and unifications // Journal of Symbolic Computations. — v. 1. — 1985. — p. 31-46.
17. Palamidessi C. Algebraic properties of idempotent substitutions // Lecture Notes in Computer Science — v. 443 — 1990. — p. 386-399.
18. Martelli A., Montanari U. An Efficient Unification Algorithm // Transactions on Programming Languages and Systems (TOPLAS). — 1982. — v.4, N 2. — p. 258-282.
19. Plotkin G.D. A note on inductive generalization // Machine Intelligence. — 1970. — v. 5, N 1. — p. 153-163.
20. Sorensen M. H., Gluck. R. An algorithm of generalization in positive supercompilation // Proceedings of the 1995 International Symposium on Logic Programming._MIT Press. — 1995. — p. 465-479.
21. Bulychev P., Kostylev E., Zakharov V. Anti-unification algorithms and their applications in program analysis // Proceedings of the 7th International Conference “Perspectives of System Informatics”, June 15-19, 2009, Novosibirsk. — 2009. — p. 82-89.
22. Захаров В.А., Костылев Е.В. О сложности задачи антиунификации // Дискретная математика. — 2008. — т. 20, N 1. — с. 131-144.
23. Zakharov V.A. On the refinement of logic programs by means of anti-unification // Proceedings of the 2nd Panhellenic Logic Symposium, Delphi, Greece. — 1999. — p. 219-224.
24. Котов В.Е., Сабельфельд В.К. Теория схем программ. — М.:Наука, 1991. — 348 с.
Review
For citations:
Zakharov V.A., Novikova T.A. On the application of substitution algebra to program unification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2011;21. (In Russ.)
Email this article 