[clang] [llvm] [analyzer] Consolidate array bound checkers (PR #125534)

Tue Feb 4 06:25:09 PST 2025

NagyDonat wrote:

I evaluated a sample of 10 random ArrayBoundV2 results from FFMPEG and I found the following:
- [Unjustified assumption of third iteration](https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=ffmpeg_n4.3.1_edonnag_llvm-main_1883de3&newcheck=ffmpeg_n4.3.1_edonnag_llvm-main_f8aa6f1&diff-type=New&report-id=6936068&report-hash=4849805b289670414ad1c51975c2eeac&report-filepath=ffmpeg%2Flibavfilter%2Faf_amultiply.c) because my recent "[don't assume third iteration](https://github.com/llvm/llvm-project/pull/119388)" change doesn't handle the case when there is a short-circuiting operator in the loop condition.
  - IIRC this covers several (5-10??) false positives in this particular project, but should be significantly less common elsewhere (FFMPEG has an unusually high concentration of 2-element arrays).
  - Eliminating these would be a technically complex task, but has no fundamental obstacles. However they're rare enough that I'm not sure if they're worth the effort. 
- [Non-realistic overflow](https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=ffmpeg_n4.3.1_edonnag_llvm-main_1883de3&newcheck=ffmpeg_n4.3.1_edonnag_llvm-main_f8aa6f1&diff-type=New&report-id=6936379&report-hash=10c43369fbbd8b9359afdebd019643ee&report-filepath=ffmpeg%2Flibavcodec%2Fansi.c) where the analyzer assumes that the code was able to read $\approx 2^{31}$ arguments from the input (which can't happen, but the analyzer cannot deduce this precondition of the analyzed function).
- [Correlated if conditions](https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=ffmpeg_n4.3.1_edonnag_llvm-main_1883de3&newcheck=ffmpeg_n4.3.1_edonnag_llvm-main_f8aa6f1&diff-type=New&page=2&report-id=6936490&report-hash=7765e71a226bf336d525811ccb01c476&report-filepath=ffmpeg%2Flibavcodec%2Fhevc_cabac.c): assuming that the `av_clip` call in line 1103 returns `-s->ps.sps->qp_bd_offset` and then assuming that this result is `> 51` produces an array underflow. I suspect that this can't happen (e.g. I'd guess that `s->ps.sps->qp_bd_offset` is always nonnegative), but I don't think that Z3 crosscheck would be helpful.
- [A classical "assuming skipped loop" error](https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=ffmpeg_n4.3.1_edonnag_llvm-main_1883de3&newcheck=ffmpeg_n4.3.1_edonnag_llvm-main_f8aa6f1&diff-type=New&page=2&report-id=6936516&report-hash=51d11525a3b6b456f1076aed8b790e61&report-filepath=ffmpeg%2Flibavcodec%2Fhevcpred_template.c) which would be silenced by [the new `assume-one-iteration` option](https://github.com/llvm/llvm-project/pull/125494) or a well-placed assertion. (Enabling that option would silence 34 of the 187 ArrayBoundV2 errors on this project.)
- [Technically justified, but unwanted assumption of a third iteration](https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=ffmpeg_n4.3.1_edonnag_llvm-main_1883de3&newcheck=ffmpeg_n4.3.1_edonnag_llvm-main_f8aa6f1&diff-type=New&page=3&report-id=6936484&report-hash=f8cf2f54adb6af9636d26f5275b959fc&report-filepath=ffmpeg%2Flibavcodec%2Fhapdec.c): first there is an `if` where the analyzer can assume `ctx->texture_count != 2` so later when the analyzer assumes that `ctx->texture_count >= 2` (i.e. it may enter the second iteration of the loop), it gets "enough fuel" to also enter the third iteration (which is an overflow error). This is a correlated assumption error (similar to the "correlated if" issue), so solving it is blocked by fundamental theoretical obstacles.
- [Yet another "assuming skipped loop" issue](https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=ffmpeg_n4.3.1_edonnag_llvm-main_1883de3&newcheck=ffmpeg_n4.3.1_edonnag_llvm-main_f8aa6f1&diff-type=New&page=3&report-id=6936513&report-hash=30e1c1cefaad9086c13fdb53692a0ff4&report-filepath=ffmpeg%2Flibavcodec%2Fhevcpred_template.c), very similar (but somewhat more complex) than the previous one.
- [Technically a true positive](https://codechecker-demo.eastus.cloudapp.azure.com/Default/report-detail?run=ffmpeg_n4.3.1_edonnag_llvm-main_1883de3&newcheck=ffmpeg_n4.3.1_edonnag_llvm-main_f8aa6f1&diff-type=New&page=5&report-id=6936917&report-hash=715cc85d94e2fcebde8b49ec355401f9&report-filepath=ffmpeg%2Ffftools%2Fffmpeg_opt.c) where the analyzer assumes that the second element of `static const char *opt_name_reinit_filters[] = {"reinit_filter", NULL};` may be non-`NULL` when the analyzed function is executed. (For a programmer it's obvious that this is a constant, but the analyzer cannot deduce this. The programmer could resolve this by adding an extra `const` qualifier.)
- The remaining three issues in my random sample are all duplicates of this one -- they appear as separate reports because the error is within a **macro that's expanded in several locations and apparently produces 80 (!) ArrayBoundV2 reports** (which correspond to other analogous arrays instead of `opt_name_reinit_filters`).

-------

These reports don't look like solver issues, I don't think that Z3 refutation or similar improvements would help with any of them. (:thinking:  In fact, perhaps Z3 refutation was already enabled -- I don't know what's the default setting in our CI.) 

In my opinion the only actionable conclusion is that we should make report deduplication more aggressive around macros -- e.g. I could imagine a heuristic that uses the location within the macro (instead of the location of the particular macro expansion) for deduplication if the complexity/length of the macro is above a certain threshold. (Otherwise unrelated reports "coming from" a small macro like `MAX` or something similar shouldn't be conflated, but reports coming from the same part of a "big" macro should be unified.) This would consolidate almost half of the reports into a single report (which is arguably a true positive, so shouldn't be silenced). However this improvement is independent of ArrayBoundV2 and IMO shouldn't block this PR.

After that, `assume-one-iteration` can eliminate 34 additional reports which are mostly unwanted -- however that change would also cause the loss of true positives (on projects that are less stable and have true positives...), so it's likely that we don't want to enable it.

The remaining 74 reports are probably false positives that are caused by incompatible assumptions ("correlated if" issues), invisible preconditions (the programmer knows something about some argument/input of the toplevel analyzed function, but the analyzer cannot deduce this) or other random issues.

https://github.com/llvm/llvm-project/pull/125534