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.
翻译:变量共享是逻辑程序静态分析中的一个基本属性,因为它对于确保正确性和提高推断许多有用程序属性时的精度至关重要。这些属性包括模式、确定性、非失败性、成本等。这推动了大量关于开发抽象域以改进共享分析精度和性能的工作。这些工作大多围绕集合共享域家族展开,因为它们提供了高精度。然而,这是有代价的:它们扩展到广泛的实际程序的可扩展性仍然具有挑战性,这阻碍了它们的更广泛采用。在这项工作中,我们不是定义新的共享抽象域,而是专注于开发可以整合到分析器中的技术,以解决已知影响这些域效率的方面(例如变量数量),同时不影响精度。这些技术灵感来源于编译器优化中使用的其他技术,如表达式重组和变量修剪。我们提出了几种此类技术,并对来自生产代码和经典基准测试的超过1100个程序模块进行了广泛的实验评估。这包括Spectector缓存分析器、s(CASP)系统、Ciao系统的库、LPdoc文档生成器、PLAI分析器本身等。实验结果非常令人鼓舞:我们获得了显著的加速,更重要的是,需要超时的模块数量减少了一半。因此,可以在合理时间内精确分析的程序数量大大增加。