Inferring null/not null invariants

[GP]

Hello,

How does Daikon infer null/not null invariants for Java programs? I see in the StackAr example one of the inferred invariants is this.theArray != null.

However, I don't see any Null.java or NonNull.java in the source code.

The closest I've found is the file AnnotateNullable.java, which creates a file with the variables that "have seen null values by looking at the NonZero invariant". Is this related to the inference step? Since this class uses an already existing Daikon invariant file, I don't think it is used to infer any invariants. 

Thank you.

[Michael Ernst]

Daikon infers properties (including ones about null/not null) by running the program, not by examining the program's source code.  This is explained in the first paragraph of the Daikon manual:  http://plse.cs.washington.edu/daikon/download/doc/daikon.html#Introduction .

Daikon outputs properties as text and/or in a binary file format.
This is explained at the beginning of section 3, and elsewhere:  http://plse.cs.washington.edu/daikon/download/doc/daikon.html#Example-usage
Your message mentions the textual output "this.theArray != null" that you saw.

AnnotateNullable is a tool that enables you to insert the output of Daikon in a program's source code, as @Nullable annotations.  This is essentially just a different way to format part of Daikon's output.  AnnotateNullable has its own section in the manual:
http://plse.cs.washington.edu/daikon/download/doc/daikon.html#AnnotateNullable .  AnnotateNullable doesn't do all the work, but is part of a 4-step process to insert @Nullable annotations in source code.

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/611e79a3-fd5b-4bbd-8f98-7fae6ea45424%40googlegroups.com.

[GP]

Hello,

I understand how Daikon infers invariants. What I'm not able to detect are the files in the source code dealing specifically with those invariants (null/not null). 

For example, there's a file Positive.java in java/daikon/inv/unary/scalar/, to check if a variable value is always greater than 0. I was expecting there to be a file, possibly called Null.java or NonNull.java, checking if a variable is always null or not.

I also don't see this type of invariants being added to proto_invs in the Daikon.setup_proto_invs method.

My goal is to extend Daikon with new invariants that work with null values. Without understanding how Daikon is able to output invariants such as "this.theArray != null", I am not able to proceed, since that's the basis I will work on.

Thank you for helping.

[Michael Ernst]

Thanks for the explanation of your question and what you tried; that is very helpful!

You were looking in nearly the right place.  The relevant invariant is NonZero:
http://plse.cs.washington.edu/daikon/download/api/daikon/inv/unary/scalar/NonZero.html

AnnotateNullable looks for the *absence* of a NonZero invariant; if the invariant is absent, then the value must have been 0 (= null) at least once, and the tool outputs @Nullable.
This is explained in the Javadoc comment for AnnotateNullable (https://github.com/codespecs/daikon/blob/master/java/daikon/AnnotateNullable.java#L23), which says:  "It determines which variables have seen null values by looking at the NonZero invariant."

A less direct way to find the NonZero invariant would have been these sections in the developer manual, which contain text that discusses "null" and "zero" together:

http://plse.cs.washington.edu/daikon/download/doc/developer.html#Program-point-declarations
http://plse.cs.washington.edu/daikon/download/doc/developer.html#V1-pptname-format

That's a bit more obscure than the AnnotateNullable documentation, though.

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/5d03d118-a1ec-4ad3-894b-c1f18115c0ae%40googlegroups.com.