KLEE: Appending variables with different alignment need to be linked

Question

I am attempting to use KLEE with some Swift code. For the sake of simplicity, I've created a basic hello world file.

I am able to compile the Swift file (that uses klee_make_symbolic) successfully but I run into issues when I attempt to actually run KLEE. Here are the steps I've followed:

1. Create main.swift (file contents below)
2. Compile it into bitcode - swiftc -import-objc-header /home/klee/klee_src/include/klee/klee.h main.swift -emit-bc -target x86_64-pc-linux-gnu
3. Run klee main.bc

When I run the command from step 3 I get a number of warnings + errors:

KLEE: output directory is "/home/klee/klee-out-3"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: $sSPMa
KLEE: WARNING: undefined reference to variable: $sSPyxGs8_PointersMc
KLEE: WARNING: undefined reference to function: $sSS1poiyS2S_SStFZ
KLEE: WARNING: undefined reference to function: $sSS21_builtinStringLiteral17utf8CodeUnitCount7isASCIISSBp_BwBi1_tcfC
KLEE: WARNING: undefined reference to variable: $sSSN
KLEE: WARNING: undefined reference to function: $sSSySSxcs25LosslessStringConvertibleRzlufC
KLEE: WARNING: undefined reference to variable: $sSiN
KLEE: WARNING: undefined reference to variable: $sSis25LosslessStringConvertiblesWP
KLEE: WARNING: undefined reference to function: $ss27_allocateUninitializedArrayySayxG_BptBwlFyp_Tg5
KLEE: WARNING: undefined reference to function: $ss40_convertConstStringToUTF8PointerArgumentyyXlSg_xtSSs01_F0RzlF
KLEE: WARNING: undefined reference to variable: $ss4Int8VN
KLEE: WARNING: undefined reference to function: $ss5print_9separator10terminatoryypd_S2StF
KLEE: WARNING: undefined reference to function: swift_beginAccess
KLEE: WARNING: undefined reference to function: swift_bridgeObjectRelease
KLEE: WARNING: undefined reference to function: swift_endAccess
KLEE: WARNING: undefined reference to function: swift_getWitnessTable
KLEE: WARNING: undefined reference to function: swift_release
KLEE: ERROR: Unable to load symbol($sSiN) while initializing globals

I've also attempted to run KLEE with --libc-uclibc (full command: klee --libc=uclibc main.bc) which has solved the warnings but gets me a different error:

KLEE: NOTE: Using klee-uclibc : /tmp/klee_build90stp_z3/runtime/lib/klee-uclibc.bca 
KLEE: output directory is "/home/klee/klee-out-0" 
KLEE: Using STP solver backend
error: Appending variables with different alignment need to be linked!

---

main.swift

func helloWorld(i: Int) -> String {
    return "Hello World " + String(i)
}

var a = 0
klee_make_symbolic(&a, MemoryLayout<Int>.size, "a")
print(helloWorld(i: a))

Answer 1

Haven't seen that anyone tried to use KLEE with Swift before, good luck! However, it seems like you need to write you own base implementation of Swift's runtime in the likeness of klee-libc and uclibc. Signatures are located in Swift's repository, for example.