Modifications to the data representation of an abstract data type (ADT) can require significant semantic refactoring of the code. Motivated by this observation, this paper presents a new method to automate semantic code refactoring tasks. Our method takes as input the original ADT implementation, a new data representation, and a so-called relational representation invariant (relating the old and new data representations), and automatically generates a new ADT implementation that is semantically equivalent to the original version. Our method is based on counterexample-guided inductive synthesis (CEGIS) but leverages three key ideas that allow it to handle real-world refactoring tasks. First, our approach reduces the underlying relational synthesis problem to a set of (simpler) programming-by-example problems, one for each method in the ADT. Second, it leverages symbolic reasoning techniques, based on logical abduction, to deduce code snippets that should occur in the refactored version. Finally, it utilizes a notion of partial equivalence to make inductive synthesis much more effective in this setting. We have implemented the proposed approach in a new tool called Revamp for automatically refactoring Java classes and evaluated it on 30 Java class mined from Github. Our evaluation shows that Revamp can correctly refactor the entire ADT in 97% of the cases and that it can successfully re-implement 144 out of the 146 methods that require modifications.

@article{paperbot2609,
  title = {Semantic Code Refactoring for Abstract Data Types},
  author = {Shankara Pailoor and Yuepeng Wang and Işıl Dillig},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {POPL},
  year = {2024},
  doi = {10.1145/3632870}
}