figure a
figure b

1 Verification Approach

Goblint is an abstract-interpretation–based static analyzer of C code, with an emphasis on the sound analysis of multi-threaded programs [14, 15]. It uses side-effecting constraint systems [2] to combine context-sensitive analysis of local states with flow-insensitive analysis of data possibly shared between threads. Goblint is equipped with a range of different analyses that, in turn, build on multiple abstract domains for expressing candidate program invariants.

1.1 Memory Safety

Techniques for detecting memory-related bugs have been extensively studied [6, 9, 10, 20]. While Goblint did not target such bugs in the past, new analyses for the sound analysis of memory safety have been added for SV-COMP 2024. The analyzer already tracks abstract address sets for pointer variables. A single abstract address consists of a variable and an abstract offset. The analyzer distinguishes between regular program variables and allocated memory blocks, which are identified by their respective allocation sites together with the allocating thread and possibly an allocation counter.

The new analyses are concerned with the detection of the following memory-safety bugs: invalid memory deallocations, invalid pointer dereferences, as well as memory leaks. Beyond null-pointer dereferences, two further kinds of invalid dereferences are now considered: memory out-of-bounds accesses and use-after-free (UAF) bugs. Memory out-of-bounds accesses can be uncovered by obtaining the size, as well as the offset from the base address of the memory being accessed. To determine whether an access via some offset may be out of bounds, the analysis relies on an expressive combination of integer domains including intervals.

Invalid dereferences due to use-after-frees can be detected in the single- and multi-threaded case. For the single-threaded setting, the analysis uses the allocation-site abstractions in order to keep track of potentially already deallocated memory, and warns on accesses to such memory. Regarding the multi-threaded case, it additionally leverages Goblint’s side-effecting functionality by maintaining a global invariant that, for each piece of deallocated memory, collects the set of all threads that may free it. Goblint tracks abstract thread IDs which allow reasoning about which threads may run in parallel [17]. The may-happen-in-parallel (MHP) information from the abstract thread ID domain (and a dedicated analysis of thread joins) is used to infer whether an access to a piece of memory may happen in parallel with (or after) the deallocation of the same piece of memory by another thread. In addition, invalid frees due to possibly occurring double frees are flagged by this analysis as well.

Potential memory leaks can be detected thanks to a dedicated analysis. To this end, all allocated memory blocks are tracked path- and context-sensitively. Furthermore, the allocation counter is relied on to potentially exclude memory leaks for a particular allocation site. Calls to deallocating functions, such as free, have the effect of removing pieces of tracked (and now deallocated memory) from the state, whenever the analysis determines that the passed pointer must point to an abstract block of memory which describes a single concrete memory location. At all exit points of the program, it is then checked whether the set of possibly still allocated memory is empty. In case any such set is non-empty, a memory leak is reported. In the multi-threaded case, the analysis checks the following stronger property and warns whenever that property may be violated:

  1. 1.

    all threads have terminated at the end point of main, and

  2. 2.

    exit and similar functions, causing early termination, are not called, and

  3. 3.

    at its return, each thread has freed all the memory it allocated.

This property allows for a thread-modular analysis, where sets of allocated and freed memory are maintained in a flow- and context-sensitive manner.

We remark that the analysis for memory leaks tracks which heap-allocated memory may not be freed yet, while the analysis to detect UAF issues tracks which memory may potentially already be freed. One direction of improvement would be to consider tracking relational pointer information along the lines of Seidl et al. [18] and, additionally, consider relational information about the lengths of arrays and memory blocks. This may be useful in the case of variable length arrays and dynamically allocated memory for which the size is not statically known.

1.2 Termination

A termination analysis has been added, largely leveraging existing features of the framework. This highlights the versatility of the framework. To account for non-termination due to loops, a counter variable is inserted into each loop and incremented in every loop iteration. A relational polyhedra analysis based on Apron [8] is then used to determine whether the counter variable is bounded. To detect potential non-termination due to recursion, the notion of a call graph is enhanced by considering functions together with their respective abstract calling contexts and taking dynamic calls via pointers into account. This graph is a posteriori extracted out of the analysis result and then checked for cycles in a post-processing phase. In case no cycles (including self-loops) exist in the abstract call graph, there can be no cycles in the concrete call graph.

The currently implemented termination analysis is just a first step in the realization of related techniques. Future work may, e.g., be the tuning of the abstract contexts for this use-case, or the incorporation of more involved techniques for termination analysis by abstract interpretation [4, 5]. Extending the presented approaches to the non-termination of concurrent programs while remaining as thread-modular as possible seems particularly challenging.

2 Software Architecture

Goblint is implemented in \(\sim \)54, 000 lines of OCaml and uses an updated fork of CIL [12] as its parser frontend for the C language. It depends on Apron [8] for relational analyses. No other major libraries or external tools are required.

The modular architecture of Goblint [1] allows a combination of analyses to be selected and automatically configured at runtime [15]. Analyses are defined through their abstract domains and transfer functions, which can communicate with other analyses using predefined queries and events. The combined analyses together with the control-flow graphs of the functions yield a side-effecting constraint system [2], which is solved using a local generic solver [19]. The solution is post-processed to determine the verdict and construct a witness.

3 Strengths and Weaknesses

Goblint once again demonstrated its soundness in this year’s competition, i.e., it did not produce any false negatives. The only other tools that did not produce any false negatives are Aise [21] (competing only in ReachSafety-Loops), Brick (competing in three sub-categories of ReachSafety), and Mopsa [11] (competing in all categories except ConcurrencySafety and Termination). Goblint is thus the only sound tool in SV-COMP 2024 to support all properties, and the only sound tool represented in the overall ranking. Among the tools participating in the overall ranking, Goblint, despite targeting only proofs – which are traditionally considered to be more time-consuming than finding counter-examples – leads the pack in terms of points achieved in \(\le {9}\text { s}\). This is most pronounced when considering runtimes \(\le {1}\text { s}\). This highlights the efficiency of Goblint. Beyond these observations, we briefly discuss the newly added analyses here. Support for soundly detecting memory safety bugs greatly broadens the applicability of the analyzer, evidencing the flexibility of the underlying framework. Of particular note is the support for verifying the memory-safety of multi-threaded programs in a thread-modular way, yielding the second-best score in ConcurrencySafety-MemSafety, after Deagle [7]. Turning to termination analysis, the added analysis demonstrates that a considerable chunk of the SV-COMP benchmarks in this category can be handled by using our extended dynamic call graph to deal with recursion and ghost counters together with numerical relational domains to deal with loops. Finally, Goblint now comes with dedicated support for analyzing programs using setjmp/longjmp and flagging their misuse [16]. We have contributed programs using this language feature to the benchmark suite.

A general weakness of Goblint currently is that, while it supports expensive but expressive relational domains such as polyhedra, it lacks a heuristic when to activate them, and thus only uses them for termination analysis. Activating these domains based on some program properties, or attempting analysis with such expensive domains after an analysis without them was inconclusive, may help to improve the precision of the analyzer without compromising its efficiency.

4 Tool Setup and Configuration

Goblint version svcomp24-0-gc2e9465a7 participated in SV-COMP 2024 [3, 13]. It is available in both binary (Ubuntu 22.04) and source code form at our GitHub repository.Footnote 1 Instructions for building from source can be found in the README. Both the tool-info module and the benchmark definition for SV-COMP are named goblint. They correspond to running the tool as follows:

./goblint --conf conf/svcomp24.json \(\backslash \)

             --set ana.specification property.prp input.c

Goblint participated in all the categories, while opting-out from FalsificationOverall.

5 Software Project and Contributors

Goblint development takes place on GitHub, while related publications are listed on its website.Footnote 2 It is an MIT-licensed project initiated by Technische Universität München and the University of Tartu.