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 boucles "busy-wait" pour la communication inter-thread à faible latence :
| Code : | Sélectionner tout |
1 2 3 4 | void busy_wait ( void ) {
while ( zero _ to _ unlock ) ;
return ;
} |
| Code : | Sélectionner tout |
loop : goto loop ;
| Code : | Sélectionner tout |
1 2 3 | do {
blue ( ) ;
} |
| Code : | Sélectionner tout |
1 2 | while ( f00 ( ∗ ( pointer + + ) ) == value ) yellow ( ) ; |
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 |
1 2 3 4 5 | while ( choose ( ) ) {
pink ( ) ;
i f ( choose ( ) ) { continue ; }
blue ( ) ;
} |
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 |
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 |
1 2 3 | do {
handle _ request ( ) ;
} while ( 1 ) ; |
| Code : | Sélectionner tout |
1 2 3 4 5 | while ( choose ( ) ) {
orange ( ) ;
if ( choose ( ) ) { break ; }
pink ( ) ;
} |
| Code : | Sélectionner tout |
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 |
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 |
1 2 3 4 5 | while ( choose ( ) ) {
orange ( ) ;
i f ( choose ( ) ) { return ; }
pink ( ) ;
} |
| Code : | Sélectionner tout |
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 : ;
} |
| Code : | Sélectionner tout |
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 ; |
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 |
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 ) ; |
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 |
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 ) ; |
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 :
- 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.
- 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.
- 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).
- 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...".
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.9...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