[JSR308] Some general questions

[Federico Mancini]

Hi,
thanks a lot for the explanation!

Just a couple of more questions about the NullChecker to check whether
I understand.

1) In which file of the source code can i find the implementation of
the rules that enforce the two properties that you mentioned?
(Are they both part of the basic checker or do they use some extension?)

2) When you say that only NonNull variable can be dereferenced, what
happens in the checker when checking this piece of code?

		 Integer i =somefunction(); \\somefunction can return null
		if (i==null)
		    System.out.println("null");
		else
		    System.out.println(i.intValue());

 The system should infer that in general i is Nullable since it can
have a null value, but I still dereference it, so I should get a
warning, but I don' t..
Is it because even though i can be null, the system infers that it is
not when I dereference it (so it can be considered NonNull), or is
there another reason?

Thanks again for your help!

Regards

Federico


2009/1/9 Mahmood Ali <mahmood at mit.edu>:
> Greetings Federico,
>
> It's great to see your interest in static analysis.
>
>> 1) The Null checker provided with the jsr308 should guarantee (up to a a
>> certain limit that I would like to understand better) that there won't
>> be a NullPointerException in the program.
>> However a type checker (as I understood it) should guarantee only that
>> the null type system is enforced, i.e., no variable declared @NonNull
>> will ever be assigned a null value.
>
> The Nullness Checker enforces two properties/rules:
> 1. Null type system rules, i.e. any NonNull reference cannot reference null
> 2. Only NonNull references (either marked explicitly by user or inferred by
> the system) can be dereferenced.  The checker warns against dereferencing of
> a nullable reference.
>
> A type system does more than verifies subtype rule of an explicit
> assignments (e.g. a = b).  A type system also checks for invalid operations
> on types (e.g. "a" * 2, or "m".nonExistingMethod()).  Dereferencing a
> nullable value in the nullness type system is an error as the type isn't
> guaranteed to contain any member elements.
>
>> 2) I think there might be a bug in the checker.
>
> Can you please provide a sample code for this bug along with the expected
> behavior?  Please send it to the jsr308-bugs mailing list
> (jsr308-bugs at lists.csail.mit.edu).
>
>> 3) Is it possible to define a new type by the kind of values that are
>> valid for that type? For example the type @Date that defines all strings
>> that matches the regular expression "[1-31]/[1-12]/[2000-2010]".
>> If so, how to extend the basic checker for this type?
>
> Yes.  Please read sections 7 and 9 of the Checkers manual.
>
> Here is a summary of those sections related to the example you provided:
>
> Summary of section 7:
> When using the basic checker, you simply need to declare the annotations:
>  @TypeQualifier
>  @SubtypeOf(Unqualified.class)
>  public @interface Date { }
> And have the basic checker enforce the semantics of the basic type system
> (checks assignments and pseudo-assignments only).
>
> Such checker doesn't verify that a string literal in the code is indeed of a
> Date format.  This makes either need to cast such string literals to @Date
> String type (which is an unsafe cast), or have a format verifier method that
> ensures the string is a Date string at run-time.
>
> Summary of Section 9:
> Because of the limitation mentioned earlier, you can build a more powerful
> checker that implicitly add @Date qualifier to the types of string literals
> that match the specified format.
>
> With this more powerful checker, you may still need to have a method that
> verifies the string Date format for strings that are inputs from the user or
> from configuration files.
>
> Hope that helps.
>
> Regards,
> Mahmood
>
>