KLEE:需要连接具有不同对齐方式的变量

Question

我正在尝试使用KLEE和一些Swift代码。为了简单起见，我创建了一个基本的hello world文件。

我能够成功地编译Swift文件(使用klee_make_symbolic)，但是当我尝试实际运行KLEE时会遇到问题。以下是我遵循的步骤：

1. 创建main.swift (以下文件内容)
2. 将其编译成bitcode - swiftc -import-objc-header /home/klee/klee_src/include/klee/klee.h main.swift -emit-bc -target x86_64-pc-linux-gnu
3. 运行klee main.bc

当我运行步骤3中的命令时，会收到许多警告+错误：

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

我还尝试使用--libc-uclibc (完整命令：klee --libc=uclibc main.bc)运行KLEE，它解决了警告，但得到了另一个错误：

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

以前没见过有人用斯威夫特用克莱，祝你好运！但是，您似乎需要编写自己的Swift运行时的基本实现，与klee和uclibc相似。例如，签名位于斯威夫特储存库中。