Dieses Kapitel befasst sich mit den neuesten Entwicklungen der Mopsa-Plattform, einem Open-Source-Werkzeug zur statischen Analyse, das auf abstrakter Interpretation beruht. Die Autoren stellen mehrere wichtige Verbesserungen vor, die umgesetzt wurden, um die Präzision und Skalierbarkeit der Plattform zu verbessern. Eine bemerkenswerte Ergänzung ist die Trace-Partitionierung, die eine vollständige Analyse gewährleistet und gleichzeitig die Präzision verbessert, indem abstrakte Zustände auf der Grundlage der Analyse-Trace getrennt bleiben. Darüber hinaus unterstützt die Plattform jetzt die Erweiterung mit konstanten Schwellenwerten, was die Präzision bei der Analyse von Schleifen erhöht, die durch Ungleichheiten geschützt sind. Eine weitere wesentliche Verbesserung ist die Speicherdeallokationsprüfung, die sicherstellt, dass der gesamte dynamisch zugewiesene Speicher ordnungsgemäß deallokiert wird, was die MemCleanup-Eigenschaft in SV-Comp unterstützt. Das Kapitel behandelt auch die Softwarearchitektur des SV-Comp-Treibers, der sequenziell immer präzisere Analysen durchführt, bis die Eigenschaft des Interesses bewiesen ist oder die genaueste Analyse erreicht ist. Darüber hinaus führen die Autoren heuristische Autosuggestionen ein, die es der Analyse ermöglichen, Optionen vorzuschlagen, die die Präzision für weitere Analysen verbessern. Die Ergebnisse der Mopsa-Performance im SV-Comp 2025 werden präsentiert und zeigen ihre Stärken in Skalierbarkeit und Präzision, insbesondere in den Bereichen SoftwareSystems und NoOverflows. Das Kapitel schließt mit einer Diskussion über Mopsas Schwächen und zukünftige Entwicklungspläne, einschließlich des Potenzials, Gegenbeispiele und Unterstützung für Kündigungs- und gleichzeitige Verifikationsaufgaben bereitzustellen.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We present advances we brought to Mopsa for SV-Comp 2025. Most notably, Mopsa now supports bounded trace partitioning, constant widening with thresholds, and can check that all memory has been correctly deallocated. Further, Mopsa now integrates a sound support of bitfields. While Mopsa at SV-Comp previously relied on a fixed, homogeneous set of configurations to verify tasks, it can now automatically leverage semantic information from a previous analysis to trigger heuristic precision improvements in further analyses. With these improvements, Mopsa wins a silver medal in the SoftwareSystems category and ranks fifth in the NoOverflows category.
Hinweise
R. Monat—Jury member.
1 Verification Approach: the Mopsa platform
Mopsa is an open-source static analysis platform relying on abstract interpretation [9]. The implementation of Mopsa aims at exploring new perspectives for the design of static analyzers.Journault et al. [13] describe the core of Mopsa principles, and Monat [22, Chapter 3] provides an in-depth introduction to Mopsa’s design. The C analysis which we rely on for this competition is based on the work of Ouadjaout and Miné [27]; it proceeds by induction on the syntax, is fully context- and flow-sensitive, and committed to be sound. This is the third time Mopsa participates in SV-Comp [23, 24]. We have brought several enhancements, including major precision improvements, described below.
Trace partitioning. Mopsa now supports a variant of trace partitioning [16]. Trace partitioning keeps some abstract states separate (depending on the analysis trace) to improve precision. In our implementation, we keep a small, bounded abstract trace to separate abstract states while maintaining full analysis coverage. The abstract trace consists in the k latest trace markers. Currently, trace markers correspond to control conditions (if, switch, different return locations), and case disjunctions when handling C stubs [27].
Anzeige
Widening with constant thresholds. Mopsa relies on the traditional abstract interpretation use of widening [9] to enforce finite convergence when analyzing loops. However these widening operators may generalize some constraints too quickly, which can be difficult to recover from. To address this issue, Mopsa now supports the standard widening with thresholds [4]. It is implemented as a plug-in, which observes the analyzer and performs some constant propagation to decide relevant thresholds for each variable. This approach greatly improves precision when analyzing loops guarded by (in)equalities.
Memory deallocation check. Mopsa can prove that programs have successfully deallocated all memory. During the end of the analysis of a program, it queries the recency abstraction [2] to ensure that all memory dynamically allocated through malloc and other glibc functions has been properly deallocated. This allows us to support the MemCleanup property of SV-Comp (especially in the corresponding uthash subcategory of SoftwareSystems).
Sound bitfield support. The low-level C memory representation of cells [20] we use works at the byte level, making bitfield reasoning hard. We have thus implemented a domain translating bitfield operations into equivalent byte-level operations with bitmasks. This approach is currently sound, although imprecise. The precision could be improved through new numeric abstractions in the future.
Other improvements. Mopsa leverages relational numeric domain through Apron’s interface [12], relying on static packing [4] to remain scalable. In order to improve precision for small and intricate programs, the last configuration used in our SV-Comp driver (Section 2) does not rely on packing (i.e., all variables are used in the same polyhedron). Noticing performance improvements in this case, we decided to rely on the PPLite polyhedra implementation [3]. Mopsa does not support the analysis of recursive functions. We added support to unroll recursive functions of bounded depth.
Anzeige
2 Software Architecture: the SV-Comp driver
By default, the C analysis of Mopsa detects all the runtime errors that may happen in the analyzed program, while SV-Comp tasks focus on a specific property at a time. We thus rely on an SV-Comp specific driver. It takes as input the task description (program, property, data model). It sequentially tries increasingly precise C analyses defined in Mopsa until the property of interest is proved or the most precise analysis is reached (or the resources are exhausted). Each analysis result is postprocessed by the driver to check if the property is proved. An analysis configuration defines the set of domains used and their parameters, allowing control of the precision-efficiency ratio. A breakdown of the results is shown in Fig. 1. Similarly to last year [23], we use five configurations. Confs. 1 and 3 are unchanged from last year. Conf. 2 now only unrolls the first 2 iterations of loops (down from 10 last year – but the precision suggestion hook mentioned below can override this parameter). Conf. 4 adds the bounded trace partitioning, where up to 7 trace markers can be kept. Conf. 5 also enables bounded trace partitioning (with up to 10 trace markers), and relies on PPLite without static packing for best precision.
Heuristic Autosuggestions. An important improvement is that the set of configurations is not fixed and uniform for all programs anymore. Each analysis can suggest enabling options that will improve the precision of further analyses. These options are decided by a plug-in observing the analysis of Mopsa. It currently supports three semantic heuristics:
Bounded recursion unrolling.
Upon detection of a call to a recursive function f having parameter n, if n lies in interval \([0, \texttt {hi}]\), and \(\texttt {hi} < 1000\), further analyses will inline recursive functions up to bound hi.1
Loop unrolling for precise allocations.
If the program contains a loop, for which we can semantically infer that (i) there are less than 30 iterations and that (ii) iterations perform allocations, further analyses will unroll this loop to keep the allocated memory blocks distinct and enhance precision.
Single loop unrolling.
If the program semantically reaches a single loop, for which we can infer an upper bound on the number of iterations, further analyses will fully unroll this loop.
Fig. 1.
Results of our sequential portfolio at SV-Comp 2025. Max. Conf. i represents the sequence of increasingly precise analyses from Conf. 1 up to Conf. i. Max. Conf. 2 is able to prove 741 tasks correct in addition to the 7002 proved by Conf. 1, although 970 tasks reach the resource limits when analyzed by Conf. 1 and 2 (581 more than by Conf. 1 alone). There are 33592 tasks in total, including 22356 correctness tasks. Mopsa can only prove program correctness for now; it yields “unknown” when unable to prove a program correct.
3 Strengths and Weaknesses
Mopsa participated in the following categories, targeting C programs: ReachSafety, MemSafety, NoOverflows and SoftwareSystems. An overview of results can be found in the competition report [5].Figure 2 highlights the progress made by Mopsa in specific subcategories, thanks to the improvements brought for this year’s edition. Note that in two subcategories, the score of Mopsa decreased due to our now-sound bitfield encoding.
Fig. 2.
Mopsa’s improvements for selected subcategories of the ReachSafety, MemSafety, NoOverflows and SoftwareSystems tracks, comparing the scores reached at SV-Comp 2024 and 2025. Property is either ReachSafety, MemSafety or NoOverflow. The last three columns show the score of Mopsa submitted last year, this year, and the best score reached by a verifier.
Strengths. Mopsa is quite scalable: our cheapest configuration is able to analyze a given program within the allocated resource budget in 98.8% of the cases. Thanks to this scalability, Mopsa is particularly competitive in the SoftwareSystems track, focusing on verifying real software systems. This year, Mopsa ranked second with 2164 points, closely trailing CPAchecker [1] with 2238 points. It is the best verifier in the DeviceDriversLinux-ReachSafety and the uthash-NoOverflows subcategories. In uthash-NoOverflows there are only two verifiers able to score points; the second is UAutomizer [11], with 6 points. The second strength of Mopsa lies in the NoOverflows track, where it ranked fifth, with results near those of Goblint [30], which is the first abstract-interpretation based verifier to enter the competition.
Weaknesses. Mopsa can only prove programs correct for now, and is currently unable to provide counterexamples otherwise. We plan to leverage the recent works of Milanese and Miné [18, 19] to address this issue. Mopsa does not support the termination property, and cannot precisely analyze concurrency-related verification tasks, but we could leverage previous abstract interpretation work targeting those properties [21, 31‐33]. Our SV-Comp driver currently tries a sequence of increasingly precise configurations: this approach is not efficient, we are planning to develop techniques deciding what would be the best configuration to analyze a given program, following the works of Oh et al. [15, 26, 35].
4 Software Project and Contributors
Mopsa is available on Gitlab [28], and released under an GNU LGPL v3 license. Mopsa was originally developed at LIP6, Sorbonne Université following an ERC Consolidator Grant award to Antoine Miné. Mopsa is now additionally developed in other places, including Inria, ENS, Airbus and Nomadic Labs. The people who improved Mopsa for SV-Comp 2025 are the authors of this paper.
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.
In other cases, Mopsa relies on the function’s prototype to return the top value, and assumes the recursive function has no side-effects. To keep this approach sound, our SV-Comp driver thus returns unknown whenever a recursive function has been encountered during the analysis.
