Daikon and Object Relationships

[GP]

Hello,

I have been reading about Daikon and studying its behavior with invariants regarding data. One of these invariants is referential integrity, meaning that if one object references another, then that referenced object must exist. In other words, if an object that is not null references another, that one must also not be null.

To check what Daikon outputs in this kind of situation, I developed a simple case study in Java, considering a shop (which could be seen as a database) storing customers and their orders (for now, the shop only stores one customer and the corresponding order). These objects are defined as follows: Customer(id, name), Order(id, Customer) and ShopDB(Customer, Order).

I am using Daikon 5.8.0, with Java 11. When running Daikon with this example, I obtain the following invariants for the state of the database (full output, in file beforerefint.txt, and code, in ShopDB.zip, is attached):

===========================================================================

ShopDB:::OBJECT

this has only one value

this.order != null

this.order.orderID != 0

this.order.customer != null

this.order.customer.customerID != 0

this.customer != null

this.customer.customerID != 0

===========================================================================

Although Daikon is able to infer that this.customer != null, this.order !=null, and this.order.customer != null, a relationship between this.order and this.customer is not explicit. I would like this relationship to be present as an invariant for the state of the database.

To obtain a solution for my goal, I started developing a new invariant that would output the result I had in mind: this.order ==> this.customer (meaning if a order exists, then a customer for that order must also exist). Since this situation would fall in the binary invariant category, I need to extend the corresponding class, BinaryInvariant. And since to check if a variable of pointer type is different than null, a strategy similar to the present in NonZero (comparing to 0) must be used, I decided to extend TwoScalar, which already extends BinaryInvariant. 

Next, according to the Daikon Developer Manual, I created a new Java class named ReferentialIntegrity (attached), in daikon/inv/binary/twoScalar/, with the necessary constructor and static method, and implementing the abstract methods of Invariant that weren't already implemented in BinaryInvariant or TwoScalar. A list of the required methods and their implementing class is present in file abstractmethods.txt, which is attached.

I then proceeded to add this new invariant as an import in Daikon.java, and also adding it to proto_invs with "proto_invs.add(ReferentialIntegrity.get_proto());". After successfully recompiling Daikon with make -C $DAIKONDIR daikon.jar, I executed Daikon with the previous case study, but unfortunately the results were not as intended

(full output, in file afterrefint.txt:

===========================================================================

ShopDB:::OBJECT

this has only one value

this.order != null

this.order.orderID != 0

this.order.customer != null

this.order.customer.customerID != 0

this.customer != null

this.customer.customerID != 0

(RefInt) this.order.customer ==> this.customer

(RefInt) this.order.customer.customerID ==> this.customer.customerID

(RefInt) this.order.customer.name ==> this.customer.name

===========================================================================

The results are not terrible, since relationships between the customer (and its fields) of an order and that order are inferred. However, the desired invariant (this.order ==> this.customer) is missing. I'm not able to figure out why.

I would appreciate any feedback, correction or suggestions to my approach or code, in order to reach a solution.

I hope I was clear enough presenting my problem. 

Best regards. 

[GP]

I would like to add what I did to try to understand what's wrong.

I used the Daikon debugger, by running java -cp $DAIKONDIR/daikon.jar daikon.Daikon --track ReferentialIntegrity@ShopDB:::OBJECT RefInt.dtrace.gz, to verify what variables were being checked in ShopDB:::OBJECT program point.

The obtained results are attached in file daikondebug.txt. It is possible to see that this.order and this.customer are never compared.

I then tried using only Chicory and Daikon, without executing DynComp, in order to obtain a less smart variable comparability, which could result in those two variables being compared. This approach also didn't provide the intended results.

I still haven't figured out how to obtain the invariant this.order ==> this.costumer.

Best regards.

[Michael Ernst]

I don't understand what invariant you want to infer.  Could you help me out by explaining it?

As written,
  this.order ==> this.customer
doesn't type-check, because this.order is not a boolean and this.customer is not a boolean.

Do you mean
  this.order != null ==> this.customer != null
or maybe
  this.order != null ==> this.order.customer != null
?

Those properties are both weaker than
  this.customer != null
  this.order.customer != null
Which do appear in Daikon's output.

Daikon has a way to infer implications:  http://plse.cs.washington.edu/daikon/download/doc/daikon.html#Conditional-invariants .
Did you try that and it didn't serve your needs?

-Mike

--
You received this message because you are subscribed to the Google Groups "Daikon discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-discus...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/e122c65f-8b2f-4020-9d5b-ba2622d82eaa%40googlegroups.com.

[GP]

Thank you for replying.

I have since been able to infer the intended invariant.

I figured after some time the problem was with type-checking (should have figured sooner).

And yes, the invariant written as this.order ==> this.costumer is wrong. It was supposed to be a shorter way of expressing

this.order != null ==> this.customer != null, which was what I intended to see.

This invariant is not supposed to replace both

this.customer != null
this.order.customer != null,

it would just be a way to represent in a more direct manner the relationship between both objects.