Open Quuxplusone opened 3 years ago
Bugzilla Link | PR49986 |
Status | CONFIRMED |
Importance | P normal |
Reported by | Marius Messerschmidt (marius.messerschmidt@googlemail.com) |
Reported on | 2021-04-16 01:22:34 -0700 |
Last modified on | 2021-04-30 11:27:43 -0700 |
Version | trunk |
Hardware | PC Linux |
CC | alexfh@google.com, balazs.benics@sigmatechnology.se, dcoughlin@apple.com, djasper@google.com, klimek@google.com, llvm-bugs@lists.llvm.org, marius.messerschmidt@googlemail.com, N.James93@hotmail.co.uk, noqnoqneo@gmail.com, vsavchenko@apple.com |
Fixed by commit(s) | |
Attachments | |
Blocks | |
Blocked by | |
See also |
Moving to the static-analyzer
Yes, this is a false positive.
You can suppress it via enabling the crosscheck-with-z3=true analyzer-config.
This will validate path constraints with the Z3 SMT solver. It has negligible
time overhead.
-----
Loops and floating numbers are not modeled perfectly.
Here is your test case annotated with some analyzer intrinsics.
https://godbolt.org/z/GqnWfToKr
I suspect that this is connected to how the memory is modelled within the
analyzer.
The main difference between using memset and raw loop is that the latter will
do a state-split at each iteration. And the loop upper bound has a
multiplication, which is also hard to model due to wrapping and stuff,...
By checking the state dumps, I can see that the 'array' has **some** direct
bindings in the store, binding 'unknown' to some elements. (These were stored
in the initialized raw loop)
I suspect that this worth investigating in depth.
Yes this is a solver bug. You can see from the bug path that it thinks it's plausible to assume that 'nValues' is equal to 2 while 'sqr' is equal to 1.
It's also definitely possible that 'nValues' is equal to 65536 while 'sqr' is equal to 0. Which may or may not make the warning useful on the original unreduced code. But that's not the situation we actively warn about.
Let me summon Valeriy as well.