Path Program

Path programs are control-flow abstractions induced by concrete execution paths, aligned with the PLDI 2007 Path Invariants approach. Each path program captures the sequence of program locations and control-flow transitions visited along a single concrete path.

Location: lib/Verification/PathProgram/

Headers: include/Verification/PathProgram/

Overview

A path program represents a set of concrete traces that follow the same sequence of control-flow decisions. The representation models:

  • Locations — the program locations (basic blocks) visited by the path.

  • Transitions — the exact control-flow edges taken between locations.

The infrastructure builds path programs from LLVM IR by:

  1. Extracting a concrete trace through a function (sequence of basic blocks).

  2. Constructing the corresponding PathProgram object with the trace’s control-flow skeleton.

  3. Optionally compressing the representation using CompressedCfg.

Components

  • PathProgram — Core data structure: ordered list of trace transitions and the induced control-flow graph.

  • PathProgramBuilder — Constructs PathProgram instances from LLVM functions and trace information.

  • PathProgramView — Provides a read-only view over a path program for downstream analyses.

  • CompressedCfg — Compressed representation of the path program’s CFG for efficient storage and traversal.

This subsystem is used by verification analyses that need path-specific reasoning, such as invariant inference and path-sensitive property checking.

See Also