Flow-sensitive and flow-insensitive program analyses occupy opposite ends of a spectrum. Between these extremes lie mixed flow-sensitive approaches in which some aspects of program behavior are analyzed flow-insensitively and others flow-sensitively. Mixed flow-sensitivity arises, for example, in the thread-modular analysis of multi-threaded code or when global-store widening is used to improve scalability.

The tutorial covers both the foundations of mixed flow-sensitive analysis and practical aspects. We first introduce and motivate mixed flow-sensitivity along some examples before presenting a convenient formalism for specifying such analyses independent of the chosen means of fixpoint computation. We then present the Goblint static analysis framework, which can be used to rapidly prototype and implement novel mixed flow-sensitive analyses. Participants will then get their feet wet as we gently guide them through the implementation of a simple mixed flow-sensitive analysis in Goblint.

For the hands-on session, we recommend having the Goblint static analyzer installed:

Setup Instructions

There are several ways to install Goblint, depending on your preferences.

Using VSCode Dev Containers (recommended):

Unless you have a strong preference for another IDE or editor, or are familiar with development in OCaml, we recommend using the VSCode Dev Containers setup. This environment is the best way to get things off the ground quickly, without having to worry about dependencies etc. It also comes with syntax highlighting and language server support for OCaml.

• Install VSCode and the Dev Containers extension.
• Ensure you have a working docker installation with your user in the docker group. (see, e.g., https://code.visualstudio.com/docs/devcontainers/containers)
• For Ubuntu: The buildx docker plugin needs to be installed: It is named docker-buildx or docker-buildx-plugin depending on how Docker was installed
• Clone the Goblint repository (https://github.com/goblint/analyzer), switch to the fm26-tutorial tag and open the directory in VSCode.
• Click the Reopen in Container button in the popup that appears. If the popup does not appear, you can also open the command palette (Ctrl+Shift+P) and select Dev Containers: Reopen in Container.
• Wait for the container to build and start. This may take a while the first time, as it needs to download the image.
• Verify the installation by running make && make test inside the terminal in VSCode.

Alternative installation:

Follow the instructions at https://goblint.readthedocs.io/en/latest/developer-guide/developing/. You may want to install OCaml support for your favorite IDE. We have positive experience with the OCaml Platform plugin for Visual Studio Code and OCaml LSP for Vim.