klee是什么
klee是通過對llvm bitcode進行解釋以實現符號執行的工具。它通過插入函數調用（klee_make_symbolic）對內存進行符號化。並且會跟蹤符號內存的使用，並收集使用這些符號內存的約束。如果有使用前面符號內存的其他內存，那么該內存也將會被符號化。當遇到一個使用符號化內存的分支時，KLEE會將執行狀態一分為二，看看分支的哪一邊可以找到一個可以滿足符號約束的解。KLEE使用STP來求解這些符號約束。
klee的主要組件
- 解釋器（Interpreter）
klee::Interpreter 在字節碼解釋器接口中是一個主要的抽象類。klee::Executor 是這個類的一個主要的實例。應用程序的狀態（比如說：內存，寄存器，和程序計數器）會被存儲在klee::ExecutionState 的一個實例中。每一條路徑被執行的的時候都會有一個這樣子的實例（除非當一些執行狀態又合並到了一起的時候）。在有分支的地方，如果條件是符號化的，那klee::Executor::fork 方法就會返回一個klee::ExecutionState::StatePair 來表示一對由分支產生的ExecutionState 。
2. 內存建模（memory）
MemoryObject 表示程序里面的地址分配（比如說調用malloc，stack objects， global variables），同時我們也可以簡單的認為它是一個分配在某個地址上的對象獨一無二的名字。ObjectState 是用來存儲在一個特定的ExecutionState 中一個MemoryObject 中實際的內容（是不能被共享的）。
每個ExecutionState都存放着一個MenoryObjects->ObjectState的映射，利用地址空間數據結構（AddressSpace）進行存儲，以immutable tree的形式實現。采用COW(寫時復制)的方式，當向一個ObjectState進行寫操作的時候，將會為這個object創建一個副本（AddressSpace::getWriteable）
通過函數AddressSpace::getWriteable(ObjectState os),找到適合寫入的os,如果需要將進行object副本創建嗎，返回os或者os的副本
從狀態和映射的角度來看，stack、heap和全局對象並沒有什么區別。唯一對stack對象有一些不同的處理就是，MemoryObject會被標記為isLocal並且這個MemoryObject會被存儲在StackFrame的分配表里面。當StackFrame進行pop之后，這些對象都會被釋放掉，以至於當前狀態就再也不能直接訪問內存了（對內存對象的引用可能仍然會在ReadExprs里，但是理論上說，實際的地址我們應該是找不到了）。
另外很重要的一點是，AddressSpace的映射是有序的。當我們想將一個符號化的地址解析為ObjectState時我們會用到它，我們先用一個特殊的值來表示符號化的地址，然后用這個值來找那些指針指向這個地址的對象。MemoryObjects和ObjectStates處理方式一樣。
當處理符號化地址的時候，會先為這個符號化地址獲得一個具體值，然后利用它開始查看指針能夠落到的Object范圍？
- 表達式（Expression）
表達式（Expressions）
很多Expr類都對llvm的指令集進行了建模。ref
Expr類對llvm指令集進行建模，也用於表示具體表達式（constant expression）
有四種類型：
1.Constant Expr
2.Concat Expr:用一些字節組成更大的類型
3.Extract Expr：從大的類型中提取出小的
4.ReadExpr:符號化數組訪問，（index，value）列表形式
內存的實現方式是將所有的訪問拆解為字節級的操作，所以內存系統（即ObjectState）會用到大量的ConcatExpr和ExtractExpr，所以這些表達式應該盡可能的壓縮他們的操作數。
ReadExpr可能是里面最重要的。理論上說，它就是一個索引和一些更新（寫入）。ReadExpr會計算所有的值，所以兩個索引是可以相等的。ObjectState使用一個cache處理具體的index的具體寫入和符號化寫入，但是對於符號化的index必須要創建一個列表。上述更新存儲在UpdateList和UpdateNode結構中,以immutable的形式，這樣可使拷貝成本較小且更容易實現共享。
對於每個ObjectState都會維護一個（index,value）嗎？index和value分別代表什么含義?是offset和value嗎？
- 搜索器（Searcher）
基礎類是klee::Searcher。Executor通過使用一個Searcher 去選擇下一個狀態（也就是說一個程序實例只走一條路徑），從而使得一條語句被執行。在KLEE中有非常多的Searcher實現，分別實現了不同的搜索策略。
klee提供了多種搜索策略:
klee::RandomSearcher 隨機選擇
klee::DFSSearcher 深度優先搜索
klee::MergingSearcher 合並states