Idées fausses sur les boucles en C et recommandations, car les cas de boucles sont plus fréquents que prévu dans le code fourni par l'utilisateur, par Martin Brain et Mahdi Malkawi

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 - Visualiser dans une fenêtre à part
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 ;
}
Ce code possède toutes les caractéristiques classiques d'une boucle [19] :
  1. Le programme vérifie d'abord la condition de la boucle. . .
  2. . ... qui est le seul moyen de sortir de la boucle.
  3. Si la condition est vraie, le corps de la boucle est exécuté.
  4. 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.

Nom : 2.jpg
Affichages : 28839
Taille : 24,4 Ko

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 - Visualiser dans une fenêtre à part
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
Le premier saut est conditionnel, le second est inconditionnel et constitue un saut en arrière puisque la cible se trouve plus tôt dans la liste.

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 - Visualiser dans une fenêtre à part
1
2
3
4
5
do {
open_ socke t ( ) ;
if (connect ( ) == SUCCESS ) { break ; }
close _ socket ( ) ;
} while ( 1 ) ;
Dans les langues disposant d'autres moyens de sortir d'une boucle, les conditions syntaxiques de boucle sont suffisantes mais pas nécessaires pour terminer la boucle. Les autres voies doivent être détectées et ajoutées pour raisonner précisément sur la sortie de la boucle. Voir la section 3.3 pour plus de détails sur les subtilités impliquées.

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 - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
while (A( ) && B ( ) ) {
green ( ) ;
}
while (A ( ) ) {
i f (!B ( ) ) { break ; }
green ( ) ;
}
Les CFG sont équivalents, mais les conditions de boucle de l'arbre de parse sont {A && B } et {A} (ou {A,B} s'ils sont augmentés comme ci-dessus).

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 - Visualiser dans une fenêtre à part
1
2
3
4
5
while (A( ) | | B ( ) | | C ( ) ) {
if (D ( ) ) { break ; }
pink ( ) ;
if ( E ( ) ) { break ; }
}
Ici, {C, D, E } seraient des "conditions de boucle CFG" mais {A || B || C} (et éventuellement D et E) seraient des conditions de boucle de l'arbre de parse.

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 - Visualiser dans une fenêtre à part
1
2
3
4
5
while ( choose ( ) ) {
if ( choose ( ) ) { red ( ) ; break ; }
else if ( choose ( ) ) { goto out ; }
}
if ( 0 ) { out : blue ( ) ; }
Dans la représentation de l'arbre d'analyse, le rouge est dans le corps de la boucle et le bleu ne l'est pas. Le CFG de la figure 2 montre que ni le rouge ni le bleu ne sont dans la boucle puisqu'ils ne peuvent pas s'atteindre eux-mêmes. Ils sont également largement indiscernables, ce qui suggère que la notion de corps de boucle de l'arbre de parse n'est pas exprimable dans le CFG.

Nom : 3.jpg
Affichages : 1689
Taille : 55,2 Ko

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 - Visualiser dans une fenêtre à part
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 ;
Dans la représentation en liste, goto B donne un saut en arrière, mais dans la représentation en CFG, ce n'est pas un bord arrière.

E Le nombre de boucles est le même dans toutes les définitions.

Comparez les programmes suivants :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
do {
do {
blue ( ) ;
} while (A ( ) ) ;
} while ( B ( ) ) ;
do {
blue ( ) ;
} while (A( ) | | B ( ) ) ;
return ;
Dans la représentation en arbre d'analyse, l'exemple de gauche a deux boucles alors que celui de droite n'en a qu'une. Cependant, dans la représentation CFG, les deux ont une boucle naturelle.


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 - Visualiser dans une fenêtre à part
1
2
3
4
5
6
if ( choose ( ) )
green ( ) ;
else
orange ( ) ;
while ( choose ( ) )
purple ( ) ;
Nom : 4.jpg
Affichages : 1688
Taille : 40,8 Ko

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 - Visualiser dans une fenêtre à part
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 ) ;
}
L'implémentation des coroutines de Simon Tatham utilise une version plus avancée de la même idée [22]. Des études suggèrent que les cycles avec des points d'entrée multiples sont rares [20].

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 - Visualiser dans une fenêtre à part
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 boucles "busy-wait" pour la communication inter-thread à faible latence :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
void busy_wait ( void ) {
while ( zero _ to _ unlock ) ;
return ;
}
SV-COMP[1] et d'autres [7] utilisent des boucles vides pour mettre fin à un chemin d'analyse

E L'emplacement d'entrée est un test pour sortir de la boucle. Le langage C et de nombreux autres langages ont une construction syntaxique où cela n'est pas vrai ; la boucle do/while :

Il est tentant de penser que le marquage des boucles do/while ou le fait de dérouler la boucle une fois rendra cette croyance vraie. Il existe un certain nombre de cas moins évidents où cela n'est pas vrai. Selon que les appels de fonction, les contrôles de validité des pointeurs, les modifications de variables, etc. nécessitent des instructions séparées, il se peut que cela ne commence pas par une sortie conditionnelle :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
while (  f00 (( pointer + + ) ) == value )
yellow ( ) ;
Il s'agit également d'un cas où l'inlining peut entraîner des changements significatifs dans les propriétés de la boucle (voir section 3.4).

E La fin d'une boucle est un saut inconditionnel. Seules les représentations en arbre d'analyse et en liste ont un concept de dernière instruction. Dans la représentation en liste, la dernière instruction doit être un saut en arrière pour qu'il s'agisse d'une boucle, mais elle peut être conditionnelle, par exemple dans la boucle do/while.

E Il n'y a qu'un seul saut en arrière ou bord arrière. Dans la représentation en liste, cela dépend si continue est implémenté comme un saut à la fin ou comme un saut au début :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
while ( choose ( ) ) {
pink ( ) ;
i f ( choose ( ) ) { continue ; }
blue ( ) ;
}
Certains langages ont des instructions de flux de contrôle pour "refaire cette itération de boucle (sans tester la condition de la boucle)". Perl et Ruby ont le mot-clé redo, utile pour l'itération sur des structures de données ou des flux où il n'y a pas forcément de moyen d'annuler la mise à jour du compteur de la boucle. L'implémentation la plus simple consiste à utiliser des bords arrière supplémentaires.

E Les boucles peuvent avoir plusieurs bords arrière, mais ils vont tous au même endroit. Dans les boucles imbriquées, le bord arrière de la boucle interne apparaîtra comme un bord arrière au milieu de la boucle externe.

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
while ( choose ( ) ) {
while ( choose ( ) ) {
yellow ( ) ;
}
}


3.3 Sortir d'une boucle

E Les boucles ont une sortie. Des boucles infinies peuvent se produire et se produisent dans un code correct. Les systèmes pilotés par des événements et certains systèmes de contrôle ont souvent une boucle de contrôle principale sans sortie.

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
do {
handle _ request ( ) ;
} while ( 1 ) ;
E Les boucles ont un seul bord de sortie. La rupture offre un moyen simple d'avoir plusieurs bords de sortie au même endroit :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
while ( choose ( ) ) {
orange ( ) ;
if ( choose ( ) ) { break ; }
pink ( ) ;
}
E Toutes les instructions de rupture vont au même endroit. Une conséquence subtile de l'exemple de la figure 2 est que la boucle CFG se termine dès qu'une instruction break est inévitable, et non pas au moment du break. Les instructions situées entre les instructions if et break sont les emplacements de sortie proprement dits. La boucle suivante comporte trois points de sortie, un pour chaque interruption et un pour la condition de la boucle :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
10
11
12
13
for ( int i = 0 ; i < firewall −> rule _ count ; ++ i ) {
if ( firewall −> rule [ i ] . matches ( packet ) ) {
if ( firewall −> rule [ i ] . type == WHITELIST ) {
packet.status = ACCEPTED; / / 1st exit location
break ;
}
else if ( firewall −> rule [ i ] . type == BLACKLIST ) {
packet.status = REJECTED ; / / 2nd exit location
break ;
}
}
}
/ / 3rd exit location
En fait, cela insère du code "après" la sortie de la boucle lorsque l'on utilise l'instruction break, mais pas lorsque l'on sort par la condition de la boucle. Python supporte les instructions else attachées aux boucles pour résoudre cette asymétrie. Une autre version de ce problème survient lorsque la boucle contient plusieurs champs de déclaration de variables et que le langage source ou intermédiaire exige des actions à la fin du champ (marquage de variables mortes, destructeurs C++, etc.). Un break peut avoir besoin d'effectuer des actions de fin de portée alors que la condition de la boucle n'en a pas besoin puisqu'elle se situe avant le début de la portée.

E Les boucles ne peuvent sortir qu'en utilisant la condition de boucle ou le break. L'instruction return fournit un troisième type d'emplacement de sortie qui n'est pas le même que la condition de boucle ou le break :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
while ( choose ( ) ) {
orange ( ) ;
i f ( choose ( ) ) { return ; }
pink ( ) ;
}
E Les boucles ne peuvent être quittées qu'à l'aide de la condition de boucle, du break ou du return. De nombreux langages permettent aux instructions break de spécifier la profondeur des boucles imbriquées qu'elles quittent. Kosaraju [12] montre que cela est essentiel pour prouver une version du théorème de programmation structurée qui ne nécessite pas de variables supplémentaires. On peut donc affirmer qu'il s'agit d'un énoncé fondamental du flux de contrôle. Le langage C ne dispose pas de break to label, ce qui fait qu'il est considéré comme l'une des utilisations légitimes de goto, par exemple :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
10
11
for ( unsigned int i = 0 ; i < WIDTH; ++ i ) {
for ( unsigned int j = 0 ; j < HEIGHT ; ++ j ) {
for ( unsigned int k = 0 ; k < DEPTH; ++k ) {
if ( next _ cell ( i , j , k ) ) { continue ; }
else if ( next_column ( i , j , k ) ) { break ; }
else if ( next_row ( i , j , k ) ) { goto nextRow ; }
else process _ cell ( i , j , k ) ;
}
}
nextRow : ;
}
Une autre utilisation légitime de goto est la création de plusieurs chemins de retour avec différentes stratégies de désallocation des ressources et de traitement des erreurs. Il s'agit d'un schéma courant dans le noyau Linux, qui permet d'obtenir des emplacements de sortie supplémentaires. L'exemple suivant offre un certain degré de robustesse contre les erreurs de programmation, car les branches et les conditions non gérées sont renvoyées par défaut vers le chemin de sortie de l'erreur :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
struct subsys ∗ s = k alloc ( size of ( struct subsys ) ) ;
int err = subsys _ init ( s , parameters , policy ) ;
if ( err ) { goto fail _ subsys ; }
for ( unsigned int i = 0 ; i < s −>hook_count ; ++ i ) {
err = subsys _ register _ hook ( s , i ) ;
if ( err ) { goto fail _ hook ; }
}
if ( subsytem_ status ( s ) == FUNCTIONAL)
{ goto success ; }
fail _ hook : subsys _ unregister _ hooks ( ) ;
fail _ subsys : kfree ( s ) ;
klog ( " Failed ␣ to ␣ configure ␣ subsys ␣%d " , err ) ;
return false ;
success :
klog ( " Subsys ␣%s ␣ configured ␣ with ␣%d ␣ hooks " ,
s −> identifier , s −>hook_count ) ;
return true ;
Certains langages disposent d'instructions de flux de contrôle supplémentaires qui fournissent d'autres emplacements de sortie différents, par exemple pour les gestionnaires d'exception.


3.4 Simplification, prétraitement et optimisation

E Les simplifications n'affectent pas l'analyse des boucles. Le raisonnement sémantique peut modifier les résultats de l'analyse des boucles. Par exemple, un modèle courant pour forcer une macro à être utilisée comme une instruction exige qu'une boucle do/while "avale" le point-virgule :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
# define INIT_SUBSYSTEM(X) do { \
bzero ( ( X) , size of ( struct subsystem ) ) ; \
load _ system_ config ( ( X ) ) ; \
register _ subsystem ( ( X ) ) ; \
} while ( 0 )
INIT_SUBSYSTEM( networking ) ;
La question de savoir si cette boucle est considérée comme telle dépend du type et de la quantité de simplification effectuée avant l'analyse de la boucle.

E La simplification n'affecte que les décisions relatives aux arêtes de contrôle. L'exemple précédent peut être traité lors de la construction du CFG en omettant les arêtes qui ne peuvent pas être prises. Malheureusement, toutes les simplifications ne sont pas aussi simples :

Code : Sélectionner tout - Visualiser dans une fenêtre à part
1
2
3
4
5
6
7
8
#define POINTER_RW( p ) do { ∗ ( p ) = ∗ ( p ) ; } while ( 0 )
do {
POINTER_RW( p ) ;
do {
some_code ( p ) ;
} while ( condition1 ( ) ) ;
p = p−> next ;
} while ( p ! = null ) ;
Si p est toujours une adresse accessible, POINTER_RW peut être supprimé, de sorte qu'il n'y a qu'une seule boucle CFG au lieu de deux. L'effet inverse est également possible ; l'ajout d'instructions ou d'instrumentation au début des corps de boucle peut augmenter le nombre de boucles.

E Le prétraitement peut modifier le nombre de boucles, mais pas les créer à partir de rien. Selon les exigences du langage et l'endroit du processus de compilation où l'analyse des boucles est effectuée, cela peut ne pas être vrai. Si le langage exige que les fonctions récursives de queue soient réécrites, il est possible que des boucles "apparaissent" dans une fonction acyclique (mais récursive).

E L'incrustation est inoffensive. L'intégration permet de simuler l'analyse contextuelle afin de simplifier potentiellement le traitement des petites fonctions utilitaires et du "sucre syntaxique". Lors de l'incrustation, les instructions de retour agissent comme une forme légèrement restreinte d'instructions goto en avant. Le retour est remplacé par un saut dans le contexte d'appel. Cela peut donner des sorties de boucle qui sont à une distance significative de la boucle, qui peuvent ou non fusionner avec le contrôle de flux de la boucle et qui ne sont pas facilement reconnues comme un cas spécial comme le sont les instructions de retour normales. Si l'outil effectue un inlining, de nombreuses intuitions des développeurs, "Cela fonctionne tant que les programmes d'entrée n'ont pas de goto", ne sont plus valables. De nombreuses utilisations de goto dans le présent document peuvent être simulées avec des instructions de retour en ligne1.

E Le threading de saut est inoffensif. Si une instruction de saut cible un second saut inconditionnel, elle peut être redirigée pour sauter directement à la cible de . Dans la plupart des cas, cela simplifie le CFG résultant, mais cela peut interagir de manière inattendue avec d'autres étapes de prétraitement et annuler d'autres simplifications. Par exemple, si continue est implémenté comme un saut à la fin du corps de la boucle (voir section 3.2), alors le threading de saut peut les transformer en bords arrière supplémentaires. Si l'instruction qui suit un appel de fonction est un saut, l'inlining et le jump threading peuvent créer un goto de n'importe quel endroit de l'appelant à n'importe quel endroit de l'appelant.


4 Recommandations

Face aux bizarreries et aux cas limites décrits dans le présent document, une réaction raisonnable consiste à se demander s'ils sont courants. D'après notre expérience, les cas limites de boucle sont plus fréquents que prévu dans le code fourni par l'utilisateur. Les sources incluent le code compilé à partir de langages avec des constructions de flux de contrôle non-C comme le for-else de Python, la boucle d'Ada ou les instructions de rupture imbriquées, le code autogénéré à partir de DSL (comme Simulink), les combinaisons d'étapes de prétraitement, comme l'inline, l'accélération de boucle, le déroulement puis la simplification, le code hérité, le code haute performance optimisé à la main, le code optimisé décompilé, en particulier le déroulement de boucle, le fractionnement, la fusion et les optimisations de disposition i-cache, et le code décompilé obfusqué.

Lorsqu'un outil devient prospère, les risques de rencontrer un ou plusieurs cas limites augmentent considérablement. Nous recommandons donc les étapes suivantes :

  1. Concevoir pour le cas le plus général. Par exemple, si vous utilisez les définitions CFG d'une boucle, l'API doit renvoyer l'ensemble des emplacements d'entrée et l'ensemble (éventuellement vide) des emplacements de sortie. Il est possible d'avoir des appels plus spécifiques tels que l'obtention de l'emplacement d'entrée ou de la condition de sortie, mais ceux-ci doivent au moins comporter une vérification de l'exécution pour s'assurer que la boucle se présente sous la forme requise.
  2. Indiquer explicitement les cas qui ne sont pas traités. Il est raisonnable de ne pas traiter initialement les boucles irréductibles ou de les traiter avec un algorithme exponentiel naïf. Toutefois, cela doit être explicitement vérifié lors de l'exécution et documenté pour l'utilisateur. Il est fortement préférable d'étendre la prise en charge en ajoutant des cas supplémentaires plutôt que d'avoir un algorithme complet pour certaines boucles et d'ajouter des étapes de réécriture avant et après pour étendre l'ensemble des boucles prises en charge.
  3. Si votre système utilise plus d'une représentation, la gestion de la traduction entre elles doit faire partie de la conception. Par exemple, un système qui génère des invariants de boucle d'arbre source/parse à l'aide d'une technique basée sur le CFG devra suivre la correspondance entre les deux définitions de boucle. Une approche consiste à annoter les concepts de l'arbre d'analyse tels que le corps de la boucle et les conditions de la boucle dans le CFG, mais il faut veiller à les préserver (voir section 3.4).
  4. Le code d'analyse des boucles doit être testé soigneusement et systématiquement en tenant compte des cas limites possibles. Les exemples donnés dans ce document sont disponibles sous la forme d'une suite de tests [5]. Chaque programme est un test minimal pour la question spécifique, avec une entrée unique qui contrôle le chemin emprunté par le programme, fournissant une sortie unique qui enregistre les branches empruntées. Cela peut être utilisé pour des tests dos à dos avec des compilateurs, des interprètes, des traductions source à source ou des outils d'analyse dynamique. Si la relation entrée/sortie change, la transformation est boguée et insère ou omet des arêtes. Pour tester les outils d'analyse statique, les programmes contiennent également des assertions qui ne sont vraies que pour les chemins valides à travers le programme. Si une assertion échoue, cela indique un bogue dans l'outil d'analyse statique. Nous fournissons une configuration utilisable pour tester les exemples fournis avec CBMC.



Remerciements

La recherche présentée dans cette publication a été soutenue par une bourse de recherche Amazon, automne 2022 CFP. Les opinions, résultats et conclusions ou recommandations exprimés dans ce document sont ceux de l'auteur ou des auteurs et ne reflètent pas les opinions d'Amazon.

Les exemples présentés dans ce document ont été rassemblés sur une longue période, à partir de rapports de bogues, de folklore, de cas particuliers découverts au cours du développement, etc. Les auteurs souhaitent remercier toutes les personnes qui ont apporté leur contribution. Dans la mesure du possible, des citations sont fournies. En particulier, Martin Brain souhaite remercier Peter Schrammel pour son modèle de développement, Holly Nyx pour son soutien éditorial et John Galea pour être la personne qui dit "Mais Martin, ça ne marche pas parce que...".

Nom : 1.jpg
Affichages : 2265
Taille : 2,8 Ko
Ce travail est soumis à une licence internationale Creative Commons Attribution 4.0.


References

[1] 2023. Competition on Software Verification (SV-COMP). https://svcomp.sosy-lab.org/

[2] Alfred Vaino Aho, Monica Sin-Ling Lam, Ravi Sethi, and Jeffrey David Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd Edition). Addison Wesley.

[3] Frances Elizabeth Allen. 1970. Control Flow Analysis. 5, 7 (1970). https://doi.org/10.1145/390013.808479

[4] Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. 2015. Safety Verification and Refutation by k-Invariants and k-Induction. In Static Analysis, Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 145–161.

[5] Martin Brain and Mahdi Malkawi. 2024. [artifact] Misconceptions About Loops in C. https://doi.org/10.5281/zenodo.11113582

[6] Larry Carter, Jeanne Ferrante, and Clark Thomborson. 2003. Folklore Confirmed: Reducible Flow Graphs Are Exponentially Larger. SIGPLAN Not. 38, 1 (jan 2003), 106–114. https://doi.org/10.1145/640128.604141

[7] Byron Cook, Björn Döbel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, and Pawel Wieczorkiewicz. 2020. Using model checking tools to triage the severity of security bugs in the Xen hypervisor. In 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020. IEEE, 185–193. https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_26

[8] Tom Duff. 1988. Re: Explanation, please! Usenet. http://doc.catv.org/bell_labs/duffs_device

[9] Paul Havlak. 1997. Nesting of Reducible and Irreducible Loops. ACM Trans. Program. Lang. Syst. 19, 4 (jul 1997), 557–567. https://doi.org/10.1145/262004.262005

[10] Matthew Sterling Hecht and Jeffrey David Ullman. 1974. Characterizations of Reducible Flow Graphs. J. ACM 21, 3 (jul 1974), 367–375. https://doi.org/10.1145/321832.321835

[11] Brian Wilson Kernighan and Dennis MacAlistair Ritchie. 1978. The C Programming Language. Bell Telephone Laboratories Incorporated.

[12] Sambasiva Rao Kosaraju. 1974. Analysis of structured programs. J. Comput. System Sci. 9, 3 (1974), 232–255. https://doi.org/10.1016/S0022-0000(74)80043-7

[13] Chloé Lourseyre. 2021. Duff’s device in 2021. https://belaycpp.com/ 2021/11/18/duffs-device-in-2021/

[14] Daniel Neville, Andrew Malton, Martin Brain, and Daniel Kroening. 2016. Towards automated bounded model checking of API implementations. CEUR Workshop Proceedings 1639, 31–42.

[15] Carl D. Offner. 2013. Notes on graph algorithms used in optimizing compilers. Technical Report. University of Massachusetts Boston. https://www.cs.umb.edu/~offner/files/flow_graph.pdf

[16] Florian Schanda and Martin Brain. 2012. Using Answer Set Programming in the Development of Verified Software. In Technical Communications of the 28th International Conference on Logic Programming (ICLP’12) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 17), Agostino Dovier and Vítor Santos Costa (Eds.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 72–85. https://doi.org/10.4230/LIPIcs.ICLP.2012.72

[17] Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, and Tom Bienmüller. 2015. Successful Use of Incremental BMC in the Automotive Industry. In Formal Methods for Industrial Critical Systems, Manuel Núñez and Matthias Güdemann (Eds.). Springer International Publishing, Cham, 62–77.

[18] Peter Schrammel, Daniel Kroening, Martin Brain, Ruben Martins, Tino Teige, and Tom Bienmüller. 2017. Incremental Bounded Model Checking for Embedded Software. Form. Asp. Comput. 29, 5 (sep 2017), 911–931. https://doi.org/10.1007/s00165-017-0419-1

[19] Kaitlyn Siu and Marcelo Badari. 2022. What’s A Loop : A Tree House Adventure. Wayland.

[20] James Stanier and Des Watson. 2012. A Study of Irreducibility in C Programs. Softw. Pract. Exper. 42, 1 (jan 2012), 117–130. https://doi.org/10.1002/spe.1059

[21] Youcheng Sun, Martin Brain, Daniel Kroening, Andrew Hawthorn, Thomas Wilson, Florian Schanda, Francisco Javier Guzmán Jiménez, Simon Daniel, Chris Bryan, and Ian Broster. 2017. Functional Requirements-Based Automated Testing for Avionics. In 2017 22nd International Conference on Engineering of Complex Computer Systems (ICECCS). 170–173. https://doi.org/10.1109/ICECCS.2017.18

[22] Simon Tatham. 2000. Coroutines in C. https://www.chiark.greenend.org.uk/~...oroutines.html

[23] Tomoya Yamaguchi, Martin Brain, Chirs Ryder, Yosikazu Imai, and Yoshiumi Kawamura. 2019. Application of Abstract Interpretation to the Automotive Electronic Control System. In Verification, Model Checking, and Abstract Interpretation, Constantin Enea and Ruzica Piskac (Eds.). Springer International Publishing, Cham, 425–445.
Received 03-MAR-2024; accepted 2023-04-19; accepted 3 May 2024

Source : Misconceptions about Loops in C

Et vous ?

Quel est votre avis sur le sujet ?

Voir aussi :

C23 : un C légèrement meilleur. Le langage de programmation C continue d'évoluer, lentement et prudemment, par Daniel Lemire

Les différentes façons de gérer les erreurs en C, le C ne dispose pas d'une seule façon claire pour gérer les erreurs