Mutual @NonNull references

Get help installing and running JSure here.
AaronGreenhouse
Posts: 9
Joined: 15 Sep 2015 13:46

Mutual @NonNull references

Postby AaronGreenhouse » 30 Sep 2015 15:33

Another tricky issue with @NonNull fields is if you need two objects to have mutual @NonNull references to each other. Consider the following attempt where we want it to the case that each A object be associated with a specific B object, and that the B object contain a back-link to the A object:

Code: Select all

@TrackPartiallyInitialized
class A {
   @NonNull
   private final B bRef;
   
   public A() {
      bRef = new B(this);
   }
}

@TrackPartiallyInitialized
class B {
   @NonNull
   private final A aRef;
   
   B(final @NonNull A aRef) {
      this.aRef = aRef;
   }
}


Each class, A and B, declares a @NonNull field to refer to the other. A() creates a new B intance, passing it a reference to the new A object. Sadly, JSure refuses to assure this scenario:

Screen Shot 2015-09-30 at 3.19.26 PM.png
Screen Shot 2015-09-30 at 3.19.26 PM.png (73.4 KiB) Viewed 1518 times


The problem is that within A() the reference 'this' is not considered a non-null reference. It is a partially initialized reference, and thus we cannot pass it to the @NonNull formal argument of constructor B(). We could attempt to fix this by changing the annotation on B() to be @Initialized(through="Object"). But this is unsatisfactory:
  • It doesn't actually capture the intent: B() is meant to hold on to a real @NonNull reference to an A object.
  • It just moves the problem into B(): the partially initialized argument cannot be assigned to a @NonNull field.
  • A field cannot be declared to be @Initalized, so we cannot continue to 'fix' the problem by replacing @NonNull with @Initialized.

The solution is to cast the reference to be @NonNull within A(). The analysis used to assure @NonNull uses the method Cast.toNonNull() to force a reference to be considered to be non-null. This is not a safe operation, and it's use is recorded specially in the verification results. Below we use a version of Cast.toNonNull() that takes a dummy String parameter that serves as a description of why the cast is necessary/safe:

Code: Select all

@TrackPartiallyInitialized
class A {
   @NonNull
   private final B bRef;
   
   public A() {
      bRef = new B(Cast.toNonNull(this, "B() only needs the reference and never dereferences it"));
   }
}

@TrackPartiallyInitialized
class B {
   @NonNull
   private final A aRef;
   
   B(final @NonNull A aRef) {
      this.aRef = aRef;
   }
}


The two classes now assure in the manner we expect. Now we see that the chain of evidence for the actual parameter to the call B() includes the fact that the cast is the reason the reference is considered to be non-null. Because the cast is not safe, it is marked with a red dot, and every result that depends on the cast is poisoned with the red dot as well. Also note that the call to Cast.toNonNull() is recorded separately under the "Vouches" heading.
Attachments
Screen Shot 2015-09-30 at 3.29.44 PM.png
Screen Shot 2015-09-30 at 3.29.44 PM.png (71.24 KiB) Viewed 1518 times

Return to “JSure”

Who is online

Users browsing this forum: No registered users and 1 guest