NullPointerException processing (ternary) conditional inside String concatenation when branches have different types

[tlringer]

I'm not sure if this error is coming from SPARTA or CheckerFramework, so please feel free to move this if it's not SPARTA-specific. I put it here because I tried it with the NullnessChecker and it didn't happen, but it might happen with other checkers, too.

I'm annotating a very small existing application. Without any annotations, it fails with a NullPointerException when I run SPARTA. I've localized the failure to one line:

mTimerTextView.setText(minutes+":"+((seconds < 10) ? "0"+seconds : seconds)+"."+milliseconds);

Interestingly, this entire expression type-checks as a String, but the inner conditional doesn't. You can assign it to Object:

Object secondsText = (seconds < 10) ? "0" + seconds : seconds; // typechecks
String secondsText = (seconds < 10) ? "0" + seconds : seconds; // doesn't typecheck

Otherwise, since seconds is an integer, you can't assign the result to a String.

So out of curiosity, I tried changing it so that the inner piece typechecks as a String:

mTimerTextView.setText(minutes+":"+((seconds < 10) ? "0"+seconds : String.valueOf(seconds))+"."+milliseconds);

This resolves the error.

Here's an abbreviated stack trace:

error: SourceChecker.typeProcess: unexpected Throwable (NullPointerException) while processing /home/tringer/app-evals/good/VoiceRecorder/src/main/java/eu/siacs/conversations/voicerecorder/ui/RecordingActivity.java
Compilation unit: /home/tringer/app-evals/good/VoiceRecorder/src/main/java/eu/siacs/conversations/voicerecorder/ui/RecordingActivity.java
Exception: java.lang.NullPointerException; Stack trace: org.checkerframework.javacutil.AnnotationUtils.annotationName(AnnotationUtils.java:165)
org.checkerframework.javacutil.AnnotationUtils.areSameByName(AnnotationUtils.java:215)
org.checkerframework.javacutil.AnnotationUtils.areSameByClass(AnnotationUtils.java:231)
sparta.checkers.FlowAnnotatedTypeFactory$FlowQualifierHierarchy.isPolySinkQualifier(FlowAnnotatedTypeFactory.java:746)
sparta.checkers.FlowAnnotatedTypeFactory$FlowQualifierHierarchy.isSubtype(FlowAnnotatedTypeFactory.java:785)
org.checkerframework.framework.type.DefaultTypeHierarchy.isAnnoSubtype(DefaultTypeHierarchy.java:260)
org.checkerframework.framework.type.DefaultTypeHierarchy.isPrimarySubtype(DefaultTypeHierarchy.java:242)
org.checkerframework.framework.type.DefaultTypeHierarchy.isPrimarySubtype(DefaultTypeHierarchy.java:228)
org.checkerframework.framework.type.DefaultTypeHierarchy.visitPrimitive_Declared(DefaultTypeHierarchy.java:631)
org.checkerframework.framework.type.DefaultTypeHierarchy.visitPrimitive_Declared(DefaultTypeHierarchy.java:51)
org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:498)
org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:220)
org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtypeOfAll(DefaultTypeHierarchy.java:309)
org.checkerframework.framework.type.DefaultTypeHierarchy.visitIntersectionSupertype(DefaultTypeHierarchy.java:776)
org.checkerframework.framework.type.DefaultTypeHierarchy.visitPrimitive_Intersection(DefaultTypeHierarchy.java:641)
org.checkerframework.framework.type.DefaultTypeHierarchy.visitPrimitive_Intersection(DefaultTypeHierarchy.java:51)
org.checkerframework.framework.util.AtmCombo.accept(AtmCombo.java:506)
org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:220)
org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:170)
org.checkerframework.framework.type.DefaultTypeHierarchy.isSubtype(DefaultTypeHierarchy.java:151)
org.checkerframework.common.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:1879)
org.checkerframework.common.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:1839)
org.checkerframework.common.basetype.BaseTypeVisitor.visitConditionalExpression(BaseTypeVisitor.java:1439)
sparta.checkers.validator.BaseFlowVisitor.visitConditionalExpression(BaseFlowVisitor.java:127)
sparta.checkers.validator.BaseFlowVisitor.visitConditionalExpression(BaseFlowVisitor.java:40)

You can find the application here. I've already changed that line, so if you want to reproduce it you'll have to change it back. SPARTA is already integrated with gradle if you run this from the top directory:

gradle compileDebugJavaWithJavac -PrunSparta=true

You can edit build.gradle to swap in other checkers.

[smillst]

Thanks for the bug report! Could you try to minimize the testcase?

[tlringer]

I can reproduce a similar bug with a single line in an arbitrary Java file:

String text = 5 + ":" + ((1 < 10 ? "0" + 1 : 1) + "." + 0);

This is totally valid in Java. In this case, I get a ClassCastException instead:

Exception: java.lang.ClassCastException: Cannot cast java.lang.String to java.lang.Double; Stack trace: java.lang.Class.cast(Class.java:3369)
org.checkerframework.javacutil.AnnotationUtils.getElementValueArray(AnnotationUtils.java:487)
org.checkerframework.common.value.ValueAnnotatedTypeFactory.getDoubleValues(ValueAnnotatedTypeFactory.java:1012)
org.checkerframework.common.value.ValueAnnotatedTypeFactory$ValueQualifierHierarchy.leastUpperBound(ValueAnnotatedTypeFactory.java:361)
org.checkerframework.framework.type.QualifierHierarchy.leastUpperBounds(QualifierHierarchy.java:170)
org.checkerframework.framework.util.AnnotatedTypes.addAnnotationsImpl(AnnotatedTypes.java:949)
org.checkerframework.framework.util.AnnotatedTypes.addAnnotations(AnnotatedTypes.java:827)
org.checkerframework.framework.util.AnnotatedTypes.annotateAsLub(AnnotatedTypes.java:768)
org.checkerframework.framework.type.TypeFromExpressionVisitor.visitConditionalExpression(TypeFromExpressionVisitor.java:145)

In this particular case it looks like it's just CheckerFramework that's crashing, so maybe this is best treated as a CheckerFramework bug? Again, I'm not sure.

I'm going to see if I can figure out how to get an NPE instead like in the original code.

[tlringer]

I'm actually not sure how to reproduce the NPE outside of the environment, so hopefully the other error combined with link to the app code is enough of a lead