Semantic code search via equational reasoning

By Varot Premtoon, James Koppel, Armando Solar-Lezama. 2020

52 citations recorded by the source corpus.

We present a new approach to semantic code search based on equational reasoning, and the Yogo tool implementing this approach. Our approach works by considering not only the dataflow graph of a function, but also the dataflow graphs of all equivalent functions reachable via a set of rewrite rules. In doing so, it can recognize an operation even if it uses alternate APIs, is in a different but mathematically-equivalent form, is split apart with temporary variables, or is interleaved with other code. Furthermore, it can recognize when code is an instance of some higher-level concept such as iterating through a file. Because of this, from a single query, Yogo can find equivalent code in multiple languages. Our evaluation further shows the utility of Yogo beyond code search: encoding a buggy pattern as a Yogo query, we found a bug in Oracle’s Graal compiler which had been missed by a hand-written static analyzer designed for that exact kind of bug. Yogo is built on the Cubix multi-language infrastructure, and currently supports Java and Python.

Subfields: Artificial Intelligence, Information Systems, Software, Code Generation & Program Synthesis, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Information Systems

In Software

In Code Generation & Program Synthesis

In Program Analysis & Verification

Citations in the corpus

egg: Fast and extensible equality saturation (2020, methodology): “…Moura and Bjùrner 2008; Detlefs et al. 2005; Nelson 1980], e-graphs have also been used to power a program optimization technique called equality saturation [Joshi et al. 2002; Nandi et al. 2020; Panchekha et al. 2015; Premtoon et al. 2020; Stepp et al. 2011; Tate et al. 2009; Wang et al. 2020].”
A large-scale benchmark for few-shot program induction and synthesis (2021, methodology): “This was originally used for compiler optimization, but Yogo (Premtoon et al., 2020) uses it for code search — and now also for equivalence-checking.”