Impossible code path involving an expression and its negation

[llvmbot]

Bugzilla Link	7491
Version	unspecified
OS	MacOS X
Reporter	LLVM Bugzilla Contributor
CC	@belkadan,@tkremenek,@xuzhongxing

Extended Description

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)

[llvmbot]

assigned to @tkremenek

[tkremenek]

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

[llvmbot]

Preprocessed source
This is the source file, preprocessed with gcc (i686-apple-darwin10-gcc-4.2.1) using the default configuration for the project.

[belkadan]

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.

[belkadan]

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.

[xuzhongxing]

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"?

[tkremenek]

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).

[tkremenek]

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)

[belkadan]

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 ( && !), for any functional .