AADT: Abstract Abstract Data Types

Proving properties of programs that manipulate compound data structures requires both disjunctive reasoning (e.g., a pointer may target different arrays) and relational reasoning. Existing abstract interpreters struggle to combine both: non-relational designs support modular composition of abstract domains but lose relations, while assignment-based relational designs capture relations but hinder modularity and reuse. We introduce open lattices and abstract abstract datatypes (AADT), a new foundation for building precise and reusable abstract domains for structured values. Open lattices generalize classical lattices by introducing shared symbolic values constrained by an abstract valuation domain, enabling relational reasoning across independently defined abstractions. AADTs are compositional transformers over open lattices that mirror the structure of concrete data types: addresses, records, unions, variants, arrays, and their arbitrary nesting. Because each AADT closely follows the concrete datatype definition, abstract domain operations are modular and easy to reuse or extend. Most AADT transformers that we provide are exact: when the abstract valuation domain is exact, the resulting abstraction is a precise translation of the concrete semantics. This enables applications beyond static analysis, such as counter-example generation. We formalize open lattices and AADTs, present key instances, and implement them in a framework for the analysis of C and binary programs. Our experiments show precision gains over state-of-the-art abstract interpreters, while maintaining comparable analysis times.