Buffer index sensitivity with non variant GEP instructions

[davidtr1037]

In the following code:
int f() { char buf[10] = {0,}; int x = buf[0]; int y = buf[1]; return x + y; }
The GEP instructions which correspond to x and y are both constant,
but when we check aliasing, we get MayAlias.
Actually, in both cases, the LocationSet of the GepObjPN is constant and equal to 0.
Is this a bug or SVF handles buffers always in an index insensitive way?

[yuleisui]

Hi David,

Variant GEP is used to handle pointer arithmetic when iterating fields of a struct.
Given ”p = q + i", if q points to an object o, then p may point any of o's fields.

Arrays (like your case) are always handled insensitively in the default memory model.

I believe you can use the following option to get what you wanted:

wpa -ander -locMM xx.bc

"-locMM" uses our fine-grained location-based memory model to distinguish constant array indexes. (see link https://github.com/unsw-corg/SVF/blob/master/include/MemoryModel/LocMemModel.h)

Note that "-locMM" is not the default option as it may be very costly and unscalable for large-size programs.