[cfe-dev] Where are the methods, which handle the Element Region’s index, in Clang Static Analyzer?

[Jordan Rose]

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:

1. 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.
2. Create a new value of '$ptr + 3', which happens in SValBuilder. The result is also represented as an ElementRegion, i.e. '&$ptr[3]'.
3. Update the Store: bind '$ptr + 3' to the VarRegion for 'ptr'.

Does that clear things up?
Jordan


On Nov 5, 2013, at 6:09 , Arthur Yoo <phjy007 at gmail.com> wrote:

> Hi Jordan,
> 
> 
> 
> What does it mean by “when you do ‘ptr = ptr + 3’, you're storing a new value into the same location”? In other words, what do ‘a new value’ and ‘the same location’ mean respectively? Does it mean that the pointee region referred by ptr is ‘element{arr,3 S32b,int}’ rather than ptr’s region itself? And what’s the kind of MemRegion does ‘ptr’ is? Just ‘VarRegion’? Is it right that Static Analyzer doesn’t know that ‘ptr’ is a pointer?
> 
> 
> 
> Actually, I want to track the pointer offsets for two platforms. How does Static Analyzer know that before “ptr = ptr + 3”, ‘ptr’ pointed to ‘element{arr,0 S32b,int}’ and after that, ‘ptr’ points to ‘element{arr,3 S32b,int}’? Thanks a lot.
> 
> 
> 
> 2013/11/5 Jordan Rose <jordan_rose at apple.com>
> 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
> 
> 
> On Nov 4, 2013, at 4:33 , Arthur Yoo <phjy007 at gmail.com> wrote:
> 
>> It seems that evalBinOp() will do the related things. evalBinOp() also calls evalBinOpLN() and evalBinOpNN().
>> 
>> 
>> 2013/10/30 Arthur Yoo <phjy007 at gmail.com>
>> 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.
>> 
>> 
>> -- 
>> Best regards,
>> Arthur Yoo
>> 
>> 
>> 
>> -- 
>> Best regards,
>> 岳佳圆 | Yue Jiayuan | Arthur Yoo
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
> 
> 
> 
> 
> -- 
> Best regards,
> 岳佳圆 | Yue Jiayuan | Arthur Yoo

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20131105/bf15d18c/attachment.html>