seahorn下載 - seahorn源代碼下載

seahorn

其他類別

v0.1.0 Release (SV-COMP'16)

下載

關於

Seahorn是基於LLVM的語言的自動分析框架。此版本針對LLVM 14編譯。

一些支持的功能是

基於抽象解釋的靜態分析
基於統一的上下文敏感指針分析
基於SMT的有限模型檢查（即符號執行）
基於CHC的軟件模型檢查（即不變推理）
可執行的反例（即，沒有報告，只是錯誤！）

Seahorn主要是用於進行自動驗證研究的框架。該框架提供了許多可以通過多種方式組合在一起的組件。但是，這不是“開箱即用”的靜態分析工具。

框架提供了許多分析工具和示例。我們一直在尋找新的應用程序，並為新用戶提供支持。有關正在發生的事情的更多信息，請查看我們（不經常更新的）博客。

執照

Seahorn根據修改後的BSD許可分發。有關詳細信息，請參見License.txt。

介紹

Seahorn提供了一個名為sea的Python腳本，可以與用戶互動。給定一個帶有斷言註釋的C程序，用戶只需要鍵入： sea pf file.c

如果所有斷言持有所有斷言，則sea-pf的結果是unsat sat如果違反了任何主張。

pf選項告訴Seahorn將file.c轉換為LLVM比特碼，生成一組驗證條件（VCS），最後解決它們。主要的後端求解器是間隔者。

命令pf提供以下選項：

--show-invars ：如果答案是unsat則顯示計算的不變性。
--cex=FILE ：如果答案是sat在FILE中存儲一個反例。
-g ：與調試信息一起編譯，以獲取更多可跟踪的反例。
--step=large ：大型編碼。每個過渡關係對應於無環的片段。
--step=small ：小步驟編碼。每個過渡關係對應於一個基本塊。
--track=reg ：模型（整數）僅註冊。
--track=ptr ：模型寄存器和指針（但不是內存內容）
--track=mem ：模擬標量，指針和內存內容
--inline ：在驗證之前將程序嵌入
--crab ：基於Crab Abstract-terpretation工俱生成的spacer中的注入不變性。在此處閱讀以獲取有關所有螃蟹選項（前綴--crab ）的詳細信息。您可以通過鍵入選項--log=crab來查看哪些不變性是由螃蟹推斷出來的。
--bmc ：使用BMC引擎。

sea pf是運行多個命令的管道。管道的各個部分也可以單獨運行：

sea fe file.c -o file.bc ：SeaHorn Frontend將C程序轉換為優化的LLVM比特碼，包括混合儀器轉換。
sea horn file.bc -o file.smt2 ：SeaHorn從file.bc生成驗證條件，並將其輸出為SMT -LIB V2格式。用戶可以通過添加以下精度的不同編碼樣式在不同的編碼樣式之間進行選擇：
- --step={small,large,fsmall,flarge} ，其中small步驟編碼， large是大量的編碼， fsmall是小步驟編碼生成平坦的號角條款（即，它僅生成一個具有一個謂詞的過渡系統），而flarge ：Block-Large-Large編碼生成平坦的角喇叭。
- --track={reg,ptr,mem}其中reg僅建模整數標量， ptr模型reg和指針地址，以及mem模型ptr和內存內容。
sea smt file.c -o file.smt2 ：以SMT -LIB2格式生成CHC。是sea fe的別名，然後是sea horn 。命令sea pf是sea smt --prove 。
sea clp file.c -o file.clp ：以CLP格式生成CHC。
sea lfe file.c -o file.ll ：運行遺產前端

要查看所有命令，請鍵入sea --help 。要查看每個單獨命令CMD（例如， horn ）的選項，型sea CMD --help （例如， sea horn --help ）。

抽象解釋的靜態分析

使用螃蟹的誘導不變性推斷

Seahorn默認情況下不使用螃蟹。要啟用螃蟹，請將選項--crab添加到sea Command。

默認情況下，抽象解釋器是過程內部的，它將區域域用作數值抽象域。對於普通用戶，這些默認選項應該足夠。對於開發人員，如果您想使用其他抽象域，則需要：

使用cmake選項編譯-DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ON
帶有選項的sea --crab-dom=DOM DOM在其中可能是：
- int間隔
- 具有未解釋功能的間隔的term-int
- boxes ：用於分離的間隔
- 十月的oct
- pk POLEHEDRA的PK

要使用螃蟹術間分析，您需要使用選項運行sea --crab-inter

默認情況下，抽象解釋器僅有關標量變量（即LLVM寄存器）的原因。與選項一起運行sea --crab-track=mem --crab-singleton-aliases=true thue of Memory內容的理由。

如何使用螃蟹在墊片中產生的不變性

螃蟹主要是對路徑不敏感的，而我們的號角求解器Spacer對路徑敏感。儘管不敏感的分析更有效，但通常需要路徑敏感性才能證明感興趣的特性。這激發了我們運行第一隻螃蟹（如果選擇--crab ）的決定，然後將生成的不變性傳遞給墊片。當前，墊片使用Crab生成的不變式有兩種方法。 sea選項--horn-use-invs=VAL告訴spacer如何使用那些不變式：

如果VAL等於bg則僅使用不變性來幫助spacer證明引理是感應的。
如果VAL等於always ，則該行為與bg相似，但此外，不變性也可用於幫助spacer阻塞反例。

默認值為bg 。當然，如果螃蟹可以證明該程序是安全的，那麼墊片不會以任何額外的費用產生。

屬性規範

假定屬性是斷言。 Seahorn提供了靜態斷言命令sassert ，如下示例所示

 /* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();

int main ( void ) {
    int k = 1 ;
    int i = 1 ;
    int j = 0 ;
    int n = nd ();
    while ( i < n ) {
        j = 0 ;
        while ( j < i ) {
            k += ( i - j );
            j ++ ;
        }
        i ++ ;
    }
    sassert ( k >= n );
}

在內部，SeaHorn遵循SV-Comp的規定編碼錯誤位置，通過呼叫指定的錯誤函數__VERIFIER_error() 。當__VERIFIER_error()無法到達時，SeaHorn返回unsat ，並且該程序被認為是安全的。當__VERIFIER_error()到達且程序不安全時，Seahorn返回sat 。 sassert()方法定義在seahorn/seahorn.h中。

檢查代碼

除了證明屬性或製作反例外，有時還要檢查正在分析的代碼以了解其複雜性是有用的。為此，Seahorn提供了指揮sea inspect 。例如，給定的C程序ex.c類型：

 sea inspect ex.c --sea-dsa=cs+t --mem-dot

選項--sea-dsa=cs+t可以實現FMCAD19中描述的新上下文，類型敏感的SEA-DSA分析。此命令為輸入程序中的每個函數FUN生成一個FUN.mem.dot文件。要可視化主函數的圖，請使用Web Graphivz接口或以下命令：

$ dot -Tpdf main.mem.dot -o main.mem.pdf

內存圖的更多詳細信息在Seadsa存儲庫中：此處。

使用sea inspect --help來查看所有選項。目前，可用選項是：

sea inspect --profiler打印功能，基本塊，循環等的數量。
sea inspect --mem-callgraph-dot打印以dot格式，由Seadsa構建的呼叫圖。
sea inspect --mem-callgraph-stats打印以標準輸出一些有關Seadsa完成的呼叫圖構造的Statstics。
sea inspect --mem-smc-stats打印了Seadsa可以證明可以證明的記憶訪問的數量。

安裝

開始使用Seahorn的最簡單方法是通過Docker發行。

$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly

首先探索sea Command可以做什麼：

$ sea --help
$ sea pf --help

nightly標籤每天自動刷新，並包含最新的開發版本。我們很少維護所有其他標籤（需要手動更新）。檢查Dockerhub上的日期，並在Github上記錄問題，以確定它們是否過時。

其他示例和配置選項在博客上。博客很少更新。特別是，選項更改，逐步淘汰功能，添加了新事物。如果您在博客中發現問題，請告訴我們。我們至少會更新博客文章，以表明它不會與最新版本的代碼一起使用。

您也可以通過以下方式手動安裝：

按照Docker文件Dockerfile中的說明： docker/seahorn-builder.Dockerfile 。

如果這不起作用，請運行：

$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *

前3個命令將安裝LLVM 14，第四命令將安裝LLVM 14省略的LIBPOLLY（但包含在後續版本中）

接下來，按照上面的Docker文件中的說明

開發人員的區域

此時的信息僅適用於開發人員。如果您想為Seahorn做出貢獻，請基於它構建自己的工具，或者只是對其在內部工作方式感興趣，請繼續閱讀。

彙編說明

Seahorn需要LLVM，Z3和Boost。庫的確切版本不斷變化，但Cmake Craft用於檢查正確版本是否可用。

要指定任何依賴項的特定版本，請使用通常的<PackageName>_ROOT和/或<PackageName>_DIR （有關詳細信息）CMAKE變量。

Seahorn被分成多個生活在不同存儲庫（在Seahorn組織下）的組件。構建過程會根據需要自動檢查所有內容。對於當前的構建說明，請檢查CI腳本。

這些是通用步驟。不要使用它們。以更好的方式閱讀：

cd seahorn ; mkdir build ; cd build （構建目錄也可以在源目錄之外。）
cmake -DCMAKE_INSTALL_PREFIX=run ../ （需要安裝！ ）
cmake --build . --target extra && cmake .. （在其他地方生活的克隆組件）
cmake --build . --target crab && cmake .. （克隆蟹庫）
cmake --build . --target install （在run下構建和安裝所有內容）
cmake --build . --target test-all （運行測試）

注意：測試工作需要安裝目標！

更好的彙編說明

為了獲得增強的發展經驗：

使用clang
在Linux上，使用lld鏈接器
在發行版中包括調試符號
使用忍者
導出compile_commands.json

在Linux上，我們建議以下cmake配置：

 $ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run 
      -DCMAKE_BUILD_TYPE=RelWithDebInfo 
      -DCMAKE_CXX_COMPILER="clang++-14" 
      -DCMAKE_C_COMPILER="clang-14" 
      -DSEA_ENABLE_LLD=ON  
      -DCMAKE_EXPORT_COMPILE_COMMANDS=1 
      ../ 
      -DZ3_ROOT=<Z3_ROOT> 
      -DLLVM_DIR=<LLMV_CMAKE_DIR> 
      -GNinja
$ (cd .. && ln -sf build/compile_commands.json .)

其中<Z3_ROOT是包含Z3二進制分佈的目錄，而LLMV_CMAKE_DIR是包含LLVMConfig.cmake的目錄。

CMAKE_BUILD_TYPE的其他法律選擇是Debug和Coverage 。請注意， CMAKE_BUILD_TYPE必須與用於編譯LLVM cmake_build_type兼容。特別是，您將需要LLVM的Debug構建來以“調試**”模式編譯SeaHorn 。確保您有足夠的耐心，磁盤空間和時間，如果您決定走這條路線。

或者，可以使用CMAKE預設配置該項目。為此，只需運行以下命令：

$ cmake --preset < BUILD_TYPE > - < PRESET_NAME >

要配置cmake，其中<BUILD_TYPE>是： Debug ， RelWithDebInfo或Coverage之一， <PRESET_NAME>是您想要使用的預設。當前可用的預設是： jammy 。這些預設假設您已安裝在/opt/z3-4.8.9中的Z3，並且安裝在/opt/yices-2.6.1中的YICES。

這還將允許使用CMAKE工具擴展程序在VS代碼中配置和編譯該項目。

如果您想使用不同的彙編設置，或者您在任何其他目錄中安裝了Z3或YICE，則需要使用自己的預設製作自己的CMakeUserPresets.json文件。

在Mac上編譯

請勿包括-DSEA_ENABLE_LLD=ON 。默認編譯器是clang的，因此您可能無需明確設置它。

額外的目標

Seahorn提供了幾個組件，它們通過extra目標自動克隆和安裝。這些組件可以由Seahorn以外的其他項目使用。

SEA-DSA： git clone https://github.com/seahorn/sea-dsa.git
sea-dsa是一種新的基於DSA的堆分析。與llvm-dsa不同， sea-dsa是上下文敏感的，因此，可以在存在功能調用的情況下生成堆的細粒分區。
蛤： git clone https://github.com/seahorn/crab-llvm.git
clam使用抽象的解釋技術為Seahorn的其餘後端提供了誘導不變性。
llvm-seahorn： git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn提供了量身定制的InstCombine和IndVarSimplify LLVM通行證以及LLVM通行證的量身定制的版本，以將不確定的值轉換為非確定呼叫等。

Seahorn不帶有自己的Clang版本，並且希望在構建目錄（ run/bin ）或路徑中找到它。確保Clang的版本與用於編譯Seahorn的LLVM的版本匹配（當前LLVM14）。提供正確版本的Clang的最簡單方法是從llvm.org下載它，在某個地方打開它，並在run/bin中創建指向clang和clang++的符號鏈接。

$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++

其中<CLANG_ROOT>是拆開包裝的位置。

測試

測試基礎架構取決於幾個Python軟件包。這些有自己的依賴性。如果您無法弄清楚它們，請改用Docker。

$ pip install lit OutputCheck networkx pygraphviz

覆蓋範圍

我們可以使用gcov和lcov來為Seahorn生成測試覆蓋信息。要啟用覆蓋範圍，我們需要在其他目錄下運行構建，並將CMAKE_BUILD_TYPE設置為CMAKE配置期間的Coverage 。

用於生成test-opsem目標覆蓋範圍報告的示例步驟：

mkdir coverage; cd coverage創建並輸入覆蓋範圍構建目錄
cmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../
照常完成構建
cmake --build . --target test-opsem運行OPSEM測試，現在.gcda和.gcno文件應在相應的CMakeFiles目錄中創建
lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info從所需模塊中收集覆蓋範圍數據，如果clang用作編譯器而不是gcc ，請創建BASH腳本llvm-gcov.sh ：

 #! /bin/bash
exec llvm-cov gcov " $@ "

$ chmod +x llvm-gcov.sh

然後將--gcov-tool <path_to_wrapper_script>/llvm-gcov.sh附加到lcov -c ...命令。 6.從所需目錄中提取數據並生成HTML報告：

lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report

然後在瀏覽器中打開coverage_report/index.html以查看覆蓋報告

另請參閱CI使用的腳本的scripts/coverage 。 Codecov提供了夜間構建的報導報告