In der Programmanalyse ist die Strukturanalyse eine statische Codeanalysetechnik , die Eigenschaften von verknüpften , dynamisch allokierten Datenstrukturen in (meist imperativen ) Computerprogrammen aufdeckt und überprüft. Sie wird typischerweise zur Kompilierzeit eingesetzt, um Softwarefehler zu finden oder die Korrektheit von Programmen auf höherer Ebene zu verifizieren. In Java -Programmen kann sie beispielsweise verwendet werden, um sicherzustellen, dass eine Sortiermethode eine Liste korrekt sortiert. In C -Programmen sucht sie nach Stellen, an denen ein Speicherblock nicht ordnungsgemäß freigegeben wird.

Anwendungen

Die Formanalyse wurde auf eine Vielzahl von Problemen angewendet:

  • Speichersicherheit: Auffinden von Speicherlecks , Dereferenzierungen von hängenden Zeigern und Aufdecken von Fällen, in denen ein Speicherblock mehr als einmal freigegeben wird. [ 1 ] [ 2 ]
  • Fehler beim Auffinden von Array-Bereichsüberschreitungen
  • Überprüfung von Typ-Status-Eigenschaften (z. B. Sicherstellen, dass eine Datei vorhanden ist, open()bevor sie gelöscht wird read())
  • Sicherstellen, dass eine Methode zum Umkehren einer verketteten Liste keine Zyklen in die Liste einführt [ 2 ].

Beispiel

Die Formanalyse ist eine Form der Zeigeranalyse , allerdings präziser als die typische Zeigeranalyse. Die Zeigeranalyse versucht, die Menge der Objekte zu bestimmen, auf die ein Zeiger zeigen kann (die sogenannte Zielmenge des Zeigers). Leider sind diese Analysen notwendigerweise approximativ (da eine perfekt präzise statische Analyse das Halteproblem lösen könnte ). Die Formanalyse kann kleinere (präzisere) Zielmengen bestimmen.

Betrachten Sie das folgende einfache C++- Programm. 

Artikel * Artikel [ 10 ];for ( int i = 0 ; i < 10 ; ++ i ) { items [ i ] = new Item (...); // Zeile [1] }process_items ( items ); // Zeile [2]for ( int i = 0 ; i < 10 ; ++ i ) { delete items [ i ]; // Zeile [3] }

Dieses Programm erstellt ein Array von Objekten, verarbeitet diese auf beliebige Weise und löscht sie anschließend. Unter der Annahme, dass die process_itemsFunktion fehlerfrei ist, ist das Programm sicher: Es greift niemals auf freigegebenen Speicher zu und löscht alle erstellten Objekte.

Leider haben die meisten Zeigeranalysen Schwierigkeiten, dieses Programm präzise zu analysieren. Um die Zeigermengen zu bestimmen, muss eine Zeigeranalyse die Objekte eines Programms benennen können . Programme können im Allgemeinen eine unbegrenzte Anzahl von Objekten allokieren; für die Terminierung kann eine Zeigeranalyse jedoch nur eine endliche Menge von Namen verwenden. Eine gängige Näherung besteht darin, allen Objekten, die in einer bestimmten Programmzeile allokiert werden, denselben Namen zu geben. Im obigen Beispiel hätten alle in Zeile [1] erzeugten Objekte denselben Namen. Daher stellt die deleteAnalyse bei der ersten Ausführung der Anweisung fest, dass eines der Objekte mit dem Namen [1] gelöscht wird. Bei der zweiten Ausführung (da sich die Anweisung in einer Schleife befindet) warnt die Analyse vor einem möglichen Fehler: Da sie die Objekte im Array nicht unterscheiden kann, könnte es sein, dass beim zweiten Mal deletedasselbe Objekt gelöscht wird wie beim ersten Mal delete. Diese Warnung ist jedoch unbegründet, und das Ziel der Formanalyse ist es, solche Warnungen zu vermeiden.

Zusammenfassung und Materialisierung

Die Formanalyse überwindet die Probleme der Zeigeranalyse durch ein flexibleres Benennungssystem für Objekte. Anstatt einem Objekt im gesamten Programm denselben Namen zu geben, können Objekte ihre Namen je nach Programmaktion ändern. Manchmal werden mehrere unterschiedliche Objekte mit verschiedenen Namen zusammengefasst oder zusammengeführt, sodass sie denselben Namen tragen. Wenn ein zusammengefasstes Objekt vom Programm verwendet werden soll, kann es materialisiert werden – das heißt, das zusammengefasste Objekt wird in zwei Objekte mit unterschiedlichen Namen aufgeteilt: eines repräsentiert ein einzelnes Objekt, das andere die verbleibenden zusammengefassten Objekte. Die grundlegende Heuristik der Formanalyse besteht darin, dass vom Programm verwendete Objekte durch eindeutige materialisierte Objekte repräsentiert werden, während nicht verwendete Objekte zusammengefasst werden.

Das Objektarray im obigen Beispiel wird in den Zeilen [1], [2] und [3] auf unterschiedliche Weise zusammengefasst. In Zeile [1] ist das Array erst teilweise aufgebaut. Die Array-Elemente 0 bis i-1 enthalten bereits aufgebaute Objekte. Das Array-Element i wird gerade aufgebaut, und die folgenden Elemente sind noch nicht initialisiert. Die Formanalyse kann diese Situation approximieren, indem sie eine Zusammenfassung für die ersten Elemente, eine materialisierte Speicheradresse für Element i und eine Zusammenfassung für die verbleibenden, nicht initialisierten Adressen verwendet, wie folgt:

0 .. i−1 ich i+1 .. 9
Zeiger auf konstruiertes Objekt (Zusammenfassung) nicht initialisiert nicht initialisiert (Zusammenfassung)

Nach Beendigung der Schleife in Zeile [2] ist es nicht mehr nötig, etwas materialisiert zu halten. Die Formanalyse stellt an dieser Stelle fest, dass alle Array-Elemente initialisiert wurden:

0 .. 9
Zeiger auf konstruiertes Objekt (Zusammenfassung)

In Zeile [3] wird das Array-Element jedoch ierneut verwendet. Daher teilt die Analyse das Array wie in Zeile [1] in drei Segmente auf. Diesmal iwurde jedoch das erste Segment davor gelöscht, und die verbleibenden Elemente sind weiterhin gültig (vorausgesetzt, die deleteAnweisung wurde noch nicht ausgeführt).

0 .. i−1 ich i+1 .. 9
kostenlos (Zusammenfassung) Zeiger auf das konstruierte Objekt Zeiger auf konstruiertes Objekt (Zusammenfassung)

Beachten Sie, dass die Analyse in diesem Fall erkennt, dass der Zeiger an der Indexposition inoch nicht gelöscht wurde. Daher wird keine Warnung vor einer doppelten Löschung ausgegeben.

Siehe auch

Referenzen

  1. ^ Rinetzky, Noam; Sagiv, Mooly (2001). „Interprozedurale Formanalyse für rekursive Programme“ (PDF) . Compilerbau . Lecture Notes in Computer Science. Band 2027. S.  133–149 . doi : 10.1007/3-540-45306-7_10 . ISBN 978-3-540-41861-0Die
  2. ^ a b Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; o'Hearn, Peter W.; Wies, Thomas; Yang, Hongseok (2007). „Shape Analysis for Composite Data Structures“ (PDF) . Computer Aided Verification . Lecture Notes in Computer Science. Band 4590. S.  178–192 . doi : 10.1007/978-3-540-73368-3_22 . ISBN 978-3-540-73367-6Die

Bibliographie

  • Neil D. Jones; Steven S. Muchnick (1982). „Ein flexibler Ansatz zur Analyse des interprozeduralen Datenflusses und von Programmen mit rekursiven Datenstrukturen“. Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages ​​- POPL '82 . ACM. S.  66–74 . doi : 10.1145/582153.582161 . ISBN 0897910656S2CID  13266723 .​
  • Wilhelm, Reinhard; Sagiv, Mooly; Reps, Thomas (2007). „Kapitel 12: Formanalyse und Anwendungen“. In: Srikant, Y. N.; Shankar, Priti (Hrsg.). The Compiler Design Handbook: Optimizations and Machine Code Generation, Zweite Auflage . CRC Press. S. 12–1–12–44. ISBN 978-1-4200-4382-2Die