Sea-DSA — Memory Graph AA

Overview

Sea-DSA is a context-sensitive, field-sensitive alias and memory analysis based on Data Structure Analysis (DSA). It builds heap graphs that summarize program memory and supports modular, interprocedural reasoning.

  • Location: lib/Alias/seadsa

  • Tools: sea-dsa-dg, seadsa-tool

  • Use Cases: Precise mod/ref information, call-graph construction, memory-shape reasoning

Memory Graphs

Sea-DSA represents memory as a graph where:

  • Nodes correspond to memory objects (heap, stack, globals).

  • Edges represent field and pointer relationships.

  • Attributes encode properties such as singleton-ness, heap/stack origin, and mutation/escape information.

Graphs can be built bottom-up, top-down, and globally, and then merged or refined through the analysis pipeline.

Usage

./build/bin/sea-dsa-dg --sea-dsa-dot example.bc
./build/bin/seadsa-tool --sea-dsa-dot --outdir results/ example.bc

sea-dsa-dg

A simple tool for generating memory graphs using Sea-DSA analysis.

./build/bin/sea-dsa-dg [options] <input LLVM bitcode file>

Key options:

  • --sea-dsa-dot – Generate DOT files visualizing the memory graphs

This tool provides a straightforward interface to the Sea-DSA analysis for generating memory graphs that can be visualized using Graphviz.

seadsa-tool

Advanced Sea-DSA analysis tool with comprehensive memory graph analysis capabilities.

./build/bin/seadsa-tool [options] <input LLVM bitcode file>

Key options:

  • --sea-dsa-dot – Generate DOT files visualizing memory graphs

  • --sea-dsa-callgraph-dot – Generate DOT files of the complete call graph

  • --outdir <DIR> – Specify an output directory for generated files

This tool provides advanced analysis capabilities for understanding memory usage patterns, pointer relationships, and potential memory-related issues in programs.

Sea-DSA results are consumed by other analyses (e.g., mod/ref, verification tools) to obtain a precise view of heap structure and aliasing.