[cfe-dev] [Analyzer] The way to solve false negatives about ArrayBoundCheckerV2?

[Gábor Horváth via cfe-dev]

Hi,

On 23 October 2017 at 13:47, Wong Henry via cfe-dev <cfe-dev at lists.llvm.org>
wrote:

> Hi all,
> Due to the limitations of range-based constraint solver,
> ArrayBoundCheckerV2 has false negatives now.(http://clang-
> developers.42468.n3.nabble.com/improving-the-ArrayBoundChecker-td4037769.
> html#a4037803).
>
> There are some simple false negative scenes can be tried to solve, like
> "index * sizeof(int) >= 10", and there are two ways I can think of to solve
> this problem.
>
> 1.Modify the ArrayBoundCheckerV2, convert "symbol * sizeof(ElementType) >=
> RegionExtent" into "symbol >= RegionExtent / sizeof(ElementType)", "sizeof
> (ElementType)" and "RegionExtent" can get as concrete int. If we're
> dealing with two known constants, we can perform the operation '/' directly.
>

Which version did you chek? Are you sure that this transformation is not
done yet? See
https://github.com/llvm-mirror/clang/blob/master/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp#L83


>
> 2.Modify "RangedConstraintManager::computeAdjustment()", which can
> support other arithmetic operators, such as '/', etc. This method can
> slightly increase the ability of the constraint solver,  so that other
> false negatives can also be solved. For example:
>

While improving the constraint manager is a good idea generally speaking,
it is not a trivial task. For example the work on the ArrayBoundCheckerV2
introduced some false positives, see: https://reviews.llvm.org/D39049

The other problem is the performance. I think if you feel like improving
the situation here, it would be awesome, but we should make sure not to
regress the performance much and also work correctly for edge cases
(overflows, signedness conversions).

Regards,
Gábor


>
> ==========================================================
>   1 int num_foo;
>
>
>   2 int foo()
>   3 {
>   4     int *ptr = 0;
>   5     if (num_foo > 100) {
>   6         if (num_foo / 10 < 10)
>   7             *ptr = 0;    <---- Dereference of null pointer (loaded
> from variable 'ptr')
>   8     }
>   9 }
>  10
>  11 int num_goo;
>  12 int goo()
>  13 {
>  14     int *ptr = 0;
>  15     if (num_goo > 100) {
>  16         if (num_goo < 100)
>  17             *ptr = 0;
>  18     }
>  19 }
> ==========================================================
> I want to know which method is appropriate? After the constraint solver Z3
> is integrated, is it necessary to implement the second methods?
>
> 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/20171023/d96889b3/attachment.html>