Re: [bddbddb-devel] Encoding FORALL quantificator (the universal quantificator) Re: Encoding Object-oriented relations in bddbddb

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

Hi,

You can accomplish FORALL in Datalog by using a double negation.  For
example, if you have predicates "student(s)" for the list of students and
"took(s,c)" if student s took class c, and "required(c)" for the list of
required classes, then you could write:

cantGraduate(s) :- student(s), required(c), !took(s,c).
canGraduate(s) :- student(s), !cantGraduate(s).

Basically you just use the fact that FORALL(P) is the same as NOT EXISTS(NOT
P).

-John


On Dec 30, 2007 8:22 AM, Pengcheng Wu <wu...@cc...> wrote:

> 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 <joe...@gm...> 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 <wu...@cc... > 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 <joe...@gm...> 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 < wu...@cc...> 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 < joe...@gm...> 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 <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
> > > > > > >
> > > > > > >
> > > > > > >
> > > > > >
> > > > >
> > > >
> > >
> >
>