DOC.md

Projet TAS - Documentation

Nous décrivons succinctement les fichiers et répertoires principaux du projet, la syntaxe du langage d'entrée et les options d'analyse.

Architecture du projet

L’arborescence des sources est la suivante :

• Makefile : compilation de l’analyseur, à modifier au fur et à mesure que vous ajoutez des sources ;
• src/main.ml : point d’entrée de l'analyseur, à modifier pour ajouter des nouvelles analyses et options ;
• src/libs/ : contient une version légèrement améliorée du module Map d’OCaml ;
• src/frontend/ : transformation du source (texte) en arbre syntaxique ;
• src/frontend/abstract_syntax_tree.ml : type des arbres syntaxiques abstraits (AST) ;
• src/frontend/lexer.mll : analyseur lexical OCamlLex ;
• src/frontend/parser.mly : analyseur syntaxique Menhir ;
• src/frontend/file_parser.ml : point d’entrée pour la transformation du source en AST ;
• src/frontend/abstract_syntax_printer.ml : affichage d’un AST sous forme de sources ;
• src/domains/ : domaines d’interprétation de la sémantique ;
• src/domains/domain.ml : signature des domaines représentant des ensembles d’environnements ;
• src/domains/concrete_domain.ml : domaine concret de la sémantique collectrice ;
• src/domains/value_domain.ml : signature des domaines représentant des ensembles d’entiers ;
• src/domains/constant_domain.ml : exemple de domaine d’ensembles d’entiers, le domaine des constantes ;
• src/domains/non_relational_domain.ml : foncteur qui crée un domaine d'environnements en associant à chaque variable une valeur de domaine d'entier ;
• src/interpreter/interpreter.ml : interprète générique des programmes paramétré par un domaine d’environnements ;
• tests/ : ensemble de programmes dans le langage analysé pour tester votre analyseur.

Langage

Nous décrivons succinctement les traits du langage d'entrée de l'analyseur :

• les tests :

if (bexpr) { block }
if (bexpr) { block } else { block }

• les boucles :

while (bexpr) { block }

• les affectations :

var = expr

• l'affichage de la valeur des variables précisées :

print(var1,...,varn)

• l'affichage de l'environnement complet (toutes les variables) :

print_all

• l'arrêt du programme :

halt

• les assertions, qui arrêtent le programme sur un message d’erreur si la condition booléenne n'est pas vérifiée :

assert(bexpr)

• les expressions entières expr sont composées des opérateurs classiques +, -, *, /, des variables, des constantes, plus une opération particulière, rand (l,h), où l et h sont deux entiers, et qui représente l’ensemble des entiers entre l et h ;
• les expressions booléennes bexpr utilisées dans les tests et les boucles, sont composées des opérateurs &&, ||, !, des constantes true et false, et de la comparaison de deux expressions entières grâce aux opérateurs <, <=, >, >=, ==, != ;
• les blocs sont composés d’une suite de déclarations de variables, suivie d’une suite d’instructions :

{ decl1; ...; declN; stat1; ...; statM; }

Seul le type int est reconnu, et les déclarations n’ont pas d’initialisation (il faut faire suivre d’une affectation). Une déclaration ne déclare qu'une variable à la fois (int a; int b; est possible, mais pas int a,b;). Dans un bloc, toutes les déclarations doivent précéder toutes les instructions.

Un exemple simple de programme valide est :

{
  int x;
  x = 2 + 2;
  print(x);
}

Pour plus d'informations sur la syntaxe, vous pouvez consulter le fichier d'analyse syntaxique src/frontend/parser.mly. Vous trouverez également des exemples de programmes dans le répertoire tests/.

Options de l'analyseur

Quelques options sont disponibles en ligne de commande, à vous d'en ajouter :

1. -concrete indique qu'il faut exécuter le programme dans la sémantique concrète collectrice ;
2. -trace permet de suivre le déroulement des calculs en affichant l'environnement après l'exécution de chaque instruction.
3. -nonreldebug permet d'afficher des informations de debugs sur l'utilisation du domaine de valeurs données en argument au foncteur Non_relational.