Java: Improve NullGuards.clearlyNotNullExpr()

[Marcono1234]

Improve NullGuards.clearlyNotNullExpr() by considering more cases where an expression cannot be null.

[aschackmull]

null is a compile-time constant expression.

[aschackmull]

Also, are there any compile-time constant operations that aren't already included directly in this predicate? If so, should they? (and leading to making this disjunct superfluous?)

[Marcono1234]

null is a compile-time constant expression.

At least according to the language specification, it is not. See JLS 16 §15.29:

Literals of primitive type (§3.10.1, §3.10.2, §3.10.3, §3.10.4), string literals (§3.10.5), and text blocks (§3.10.6)

All of the other definitions rely on this point, so a NullLiteral cannot be a compile time constant.

Though you are right, with the check for primitive type below, the check for a CompileTimeConstantExpr here would probably be redundant.

[aschackmull]

At least according to the language specification, it is not. See JLS 16 §15.29:

Ah, right, I missed that (and the fact that CompileTimeConstantExpr indeed doesn't include null). But I'd expect all (or most of) the operations that make up compile-time constants to be included here, thus making it redundant.

[joefarebrother]

I believe this could be a forex statement:

Suggested change

	var.getAnAssignedValue() = clearlyNotNullExpr(reason) and
	forall(Expr assignedValue | assignedValue = var.getAnAssignedValue() |
	assignedValue = clearlyNotNullExpr()
	)
	forex(Expr assignedValue | assignedValue = var.getAnAssignedValue() |
	assignedValue = clearlyNotNullExpr()
	)

[aschackmull]

I think this entire disjunct rewrite looks a bit curious. Why the change from Field to Variable? We ought to be able to handle all non-fields more precisely through SSA. What's the idea behind this change?

[Marcono1234]

I believe this could be a forex statement:

I used forall here to report the reason; with your proposal reason would not be bound. Note that for SwitchExpr I tried binding the reason in the forall but that did not work, therefore I wrote it as separate formula here as well.

---

I think this entire disjunct rewrite looks a bit curious

Do you mean usage of getAnAssignedValue()? The reason is that getInitializer() is too restrictive and does not cover a lot of cases, e.g. consider:

class Test
  final String s;

  public Test(boolean b) {
    if (b) {
      s = "a";
    } else {
      s = "b";
    }
  }
}

Here s cannot be null because all assigned values are non-null, even though they do not appear as part of the initializer. But that does not matter since you cannot access an uninitialized final variable, see JLS 16 §16.

Actually when a LocalVariableDecl is used, the final requirement could be dropped, but this would require special handling for variables being assined a value implicitly, for example the variable of an enhanced for loop (for (String s : strings)).

---

We ought to be able to handle all non-fields more precisely through SSA.

I think here it does not matter due to not being able to access an unassigned final variable, see above. However, at least at the current state reducing this back to Field fails finding n3 of the included test.
I am not familiar enough with SSA, so if you think it should be solved using that, feel free to improve the pull request in that regard.

[aschackmull]

Do you mean usage of getAnAssignedValue()

Yes. It would be cleaner to add a case for phi-nodes. But this predicate isn't intended to cover everything that we think isn't null - it's intended to cover everything that clearly isn't null.
Are these changes motivated by concrete query FPs in real code?

[Marcono1234]

But this predicate isn't intended to cover everything that we think isn't null - it's intended to cover everything that clearly isn't null.

When all getAnAssignedValue() expressions are clearly not null, then any read access of the variable has a clearly non-null result, see JLS 16 §16 linked above.
Checking only getInitializer() misses a lot cases where a variable or field is not directly assigned a value in the initializer, see Java source code example above.

(Note that this ignores reflection here since the previous code did not consider it either.)

[aschackmull]

These cannot be null simply due to their type, so possibly out of scope for this predicate. But I could imagine places where this disjunct might contribute. Please explain where you think that's the case and consider whether those cases are handled better without including all primitive-type expressions in this predicate.

[Marcono1234]

These cannot be null simply due to their type

Can't they? At least for expressions which actually have a value a primitive value can never be null (any dereferencing would have thrown a NullPointerException before).
For non-value expressions this of course does not apply, which is why I excluded TypeAccess; maybe there are more which need to be excluded. Though I assume since this predicate is mostly used with control flow analysis, such Expr types would not be part of the result set in the first place, but maybe it would be good to restrict it more nonetheless?

[aschackmull]

I agree that this addition is technically correct, hence "These cannot be null simply due to their type". What I'm questioning is the value that this adds, since the cost is a great many tuples.

[Marcono1234]

Sorry, misread your comment. Yes, performance considerations might be a fair point (you can probably estimate or meassure that better than me).

However, this change does increase the number of findings, see this query.

[Marcono1234]

The predicate clearlyNotNull(SsaVariable v, Expr reason) is probably also missing an AssignAddExpr of type String (performing String concatenation). In this case regardless of what value the variable or the RHS had, the variable will afterwards have a non-null result.
How would you model that?