seahorn
v0.1.0 Release (SV-COMP'16)
Seahornは、LLVMベースの言語の自動分析フレームワークです。このバージョンは、LLVM 14に対してコンパイルされます。
サポートされている機能のいくつかはです
Seahornは、主に自動検証で研究を実施するためのフレームワークとして開発されています。フレームワークは、さまざまな方法でまとめることができる多くのコンポーネントを提供します。ただし、「すぐに使用できる」静的分析ツールではありません。
多くの分析ツールと例には、フレームワークが記載されています。私たちは常に新しいアプリケーションを探しており、新しいユーザーにサポートを提供しています。何が起こっているのかの詳細については、（まったく更新されていない）ブログを確認してください。
Seahornは、変更されたBSDライセンスの下で配布されています。詳細については、license.txtを参照してください。
Seahornは、ユーザーと対話するためにseaと呼ばれるPythonスクリプトを提供します。アサーションが注釈されたCプログラムが与えられた場合、ユーザーは次のように入力する必要があります。SEAPF sea pf file.c
sea-pfの結果は、すべてのアサーションが保持されている場合、ASSのいずれかに違反している場合はunsat sat 。
オプションpf 、Seahornにfile.c llvmビットコードに翻訳し、一連の検証条件（VC）を生成し、最後に解決するように指示します。メインバックエンドソルバーはスペーサーです。
コマンドpf 、とりわけ、次のオプションを提供します。
--show-invars ：回答がunsat場合は、計算された不変剤を表示します。
--cex=FILE ：回答がsatいる場合はFILEにカウンターエクサムを保存します。
-g ：より追跡可能なカウンターエクサムをするために、デバッグ情報をコンパイルします。
--step=large ：大きなステップエンコーディング。各遷移関係は、ループフリーフラグメントに対応します。
--step=small ：小さなステップエンコーディング。各遷移関係は、基本ブロックに対応します。
--track=reg ：モデル（整数）レジスタのみ。
--track=ptr ：モデルレジスタとポインター（ただしメモリコンテンツではありません）
--track=mem ：スカラー、ポインター、およびメモリの両方の内容をモデル化します
--inline ：検証前にプログラムを導入します
--crab ：CRABの抽象的な解釈ベースのツールによって生成されたspacerに不変剤を注入します。すべてのクラブオプション（プレフィックス--crab ）の詳細については、こちらをご覧ください。オプション--log=crab入力することにより、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は平らなホーン句を生成する小さなステップをエンコードします（つまり、遷移システムは1つだけで生成flargeれます）。
--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を使用しません。 CRABを有効にするには、オプション--crab seaコマンドに追加します。
抽象的な通訳者はデフォルトでは操縦内であり、ゾーンドメインを数値抽象ドメインとして使用します。これらのデフォルトのオプションは、通常のユーザーに十分である必要があります。開発者の場合、他の抽象的なドメインを使用したい場合は、次の必要があります。
cmake options -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONでコンパイルします--crab-dom=DOMでseaを走らせるDOMができる：intterm-intboxes ：分離的な間隔の場合octpkクラブ間分析を使用するには、オプションでseaを走らせる必要があります--crab-inter
デフォルトでは、抽象的な通訳は、スカラー変数（つまり、LLVMレジスタ）に関する理由のみを理由にします。オプションでsea走らせる--crab-track=mem --crab-singleton-aliases=true 。
クラブはほとんどが経路に依存しますが、ホーン句ソルバーであるSpacerは経路に敏感です。経路に依存しない分析はより効率的ですが、関心のある特性を証明するには通常、パス感受性が必要です。これにより、ファーストクラブ（if option --crab ）を実行するという決定を動機付け、生成された不変剤をスペーサーに渡します。現在、スペーサーがカニによって生成された不変剤を使用する2つの方法があります。 seaオプション--horn-use-invs=VAL spacerそれらの不変剤の使用方法を伝えます。
VALがbgに等しい場合、不変剤は、補題が誘導的であることを証明するspacer誘導性を証明するためにのみ使用されます。VALがalways等しい場合、動作はbgに類似していますが、さらに不変性も使用され、 spacer反例をブロックするのに役立ちます。デフォルト値はbgです。もちろん、CRABがプログラムが安全であることを証明できる場合、スペーサーは余分なコストで負担しません。
プロパティはアサーションであると想定されています。 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は、指定されたエラー関数__VERIFIER_error()を呼び出すことにより、エンコードエラーロケーションのSV-Comp慣習に従います。 Seahornは、 __VERIFIER_error()が到達不可能で、プログラムが安全であると見なされた場合、 unsat返します。 Seahornは__VERIFIER_error()が到達可能で、プログラムが安全でないときに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プリントは、Seadsaによって構築されたコールグラフをdot形式で形成します。sea inspect --mem-callgraph-statsプリントは、Seadsaが行ったコールグラフ構造に関するいくつかの統計を標準出力します。sea inspect --mem-smc-stats Seadsaによって安全であることが証明できるメモリアクセスの数を印刷します。Seahornを始める最も簡単な方法は、Docker Distributionを使用することです。
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly sea Commandができることを探ることから始めます。
$ sea --help
$ sea pf --help nightlyタグは毎日自動的に更新され、最新の開発バージョンが含まれています。他のすべてのタグ（手動の更新が必要な）をまったく維持します。 DockerHubの日付を確認し、GitHubが古すぎる場合はGitHubに問題を記録します。
追加の例と構成オプションはブログにあります。ブログはまれに更新されます。特に、オプションの変更、機能が段階的に廃止され、新しいものが追加されます。ブログに問題がある場合は、お知らせください。少なくとも、ブログ投稿を更新して、コードの最新バージョンで動作することが期待されていないことを示します。
手動でインストールすることもできます。
Dockerファイルの指示に従って、 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をインストールし、4番目はLLVM 14から誤って省略されているLibpollyをインストールします（ただし、後続のバージョンに含まれます）
次に、上記のDockerファイルの命令に従ってください
この時点からの情報は、開発者のみです。 Seahornに貢献したい場合は、それに基づいて独自のツールを作成したい場合は、内部でどのように機能するかに興味がある場合は、読み続けてください。
SeahornにはLLVM、Z3、およびブーストが必要です。ライブラリの正確なバージョンは変更を続けていますが、Cmake Craftを使用して、正しいバージョンが利用可能であることを確認します。
依存関係の特定のバージョンを指定するには、通常の<PackageName>_ROOTおよび/または<PackageName>_DIRを使用します（詳細についてはfind_package（）を参照）cmake変数を使用します。
Seahornは、さまざまなリポジトリ（Seahorn Organizationの）に住む複数のコンポーネントに分かれています。ビルドプロセスは、必要に応じてすべてを自動的にチェックアウトします。現在のビルド手順については、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を使用してください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をコンパイルするために使用されるものと互換性がある必要があることに注意してください。特に、 `debug **モードでSeaHornコンパイルするには、LLVMのDebugビルドが必要です。このルートに行くことにした場合は、十分な忍耐、ディスクスペース、時間があることを確認してください。
または、プロジェクトはCmakeプリセットを使用して構成することができます。これを行うには、次のコマンドを実行するだけです。
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > cmakeを構成するには、 <BUILD_TYPE>がDebug 、 RelWithDebInfoまたはCoverage 、 <PRESET_NAME>を使用したいプリセットの1つです。現在利用可能なプリセットはjammyです。これらのプリセットでは、Z3が/opt/z3-4.8.9にインストールされ、yicesが/opt/yices-2.6.1にインストールされていると想定しています。
また、これにより、CMAKEツール拡張機能を使用して、VSコード内でプロジェクトを構成およびコンパイルできます。
別のコンピレーション設定を使用する場合、または他のディレクトリにz3またはyicesがインストールされている場合は、独自のプリセットを備えた独自のCMakeUserPresets.jsonファイルを作成する必要があります。
-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コンテキストに敏感であるため、ヒープのより細かい粒子のパーティションを機能呼び出しの存在下で生成できます。
CLAM： 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が付属しておらず、Build Directory（ run/bin ）またはPathで見つけることを期待しています。 Clangのバージョンが、Seahorn（現在LLVM14）のコンパイルに使用されたLLVMのバージョンと一致していることを確認してください。 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>は、Clangが開梱された場所です。
インフラストラクチャのテストは、いくつかのPythonパッケージに依存します。これらには独自の依存関係があります。それらを理解できない場合は、代わりにDockerを使用してください。
$ pip install lit OutputCheck networkx pygraphvizgcovとlcovを使用して、Seahornのテストカバレッジ情報を生成できます。カバレッジを有効にしてビルドするには、別のディレクトリの下でビルドを実行し、CMAKE構成中にCMAKE_BUILD_TYPEをCoverageする必要があります。
test-opsemターゲットのカバレッジレポートを生成するための例：
mkdir coverage; cd coverage CREATEとENTER COVERAGE BUILDディレクトリcmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem Run Opsemテストでは、対応するCMakeFilesディレクトリに.gcdaおよび.gcnoファイルを作成する必要があります。clang lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info希望モジュールgccカバレッジデータ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を参照してください。 Nightly Buildsのカバレッジレポートは、Codecovで入手できます
Seahornプロジェクトのコンパイルデータベースとそのすべてのサブプロジェクトは、 cmakeのオプションで-DCMAKE_EXPORT_COMPILE_COMMANDS=ON使用して生成されます。
コンパイルデータベースサポートでコードインデックスを取得する簡単な方法は、 compilation_database.jsonファイルをメインプロジェクトディレクトリにリンクし、エディターに固有の手順に従うことです。
clangdでlsp-uiを使用しますClion Check Clionの構成を備えたリモートワークフローの詳細なガイド。
MainFramerのフォークを使用してください。例の構成をお見逃しなく。
