A Categorical Basis for Robust Program Analysis

TL;DR

This paper introduces a categorical framework for analyzing and designing robust program analyses, ensuring predictable results under program transformations.

Contribution

It provides a unified categorical language for robustness and a general recipe for designing analyses that are inherently robust.

Findings

Existing analyses like loop summarization are instances of the proposed recipe.

Robustness can be characterized by structure-preserving functors in the categorical model.

Robust operators lead to analyses that behave predictably under refactoring.

Abstract

Users of program analyses expect that results change predictably in response to changes in their programs, but many analyses fail to provide such robustness. This paper introduces a theoretical framework that provides a unified language to articulate robustness properties. By modeling programs and their properties as objects in a category, diverse notions of robustness-from variable renaming to semantic refinement and structural transformation-can be characterized as structure-preserving functors. Beyond formulating the meaning of robustness, this paper provides methods for achieving it. The first is a general recipe for designing robust analyses, by lifting a sound and robust analysis from a restricted (sub-Turing) model of computation to a sound and robust analysis for general programs. This recipe demystifies the design of several existing loop summarization and termination analyses by showing they are instantiations of this general recipe, and furthermore elucidates their robustness properties. The second is a characterization of a sense in which an algebraic program analysis is robust, provided that it is comprised of robust operators. In particular, we show that such analyses behave predictably under common refactoring patterns, such as variable renaming and loop unrolling.