On generation of invariants of the form "var >= 0" by Daikon

[Priyanka Darke]

Hello,

I have recently started using daikon to generate program invariants. I wanted

to check on the generation of invariants of the form "var >= 0" by daikon. In

the attached examples, invariant "k>=0.0" is generated from the e.dtrace file,

while the invariant "n>=0" or "i>=0" are not generated from h.dtrace.  Could

someone please explain why, or refer to an explanation if one already

exists? I have used the following commands and infrastructure.

1.  Dowloaded the Daikon distribution, version - 5.8.2 from https://plse.cs.washington.edu/daikon/download/.

2.  Executed convertcsv.pl on the attached csv files. This generated the respective decls and dtrace files. The commands are as follows:

[d]$ perl convertcsv.pl h.csv

[d]$ perl convertcsv.pl e.csv

3.  Then I fired the Daikon invariant generation commands as follows:

[d]$ java -cp ~/XXX/daikon.jar daikon.Daikon e.dtrace e.decls

Daikon version 5.8.2, released May 4, 2020; http://plse.cs.washington.edu/daikon.

(read 1 decls file)

Processing trace data; reading 1 dtrace file:

[5:31:50 PM]: Finished reading /XXX/e.dtrace

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

aprogram.point:::POINT

i >= 0.0

k >= 0.0

k1 >= 1.0

j >= 1.0

i >= k

i != k1

k - k1 + 1 == 0

k < j

k1 <= j

Exiting Daikon.

[d]$ java -cp ~/XXX/daikon.jar daikon.Daikon h.dtrace h.decls

Daikon version 5.8.2, released May 4, 2020; http://plse.cs.washington.edu/daikon.

(read 1 decls file)

Processing trace data; reading 1 dtrace file:

[5:32:17 PM]: Finished reading /XXX/h.dtrace

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

aprogram.point:::POINT

i >= n

Exiting Daikon.

4. java : openjdk version "1.8.0_141", OpenJDK Runtime Environment (build 1.8.0_141-b16), OpenJDK 64-Bit Server VM (build 25.141-b16, mixed mode) 

5.  OS: Fedora core, version - 24 (Server Edition)

Am I missing something here? Any inputs or explanation will be appreciated. Thanks.

With best regards,

Priyanka.

[Michael Ernst]

Thanks for your message.  I'm sorry you are having trouble.

The Daikon output that you showed contains:

...
k >= 0.0
...
i >= k
...


Together, these properties imply i >= 0.0.  To keep its output less verbose, Daikon does not output redundant invariants that are implied by invariants that it prints.  This is disussed in the "Redundant invariants" section of the manual:  http://plse.cs.washington.edu/daikon/download/doc/daikon.html#Redundant-invariants .

Following the instructions in that section, you can enable output of redundant invariants by passing
  --config_option daikon.inv.filter.ObviousFilter.enabled=false
on the command line.

When I run
java -cp .../daikon.jar daikon.Daikon --config_option daikon.inv.filter.ObviousFilter.enabled=false e.dtrace e.decls
the output is:

===========================================================================
aprogram.point:::POINT
i == i
k == k
k1 == k1
j == j
i >= 0

i >= 0.0
k >= 0
k >= 0.0

k1 >= 0
k1 >= 1.0
j <= 393216.0
j >= 0
j >= 1.0
i - i == 0

i >= k
i != k1

k - k == 0

k - k1 + 1 == 0

k < k1
k < j
k1 - k1 == 0
k1 <= j
j - j == 0
Exiting Daikon.

I hope this helps.

-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/fdc0282d-67db-42d4-af98-6093908e2ff4%40googlegroups.com.

[Priyanka Darke]

Hello,

Thank you for the reply. If we consider the attached h.dtrace file, we get a single invariant "i >= n", as follows (mentioned in the earlier email) :

[xx]$ java -cp ~/yy/daikon.jar daikon.Daikon h.dtrace h.decls

Daikon version 5.8.2, released May 4, 2020; http://plse.cs.washington.edu/daikon.

(read 1 decls file)                                                            .

Processing trace data; reading 1 dtrace file:

[3:59:17 PM]: Finished reading h.dtrace

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

aprogram.point:::POINT

i >= n

Exiting Daikon.

Are you seeing a similar behavior? Why don't we see the invariants "i >= 0" and "n >= 0" here?

Thank you in advance.

With best regards,

Priyanka.

To unsubscribe from this group and stop receiving emails from it, send an email to daikon-...@googlegroups.com.

[Michael Ernst]

Please read section "Missing output invariants" in the "Troubleshooting" chapter of the manual.
If you are still having trouble, please ask -- but be sure to say what you have tried so far.

I ran Daikon with the "--disc_reason all" command-line argument (--disc_reason is suggested at the beginning of the "Missing output invariants" section).  Part of the output is

i >= 0.0
Unjustified confidence
Had confidence: 0.5
...
n >= 0.0
Unjustified confidence
Had confidence: 0.5

There were few distinct samples, so the invariant is not statistically justified, so Daikon does not print it.

Mike

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/7b66fae8-7fa7-4c7e-95c4-9ad7945d42e7o%40googlegroups.com.