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énération de tests Critères de test avancés Test Logiciel 2/ 129 Contexte Définition du test Aspects pratiques Discussion Test Logiciel 3/ 129 Coût des bugs Coûts économique : 64 milliards $/an rien qu’aux US (2002) Coûts humains, environnementaux, etc. Nécessité d’assurer la qualité des logiciels Domains critiques atteindre le (très haut) niveau de qualité imposée par les lois/normes/assurances/... (ex : DO-178B pour aviation) Autres domaines atteindre le rapport qualité/prix jugé optimal (c.f. attentes du client) Test Logiciel 4/ 129 Validation et Vérification (V & V) Vérification : 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éthodes ? revues simulation/ animation tests méthode de loin la plus utilisée méthodes formelles encore très confidentielles, même en syst. critiques Coût de la V & V 10 milliards $/an en tests rien qu’aux US plus de 50% du développement d’un logiciel critique (parfois - 90%) en moyenne 30% du développement d’un logiciel standard Test Logiciel 5/ 129 La vérification est une part cruciale du développement Le test est de loin la méthode la plus utilisée Les méthodes manuelles de test passent tr es mal a l’échelle en terme de taille de code / niveau d’exigence fort besoin d’automatisation Test Logiciel 6/ 129 Contexte Définition du test Aspects pratiques Discussion Test Logiciel 7/ 129 Le test est une méthode dynamique visant à trouver des bugs Tester, c’est exécuter le programme dans l’intention d’y trouver des anomalies ou des défauts - 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énario à exécuter 2 estimer le résultat attendu du CT (Oracle) 3 déterminer (1) une donnée de test (DT) suivant le CT, et (2) son oracle concret (concrétisation) 4 exécuter le programme sur la DT (script de test) 5 comparer le résultat obtenu au résultat attendu (verdict : pass/fail) Script de Test : code / script qui lance le programme à tester sur le DT choisi, observe les résultats, calcule le verdict Suite / Jeu de tests : ensemble de cas de tests Test Logiciel 9/ 129 Spécification : tri de tableaux d’entiers + enlèver 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é CT2 tableau vide le tableau vide CT3 tableau avec 2 entiers redondants trié sans redondance Concrétisation : DT et résultat 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é 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èmes non informatiques Un bon jeu de tests doit donc : exercer un maximum de “comportements différents” du programme (notion de critères de test) notamment - tests nominaux : cas de fonctionnement les plus fréquents - tests de robustesse : cas limites / délicats Test Logiciel 12/ 129 1- Contribuer à assurer la qualité du produit lors de la phase de conception / codage en partie par les développeurs (tests unitaires) but = trouver rapidement le plus de bugs possibles (avant la commercialisation) - test réussi = un test qui trouve un bug 2- Validation : Démontrer la qualité à un tiers une fois le produit terminé idéalement : par une équipe dédiée but = convaincre (organismes de certification, hiérarchie, client - Xtrem programming) - test réussi = un test qui passe sans problème - + tests jugés représentatifs (systèmes critiques : audit du jeu de tests) Test Logiciel 13/ 129 Critère de tests boite blanche / boite noire / probabiliste Phase du processus de test test unitaire, d’intégration, système, acceptation, regression Test Logiciel 14/ 129 Tests unitaire : tester les différents modules en isolation définition non stricte de “module unitaire” (procédures, classes, packages, composants, etc.) uniquement test de correction fonctionnelle Tests d’intégration : tester le bon comportement lors de la composition des modules uniquement test de correction fonctionnelle Tests système / de conformité : valider l’adéquation du code aux spécifications on teste aussi toutes les caractéristiques émergentes sécurité, performances, etc. Tests de validation / acceptance : valider l’adéquation aux besoins du client souvent similaire au test système, mais réaliser / vérifier par le client Tests de régression : vérifier que les corrections / évolutions du code n’ont pas introduits de bugs Test Logiciel 15/ 129 Test Logiciel 16/ 129 Boˆıte Noire : à partir de spécifications dossier de conception interfaces des fonctions / modules modèle formel ou semi-formel Boˆıte Blanche : à partir du code Probabiliste : domaines des entrées + arguments statistiques Test Logiciel 17/ 129 Ne nécesite pas de connaˆıtre la structure interne du système Basé sur la spécification de l’interface du système et de ses fonctionnalités : taille raisonnable Permet d’assurer la conformance spéc - code, mais aveugle aux défauts fins de programmation Pas trop de probl eme d’oracle pour le CT, mais probl eme de la concrétisation Approprié pour le test du système mais également pour le test unitaire Test Logiciel 18/ 129 La structure interne du système doˆıt être accessible Se base sur le code : très précis, mais plus “gros” que les spécifications Conséquences : DT potentiellement plus fines, mais très nombreuses Pas de probl eme de concrétisation, mais probl eme de l’oracle Sensible aux défauts fins de programmation, mais aveugle aux fonctionnalités absentes Test Logiciel 19/ 129 Les données sont choisies dans leur domaine selon une loi statistique loi uniforme (test aléatoire ) loi statistique du profil opérationnel (test statistique) Pros/Cons du test aléatoire sélection aisée des DT en général test massif si oracle (partiel) automatisé “objectivité” 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éduire une garantie statistique sur le programme trouve les défauts les plus probables : défauts mineurs ? PB : difficile d’avoir la loi statistique Test Logiciel 20/ 129 Contexte Définition du test Aspects pratiques Discussion Test Logiciel 21/ 129 La définition de l’oracle est un probl eme tr es difficile limite fortement certaines méthodes de test (ex : probabiliste, BN) impose un trade-off avec la sélection de tests point le plus mal maitrisé pour l’automatisation Test Logiciel 22/ 129 Quelques cas pratiques d’oracles parfaits automatisables comparer à une référence : logiciel existant, tables de résultats résultat simple à vérifier (ex : solution d’une équation) disponibilité d’un logiciel similaire : test dos à dos Des oracles partiels mais automatisés peuvent être utiles oracle le plus basique : le programme ne plante pas instrumentation du code (assert) plus évolué : programmation avec contrats (Eiffel, Jml pour Java) Test Logiciel 23/ 129 Composition du script de test préambule : amène le programme dans la configuration voulue pour le test (ex : initialisation de BD, suite d’émissions / réceptions de messages, etc.) corps : appel des “stimuli” testés (ex : fonctions et DT) identification : opérations d’observations pour faciliter / permettre le travail de l’oracle (ex : log des actions, valeurs de variables globales, etc.) postambule : retour vers un état initial pour enchainer les tests Le script doit souvent inclure de la glue avec le reste du code bouchon : simule les fonctions appelées mais pas encore écrites Test Logiciel 24/ 129 Quelques exemples de problèmes Code manquant (test incrémental) Exécution d’un test très coûteuse en temps Hardware réel non disponible, ou peu disponible Présence d’un environnement (réseau, Base de Données, machine, etc.) comment le prendre en compte ? (émulation ?) Réinitialisation possible du système ? si non, l’ordre des tests est très 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érations (manuelles ?) sur l’interface disponible (informatique ? électronique ? mécanique ?) Test Logiciel 25/ 129 Message : code “desktop” sans environnement : facile code embarqué temps réel peut poser de sérieux problèmes, solutions ad hoc Test Logiciel 26/ 129 Tests de régression : à chaque fois que le logiciel est modifié, s’assurer que “ce qui fonctionnait avant fonctionne toujours” Pourquoi modifier le code déjà testé ? correction de défaut ajout de fonctionnalités Quand ? en phase de maintenance / évolution ou durant le développement Quels types de tests ? tous : unitaires, intégration, système, etc. Objectif : avoir une méthode automatique pour rejouer automatiquement les tests détecter les tests dont les scripts ne sont plus (syntaxiquement) corrects Test Logiciel 27/ 129 Junit pour Java : idée principale = tests écrits en Java simplifie l’exécution et le rejeu des tests (juste tout relancer) simplifie la détection d’une partie des tests non à jour : tests recompilés en même temps que le programme simplifie le stockage et la réutilisation des tests ( tests de MyClass dans MyClassTest) JUnit offre : des primitives pour créer un test (assertions) des primitives pour gérer des suites de tests des facilités pour l’exécution des tests statistiques sur l’exécution des tests interface graphique pour la couverture des tests points d’extensions pour des situations spécifiques Solution très simple et extrêmement efficace Test Logiciel 28/ 129 Problèmes de la sélection de tests : efficacité du test dépend crucialement de la qualité des CT/DT ne pas “râter” un comportement fautif MAIS les CT/DT sont coûteux (design, exécution, stockage, etc.) Deux enjeux : DT suffisamment variées pour espérer trouver des erreurs maˆıtriser la taille : éviter 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épondre à la question : “qu’est-ce qu’un bon jeu de test ?” Plusieurs utilisations des critères : guide pour choisir les CT/DT les plus pertinents évaluer la qualité d’un jeu de test donner un critère objectif pour arrêter la phase de test Quelques qualités atttendues d’un critère de test : bonne corrélation au pouvoir de détection des fautes concis automatisable Test Logiciel 31/ 129 Le graphe de flot de contrôle d’un programme est défini 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 être étiquetté par l’instruction en question Quelques définitions 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écisions 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ères de couverture sur flot de contrôle Tous les noeuds (I) : le plus faible. Tous les arcs / décisions (D) : test de chaque décision Toutes les conditions (C) : peut ne pas couvrir toutes les décisions Toutes les conditions/décisions (DC) Toutes les combinaisons de conditions (MC) : explosion combinatoire ! Tous les chemins : le plus fort, impossible à réaliser s’il y a des boucles Test Logiciel 34/ 129 Utilisé en avionique (DO-178B). But : puissance entre DC et MC ET garde un nombre raisonnable de tests Définition critère DC ET les tests doivent montrer que chaque condition atomique peut influencer la décision : 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écision globale C Test Logiciel 35/ 129 Notion de hiérarchie entre ces différents critères de couverture Le crit ere CT1 est plus fort que le crit ere CT2 (CT1 subsumes CT2, noté 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ère CT1 tq CT1 ⪰ CT2. Question : TS1 trouve-t-il forcément le même bug que TS2 ? Test Logiciel 36/ 129 Test Logiciel 37/ 129 Ne sont pas reliés à la qualité finale du logiciel (MTBF, PDF, ...) sauf test statistique Ne sont pas non plus vraiment reliés au # bugs /kloc exception : mcdc et contrôle-commande exception : mutations Mais toujours mieux que rien ... Test Logiciel 38/ 129 Sélection des CT/DT pertinents : très difficile expériences industrielles de synthèse automatique Script de test : de facile a difficile, mais toujours tr es ad hoc Verdict et oracle : très difficile certains cas particuliers s’y prêtent bien des oracles partiels automatisés peuvent être utiles Régression : bien automatisé (ex : JUnit pour Java) Test Logiciel 39/ 129 Introduction to software testing Foundations of Software Testing Art of Software Testing (2nd édition) Software Engineering Test Logiciel 40/ 129 Contexte Définition du test Aspects pratiques Discussion Test Logiciel 41/ 129 Difficile trouver les défauts = pas naturel (surtout pour le programmeur) qualité du test dépend de la pertinence des cas de tests Coûteux : entre 30 % et 50 % du développement Test Logiciel 42/ 129 Oui, mais ... Correspond au niveau de fiabilité exigé du reste du système Correspond aux besoins réels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilité exigé du reste du système Correspond aux besoins réels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilité exigé du reste du système Correspond aux besoins réels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilité exigé du reste du système Correspond aux besoins réels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilité exigé du reste du système Correspond aux besoins réels de beaucoup d’industriels Peut attaquer des programmes + complexes Test Logiciel 43/ 129 Oui, mais ... Correspond au niveau de fiabilité exigé du reste du système Correspond aux besoins réels 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énération de tests Critères de test avancés Test Logiciel 45/ 129 On se concentre dans cette partie sur la génération de données de test à partir du code L’oracle est vu comme un problème orthogonal On suppose qu’on dispose d’un oracle automatisé oracle exact dans certains cas (test dos à 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ée Approche globale : tout le programme est transformé en une formule logique théories complexes : quantificateurs ou points fixes pour les boucles comment transformer le programme (boucles) ? Approche locale / orientée chemin : un seul chemin est considéré à la fois théories plus simples : sans quantificateur, juste conjonction mais énumération de chemins nous verrons deux techniques - exécution symbolique - exécution symbolique dynamique (dite aussi exécution concolique) Test Logiciel 47/ 129 Prédicat de chemins Exécution symbolique Exécution concolique Aspects logiques Optimisations En pratique Discussion Test Logiciel 48/ 129 Le graphe de flot de contrôle d’un programme est défini 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-à-d π ∈ L(P), si P vu comme automate) D l’espace des entrées du programme (arguments, variables volatiles, etc.) V ∈ D une entrée du programme T une théorie logique On note P(V ) la trace d’exécution de P lancé sur la donnée d’entrée V On note par ⪯ la relation de préfixe entre les chemins (≈ préfixes de mots, ab ⪯ abc ) Test Logiciel 51/ 129 Soit des variables sur un domaine D quelconque, ϕ une formule dans une logique interprétée 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 à 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 éléments 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 éléments ayant au moins un prédécesseur 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édicat de chemin le plus faible de π est défini par : ϕ¯π = wpre(t1, wpre(t2, . . . wpre(tn, ⊤))) conséquence : un prédicat de chemin quelconque ϕπ pour π vérifie : ϕπ ⇒ ϕ¯π Test Logiciel 53/ 129 Un prédicat de chemin pour π peut se calculer en exécutant symboliquement le chemin exécution concr ete : m aj des valeurs des variables exécution symbolique : màj des relations logiques entre variables (calcul avec post) Mémoire concrète / symbolique concret : (variable, point de contrôle) → valeur concrète symbolique : (variable, point de contrôle) → formule logique Test Logiciel 54/ 129 Formellement, on utiliser le calcul en avant (post) pour calculer un prédicat de chemin prédicat de chemin de π calculé 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édicat de chemin (entrées 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édicat de chemin (entrées 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édicat de chemin (entrées 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édicat de chemin (entrées 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édicat de chemin (entrées 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édicat de chemin (entrées Y0 et Z0) ⊤∧ W1 = Y0 + 1 ∧ X2 = W1 + 3 ∧ X2 < 2 × Z0 ∧ X2 ≥ Z0 Projection sur les entrées Y0 + 4 < 2 × Z0 ∧ Y0 + 4 ≥ Z0 Test Logiciel 56/ 129 Prédicat de chemins Exécution symbolique Exécution concolique Aspects logiques Optimisations En pratique Discussion Test Logiciel 57/ 129 Génération de tests basée sur les chemins 1 choisir un chemin π du CFG 2 calculer un de ses prédicats de chemin ϕπ 3 résoudre ϕπ : une solution = une DT exerçant le chemin π 4 si couverture incomplète, goto 1 Idée ancienne, mais automatisation complète récente PathCrawler, Dart, Cute, Exe concept introduit par King dans les années 1970 au début : tout à la main, utilisateur se débrouille ensuite : on crée ϕπ, puis utilisateur se débrouille automatisation complète sur des programmes : 1995-2005 (CEA) regain d’intérêt récent (Berkeley, CMU, Microsoft, Stanford) Test Logiciel 58/ 129 Variable globale Tests initialisée à ∅ Procédure principale : Search(node init, ε, ⊤) /* màj 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édure SOLVE : T →{OK (TD), KO} Procédure SYMB : Instr → T transforme une instruction de base en formule exemple : x:=x+1 → X1 = X0 + 1 attention : introduire une nouvelle variable logique à chaque nouvelle utilisation d’une variable du programme Test Logiciel 60/ 129 expr ::= | VC | k ∈ N | expr (+,-,*) expr Expressions de la théorie logique T définies 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éfinit de manière similaire sur les conditions Test Logiciel 61/ 129 Pourquoi α(Vc ) : les “variables” du programme C peuvent être modifiées à chaque étape de l’exécution les “variables” de la théorie T sont des inconnues, de valeur constante le renommage est nécessaire pour prendre en compte la dynamique de l’exécution - prédicat de chemin pour x := x+1 ? - Xn+1 = Xn + 1, plutôt que X = X + 1 Test Logiciel 62/ 129 Le calcul de prédicat de chemin est : correct s’il produit un prédicat de chemin plus fort que le prédicat de chemin le plus lâche complet s’il produit un prédicat de chemin équisatisfiable au prédicat de chemin le plus lâche Le calcul symbolique symbolique est correct (resp. complet) si : le calcul de prédicat de chemin est correct (resp. complet) le solveur est correct et complet pour la théorie considérée Propriétés Correction si le calcul symbolique est correct, alors la procédure est correcte : chaque DT généré suit le chemin prévu Complétude si le calcul symbolique est complet, alors la procédure est complète : quand la procédure termine, chaque chemin faisable est couvert Terminaison la procédure termine ssi le nombre de chemins est fini Test Logiciel 63/ 129 La procédure produit des témoins d’accessibilité : on peut vérifier le résultat fournit par des outils externes simples (calcul de couverture) un couple (DT, π) est plus facile à comprendre humainement que des invariants les DT peuvent être exportées vers des outils classiques de gestion de tests (couverture, tests de régression) Correction : chaque DT généré suit le chemin prévu pas de faux positifs ! ! un bug reporté est un bug trouvé la couverture du jeu de tests fourni est effectivement atteinte les instructions couvertes lors de l’exécution symboliques sont vraiment atteignables MAIS : La complétude n’est que rarement obtenue, car le nombre de chemins doit être limité a priori Test Logiciel 64/ 129 Méthode de base : couverture de chemins, mais ... Base pour d’autres critères (instructions ou branches) arrêt lorsque le taux de couverture est suffisant guide le choix des chemins Paramètres : théorie logique, énumération de chemins Test Logiciel 65/ 129 Ajouts classiques à la procédure borne sur la longueur des chemins time out sur le solveur gestion de couverture (instructions, branches) Les points 1. et 2. cassent la propriétés de complétude 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étude (cohérent 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 à l’échelle / Performances (cf plus tard dans le cours) coût d’un appel au solveur nombre de chemins Exploration (inutile) de chemins infaisables (PB1) pas de détection : coûteux en # chemins inutiles explorés détection au plus tôt : coûteux en # appels solveurs Constructions du langage hors de portée de la théorie choisie (PB2) opérations non linéaire assembleur incorporé, bibliothèques en code natif L’exécution 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écutions possibles Test Logiciel 68/ 129 Supposons un chemin infaisable dans l’arbre des exécutions possibles Test Logiciel 68/ 129 Méthode usuelle : résoudre le prédicat à la fin du chemin : un appel au solveur par chemin (sur un arbre : 2 ) : on peut continuer la recherche à partir de préfixes UNSAT KO sur programmes avec beaucoup de chemins infaisables Test Logiciel 68/ 129 Alternative : résoudre le prédicat à chaque branche : détecte UNSAT au plus tôt : un appel au solveur par préfixe de chemin faisable, et un appel au solveur par préfixe minimal infaisable (sur un arbre : 2 ∗ 2 - 1) KO sur programmes avec peu de chemins infaisables Test Logiciel 68/ 129 Un problème classique : constructions du langage hors de portée de la théorie choisie Générer un test pour f atteignant ERROR ci-dessous (théorie = arithmétique linéaire) g(int x) {return x*x+(x modulo 2); } f(int x, int y) {z=g(x); if (y == z) {ERROR; }else OK } Problème Une exécution symbolique génère une expression symbolique de type Z = X ∗ X + (X modulo 2) Cette expression n’est pas solvable en arithmétique linéaire Solutions classiques tirées de l’analyse statique / preuve de programme surapproximation ici par exemple Z = ⊤. PROBLEME : on perd la correction le TD généré peut ne pas suivre le chemin prévu Test Logiciel 69/ 129 L’exécution concolique offre : une solution tr es élégante a PB1 - détecte UNSAT au plus tôt - un appel au solveur par chemin (maximal) faisable + un appel par prefixe minimal infaisable une solution pragmatique à PB2 Test Logiciel 70/ 129 Prédicat de chemins Exécution symbolique Exécution concolique Aspects logiques Optimisations En pratique Discussion Test Logiciel 71/ 129 Exécution concrète : collecte des infos pour aider le raisonnement symbolique concrétisation : force une variable symbolique a prendre sa valeur concr ete courante Deux utilisations typiques suivre uniquement des chemins faisables à moindre coût toujours suivre une exécution concrète + résoudre au plus tôt approximation de constructions du langage “difficiles” concrétisation d’une partie des entrées/sorties approximations correctes Test Logiciel 72/ 129 concret : X=12 backtrack + résolution, solution X = 5 concret : X=5 backtrack + résolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + résolution, solution X = 5 concret : X=5 backtrack + résolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + résolution, solution X = 5 concret : X=5 backtrack + résolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + résolution, solution X = 5 concret : X=5 backtrack + résolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + résolution, solution X = 5 concret : X=5 backtrack + résolution, unsat Test Logiciel 73/ 129 concret : X=12 backtrack + résolution, solution X = 5 concret : X=5 backtrack + résolution, unsat Test Logiciel 73/ 129 Test Logiciel 74/ 129 Test Logiciel 74/ 129 Méthode usuelle : résoudre le prédicat à la fin du chemin : un appel au solveur par chemin (sur un arbre :...