Parametrizing Program Analysis by Lifting to Cardinal Power Domains

TL;DR

This paper introduces a method to create parametric program analyses using the Cardinal power domain, enabling analysis outputs to depend functionally on inputs, demonstrated with a groundness analysis of logic programs.

Contribution

It proposes a novel approach to parametrize existing analyses via the Cardinal power domain, enhancing flexibility without significant computational overhead.

Findings

Parametric analysis captures functional dependencies of output on input.

Prototype implementation shows negligible extra cost.

Method generalizes to other analyses beyond groundness.

Abstract

A parametric analysis is an analysis whose input and output are parametrized with a number of parameters which can be instantiated to abstract properties after analysis is completed. This paper proposes to use Cousot and Cousot's Cardinal power domain to capture functional dependencies of analysis output on its input and obtain a parametric analysis by parametrizing a non-parametric base analysis. We illustrate the method by parametrizing a $\pos$ based groundness analysis of logic programs to a parametric groundness analysis. In addition, a prototype implementation shows that generality of the parametric groundness analysis comes with a negligible extra cost.