search

typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
1.02k stars 351 forks source link

Algebraic Data Type Performance Problems #4412

Open hborders opened 3 years ago

hborders commented 3 years ago

Thanks so much for this project. It's the best way I've found to analyze nullability of Java!

When using an algebraic data type pattern, checker performance degrades as the number of cases within the algebraic data type increases. I haven't let checker run long enough to complete the either5 or higher or emptyeither6 or higher cases.

An example project is available at https://github.com/hborders/checker-perf

$ ./gradlew :emptyeither2:assemble -DrocksSkipCheckerFramework=false
Configuration on demand is an incubating feature.

BUILD SUCCESSFUL in 4s

$ ./gradlew :either2:assemble -DrocksSkipCheckerFramework=false
Configuration on demand is an incubating feature.

BUILD SUCCESSFUL in 5s

$ ./gradlew :emptyeither3:assemble -DrocksSkipCheckerFramework=false
Configuration on demand is an incubating feature.

BUILD SUCCESSFUL in 8s

$ ./gradlew :either3:assemble -DrocksSkipCheckerFramework=false
Configuration on demand is an incubating feature.

BUILD SUCCESSFUL in 16s

$ ./gradlew :emptyeither4:assemble -DrocksSkipCheckerFramework=false
Configuration on demand is an incubating feature.

BUILD SUCCESSFUL in 47s

$ ./gradlew :either4:assemble -DrocksSkipCheckerFramework=false
Configuration on demand is an incubating feature.

BUILD SUCCESSFUL in 2m 20s

$ ./gradlew :emptyeither5:assemble -DrocksSkipCheckerFramework=false
Configuration on demand is an incubating feature.

BUILD SUCCESSFUL in 8m 17s
smillst commented 3 years ago

Thanks for reporting this and the test case. I've made some progress on speeding up this test case, #4416, but it's still too slow.

hborders commented 3 years ago

Thanks. I'll test it on the next release.