Nullness Type System for key.core

[wadoon]

More nullness type system checks. Now for key.core.

I want first to merge #3399 into KeY to avoid double work.

[wadoon]

I have pushed further and activated Nullness checks for more packages but have not finished everything. Annoying are the situations where the InitilizationChecker hits:

class A {
  public A() { ... 
    setFoo(2);
  }
  void setFoo(int i){...}
}

The complain is that setFoo is called with @Unintialized A this but expects @Initialized A this.

@wmdietl @flo2702
Is there any trick to get pass this message? For example, an

assert this instanceof @Initialized A;

would be fine.

Inside KeY, we have many of these moments. It is also not a bad code design and is hard to avoid. Also adding the right annotation leads to ugly code:

class A {
  public A() { ...; setFoo(2);  }
  void setFoo(@Uninitialized A this, int i){...}
}

and this needs to be added to all transitive called methods.

[wmdietl]

The warning from the Initialization Checker is correct.
Class A isn't final, so there could be the following code:

class A {
  public A() { ... 
    setFoo(2);
  }
  void setFoo(int i){...}
}

class B extends A {
  Object o; // non-null by default

  @Override
  void setFoo(int i) {
    foo = i + o.hashCode(); 
  }
}

This code would lead to an NPE, as setFoo is called before B.o has been initialized.
B.setFoo is correctly implemented, as the receiver of setFoo promises a fully initialized receiver.

The right thing to do is to document this by setting the receiver type of setFoo.
The wrong thing to do is to suppress the warning on the call in the constructor of A (and at least add a comment to setFoo that it will be invoked on an under-initialization receiver).

Addition: you could use UnknownInitialization(A.class) A this as the receiver type of setFoo to express that the receiver is initialized up to and including class A.

[wadoon]

@wmdietl I saw that this error is correct. However, I want to avoid the clutter of receiver types in the source code.

[wmdietl]

@wadoon If this only happens in a few constructors, simply suppress the warning there.
If you never care about warnings from the Initialization Checker, pass -AassumeInitialized to turn it off.
You might be able to get something in-between by passing -AsuppressWarnings= with the error key from the call... https://eisop.github.io/cf/manual/manual.html#suppresswarnings-command-line

Do you see any other option that we could add to the framework?

[wadoon]

For the first, I stick to -AassumeInitialized.

This pattern of calling own methods in constructor is rather common in UI code, e.g., AbstractAction in Swing.

Do you see any other option that we could add to the framework?

I am thinking about, why is this so easy in Kotlin, and in Java so complicated.

My first thought was that a simpler annotation would be fine. At least lower the clutter.

typealias @ActionInit = `@UnknownInitialization(javax.swing.AbstractAction.class) KeYAction this`;
public class KeyAction { @ActionInit public KeyAction setName(...) {...} }

My second thought was, why am I not able to stop the "under-initialization phase" by calling this(..); or getting an UnknownInitialization(A.class) A this by calling super();

Here is the excerpt on how we typically build our Swing Actions:

abstract class javax.swing.AbstractAction  implements ActionListener {
   private Map<> attrib = new HashMap<>();
   public void putValue(Object key, Object value);
}

class KeyAction extends AbstractAction {   
    void setName(String name) { putValue(NAME, name);} 
}

class AboutDialogAction extends KeyAction {
    public AboutDialog() { 
        super(); // normally implicit
        setName("About..."); // <--- should be possible KeyAction is constructed.
    }
}

Of course, there might be loopholes (super() calls an overridden method) for certain scenarios this should be valid, especially when a class is "encapsulated under inheritance" iff. I could use the parent class also via delegation.

[as2-0]

In the package key.core/src/main/java/de/uka/ilkd/key/macros/ there are methods with ~20 implm. Some of the paramters are sometimes only used in a few or maybe even none of the implementations (I didn't had the time to check).
Maybe its better to refactor them.

[wadoon]

KaKeY:

• First: Make the PR fit again.
• Second: Make the annotation runtime checkable.

[mattulbrich]

Agreed during meeting:

• new checkerframework version to avoid errors
• merge main into this
• find a RAC framework for @NonNull (I wrote one a while ago, ...)
• then merge this into main (medium term) even if not verifiable to allow for compatibility.