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

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

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

Eric Fiselier via cfe-dev
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.

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:

==========================================================
  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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [Analyzer] The way to solve false negatives about ArrayBoundCheckerV2?

Eric Fiselier via cfe-dev
Hi,

On 23 October 2017 at 13:47, Wong Henry via cfe-dev <[hidden email]> 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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

答复: [Analyzer] The way to solve false negatives about ArrayBoundCheckerV2?

Eric Fiselier via cfe-dev
Thank you for your explanation, Gábor! My mistake. I'll take a good look at the information you provide.

Henry Wong
Qihoo 360 Codesafe Team

发件人: Gábor Horváth <[hidden email]>
发送时间: 2017年10月23日 11:54
收件人: Wong Henry
抄送: [hidden email]
主题: Re: [cfe-dev] [Analyzer] The way to solve false negatives about ArrayBoundCheckerV2?
 
Hi,

On 23 October 2017 at 13:47, Wong Henry via cfe-dev <[hidden email]> 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
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev



_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev