[cfe-dev] [PATCH] expand a symbolic pointer

[Zhongxing Xu]

New patch.
 - A new method CheckStructBase is taking care of the creation of
AnonPointeeRegion.
 - A lightweight lvalue evaluation method is used to get the location of the
base expr
   whose store may be changed.
 - AnonPointeeRegion is now identified the the memregion of the pointer
pointing to it.


On Wed, Dec 10, 2008 at 9:12 AM, Ted Kremenek <kremenek at apple.com> wrote:

> Hi Zhongxing,
>
> I like the main ideas about the patch, but I'm a little concerned about
> placing this logic in StoreManager::getLValueField.
>
> Do you feel that StoreManager::getLValueField should do the work for both
> 'x.f' and 'x->f'.  That is, the latter can be rewritten as:  (*x).f.  It
> seems to me that the (*x) portion is what should lazily create the
> AnonPointeeRegion, and at that point do the null check.  Then,
> getLValueField just reasons (and only reasons) about "SOMETHING.f", where
> SOMETHING is an SVal.
>
> The nice thing about decoupling things in this way is that:
>
> 1) StoreManager::getLValueField and GRStateManager::getLValueField stay
> simple; they only need to reason about dot-accesses.
>
> 2) GRExprEngine can do the heavy lifting of reasoning about the syntax.  As
> I said, x->f is the same as (*x).f.  There is no reason that StoreManager or
> GRStateManager should be reasoning about syntax in this way.  Let's keep the
> complexity of reasoning about syntax in one place (i.e, GRExprEngine), and
> have the other components just reason about pure semantic operations (if
> possible).
>
> 3) Having GRExprEngine handle the syntax allows different StoreManagers to
> automatically "get it right" with regards to both (*x).f and x->f if they
> decide to reason about fields.  If we need an interface to conjure up new
> regions (AnonPointeeRegion), then we should add it to StoreManager.
>
> I also found the following FIXME interesting:
>
> +      // FIXME: Should also update the value of the base expr. It's no
> longer a
> +      // symbolic pointer.
>
> In what ways is it no longer symbolic?  What does it mean for a region to
> be symbolic?  A symbol is just an abstract name.  If we rename the region,
> what would its new name be?
>

This fixme is no longer relevant. GRStateManager::CheckStructBase takes care
of updating the base expr value.

By 'symbolic pointer' I simply means loc::SymbolVal. If we create an
AnonPointeeRegion, we should replace it with the loc::MemRegionVal of the
AnonPointeeRegion.

I think SymbolicRegion is not involved in this problem. All regions we deal
with here are concrete. Only their bindings may be loc::SymbolVal.


>
> We should probably put some more effort into defining the concept of a
> symbolic region.  Also, if we were to alpha-rename a region, we would need
> to do it throughout the entire state (environment, store, and gdm).
>  Renaming/replacing regions in a GRState once we start using them is
> something that will be challenging to do, and we should think about whether
> or not it is necessary.
>
>
> On Dec 9, 2008, at 5:14 AM, Zhongxing Xu wrote:
>
>  Conditionally expand a symbolic pointer into a pointer to a real struct.
>> In the following code,
>>
>> struct x {
>>        int partno;
>> };
>> int foo(struct x *pt)
>> {
>>        int found;
>>        if(pt->partno != 1) {
>>                found = 0;
>>        }
>>        if(pt->partno == 1 || !found) {
>>                return 1;
>>        }
>>        return 0;
>> }
>>
>> when we visit pt->partno, an AnonPointeeRegion is created lazily for pt.
>> Moreover, only when pt is feasible not null, the region is created. This
>> fixes PR2304.
>> <expand.patch>_______________________________________________
>> cfe-dev mailing list
>> cfe-dev at cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/cfe-dev
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20081210/d5dca026/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: expand2.patch
Type: application/octet-stream
Size: 9389 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20081210/d5dca026/attachment.obj>