function

Función

La función es un analizador estático de prototipo de investigación diseñado para probar la terminación condicional y las propiedades de garantía condicional y recurrencia de los programas C. La herramienta infiere automáticamente las funciones de clasificación definidas por partes y las condiciones previas suficientes para las propiedades de terminación, garantía y recurrencia mediante interpretación abstracta.

La función se desarrolló para implementar y probar el método de análisis y los dominios abstractos descritos en los artículos:

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

El sitio web principal de la función es: 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

Instalación

La función requiere las siguientes aplicaciones y bibliotecas:

• Ocaml

   (sudo) apt-get install ocaml-interp
  

• Findlib

   (sudo) apt-get install ocaml-findlib
  

• Menhir: LR (1) Generador de analizador

   (sudo) apt-get install menhir
  

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

   (sudo) apt-get install opam
  

• Dune: sistema de compilación OCAML

   opam install dune
  

• De un ouit

   opam install ounit
  

• Delantal: biblioteca numérica de dominio abstracto

   opam install apron
  

• Zarith: operaciones enteras de precisión arbitraria

   opam install zarith
  

Función de compilación

Una vez que se instalan todas las bibliotecas requeridas, la función se puede compilar con 'Dune':

 dune build

Esto generará la 'función' del programa de línea de comandos en el directorio del proyecto.

Alternativamente, 'OcamlBuild' se puede usar para construir la función con el siguiente 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

El analizador de línea de comandos se puede invocar utilizando el siguiente patrón de llamadas:

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

donde "archivo" es la ruta al archivo c que se analizará y "análisis" el tipo de análisis a realizar.

El analizador primero realiza un análisis de accesibilidad hacia adelante, y luego un análisis hacia atrás para encontrar una función de clasificación definida por partes y condiciones previas suficientes en el punto de entrada para que el programa satisfaga la propiedad analizada dada.

Se reconocen las siguientes opciones de línea de comandos generales (que muestran su valor predeterminado):

 -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

El analizador responde verdadero en caso de que pueda probar con éxito la propiedad. De lo contrario, responde desconocido.

La función puede analizar las siguientes propiedades:

• Terminación
• Garantía / recurrencia
• Cálculo-árbol-logic (CTL)

Terminación

Para verificar la terminación, llame al analizador con el siguiente patrón de llamadas:

 ./function <file> -termination [options]

Garantía / recurrencia

El siguiente patrón de llamadas se puede utilizar para propiedades de garantía o propiedades de recurrencia:

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

donde "Property_File" es la ruta al archivo que contiene la propiedad de garantía o recurrencia.

CTL

Las propiedades de CTL se pueden analizar utilizando el siguiente patrón de llamadas:

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

donde la "propiedad" es la propiedad CTL a analizar.

Existen las siguientes opciones de línea de comandos adicionales para el análisis CTL: (que muestra su valor predeterminado):

 -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