Efficient and precise sharing domains for logic programs

Abstract

Sharing information between logical variables is crucial for a lot of analyses of logic programs, e.g., freeness analysis, detection of And-parallelism, and occur-check. Therefore, the development of accurate sharing domains has attracted a lot of research. The sharing domain bf JL of Jacobs/Langen, which represents substitutions by powersets of variables, is considered one of the most precise sharing domains. However, it is too inefficient in practice; lots of programs cannot be analyzed in reasonable time. Improvements of bf JL, by adding auxiliary information like linearity, suffer from the same inefficiency, too. To improve upon this situation, we systematically derived a new sharing domain mathorddownarrowbf JL from bf JL which represents variables by downward closed powersets of variables. We combined mathorddownarrowbf JL with the groundness domain bf POS. Both bf JL and the new domain mathorddownarrowbf JL+bf POS have been implemented with the help of the Prolog analyzer generator GENA. In order to study the impact of linearity, we also implemented the abstract domains bf JL+bf LIN and mathorddownarrowbf JL+bf POS+bf LIN. The new domains are much more efficient as their counterparts bf JL and bf JL+bf LIN, respectively. Even more important, they can analyze even largest real-world programs in reasonable time. Surprisingly, the new sharing domains seem to have the same precision than bf JL and bf JL+bf LIN in practice.