Modular Construction of Shape-Numeric Analyzers

TL;DR

This paper presents a modular framework for static analysis that combines shape and numeric invariants using abstract interpretation, facilitating easier formalization and implementation of complex shape-numeric analyzers.

Contribution

It introduces a modular, expressive abstract interpretation framework for simultaneous shape-numeric analysis, enabling step-by-step abstraction while maintaining high expressiveness.

Findings

The framework allows modular composition of shape and numeric abstractions.

It preserves expressiveness through a step-by-step abstraction of concrete semantics.

The modular design simplifies formalization and implementation of shape-numeric analyzers.

Abstract

The aim of static analysis is to infer invariants about programs that are precise enough to establish semantic properties, such as the absence of run-time errors. Broadly speaking, there are two major branches of static analysis for imperative programs. Pointer and shape analyses focus on inferring properties of pointers, dynamically-allocated memory, and recursive data structures, while numeric analyses seek to derive invariants on numeric values. Although simultaneous inference of shape-numeric invariants is often needed, this case is especially challenging and is not particularly well explored. Notably, simultaneous shape-numeric inference raises complex issues in the design of the static analyzer itself. In this paper, we study the construction of such shape-numeric, static analyzers. We set up an abstract interpretation framework that allows us to reason about simultaneous shape-numeric properties by combining shape and numeric abstractions into a modular, expressive abstract domain. Such a modular structure is highly desirable to make its formalization and implementation easier to do and get correct. To achieve this, we choose a concrete semantics that can be abstracted step-by-step, while preserving a high level of expressiveness. The structure of abstract operations (i.e., transfer, join, and comparison) follows the structure of this semantics. The advantage of this construction is to divide the analyzer in modules and functors that implement abstractions of distinct features.