Abstract Environment Trimming

作     者：Jurjo-rivas, Daniel Morales, Jose F. Lopez-garcia, Pedro Hermenegildo, Manuel, V 

作者机构：Univ Politecn Madrid UPM IMDEA Software Inst Madrid Spain IMDEA Software Inst Spanish Council Sci Res Madrid Spain 

出 版 物：《THEORY AND PRACTICE OF LOGIC PROGRAMMING》 

年 卷 期：2024年第24卷第4期

页      面：863-884页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：MICINN [PID2019-108528RB-C21, TED2021-132464B-I00] Tezos foundation 

主　　题：logic programming methodology and applications specification analysis and verification of systems security 

摘      要：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 speedups, 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.