Computing Program Equivalence Based on a Hierarchy of Program Semantics and Related Canonical Representations

摘要

Methods, systems, and articles of manufacture for computing program equivalence based on a hierarchy of program semantics and related canonical representations are provided herein. A method includes defining a program semantic representation for a first program; generating a search query based on said semantic representation for the first program; executing said search query against an index of multiple programs to determine a set of candidate programs among the multiple programs, wherein said index comprises a program semantic representation defined for each of the multiple programs; and identifying one or more programs among the set of candidate programs that match the first program by performing one or more comparisons, across the set of candidate programs, of a canonical representation associated with each program in the identified set of candidate programs to a canonical representation associated with the first program.

主权项

1. A method comprising:
defining a program semantic representation for a first program; generating a search query based on said program semantic representation; executing said search query against an index of multiple programs to determine a set of candidate programs among the multiple programs, wherein said index comprises a program semantic representation for each of the multiple programs; refactoring (i) the first program and (ii) each program in the set of candidate programs to transform each of (i) the first program and (ii) each respective program in the set of candidate programs to a canonical representation, wherein said refactoring is based on (a) one or more patterns of program equivalence and (b) one or more canonicalization operators; and identifying one or more programs among the set of candidate programs that match the first program by performing one or more comparisons, across the set of candidate programs, of the canonical representation associated with each respective program in the identified set of candidate programs to the canonical representation associated with the first program; wherein at least one of said defining, said generating, said executing, said refactoring, and said identifying is carried out by a computing device.