Towards Cumulative Abstract Semantics via Handlers

TL;DR

This paper introduces a modular approach to abstract interpretation using scoped effects, enabling flexible, composable semantic analysis by separating syntax handling from semantic domain effects.

Contribution

It proposes a novel framework leveraging handlers for cumulative abstract semantics, enhancing modularity and flexibility in interpreters and static analyses.

Findings

Enables multiple evaluators from a single interpreter

Facilitates combining different path- and flow-sensitive analyses

Improves modularity and elegance of abstract interpretation implementations

Abstract

We consider the problem of modularizing control flow in a generic abstract interpretation framework. A generic abstract interpretation framework is not truly flexible if it does not allow interpreting with different path- and flow-sensitivities, by going forwards or backwards, and over- or under-approximately. Most interpreters inherently intertwine syntax and semantics, making the implementation antagonistic to modularity. Current approaches to modular designs require the use of complex data structures (e.g., monad transformers), providing modularity but often proving unwieldy (e.g., lifts). We observe that leveraging scoped effects within an interpreter facilitates the accumulation of semantic fragments against a fixed syntax. In this paper, we define cumulative abstract semantics, illustrating the potential for creating multiple dynamic evaluators and static analyses from one interpreter. This modularity is achieved by grouping effects into two categories: syntax elimination and domain-semantic introduction handlers. Our contribution shows the benefits of using effects as an instrument for designing a clean, elegant, and modular abstract interpretation framework.