Abstract Domain Explorer

Abstract Domain Explorer

Overview

This skill applies abstract interpretation to statically analyze programs using various abstract domains. It infers invariants, value ranges, and relationships between variables without executing the code. Different domains offer different trade-offs between precision and efficiency.

Analysis Workflow

Follow these steps to analyze programs with abstract domains:

1. Select Appropriate Domain(s)

Choose based on analysis goals:

Interval Domain:

• Use for: Range analysis, bounds checking, array indexing
• Precision: Low to medium
• Cost: Very efficient
• Example: Determine if x ∈ [0, 100]

Sign Domain:

• Use for: Sign analysis, division by zero detection
• Precision: Low
• Cost: Very efficient
• Example: Determine if x is positive, negative, or zero

Congruence Domain:

• Use for: Modular arithmetic, alignment analysis
• Precision: Medium (for specific patterns)
• Cost: Efficient
• Example: Determine if x ≡ 0 (mod 4)

Octagon Domain:

• Use for: Relational analysis, loop invariants with simple relationships
• Precision: Medium to high
• Cost: Moderate (O(n³) operations)
• Example: Infer x ≤ y + 5, x + y ≤ 10

Polyhedra Domain:

• Use for: Complex linear relationships, precise invariants
• Precision: High
• Cost: Expensive (exponential worst-case)
• Example: Infer 2x + 3y ≤ z + 10

Reduced Product:

• Use for: Combining strengths of multiple domains
• Precision: Higher than individual domains
• Cost: Sum of component costs
• Example: Intervals × Congruence for precise range with modular constraints

2. Initialize Abstract State

Set initial values for program entry:

• Constants: Exact values (e.g., x = 5 → x ∈ [5, 5])
• Inputs: Top element (e.g., user input → x ∈ [-∞, +∞])
• Uninitialized: Bottom element (unreachable)

Example:

int x = 0;        // x ∈ [0, 0]
int y = input();  // y ∈ [-∞, +∞]

3. Apply Transfer Functions

For each statement, compute abstract semantics:

Assignment (x = e):

• Evaluate expression e in abstract domain
• Update abstract state for x

Condition (assume c):

• Refine abstract state based on condition
• Intersect with constraint

Join (control flow merge):

• Compute least upper bound of incoming states
• Used after if-else, at loop headers

Example (Intervals):

x = y + 5;        // If y ∈ [a, b], then x ∈ [a+5, b+5]
assume(x > 10);   // If x ∈ [a, b], then x ∈ [max(a, 11), b]

4. Handle Loops with Widening

For loops, apply widening to ensure termination:

1. Compute first iteration
2. Compute second iteration
3. Apply widening operator (∇)
4. Check for convergence
5. Continue until fixpoint reached

Example:

int x = 0;
while (x < 100) {
    x = x + 1;
}

• Iteration 0: x ∈ [0, 0]
• Iteration 1: x ∈ [0, 1]
• Widening: x ∈ [0, +∞]
• Refine with condition: x ∈ [0, 99] in loop
• Exit: x ∈ [100, 100]

5. Refine with Narrowing (Optional)

Apply narrowing to improve precision:

• Iterate a few more times (typically 1-3)
• Use narrowing operator (△)
• Refine over-approximations from widening

6. Extract Invariants

Identify inferred properties:

• Value ranges for each variable
• Relationships between variables
• Loop invariants
• Preconditions for safe operations

Report format:

• Variable: abstract value
• Invariants: logical formulas
• Safety properties: bounds checks, division by zero, etc.

Analysis Examples

Example 1: Range Analysis with Intervals

Code:

int x = 0;
int y = 100;
while (x < 10) {
    x = x + 1;
    y = y - 1;
}
// What are the values of x and y here?

Analysis (Interval Domain):

• Entry: x ∈ [0, 0], y ∈ [100, 100]
• Loop iterations with widening:
  • Iter 0: x ∈ [0, 0], y ∈ [100, 100]
  • Iter 1: x ∈ [0, 1], y ∈ [99, 100]
  • Widening: x ∈ [0, +∞], y ∈ [-∞, 100]
  • Refine with x < 10: x ∈ [0, 9], y ∈ [-∞, 100]
• Narrowing: y ∈ [91, 100]
• Exit: x ∈ [10, 10], y ∈ [90, 90]

Inferred Invariants:

• Loop: x ∈ [0, 9], y ∈ [91, 100]
• Exit: x = 10, y = 90
• Implicit: x + y = 100 (not captured by intervals alone)

Example 2: Relational Analysis with Octagons

Code:

int x = 0;
int y = 0;
while (x < 10) {
    x = x + 1;
    y = y + 1;
}

Analysis (Octagon Domain):

• Entry: x = 0, y = 0, x - y = 0
• Loop iterations:
  • Maintains x - y = 0 throughout
  • x ∈ [0, 10], y ∈ [0, 10]
• Exit: x = 10, y = 10, x = y

Inferred Invariants:

• x = y (captured by octagon)
• x ∈ [0, 10], y ∈ [0, 10]

Advantage over Intervals: Intervals would only infer x ∈ [0, 10], y ∈ [0, 10] but miss the relationship x = y.

Example 3: Linear Relationships with Polyhedra

Code:

int x = 0, y = 0, z = 0;
while (x < 10) {
    x = x + 1;
    y = y + 2;
    z = x + y;
}

Analysis (Polyhedra Domain):

• Entry: x = 0, y = 0, z = 0
• Loop iterations:
  • Infers: y = 2x, z = x + y, z = 3x
  • x ∈ [0, 10]
• Exit: x = 10, y = 20, z = 30

Inferred Invariants:

• y = 2x
• z = x + y
• z = 3x
• x ∈ [0, 10]

Advantage over Octagons: Polyhedra can express y = 2x, which octagons cannot.