313
edits
Abstract Interpretation: Difference between revisions
Jump to navigation
Jump to search
→Solving
No edit summary |
|||
| Line 241: | Line 241: | ||
==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 | |||