A Posteriori Soundness for Non-deterministic Abstract Interpretations

摘要

An abstract interpretation's resource-allocation policy (e.g.,one heap summary node per allocation site) largely determines bothits speed and precision. Historically, context has driven allocation poli-cies, and as a result, these policies are said to determine the "context-sensitivity" of the analysis. This work gives analysis designers newfoundfreedom to manipulate speed and precision by severing the link betweenallocation policy and context-sensitivity: abstract allocation policies maybe unhinged not only from context, but also from even a predefined cor-respondence with a concrete allocation policy. We do so by proving thatabstract allocation policies can be made non-deterministic without sac-rificing correctness; this non-determinism permits precision-guided allo-cation policies previously assumed to be unsafe. To prove correctness, weintroduce the notion of a posteriori soundness for an analysis. A proof ofa posteriori soundness differs from a standard proof of soundness in thatthe abstraction maps used in an a posteriori proof cannot be constructeduntil after an analysis has been run. Delaying construction allows themto be built so as to justify the decisions made by non-determinism. Thecrux of the a posteriori soundness theorem is to demonstrate that ajustifying abstraction map can always be constructed.