function

Função

A função é um analisador estático de protótipo de pesquisa projetado para provar que a rescisão condicional e as propriedades de garantia condicional e recorrência dos programas C. A ferramenta infere automaticamente funções de classificação definidas por partes e pré-condições suficientes para propriedades de rescisão, garantia e recorrência por meio de interpretação abstrata.

A função foi desenvolvida para implementar e testar o método de análise e os domínios abstratos descritos nos artigos:

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

O site principal da função é: http://www.di.ens.fr/~urban/function.html

Autor

 Caterina Urban, ETH Zurich, [email protected] 

Colaboradores

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

Instalação

A função requer os seguintes aplicativos e bibliotecas:

• OCAML

   (sudo) apt-get install ocaml-interp
  

• FindLib

   (sudo) apt-get install ocaml-findlib
  

• MENHIR: LR (1) Gerador de salvador

   (sudo) apt-get install menhir
  

• Opam: https://opam.ocaml.org/doc/install.html

   (sudo) apt-get install opam
  

• Dune: Sistema de compilação OCAML

   opam install dune
  

• OUNIT

   opam install ounit
  

• Avental: Biblioteca de domínio abstrato numérico

   opam install apron
  

• Zarith: operações inteiras de precisão arbitrária

   opam install zarith
  

Função de compilação

Depois que todas as bibliotecas necessárias forem instaladas, a função pode ser compilada com 'Dune':

 dune build

Isso gerará o programa da linha de comando 'Função' no diretório do projeto.

Como alternativa, o 'ocamlbuild' pode ser usado para construir a função com o seguinte comando:

 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

Uso

O analisador de linha de comando pode ser chamado usando o seguinte padrão de chamada:

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

onde "arquivo" é o caminho para o arquivo C a ser analisado e "análise" o tipo de análise a ser executada.

O analisador realiza primeiro uma análise de acessibilidade avançada e, em seguida, uma análise versária para encontrar uma função de classificação definida por partes e pré-condições suficientes no ponto de entrada para o programa para satisfazer a propriedade analisada especificada.

As seguintes opções de linha de comando geral são reconhecidas (mostrando seu valor padrão):

 -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

O analisador responde verdadeiro caso possa provar com sucesso a propriedade. Caso contrário, responde desconhecido.

A função pode analisar as seguintes propriedades:

• Rescisão
• Garantia / recorrência
• Computação-árvore-lógica (CTL)

Rescisão

Para verificar a rescisão, ligue para o analisador com o seguinte padrão de chamada:

 ./function <file> -termination [options]

Garantia / recorrência

O seguinte padrão de chamada pode ser usado para propriedades de garantia ou propriedades de recorrência:

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

onde "Property_file" é o caminho para o arquivo que contém a propriedade de garantia ou recorrência.

CTL

As propriedades do CTL podem ser analisadas usando o seguinte padrão de chamada:

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

onde "propriedade" é a propriedade CTL a ser analisada.

As seguintes opções de linha de comando seguintes existem para a análise CTL: (mostrando seu valor padrão):

 -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