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

[Henry Wong via cfe-dev]

Thanks for the explanation, Artem! Sorry for my mistaken! ArrayBoundCheckerV2 did add the `Idx >= 0` constraint as well.

It make sense to me that add the constraints on the symbol according to the program semantic!

My problem can be explained by the following diagram. IMHO, the constraints should be added on `x` after the access really occurred,  this request may be a bit picky.


                     ---------------------------------------------------------------
                    |        BinaryOperator 0x9a0d8f0 buf[x] = 1           |
                    | --------------------------------------------------------------
                    |                        Ranges are empty.                           |
                     ---------------------------------------------------------------
                                                              |
                                                            \|/    ArrayBoundCheckerV2::checkLocation()
                     ---------------------------------------------------------------
                    |        BinaryOperator 0x9a0d8f0 buf[x] = 1            |
                    | --------------------------------------------------------------
                    | Ranges of symbol values:                                       |
                    |   reg_$0<unsigned long x> : { [0, 99] }                  |
                     ----------------------------------------------------------------
                                                             |
                                                           \|/
                                                                   MyOwnChecker::checkLocation()
                                                                   Want to get the original constraint info on `x`, however the constraint information has changed.
                                                            ...
                                                             |
                                                           \|/
                     ----------------------------------------------------------------
                    |        BinaryOperator 0x9a0d8f0 buf[x] = 1           |
                    | PostStore                                                                   |
                    | ---------------------------------------------------------------
                    | Ranges of symbol values:                                       |
                    |   reg_$0<unsigned long x> : { [0, 99] }                 |
                     ---------------------------------------------------------------
                                                            |
                                                          \|/   The constraint should be added to `x` after the access really happens.

My problem has been solved by moving the code logic of `MyOwnChecker::checkLocation()` to `ArrayBoundCheckerV2::checkLocation()`.

Henry Wong
Qihoo 360 Codesafe Team
________________________________
From: Artem Dergachev <noqnoqneo at gmail.com>
Sent: Thursday, July 12, 2018 3:00
To: Henry Wong; cfe-dev at lists.llvm.org
Subject: Re: [cfe-dev] [Analyzer] ArrayBoundCheckerV2: Why the analyzer add the constraint `Idx < ArraySize` after element access?

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<mailto: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/20180712/840aeb2c/attachment.html>