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).

Основной веб -сайт функции: http://www.di.ens.fr/~ururban/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
  

• Унит

   opam install ounit
  

• Фартук: библиотека численной абстрактной домены

   opam install apron
  

• Зарит: целочисленные операции по произвольному назначению

   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

Анализатор отвечает истинно, если он может успешно доказать свойство. В противном случае он отвечает неизвестным.

Функция может проанализировать следующие свойства:

• Завершение
• Гарантия / повторение
• Вычислительный дерево-логик (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