The simplest BT lattice has just two elements:
bt ::=dynamic is top, static is bottom (
Say we are analyzing
(prim r + a b)
In abstract interpretation, the value assigned to
r is the
abstraction of the
+ primop (denoted ) applied to the
b in the analysis environment.
In my BTA the abstraction of all the generic primops is the same: if
any argument is not
S then the result is
D. Call this function
. Thus if any argument is unknown at compile time, then the
prim must be delayed until runtime.