On Apr 30, 2014, at 10:23 , Manuel Klimek <[email protected]> wrote:
> On Wed, Apr 30, 2014 at 7:16 PM, Jordan Rose <[email protected]> wrote: > > On Apr 30, 2014, at 1:35 , Manuel Klimek <[email protected]> wrote: > >> On Wed, Apr 30, 2014 at 5:34 AM, Jordan Rose <[email protected]> wrote: >> What this is basically saying is that we will never be in a situation where >> the condition (or the rightmost branch in the condition) was not evaluated >> in the current CFG block. That seems a bit questionable in general but >> reasonable given the way the CFG is currently constructed. >> >> Well, all I've been trying to do here is to a) document and b) encode in the >> assert the actual current CFG invariant the analyzer relies on for >> correctness. >> The problem is that if what is returned from ResolveCondition is *not* >> evaluated in the block, we have no guarantee that it was evaluated at all - >> but the correctness of all the path analyses relies on it being in the SVal >> cache of the state. Otherwise we will assume branches are reachable that are >> clearly unreachable because of which parts of the logical operator tree we >> *assumed* to be true (so we know the condition must be statically knowable >> in the current state). >> >> I have a hard time putting that into words though, so any help for how to >> wordsmith this to be easier to understand would be highly appreciated... > > "in the SVal cache of the state" is "in the Environment" using analyzer > terminology (it's not really a cache, since it's not reproducible) > > exactly :) I learned that today while doing more digging through the code... > > , but since things regularly get cleaned out of the Environment there aren't > that many cases where a condition would be present but wouldn't have been > evaluated in the previous block. > > I don't yet understand how exactly things get cleaned out of the environment > (other than losing scope). > It seems to me like a lot of the warnings rely on branch conditions always > being in the environment at the point of the terminator, otherwise it's easy > to produce false positives in unreachable code paths. The presence of bindings in the Environment is controlled by the LiveVariables analysis. Essentially, an expression is live from the point of its evaluation to the point it is consumed. Unfortunately, it can be a little more complicated than that sometimes...especially with LiveVariables being a flow-sensitive analysis but not a path-sensitive one. (This is one of the reasons for the liveness bug that Pavel uncovered.) Please do commit the change. Thanks for taking the time to work through it! Jordan
_______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
