CW 615
Ilya Sergey, Jan Midtgaard and Dave ClarkeDominance analysis via ownership types and abstract interpretation
Abstract
Ownership types provide a declarative way to statically structure the topology of the heap and control aliasing in object-oriented programs. However, the relation between systematically derived static program analyses by abstract interpretation and semantic properties enforced by ownership types has not yet been investigated. In this work we build a framework to statically compute an abstract object dominance tree, based on the information provided by ownership types in the context of the owners-as-dominators policy. We develop a series of concrete and abstract domains that enable us to abstract a tree-like structure in a way that respects the ancestor relation between particular nodes of the tree and prove them to be Galois connections. We then plug the developed domains into a traditional abstract interpretation-based points-to analysis. The resulting abstract semantics is derived systematically from the concrete transition relation instrumented for tree computation and proven to be sound. The presented framework is tunable concerning polyvariance: the resulting abstract tree depends on the underlying context picking strategy.
report.pdf (342K) / mailto: I. Sergey