An Abstract Domain Combinator for Separately Conjoining Memory Abstractions

International audienceThe breadth and depth of heap properties that can be inferred by theunion of today’s shape analyses is quite astounding. Yet, achieving scalabilitywhile supporting a wide range of complex data structures in a generic way remainsa long-standing challenge. In this paper, we propose a way to side-stepthis issue by defining a generic abstract domain combinator for combining memoryabstractions on disjoint regions. In essence, our abstract domain constructionis to the separating conjunction in separation logic as the reduced product constructionis to classical, non-separating conjunction. This approach eases the designof the analysis as memory abstract domains can be re-used by applying ourseparating conjunction domain combinator. And more importantly, this combinatorenables an analysis designer to easily create a combined domain that appliescomputationally-expensive abstract domains only where it is required