ArrayBoundCheckerV2 false positive due to dead symbol remove.

[Quuxplusone]

Bugzilla Link	PR27820
Status	NEW
Importance	P normal
Reported by	Lei Zhang (ioripolo@foxmail.com)
Reported on	2016-05-19 22:24:30 -0700
Last modified on	2016-06-01 00:03:11 -0700
Version	3.6
Hardware	PC Windows NT
CC	humeafo@gmail.com, llvm-bugs@lists.llvm.org
Fixed by commit(s)
Attachments
Blocks
Blocked by
See also

I got a simple test case as below:

  typedef struct _FILE FILE;
  extern FILE *stdin;

  void foo() {
    int pos = 1;
    int table[] = {1, 2};
    char inputBuffer[2] = "";
    fgets(inputBuffer, 2, stdin);
    pos = atoi(inputBuffer);
    if (pos > 0 && pos <=2) {
      table[pos] = 10;
    }
  }

And with the command line "clang -cc1 -analyze -w -analyzer-
checker=alpha.security.ArrayBoundV2 -analyzer-checker=alpha.security.taint
test.c"

Then i got a warning like this:

  test.c:15:16: warning: Out of bound memory access (index is tainted)
    table[pos] = 10;
    ~~~~~~~~~~~^~~~
  1 warning generated.

But we have a validation "if (pos > 0 && pos <=2)", so the extent of pos should
be OK.

After took a look inside this false positive, i think i found the reason:

In the 'PreStmtPurgeDeadSymbols' process of the assign binaryoperator
'table[pos] = 10', the 'pos' is not live any more, so the conjured symbol and
it's constraint were removed.

Later when we check the location for ArrayBoundV2, because the removement of
the conjured symbol, both 'state_exceedsUpperBound'and 'state_withinUpperBound'
are not null. Finally got the warning according the logic below.

    // If we are under constrained and the index variables are tainted, report.
    if (state_exceedsUpperBound && state_withinUpperBound) {
      if (state->isTainted(rawOffset.getByteOffset()))
        reportOOB(checkerContext, state_exceedsUpperBound, OOB_Tainted);
        return;
    }

[Quuxplusone]

int table[] = {1, 2};
when index is 2, it's really out of bound.

so the problem besides you described the checker has a serious bug too.

[Quuxplusone]

Sorry for this mistake.

But if we change the condition to

if (pos >= 0 && pos <2)

this false positive remains