Potential NPE in AnnotatedTerm.java

[ErrReporter]

Hello, Our static analyses found a following potential NPE:

1. Return null to caller https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java#L1579

2. Return the return value of function term to caller https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/dpll/Clause.java#L292

3. Function toTerm executes and stores the return value to res (res can be null) https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/proof/SourceAnnotation.java#L75

4. res is used as the 2nd parameter in function annotatedTerm (res can be null) https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/SMTInterpol/src/de/uni_freiburg/informatik/ultimate/smtinterpol/proof/SourceAnnotation.java#L79

5. sub is used as the 2nd parameter in function hashAnnotations (sub can be null) https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/Theory.java#L1671

6. subTerm is passed as the this pointer to function hashCode (subTerm can be null) https://github.com/ultimate-pa/smtinterpol/blob/828ec76df5a88e07883a616002688ad6f2d8a184/Library-SMTLIB/src/de/uni_freiburg/informatik/ultimate/logic/AnnotatedTerm.java#L70

Commit: 828ec76df5a88e07883a616002688ad6f2d8a184

[jhoenicke]

It's a bit difficult to reply to this report. On the one hand, I applaud the use of formal methods to search for possible bugs. On the other hand, I believe there should be a few hundreds or thousands similar issues and it is hard to say how to "fix" them without introducing too much clutter.

First, one should not be able to trigger the NPE. Proving this would be very tricky, though. One would need to show that the code in question can only be executed after a logic was set, that setting any logic would ensure that the function symbol hashtable contains the symbol "or" with the right type, that the toTerm() methods of all implementations of Literal will always return a term of type bool, and probably also some more constraints that I'm currently overlooking. I can't be 100 % sure that all these conditions are actually satisfied for the current code and there may be an obscure situation where one of these assumptions is not true. However, I would see it as a different bug in other code, if this is triggered.

From a practical point, I believe that any triggered NPE will be close enough to the real bug to make it easily identifiable. One could improve it a bit by adding an explicit assumption to clause.toTerm() that the result is not null with a more clear error message to guide the coder that either the logic wasn't set or the input terms had wrong type. The question is if such an assertion would make the static verifier happy or wether it would just complain about the possible assertion violation.

[ErrReporter]

@jhoenicke Thank you for the insightful comments.

In fact, we believe your code quality is generally good, and our ultra-precise path-sensitive code analyzer only produces a dozen of NPE reports. Defending them would not generate too much clutter and would significantly strengthen the solver availability in very extreme cases generated from solver fuzzing tools if you have heard any. We are very happy to submit the rest bug reports and corresponding PRs to fix them if you would like to do so.