Finding errors from reverse-engineered equality models using a constraint solver

Java objects are required to honor an equality contract in order to participate in standard collection data structures such as List, Set, and Map. In practice, the implementation of equality can be error prone, resulting in subtle bugs. We present a checker called EQ that is designed to automatically detect such equality implementation bugs. The key to EQ is the automated extraction of a logical model of equality from Java code, which is then checked, using Alloy Analyzer, for contract conformance. We have evaluated EQ on four open-source, production code bases in terms of both scalability and usefulness. We discuss in detail the detected problems, their root causes, and the reasons for false alarms.