313
edits
Changes
→Fixed Point Solving
let ebb = the entry basic block
set ebb.inState = (user-defined initial state)
// Iterate until fixed point
do:
bb.outState = cur_state
until not changed
Exactly why this works depends on a bunch of math that we don't need to get into, but we can give some intuitions.
First off, when there are no loops, basically we're just doing straight abstract interpretation in arbitrary order. If we do a later block, then an earlier block, we just redo the later block and throw out the old results, but the end result is the same as if we went in the "perfect" order we'd do by hand.
Now consider a loop, like this (using our example lock()/unlock() analysis):
[[Image:treehydra-lock-cfg.png|right]]
[[Image:treehydra-lock-cfg-0.png|right]]
[[Image:treehydra-lock-cfg-1.png|right]]
