313
edits
Changes
→Solving
[[Image:treehydra-loop.png]]
==Remarks==
The solver interprets the basic blocks in arbitrary order, and more than once. So if you watch the solver (using its tracing mode), you won't see code paths being executed or collected. This is a necessary consequence of avoiding path explosion.
The states in the solver can be "wrong" on the intermediate steps, before the solver is finished. This means you shouldn't try to check properties or use the results inside the flow function, while the solver is running. Instead, you should check after the solver is all done.
The Treehydra solver tries to process basic blocks in a good order to reduce the number of times they have to be processed to get the solution. Basically, when there are no loops it goes in topological order (much like 'make'). When there are loops it uses something like topological order (reverse postorder).
Some abstract interpretations can go into infinite loops. (Note that the examples we gave always terminate.) Usually, this can only happen if there is a bug in the flow function or if the lattice has a path with infinitely many steps from bottom to top (e.g., the lattice of all integer ranges). The analysis can also run a really long time if the lattice just has a long path from bottom to top. Diagnosing and repairing termination issues is an advanced topic I'm not prepared to go into here, but feel free to ask for help with specific issues.
Note that sometimes solving just takes a long time: functions can have 1000 or more basic blocks, and analyzing such a function in detail in JS take take up to a minute or so.
