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

[Zhongxing Xu]

On Thu, Dec 11, 2008 at 1:54 PM, Ted Kremenek <kremenek at apple.com> wrote:

>
> On Dec 10, 2008, at 8:06 PM, Zhongxing Xu wrote:
>
>  Thanks for your comments. They were helpful. Now the interfaces get
>> simplified a lot. Variables and functions are commented well.
>>
>> Here I explain the main idea.
>>
>> Some struct base is not mutable, e.g., struct s a; a.f = 3; Here the
>> struct base 'a' is not mutable. But some can, e.g.,
>>
>> void foo(struct s* p) {
>>  p->f = 3
>> }
>>
>> When we getInitialStore(), p is initialized to have value loc::SymbolVal,
>> which I call a symbolic pointer. (Note: here no symbolic region is
>> involved).
>>
>> In this patch we try to concretize the struct pointer p. We have several
>> preconditions for this concretization:
>>  - the struct base is a pointer
>>  - the pointer is symbolic
>>  - the pointer is an lvalue, so that it can be modified.
>>
>> When concretizing the struct base pointer, we pass the pointer's location
>> to StoreManager. Therefore the pointer should be an lvalue and has a
>> location. We get this location by calling
>> GRExprEngine::getBasePtrLoc(). This method only handles a few cases. In
>> other cases, BasePtrLoc is left Undefined intentionally.
>>
>
> Hi Zhongxing,
>
> The patch is looking great, but I still have some concerns about the
> overall approach.  Consider your example with one modification:
>
> void foo(struct s* p) {
>  struct s* q = p;
>  p->f = 3
> }
>
> After evaluating 'p->f' p will bind to an AnonPointeeRegion, but 'q' will
> bind to the original symbol.  They are aliases.  It gets arbitrarily worse
> if the value of 'p' is stored in other places, passed to functions, etc.
>
> This overall approach feels a little "destructive."  We're losing
> information here.  After evaluating 'p->f' we've lost the fact that 'p'
> *still* binds to the value at the entry to the function.
>
> I see this as being fundamental problematic for four reasons:
>
> (1) Different analyses may attach information (perhaps using the GDM) to a
> symbolic value.  Actually replacing a symbolic value with something
> "concrete" loses that information.
>
> (2) Consider function summaries.  We don't have them yet, but  basically we
> would build up a set of constraints and effects in terms of the input to the
> function.  That input is the symbolic values.  Even if we "concretize" them
> we need to keep them around.
>
> (3) Aliasing (i.e., the example I gave).  Concretization via replacing
> loses this critical information.
>
> (4) The BugReporter "module" needs to reconstruct information from the
> ExplodedGraph, including when aliasing relationships come into effect, etc.
>  Blowing away the original value of 'p' makes this difficult at best.
>
> The only way to replace a symbolic value with a concrete value is to
> alpha-rename it throughout the entire state.  This isn't trivial, especially
> when one considers the GDM.
>
> I honestly think we need to take a "layered" approach.  Keep a map on the
> side from "symbols" to concrete values.  That's basically what we do in
> ConstraintManager when it comes to equality relationships with integers.
>  Equality relationships with integers is a form of concretizations; that's
> all were basically doing here, except we're reasoning about the
> concretization of the heap.
>
> What do you think?  I have specific comments about your patch (which is
> looking great!) but I will defer them until we iterate more on this design
> point.
>
> Ted
>

Thanks for bringing up these issues. I agree that we should keep the
original symbolic value around, and do the conretization with a side
mapping. I'll try to implement the idea and see what problems would come up.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20081211/357d3d23/attachment.html>