function

関数

関数は、Cプログラムの条件付き終了と条件付き保証と再発特性を証明するために設計された研究プロトタイプ静的分析器です。このツールは、抽象的な解釈により、終了、保証、再発の特性のために、区分的定義のランキング関数と十分な前提条件を自動的に推進します。

機能は、記事に記載されている分析方法と抽象的なドメインを実装およびテストするために開発されました。

 N. Courant, C. Urban. Precise Widening Operators for Proving Termination by Abstract Interpretation.

C. Urban, A. Miné. Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation.
In Proc. 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015). 

C. Urban, A. Miné. A Decision Tree Abstract Domain for Proving Conditional Termination.
In Proc. 21st International Static Analysis Symposium (SAS 2014).

C. Urban, A. Miné. An Abstract Domain to Infer Ordinal-Valued Ranking Functions.
In Proc. 23rd European Symposium on Programming (ESOP 2014).

C. Urban. The Abstract Domain of Segmented Ranking Functions.
In Proc. 20th International Static Analysis Symposium (SAS 2013).

関数のメインWebサイトは、http：//www.di.ens.fr/~urban/function.htmlです

著者

 Caterina Urban, ETH Zurich, [email protected] 

貢献者

 Naïm Moussaoui Remil, École Normale Supérieure
Samuel Ueltschi, ETH Zurich
Nathanaëlle Courant, École Normale Supérieure

インストール

関数には、次のアプリケーションとライブラリが必要です。

• ocaml

   (sudo) apt-get install ocaml-interp
  

• findlib

   (sudo) apt-get install ocaml-findlib
  

• Menhir：LR（1）パーサージェネレーター

   (sudo) apt-get install menhir
  

• OPAM：https：//opam.ocaml.org/doc/install.html

   (sudo) apt-get install opam
  

• 砂丘：OCAMLビルドシステム

   opam install dune
  

• ounit

   opam install ounit
  

• エプロン：数値抽象ドメインライブラリ

   opam install apron
  

• Zarith：任意の整数整数操作

   opam install zarith
  

コンパイル機能

必要なすべてのライブラリがインストールされると、機能を「砂丘」でコンパイルできます。

 dune build

これにより、プロジェクトディレクトリにコマンドラインプログラム「機能」が生成されます。

または、「ocamlbuild」を使用して、次のコマンドで機能を構築できます。

 ocamlbuild ml_float.o Main.native -use-ocamlfind -use-menhir -pkgs 'apron,gmp,oUnit,zarith' -I utils -I banal -I domains -I frontend -I cfgfrontend -I main -libs boxMPQ,octD,polkaMPQ,str,zarith -lflags banal/ml_float.o

使用法

コマンドラインアナライザーは、次のコールパターンを使用して呼び出すことができます。

 ./function <file> <analysis> [options] 

ここで、「ファイル」は分析するCファイルへのパスであり、実行する分析のタイプを「分析」します。

アナライザーは最初に順方向の到達可能性分析を実行し、次に後方分析を実行して、特定の分析されたプロパティを満たすためのプログラムのエントリポイントで、区分的定義のランキング関数と十分な前提条件を見つけます。

次の一般的なコマンドラインオプションが認識されます（デフォルト値を表示）：

 -main main                         set the analyzer entry point (defaults to main)
 -domain boxes|octagons|polyhedra   set the abstract domain (defaults to boxes)
 -joinfwd 2                         set the widening delay in forward analysis
 -joinbwd 2                         set the widening delay in backward analysis
 -meetbwd 2			                set the dual widening delay in backward analysis
 -ordinals 2                        set the maximum ordinal value for the ranking functions
 -refine            			    reduces the backward analysis to the reachabile states

アナライザーは、プロパティを正常に証明できる場合に備えて真で答えます。そうでなければ、それは不明に答えます。

関数は次のプロパティを分析できます。

• 終了
• 保証 /再発
• Computation-Tree-Logic（CTL）

終了

終了を確認するには、次のコールパターンでアナライザーに電話してください。

 ./function <file> -termination [options]

保証 /再発

次の呼び出しパターンは、保証プロパティまたは再発プロパティに使用できます。

 ./function <file> -guarantee <property_file> [options]
./function <file> -recurrence <property_file> [options] 

ここで、「Property_File」は、保証または再発プロパティを含むファイルへのパスです。

CTL

CTLプロパティは、次のコールパターンを使用して分析できます。

 ./function <file> -ctl <property> [options]

ここで、「プロパティ」は分析されるCTLプロパティです。

CTL分析には、次の追加のコマンドラインオプションが存在します。（デフォルト値を表示）：

 -precondition true                 a precondition that is assumed to hold at the start of the program
 -noinline			                disable inlining of function calls
 -ast                               run the analysis on the abstract-syntax-tree instead of the control-flow-graph,
                                    note that in that case function calls and goto/break/continue are not supported
 -dot                               print out control-flow-graph and decision trees in graphviz dot format