313
edits
Abstract Interpretation: Difference between revisions
Jump to navigation
Jump to search
→Interpreting Branch Conditions
No edit summary |
|||
| Line 300: | Line 300: | ||
== Interpreting Branch Conditions == | == Interpreting Branch Conditions == | ||
Way back in our original example, you may have noticed a fact that our abstract interpretation failed to discover: than m is constant with value zero at the end of the function. The reason we don't discover this is that on the "a == 0" branch of the conditional, we do "m := a", and our state has "a = ?", so we set "m = ?". But if we're on the "a == 0" branch, then a has to be zero, right? | |||
Of course. But basic abstract interpretation doesn't try to interpret branch conditions. One reason is that the branch has no side effects, so interpreting it abstractly doesn't assign anything. | |||
But we certainly can try to discover and apply information from conditionals, and the Treehydra libraries include this feature. It's a little harder than a flow function, because in this case we're not executing an instruction and | |||
approximating, but rather reasoning backward from the truth or falsity of a condition. This also means we need a separate function from the flow function, a "conditional flow" or filtering function. Treehydra calls it "flowStateCond". The input is a state, a conditional expression, and whether the expression is true or false. The output is a state representing the values from the original state that pass the expression. | |||
In the example above, we are in state "a = ?" and learn that the condition "a == 0" is true. So we filter '?' down to just the values equal to 0, namely 0 itself. So the result is "a = 0". | |||
If the input state had instead been "a = NZ', then we filter NZ (nonzero) down to just the values equal to 0, which is the empty set. So the result is "a = bottom", effectively proving that this branch is not taken. | |||
Treehydra contains the basic machinery to detect conditionals and exclude branches that cannot be executed. The user only has to supply the flowStateCond function. | |||
== More Powerful Lattices == | == More Powerful Lattices == | ||
== ESP == | == ESP == | ||