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

Hi Dr. Whaley,

Thanks for your time answering my questions. I really appreciate them.

I am having another question about how to encode the FORALL quantificator (the universal quantificator) in bddbddb, and am wondering if you can give me some help. I realize that it is more of a Datalog question, instead of a direct question about the bddbddb tool. But I will appreciate your thoughts/suggestions.

I want to implement a CHA (Class Hierarchy Analysis) algorithm in bddbddb, where I need to encode the FORALL quantificator, because to determine if a method in a subclass (Sub) overrides another method in a superclass (Sup), I need to specify the constraint that the method name has to match, and FORALL of the arguments, the static types have to match. The first of my attempt is to encode the method arguments signature to be something like:

   methodsignature(meth, argPosition, argName, argType)

But soon I realized that I could not write down the overriding determination algorithm this way, because as far as I know, there is no FORALL quantificator in Datalog (I could be wrong about this), which I believe is necessary for expressing this constraint.

Then I looked into your PLDI'04 paper, where you also needed to use the CHA algorithm. However, I found in your paper, the CHA relation was not actually computed from the bddbddb slover. Instead, it was given as an 'a priori' fact, possibly pre-computed by some Java program (this is just my guess). So was that a deliberate decision due to the lack of FORALL quantificator in Datalog, or was that just due to a performance consideration (probably computing that in Java was faster)?  If it is the latter, could it have been computed in bddbddb rules directly?

Thanks again,

--Pengcheng

On Dec 26, 2007 4:20 PM, John Whaley <joewhaley <at> gmail.com> wrote:

Hi,

You can find an example in testMap.datalog in bddbddb_examples, here:
http://bddbddb.svn.sourceforge.net/viewvc/bddbddb/trunk/bddbddb_examples/testMap.datalog?revision=304&view=markup

-John

On Dec 26, 2007 12:43 PM, Pengcheng Wu <wupc <at> ccs.neu.edu > wrote:

I was not aware of the "=>" operator. Can you please elaborate it? Or if there is a link to a relevant doc/paper, please let me know.

Thanks for the info!
--Pengcheng

On Dec 26, 2007 3:15 PM, John Whaley <joewhaley <at> gmail.com> wrote:

Yes, the easiest way to accomplish that is to always use "IsRegionMem()" when using "size()".  Basically instead of using a predicate "P(...,m:RegionMem,...)", use two predicates "P(...,m:Memory,...)" and "IsRegionMem(m:Memory)".

The other way to do it would be to separate the domains and use the "=>" operator to move between domains.

-John

On Dec 26, 2007 11:29 AM, Pengcheng Wu < wupc <at> ccs.neu.edu> wrote:

Sure we can do that. But I can see an issue of losing type precision when we cannot introduce separate domains for "HeapMem" and "RegionMem" respectively. Imagine there is a relation 'size' that only makes sense for "RegionMem' but not for "HeapMem", i.e., the following meta-model:

    +----------+                              +---------------+

    | Pointer | ---------------------------> |  Memory  | <|----+
    +-----------+              pointsTo   +--------------+        |
                                                                          |
                                                            -------------------------------
                                                            |                              |
                                                     +---------------+           +-----------------+          +----------+
                                                     | HeapMem |            | RegionMem| --------> | Size   |
                                                     +---------------+           +-----------------+           +---------+

We would have to define the size relation to be:

  size(m:Memory, s:Size)

And use this relation always conjunction with predicate IsRegionMem. I guess a relation like size(rm:RegionMem, s:Size) would have made this conjunction unnecessary and would have allowed us to exclude some ill-formed facts earlier by type-checking.

Do you agree?

Thanks,
--Pengcheng

On Dec 26, 2007 1:08 PM, John Whaley < joewhaley <at> gmail.com> wrote:

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 <wupc <at> ccs.neu.edu > 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