Programs written in modern languages perform intricate manipulations of containers such as arrays, lists, dictionaries, and sets. We present an interpretation-based framework for automatically inferring relations between the set of values stored in these containers. Relations include inclusion relations over unions and intersections, as well as quantified relationships with scalar variables. We develop an domain constructor that builds a container domain out of a Quantified Union-Intersection Constraint (QUIC) graph parameterized by an arbitrary base domain. We instantiate our domain with a polyhedral base domain and evaluate it on programs extracted from the Python test suite. Over traditional, non-relational domains, we find significant precision imDrovements with minimal performance cost.
展开▼
