RésuméL'analyse des boucles est un élément clé des outils d'analyse statique. Malheureusement, il existe quelques rares cas limites. Lorsqu'un outil passe du stade de prototype académique à celui de produit prêt à l'emploi, des cas obscurs peuvent se produire et se produisent effectivement. Il en résulte que l'analyse de boucle est une source clé de bogues algorithmiques importants découverts tardivement. Pour éviter cela, ce document présente une collection d'exemples et de défis "folkloriques" dans l'analyse de boucle.
Concepts du CSC : Logiciel et son ingénierie - Vérification de logiciel ; Analyse statique automatisée.
Mots-clés : Analyse de boucle, Vérification de logiciel, Analyse statique
1 Introduction
Lors du développement d'un nouvel outil d'analyse statique, il y a peu de distance entre les développeurs et les utilisateurs. Souvent, ils sont les mêmes. Le diagnostic et le débogage des problèmes liés à l'outil ne sont pas plus difficiles que le développement normal. La distance entre les utilisateurs et les développeurs augmente au fur et à mesure que l'outil devient plus performant. Pour identifier les défauts, il faut que les utilisateurs aient la volonté et la capacité d'envoyer des rapports de bogues. La reproduction peut nécessiter des accords de non-divulgation ou des déplacements dans les locaux du client. La confirmation des corrections peut nécessiter un cycle complet de publication et de déploiement. Des bogues qui auraient pris des jours à corriger au début du développement prennent aujourd'hui des semaines, ce qui souligne l'importance d'une détection précoce des bogues.
Les bogues dans les outils d'analyse statique varient en termes de gravité et d'impact. Les pannes survenant au début des entrées peuvent normalement être isolées assez facilement. Les bogues de correction dus à des erreurs dans les algorithmes de base sont parmi les plus difficiles à trouver et à corriger. Les pires de ces cas sont ceux qui comportent plusieurs cas limites, et il semble qu'un seul doive être corrigé. Cela peut conduire à un cycle de rapports de bogues et de corrections, qui consomme le temps, le budget et la bonne volonté des utilisateurs à une vitesse effrayante.
Cet article traite des bogues qui résultent des croyances erronées et des hypothèses incorrectes des développeurs d'outils concernant les boucles et leur structure. L'expérience acquise avec divers outils, notamment CBMC [17, 18, 21], SPARK [16], 2LS [4] et goto-analyzer [14, 23], à différents stades de développement, a montré qu'il s'agit d'une source persistante de bogues complexes et détectés tardivement. Les boucles qui ne répondent pas aux hypothèses du développeur sont souvent corrigées par une simple solution de contournement pour l'exemple spécifique, qui résout rarement l'ensemble du problème, ce qui conduit à des bogues supplémentaires avec des corrections précaires et une complexité de code croissante.
Ce document apporte les contributions suivantes :
- La section 2 passe en revue plusieurs définitions de boucles utilisant différentes représentations de programmes et donne des exemples mettant en évidence leurs différences.
- La section 3 explique les erreurs (marquées E) que les auteurs et d'autres ont commises à propos de la structure des boucles. Ces erreurs ont été identifiées comme les causes principales des bogues de correction trouvés dans plusieurs outils, dont beaucoup ont conduit à des bogues graves et coûteux en temps.
- La section 4 fournit des recommandations pour l'analyse des boucles, la prévention des bogues et les vérifications permettant d'éviter certaines des erreurs décrites dans la section 3.
2 Que sont les boucles ?
Pour illustrer nos définitions, nous utilisons la "première" boucle en C [11] :
| Code : | Sélectionner tout |
1 2 3 4 5 | while (fahr <= upper) {
celsius = ( 5.0/9.0 ) ∗ ( fahr−32.0 ) ;
printf ("%4.0f␣%6.1f\n", fahr, celsius ) ;
fahr = fahr + step ;
} |
- Le programme vérifie d'abord la condition de la boucle. . .
- . ... qui est le seul moyen de sortir de la boucle.
- Si la condition est vraie, le corps de la boucle est exécuté.
- Le programme revient au début de la boucle une fois que le corps de la boucle est terminé et tout se répète.
Malheureusement, aucune de ces conditions ne s'applique à toutes les boucles.
Lorsqu'un programme est représenté sous la forme d'un arbre d'analyse, une boucle est toute instance des règles de la grammaire des boucles, telles que les règles while ou for. Dans l'exemple, nous avons une seule boucle while, avec une condition de boucle (fahr <= upper) et un corps de boucle.
Une autre représentation du programme est une liste d'instructions. Les sauts transfèrent l'exécution à une partie différente de la liste d'instructions, en fonction d'une certaine condition ou en renonçant inconditionnellement à l'exécution des instructions entre le saut et l'étiquette cible. L'exemple en cours peut être représenté à l'aide de six instructions :
| Code : | Sélectionner tout |
1 2 3 4 5 6 | A: JUMP_IF ! ( fahr <= upper ), B ASSIGN celsius, (5.0/9.0) * (fahr-32.0) CALL printf, "%4.0f %6.1f\n", fahr, celsius ASSIGN fahr, fahr + step JUMP A B: SKIP |
Une troisième représentation est un graphe de flux de contrôle (CFG) [3], qui résume la liste des instructions en un graphe orienté. Chaque instruction devient un nœud. Les sauts conditionnels ont deux arêtes : vers la cible du saut et vers l'instruction suivante. Les sauts inconditionnels ont une seule arête vers leur cible. Toutes les autres instructions (sauf la dernière) ont une seule arête vers l'instruction suivante. La figure 1 présente le CFG de l'exemple.
Il existe deux définitions largement utilisées des boucles dans les CFG : une boucle naturelle et un cycle. Suivant [2, 10], nous décrivons une arête arrière comme toute arête dans le graphe de C - ℎ où chaque chemin du début de la fonction à C passe par ℎ. Nous appelons ℎ la tête de la boucle et C la queue de la boucle. La boucle naturelle correspondante est ℎ plus l'ensemble des nœuds qui peuvent atteindre C sans passer par ℎ. Les boucles naturelles ayant la même tête sont fusionnées et considérées comme une boucle singulière. Suivant [9], nous décrivons un cycle comme une composante maximale fortement connectée (SCC). Les cycles sont plus généraux et peuvent contenir plusieurs points d'entrée, contrairement aux boucles naturelles.
Les définitions des boucles ne sont pas équivalentes. Comme les quatre définitions cherchent à décrire la même structure fondamentale, il n'est pas déraisonnable de les considérer comme identiques ou au moins "essentiellement équivalentes". Par exemple, les outils de vérification déductive fournissent des annotations permettant au programmeur d'énoncer des invariants de boucle. Les interprètes abstraits et les outils basés sur la synthèse inductive guidée par des contre-exemples calculent également des invariants de boucle. Les outils de vérification déductive utilisent généralement les définitions de l'arbre d'analyse des boucles, tandis que d'autres outils utilisent les définitions du CFG ou de la liste. Ces différences de définition et de propriétés des boucles peuvent être à l'origine d'incompréhensions et de bogues considérables lorsque l'on tente de combiner différents types d'outils [4, 21]. Cette section présente quelques sources de ces erreurs.
E Les conditions de boucle sont les mêmes dans toutes les définitions. Les conditions de boucle sont une caractéristique de la représentation de l'arbre d'analyse, comme elles sont une caractéristique syntaxique de la plupart des langages. Malheureusement, les conditions de boucle sont plus fragiles qu'on ne le pense souvent. Dans le code suivant, la représentation de l'arbre d'analyse contient une seule condition de boucle vraie suggérant que la boucle ne se termine pas :
| Code : | Sélectionner tout |
1 2 3 4 5 | do {
open_ socke t ( ) ;
if (connect ( ) == SUCCESS ) { break ; }
close _ socket ( ) ;
} while ( 1 ) ; |
Les conditions de boucle de l'arbre d'analyse ne sont pas directement définissables dans les listes d'instructions et les CFG. Comparez les deux programmes suivants qui utilisent des opérateurs "raccourcis" :
| Code : | Sélectionner tout |
1 2 3 4 5 6 7 | while (A( ) && B ( ) ) {
green ( ) ;
}
while (A ( ) ) {
i f (!B ( ) ) { break ; }
green ( ) ;
} |
Il est tentant de penser qu'il existe une définition CFG d'une condition de boucle du type "Une branche conditionnelle où une branche est en dehors de la CSC", mais cela ne correspond pas à la définition de l'arbre de parse :
| Code : | Sélectionner tout |
1 2 3 4 5 | while (A( ) | | B ( ) | | C ( ) ) {
if (D ( ) ) { break ; }
pink ( ) ;
if ( E ( ) ) { break ; }
} |
E Les corps de boucle sont identiques dans toutes les définitions. De même que les conditions de boucle, les corps de boucle sont une caractéristique syntaxique dans la plupart des langages et sont clairement définis. Ils ne correspondent pas nécessairement aux instructions considérées comme faisant partie de la boucle dans d'autres représentations. Prenons un exemple :
| Code : | Sélectionner tout |
1 2 3 4 5 | while ( choose ( ) ) {
if ( choose ( ) ) { red ( ) ; break ; }
else if ( choose ( ) ) { goto out ; }
}
if ( 0 ) { out : blue ( ) ; } |
E Les arêtes arrière sont les mêmes que les sauts en arrière. Les bords arrière dans une représentation de liste ne sont pas garantis dans le CFG. Considérons la représentation de liste suivante :
| Code : | Sélectionner tout |
1 2 3 4 5 6 7 8 9 10 | goto A; B : second ( ) ; assert ( counter == 2 ) ; goto C; A : f i r s t ( ) ; a s s e r t ( counter == 1 ) ; goto B ; C : third ( ) ; assert ( counter == 3 ) ; return ; |
E Le nombre de boucles est le même dans toutes les définitions.
Comparez les programmes suivants :
| Code : | Sélectionner tout |
1 2 3 4 5 6 7 8 9 | do {
do {
blue ( ) ;
} while (A ( ) ) ;
} while ( B ( ) ) ;
do {
blue ( ) ;
} while (A( ) | | B ( ) ) ;
return ; |
3 Erreurs courantes concernant la structure des boucles
3.1 Entrée dans les boucles
E Les boucles ont un bord d'entrée. Si deux ou plusieurs chemins de contrôle fusionnent à l'entrée de la boucle et qu'il n'y a pas de noeud de fusion explicite, il est possible d'avoir plusieurs bords d'entrée. Considérons le programme suivant et son CFG donné dans la Figure 3 :
| Code : | Sélectionner tout |
1 2 3 4 5 6 | if ( choose ( ) ) green ( ) ; else orange ( ) ; while ( choose ( ) ) purple ( ) ; |
E Tous les bords d'entrée vont au même endroit. Le langage C et certains autres langages permettent d'écrire des boucles avec plusieurs points d'entrée. Sans doute une "caractéristique" involontaire du langage, les étiquettes utilisées par les instructions de commutation sont des étiquettes normales et peuvent apparaître dans d'autres structures de flux de contrôle. Duff [8, 13] s'en est servi pour fournir une version manuelle du déroulement des boucles pour les anciens compilateurs et le matériel :
| Code : | Sélectionner tout |
1 2 3 4 5 6 7 8 | switch ( n & 0 x3 ) {
do {
case 0 : dest [ i ++] = src [ j ++] ;
case 1 : dest [ i ++] = src [ j ++] ;
case 2 : dest [ i ++] = src [ j ++] ;
case 3 : dest [ i ++] = src [ j ++] ;
} while ( j < n ) ;
} |
E Les points d'entrée multiples d'une boucle peuvent être corrigés par un déroulement. Comme les points d'entrée n'affectent que la première itération, une solution tentante consiste à dérouler la première itération de toute boucle comportant des points d'entrée multiples. Dans la plupart des cas, il s'agit d'une solution simple et raisonnablement efficace. Cependant, [6, 15] montrent qu'il existe des cas pathologiques qui entraînent une augmentation exponentielle de la taille.
E La première instruction doit être un emplacement d'entrée. Il est possible qu'il n'y ait pas d'entrée à la première instruction évidente, et que l'entrée provienne de l'intérieur d'une boucle imbriquée.
| Code : | Sélectionner tout |
1 2 3 4 5 6 7 8 9 10 11 | if ( choose ( ) ) goto one ;
else if ( choose ( ) ) goto two ;
else goto three ;
while ( choose ( ) ) {
while ( choose ( ) ) {
red ( ) ;
one : orange ( ) ;
two : yellow ( ) ;
three : green ( ) ;
}
} |
3.2 Boucles internes
E Les boucles ont un contenu. Dans toutes les représentations, il est possible de créer une boucle vide. Par exemple, les...
La fin de cet article est réservée aux abonnés. Soutenez le Club Developpez.com en prenant un abonnement pour que nous puissions continuer à vous proposer des publications.