Optimal matching for sharing and linearity analysis
Gianluca Amato, Francesca Scozzari
TL;DR
The paper tackles the problem of deriving optimal abstract matching operators for sharing and linearity in static analysis of logic programs. It extends the ${ShLin^{\omega}}$ framework to goal-dependent analysis and proves an optimal matching operator for ${ShLin^{\omega}}$, from which optimal operators for ${ShLin^2}$ and ${Sharing\times Lin}$ are derived. The results ensure maximal precision in backward unification via matching and provide practical optimization techniques for real analyzers. Overall, the work enhances precision and efficiency of goal-driven analyses in logic programming and informs the design of combined sharing/linearity domains.
Abstract
Static analysis of logic programs by abstract interpretation requires designing abstract operators which mimic the concrete ones, such as unification, renaming and projection. In the case of goal-driven analysis, where goal-dependent semantics are used, we also need a backward-unification operator, typically implemented through matching. In this paper we study the problem of deriving optimal abstract matching operators for sharing and linearity properties. We provide an optimal operator for matching in the domain ${\mathtt{ShLin}^ω}$, which can be easily instantiated to derive optimal operators for the domains ${\mathtt{ShLin}^{2}}$ by Andy King and the reduced product $\mathtt{Sharing} \times \mathtt{Lin}$.