Unbounded Static Analysis

Christian Gram Kalhauge

Table of Contents

  1. Dependent Values
  2. Unbounded Static Analysis

Questions

  1. What does it mean for two variables to be dependent?

  2. What is the primary problem when doing unbounded static analysis?

  3. Why do we need a widening operator?

Dependent Values (§1)

@Case("(0) -> ok")
@Case("(1) -> ok")
public static int safeDivByN(int n) { 
  if (n != 0) {
    return 1 / n;
  }
  return 0;
}
OffsetInstructionAbstract State
000load:I 0⟨{0↦{+,−,0}},ϵ,0⟩→{1}
001ifz eq 6⟨{0↦{+,−,0}},{+,−,0},1⟩→{2,6}
002push:I 1⟨{0↦{+,−,0}},ϵ,2⟩→{3}
003load:I 0⟨{0↦{+,−,0}},{+},3⟩→{4}
004binary:I div⟨{0↦{+,−,0}},{+}{+,−,0},4⟩→{5,err(‘𝚍𝚒𝚟 𝚋𝚢 𝚣𝚎𝚛𝚘’)}
005return:I⟨{0↦{+,−,0}},{+,−},5⟩→{ok}
006push:I 0⟨{0↦{+,−,0}},ϵ,6⟩→{7}
007return:I⟨{0↦{+,−,0}},{0},7⟩→{ok}
OffsetInstructionAbstract State
000load:I 0{n↦{+,−,0}}/⟨{0↦n},ϵ,0⟩→{1}
001ifz eq 6{n↦{+,−,0}}/⟨{0↦n},n,1⟩→{2,6}
002push:I 1{n↦{+,−}}/⟨{0↦n},ϵ,2⟩→{3}
003load:I 0{n↦{+,−}}/⟨{0↦n},{+},3⟩→{4}
004binary:I div{n↦{+,−}}/⟨{0↦n},{+}n,4⟩→{5}
005return:I{n↦{+,−}}/⟨{0↦n},{+,−},5⟩→{ok}
006push:I 0{n↦{0}}/⟨{0↦n},ϵ,6⟩→{7}
007return:I{n↦{0}}/⟨{0↦n},{0},7⟩→{ok}

Dependencies between different values. (§1.1)

@Case("(0, 0) -> ok")
@Case("(1, 1) -> ok")
public static int safeDivAByB(int a, int b) { 
  if (a >= 0) {
    if (b > a) {
      return a / b
    }
  }
  return 0;
}

Unbounded Static Analysis (§2)

Fixed Points (§2.1)

Minimal Fixed Point

Given a function f:A→A, that is monotone over (A,⊑A) (∀a∈A.a⊑Af(a)) then the minimal fixed point is the least n st. fn(⊥)=fn+1(⊥).

fn(⊥) means f(f(…f(⊥)…)), where f is applied n times.

a(x)=x+𝐒𝐢𝐠𝐧α({1})
f(x)=x⊔a(x)
f0({0})={0}f1({0})=f({0})={0}⊔{+}={0,+}f2({0})=f(f1({0}))={0,+}⊔{+}={0,+}

The Interval Abstraction (§2.2)

α(S)=[minS,maxS]γ([i,j])={n∈ℤ|j≥n≤i}[i,j]⊑𝐈𝐭𝐯𝐚𝐥[k,h]≡k≤i∧j≤h[i,j]⊔𝐈𝐭𝐯𝐚𝐥[k,h]≡[min{i,k},max{j,h}][i,j]⊓𝐈𝐭𝐯𝐚𝐥[k,h]≡[max{i,k},min{j,h}]⊤𝐈𝐭𝐯𝐚𝐥=[−∞,∞]⊥𝐈𝐭𝐯𝐚𝐥=[∞,−∞]
void example() {
  int i = 0;
  while (i >= 0) {
    i = i + 1;
  }
}
StateComment
{}int i = 0
{i↦[0,0]}see that i >= 0
{i↦[0,0]}i = i + 1
{i↦[0,0]⊔[1,1]}loop back
{i↦[0,1]}see that i >= 0
{i↦[0,1]+[1,1]}i = i + 1
{i↦[0,1]⊔[1,2]}loop back
......

The Widening Operator (§2.3)

  • An operator ∇

K Interval

[i,j]∇[k,h]=[minK{i,k},maxK{j,h}]
α(S)=[minS,maxS]γ([i,j])={n∈ℤ|j≥n≤i}[i,j]⊑𝐈𝐭𝐯𝐚𝐥K[k,h]≡k≤i∧j≤h[i,j]⊔𝐈𝐭𝐯𝐚𝐥K[k,h]≡[min{i,k},max{j,h}][i,j]⊓𝐈𝐭𝐯𝐚𝐥K[k,h]≡[max{i,k},min{j,h}]⊤𝐈𝐭𝐯𝐚𝐥K=[−∞,∞]⊥𝐈𝐭𝐯𝐚𝐥K=[∞,−∞][i,j]∇𝐈𝐭𝐯𝐚𝐥K[k,h]=[minK{i,k},maxK{j,h}]

Proving Widening (§2.3.1)

∀a,b∈A.a⊑(a∇b)∧b⊑(a∇b)
∃n∈ℕ.∀x∈An+1,a∈A.(a0∇a1)∇a2)⋯∇an=((a0∇a1)∇a2)⋯∇an+1

The Worklist Algorithm (§2.4)

def step(self) -> tuple[PC, set[str]]:
    # Pop from worklist
    pc = self.worklist.pop()
    for res in manystep(self.bc, pc, self.states[pc]):
        pc_, st = res
        before = self.states.get(pc_, st)
        after = before | st
        if pc_ not in self.states or after != before:
            self.states[pc_] = after
            # Update worklist
            self.worklist.append(pc_)
    # ...

Control-Flow Analysis and Optimal Order (§2.4.1)

void fn(int x) { 
  int i = 0;
  if (x == 0) { 
    i += 1;
  } else { 
    i -= 1:
  }
  // Many operations on i.
}
void fn() { 
  int i = 0;
  while (i < 100) { 
    i += 1;
  }
  // Many operations on i.
}
i = 0 i < 100? i += 1 Many operations depedents on i true false

The control flow graph of the example code.

Questions

  1. What does it mean for two variables to be dependent?

  2. What is the primary problem when doing unbounded static analysis?

  3. Why do we need a widening operator?