Join operators for bi-abductive analysis of low-level code

Abstract

Static code analysis plays an important role in ensuring the correctness of program segments or entire programs, often performed using abstract interpretation to generate contracts consisting of pre- and postconditions for code blocks. Here, an ongoing question is how to handle situations where two program paths merge (commonly at the end of conditional branches or loops) and several such contracts are available. Specifically, this question has previously gone unanswered in Broom, a static analysis tool that specializes in analyzing low-level code that operates on linked pointer segments. For that reason, an algorithm capable of joining the formulas generated by Broom is introduced, and its effects on the quality of generated results as well as on the efficiency of the analysis process are studied by comparing contracts generated for a set of representative examples while using this join algorithm to ones generated without. With the conclusions of this evaluation, the parameters for the proposed algorithm are adjusted to get the best possible results.

Statische Codeanalyse spielt eine wichtige Rolle bei der Sicherstellung von Korrektheit bestimmter Programme oder von Segmenten davon. Bewerkstelligt wird dies oft mittels abstrakter Interpretation, bei der Verträge, bestehend aus Vor- und Nachbedingungen, für Codeblöcke generiert werden. Eine in diesem Kontext offene Frage ist, wie Situationen, in denen zwei Programmpfade aufeinandertreffen (häufig am Ende von Fallunterscheidungen oder Schleifen), und in denen mehrere solche Verträge verfügbar sind, gehandhabt werden sollen. So ist diese Frage auch in Broom, einem Werkzeug für die statische Analyse speziell von systemnahem Code, welcher mit verketteten Datenstrukturen arbeitet, bislang unbeantwortet. Aus diesem Grund wird ein Algorithmus, welcher es ermöglicht, von Broom erzeugte Formeln zu vereinen, vorgestellt, und seine Auswirkungen auf die Qualität der Ergebnisse sowie die Effizienz des Analyseprozesses werden durch einen Vergleich von Verträgen, welche für repräsentative Beispiele mit und ohne dieses Join-Algorithmus generiert werden, untersucht. Mit den Ergebnissen dieser Untersuchungen werden schlussendlich Parameter für den Algorithmus gefunden, welche zu möglichst guten Resultaten führen.