Abstract Environment Trimming

TL;DR

Set-sharing analyses in logic programming offer high precision for properties like modes and determinacy but suffer from scalability due to potentially exponential sharing abstractions, bounded by $\mathcal{P}^0(V)$. The paper introduces two compiler-inspired techniques—Environment Reassociation (program transformations that fold body literals into smaller-environment auxiliaries) and Abstract Environment Trimming (live-variable-based dynamic domain shrinking during analysis)—to reduce the number of variables in abstract environments while preserving precision. The PLAI Top-Down Analyzer is extended with these approaches, and extensive experiments on over 1100 modules show substantial speed-ups and fewer timeouts, validating the practical impact for production code and large libraries. These results suggest that local, analysis-time and program-structure adaptations can significantly improve the scalability of set-sharing analyses without sacrificing their benefits. The work also identifies avenues for future enhancements, such as a broader notion of live variables across predicate calls.

Abstract

Variable sharing is a fundamental property in the static analysis of logic programs, since it is instrumental for ensuring correctness and increasing precision while inferring many useful program properties. Such properties include modes, determinacy, non-failure, cost, etc. This has motivated significant work on developing abstract domains to improve the precision and performance of sharing analyses. Much of this work has centered around the family of set-sharing domains, because of the high precision they offer. However, this comes at a price: their scalability to a wide set of realistic programs remains challenging and this hinders their wider adoption. In this work, rather than defining new sharing abstract domains, we focus instead on developing techniques which can be incorporated in the analyzers to address aspects that are known to affect the efficiency of these domains, such as the number of variables, without affecting precision. These techniques are inspired in others used in the context of compiler optimizations, such as expression reassociation and variable trimming. We present several such techniques and provide an extensive experimental evaluation of over 1100 program modules taken from both production code and classical benchmarks. This includes the Spectector cache analyzer, the s(CASP) system, the libraries of the Ciao system, the LPdoc documenter, the PLAI analyzer itself, etc. The experimental results are quite encouraging: we have obtained significant speed-ups, and, more importantly, the number of modules that require a timeout was cut in half. As a result, many more programs can be analyzed precisely in reasonable times.

Figures (9)

• Figure 1: qplan/3 predicate and its environment trimming-based transformation.
• Figure 2: Cactus plot aggregating all the benchmarks (1185 modules). Times are in mS.
• Figure 3: Scatter plot comparing absolute analysis times (in mS).
• Figure 4: Scatter plot showing classic analysis time (in mS) vs. speed-up obtained (logscaled base 10).
• Figure 6: Cactus plots aggregating results of analyzing the classic benchmarks set.