[cfe-dev] improving the ArrayBoundChecker.

[Per Viberg]

// oops, sent this by mistake to the commits list..


Hi,

I am going to look into the ArrayBoundChecker. Currently it doesn't handle symbolic constraints on indexing with '>' or '<' properly.

There are two implementation of the ArrayBoundChecker, and some errors are not detected with the V2, (see below), so my main question is: Which of the ArrayBoundV2 or ArrayBound is the one that should be improved on? Also, any specific class/interfaces that should/shouldn't be used?. Any other useful hints on where to fix this are also highly appreciated.

cheers!,

Per



The ArrayBound check doesn't find this error:

void writeOutOfBoundsGEConstraint(int x) {
  int a[10];
  if (x >= 10)
     a[x] = 5;  // ← 1. write access GE does not generate error
}

It does however find the read access with '>', but only using ArrayBound, _not_ ArrayBoundV2.

int readOutOfBoundsGEConstraint(int x) {
  int a[10];
  int g=5;
  if (x >= 10)
    g = a[x];   // ← 2. read access GE generate error on V0
  return g;
}

out-of-bounds_2.c:13:9: warning: Access out-of-bound array element (buffer overflow)
    g = a[x];   // ← 2. read access GE generate error on V0
        ^~~~

The rest below are found in both ArrayBound and ArrayBoundV2:

void writeOutOfBoundsEQ(int x) {
  int a[10];
  if (x == 10)
     a[x] = 0;  // ← 3. write access EQ generate error on V0 and V2
}

out-of-bounds_2.c:20:11: warning: Access out-of-bound array element (buffer overflow)
     a[x] = 0;  // ← 3. write access EQ generate error on V0 and V2
     ~~~~ ^

int readOutOfBoundsEQ(int x) {
  int a[10];
  int g=5;
  if (x == 10)
    g = a[x];   // ← 4. read access EQ generate error on V0 and V2
  return g;
}

out-of-bounds_2.c:26:9: warning: Access out-of-bound array element (buffer overflow)
    g = a[x];   // ← 4. read access EQ generate error on V0 and V2
        ^~~~


.......................................................................................................................
Per Viberg Senior Engineer
Evidente ES East AB  Warfvinges väg 34  SE-112 51 Stockholm  Sweden
Phone:    +46 (0)8 402 79 00
Mobile:    +46 (0)70 912 42 52
E-mail:     Per.Viberg at evidente.se<mailto:Per.Viberg at evidente.se>

www.evidente.se<http://www.evidente.se>
This e-mail, which might contain confidential information, is addressed to the above stated person/company. If you are not the correct addressee, employee or in any other way the person concerned, please notify the sender immediately. At the same time, please delete this e-mail and destroy any prints. Thank You.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20140211/8dd126aa/attachment.html>