Eine sehr effektive Möglichkeit zur automatischen Testgenerierung ist die Symbolische Ausführung eines Programms, bei der alle möglichen Ausführungspfade und deren Bedingungen rein durch Analyse des Programmcodes ermittelt werden, ohne dass das Programm tatsächlich ausgeführt werden muss. Die Analyseergebnisse können zur Generierung von Testfällen mit hoher Testabdeckung genutzt werden. Darüber hinaus deckt die Symbolische Ausführung auch Fehlerklassen wie beispielsweise Zugriffe auf nicht initialisierte Objekte, fehlerhafte Indexzugriffe oder Überläufe ab. Für diese können ebenfalls gezielt Testfälle generiert werden, um diese Fehler mit konkreten Werten nachvollziehbar zu machen.
Erreicht wird das, indem für alle Pfade durch das Programm eine Pfadbedingung berechnet wird. Diese Pfadbedingung ist ein logischer Ausdruck, der die Voraussetzungen angibt, unter denen der Pfad erreicht werden kann. Mithilfe eines Constraint-Solvers können für die Pfadbedingungen dann konkrete Werte – die Testdaten – berechnet und so ausführbare Testfälle für alle möglichen Pfade erzeugt werden.
Symbolischen Ausführung anhand eines Beispiels
Wie Symbolische Ausführung arbeitet, lässt sich anhand eines einfachen Beispiels veranschaulichen. Listing 1 zeigt die Methode get AveragePoints() der Klasse Exam, die getestet werden soll. Die Methode enthält durch die Verzweigung und die Schleife mehrere Pfade sowie arithmetische Berechnungen. Am Ende wird eine Division durchgeführt.
Listing 1: Methode getAveragePoints() der Klasse Exam
Mit Symbolischer Ausführung können wir ermitteln, mit welchen Werten für die Variable students die Pfade der Methode erreicht werden können und ob dabei Probleme auftreten können. Abbildung 1 veranschaulicht, wie die Programmpfade mit Symbolischer Ausführung berechnet werden.
Abb. 1: Berechnung von Programmpfaden mit Symbolischer Ausführung
Listing 2 zeigt die resultierenden Testfälle, die mit Werkzeugen wie Symflower [SymF] auf Basis Symbolischer Ausführung generierten werden können.
Listing 2: Resultierenden Testfälle, die auf Basis Symbolischer Ausführung generierten werden können
Als Erstes wird die If-Abfrage analysiert. Die Ausführung teilt sich hier bereits in zwei mögliche Pfade: einen, in dem die Bedingung students == null erfüllt ist, und einen, in dem diese Bedingung nicht erfüllt ist. Im ersten Fall wird die Bedingung, um den Pfad zu betreten, als Pfadbedingung gesetzt. Das folgende return-Statement bedeutet das Ende dieses Pfads und der Constraint-Solver wird mit der Pfadbedingung aufgerufen. Der Solver liefert die Lösung students = null, womit der Testfall getAverage-Points1() generiert werden kann.
Im False-Pfad wird als Nächstes die Variable sum mit 0 initialisiert und die Pfadbedingung entsprechend ergänzt. Danach kommt die For-Schleife, welche bei der Symbolischen Ausführung aufgerollt wird, indem die Zählvariable i und die Schleifenbedingung i < students.length eingeführt werden.
Wird die Schleife nicht betreten, kommt als nächste Anweisung eine Division. Falls dabei der Nenner null ist, tritt der Fehler Division durch null auf. Deshalb wird eine entsprechende Pfadbedingung ergänzt. Der Solver findet die Lösung für diesen Pfad – ein leeres Array – und der Testfall getAverage-Points2(), der die Division durch null aufzeigt, wird generiert.
Anschließend wird der Pfad geprüft, in dem die Schleife betreten wird. Dort wird die Variable s auf das erste Element des Arrays gesetzt. Der Zugriff auf s kann eine Null-PointerException verursachen. Darum wird hier der Pfad erneut geteilt und geprüft, ob s = null sein kann. Der Solver findet eine Lösung, die zu einer NullPointer Exception führt, indem das erste Element in students = null gesetzt wird; siehe Testfall getAveragePoints3().
Im Pfad s != null wird dann die Summe sum berechnet. Gilt sum = 0, kommt es zu keinem Überlauf und die Analyse wird fortgesetzt. Die Zählvariable wird erhöht und die Schleifenbedingung geprüft. Dies führt erneut zu einer Verzweigung, die Pfadbedingung wird erweitert, der Solver findet dafür eine Lösung mit einem Student-Objekt mit null Punkten und der Testfall getAverage Points4() wird generiert.
Damit wurden alle Zeilen der Methode abgedeckt, allerdings noch nicht ein möglicher Überlauf bei der Addition. Die Schleife wird daher weiter ausgeführt, die Variable s wird auf das zweite Element gesetzt und die Addition erneut durchgeführt. Der Solver findet in dieser Konstellation eine Lösung, die einen Überlauf verursacht: Mit diesen Werten wird ein weiterer Testfall getAverage-Points5() generiert.
Insgesamt wurden durch Symbolische Analyse damit fünf Testfälle erzeugt, die den Programmcode vollständig abdecken. Drei der Testfälle zeigen eine Fehlersituation auf: Division durch null, Dereferenzierung eines Null-Pointers und Integer-Überlauf. Sie liefern dafür auch konkrete Werte, mit denen diese Fehler nachvollzogen werden können.
Innovationen und Praxistauglichkeit
Die Idee zur Symbolischen Ausführung wurde bereits 1976 von James C. King am IBM Reseach Center beschrieben [Kin76]. Lange Zeit blieb der Ansatz aber auf einfache Beispiele beschränkt und spielte nur in der Forschung eine Rolle. Erst in den letzten Jahren konnten entscheidende Innovationen und Verbesserung erreicht werden, die in Summe der Symbolischen Ausführung zur breiten praktischen Anwendbarkeit verhelfen [Yan19]. Dazu zählen:
Power heutiger Constraint-Solver
Moderne Solver [Bie21] ermöglichen es, Bedingungen zu lösen, die in der Vergangenheit als viel zu komplex gegolten haben. Zum Beispiel nicht-lineare Operationen wie Multiplikation, Division oder komplexe Operationen wie Logarithmen wurden früher nicht oder nur sehr eingeschränkt unterstützt. Dadurch war auch die praktische Anwendbarkeit von Symbolischer Ausführung stark eingeschränkt. Moderne Solver können Bedingungen lösen, die Gleitkommazahlen, String-Operationen und komplexe Datentypen enthalten.
Such-Algorithmen und massiver Anstieg der Rechenleistung
Die Verfügbarkeit massiver Rechenleistung wird oft als wichtiger Durchbruch für den praktischen Einsatz von künstlicher Intelligenz angegeben. Auf ähnliche Weise ermöglicht eine größere Rechenleistung und eine bessere Parallelisierung, sehr viele Pfade in kurzer Zeit zu analysieren, was in der Vergangenheit ein kritischer Flaschenhals für den Einsatz von Symbolischer Ausführung war. Zudem wurden auch effiziente Such-Algorithmen entwickelt, mit denen die Analyse weiter optimiert werden kann.
Auflösen von Abhängigkeiten zu externen Systemen
Die Symbolische Ausführung stieß bei Abhängigkeiten zu externen Komponenten und Bibliotheken regelmäßig an ihre Grenzen, wenn diese nicht in analysierbarer Form (zum Beispiel als Quellcode) verfügbar waren. Mittlerweile gibt es auch dafür praktische Lösungen wie die dynamische Symbolische Ausführung, die solche Programmteile mit konkreten Werten aus der Analyse ausführt und die Ergebnisse für die weitere Analyse verwendet. Zudem werden vermehrt Anstrengungen unternommen, um Pfadbedingungen für gängige Bibliotheken bereits vorzurechnen, damit diese bei der Analyse einfach eingesetzt werden können.
Anwendungsmöglichkeiten von Symbolischer Ausführung
Genannte Neuerungen machen die Symbolische Ausführung für den praktischen Einsatz beim Softwaretest und in der Software-Qualitätssicherung tauglich. Damit ergibt sich eine Reihe von praktischen Anwendungsmöglichkeiten:
Fehlerdetektion und Fehlerlokalisierung
Symbolische Ausführung ermöglicht es, ein weites Spektrum an Fehlerklassen zu finden. Im Gegensatz zu anderen statischen Analyseansätzen liefert dieser Ansatz auch konkrete Werte, mit denen etwaige Fehler nachvollzogen werden können. So können etwa ausführbare Testfälle generiert werden, mit denen sich die Fehler im Debugger Schritt für Schritt nachstellen lassen. Die Fehlerlokalisierung sowie auch die -behebung werden damit deutlich vereinfacht. Falsche Alarme, wie sie bei rein statischer Programmanalyse vorkommen, können vermieden werden.
Prüfung benutzerdefinierter Eigenschaften
Bei Ansätzen wie Property Based Testing werden wichtige (funktionale) Eigenschaften eines Programms vom Tester zum Beispiel in Form von Nachbedingungen spezifiziert. Mittels Symbolischer Ausführung können dann gezielt Testfälle generiert werden, die die angegebenen Eigenschaften verletzen, das heißt, die zu Fehlern führen. Dies ermöglicht es, über die zuvor genannten Fehlerklassen hinaus auch semantische Fehler in Programmen zu finden.
Unterstützung von Refactorings
Die mittels Symbolischer Ausführung generierten Testfälle zeichnen sich durch eine besonders hohe Abdeckung aus. Werden bei jedem generierten Testfall auch die tatsächlichen Ergebniswerte geprüft, so kann mit diesen Testfällen das aktuelle Verhalten einer Anwendung in allen möglichen Ausführungspfaden „eingefroren” werden. Dies unterstützt das Refactoring von Programmen, da unbeabsichtigte Seiteneffekte mit den Tests rasch aufgedeckt werden können.
Testwerkzeuge auf Basis Symbolischer Ausführung
Symbolische Ausführung wird heute von einer Reihe von Testwerkzeugen implementiert. Hervorzuheben sind hier:
- KLEE (C/C++) kommt aus einem langjährigen universitären Forschungsprojekt. Die Symbolische Ausführung operiert auf LLVM bitcode. KLEE ist frei verfügbar und heute in einem Status, der die praktische Anwendung zur Analyse vollständiger Binaries ermöglicht [Klee].
- IntelliTest (C#): Das Testwerkzeug ist als Teil von Microsoft Visual Studio (Enterprise Edition) kommerziell verfügbar und ermöglicht es, automatisiert Unittests für C#-Code zu generieren [MicroS].
- Symflower (Java, Go) basiert auf einem technologieübergreifenden Ansatz, der Symbolische Ausführung von verschiedenen Programmiersprachen ermöglicht; derzeit werden Java und Go unterstützt. Das Werkzeug generiert Unittests, zum Beispiel im weitverbreiteten JUnit-Format. Symflower wird von einem gleichnamigen Start-up entwickelt und ist frei verfügbar [SymF].
Zusammenfassung
Das Potenzial der Symbolischen Ausführung für die Testfallgenerierung ist seit Langem bekannt. Die breite praktische Anwendbarkeit wurde aber erst durch eine Reihe von Innovationen möglich, vor allem rund um moderne Constraint-Solver. Noch vor einigen Jahren scheiterte die Symbolische Ausführung bei Programmen mit komplexen Datenstrukturen und Bedingungen sowie bei Abhängigkeiten zu externen Komponenten.
Heute stehen Entwicklern und Testern mehrere kommerzielle und freie Testwerkzeuge zur Verfügung, die diese Herausforderungen meistern und mittels Symbolischer Ausführung automatisch Testfälle erzeugen können. Die automatisiert generierten Tests bieten eine wertvolle, zusätzliche Unterstützung für die Entwicklung in kurze Sprints, kontinuierliche Integration, Fehlerdetektion und Fehlerlokalisierung sowie beim laufenden Refactoring.
Referenzen
[Bie21]
A. Biere, M. Heule, H. Van Maaren, T. Walsh, Handbook of Satisfiability (2nd Ed.), IOS Press 2021
[Kin76]
J. C. King, Symbolic execution and program testing, in: Commun. ACM 19, 7 (July 1976), 385-394
[Klee]
https://klee.github.io/
[MicroS]
https://docs.microsoft.com/en-us/visualstudio/test/intellitest-manual
[SymF]
https://symflower.com/
[Yan19]
G. Yang, A. Filieri, M. Borges, D. Clun, J. Wen, Advances in symbolic execution, in: Advances in Computers 113 (2019), 225-287
