[analyzer] `security.ArrayBound` false positive

[alyssais]

#include <stdlib.h>
#include <assert.h>
#include <unistd.h>
#include <stdint.h>

#include <sys/stat.h>

void foo(size_t max_path_len)
{
	assert(max_path_len < SIZE_MAX);
	char *buf = malloc(max_path_len + 1);
	assert(buf);

	int path_len_signed = readlink("hello", buf, max_path_len);
	assert(path_len_signed >= 0);
	size_t path_len = (size_t)path_len_signed;
	assert(path_len <= max_path_len);

	buf[path_len] = 0;
}

Here the access to buf[path_len] is always valid, but the analyzer doesn't think so. This happens even if I change SIZE_MAX in the first assert to 5, so it's not anything to do with huge allocations.

$ clang-tidy repro.c 
Error while trying to load a compilation database:
Could not auto-detect compilation database for file "repro.c"
No compilation database found in /tmp or any parent directory
fixed-compilation-database: Error while opening fixed database: No such file or directory
json-compilation-database: Error while opening JSON database: No such file or directory
Running without flags.
3 warnings generated.
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/stdint.h:95:11: warning: '__INT64_C' macro redefined [clang-diagnostic-macro-redefined]
   95 | #  define __INT64_C(c)  c ## L
      |           ^
note: previous definition is here
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/stdint.h:96:11: warning: '__UINT64_C' macro redefined [clang-diagnostic-macro-redefined]
   96 | #  define __UINT64_C(c) c ## UL
      |           ^
note: previous definition is here
/tmp/repro.c:19:2: warning: Potential out of bound access to the heap area with tainted index [clang-analyzer-security.ArrayBound]
   19 |         buf[path_len] = 0;
      |         ^~~~~~~~~~~~~
/tmp/repro.c:10:9: note: Assuming 'max_path_len' is < -1
   10 |         assert(max_path_len < SIZE_MAX);
      |                ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:11: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |           ^~~~
/tmp/repro.c:10:2: note: Taking true branch
   10 |         assert(max_path_len < SIZE_MAX);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:12:9: note: Assuming 'buf' is non-null
   12 |         assert(buf);
      |                ^
/tmp/repro.c:12:2: note: Taking true branch
   12 |         assert(buf);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:14:24: note: Taint originated here
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:14:24: note: Assuming that the 3rd argument to 'readlink' is <= 18446744073709551615
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:14:24: note: Taint propagated to the return value
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:14:24: note: Assuming that 'readlink' is successful
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:15:9: note: 'path_len_signed' is >= 0
   15 |         assert(path_len_signed >= 0);
      |                ^
/tmp/repro.c:15:2: note: Taking true branch
   15 |         assert(path_len_signed >= 0);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:17:9: note: 'path_len' is <= 'max_path_len'
   17 |         assert(path_len <= max_path_len);
      |                ^
/tmp/repro.c:17:2: note: Taking true branch
   17 |         assert(path_len <= max_path_len);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:19:2: note: Access of the heap area with a tainted index that may be too large
   19 |         buf[path_len] = 0;
      |         ^~~~~~~~~~~~~

[llvmbot]

@llvm/issue-subscribers-clang-static-analyzer

Author: Alyssa Ross (alyssais)

```c #include <stdlib.h> #include <assert.h> #include <unistd.h> #include <stdint.h>

#include <sys/stat.h>

void foo(size_t max_path_len)
{
assert(max_path_len < SIZE_MAX);
char *buf = malloc(max_path_len + 1);
assert(buf);

int path_len_signed = readlink("hello", buf, max_path_len);
assert(path_len_signed >= 0);
size_t path_len = (size_t)path_len_signed;
assert(path_len <= max_path_len);

buf[path_len] = 0;

}

Here the access to `buf[path_len]` is always valid, but the analyzer doesn't think so.  This happens even if I change `SIZE_MAX` in the first assert to `5`, so it's not anything to do with huge allocations.

```ShellSession
$ clang-tidy repro.c 
Error while trying to load a compilation database:
Could not auto-detect compilation database for file "repro.c"
No compilation database found in /tmp or any parent directory
fixed-compilation-database: Error while opening fixed database: No such file or directory
json-compilation-database: Error while opening JSON database: No such file or directory
Running without flags.
3 warnings generated.
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/stdint.h:95:11: warning: '__INT64_C' macro redefined [clang-diagnostic-macro-redefined]
   95 | #  define __INT64_C(c)  c ## L
      |           ^
note: previous definition is here
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/stdint.h:96:11: warning: '__UINT64_C' macro redefined [clang-diagnostic-macro-redefined]
   96 | #  define __UINT64_C(c) c ## UL
      |           ^
note: previous definition is here
/tmp/repro.c:19:2: warning: Potential out of bound access to the heap area with tainted index [clang-analyzer-security.ArrayBound]
   19 |         buf[path_len] = 0;
      |         ^~~~~~~~~~~~~
/tmp/repro.c:10:9: note: Assuming 'max_path_len' is < -1
   10 |         assert(max_path_len < SIZE_MAX);
      |                ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:11: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |           ^~~~
/tmp/repro.c:10:2: note: Taking true branch
   10 |         assert(max_path_len < SIZE_MAX);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:12:9: note: Assuming 'buf' is non-null
   12 |         assert(buf);
      |                ^
/tmp/repro.c:12:2: note: Taking true branch
   12 |         assert(buf);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:14:24: note: Taint originated here
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:14:24: note: Assuming that the 3rd argument to 'readlink' is <= 18446744073709551615
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:14:24: note: Taint propagated to the return value
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:14:24: note: Assuming that 'readlink' is successful
   14 |         int path_len_signed = readlink("hello", buf, max_path_len);
      |                               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/tmp/repro.c:15:9: note: 'path_len_signed' is >= 0
   15 |         assert(path_len_signed >= 0);
      |                ^
/tmp/repro.c:15:2: note: Taking true branch
   15 |         assert(path_len_signed >= 0);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:17:9: note: 'path_len' is <= 'max_path_len'
   17 |         assert(path_len <= max_path_len);
      |                ^
/tmp/repro.c:17:2: note: Taking true branch
   17 |         assert(path_len <= max_path_len);
      |         ^
/nix/store/cz0l7aa2dzk2sgz9b55i1wzn0v80ygwq-glibc-2.40-66-dev/include/assert.h:117:7: note: expanded from macro 'assert'
  117 |       if (expr)                                                         \
      |       ^
/tmp/repro.c:19:2: note: Access of the heap area with a tainted index that may be too large
   19 |         buf[path_len] = 0;
      |         ^~~~~~~~~~~~~

[NagyDonat]

Thanks for the bug report, I was able to reproduce it with the code that you provided (on a current main revision, also with the version where SIZE_MAX is replaced by 5). I don't have any concrete guesses immediately, but I know that conversions between integer types are a bit shaky in the analyzer, so I'm not very surprised to see this bug report.

I'll try to investigate and resolve this.

[NagyDonat]

I investigated the issue and it turns out that (in this particular case) the casting works correctly – and the problem is with the addition.

The analyzer automatically knows that the result of readlink is <= its third argument, so it knows that path_len <= max_path_len (even without the assertion that asserts this), but it cannot deduce that this relationship implies path_len < max_path_len + 1 (which is the extent of the memory region). I see that the assertion assert(max_path_len < SIZE_MAX) guarantees that this deduction would be correct, but this " $A \le B$ implies $A &lt; B + C$ if $C$ is a positive and there is no overflow" feature is simply not yet implemented in the analyzer.

It would be nice to extend the analyzer engine with deduction rules like this, but changing these "central" parts is very difficult because they might affect the result set of many checkers and cause unpredictable performance regressions (especially in the worst case). Also, it would be nontrivial to find the proper "size" of these rules: if they only cover a few trivial cases, then it's not worth the effort; but if we aim to be general, then they may become too complex and slow.

I hope that eventually the analyzer engine will be able to cover "common sense" deductions like this one (and it is good to have a concrete reproducer that highlights this issue), but unfortunately I don't think that it can be squeezed into the short term development plans of the existing developers (and this task is far too complex to be tackled as the first project of a new contributor).

However, the static analyzer also has an optional feature called "crosscheck-with-z3" (also known as "Z3 refutation") which postprocesses the analyzer results with the Z3 theorem prover and discards the results that are infeasible. I strongly suspect that this false positive would have been discarded by that postprocessing step. EDIT: I verified that this false positive does not appear when crosscheck-with-z3 is enabled.

Unfortunately this crosscheck-with-z3 configuration option of the static analyzer is off by default, and when the static analyzer is used through Clang Tidy (as in your reproducer example) AFAIK there is no way to forward configuration options to the static analyzer. (It also requires building clang with support for Z3.)

[NagyDonat]

I'm un-assigning this ticket from myself, because I tracked down that this is a symptom of a missing engine feature (that the analyzer can't deduce that A <= B implies A < B+1) and I don't have time to work on fixing that in the foreseeable future.