ikos
Public release 3.4
IKOS（オープン静的アナライザーの推論カーネル）は、抽象的な解釈の理論に基づいたC/C ++の静的分析器です。
Ikosは、抽象的な解釈に基づいてサウンド静的アナライザーの開発を促進するように設計されたC ++ライブラリとしてスタートしました。アプリケーションのアプリケーションまたはファミリのための静的アナライザーの専門化は、精度とスケーラビリティの両方を達成するために重要です。このようなアナライザーを開発することは困難であり、抽象的な解釈において重要な専門知識が必要です。
IKOSは、コントロールフローグラフ、フィックスポイントイテレーター、数値抽象ドメインなどの最先端の抽象的な解釈データ構造とアルゴリズムの一般的かつ効率的な実装を提供します。IKOSは特定のプログラミング言語とは無関係です。
Ikosは、LLVMに基づいたCおよびC ++静的アナライザーも提供します。 CおよびC ++プログラムにランタイムエラーがないことを検出および証明するためのスケーラブルな分析を実装します。
IKOSはNASAオープンソース契約バージョン1.3の下でリリースされました。ライセンスを参照してください。
リリースを参照してください。
トラブルシューティングを参照してください
LinuxまたはMacOSにIkosをインストールするには、 Homebrewを使用することをお勧めします。
まず、これらの指示に従ってHomeBrewをインストールします。
次に、単に実行します：
$ brew install nasa-sw-vnv/core/ikos
Windowsについては、LinuxにWindowsサブシステムの使用を検討してください。
loop.cと呼ばれるファイル内の次のCプログラムを分析するとします。
1 : #include <stdio.h>
2 : int a [ 10 ];
3 : int main ( int argc , char * argv []) {
4 : size_t i = 0 ;
5 : for (; i < 10 ; i ++ ) {
6 : a [ i ] = i ;
7 : }
8 : a [ i ] = i ;
9 : printf ( "%i" , a [ i ]);
10 : }このプログラムをIKOSで分析するには、単に実行してください。
$ ikos loop.c
次の出力が表示されます。 Ikosは、8行目と9行でバッファオーバーフローの2つの発生を報告しています。
[*] Compiling loop.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
# Time stats:
clang : 0.037 sec
ikos-analyzer: 0.023 sec
ikos-pp : 0.007 sec
# Summary:
Total number of checks : 7
Total number of unreachable checks : 0
Total number of safe checks : 5
Total number of definite unsafe checks: 2
Total number of warnings : 0
The program is definitely UNSAFE
# Results
loop.c: In function 'main':
loop.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
a[i] = i;
^
loop.c: In function 'main':
loop.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
printf("%i", a[i]);
^
ikosコマンドは、ソースファイル（ .c 、 .cpp ）またはllvmビットコードファイル（ .bc ）を入力として使用し、ランタイムエラー（未定義の動作とも呼ばれる）を見つけるために分析し、現在のワーキングディレクトリに結果データベースoutput.dbを作成し、レポートを印刷します。
レポートでは、各行に次のステータスのいずれかがあります。
デフォルトでは、Ikosは、コンパイラが行うように、ターミナルに直接警告とエラーを表示します。
分析レポートが大きすぎる場合、使用する必要があります。
ikos-report output.dbターミナルのレポートを調べますikos-view output.db Webインターフェイスでレポートを調べる詳細：
以下は、ソースからikosを構築するための指示です。これは、オペレーティングシステムにIKOをパッケージ化するか、コードベースを試したい上級ユーザー向けです。それ以外の場合は、上記の指示に従ってください。
アナライザーを構築して実行するには、次の依存関係が必要になります。
それらのほとんどは、パッケージマネージャーを使用してインストールできます。
注：ソースからLLVMを構築する場合、ランタイムタイプ情報（RTTI）を有効にする必要があります。
システムにすべての依存関係があるので、IKOSを構築およびインストールできます。
IKOS分布を開くと、次のディレクトリ構造が表示されます。
.
├── CMakeLists.txt
├── LICENSE.pdf
├── README.md
├── RELEASE_NOTES.md
├── TROUBLESHOOTING.md
├── analyzer
├── ar
├── cmake
├── core
├── doc
├── frontend
├── script
└── test
IkosはCmakeビルドシステムを使用しています。インストール後にすべてのバイナリ、ライブラリ、ヘッダーを含むインストールディレクトリを指定する必要があります。このディレクトリを指定しない場合、Cmakeはすべてを配布のルートディレクトリにinstall下にインストールします。以下の手順では、IKOSの下の/path/to/ikos-install-directoryをインストールします。
IKOSの構築とインストールの手順は次のとおりです。
$ mkdir build
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=/path/to/ikos-install-directory ..
$ make
$ make install
次に、パスにikosを追加します（.bashrcにこれを追加することを検討してください）：
$ PATH="/path/to/ikos-install-directory/bin:$PATH"
テストを構築して実行するには、単に入力してください。
$ make check
Contributors.mdを参照してください
Sung Kook Kim、Arnaud J. Venet、Aditya V. Thakur。決定論的並列フィックスポイント計算。プログラミング言語の原則（POPL 2020） 、ルイジアナ州ニューオーリンズ（PDF）。
Guillaume Brat、Jorge Navas、Nija Shi、Arnaud Venet。 IKOS：抽象的な解釈に基づく静的分析のフレームワーク。ソフトウェアエンジニアリングおよび正式な方法に関する国際会議（SEFM 2014）の議事録、フランス、Grenoble（PDF）。
Arnaud Venet。ゲージドメイン：線形不平等不変剤のスケーラブルな分析。コンピューター支援検証の議事録（CAV 2012） 、バークレー、カリフォルニア州、米国2012年。コンピューターサイエンスの講義ノート、139〜154ページ、第7358巻、Springer 2012（PDF）。
doc/coding_standards.mdを参照してください
doc/overview.mdを参照してください
