Unbounded Static Analysis

Christian Gram Kalhauge

Table of Contents

  1. Dependent Values
  2. Implementing an Abstract Interpreter
  3. 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 0n={+,−,0}⊢⟨{0↦n},ϵ,0⟩→{1}
001ifz eq 6n={+,−,0}⊢⟨{0↦n},n,1⟩→{2,6}
002push:I 1n={+,−}⊢⟨{0↦n},ϵ,2⟩→{3}
003load:I 0n={+,−}⊢⟨{0↦n},{+},3⟩→{4}
004binary:I divn={+,−}⊢⟨{0↦n},{+}n,4⟩→{5}
005return:In={+,−}⊢⟨{0↦n},{+,−},5⟩→{ok}
006push:I 0n={0}⊢⟨{0↦n},ϵ,6⟩→{7}
007return:In={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;
}

Implementing an Abstract Interpreter (§2)

def manystep(sts : StateSet[A]) -> Iteratable[A | str]:
  ...
final = {}
sts = A.initialstate_from_method(methodid)
for i in range(MAX_STEPS):
  for s in manystep(sts):
    if isinstance(s, str):
      final.add(s)
    else:
      sts |= s
log.info(f"The following final states {final} is possible in {MAX_STEPS}")

Grouping Per Instruction (§2.1)

for pc, state in sts.per_instruction():
  match bc[pc]:
    case jvm.Binary(type=jvm.Int(), operant=opr):
      ...

Grouping Per Variable (§2.2)

for ([va1, va2], after) for state.group(pop=[jvm.Int(), jvm.Int()]):
  ...

Doing the Operation (§2.3)

for res in after.binary(opr, va1, va2):
  match res with 
    case (va3, after):
        yield after.frame.update(push=[va3], pc=pc+1)
    case err:
        yield err

Constraining the Space (§2.4)

case jvm.Ifz(condition=con, target=target):
  for ([va1], after) for state.group(pop=[jvm.Int()]):
    for res in after.binary(con, va1, 0):
      match res:
        case (True, after):
          yield after.frame.update(pc=target)
        case (False, after):
          yield after.frame.update(pc=pc+1)
        case err:
          yield err

Unbounded Static Analysis (§3)

Fixed Points (§3.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(⊥)…)), were 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 (§3.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;
  }
}
1{i↦[0,0]}2{i↦[0,0]}𝚜𝚎𝚎 𝚝𝚑𝚊𝚝 𝚒 >= 𝟶3{i↦[0,0]+[1,1]}𝚒 = 𝚒 + 𝟷4{i↦[0,0]⊔[1,1]}𝚕𝚘𝚘𝚙 𝚋𝚊𝚌𝚔5{i↦[0,1]}𝚜𝚎𝚎 𝚝𝚑𝚊𝚝 𝚒 >= 𝟶6{i↦[0,1]+[1,1]}𝚒 = 𝚒 + 𝟷7{i↦[0,1]⊔[1,2]}𝚕𝚘𝚘𝚙 𝚋𝚊𝚌𝚔8...𝚊𝚗𝚍 𝚜𝚘 𝚘𝚗

The Widening Operator (§3.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 (§3.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 (§3.4)

class StateSet[A]:
  per_inst : dict[PC, A]
  needswork : set[PC]

  def per_instruction(self):
    for pc in self.needswork: 
      yield (pc, self.per_inst[pc])

  # sts |= astate
  def __ior__(self, astate):
    old = self.per_inst[astate] 
    self.per_inst[astate.pc] |= astate
    if old != self.per_inst[astate.pc]:
      needswork.add(astate.pc)
  
  ...

The Reverse Post-Order (§3.4.1)

void fn() { 
  int i = 0;
  while (i < 100) { 
    i += 1;
  }
  // Many operations on i.
}

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?