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

[Wong Henry 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20171023/123045b3/attachment.html>