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. > As I understand it, the actual purpose of ResolveCondition is that when > your branch condition is a BinaryOperator, you might not have bothered to > evaluate the BinaryOperator expression itself, but if not you definitely > would have evaluated its RHS. (Testing *without* ResolveCondition, this > happens when you have chained logical operators "a || b || c", because we > don't stop to evaluate the entire "a || b" expression when deciding whether > to get to "c". We know we wouldn't have gotten to this point if we hadn't > evaluated the RHS.) > Exactly. > Looking at Ted's original patch, it looks like some constructs will still > stop to evaluate the expression before using it as a condition, so if the > last statement in the CFG really does happen to be the whole logical > expression, we can use it as a condition directly. > > ...hm, that's still not so clearly worded! > :) I can just check in the current version, seems better than not having any documentation, and I think it's factually right (if not perfectly worded)... > > > (Especially if/when this whole block of code can go away!) >> > > I'm not sure what you mean about "this whole block of code can go away". > The only part that will go away is the special case handling for temporary > dtor terminators, as those will be handled in a completely different code > path. > > > Ah, you're right. The code is there to handle a logical expressions being > used as conditions, and that's not going away. It took me a long time to > understand that this comment: > > // For logical operations, we still have the case where some branches > // use the traditional "merge" approach and others sink the branch > // directly into the basic blocks representing the logical operation. > // We need to distinguish between those two cases here. > > refers to the "some constructs will still evaluate the expression before > using it as a condition" I said above. > > Jordan >
_______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
