execution-based algorithm for computing maximum fixed-point solution to a DFP

Input: data-flow problem (DFP) (P, L, exec⟦code⟧(state), a₀)
       where P = I[0]..I[n], L = 〈A,⊓,⊔〉

       this is (program, lattice, language, initial_state)
       where a lattice is a value domain with meet and join operators

Output: s[0]..s[n] ∈ A
        where each s[i] gives the abstract value of each variable as
        preconditions for step #i

s[0] := a₀
for i := 1 to n do s[i] := ⊤
W := {0,...,n}
while W ≠ ∅ do
  choose pc ∈ W
  repeat
    W := W - pc
    new := exec⟦I[pc]⟧(s[pc])
    if I[pc] == (goto l) then pc´ := l
    else
      pc´ := pc+1
      if I[pc] == (if ψ goto l) and new ⊲ s[l] then
         W := W + l
 	 s[l] := update(s[l], new)
      end
    end
    if new ⊲ s[pc´] then
       s[pc´] := update(s[pc´], new)
       pc := pc´
    else
       pc := n+1
    end
  until pc == n+1
end

final type assignment for variable v is fold(⊔, ⊥, { s[i,v] | i=0..n })

in the original algorithm:

define  new⊲s = (new ⊓ s == new) ∧ (new ≠ s)
define  update(s, new) = new

possible alternate for type inference:

define  new⊲s = (new ≠ s)
define  update(s, new) = s ⊓ new

define  new⊲s = !(new <: s)
define  update(s, new) = s ⊔ new

or  update(s, new) = {U=(s[U] ⊓ new[U]), L=(s[L] ⊓ new[L]) ⊓ s[U]}

define exec⟦z := f(x,y)⟧(s[v,UL]) =
  s' = s
  s'[z,U] = tf⟦f⟧(s[x,U], s[y,U]) ⊓ s[z,U]
  s'[z,L] = tf⟦f⟧(s[x,L], s[y,L]) ⊓ s[z,U]
  return s'
end

where tf⟦f⟧ is the t-function for f


from NTI algorithm:

s[U] = (join all predecessor upper bounds) ⊓ s[U]
s[L] = (join all predecessor lower bounds) ⊓ s[U]

F = diagonal matrix of functions, Fii = exec⟦I[i]⟧, off-diag Fij = ⊥
C = square matrix, Cij = (I[j] is a successor to I[i])
S = vector of states, S[i] = {type assignments for all variables}
B = like F but using backward t-functions

find the limit of (F*C)^n * S

complete algorithm:

U := ⊤;
repeat {
  oldU := U;
  L := ⊥; repeat {oldL := L; L := (F*C*L) meet U} until L=oldL;
  U := L;
  L := ⊥; repeat {oldL := L; L := (C^t*B*L) meet U} until L=oldL;
  U := L; } until U=oldU;

-------------------------------------------------------------------------------

jeff's version: the above MFP algorithm combined with K-U for dynamic
type inference

Input: same as above
Output: s[0]..s[n], where each s[i] is a State record
        {pred::Set, before::List[Bounds], after::List[Bounds]}
        where Bounds is a record {upper::Type, lower::Type}

s[0] := {pred=∅, before=after={{upper=a₀.upper, lower=a₀.lower} ∀ vars}}
for i := 1 to n do s[i] := {pred=∅, before=after={{upper=⊤, lower=⊥} ∀ vars}}
W := {0,...,n}
while W ≠ ∅ do
  choose pc ∈ W
  repeat
    W := W - pc
    new := s[pc].after := exec⟦I[pc]⟧(s[pc].before)
    if I[pc] == (goto l) then
      pc´ := l
    else
      pc´ := pc+1
      if I[pc] == (if ψ goto l) then
         s[l].pred ∪= {pc}
         if new ⊲ s[l].before then
            W := W ∪ {l}
 	    update(s, l)
         end
      end
    end
    s[pc´].pred ∪= {pc}
    if new ⊲ s[pc´].before then
       update(s, pc´)
       pc := pc´
    else
       pc := n+1
    end
  until pc == n+1
end

NOTE: ψ must not affect type assignments, so it must be a variable

define ⊲(new::List[Bounds], s::List[Bounds])

define update(s::List[State], p::Int)
  s0 = s[p]
  U = ⊥
  L = ⊥
  for i in s0.pred
    U = U ⊔ s[i].after.upper
    L = L ⊔ s[i].after.lower
  end
  s0.before.upper = U ⊓ s0.before.upper
  s0.before.lower = L ⊓ s0.before.upper
end

-------------------------------------------------------------------------------

adding function types to the mix.
example of infererence on a call to map():

assuming:
 cons(x,y) = Cons(x,y)
 map(f, l::Nil) = l
 map(f, l::Cons) = cons(f(head(l)), map(f, tail(l)))

map(x->2x, list(...))

 map(A-->B, Cons{C})

 cons(f(C), map(A-->B, List{C}))
   => A==C

 map(A-->B, List{C})
   ==> Union(Rec{map(A-->B,Cons{C})}, Nil)

 cons(f(C), Union(Rec{map(A-->B,Cons{C})}, Nil))
                                            
 cons(B, Union(Rec, Nil))
                                            
 Cons( ((B,Union(Rec,Nil)) ∩ (T,List{T}))... )  
   => T==B
   ==> Cons{B}

 cons(B, Union(Cons{B}, Nil))

 Cons(B, Union(Cons{B}, Nil))
   ==> Cons{B}

 ==> Cons{B}

map collects all types that might be passed as A and unions them as if
A were a single location.
so ideally inference on the map() call returns Cons{B} and also
somehow tells us that A is C.