==================================
UnderApproxAA — Must-Alias Analysis
==================================

Overview
========

UnderApproxAA is a **sound but incomplete** alias analysis that computes
**must-alias** information: if two pointers are reported as aliasing, they
are **guaranteed** to point to the same memory; otherwise the result is
unknown.

* **Location**: ``include/Alias/UnderApproxAA/``
* **Style**: Intra-procedural, under-approximate
* **Goal**: Cheap, reliable must-alias facts for safety-critical reasoning

Components
==========

* **Canonical** – Canonical form representations
* **EquivDB** – Equivalence class database
* **UnderApproxAA** – Core under-approximation algorithm

**Features**: Conservative alias analysis for safety-critical applications.

Algorithm
=========

UnderApproxAA maintains an **equivalence relation** over pointer-producing
values using a union-find data structure:

1. **Seeding (Atomic Rules)**  
   Scan instructions and apply local, syntactic rules (identity,
   bitcast/addrspace casts, zero-offset GEPs, trivial PHIs/selects, etc.)
   to add must-alias pairs to a worklist.

2. **Propagation (Semantic Rules)**  
   Process the worklist and unify equivalence classes. When classes merge,
   re-check watched PHI and select instructions. If all operands belong to
   the same class, new must-alias facts are inferred.

The resulting equivalence classes encode must-alias sets. Queries are
essentially ``O(α(N))`` union-find lookups.

Characteristics
===============

**Strengths**

* No false positives: any reported alias is guaranteed.
* Very fast construction and query time.
* Simple data structures and clear semantics.

**Limitations**

* Intra-procedural only (no cross-function reasoning).
* Focused on stack/global allocations; heap modeling is limited.
* May miss many true aliases (by design, under-approximate).

Usage
=====

UnderApproxAA is exposed via the AA wrapper and can be enabled where
**must-alias** information is preferable to may-alias over-approximation.
It is especially useful as a building block in verification and
sanity-checking passes.