313
edits
Changes
→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 ==
== ESP ==
