Modular Abstract Interpretation for Stack-Heap Analysis of C/C++ via LLVM IR

Abstract

Detecting memory errors in C/C++ by static analysis means reasoning about program values and memory structure together, but value- and memory-oriented analyses are usually combined in fixed, domain-specific ways. This work proposes a modular, parametric framework, based on abstract interpretation theory, with a split-state abstraction that separates values from memory structure into two independent, interchangeable domains. Any pair satisfying a minimal interface yields a sound combined analysis by construction. Precision can thus be adapted without redesigning the analysis, for instance by trading a coarser memory domain for a richer value one.