function

Fonction

La fonction est un analyseur statique prototype de recherche conçu pour prouver les propriétés de terminaison conditionnelle et de garantie conditionnelle et de récidive des programmes C. L'outil déduit automatiquement des fonctions de classement définies par morceaux et des conditions préalables suffisantes pour les propriétés de résiliation, de garantie et de récidive au moyen d'une interprétation abstraite.

La fonction a été développée pour mettre en œuvre et tester la méthode d'analyse et les domaines abstraits décrits dans les articles:

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

Le site Web principal de la fonction est: http://www.di.ens.fr/~urban/fonction.html

Auteur

 Caterina Urban, ETH Zurich, [email protected] 

Contributeurs

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

Installation

La fonction nécessite les applications et les bibliothèques suivantes:

• Ocaml

   (sudo) apt-get install ocaml-interp
  

• Finir

   (sudo) apt-get install ocaml-findlib
  

• Menhir: LR (1) générateur d'analyse

   (sudo) apt-get install menhir
  

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

   (sudo) apt-get install opam
  

• Dune: Système de construction OCAML

   opam install dune
  

• Ounit

   opam install ounit
  

• Tablier: bibliothèque de domaine abstrait numérique

   opam install apron
  

• Zarith: opérations entières de précision arbitraire

   opam install zarith
  

Fonction de compilation

Une fois toutes les bibliothèques requises installées, la fonction peut être compilée avec «dune»:

 dune build

Cela générera le programme de ligne de commande «fonction» dans le répertoire du projet.

Alternativement, «OCAMLBUILD» peut être utilisé pour créer une fonction avec la commande suivante:

 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

Usage

L'analyseur de ligne de commande peut être invoqué en utilisant le modèle d'appel suivant:

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

où "fichier" est le chemin du fichier C à analyser et "analyse" le type de l'analyse à effectuer.

L'analyseur effectue d'abord une analyse de réaction avant, puis une analyse en arrière pour trouver une fonction de classement définie par morceaux et des conditions préalables suffisantes au point d'entrée pour le programme pour satisfaire la propriété analysée donnée.

Les options de ligne de commande générales suivantes sont reconnues (affichant leur valeur par défaut):

 -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

L'analyseur répond vrai dans le cas où il pourrait prouver avec succès la propriété. Sinon, il répond inconnu.

La fonction peut analyser les propriétés suivantes:

• Terminaison
• Garantie / récidive
• Calcul-are-logic (CTL)

Terminaison

Pour vérifier la résiliation, appelez l'analyseur avec le modèle d'appel suivant:

 ./function <file> -termination [options]

Garantie / récidive

Le modèle d'appel suivant peut être utilisé pour la garantie des propriétés ou des propriétés de récidive:

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

où "Property_file" est le chemin d'accès au fichier contenant la garantie ou la propriété de récidive.

Ctl

Les propriétés CTL peuvent être analysées à l'aide du modèle d'appel suivant:

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

où "propriété" est la propriété CTL à analyser.

Les options de ligne de commande supplémentaires suivantes existent pour l'analyse CTL: (montrant leur valeur par défaut):

 -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