[cfe-dev] [Analyzer] ArrayBoundCheckerV2: Why the analyzer add the constraint `Idx < ArraySize` after element access?

[Artem Dergachev via cfe-dev]

If 'x' is 100 or greater, it'd mean that undefined behavior has already 
occured, and it's pointless to explore that path further.

Same with 'x' being less than 0, so the checker should have added that 
as well.

So i believe that this is a valid behavior. A similar approach is taken 
by, say, DivZeroChecker that refutes the "y == 0" patch after "x / y" is 
evaluated. NullDereferenceChecker also assumes that all dereferenced 
pointers are non-null.

If they can prove that the operation is indeed unsafe on the current 
path, then the assumption would fail, and these checkers would report a 
warning instead.

What sort of problem are you having with these assumptions? Why are they 
affecting your checker? With constraints it shouldn't normally ever be 
an issue, because adding constraints doesn't really "mutate" the program 
state, it just "clarifies" it.

On 7/11/18 3:27 AM, Henry Wong via cfe-dev wrote:
> Hi all,
>
> For the code below, the `ArrayBoundCheckerV2` will add the constraint 
> `x < 100` after the `buf[x] = 1`, see https://reviews.llvm.org/D23112.
> ```
> void test_assume_after_access(unsigned long x) {
>     int buf[100];
>     buf[x] = 1;
>     clang_analyzer_eval(x <= 99); // expected-warning{{TRUE}}
> }
> ```
>
> 1.What is the purpose for doing this?
> 2. why not add `x >= 0` as well?
>
> I used`checkLocation()`, same as `ArrayBoundCheckerV2`, in my own 
> checker too. Due to the uncertain calling order, I got the wrong 
> constraints on `x` in my own checker. That's why I pay attention to 
> this problem.
>
> Thanks in advance!
>
> Henry Wong
> Qihoo 360 Codesafe Team
>
> _______________________________________________
> cfe-dev mailing list
> cfe-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20180711/ff8f9aa6/attachment.html>