本文翻译自KLEE官方doxygen文档High level overview of KLEE。
原文链接：http://www.doc.ic.ac.uk/~dsl11/klee-doxygen/overview.html
KLEE 概览
这一篇文章宏观的讲述了一些KLEE内部实现的机制。
KLEE是基于LLVM的字节码来实现符号执行的。符号化的内存定义的方法是在程序执行过程中插入一个对KLEE的特殊调用（使用klee_make_symbolic函数）。KLEE会跟踪所有的符号化内存的使用，并且会收集使用这些符号化内存时的约束。那些使用了已声明的符号化内存的内存也会被符号化。当遇到一个使用符号化内存的分支时，KLEE会将执行状态一分为二，看看分支的哪一边可以找到一个可以满足符号约束的解。KLEE使用STP来求解这些符号约束。
接下来我们会介绍一些KLEE重要的组件。
解释器（Interpreter）
klee::Interpreter 在字节码解释器接口中是一个主要的抽象类。klee::Executor 是这个类的一个主要的实例。应用程序的状态（比如说：内存，寄存器，和程序计数器）会被存储在klee::ExecutionState 的一个实例中。每一条路径被执行的的时候都会有一个这样子的实例（除非当一些执行状态又合并到了一起的时候）。在有分支的地方，如果条件是符号化的，那klee::Executor::fork 方法就会返回一个klee::ExecutionState::StatePair 来表示一对由分支产生的ExecutionState 。
内存模型（Memory model）
MemoryObject 表示程序里面的地址分配（比如说调用malloc，stack objects， global variables），同时我们也可以简单的认为它是一个分配在某个地址上的对象独一无二的名字。ObjectState 是用来存储在一个特定的ExecutionState 中一个MemoryObject 中实际的内容（是不能被共享的）。事实上，我觉得这两个东西应该有更好的名字才对。
每一个ExecutionState 使用AddressSpace 数据结构来保存从MemoryObjects -> ObjectState 的映射（AddressSpace是通过一个固定的树来实现的，所以可以很轻易的复制和共享）。每个AddressSpace都会包含在映射中ObjectStates 的一部分。当一个AddressSpace被复制的时候，它会丢失它所包含的ObjectState。之后所有对ObjectState的写入操作，都会生成一个这个对象的复制（AddressSpace::getWriteable）。这是一个保险机制（这个机制对所有的对象都是有效的，不仅仅的全局对象）。
从状态和映射的角度来看，堆、栈和全局对象并没有什么区别。唯一对栈对象有一些些不同的处理就是，MemoryObject会被标记为isLocal并且这个MemoryObject会被存储在StackFrame的分配表里面。当StackFrame进行pop之后，这些对象都会被释放掉，以至于当前状态就再也不能直接访问内存了（对内存对象的引用可能仍然会在ReadExprs里，但是理论上说，实际的地址我们应该是找不到了）。
另外很重要的一点是，AddressSpace的映射是有序的。当我们想将一个符号化的地址解析为ObjectState时我们会用到它，我们先用一个特殊的值来表示符号化的地址，然后用这个值来找那些指针指向这个地址的对象。MemoryObjects和ObjectStates并没有什么区别。
表达式（Expressions）
很多Expr类都对llvm的指令集进行了建模。ref<Expr>是用来维护引用计数的，但是同时也是嵌入了许多常量表达式。事实上在现在的代码中，ConstantExprs几乎都不用被创建了。大多数表达式都是简明直接的。有一些表达式非常重要，比如说Concat?Expr这种类型的表达式，它能够将一些字节合并到一个更大的类型中。ExtractExpr能够将一个小类型从大类型中提取出来。ReadExpr能够访问一个符号化的数组。
所有对内存的访问都会被拆分成字节级的操作来实现。这就意味着内存系统（我指的的是ObjectState 数据结构）需要使用非常多的ExtractExpr和Concat?Expr表达式，所以这些表达式应该尽可能的压缩他们的操作数。
ReadExpr可能是里面最重要的一个了。理论上说，它就是一个索引和一些更新（写入）。ReadExpr会计算所有的值，所以两个索引是可以相等的。 ObjectState会缓存那些具体的写入或者是在具体的索引上的一些形式化的写入，但是对于形式化的索引来说它就需要构建一个针对这些更新的列表。这些信息会放在UpdateList和UpdateNode中，同样他们也是固定的数据结构，所以可以轻易的复制和共享。
搜索器（Searcher）
基础类是klee::Searcher。Executor通过使用一个Searcher 去选择下一个状态（也就是说一个程序实例只走一条路径），从而使得一条语句被执行。在KLEE中有非常多的Searcher实现，分别实现了不同的搜索策略。klee::RandomSearcher是随机选择下一个状态，klee::DFSSearcher使用了深度遍历的搜索方法。klee::MergingSearcher尝试去合并状态。