interval-abstract-interpreter

Answer

The implementation is a sound interval-based abstract interpreter for a C-like subset with integer variables, arrays, conditionals, and while loops. It is a single file (abstract_interpreter.py, ~1300 lines) with these key components:

Architecture

1. Interval Domain (class Interval) - Represented as [lo, hi] with ±∞ bounds and None as ⊥ (bottom/unreachable) - Lattice operations: join (⊔), meet (⊓), widen (∇), narrow (Δ) - Arithmetic: +, -, *, / propagate bounds using interval arithmetic - Comparison refinement: lt_meet, le_meet, gt_meet, ge_meet, eq_meet, ne_meet

2. Abstract State (class AbstractState) - Maps variable names → Interval - Tracks array declarations with valid index bounds - Provides join, widen, narrow operations over the entire state

3. Widening at Loop Heads (in exec_while) - At each loop head, the post-body state is widened toward the pre-loop state using state_old ∇ state_new - Continues until a fixed point is reached or a threshold (10 iterations) is hit - Standard widening: if the lower bound decreases, send it to −∞; if the upper bound increases, send it to +∞

4. Narrowing for Precision Recovery (after widening converges) - Up to 3 narrowing iterations refine the widened state using state_old Δ state_body_out - Standard narrowing: −∞ bounds are replaced by concrete values, +∞ bounds are tightened

5. Error Detection - Division by zero: check if divisor interval contains 0 (lo ≤ 0 ≤ hi) - Out-of-bounds array access: check if index interval falls outside [0, size-1] - Errors are deduplicated by (kind, location) so each source location produces at most one warning per error type

6. Condition Refinement (for precise branch analysis) - _apply_op_refine tightens variable intervals along true/false paths - E.g., x > 0 → true: x ∈ [1, +∞); false: x ∈ (−∞, 0]

Parser (subset grammar)

program     → decl_or_stmt*
decl_or_stmt → decl | stmt
decl        → 'int' IDENT ('[' NUMBER ']')* ';'    // array
            | 'int' IDENT ('=' expr)? ';'            // variable
stmt        → IDENT '=' expr ';'                     // assign
            | IDENT '[' expr ']' = expr ';'          // array assign
            | 'if' '(' expr ')' stmt ('else' stmt)?
            | 'while' '(' expr ')' stmt
            | '{' decl_or_stmt* '}'
            | 'skip' ';'
expr        → comparison (('<' | '>' etc.) comparison)?
            → expr ('+' | '-') term
            → term ('*' | '/') unary
            → ('-')? primary
primary     → NUMBER | IDENT | IDENT '[' expr ']' | '(' expr ')'

Key Code Snippets

Interval widening and narrowing:

def widen(self, other: 'Interval | None') -> 'Interval | None':
    if other is None: return self
    if self is None: return other
    lo = self.lo if self.lo <= other.lo else NEG_INF
    hi = self.hi if self.hi >= other.hi else INF
    return Interval(lo, hi)

def narrow(self, other: 'Interval | None') -> 'Interval | None':
    if other is None: return self
    if self is None: return other
    lo = other.lo if self.lo == NEG_INF else self.lo
    hi = other.hi if self.hi == INF else self.hi
    return Interval(lo, hi) if lo <= hi else None

While loop execution with widening/narrowing:

def exec_while(self, state, stmt):
    # Phase 1: Widening
    prev = state
    while True:
        body_in, _ = self.check_cond(prev, stmt.cond)
        body_out = self.exec_stmts(body_in, stmt.body)
        widened = prev.widen(body_out)
        if widened == prev: break
        prev = widened

    # Phase 2: Narrowing
    narrowed = prev
    for _ in range(self.narrow_iterations):
        body_in, _ = self.check_cond(narrowed, stmt.cond)
        body_out = self.exec_stmts(body_in, stmt.body)
        new = narrowed.narrow(body_out)
        if new == narrowed: break
        narrowed = new

    _, exit_state = self.check_cond(narrowed, stmt.cond)
    return exit_state