Méthodes d’estimation d’un projet Informatique

Automatisation du Test Logiciel Hatem Ben Sta 2 ING-IDL 2019-2020 Test Logiciel 1/ 129 Introduction Automatisation de la g´en´eration de tests Crit`eres de test avanc´es Test Logiciel 2/ 129 Contexte D´efinition du test Aspects pratiques Discussion Test Logiciel 3/ 129 Coˆut des bugs Coˆuts ´economique : 64 milliards $/an rien qu’aux US (2002) Coˆuts humains, environnementaux, etc. N´ecessit´e d’assurer la qualit´e des logiciels Domains critiques atteindre le (tr`es haut) niveau de qualit´e impos´ee par les lois/normes/assurances/... (ex : DO-178B pour aviation) Autres domaines atteindre le rapport qualit´e/prix jug´e optimal (c.f. attentes du client) Test Logiciel 4/ 129 Validation et V´erification (V & V) V´erification : est-ce que le logiciel fonctionne correctement ? - “are we building the product right ?” Validation : est-ce que le logiciel fait ce que le client veut ? - “are we building the right product ?” Quelles m´ethodes ? revues simulation/ animation tests m´ethode de loin la plus utilis´ee m´ethodes formelles encore tr`es confidentielles, mˆeme en syst. critiques Coˆut de la V & V 10 milliards $/an en tests rien qu’aux US plus de 50% du d´eveloppement d’un logiciel critique (parfois - 90%) en moyenne 30% du d´eveloppement d’un logiciel standard Test Logiciel 5/ 129 La v´erification est une part cruciale du d´eveloppement Le test est de loin la m´ethode la plus utilis´ee Les m´ethodes manuelles de test passent tr es mal a l’´echelle en terme de taille de code / niveau d’exigence fort besoin d’automatisation Test Logiciel 6/ 129 Contexte D´efinition du test Aspects pratiques Discussion Test Logiciel 7/ 129 Le test est une m´ethode dynamique visant `a trouver des bugs Tester, c’est ex´ecuter le programme dans l’intention d’y trouver des anomalies ou des d´efauts - G. J. Myers (The Art of Software Testing, 1979) Test Logiciel 8/ 129 Process (1 seul test) 1 choisir un cas de tests (CT) = sc´enario `a ex´ecuter 2 estimer le r´esultat attendu du CT (Oracle) 3 d´eterminer (1) une donn´ee de test (DT) suivant le CT, et (2) son oracle concret (concr´etisation) 4 ex´ecuter le programme sur la DT (script de test) 5 comparer le r´esultat obtenu au r´esultat attendu (verdict : pass/fail) Script de Test : code / script qui lance le programme `a tester sur le DT choisi, observe les r´esultats, calcule le verdict Suite / Jeu de tests : ensemble de cas de tests Test Logiciel 9/ 129 Sp´ecification : tri de tableaux d’entiers + enl`ever la redondance Interface : int[] my-sort (int[] vec) Quelques cas de tests (CT) et leurs oracles : CT1 tableau d’entiers non redondants le tableau tri´e CT2 tableau vide le tableau vide CT3 tableau avec 2 entiers redondants tri´e sans redondance Concr´etisation : DT et r´esultat attendu DT1 vec = [5,3,15] res = [3,5,15] DT2 vec = [] res = [] DT3 vec = [10,20,30,5,30,0] res = [0,5,10,20,30] Test Logiciel 10/ 129 Script de test 1 void t e s t S u i t e () { 2 3 i n t [ ] td1 = [ 5, 3, 1 5 ] ; /∗ prepa re data ∗/ 4 i n t [ ] - r a c l e 1 = [ 3, 5, 1 5 ] ; /∗ prepa re - r a c l e ∗/ 5 i n t [ ] res 1 = my−s o r t ( td1 ) ; /∗ run CT and ∗/ 6 /∗ obs erv e r e s u l t ∗/ 7 i f ( array −compare ( res1, - r a c l e 1 )) /∗ a s s e s s v a l i d i t y ∗/ 8 then p r i n t ( ‘ ‘ t e s t 1 ok ’ ’ ) 9 e l s e { p r i n t ( ‘ ‘ t e s t 1 e r r e u r ’ ’ ) } ; 10 11 12 i n t [ ] td2 = [ ] ; /∗ prepa re data ∗/ 13 i n t [ ] - r a c l e 2 = [ ] ; /∗ prepa re - r a c l e ∗/ 14 i n t [ ] res 2 = my−s o r t ( td2 ) ; 15 i f ( array −compare ( res2, - r a c l e 2 )) /∗ a s s e s s v a l i d i t y ∗/ 16 then p r i n t ( ‘ ‘ t e s t 2 ok ’ ’ ) 17 e l s e { p r i n t ( ‘ ‘ t e s t 2 e r r e u r ’ ’ ) } ; 18 19 20 . . . /∗ same f o r TD3 ∗/ 21 22 23 } Test Logiciel 11/ 129 Le test ne peut pas prouver au sens formel la validit´e d’un programme Testing can only reveal the presence of errors but never their absence. - E. W. Dijkstra (Notes on Structured Programming, 1972) Par contre, le test peut “augmenter notre confiance” dans le bon fonctionnement d’un programme correspond au niveau de validation des syst`emes non informatiques Un bon jeu de tests doit donc : exercer un maximum de “comportements diff´erents” du programme (notion de crit`eres de test) notamment - tests nominaux : cas de fonctionnement les plus fr´equents - tests de robustesse : cas limites / d´elicats Test Logiciel 12/ 129 1- Contribuer `a assurer la qualit´e du produit lors de la phase de conception / codage en partie par les d´eveloppeurs (tests unitaires) but = trouver rapidement le plus de bugs possibles (avant la commercialisation) - test r´eussi = un test qui trouve un bug 2- Validation : D´emontrer la qualit´e `a un tiers une fois le produit termin´e id´ealement : par une ´equipe d´edi´ee but = convaincre (organismes de certification, hi´erarchie, client - Xtrem programming) - test r´eussi = un test qui passe sans probl`eme - + tests jug´es repr´esentatifs (syst`emes critiques : audit du jeu de tests) Test Logiciel 13/ 129 Crit`ere de tests boite blanche / boite noire / probabiliste Phase du processus de test test unitaire, d’int´egration, syst`eme, acceptation, regression Test Logiciel 14/ 129 Tests unitaire : tester les diff´erents modules en isolation d´efinition non stricte de “module unitaire” (proc´edures, classes, packages, composants, etc.) uniquement test de correction fonctionnelle Tests d’int´egration : tester le bon comportement lors de la composition des modules uniquement test de correction fonctionnelle Tests syst`eme / de conformit´e : valider l’ad´equation du code aux sp´ecifications on teste aussi toutes les caract´eristiques ´emergentes s´ecurit´e, performances, etc. Tests de validation / acceptance : valider l’ad´equation aux besoins du client souvent similaire au test syst`eme, mais r´ealiser / v´erifier par le client Tests de r´egression : v´erifier que les corrections / ´evolutions du code n’ont pas introduits de bugs Test Logiciel 15/ 129 Test Logiciel 16/ 129 Boˆıte Noire : `a partir de sp´ecifications dossier de conception interfaces des fonctions / modules mod`ele formel ou semi-formel Boˆıte Blanche : `a partir du code Probabiliste : domaines des entr´ees + arguments statistiques Test Logiciel 17/ 129 Ne n´ecesite pas de connaˆıtre la structure interne du syst`eme Bas´e sur la sp´ecification de l’interface du syst`eme et de ses fonctionnalit´es : taille raisonnable Permet d’assurer la conformance sp´ec - code, mais aveugle aux d´efauts fins de programmation Pas trop de probl eme d’oracle pour le CT, mais probl eme de la concr´etisation Appropri´e pour le test du syst`eme mais ´egalement pour le test unitaire Test Logiciel 18/ 129 La structure interne du syst`eme doˆıt ˆetre accessible Se base sur le code : tr`es pr´ecis, mais plus “gros” que les sp´ecifications Cons´equences : DT potentiellement plus fines, mais tr`es nombreuses Pas de probl eme de concr´etisation, mais probl eme de l’oracle Sensible aux d´efauts fins de programmation, mais aveugle aux fonctionnalit´es absentes Test Logiciel 19/ 129 Les donn´ees sont choisies dans leur domaine selon une loi statistique loi uniforme (test al´eatoire ) loi statistique du profil op´erationnel (test statistique) Pros/Cons du test al´eatoire s´election ais´ee des DT en g´en´eral test massif si oracle (partiel) automatis´e “objectivit´e” des DT (pas de biais) PB : peine a produire des comportements tr es particuliers (ex : x=y sur 32 bits) Pros/Cons du test statistique permet de d´eduire une garantie statistique sur le programme trouve les d´efauts les plus probables : d´efauts mineurs ? PB : difficile d’avoir la loi statistique Test Logiciel 20/ 129 Contexte D´efinition du test Aspects pratiques Discussion Test Logiciel 21/ 129 La d´efinition de l’oracle est un probl eme tr es difficile limite fortement certaines m´ethodes de test (ex : probabiliste, BN) impose un trade-off avec la s´election de tests point le plus mal maitris´e pour l’automatisation Test Logiciel 22/ 129 Quelques cas pratiques d’oracles parfaits automatisables comparer `a une r´ef´erence : logiciel existant, tables de r´esultats r´esultat simple `a v´erifier (ex : solution d’une ´equation) disponibilit´e d’un logiciel similaire : test dos `a dos Des oracles partiels mais automatis´es peuvent ˆetre utiles oracle le plus basique : le programme ne plante pas instrumentation du code (assert) plus ´evolu´e : programmation avec contrats (Eiffel, Jml pour Java) Test Logiciel 23/ 129 Composition du script de test pr´eambule : am`ene le programme dans la configuration voulue pour le test (ex : initialisation de BD, suite d’´emissions / r´eceptions de messages, etc.) corps : appel des “stimuli” test´es (ex : fonctions et DT) identification : op´erations d’observations pour faciliter / permettre le travail de l’oracle (ex : log des actions, valeurs de variables globales, etc.) postambule : retour vers un ´etat initial pour enchainer les tests Le script doit souvent inclure de la glue avec le reste du code bouchon : simule les fonctions appel´ees mais pas encore ´ecrites Test Logiciel 24/ 129 Quelques exemples de probl`emes Code manquant (test incr´emental) Ex´ecution d’un test tr`es coˆuteuse en temps Hardware r´eel non disponible, ou peu disponible Pr´esence d’un environnement (r´eseau, Base de Donn´ees, machine, etc.) comment le prendre en compte ? (´emulation ?) R´einitialisation possible du syst`eme ? si non, l’ordre des tests est tr`es important Forme du script et moyens d’action sur le programme ? sources dispo, compilables et instrumentables : cas facile, script = code si non : difficile, “script de test” = succession d’op´erations (manuelles ?) sur l’interface disponible (informatique ? ´electronique ? m´ecanique ?) Test Logiciel 25/ 129 Message : code “desktop” sans environnement : facile code embarqu´e temps r´eel peut poser de s´erieux probl`emes, solutions ad hoc Test Logiciel 26/ 129 Tests de r´egression : `a chaque fois que le logiciel est modifi´e, s’assurer que “ce qui fonctionnait avant fonctionne toujours” Pourquoi modifier le code d´ej`a test´e ? correction de d´efaut ajout de fonctionnalit´es Quand ? en phase de maintenance / ´evolution ou durant le d´eveloppement Quels types de tests ? tous : unitaires, int´egration, syst`eme, etc. Objectif : avoir une m´ethode automatique pour rejouer automatiquement les tests d´etecter les tests dont les scripts ne sont plus (syntaxiquement) corrects Test Logiciel 27/ 129 Junit pour Java : id´ee principale = tests ´ecrits en Java simplifie l’ex´ecution et le rejeu des tests (juste tout relancer) simplifie la d´etection d’une partie des tests non `a jour : tests recompil´es en mˆeme temps que le programme simplifie le stockage et la r´eutilisation des tests ( tests de MyClass dans MyClassTest) JUnit offre : des primitives pour cr´eer un test (assertions) des primitives pour g´erer des suites de tests des facilit´es pour l’ex´ecution des tests statistiques sur l’ex´ecution des tests interface graphique pour la couverture des tests points d’extensions pour des situations sp´ecifiques Solution tr`es simple et extrˆemement efficace Test Logiciel 28/ 129 Probl`emes de la s´election de tests : efficacit´e du test d´epend crucialement de la qualit´e des CT/DT ne pas “rˆater” un comportement fautif MAIS les CT/DT sont coˆuteux (design, ex´ecution, stockage, etc.) Deux enjeux : DT suffisamment vari´ees pour esp´erer trouver des erreurs maˆıtriser la taille : ´eviter les DT redondantes ou non pertinentes Test Logiciel 29/ 129 Test Logiciel 30/ 129 Test Logiciel 30/ 129 Test Logiciel 30/ 129 Test Logiciel 30/ 129 Sujet central du test Tente de r´epondre `a la question : “qu’est-ce qu’un bon jeu de test ?” Plusieurs utilisations des crit`eres : guide pour choisir les CT/DT les plus pertinents ´evaluer la qualit´e d’un jeu de test donner un crit`ere objectif pour arrˆeter la phase de test Quelques qualit´es atttendues d’un crit`ere de test : bonne corr´elation au pouvoir de d´etection des fautes concis automatisable Test Logiciel 31/ 129 Le graphe de flot de contrˆole d’un programme est d´efini par : un noeud pour chaque instruction, plus un noeud final de sortie pour chaque instruction du programme, le CFG comporte un arc reliant le noeud de l’instruction au noeud de l’instruction suivante (ou au noeud final si pas de suivant), l’arc pouvant ˆetre ´etiquett´e par l’instruction en question Quelques d´efinitions sur les instructions conditionnelles : if (a<3 && b<4) then ... else ... un if est une instruction conditionnelle / branchante (a<3 && b<4) est la condition les deux d´ecisions possibles sont (condition, true) et (condition, false) (chaque transition) les conditions simples sont a<3 et b<4 Test Logiciel 32/ 129 Test Logiciel 33/ 129 Quelques crit`eres de couverture sur flot de contrˆole Tous les noeuds (I) : le plus faible. Tous les arcs / d´ecisions (D) : test de chaque d´ecision Toutes les conditions (C) : peut ne pas couvrir toutes les d´ecisions Toutes les conditions/d´ecisions (DC) Toutes les combinaisons de conditions (MC) : explosion combinatoire ! Tous les chemins : le plus fort, impossible `a r´ealiser s’il y a des boucles Test Logiciel 34/ 129 Utilis´e en avionique (DO-178B). But : puissance entre DC et MC ET garde un nombre raisonnable de tests D´efinition crit`ere DC ET les tests doivent montrer que chaque condition atomique peut influencer la d´ecision : par exemple, pour une condition C = a ∧ b, les deux DT a = 1, b = 1 et a = 1, b = 0 prouvent que b seul peut influencer la d´ecision globale C Test Logiciel 35/ 129 Notion de hi´erarchie entre ces diff´erents crit`eres de couverture Le crit ere CT1 est plus fort que le crit ere CT2 (CT1 subsumes CT2, not´e CT1 ⪰ CT2) si pour tout programme P et toute suite de tests TS pour P, si TS couvre CT1 (sur P) alors TS couvre CT2 (sur P). Exercice : supposons que TS2 couvre CT2 et trouve un bug sur P, et TS1 couvre un crit`ere CT1 tq CT1 ⪰ CT2. Question : TS1 trouve-t-il forc´ement le mˆeme bug que TS2 ? Test Logiciel 36/ 129 Test Logiciel 37/ 129 Ne sont pas reli´es `a la qualit´e finale du logiciel (MTBF, PDF, ...) sauf test statistique Ne sont pas non plus vraiment reli´es au # bugs /kloc exception : mcdc et contrˆole-commande exception : mutations Mais toujours mieux que rien ... Test Logiciel 38/ 129 S´election des CT/DT pertinents : tr`es difficile exp´eriences industrielles de synth`ese automatique Script de test : de facile a difficile, mais toujours tr es ad hoc Verdict et oracle : tr`es difficile certains cas particuliers s’y prˆetent bien des oracles partiels automatis´es peuvent ˆetre utiles R´egression : bien automatis´e (ex : JUnit pour Java) Test Logiciel 39/ 129 Introduction to software testing Foundations of Software Testing Art of Software Testing (2nd ´edition) Software Engineering Test Logiciel 40/ 129 Contexte D´efinition du test Aspects pratiques Discussion Test Logiciel 41/ 129 Difficile trouver les d´efauts = pas naturel (surtout pour le programmeur) qualit´e du test d´epend de la pertinence des cas de tests Coˆuteux : entre 30 % et 50 % du d´eveloppement Test Logiciel 42/ 129 Oui, mais ... Correspond au niveau de fiabilit´e exig´e du reste du syst`eme Correspond aux besoins r´eels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilit´e exig´e du reste du syst`eme Correspond aux besoins r´eels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilit´e exig´e du reste du syst`eme Correspond aux besoins r´eels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilit´e exig´e du reste du syst`eme Correspond aux besoins r´eels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilit´e exig´e du reste du syst`eme Correspond aux besoins r´eels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilit´e exig´e du reste du syst`eme Correspond aux besoins r´eels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Beware of bugs in the above code ; I have only proved it correct, not tried it. - Donald Knuth (1977) It has been an exciting twenty years, which has seen the research focus evolve [. . .] from a dream of automatic program verification to a reality of computer-aided debugging. - Thomas A. Henzinger (2001) Test Logiciel 44/ 129 Introduction Automatisation de la g´en´eration de tests Crit`eres de test avanc´es Test Logiciel 45/ 129 On se concentre dans cette partie sur la g´en´eration de donn´ees de test `a partir du code L’oracle est vu comme un probl`eme orthogonal On suppose qu’on dispose d’un oracle automatis´e oracle exact dans certains cas (test dos `a dos) oracle partiel sinon : assertions, contrats (JML, Spec#) Test Logiciel 46/ 129 Principe : transformer tout ou partie du programme en une formule logique ϕ telle que solution de ϕ = DT cherch´ee Approche globale : tout le programme est transform´e en une formule logique th´eories complexes : quantificateurs ou points fixes pour les boucles comment transformer le programme (boucles) ? Approche locale / orient´ee chemin : un seul chemin est consid´er´e `a la fois th´eories plus simples : sans quantificateur, juste conjonction mais ´enum´eration de chemins nous verrons deux techniques - ex´ecution symbolique - ex´ecution symbolique dynamique (dite aussi ex´ecution concolique) Test Logiciel 47/ 129 Pr´edicat de chemins Ex´ecution symbolique Ex´ecution concolique Aspects logiques Optimisations En pratique Discussion Test Logiciel 48/ 129 Le graphe de flot de contrˆole d’un programme est d´efini par : un noeud pour chaque instruction, plus un noeud final de sortie pour chaque instruction du programme, le CFG comporte un arc reliant le noeud de l’instruction au noeud de l’instruction suivante (ou au noeud final si pas de suivant) Test Logiciel 49/ 129 Test Logiciel 50/ 129 π un chemin (fini) du programme P (c-`a-d π ∈ L(P), si P vu comme automate) D l’espace des entr´ees du programme (arguments, variables volatiles, etc.) V ∈ D une entr´ee du programme T une th´eorie logique On note P(V ) la trace d’ex´ecution de P lanc´e sur la donn´ee d’entr´ee V On note par ⪯ la relation de pr´efixe entre les chemins (≈ pr´efixes de mots, ab ⪯ abc ) Test Logiciel 51/ 129 Soit des variables sur un domaine D quelconque, ϕ une formule dans une logique interpr´et´ee sur D, et t une transition d’un programme. On note x −→t y pour indiquer que la valuation y ∈ D est obtenue en appliquant la transition t `a la valuation x ∈ D. ϕ est l’ensemble des d ∈ D tq d |= ϕ. wpre(t, X [′] ) : ensemble X ⊆ D tq ∀x ∈ X, ∀y tq x −→t y alors y ∈ X ′ ensemble des ´el´ements dont tous les successeurs par t sont dans X’ wpre(t, ϕ [′] ) : formule ϕ tq ϕ = wpre(t, ϕ [′] ) post(X, t) : ensemble X [′] ⊆ D tq ∀y ∈ X [′], ∃x ∈ X telque x −→t y ensemble des ´el´ements ayant au moins un pr´ed´ecesseur par t dans X post(ϕ, t) : formule ϕ [′] tq ϕ [′] - = post( ϕ , t) Test Logiciel 52/ 129 Soit un un chemin du programme P : π =−→ [1] −→ [2] . . . −→ Alors le pr´edicat de chemin le plus faible de π est d´efini par : ϕ¯π = wpre(t1, wpre(t2, . . . wpre(tn, ⊤))) cons´equence : un pr´edicat de chemin quelconque ϕπ pour π v´erifie : ϕπ ⇒ ϕ¯π Test Logiciel 53/ 129 Un pr´edicat de chemin pour π peut se calculer en ex´ecutant symboliquement le chemin ex´ecution concr ete : m aj des valeurs des variables ex´ecution symbolique : m`aj des relations logiques entre variables (calcul avec post) M´emoire concr`ete / symbolique concret : (variable, point de contrˆole) → valeur concr`ete symbolique : (variable, point de contrˆole) → formule logique Test Logiciel 54/ 129 Formellement, on utiliser le calcul en avant (post) pour calculer un pr´edicat de chemin pr´edicat de chemin de π calcul´e en avant : ′ ϕ¯π = post(post(post(⊤, t1), t2) . . ., tn) relation entre les deux approches (valable pour un chemin du programme) : ′ ϕ¯π ⇔ ϕ¯π Test Logiciel 55/ 129 Loc Instruction 0 input(y,z) 1 w := y+1 2 x := w + 3 3 if (x < 2 - z) (branche True) 4 if (x < z) (branche False) Pr´edicat de chemin (entr´ees Y0 et Z0) ⊤ Test Logiciel 56/ 129 Loc Instruction 0 input(y,z) 1 w := y+1 2 x := w + 3 3 if (x < 2 - z) (branche True) 4 if (x < z) (branche False) Pr´edicat de chemin (entr´ees Y0 et Z0) ⊤∧ W1 = Y0 + 1 Test Logiciel 56/ 129 Loc Instruction 0 input(y,z) 1 w := y+1 2 x := w + 3 3 if (x < 2 - z) (branche True) 4 if (x < z) (branche False) Pr´edicat de chemin (entr´ees Y0 et Z0) ⊤∧ W1 = Y0 + 1 ∧ X2 = W1 + 3 Test Logiciel 56/ 129 Loc Instruction 0 input(y,z) 1 w := y+1 2 x := w + 3 3 if (x < 2 - z) (branche True) 4 if (x < z) (branche False) Pr´edicat de chemin (entr´ees Y0 et Z0) ⊤∧ W1 = Y0 + 1 ∧ X2 = W1 + 3 ∧ X2 < 2 × Z0 Test Logiciel 56/ 129 Loc Instruction 0 input(y,z) 1 w := y+1 2 x := w + 3 3 if (x < 2 - z) (branche True) 4 if (x < z) (branche False) Pr´edicat de chemin (entr´ees Y0 et Z0) ⊤∧ W1 = Y0 + 1 ∧ X2 = W1 + 3 ∧ X2 < 2 × Z0 ∧ X2 ≥ Z0 Test Logiciel 56/ 129 Loc Instruction 0 input(y,z) 1 w := y+1 2 x := w + 3 3 if (x < 2 - z) (branche True) 4 if (x < z) (branche False) Pr´edicat de chemin (entr´ees Y0 et Z0) ⊤∧ W1 = Y0 + 1 ∧ X2 = W1 + 3 ∧ X2 < 2 × Z0 ∧ X2 ≥ Z0 Projection sur les entr´ees Y0 + 4 < 2 × Z0 ∧ Y0 + 4 ≥ Z0 Test Logiciel 56/ 129 Pr´edicat de chemins Ex´ecution symbolique Ex´ecution concolique Aspects logiques Optimisations En pratique Discussion Test Logiciel 57/ 129 G´en´eration de tests bas´ee sur les chemins 1 choisir un chemin π du CFG 2 calculer un de ses pr´edicats de chemin ϕπ 3 r´esoudre ϕπ : une solution = une DT exer¸cant le chemin π 4 si couverture incompl`ete, goto 1 Id´ee ancienne, mais automatisation compl`ete r´ecente PathCrawler, Dart, Cute, Exe concept introduit par King dans les ann´ees 1970 au d´ebut : tout `a la main, utilisateur se d´ebrouille ensuite : on cr´ee ϕπ, puis utilisateur se d´ebrouille automatisation compl`ete sur des programmes : 1995-2005 (CEA) regain d’int´erˆet r´ecent (Berkeley, CMU, Microsoft, Stanford) Test Logiciel 58/ 129 Variable globale Tests initialis´ee `a ∅ Proc´edure principale : Search(node init, ε, ⊤) /* m`aj Tests, ensemble de paires (TD,π) */ procedure Search(node, π, Φ) input : CFG node, path prefix π, path predicate Φ for π output : no result, update Tests 1: Case node of 2: | ε → /* end node / 3: try Sp := solve(Φ) ; Tests := Tests + {(Sp, π)} / new TD / 4: with unsat → () ; 5: end try 6: | block i → Search(node.next, π · node, Φ ∧ symb(i)) 7: | goto tnode → Search(tnode, π · node, Φ) 8: | ite(cond,inode,tnode) → / branching*/ 9: Search(inode, π · node,Φ ∧ symb(cond)) ; 10: Search(tnode, π · node,Φ ∧¬symb(cond)) 11: end case Test Logiciel 59/ 129 Proc´edure SOLVE : T →{OK (TD), KO} Proc´edure SYMB : Instr → T transforme une instruction de base en formule exemple : x:=x+1 → X1 = X0 + 1 attention : introduire une nouvelle variable logique `a chaque nouvelle utilisation d’une variable du programme Test Logiciel 60/ 129 expr ::= | VC | k ∈ N | expr (+,-,*) expr Expressions de la th´eorie logique T d´efinies par termF : := k ∈ N | VF | termF +F termF | termF −F termF | termF ×F termF let SYMB e = match e with | VC → α(Vc ) // fonction de renommage | k → k | e1 (+,-,*) e2 → SYMB(e1) (+F,−F,×F ) SYMB(e2) SYMB d´efinit de mani`ere similaire sur les conditions Test Logiciel 61/ 129 Pourquoi α(Vc ) : les “variables” du programme C peuvent ˆetre modifi´ees `a chaque ´etape de l’ex´ecution les “variables” de la th´eorie T sont des inconnues, de valeur constante le renommage est n´ecessaire pour prendre en compte la dynamique de l’ex´ecution - pr´edicat de chemin pour x := x+1 ? - Xn+1 = Xn + 1, plutˆot que X = X + 1 Test Logiciel 62/ 129 Le calcul de pr´edicat de chemin est : correct s’il produit un pr´edicat de chemin plus fort que le pr´edicat de chemin le plus lˆache complet s’il produit un pr´edicat de chemin ´equisatisfiable au pr´edicat de chemin le plus lˆache Le calcul symbolique symbolique est correct (resp. complet) si : le calcul de pr´edicat de chemin est correct (resp. complet) le solveur est correct et complet pour la th´eorie consid´er´ee Propri´et´es Correction si le calcul symbolique est correct, alors la proc´edure est correcte : chaque DT g´en´er´e suit le chemin pr´evu Compl´etude si le calcul symbolique est complet, alors la proc´edure est compl`ete : quand la proc´edure termine, chaque chemin faisable est couvert Terminaison la proc´edure termine ssi le nombre de chemins est fini Test Logiciel 63/ 129 La proc´edure produit des t´emoins d’accessibilit´e : on peut v´erifier le r´esultat fournit par des outils externes simples (calcul de couverture) un couple (DT, π) est plus facile `a comprendre humainement que des invariants les DT peuvent ˆetre export´ees vers des outils classiques de gestion de tests (couverture, tests de r´egression) Correction : chaque DT g´en´er´e suit le chemin pr´evu pas de faux positifs ! ! un bug report´e est un bug trouv´e la couverture du jeu de tests fourni est effectivement atteinte les instructions couvertes lors de l’ex´ecution symboliques sont vraiment atteignables MAIS : La compl´etude n’est que rarement obtenue, car le nombre de chemins doit ˆetre limit´e a priori Test Logiciel 64/ 129 M´ethode de base : couverture de chemins, mais ... Base pour d’autres crit`eres (instructions ou branches) arrˆet lorsque le taux de couverture est suffisant guide le choix des chemins Param`etres : th´eorie logique, ´enum´eration de chemins Test Logiciel 65/ 129 Ajouts classiques `a la proc´edure borne sur la longueur des chemins time out sur le solveur gestion de couverture (instructions, branches) Les points 1. et 2. cassent la propri´et´es de compl´etude pour assurer terminaison et temps de calcul raisonnable En pratique, l’hypoth ese de calcul symbolique parfait (correct + complet) est difficile a obtenir. pour du test, il vaut mieux garder la correction et sacrifier la compl´etude (coh´erent avec la restriction arbitraire du nombre de chemins) remarque : dans le cas concolique (cf + tard), on peut imaginer se passer dans une certaine mesure de la correction du solveur Test Logiciel 66/ 129 Passage `a l’´echelle / Performances (cf plus tard dans le cours) coˆut d’un appel au solveur nombre de chemins Exploration (inutile) de chemins infaisables (PB1) pas de d´etection : coˆuteux en # chemins inutiles explor´es d´etection au plus tˆot : coˆuteux en # appels solveurs Constructions du langage hors de port´ee de la th´eorie choisie (PB2) op´erations non lin´eaire assembleur incorpor´e, biblioth`eques en code natif L’ex´ecution concolique apporte des solutions aux 2 derniers probl emes (cf apr es) Test Logiciel 67/ 129 Supposons un chemin infaisable dans l’arbre des ex´ecutions possibles Test Logiciel 68/ 129 Supposons un chemin infaisable dans l’arbre des ex´ecutions possibles Test Logiciel 68/ 129 M´ethode usuelle : r´esoudre le pr´edicat `a la fin du chemin : un appel au solveur par chemin (sur un arbre : 2 ) : on peut continuer la recherche `a partir de pr´efixes UNSAT KO sur programmes avec beaucoup de chemins infaisables Test Logiciel 68/ 129 Alternative : r´esoudre le pr´edicat `a chaque branche : d´etecte UNSAT au plus tˆot : un appel au solveur par pr´efixe de chemin faisable, et un appel au solveur par pr´efixe minimal infaisable (sur un arbre : 2 ∗ 2 - 1) KO sur programmes avec peu de chemins infaisables Test Logiciel 68/ 129 Un probl`eme classique : constructions du langage hors de port´ee de la th´eorie choisie G´en´erer un test pour f atteignant ERROR ci-dessous (th´eorie = arithm´etique lin´eaire) g(int x) {return x*x+(x modulo 2); } f(int x, int y) {z=g(x); if (y == z) {ERROR; }else OK } Probl`eme Une ex´ecution symbolique g´en`ere une expression symbolique de type Z = X ∗ X + (X modulo 2) Cette expression n’est pas solvable en arithm´etique lin´eaire Solutions classiques tir´ees de l’analyse statique / preuve de programme surapproximation ici par exemple Z = ⊤. PROBLEME : on perd la correction le TD g´en´er´e peut ne pas suivre le chemin pr´evu Test Logiciel 69/ 129 L’ex´ecution concolique offre : une solution tr es ´el´egante a PB1 - d´etecte UNSAT au plus tˆot - un appel au solveur par chemin (maximal) faisable + un appel par prefixe minimal infaisable une solution pragmatique `a PB2 Test Logiciel 70/ 129 Pr´edicat de chemins Ex´ecution symbolique Ex´ecution concolique Aspects logiques Optimisations En pratique Discussion Test Logiciel 71/ 129 Ex´ecution concr`ete : collecte des infos pour aider le raisonnement symbolique concr´etisation : force une variable symbolique a prendre sa valeur concr ete courante Deux utilisations typiques suivre uniquement des chemins faisables `a moindre coˆut toujours suivre une ex´ecution concr`ete + r´esoudre au plus tˆot approximation de constructions du langage “difficiles” concr´etisation d’une partie des entr´ees/sorties approximations correctes Test Logiciel 72/ 129 concret : X=12 backtrack + r´esolution, solution X = 5 concret : X=5 backtrack + r´esolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + r´esolution, solution X = 5 concret : X=5 backtrack + r´esolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + r´esolution, solution X = 5 concret : X=5 backtrack + r´esolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + r´esolution, solution X = 5 concret : X=5 backtrack + r´esolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + r´esolution, solution X = 5 concret : X=5 backtrack + r´esolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + r´esolution, solution X = 5 concret : X=5 backtrack + r´esolution, unsat Test Logiciel 73/ 129 Test Logiciel 74/ 129 Test Logiciel 74/ 129 M´ethode usuelle : r´esoudre le pr´edicat `a la fin du chemin : un appel au solveur par chemin (sur un arbre :...