CSE271: Principles of Programming Languages

Null-Pointer Analysis

Jooyong Yi (UNIST)

Question

p = alloc();
q = &p;
n = null;
*q = n; // safe?
*p = n; // safe?

p = alloc();

• Can p be null?

p = alloc();

• Can p be null?

  • No.

• A(p = alloc()) = update(σ, {p ≠ null})

  • σ: the program state when p = alloc() is executed

p = alloc();

• Can p be null?

  • No.

• A(p = alloc()) = update(σ, {p ≠ null})

  • ρ(p) = 𝑙, σ(𝑙) ≠ null

p = alloc();

• Can p be null?

  • No.

• A(p = alloc()) = update(σ, {p ≠ null})

  • ρ(p) = 𝑙, σ(𝑙) ≠ null

• A(p = alloc()) = update(σ, {p ↦ NotNull})

p = alloc(); // 𝑙₁ ∈ pts(p) 

• Can p be null?

  • No.

• A(p = alloc()) = update(σ, {p ≠ null})

  • ρ(p) = 𝑙, σ(𝑙) ≠ null

• A(p = alloc()) = update(σ, {p ↦ NotNull, 𝑙₁ ↦ ?})

p = alloc(); // 𝑙₁ ∈ pts(p) 

• Can p be null?

  • No.

• A(p = alloc()) = update(σ, {p ≠ null})

  • ρ(p) = 𝑙, σ(𝑙) ≠ null

• A(p = alloc()) = update(σ, {p ↦ NotNull, 𝑙₁ ↦ Nullable})

             σ₀ = ∅
p = alloc();  
             σ₁ = update(∅, {p ↦ NotNull, 𝑙₁ ↦ Nullable})
                = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;
n = null;
*q = n; // safe?
*p = n; // safe?

• A(q = &p) = ?

• A(q = &p) = update(σ, {q ↦ NotNull})

              σ₀ = ∅
p = alloc();  
              σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;
              σ₂ = update({p ↦ NotNull, 𝑙₁ ↦ Nullable}, {q ↦ NotNull}) 
                 = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
n = null;
*q = n; // safe?
*p = n; // safe?

• A(n = null) = ?

• A(n = null) = update(σ, {n ↦ Nullable})

              σ₀ = ∅
p = alloc();  
              σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;
              σ₂ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
n = null;
              σ₃ = update({p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}, {n ↦ Nullable}) 
                 = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
*q = n; // safe?
*p = n; // safe?

• A(*q = n) = ?

• Suppose pts(q) = {𝑙}
• A(*q = n) = ?

• Suppose pts(q) = {𝑙}
• A(*q = n) = update(σ, {𝑙 ↦ σ(n)})

• Suppose pts(q) = {𝑙₁, 𝑙₂}
• A(*q = n) = update(σ, {𝑙₁ ↦ ?, 𝑙₂ ↦ ?})

• Suppose pts(q) = {𝑙₁, 𝑙₂}
• Suppose σ(𝑙₁) = Nullable, σ(𝑙₂) = NotNull, σ(n) = NotNull
• A(*q = n) = update(σ, {𝑙₁ ↦ ?, 𝑙₂ ↦ ?})

• Suppose pts(q) = {𝑙₁, 𝑙₂}
• Suppose σ(𝑙₁) = Nullable, σ(𝑙₂) = NotNull, σ(n) = NotNull
• A(*q = n) = update(σ, {𝑙₁ ↦ Nullable, 𝑙₂ ↦ NotNull})

• Suppose pts(q) = {𝑙₁, 𝑙₂}
• Suppose σ(𝑙₁) = Nullable, σ(𝑙₂) = NotNull, σ(n) = NotNull
• A(*q = n) = update(σ, {𝑙₁ ↦ σ(𝑙₁) ⊔ σ(n), 𝑙₂ ↦ σ(𝑙₂) ⊔ σ(n)})

    Nullable
       |
    NotNull

• A(*q = n) = update(σ, {𝑙 ↦ σ(𝑙) ⊔ σ(n)})

              σ₀ = ∅
p = alloc();  
              σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;
              σ₂ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
n = null;
              σ₃ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
*q = n;       σ₄ = update({p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}, {p ↦ NotNull ⊔ Nullable})
                 = {p ↦ Nullable, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
*p = n; 

• Andersen’s points-to analysis results
  • pts(p) = {𝑙₁}
  • pts(q) = {p}
  • pts(n) = ∅

              σ₀ = ∅
p = alloc();  
              σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;
              σ₂ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
n = null;
              σ₃ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
*q = n;       σ₄ = {p ↦ Nullable, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
*p = n;       σ₅ = update({p ↦ Nullable, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}, {𝑙₁ ↦ Nullable ⊔ Nullable})
                 = {p ↦ Nullable, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable, 𝑙₁ ↦ Nullable}

• Andersen’s points-to analysis results
  • pts(p) = {𝑙₁}
  • pts(q) = {p}
  • pts(n) = ∅

• A(p = alloc()) = update(σ, {p ↦ NotNull})
• A(q = &p) = update(σ, {q ↦ NotNull})
• A(n = null) = update(σ, {n ↦ Nullable})
• A(*q = n) = update(σ, {𝑙 ↦ σ(𝑙) ⊔ σ(n)})
• A(p = *q) = update(σ, {p ↦ σ(𝑙)})

Question #2

p = alloc();    // σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;         // σ₂ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
if (x > y) 
  n = null;     // σ₃ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
else
  n = alloc();  // σ₄ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ NotNull, 𝑙₂ ↦ Nullable}
*q = n;         // σ₅(n) = ?  
*p = n; 

• Andersen’s points-to analysis results
  • pts(p) = {𝑙₁}
  • pts(q) = {p}
  • pts(n) = {𝑙₂}

Question #2

p = alloc();    // σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;         // σ₂ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
if (x > y) 
  n = null;     // σ₃ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
else
  n = alloc();  // σ₄ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ NotNull, 𝑙₂ ↦ Nullable}
*q = n;         // σ₅(n) = σ₃(n) ⊔ σ₄(n) = Nullable ⊔ NotNull = Nullable   
*p = n; 

Question #2

p = alloc();    // σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;         // σ₂ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
if (x > y) 
  n = null;     // σ₃ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
else
  n = alloc();  // σ₄ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ NotNull, 𝑙₂ ↦ Nullable}
*q = n;         // σ₅ = σ₃ ⊔ σ₄
*p = n; 

Question #2

p = alloc();    // σ₁ = {p ↦ NotNull, 𝑙₁ ↦ Nullable}
q = &p;         // σ₂ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull}
if (x > y) 
  n = null;     // σ₃ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ Nullable}
else
  n = alloc();  // σ₄ = {p ↦ NotNull, 𝑙₁ ↦ Nullable, q ↦ NotNull, n ↦ NotNull, 𝑙₂ ↦ Nullable}
*q = n;         // σ₅ = σ₃ ⊔ σ₄
*p = n; 

• A(*q = n) = update(σ, {𝑙 ↦ σ(𝑙) ⊔ σ(n)})
  • σ = σ

• A(p = alloc()) = update(σ, {p ↦ NotNull})
• A(q = &p) = update(σ, {q ↦ NotNull})
• A(n = null) = update(σ, {n ↦ Nullable})
• A(*q = n) = update(σ, {𝑙 ↦ σ(𝑙) ⊔ σ(n)})
• A(p = *q) = update(σ, {p ↦ σ(𝑙)})