With some help from the Kt native team im sure it ...

# kotlin-native

[jkbbwr]

With some help from the Kt native team im sure it could be made more stable and then it could provide a massive boon to the kt/native ecosystem

[olonho]

pretty interesting, how do you think it shall be better done?

[jkbbwr]

So the biggest issue was, that kotlin methods like @Kotlin_Int_inc were not defined in the bitcode, so the verifier couldn't run against them. The seahorn guy worked around it by manually defining them

;;declare i32 @Kotlin_Int_inc(i32)
define i32 @Kotlin_Int_inc(i32) {
entry:
   %y = add i32 %0, 1
   ret i32 %y
}

[jkbbwr]

Either offering some shadow implementations in pure llvm bitcode or forcing the compiler to have an option where it emits everything would solve this

[olonho]

It is in the bitcode, just one produced from C++ sources, but it is linked together, and so could be analyzed

[jkbbwr]

I couldn't find a way with the compiler to get everything emitted to bitcode in one step

[jkbbwr]

https://gist.github.com/jkbbwr/fa3b7c6ac53a57c8bcf2b2cb753e4f4a

[olonho]

guess smth like bitcode stored here https://github.com/JetBrains/kotlin-native/blob/9e1e7559a2c39ebc51644234033fc44aa3a2b3e5/backend.native/compiler/ir/backend.native/src/org/jetbrains/kotlin/backend/konan/CompilerOutput.kt#L67 is what you need

[olonho]

or even better here: https://github.com/JetBrains/kotlin-native/blob/9e1e7559a2c39ebc51644234033fc44aa3a2b3e5/backend.native/compiler/ir/backend.native/src/org/jetbrains/kotlin/backend/konan/LinkStage.kt#L120

[jkbbwr]

Huh I might "hack" an emitter into that and report back