PAGAI: a path sensitive static analyzer

TL;DR

PAGAI is a static analyzer that combines abstract interpretation and SMT-solving to compute invariants in LLVM programs, focusing on path sensitivity and efficiency.

Contribution

It introduces a flexible, path-sensitive static analysis framework integrating multiple algorithms and domains, with extensive experimental evaluation.

Findings

PAGAI effectively balances precision and performance.

Different algorithm and domain combinations impact analysis results.

The tool performs well on real-world benchmarks.

Abstract

We describe the design and the implementation of PAGAI, a new static analyzer working over the LLVM compiler infrastructure, which computes inductive invariants on the numerical variables of the analyzed program. PAGAI implements various state-of-the-art algorithms combining abstract interpretation and decision procedures (SMT-solving), focusing on distinction of paths inside the control flow graph while avoiding systematic exponential enumerations. It is parametric in the abstract domain in use, the iteration algorithm, and the decision procedure. We compared the time and precision of various combinations of analysis algorithms and abstract domains, with extensive experiments both on personal benchmarks and widely available GNU programs.