lart

LART：LLVM抽象和改進工具

LART = LLVM抽象和改進工具。該工具的目的是提供實施各種程序摘要的LLVM至llVM轉換。就指令集而言，結果程序是正常的，可以執行和分析的混凝土LLVM程序。有關使用特殊LLVM固有功能和LLVM元數據節點插入（片段）程序上有效的抽象（S）的額外信息。 LART既提供了一個獨立的工具，該工具可以處理盤式比特碼文件，也提供了可以集成到復雜基於LLVM的工具中的框架。 LART背後的主要動機是為基於LLVM的模型檢查器和其他分析工具提供“預處理器”，從而通過減少問題大小來簡化其工作，而不會損害分析的健全性。 LART實施的抽象通常可以根據有關抽象的“部分”太粗糙的特定說明來完善（太粗糙的抽象會產生可見的虛假錯誤，可在後續分析中可見，但在原始程序中不存在）。

LLVM比特碼的抽象

整個練習的目的是從LLVM比特碼中抽象信息，從而使後續分析更有效（以某種精度為代價）。為此，我們主要需要能夠在LLVM程序中編碼非確定性選擇，這可以通過專用功能（類似於LLVM Interinsics）來完成。該函數命名為@lart.choice ，將一對界限作為參數，而非確定性返回屬於這些界限之間的值。

LLVM語義的擴展需要由下游工具識別。這也是唯一與標準LLVM比特碼的關鍵偏差。許多分析工具已經在內部甚至具有外部接口實現了類似的機制。適應工具不支持@lart.choice與LART合作通常非常簡單。

LART提供了其他特殊用途的功能，即@lart.meta.*家庭，但是就這些說明而言，大多數工具將能夠安全地忽略其存在，就像現有@llvm.dbg.*一樣。如果召集LART來提煉抽象（LART提供的每個抽像都帶有相應的改進程序，則計劃轉換將保留這些調用，以進行相應的改進程序，通常需要查找@lart.meta呼叫，該呼叫由抽象插入）。

雖然大多數傳統的抽象引擎是口譯員的工作，但也可以將抽象“彙編”到程序中。可以編譯符號指令，而不是（重新）解釋指令。在謂詞抽象的情況下，所得的比特碼將直接操縱和使用估計值代替具體變量。如上所述，重要的區別在於，由於某些謂詞可能具有不確定的估值（既是真實和錯誤），因此比特碼需要做出非確定性選擇。某些變量甚至可以完全抽象，所有這些變量的測試都將產生是和否答案。

建造

暫時使用或重複./devcontainer/Dockerfile的設置。

然後使用：

 ./scripts/build.sh

運行編譯器

 ./build/bin/lartcc <domain> <compiler arguments> in.c

選擇

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

測試

 lit -v build/test

注意： build/lartcc/lartcc必須具有exacutabple許可。