Re: [bddbddb-devel] Encoding Object-oriented relations in bddbddb

[John W. <joe...@gm...>]

Sure, one easy way to do this is to partition your "Memory" domain into
smaller parts, and add "IsHeapMem()" or "IsRegionMem()" predicates to
distinguish between them for the rules that need to.  You can partition the
domain by e.g. saying elements 1-10000 are heap and 10001-20000 are region.

Example:

PointsTo(v1,h) :- Assign(v1,v2), PointsTo(v2,h).

PointsToNonRegionMem(v) :- PointsTo(v,h), !IsRegionMem(h).
PointsToOnlyRegionMem(v) :- PointsTo(v,_), !PointsToNonRegionMem(v).

-John


On Dec 26, 2007 9:21 AM, Pengcheng Wu <wu...@cc...> wrote:

> Dear Dr. John Whaley,
>
> How are you?
>
> I am a PhD student with Northeastern University, Boston, trying to use
> your bddbddb tool to do some software analysis tasks. I have a question
> about the tool itself, and I would appreciate it very much if you can spend
> some time answering it.
>
> My question is specific to how to encode object-oriented relations in
> bddbddb. I understand that when using bddbddb, one needs to firstly define
> domains and the relations (with relation signatures) over the domains.
> However, all the examples that I have seen (in your papers) only use pure
> relational relations, and it is not clear to me whether the tool directly
> supports inheritance paradigm that is common in O-O modeling. Let me use one
> specific example to get my point. Assume I have the following OO meta-model
> (using the UML notation), on which I want to run some query using bddbddb:
>
>     +----------+                              +---------------+
>     | Pointer | ---------------------------> |  Memory  | <|----+
>     +-----------+              pointsTo   +--------------+        |
>
> |
>
> -------------------------------
>                                                             |
>                  |
>
> +---------------+           +-----------------+
>                                                      | HeapMem
> |            | RegionMem|
>                                                      +---------------+
>           +-----------------+
>
> As hopefully can be seen in the diagram, a pointer can point to a memory
> object, which can be either a HeapMem object or a RegionMem object at run
> time. It is unclear to me how to encode the pointsTo relation. For example,
> I may encode it as:
>
>     pointsTo(p:Pointer, m:Memory)
>
> but when I forms the ground rules (facts), I have to make a $p$ points to
> either a HeapMem object, or a RegionMem object, which is not in the domain
> of Memory.
>
> Am I supposed to flatten this relation, such that we have the following?
>
>    pointsToHeap(p:Pointer, hm:HeapMem)
>    pointsToRegion(p:Pointer,rm:RegionMem)
>
> But I can see many more rules will need to be made when the O-O meta-model
> gets bigger and more inheritances are used (or the inheritance chain gets
> deeper).
>
> Or better, does bddbddb support the notion that a domain can be built up
> from other domains using primitive set operations, e.g., the domain of
> Memory could be got by doing union on the two disjoint domains from HeapMem
> and RegionMem? This way, I would not need to flatten the diagram. Maybe the
> tool already supports this, but I didn't find an example. So if that is the
> case, please let me know where I can find such an example.
>
> Thanks a lot in advance!
>
> Happy holiday!
>
> --Pengcheng
>
>
>