313
edits
Changes
→Solving
==Solving==
In our examples above, to run the abstract interpretations, we just sort of went down paths by hand. That's not much of an algorithm: it doesn't explain what order to go in or how to sync up at join points. (And in fact, it's not necessary to explicitly sync up at join points at all.) Also, we didn't do loops.
Fortunately, the Treehydra library code implements all of this 'solving' process: all you have to do is specify the lattice, a .flowState() function, and an initialState() function. But it might be helpful to understand what the solver does.
===Fixed Point Solving===
The basic solving algorithm works on basic blocks. In each step, we get the entry ("in") state of a basic block from its predecessors, then abstractly interpret the basic block, and finally set the new exit ("out") state for that block. If the out state changed from the last time we interpreted that block, then we need to make sure the successor blocks run again (because their in state depends on the current block's out state). In this way, we keep running blocks until no state changes from last time. The resulting state (at every program point) is called a '''fixed point''', because further abstract interpretation doesn't change it.
Here is the basic algorithm as pseudocode:
// Set initial states
for each basic block bb:
set bb.inState = top for every variable
set bb.outState = top for every variable
let ebb = the entry basic block
set ebb.inState = (user-defined initial state)
// Iterate until fixed point
do:
let changed = false
// Process all basic blocks, looking for changes
for each basic block bb:
// Set up in state
if (bb != ebb)
set bb.inState = merge out states of predecessors
let cur_state = bb.inState
// Interpret block
for each instruction of bb, isn:
cur_state = (user-defined flow function)(isn, cur_state)
// Set out state and check for changes
if (cur_state != bb.outState) changed = true
bb.outState = cur_state
until not changed
