Hi all,
ElementRegion has a field named Index (NoLoc) to record the index of that Array Element. We can also use pointer offset operation to calculate a new index and get the corresponding array element. For example:
1 void func() {
2 int arr[10];
3 int *ptr, *ptr2;
4 ptr = arr;
5 ptr = ptr + 3;
6 *ptr = 9;
7 ptr2 = ptr + 1;
8 *ptr2 = 10;
9 }
Line 5 shows the pointer offset operation. I dumped the information of the pointee MemRegion referenced by ptr, the Static Analyzer gave me such result: element{arr,3 S32b,int}. That means after the pointer offset operation by line 5, the ptr’s pointee MemRegion became an ElementRegion of arr[], which index was 3 S32b. The line 7’s effect is same, it showed me element{arr,4 S32b,int}. Obviously, after the pointer offset operation, the ElementRegion’s Index will be changed. I want to know where are the methods that handle the Element Region’s index in pointer offset operation. Cause I want to find these methods and add some codes into them.
Thanks a lot.
It seems that evalBinOp() will do the related things. evalBinOp() also calls evalBinOpLN() and evalBinOpNN().
That’s correct. Also, remember that symbolic values are immutable; when you do “ptr = ptr + 3”, you’re storing a new value into the same location. So the ElementRegion’s index doesn’t change, but ‘ptr’ now refers to a different ElementRegion.
Jordan
I recommend reading up on the Checker Developer Manual on the analyzer site, but here’s the gist of it:
- Values are immutable things. Regions represent regions of memory. The address of a region can be a value.
- Any local variable or parameter is a VarRegion. VarRegions are TypedRegions, so the analyzer does know that ‘ptr’ is a pointer, but the value might be some integer casted to a pointer, which can’t actually behave as a region.
- The Store is what keeps tracking of what value is bound to a particular region.
So, when you do “ptr = ptr + 3”, the analyzer will do this:
- Get the value currently stored in the VarRegion for ‘ptr’. Call it ‘$ptr’, though if the value is symbolic it may be represented as an ElementRegion ‘&$ptr[0]’. This is because we don’t know if ‘*ptr’ is a single object or part of an array.
- Create a new value of ‘$ptr + 3’, which happens in SValBuilder. The result is also represented as an ElementRegion, i.e. ‘&$ptr[3]’.
- Update the Store: bind ‘$ptr + 3’ to the VarRegion for ‘ptr’.
Does that clear things up?
Jordan