NotSubtype thrown while typechecking an ArrayStore opcode

[akshayutture]

Even without the --dump option, the benchmark below crashes for Jreduce

Here is the app+lib.jar file https://drive.google.com/file/d/1ZJuoszSs6eDEsoimyyQMCMWBR4ppnqGO/view?usp=sharing

Here is the command used and the output

• jreduce --work-folder _jreduce/workfolder --jre /usr/lib/jvm/java-8-openjdk-amd64/jre -S items+logic --stdlib ../../stdlib.bin -o app+lib.after.jar --timelimit 1800 app+lib.jar -- ls 17:37:16 ├ JReduce 17:37:16 │ ├ Started JReduce. 17:37:16 │ ├ Reading inputs 17:37:16 │ │ └ 0.002s 17:37:16 │ ├ Calculating Initial Problem 17:37:16 │ │ ├ setup 17:37:16 │ │ │ └ 0.050s 17:37:16 │ │ ├ run 17:37:16 │ │ │ └ 0.009s 17:37:16 │ │ └ 0.061s 17:37:16 │ ├ Refining Problem 17:37:16 │ │ └ 0.127s 17:37:16 │ ├ Initializing key function 17:37:16 │ │ ├ Calculating the hierarchy 17:37:16 │ │ │ ├ Load stdlib stubs 17:37:23 │ │ │ │ └ 6.516s 17:37:23 │ │ │ ├ Load project stubs 17:37:30 │ │ │ │ └ 7.024s 17:37:30 │ │ │ ├ Compute hierarchy 17:37:32 │ │ │ │ └ 2.242s 17:37:32 │ │ │ └ 15.783s 17:37:32 │ │ ├ Found 43862 items. 17:37:32 │ │ ├ Found 43844 facts. 17:37:33 │ │ ├ The core is 0 of them. 17:37:33 │ │ └ 16.359s 17:37:33 │ ├ Compute CNF 17:37:33 │ │ └ 0.289s jreduce: "io/reactivex/internal/operators/observable/ObservableAmb.subscribeActual:(Lio/reactivex/Observer;)V" Just (ByteCodeInst {offset = 104, opcode = ArrayStore ARef}) NotSubtype (TRef ["Lio/reactivex/ObservableSource;"]) (TRef ["Lio/reactivex/Observable;","Lio/reactivex/ObservableSource;"]) CallStack (from HasCallStack): error, called at src/JReduce/Logic.hs:971:31 in jreduce-0.1.0-Abs4ufFiDadAKpDliDdD1j:JReduce.Logic CallStack (from -prof): JReduce.Logic.logic.typeCheckStates (src/JReduce/Logic.hs:(969,7)-(977,29)) JReduce.Logic.logic (src/JReduce/Logic.hs:(624,1)-(1014,35)) JReduce.Logic.initializeKeyFunction (src/JReduce/Logic.hs:(277,1)-(373,69)) JReduce.Logic.computeCNF (src/JReduce/Logic.hs:(382,1)-(389,12)) JReduce.Logic.describeLogicProblem.\ (src/JReduce/Logic.hs:(481,91)-(556,5)) Control.Reduce.Problem.refineProblemA' (src/Control/Reduce/Problem.hs:(495,1)-(503,5)) JReduce.Logic.describeLogicProblem (src/JReduce/Logic.hs:(481,1)-(556,5)) JReduce.run.\ (src/JReduce.hs:(101,52)-(193,44)) Control.Reduce.Util.OptParse.withWorkFolder (src/Control/Reduce/Util/OptParse.hs:(107,1)-(116,41)) JReduce.run (src/JReduce.hs:(96,1)-(224,40)) Control.Reduce.Util.Logger.timeIO (src/Control/Reduce/Util/Logger.hs:(249,1)-(253,48)) Control.Reduce.Util.Logger.timedPhase'.runMa (src/Control/Reduce/Util/Logger.hs:163:7-84) Control.Reduce.Util.Logger.timedPhase' (src/Control/Reduce/Util/Logger.hs:(161,1)-(181,11)) JReduce.main (src/JReduce.hs:(69,1)-(81,48))

[kalhauge]

The main error that you encounter is while type checking the method:

io/reactivex/internal/operators/observable/ObservableAmb.subscribeActual:(Lio/reactivex/Observer;)V

and at the opcode:

Just (ByteCodeInst {offset = 104, opcode = ArrayStore ARef})

the typechecker throw:

NotSubtype (TRef ["Lio/reactivex/ObservableSource;"]) (TRef ["Lio/reactivex/Observable;","Lio/reactivex/ObservableSource;"])

I think that the error code should be improved, to me more readable, but that will not fix the problem you are facing.

Inspecting the app+lib.jar, here ObservableSource is a super interface of Observable. Which means that correctly that ObservableSource is not a subtype of Observable and ObservableSource.

It looks like the problem might be due to a typing problem, while storing in an array, in Java: https://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29#Covariant_arrays_in_Java_and_C.23

And currently, Jreduce, sadly, does not support covariant arrays.

Inspecting the decompiled code, my hypothesis seems to be correct, but if you have access to the source code, can you verify that the code in io/reactivex/internal/operators/observable/ObservableAmb.subscribeActual uses arrays covariance.

[akshayutture]

No there is no source code available. That class is from the library code. I guess we will have to rely on the decompiler output (assuming the decompiler will add back Generics that were erased in compilation)

Okay, I shall skip this benchmark in that case.