A Partial-Order Approach to Array Content Analysis

TL;DR

This paper introduces a parametric abstract domain for array content analysis that uses an array content graph to efficiently analyze array regions without initial partitioning, compatible with various numeric domains.

Contribution

It proposes a novel array content graph approach that simplifies array analysis and integrates with different numeric relational abstract domains.

Findings

Effective analysis of array regions in program fragments

Compatible with multiple numeric relational domains

Avoids upfront factorial partitioning step

Abstract

We present a parametric abstract domain for array content analysis. The method maintains invariants for contiguous regions of the array, similar to the methods of Gopan, Reps and Sagiv, and of Halbwachs and Peron. However, it introduces a novel concept of an array content graph, avoiding the need for an up-front factorial partitioning step. The resulting analysis can be used with arbitrary numeric relational abstract domains; we evaluate the domain on a range of array manipulating program fragments.