Dieses Kapitel vertieft sich in die formale Verifizierung von Datenflusslösern und konzentriert sich auf den Vergleich zwischen WTO-basierten Lösern und dem traditionellen Kildall-Algorithmus, wie er im CompCert-C-Compiler implementiert ist. Die Studie wertet verschiedene Datenflussanalysen aus, einschließlich konstanter Ausbreitung und Registerallokation, und verwendet dabei eine Vielzahl von Benchmark-Programmen. Diese Benchmarks reichen von kryptographischen Primitiven bis hin zu zufälligen C-Programmen, die mit Csmith erstellt wurden, was eine gründliche Bewertung der Skalierbarkeit von Lösern ermöglicht. Die experimentellen Ergebnisse liefern einen detaillierten Vergleich der Analysezeiten und Rechenkosten und heben die Stärken und Schwächen jedes Lösers hervor. Bemerkenswert ist, dass WTO-basierte Solver mit zunehmender Funktionsgröße eine überlegene Skalierbarkeit aufweisen, obwohl sie aufgrund der WTO-Berechnung einen Mehraufwand verursachen. Auch die Präzision der Lösungsmittel wird bewertet, was minimale Unterschiede offenbart, die in bestimmten Fällen die WTO-basierten Methoden begünstigen. Dieses Kapitel bietet einen tiefen Einblick in die Leistungsfähigkeit und Präzision von Datenflusslösern und liefert wertvolle Erkenntnisse zur Optimierung der Compilerleistung und formaler Verifikationsprozesse.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
In this report, we provide our full set of results for the experimental evaluation of our formally verified, WTO-based dataflow solvers [2]. We also detail useful information regarding our artifact [3] and evaluation setup. In particular, we validate experimentally that our implementation of Bourdoncle’s iteration strategies have acceptable performances in practice, when applied to the dataflow analyses used in the CompCert C verified compiler. Our experiments also help better understanding the differences between the solvers, their strengths and their weaknesses.
1 Experimental Data
Our baseline for comparison is the generic dataflow solver from the CompCert C compiler [4] version 3.13, which implements Kildall’s algorithm [1]. Below we describe the dataflow analyses implemented in CompCert, as well as the set of program benchmarks we used to evaluate our solvers.
1.1 Dataflow Analyses used by Compiler Passes
CompCert relies on several dataflow analyses operating over different intermediate representations. All of these represent programs as control-flow graphs (CFG). Common optimizations, e.g., constant propagation, or common subexpression elimination (CSE), are performed on the RTL representation. Register allocation is performed on the XTL representation, and the linearization of the CFG is performed on the LTL representation. Depending on the analysis problem, the CFG must be traversed forwards or backwards.
Anzeige
Table 1 sums up representative dataflow analyses from CompCert, their abstract domains and the compilation passes to which they are related. Forward analyses always start the CFG traversal from the CFG entry node. Backward NS refers to backward analyses starting from an over-approximated node set (NS) for exit nodes. Backward AN refers to backward analyses where all nodes (AN) are considered as exit nodes.
Table 1:
Dataflow analyses in CompCert (NS = Node Set, AN = All Nodes).
Dummy
1.2 Test Suites
We evaluate our solvers against six test suites, which we list in Table 2. The first five suits are taken from CompCert’s distribution: Spass is the prover for first-order logic Spass [5], Ray is a ray tracer, Comp is a compression library, Misc is a set of cryptographic primitives (AES, SHA1, SHA3) and miscellaneous C programs (incl. FFT), and Reg corresponds to regression testing programs.
We added a sixth suite, Random, made of 10 random C programs generated with Csmith [6]. This suite allows us evaluating the scalability of our solvers as the size of the analyzed functions grows up. The biggest function in Random has 3916 RTL instructions while functions in the other suites are up to 1245 RTL instructions.
Table 2:
Tests suites. A functions size counts the instructions in the RTL CFG.
Dummy
2 Experimental Results
We use the following abbreviations to refer to each of the solver we consider in this report: K is the Kildall solver as implemented in CompCert, BIter is our WTO-iterative solver, and BRec is our WTO-recursive solver.
Anzeige
Total compilation times are discussed in the paper [2]; they show that BIter and BRec have acceptable performance in practice. Below, we provide detailed results for the finer-grained comparison of our solvers.
Fig. 1:
Analysis time, by function (in seconds, log/log scale). Comparing K with BRec. Left: ValueAnalysis (forward). Right: Liveness (backward). Top: preprocessing time included. Bottom: fixpoint computation time only.
2.1 Efficiency of the Solvers: Analysis Times
We compare the analysis time of the solvers, for each analysis, and function by function. Our detailed results are given in Fig. 1 for ValueAnalysis and Liveness, which are good representatives of forward and backward analyses, respectively. In Fig. 1, the points compare analysis time measures for a single function. The (x, y) coordinates correspond to the time measures for each algorithm.
For long analysis times, BRec performs better, while K is better for short analysis times. But, as compilation time is linearly correlated with the size of the CFG (in number of nodes, i.e., instructions), this means that, as the size of the function increases, the gain of iterating more efficiently is worth the cost of computing and validating the WTO itself. Solvers BRec and BIter scale better with function size. Our interpretation is confirmed by the difference between plots which include preprocessing time (top ones) and the ones that only include the fixpoint computation time (bottom ones). Indeed, if we only compare fixpoint computation times, BRec scales better than K (see the bottom left plot of Fig. 1).
In conclusion, there is an improvement on the fixpoint computation thanks to more efficient iterations, but this improvement is limited by an overhead due to the computation of the WTO.
2.2 Efficiency of the Solvers: Analysis Costs
In addition to wall-clock analysis times, we also consider dataflow solvers computation costs that are relative to the number of transfer functions (T) application and join operators (\(\sqcup \)). Figure 2 shows the dataflow solver costs in terms of transfer functions and join operators, comparing K with BRec. We only show results for ValueAnalysis, they are similar for other analyses, either forward or backward.
Fig. 2:
Analysis costs, by function, for ValueAnalysis (log/log scale). BRec versus K. Left: number of application of transfer functions T. Right: number of application of join operator \(\sqcup \).
BRec applies more often transfer functions T than K does. However, BRec applies drastically less \(\sqcup \) operators. Indeed, when analyzing a node, BRec retrieves dataflow facts from its predecessors, after applying the transfer function to each of them: T needs to be applied once per predecessor each time we analyze a node. Instead, K starts by applying the transfer function of the node, and then propagates the output dataflow fact to all of its successors. Moreover, BRec only applies \(\sqcup \) for component heads and for nodes having several predecessors, while K needs to apply it when analyzing every node, to join the output dataflow fact with the fact previously computed for that node.
2.3 Precision of the Solvers
We evaluate the precision of the solvers by comparing the abstract values they return, for each analysis, and for each function. Comparison is done using the partial order from the analysis pseudo-semi-lattice domain.
The three solvers return almost always the same value, except for a few functions (6.1‰ of 5766 analyzed functions) on domains where the join operator over-approximates the least upper bound. More precisely, Table 3 compares the precisions of the dataflow solvers, two-by-two, for Value Analysis. For each pair of solvers (A, B), we give the number of functions where A is more precise than B on at least one node of the CFG. Indeed, differences tend to propagate to large parts of the CFG, so we do not consider how many nodes in the CFG give rise to different abstract values.
There are very few differences, and they tend to be in favor of Bourdoncle’s method BIter and BRec. These results are to be put in perspective: the differences affect a small number of functions. Additionally, to date, CompCert’s optimizations do not take advantage of these precision gains.
Table 3:
Comparing the precision of dataflow algorithms for Value Analysis. For instance, there are 34 functions where BRec is more precise than K (at more than one CFG node), and this represents 5.9‰ of the analyzed functions.
Dummy
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
