Modélisation par contraintes du bytecode Java pour la génération de données de test 

Télécharger le fichier pdf d’un mémoire de fin d’études

Description de quelques outils

Cette section décrit quelques outils de génération de tests à base de modèle parmi les très nombreux outils existants.
L’outil industriel Test Designer (anciennement LTG, Leirios Test Generator) se base sur un modèle de test en UML, comportant des diagrammes de classes, des machines à états, des diagrammes d’instances, ainsi que des spécifications en OCL (spécifications sous la forme pre-post), pour définir une modélisation comportementale de l’application à tester. L’utili-sateur indique dans la spécification des cibles de test à couvrir, et l’outil essaie de générer des données de test pour atteindre l’ensemble de ces cibles. Cet outil supporte également une spécification en B [JL07]. L’outil LTG exploitait la programmation par contraintes pour parcourir symboliquement des chemins de la spécification, Test Designer quant à lui exploite des algorithmes de recherche et des prouveurs de théorèmes.
TGV (Test Generation with Verification technology) [JJ04] est un générateur automatique de tests de conformité à partir de spécifications (en Sdl, en Lotos ou en UML) pour les systèmes réactifs. Il prend en entrée une description du comportement d’un protocole et un objectif de test. Il est basé sur le modèle des IOLTS (Input-Output Labelled Transition Systems).
STG (Symbolic Test Generation) [CJRZ02, RdBJ00] est un générateur de tests exploitant des techniques symboliques. Il prend en entrée des spécifications et des objectifs de test symboliques décrits sous la forme d’IOSTS (Input/Output Symbolic Transition System), et génère des cas de test également sous la forme d’IOSTS. Après être traduits en C++ ou Java, les cas de test peuvent être exécutés par une implémentation dans le langage corres-pondant. Les contraintes portant sur les entrées sont résolues à la volée durant l’exécution. Autofocus [SH99, WLPO00] est un outil de spécification graphique pour les systèmes dis-tribués. Il exploite différentes vues du système sous test : la structure du système avec des composants et des canaux, une description du comportement du système incluant ces composants et ces canaux, les données gérées par le système et transmises par les canaux et l’interaction entre les composants et l’environnement via des échanges de messages. Le comportement des composants est spécifié par des automates dont les transitions sont éti-quetées par des pré-conditions et des post-conditions. Autofocus traduit la spécification sous forme de logique propositionnelle et génère automatiquement des séquences de test pour couvrir des objectifs de test (par exemple atteindre un état cible ou provoquer l’exé-cution d’une séquence de transitions).
Le langage Lustre est un langage déclaratif à flots de données synchrones muni d’opérateurs temporels permettant de se référer à des valeurs passées des données. L’outil GATeL [MA00] génère automatiquement des séquences de tests à partir de descriptions Lustre. Il repose sur une interprétation des constructions du langage Lustre sous la forme de contraintes portant sur des variables booléennes ou entières. Pour générer des séquences de test, ces contraintes sont résolues à l’aide de techniques de programmation logique par contraintes.

Test basé sur le code

Prérequis

Remplir un critère de test pour un ensemble de données de test est considéré comme un gage de qualité, et les critères sont souvent utilisés pour guider la génération manuelle ou automatique de tels ensembles. Les critères de test utilisés pour le test basé sur le code se fondent sur le flot de contrôle ou sur le flot des données.

Critères basés sur le flot de contrôle

Une donnée de test décrit quelles valeurs donner aux paramètres de la fonction sous test et en particulier quelle est la forme de la mémoire en entrée. La génération de données de test se fait dans le but de couvrir des éléments spécifiques du graphe de flot de contrôle. Voici quelques uns de ces critères.
– Le critère de couverture de toutes les instructions. La couverture de ce critère est considérée comme étant un minimum à atteindre, un prérequis à toute utilisation du programme.
– Le critère de couverture de toutes les branches. La couverture de toutes les branches garantit la couverture de toutes les instructions.
– Le critère de couverture de tous les chemins. La couverture de tous les chemins garantit la couverture de toutes les branches et de toutes les instructions.
– Le critère de couverture des k-chemins. Comme le nombre de chemins exécutables d’un programme peut être infini, le critère de couverture de tous les chemins est souvent relaxé avec le critère de couverture des k-chemins où seuls les chemins pour lesquels chacune des boucles est dépliée moins de k fois sont à couvrir.

Critères basés sur le flot des données

Pour les critères basés sur le flot des données, les définitions (def ) des variables du programme ainsi que leurs différentes utilisations (p-use dans un prédicat, c-use dans un calcul) sont identifiées. Le test vise alors à couvrir les différentes combinaisons des paires def-use.

Approches orientées chemins et approches orientées but

Pour couvrir un objectif donné, la plupart des approches consistent à essayer de trou-ver un ensemble de chemins exécutables tels que la couverture de chacun de ces chemins par une donnée de test assure la couverture du critère de test considéré. C’est ce que l’on appelle des méthodes orientées chemins. Cet ensemble de chemins peut être sélectionné en amont de la génération des données de test, mais s’il comprend des chemins non exécu-tables, ceux-ci peuvent faire baisser le taux de couverture. Dans les méthodes de génération de données de test actuelles, les chemins qui mènent à la couverture du critère sont le plus souvent choisis au fur et à mesure de la génération, en prenant en compte les informations acquises sur des sous-chemins non exécutables ou sur la structure du graphe de flot de contrôle.
L’approche orientée but fut proposée par Ferguson et Korel [FK96]. Dans cette ap-proche, pour couvrir un objectif qui peut être une branche ou une instruction, aucun chemin n’est choisi a priori.

Exécution symbolique et langages de programmation impératifs ou orientés objet

L’exécution symbolique telle que présentée ci-dessus a été proposée pour des pro-grammes prenant en entrée des variables numériques. Pendant l’exécution symbolique, des manipulations algébriques sont effectuées pour simplifier les expressions symboliques ce qui peut rendre la méthode coûteuse. Outre ce problème de coût, pour pouvoir appliquer ce type de raisonnement à des langages plus complexes, en particulier les programmes orientés objets qui sont l’objet de cet écrit, il faut pouvoir étendre le traitement symbolique à des structures de données complexes.
Les manipulations de tableaux peuvent poser problème pour l’exécution symbolique. Ainsi, une expression de type t[i] telle que la valeur de i dépende des valeurs d’entrée pré-sente des difficultés, car la valeur symbolique à laquelle on accède n’est pas déterminée. Les méthodes usuelles envisagent toutes les possibilités : i=0, i=1, etc. Cela multiplie le nombre de chemins à analyser durant l’exécution symbolique.
Le problème de la détermination de la forme de la mémoire quand le langage permet l’allocation dynamique (problème Mem_shape) pose également de grandes difficultés pour la mise en œuvre de l’exécution symbolique. Ainsi, pour une méthode qui manipule des listes cycliques comme paramètres, le nombre d’objets, et donc de variables d’instance, peut être différent d’une liste à l’autre. Le nombre de variables d’instance n’étant pas connu, on ne sait pas a priori combien de variables symboliques seront nécessaires pour représenter les états des objets.

Méthodes exploitant l’exécution symbolique

Doyle et al. [DM03b, DM03a] proposent une méthode pour générer des données de test pour des programmes en bytecode Java, implantée dans l’outil IBIS. IBIS effectue des exécutions symboliques pour générer des contraintes de chemins résolues par une librairie de contraintes basée sur le simplexe. La méthode proposée ne couvre qu’une partie très restreinte du bytecode Java puisqu’elle ne traite les objets et les appels de méthode qu’à un « degré limité » selon les auteurs, et les exemples détaillés dans les articles décrivant cette méthode ne manipulent que des entiers.
Müller et al. [MLK04] présentent également une méthode pour tester des programmes en bytecode Java. Son objectif est de couvrir différents critères de couverture : couverture des instructions, des branches, et des couples def-use. Pour cela, les chemins du programme sont exécutés symboliquement par une machine virtuelle Java dite symbolique. La méthode est implantée dans l’outil GlassTT, la résolution des conditions de chemin fait appel, selon le type de contraintes à résoudre, à différents solveurs de contraintes, ou encore au système de calcul algébrique Mathematica.
Dans cette méthode, pour couvrir le critère def-use, chacun des couples def-use rencontrés est mémorisé avec la chaîne def-use ayant permis de le sensibiliser. Si le même couple avec la même chaîne est rencontré, alors l’exploration ne se poursuit pas car cela indique qu’une boucle est rencontrée et que la parcourir plusieurs fois n’augmentera pas la couverture. Ce constat paraît discutable en présence de références, mais la méthode ne semble traiter que les types entiers. Cette limitation n’est pas explicite dans les articles mais la gestion des références n’est pas évoquée et les exemples ne présentent que des entiers.

Exécution symbolique et model-checking

Initialisation paresseuse

Kurshid, Pasareanu et Visser proposent de combiner des techniques d’exécution sym-bolique et de model-checking [KPV03, VPK04, PMB+08] pour générer automatiquement des données de test pour la couverture de code en bytecode Java. L’objectif est de pouvoir tester des programmes qui prennent en entrée des structures complexes avec des données non bornées (nombre d’objets en mémoire initialement inconnu par exemple), ainsi que les programmes concurrents pour l’analyse desquels le model-checking est très utilisé. Pour générer des entrées afin de satisfaire un critère de test basé sur le code, par exemple la cou-verture de toutes les instructions, la méthode sous test est exécutée symboliquement pour la vérifier par rapport à des propriétés qui encodent le critère de test. Les contre-exemples pour ces propriétés sont des chemins qui satisfont le critère.
La méthode utilise une généralisation de l’exécution symbolique [KPV03] pour sup-porter les constructions avancées des langages modernes comme Java, en particulier pour traiter le problème de la méconnaissance de la forme de la mémoire en entrée de méthode (problème Mem_shape). Le model-checker permet d’explorer les chemins, et de les exécu-ter symboliquement de la manière suivante. Initialement, les variables d’instance de type référence en entrée de méthode sont non initialisées. Elles le seront au fur et à mesure des besoins lors de l’exécution symbolique, on parle d’initialisation paresseuse. Les variables entières sont symboliques comme pour toute exécution symbolique. Quand l’exécution sym-bolique accède à une variable d’instance référence, l’algorithme initialise de manière aléa-toire cette référence qui : (1) soit vaut null, (2) soit référence un objet symbolique qu’il crée et dont les attributs sont non initialisés, (3) soit référence un objet symbolique déjà créé ayant un type compatible. Le troisième cas permet de générer des situations d’alia-sing. Quand une condition de branchement c portant sur des variables entières est évaluée, l’algorithme choisit une branche de manière non déterministe en ajoutant à la condition de chemin courante soit la condition c, soit la négation de c, et appelle une procédure de décision pour vérifier la satisfiabilité de la condition de chemin. Si la condition de chemin devient contradictoire, l’algorithme revient en arrière (backtrack ) pour choisir une autre branche et donc un autre chemin. Chaque chemin sensibilisé est caractérisé par une confi-guration en entrée du tas, qui encode les contraintes sur les attributs de type référence, et une condition portant sur les variables symboliques entières. La valeur des références non utilisées sur le chemin est fixée à null. L’utilisateur peut fournir des pré-conditions en Java que doivent vérifier les objets créés, y compris ceux qui sont créés lors de l’exploration des chemins.
Les auteurs mettent en œuvre leur méthode via une extension, appelée JPF-SE, au model-checker Java PathFinder pour du bytecode Java [APV07]. Pour vérifier les condi-tions de chemins, plusieurs procédures de décisions peuvent être utilisées (Oméga, CVC-lite, YICES et STP). Dans [VPP06] et [APV09], des abstractions d’états sont utilisées pour comparer l’état cou-rant à des états déjà rencontrés. L’avantage est de réduire l’explosion du nombre d’états, l’inconvénient est d’exclure indûment certains états du parcours à cause de l’abstraction et donc de sous-approximer les comportements du programme.
Des exécutions concrètes peuvent être utilisées pour mettre l’environnement dans un cer-tain état qui sera exploité pour l’exécution symbolique.
Concernant les inconvénients de cette méthode, le nombre de chemins dans un pro-gramme peut être non borné, et le model-checker explore ces chemins selon des heuristiques telles que l’exploration en largeur ou en profondeur, bornée par la taille des chemins et des entrées. Cependant, il ne tient pas compte de la structure du programme pour guider l’ex-ploration, ainsi cette méthode ne permet pas de borner le nombre de dépliage d’une boucle. Les références ne sont pas gérées de manière symbolique, un choix est effectué quand la connaissance de leur valeur est nécessaire, multipliant ainsi le nombre de chemins pouvant être explorés. Augmenter ainsi le nombre de chemins augmente aussi potentiellement le nombre de chemins non exécutables dans le cas où le choix effectué n’est pas compatible avec les conditions qui suivent sur le chemin exploré.
Cette méthode a le mérite de proposer une solution pour couvrir des codes de méthodes prenant en entrée des structures complexes. La satisfiabilité de la condition de chemin est testée au fur et à mesure de sa construction ce qui permet de couper dès que possible l’exploration de l’arbre des exécutions et d’exclure ainsi des chemins non exécutables.

Lazier initialization

Les travaux sur JPF-SE ont inspiré ceux de Deng, Robby et Hatcliff [DRH07]. Ils uti-lisent l’exécution symbolique généralisée proposée dans [KPV03] en l’améliorant afin de retarder davantage le choix non déterministe effectué lors de l’utilisation d’une référence et de réduire ainsi le nombre de chemins à explorer. Ils proposent pour cela la lazier ini-tialization. L’initialisation paresseuse de [KPV03] initialise une variable d’instance de type référence lorsqu’une instruction y accède. Soit o.f une référence, dans l’initialisation pro-posée, la lazier initialization, son initialisation est retardée jusque ce qu’elle soit utilisée pour un accès à un attribut (o.f.g par exemple) ou un test d’égalité (o.f=o’ par exemple). Pour ce faire, un accès à la référence o.f retourne seulement une référence symbolique, de potentiels usages ultérieurs provoqueront l’initialisation de sa valeur en choisissant de ma-nière non déterministe entre un nouvel objet ou un objet déjà présent dans le tas de type compatible. Les références sont donc en partie traitées de manière symbolique, mais des choix non déterministes peuvent encore être nécessaires.
Le fait de retarder l’initialisation limite le nombre de chemins à considérer car le choix non déterministe lié à une référence se fait soit plus tard, soit jamais. Le traitement symbolique des références nécessite de propager en arrière l’information lorsqu’elles sont concrétisées. A l’issue de l’exécution symbolique d’un chemin, un solveur de contraintes est utilisé pour instancier les éléments encore inconnus.
Une borne, k, limite la longueur des chaînes de références, une autre borne limite le dépliage des boucles. L’approche est implantée dans l’outil KUnit, qui exploite l’exécution symbolique de Bogor/Kiasan [DLR06]. Il utilise une procédure de décision (CVC Lite) et un solveur de contraintes. Les éléments manquants du système peuvent être remplacés par des contrats. Comme pour JPF-SE, les pré-conditions portant sur les objets sont exploitées pour la construction des objets. L’objectif affiché de la méthode n’est pas seulement d’atteindre une couverture élevée du code, mais aussi de tester le programme avec des configurations d’entrée variées. Grâce à la borne k, il est possible de garantir que toutes les formes du tas possibles dans la limite de la borne k seront générées pour chacun des chemins explorés. L’un des inconvénients qui en découle est l’importance du nombre d’entrées générées. Ainsi, pour certains exemples présentés, en fixant k =3 plus de mille données de test sont générées.

Représentation symbolique de librairies

Les auteurs de [KS05] partent du constat que les appels aux librairies peuvent être coûteux pour l’exécution symbolique. En effet, les implémentations de librairies représen-tant, par exemple, des ensembles comportent souvent des optimisations qui multiplient le nombre de chemins. Ils proposent d’utiliser une modélisation symbolique des librairies Java Set et Map : les opérations sont modélisées sous forme d’opérations symboliques en se défaisant des détails d’implémentation. Leur méthode est implantée dans l’outil Dianju, basé sur (l’ancêtre de) JPF-SE.

Exécution symbolique dynamique

L’exécution symbolique dynamique, ou exécution concolique, associe exécution concrète du programme et exécution symbolique afin d’explorer les chemins du programme. L’exé- cution concrète dans ce cadre sert à guider l’exploration des chemins du graphe de flot de contrôle, et parfois à aider l’exécution symbolique en approximant la valeur d’expres-sions complexes telles que les expressions non linéaires. Différentes méthodes exploitent l’exécution symbolique dynamique pour la génération de données de test, pour tester des programmes en C [WMMR05, GKS05, God07, SMA05], des programmes en bytecode Java [SA06], des programmes dans le langage intermédiaire du .NET [TdH08, TS06] et des exécu-tables [BH08]. Certaines méthodes [GKS05, God07, SMA05, SA06, BH08] sont cependant plus spécialisées dans la recherche de bugs, elles essaient de mettre en évidence des erreurs d’exécution ou des failles de sécurité.

Tests paramétrés

Tillmann, de Halleux et Schulte proposent également une méthode de génération de données de test basée sur l’exécution symbolique dynamique [TdH08, TS06]. Leur méthode est implantée dans Pex, un outil développé par Microsoft pour générer des données de test couvrant les branches, ou encore mettant en évidence des erreurs d’exécution ou des failles de sécurité. Il supporte de très nombreuses fonctionnalités des programmes en bytecode .NET (hormis le non-déterminisme, la concurrence, le code natif et les flottants), peut être intégré à Visual Studio pour le langage C#, et il génère les scripts de test permettant d’exé-cuter des séquences d’appels pour créer les objets et les placer dans l’état désiré. Il rapporte un taux de couverture des branches qui est dit « dynamique » : il s’agit du taux de couver-ture des branches explorées, qui peut être distinct du taux de couverture des branches du graphe de flot de contrôle ; en particulier si l’outil ne parvient pas à générer des entrées pour un préfixe exécutable, tous les chemins débutant par ce préfixe sont exclus de l’exploration.
La méthode de génération utilisée par Pex exploite l’exécution symbolique dynamique pour parcourir le graphe de flot de contrôle en cherchant à couvrir au plus tôt toutes les branches. De multiples paramètres permettent de borner l’exploration : bornes sur le nombre d’exécutions, sur la longueur des chemins, sur le nombre de branches pour un chemin, sur le temps imparti à la génération, sur le temps imparti au solveur, sur le nombre de conditions portant sur les entrées pour un chemin, sur la taille de la pile, sur la taille de la mémoire, etc.
Pour la résolution des conditions de chemin, le solveur SMT Z3 [dMB08] est utilisé. Comme dans les méthodes utilisées dans DART, SMART, Cute et JCute, l’aspect dynamique de l’approche est exploitée pour approximer certaines expressions symboliques complexes par des valeurs concrètes, par exemple pour les accès aux tableaux via des indices variables. Le nombre de comportements du programme pris en compte peut s’en trouver réduit.
Concernant le traitement des références et des alias, le modèle mémoire utilisé par Pex n’étant pas décrit précisément, il est difficile de savoir si la concrétisation est utilisée pour les références, et si oui dans quels cas : cela n’est à notre connaissance pas renseigné, ni dans les articles, ni dans la documentation de l’outil. Les expériences montrent qu’il ne permet pas de résoudre certaines conditions de chemins impliquant des relations entre les références (et par conséquent des structures de données) complexes.
Dans le cas où un paramètre a un type interface (classe abstraite) ou si une classe n’est pas encore développée, Pex permet à l’utilisateur d’utiliser des « mock objects » pour simuler le comportement attendu d’un objet. Cette approche peut réduire le nombre de chemins dans les méthodes appelées, de manière similaire à l’approche de PathCrawler.

Test de code exécutable

Bardin et Herrmann proposent une méthode pour générer des données de test pour du code exécutable [BH08], ce qui présente plusieurs avantages par rapport au test de code source. D’une part des programmes dont le code source n’est pas disponible (sous-traitance, appels à des librairies) peuvent être testés. D’autre part, quand la vérification est faite au niveau du code source, il faudrait assurer que la compilation conserve la sémantique ce qui est parfois difficile quand le compilateur utilise des optimisations. Tester directement le code binaire assure que l’on teste ce qui sera réellement exécuté, mais travailler au niveau du binaire est plus difficile (pas de types, pas de flot de contrôle, . . . ).
La méthode proposée utilise uniquement le code de l’exécutable (pas de spécifications) pour générer des données de test afin de couvrir les critères de couverture de toutes les branches ou toutes les instructions. L’architecture et l’ensemble d’instructions utilisées dans les exécutables sont très dépendants du système, l’approche présentée se veut générique pour s’adapter à plusieurs processeurs.
La structure du programme peut partiellement être retrouvée statiquement à partir du code binaire. Puis l’exécution symbolique dynamique permet de découvrir davantage de branchements, liés aux sauts dynamiques (des sauts dont l’adresse de l’instruction cible est une variable, par exemple goto x où la valeur de x est seulement connue à l’exécution). Cependant, il n’est pas garanti que l’intégralité de la structure du graphe de flot de contrôle puisse être retrouvée, la couverture peut donc être incomplète.
Le parcours des chemins se fait en profondeur d’abord et de manière bornée. Les conditions de chemins sont exprimées avec des contraintes sur des vecteurs de bits : les vecteurs de bits facilitent la formalisation des instructions standards des machines au niveau des bits (opérations bit à bit par exemple), et la flexibilité de la programmation par contraintes permet d’encoder toutes les instructions rencontrées.
Concernant les alias, n’ayant pas accès à des informations de haut niveau, les rela-tions d’alias de l’exécution concrète sont extraites et ajoutées aux prédicats de chemin. Cependant, comme dans le cas des méthodes utilisées dans les outils Cute et Pex, cette sous-approximation des comportements peut rendre le prédicat de chemin insatisfiable alors que le chemin est exécutable. Pour atténuer cet inconvénient, différentes alternatives pour les alias sont énumérées en relaxant certaines contraintes.

Méthode de Cadar et al.

Cadar et al. [CGP+06, CGP+08] proposent une méthode de génération de données de test pour couvrir les chemins et détecter un maximum d’erreurs d’exécution (par exemple les divisions par zéro) pour les programmes C. Elle exploite elle aussi une complémentarité entre exécution symbolique et exécution concrète du programme, mais pas de la même ma-nière que les autres méthodes détaillées précédemment puisque l’utilisateur indique quelles zones de mémoire traiter symboliquement, les autres zones de mémoire étant traitées avec leur valeur concrète.
Les chemins sont explorés exhaustivement selon une heuristique qui choisit en priorité des chemins couvrant des instructions non encore atteintes. L’exécution symbolique portant sur les zones de mémoire à traiter symboliquement débute par le point d’entrée du pro-gramme. Quand une expression conditionnelle est symboliquement exécutée, un fork est effectué afin qu’il y ait un processus pour le cas où l’expression est vraie et un autre pour le cas où elle est fausse. De ce mécanisme de création de processus résulte un processus par chemin. La priorité donnée à chacun des processus détermine dans quel ordre sont parcourus les chemins.
L’approche est implantée dans l’outil EXE. Quand une erreur d’exécution peut être pro-duite ou quand l’exécution symbolique est achevée, la résolution des contraintes de chemins s’effectue dans cet outil à l’aide d’un solveur de contraintes dédié, STP, qui est une pro-cédure de décision sur les vecteurs de bits et les tableaux. En effet, la mémoire est vue comme un tableau de bits. STP implante toutes les opérations arithmétiques sur les en-tiers et les booléens, y compris les opérations non linéaires. Les instructions n’impliquant que des opérandes concrets sont exécutées concrètement.
La méthode ne traite les pointeurs que partiellement puisqu’elle ne gère pas le double déréférencement symboliquement. En présence d’un double déréférencement **p, la première déréférence *p prend une valeur concrète parmi ses valeurs possibles.
L’utilisation d’une duplication des processus est intéressante dans le cas où une paral-lélisation est possible (grille de calcul par exemple). Contrairement aux autres méthodes utilisant l’exécution symbolique dynamique, cette approche ne cherche pas à détecter dès que possible les préfixes de chemin non exécutables. En effet, la résolution des contraintes n’est lancée que lorsqu’un chemin complet est parcouru. Cela peut ralentir considérable-ment le parcours des chemins en présence de chemins partageant le même préfixe de chemin non exécutable.

Approche orientée but

Méthode de génération de tests pour le C et C++

Dans [GBR98, GBW06], une méthode de génération de tests pour le C et C++ est pro-posée. Elle prend comme objectif de test un élément du code source du programme sous test (instruction, branche) et essaie de générer une donnée de test pour couvrir cet élément. L’approche est orientée but, c’est-à-dire que pour couvrir une instruction elle ne fait pas le choix a priori d’un chemin particulier. Ainsi, elle ne borne ni le nombre de dépliages des boucles, ni la longueur des chemins contrairement aux autres approches, elle permet donc potentiellement d’atteindre des instructions que les autres approches ne couvrent pas ou difficilement à cause de ces bornes. Cette méthode gère les programmes avec des pointeurs [GDB05], des allocations dynamiques [CBG09] et des nombres flottants [BGM06].
La méthode est implantée dans un outil, InKa, dont le fonctionnement est le suivant. Le programme C ou C++ à tester est d’abord traduit dans un langage intermédiaire. Cette normalisation divise des instructions complexes pour obtenir des instructions plus simples, grâce à l’introduction de variables temporaires. La normalisation permet aussi de rendre explicites des opérations implicites, comme les conversions de type et les surcharges. Puis ces instructions du langage intermédiaire sont interprétées pour générer un système de contraintes. L’obligation d’atteindre l’instruction souhaitée est également traduite sous forme de contraintes ajoutées au système. La résolution du système de contraintes est lan-cée. Si InKa détermine que le système de contraintes a des solutions, il retourne une donnée de test permettant d’atteindre l’instruction sélectionnée. S’il détermine que le système de contraintes n’a pas de solution, l’instruction à atteindre est inaccessible (code mort). Si la résolution du système de contraintes excède un temps fixé, la résolution du système s’arrête sans que l’outil ne puisse ni fournir une donnée de test, ni affirmer que l’instruction du programme à atteindre est inaccessible. InKa utilise le solveur de contraintes clp(fd) de SICStus prolog pour les entiers et son propre solveur pour les autres contraintes.
Des relations entre états mémoires Dans l’approche proposée, toutes les instructions C et C++ sont traitées comme des relations entre deux états mémoires, un état mémoire étant une représentation abstraite de la mémoire physique en un point de l’exécution. Les contraintes générées par interprétation d’une instruction FINOP traduisent les liens entre la mémoire physique avant instruction et la mémoire physique après instruction, sous forme d’une relation entre ces états mémoires. Si de l’information est acquise sur la mémoire en entrée, les contraintes liant les mémoires en entrée et en sortie permettront de faire des déductions sur la mémoire en sortie, et inversement.
Gestion des structures de contrôle Les structures de contrôle telles que le if-then-else et le while sont gérées par des opérateurs spécifiques. Seul le cas du if-then-else est détaillé ici, les autres opérateurs s’appuyant sur des principes similaires.
Une instruction de contrôle if-then-else est traitée par un opérateur nommé ite/3. Soit c la contrainte traduisant la conditionnelle sur laquelle porte le if, Cthen la conjonction des contraintes obtenues en interprétant les instructions du corps du then et Celse la conjonc-tion des contraintes obtenues en interprétant les instructions du corps du else. Lorsque la contrainte ite(c,Cthen,Celse) devient active, l’évaluation de la contrainte consiste à déter-miner par quelle branche il faut passer. La branche par laquelle il faut passer peut être
imposée par l’objectif. Si cela n’est pas le cas, il faut essayer de prouver que (c ∧ Cthen) ou (¬c ∧ Celse) est incompatible avec le système de contraintes, prouvant ainsi respectivement qu’il ne faut pas passer par la branche then ou par la branche else mais par l’autre branche et écartant de la sorte une branche du processus de génération. Si aucune branche n’est écartée, la mémoire en entrée (respectivement en sortie) de la structure de contrôle est une union disjonctive des états mémoires en entrée (respectivement en sortie) de chacune des branches, et l’opérateur ite est suspendu, c’est-à-dire qu’il pourra être de nouveau utilisé pour tenter d’éliminer une branche quand davantage d’information sera acquise sur les mémoires en entrée ou en sortie.

Vérification de programmes C critiques

Une autre approche à base de contraintes [Got09] a également été proposée pour vé-rifier des programmes C critiques. Elle permet non seulement générer des données de test pour atteindre un élément d’un code, mais aussi de vérifier des propriétés de sécurité ou de générer des contre-exemples qui les invalident. Cependant comme ces problèmes sont indé-cidables dans le cas général, la procédure est semi-correcte. La méthode présentée permet de générer une donnée de test pour atteindre un point particulier du programme ou indique qu’il n’est pas atteignable. Dans le cadre de la vérification, l’utilisateur peut ajouter des propriétés de sécurité qui peuvent être données sous la forme de pre et post conditions ou sous la forme d’assertions directement dans le code.
Cette méthode est orientée but et reprend des principes proposés dans [GBR98, GBW06], en particulier les opérateurs à contraintes pour les structures de contrôle. Les pointeurs vers des zones nommées sont traités grâce à une analyse de points-to.
La détection de la non satisfiabilité d’un système de contraintes, nécessaire pour réfuter des branches non exécutables, est améliorée par l’utilisation de relaxations linéaires dyna-miques [DGD07b]. En effet, les techniques de programmation linéaire telles que le simplexe peuvent résoudre des problèmes linéaires très efficacement. La relaxation linéaire pour cette approche peut être vue comme une manière de sur-approximer par des contraintes linéaires les relations maintenues par le système de contraintes généré. En particulier le traitement des boucles est rendue plus efficace par des relaxations linéaires spécifiques basées sur un raisonnement par cas et des techniques d’interprétation abstraite [DGD07a].
Cette méthode est implantée dans un outil, Euclide, qui a été utilisé pour vérifier une version préliminaire d’un composant critique du TCAS (un système d’aide à la décision pour les pilotes d’avions) [Got09].

Table des matières

Introduction
I Contexte et état de l’Art 
1 Test des programmes 
1.1 Test basé sur le modèle
1.1.1 Une taxonomie du test à base de modèle
1.1.2 Description de quelques outils
1.2 Test basé sur le code
1.2.1 Prérequis
1.2.2 Exécution symbolique
1.2.3 Exécution symbolique et langages de programmation impératifs ou orientés objet .
1.2.4 Méthodes exploitant l’exécution symbolique
1.2.5 Exécution symbolique et model-checking
1.2.6 Exécution symbolique dynamique
1.2.7 Approche orientée but
1.2.8 Bilan .
2 Mécanismes de la programmation par contraintes 
2.1 Problème de satisfaction de contraintes sur des domaines finis
2.2 Résolution d’un système de contraintes sur des domaines finis
2.2.1 Propagation de contraintes
2.2.2 Énumération des variables
II Modélisation par contraintes du bytecode Java pour la génération de données de test 
3 Intérêt et aperçu du modèle à contraintes d’une JVM 
3.1 Rappel des contributions
3.2 Intérêt du modèle
3.3 Aperçu du modèle
3.3.1 Exemple détaillé
3.3.2 Aperçu des EMC et des relations qui les lient
3.4 Difficultés principales pour la modélisation
3.4.1 Détermination de la forme de la mémoire
3.4.2 Héritage et polymorphisme
4 Modèle mémoire d’une JVM 
4.1 Description d’une JVM
4.1.1 Type des données manipulées par une JVM
4.1.2 Description des zones de stockage des données d’une JVM
4.1.3 Définition d’un état de la mémoire
4.2 Notre modèle mémoire d’une JVM
4.2.1 Modélisation des registres et de la pile d’opérandes
4.2.2 Modélisation du tas et des objets
4.2.3 Modélisation des variables de type primitif ou référence
4.2.4 Etat mémoire sous contraintes (EMC)
5 Modélisation des instructions 
5.1 Remarques préliminaires sur la modélisation proposée
5.1.1 Une sémantique sans erreurs
5.1.2 Instructions modélisées
5.1.3 Informations sur la présentation de la modélisation
5.2 Contraintes portant sur les VTPR
5.2.1 Contraintes portant sur les entiers
5.2.2 Contraintes portant sur les références
5.2.3 Notation de la contrainte d’égalité
5.3 Traduction des instructions en contraintes
5.3.1 Principe de l’interprétation en contraintes
5.3.2 Instructions d’une JVM et informations de type
5.3.3 Instructions d’accès aux registres et de modification des registres
5.3.4 Instructions de manipulation de la pile
5.3.5 Instructions arithmétiques
5.3.6 Instructions de branchement conditionnel
5.3.7 Instructions de manipulation d’instances de classe
5.3.8 Appels de méthodes et de constructeurs
6 Génération de données de test 
6.1 Un parcours de graphe en arrière et incrémental
6.1.1 Le choix d’un parcours en arrière
6.1.2 Un parcours incrémental
6.1.3 Stratégies pour le parcours de graphe
6.2 Enumération de la mémoire d’entrée
6.3 Correction et complétude de la méthode de génération
7 Comparaison de notre approche avec l’état de l’Art 
7.1 Comparaison avec les approches exploitant le model-checking et l’exécution symbolique .
7.2 Comparaison avec les méthodes basées sur l’exécution symbolique dynamique
7.3 Comparaison avec l’approche orientée but
III Validation expérimentale 
8 Description de l’outil JAUT 
8.1 Principe de fonctionnement
8.2 Architecture détaillée
9 Validation expérimentale 
9.1 Programmes avec arithmétique
9.1.1 Programme trityp
9.1.2 Programme avec boucle
9.2 Programmes avec structures de données
9.2.1 Listes doublement chaînées
9.2.2 Arbres colorés
9.3 Limitation du parcours de graphe
9.3.1 Josephus_m
9.4 Conclusion sur la validation de l’approche
IV Conclusion et perspectives 
10 Conclusion 
11 Perspectives 
11.1 Améliorer le parcours du graphe de flot de contrôle
11.2 Étendre le langage traité
11.2.1 Gestion des nombres flottants
11.2.2 Traitement des tableaux
11.2.3 Autres extensions
11.3 Génération de séquences d’initialisation
11.4 Prendre en compte des spécifications
11.5 Améliorer le traitement des appels de méthode
11.6 Étendre l’approche pour couvrir d’autres critères
11.7 Rendre les opérateurs à contraintes sur le tas plus déductifs en enrichissant le modèle mémoire
11.8 Exploiter le modèle de mémoire dans une approche orientée but
Annexe A 
Annexe B 
Bibliographie 

Télécharger le rapport complet