Impossible code path involving an expression and its negation

[Quuxplusone]

Bugzilla Link	PR7491
Status	NEW
Importance	P normal
Reported by	Andrea Canciani (ranma42@gmail.com)
Reported on	2010-06-25 04:22:23 -0700
Last modified on	2010-08-18 01:00:50 -0700
Version	unspecified
Hardware	Macintosh MacOS X
CC	jrose@belkadan.com, kremenek@apple.com, llvm-bugs@lists.llvm.org, xu_zhong_xing@163.com
Fixed by commit(s)
Attachments	cairo-lzw.i (229431 bytes, text/plain)
Blocks
Blocked by
See also

As shown here http://people.freedesktop.org/~ranma42/scan-build-2010-06-25-
1/report-RS3Z6A.html#EndPath
the static analyzer is reposting an impossible code path:
if (bytes_remaining) // not taken
and right after that
if (bytes_remaining == 0) // not taken

OS: MacOS 10.6.4
ANALYZER BUILD: checker-242 (2010-06-21 13:44:48)

[Quuxplusone]

Andrea: Can you attached a preprocessed file of this source file? That will provide a self-contained test case. Thanks.

[Quuxplusone]

Attached cairo-lzw.i (229431 bytes, text/plain): Preprocessed source

[Quuxplusone]

Partly fixed in r106972 (see misc-ps.m for a reduced test case). The main thing
was a FIXME left over in SimpleConstraintManager: non-comparison symbolic
expressions weren't being implicitly compared to zero. But this is still going
to be a problem for cases where the symbolic expression involves an operation
we can't reason about.

int x = foo() * 2;
if (x) return;
if (!x) return;
(void)*NULL; // unreachable but will still warn.

[Quuxplusone]

We could fix this by using conjured symbols for /any/ binary operation whose result we can't model...i.e. whenever Bind() is given an UnknownVal, we conjure a symbol. But that wouldn't help for cases where the expression is repeated.

[Quuxplusone]

(In reply to comment #4)
> We could fix this by using conjured symbols for /any/ binary operation whose
> result we can't model...i.e. whenever Bind() is given an UnknownVal, we
conjure
> a symbol. But that wouldn't help for cases where the expression is repeated.

Hi Jordy,

What do you mean by "the expression is repeated"?

[Quuxplusone]

(In reply to comment #4)
> We could fix this by using conjured symbols for /any/ binary operation whose
> result we can't model...i.e. whenever Bind() is given an UnknownVal, we
conjure
> a symbol. But that wouldn't help for cases where the expression is repeated.

We should just fix it the right way, by improving the symbolic analysis.  In
practice conjuring a symbol here won't help much since we already conjure
symbols in assignments (where values actually get propagated to be consulted
farther down the path).

[Quuxplusone]

(In reply to comment #5)
> (In reply to comment #4)
> > We could fix this by using conjured symbols for /any/ binary operation whose
> > result we can't model...i.e. whenever Bind() is given an UnknownVal, we
conjure
> > a symbol. But that wouldn't help for cases where the expression is repeated.
>
> Hi Jordy,
>
> What do you mean by "the expression is repeated"?

I'm assuming Jordy meant something like:

if (exp1 op exp2)
...
if (exp1 op exp2)

[Quuxplusone]

(In reply to comment #7)
> (In reply to comment #5)
> > (In reply to comment #4)
> > > We could fix this by using conjured symbols for /any/ binary operation
whose
> > > result we can't model...i.e. whenever Bind() is given an UnknownVal, we
conjure
> > > a symbol. But that wouldn't help for cases where the expression is
repeated.
> >
> > Hi Jordy,
> >
> > What do you mean by "the expression is repeated"?
>
> I'm assuming Jordy meant something like:
>
> if (exp1 op exp2)
> ...
> if (exp1 op exp2)

Right, or the equivalent with a negation thrown in.

I didn't notice that assignments conjured symbols. That's probably as much as
conjuring symbols is going to help, then, unless we can unique them by the
SymExprs they represent and the current state, which is probably going too far.

Minimal test case is probably of the form (<exp> && !<exp>), for any functional
<exp>.