FM'26 Tutorial by michael-schwarz · Pull Request #2012 · goblint/analyzer

michael-schwarz · 2026-04-27T04:24:10Z

This is the first half of the tutorial for FM'26 and probably as far as we will go for the FOCS version.

This includes:

An interval analyses treating all globals as top where a local transfer function should be fixed
Extending this analysis so it uses global store widening
Turning into a mixed-flow sensitive analysis that tracks values locally for the owning thread if there is one.

Co-authored-by: Copilot <copilot@github.com>

michael-schwarz · 2026-04-27T04:32:56Z

For the longer session at FM'26 the idea would be to additionally ask for an analysis that detects which global variables are effectively thread-local, i.e., accessed only by one thread (like #1966 and https://github.com/goblint/analyzer/blob/ghosts/src/analyses/phaseGhost.ml) and interact with the gStoreWidening analysis via queries to treat such globals flow-sensitively.

Ideally, we could even distinguish between writes and reads and have both a flow-sensitive treatment within the owner, and a flow-insensitive one for other threads. That would really make it mixed flow-sensitive.

Avoids error when setting up pre-commit hook.

Avoids warnings on build.

…e for devcontainer

michael-schwarz · 2026-05-08T13:25:21Z

Somehow opening the dev container gets stuck at

=> [2/2] RUN eval $(sed -n "s/opam:[^:]:([^:]):([^:]):[^:]:([^ 14.7s

for over 10 minutes. I'm not sure where that command is even from? Any idea how to debug this @arkocal @sim642? 🙏

sim642 · 2026-05-08T14:10:39Z

I have no idea where that command even is from. It looks like the build of some Dockerfile but I don't know where it might be from. Is that from some VSCode log that has more context?

michael-schwarz · 2026-05-08T14:24:29Z

This is the complete log file

[78 ms] Dev Containers 0.460.0 in VS Code 1.120.0-insider (89bab60dbb6cdd0d1394f011e110457d885b9fa3).
[75 ms] Start: Resolving Remote
[113 ms] Setting up container for folder or workspace: /home/michael/Documents/analyzer-devcontainer/analyzer
[119 ms] Start: Check Docker is running
[120 ms] Start: Run: docker version
[156 ms] Client:
 Version:           29.1.3
 API version:       1.52
[157 ms]  Go version:        go1.24.4
 Git commit:        29.1.3-0ubuntu3~22.04.2
 Built:             Wed Apr 29 22:18:59 2026
 OS/Arch:           linux/amd64
 Context:           default

Server:
 Engine:
  Version:          29.1.3
  API version:      1.52 (minimum version 1.44)
  Go version:       go1.24.4
  Git commit:       29.1.3-0ubuntu3~22.04.2
  Built:            Wed Apr 29 22:18:59 2026
  OS/Arch:          linux/amd64
  Experimental:     false
 containerd:
  Version:          2.2.1
  GitCommit:        
 runc:
  Version:          1.3.4-0ubuntu1~22.04.1
  GitCommit:        
 docker-init:
  Version:          0.19.0
  GitCommit:        
[163 ms] Start: Run: docker volume ls -q
[190 ms] Start: Run: docker ps -q -a --filter label=vsch.local.folder=/home/michael/Documents/analyzer-devcontainer/analyzer --filter label=vsch.quality=insider
[214 ms] Start: Run: docker ps -q -a --filter label=devcontainer.local_folder=/home/michael/Documents/analyzer-devcontainer/analyzer --filter label=devcontainer.config_file=/home/michael/Documents/analyzer-devcontainer/analyzer/.devcontainer/devcontainer.json
[237 ms] Start: Run: docker ps -q -a --filter label=devcontainer.local_folder=/home/michael/Documents/analyzer-devcontainer/analyzer
[259 ms] Start: Run: docker ps -q -a --filter label=devcontainer.local_folder=/home/michael/Documents/analyzer-devcontainer/analyzer
[282 ms] Running Dev Containers CLI:   up --user-data-folder /home/michael/.config/Code - Insiders/User/globalStorage/ms-vscode-remote.remote-containers/data --container-session-data-folder /tmp/devcontainers-6e9677ae-78c0-4fa6-a21b-42add38c5d991778250218397 --workspace-folder /home/michael/Documents/analyzer-devcontainer/analyzer --workspace-mount-consistency cached --gpu-availability detect --id-label devcontainer.local_folder=/home/michael/Documents/analyzer-devcontainer/analyzer --id-label devcontainer.config_file=/home/michael/Documents/analyzer-devcontainer/analyzer/.devcontainer/devcontainer.json --log-level debug --log-format json --config /home/michael/Documents/analyzer-devcontainer/analyzer/.devcontainer/devcontainer.json --default-user-env-probe loginInteractiveShell --experimental-lockfile --mount type=volume,source=vscode,target=/vscode,external=true --mount type=bind,source=/run/user/1001/wayland-0,target=/tmp/vscode-wayland-aa000a6d-bc9a-4690-b9fd-86b92aaf1218.sock --skip-post-create --update-remote-user-uid-default on --mount-workspace-git-root --include-configuration --include-merged-configuration
[283 ms] Start: Run: /snap/code-insiders/2385/usr/share/code-insiders/code-insiders /home/michael/.vscode-insiders/extensions/ms-vscode-remote.remote-containers-0.460.0/dist/spec-node/devContainersSpecCLI.js up --user-data-folder /home/michael/.config/Code - Insiders/User/globalStorage/ms-vscode-remote.remote-containers/data --container-session-data-folder /tmp/devcontainers-6e9677ae-78c0-4fa6-a21b-42add38c5d991778250218397 --workspace-folder /home/michael/Documents/analyzer-devcontainer/analyzer --workspace-mount-consistency cached --gpu-availability detect --id-label devcontainer.local_folder=/home/michael/Documents/analyzer-devcontainer/analyzer --id-label devcontainer.config_file=/home/michael/Documents/analyzer-devcontainer/analyzer/.devcontainer/devcontainer.json --log-level debug --log-format json --config /home/michael/Documents/analyzer-devcontainer/analyzer/.devcontainer/devcontainer.json --default-user-env-probe loginInteractiveShell --experimental-lockfile --mount type=volume,source=vscode,target=/vscode,external=true --mount type=bind,source=/run/user/1001/wayland-0,target=/tmp/vscode-wayland-aa000a6d-bc9a-4690-b9fd-86b92aaf1218.sock --skip-post-create --update-remote-user-uid-default on --mount-workspace-git-root --include-configuration --include-merged-configuration
[545 ms] @devcontainers/cli 0.86.1. Node.js v22.22.1. linux 5.15.0-176-generic x64.
[545 ms] Start: Run: docker buildx version
[753 ms] github.com/docker/buildx 0.30.1 0.30.1-0ubuntu1~22.04.1
[754 ms] 
[754 ms] Start: Run: docker version --format {{.Server.Version}}
[794 ms] 29.1.3
[794 ms] 
[794 ms] Start: Run: docker -v
[825 ms] Start: Resolving Remote
[833 ms] Start: Run: git rev-parse --show-cdup
[848 ms] Loading 146 extra certificates from /etc/ssl/certs/ca-certificates.crt.
[1024 ms] Start: Run: docker ps -q -a --filter label=devcontainer.local_folder=/home/michael/Documents/analyzer-devcontainer/analyzer --filter label=devcontainer.config_file=/home/michael/Documents/analyzer-devcontainer/analyzer/.devcontainer/devcontainer.json
[1093 ms] Start: Run: docker inspect --type image ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial
[1483 ms] Start: Run: docker-credential-secret get
[3796 ms] Error fetching image details: 
[3797 ms] Start: Run: docker pull ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial
fm26-tutorial: Pulling from goblint/analyzer-devcontainer
Digest: sha256:4de03ce036914f2fdb795987e895d994de9461065607571bdf6c813f0dae1767
Status: Downloaded newer image for ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial
ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial
[4994 ms] Start: Run: docker inspect --type image ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial
[5045 ms] Start: Run: docker build -f /tmp/devcontainercli-michael/updateUID.Dockerfile-0.86.1 -t vsc-analyzer-f4302c0a1788c4f90215b9e918c174e776ba6e16074bf41ce26823fdb3bf1988-uid --platform linux/amd64 --build-arg BASE_IMAGE=ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial --build-arg REMOTE_USER=opam --build-arg NEW_UID=1001 --build-arg NEW_GID=140 --build-arg IMAGE_USER=opam /home/michael/.config/Code - Insiders/User/globalStorage/ms-vscode-remote.remote-containers/data/empty-folder
[+] Building 15.6s (4/5)                                         docker:default
 => [internal] load build definition from updateUID.Dockerfile-0.86.1      0.0s
 => => transferring dockerfile: 1.36kB                                     0.0s
 => WARN: InvalidDefaultArgInFrom: Default value for ARG $BASE_IMAGE resu  0.0s
 => [internal] load metadata for ghcr.io/goblint/analyzer-devcontainer:fm  0.0s
 => [internal] load .dockerignore                                          0.0s
 => => transferring context: 2B                                            0.0s
 => CACHED [1/2] FROM ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial  0.0s
 => => resolve ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial@sha256  0.0s
 => [2/2] RUN eval $(sed -n "s/opam:[^:]*:\([^:]*\):\([^:]*\):[^:]*:\([^  15.5s

sim642 · 2026-05-08T14:30:25Z

It's using the given prebuilt image as a base for some custom container with

docker build -f /tmp/devcontainercli-michael/updateUID.Dockerfile-0.86.1 [...]

Maybe it's possible look at that temporary Dockerfile to figure out something more. "updateUID" sounds like some general thing which as nothing to do with opam specifically. I guess it's trying to adapt something to the "remoteUser": "opam".

michael-schwarz · 2026-05-08T14:51:40Z

Thanks for the help! The file is:

ARG BASE_IMAGE
FROM $BASE_IMAGE

USER root

ARG REMOTE_USER
ARG NEW_UID
ARG NEW_GID
SHELL ["/bin/sh", "-c"]
RUN eval $(sed -n "s/${REMOTE_USER}:[^:]*:\([^:]*\):\([^:]*\):[^:]*:\([^:]*\).*/OLD_UID=\1;OLD_GID=\2;HOME_FOLDER=\3/p" /etc/passwd); \
        eval $(sed -n "s/\([^:]*\):[^:]*:${NEW_UID}:.*/EXISTING_USER=\1/p" /etc/passwd); \
        eval $(sed -n "s/\([^:]*\):[^:]*:${NEW_GID}:.*/EXISTING_GROUP=\1/p" /etc/group); \
        if [ -z "$OLD_UID" ]; then \
                echo "Remote user not found in /etc/passwd ($REMOTE_USER)."; \
        elif [ "$OLD_UID" = "$NEW_UID" -a "$OLD_GID" = "$NEW_GID" ]; then \
                echo "UIDs and GIDs are the same ($NEW_UID:$NEW_GID)."; \
        elif [ "$OLD_UID" != "$NEW_UID" -a -n "$EXISTING_USER" ]; then \
                echo "User with UID exists ($EXISTING_USER=$NEW_UID)."; \
        else \
                if [ "$OLD_GID" != "$NEW_GID" -a -n "$EXISTING_GROUP" ]; then \
                        echo "Group with GID exists ($EXISTING_GROUP=$NEW_GID)."; \
                        NEW_GID="$OLD_GID"; \
                fi; \
                echo "Updating UID:GID from $OLD_UID:$OLD_GID to $NEW_UID:$NEW_GID."; \
                sed -i -e "s/\(${REMOTE_USER}:[^:]*:\)[^:]*:[^:]*/\1${NEW_UID}:${NEW_GID}/" /etc/passwd; \
                if [ "$OLD_GID" != "$NEW_GID" ]; then \
                        sed -i -e "s/\([^:]*:[^:]*:\)${OLD_GID}:/\1${NEW_GID}:/" /etc/group; \
                fi; \
                chown -R $NEW_UID:$NEW_GID $HOME_FOLDER; \
        fi;

ARG IMAGE_USER
USER $IMAGE_USER

michael-schwarz · 2026-05-09T13:44:44Z

I tied again today, and this time it worked, maybe it has to do something with the reboot. However, I noticed another issue

For make test:

qcheck-ounit seems not installed
Missing os gem (install with: gem install os)

For ./regtest.sh:

pygmentize: not found
dot: not found

Copilot

Pull request overview

This PR introduces the first half of the FM’26 tutorial material by adding a new simplified-analysis interface (and a lifter to the standard Analyses.Spec), along with tutorial analyses and regression tests demonstrating global-store widening and related concepts.

Changes:

Added SimplifiedAnalysis and SimplifiedLifter to enable writing analyses with an explicit local state argument and a single combine hook.
Added tutorial analyses (gStoreWidening, effectivelyLocal) plus a provided solution (gStoreWideningSol) and a new tutorial query TutorialEffectivelyLocal.
Added two regression tests for the tutorial and adjusted devcontainer setup to use a prebuilt image.

Reviewed changes

Copilot reviewed 15 out of 15 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
tests/regression/99-tutorials/06-gstore-thread.c	Adds multithreaded tutorial regression test for global-store widening behavior.
tests/regression/99-tutorials/05-gstore-zero.c	Adds single-thread tutorial regression test for dead-code via branching precision.
src/goblint_lib.ml	Exposes new tutorial and simplified-framework modules via the public library.
src/framework/simplifiedLifter.ml	Implements adapter from simplified spec interface to standard `Analyses.Spec`.
src/framework/simplifiedAnalysis.ml	Defines the simplified analysis interface and manager record passed to transfer functions.
src/dune	Adjusts library module list (notably around memtrace module inclusion).
src/domains/queries.ml	Adds `TutorialEffectivelyLocal` query (MustBool) for tutorial helper analysis.
src/cdomain/value/cdomains/int/intervalSetDomain.ml	Removes unused helper (`interval_to_bool`).
src/analyses/tutorials/gStoreWideningSol.ml	Adds solution implementation for the tutorial analysis.
src/analyses/tutorials/gStoreWideningHelper.ml	Adds helper utilities (interval domain wrapper, tracking predicates, casting helpers).
src/analyses/tutorials/gStoreWidening.ml	Adds tutorial starter implementation with TODO steps and a helper analysis skeleton.
src/analyses/mCPRegistry.ml	Adds `registered_simplified_analysis` to register simplified analyses via the lifter.
src/analyses/assert.ml	Removes unused opens.
.devcontainer/Dockerfile	Adds caching layer for `make setup` and installs dev tools when building the image.
.devcontainer/devcontainer.json	Switches to prebuilt devcontainer image and changes post-create setup command.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

+    "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial",
    "remoteUser": "opam",
-    "postCreateCommand": "make setup; make dev",
+    "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .",


Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot

Pull request overview

Copilot reviewed 16 out of 16 changed files in this pull request and generated 4 comments.

+    "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial",
    "remoteUser": "opam",
-    "postCreateCommand": "make setup; make dev",
+    "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .",


Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot

Pull request overview

Copilot reviewed 16 out of 16 changed files in this pull request and generated 3 comments.

+    "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial",
    "remoteUser": "opam",
-    "postCreateCommand": "make setup; make dev",
+    "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .",


+    && make setup \
+    && eval $(opam env) \
+    && opam install -y utop ocaml-lsp-server ocp-indent \
+    && sudo gem install parallel


michael-schwarz and others added 3 commits April 27, 2026 10:08

Simplified Interface

949c1fc

Provide interface to register simplified analysis

de24002

Progress on analysis

5572c29

Co-authored-by: Copilot <copilot@github.com>

michael-schwarz added the feature label Apr 27, 2026

Progress

342f5bf

sim642 self-requested a review April 27, 2026 05:40

sim642 mentioned this pull request Apr 28, 2026

Clean up library function spawning in base analysis #1553

Open

michael-schwarz and others added 10 commits April 28, 2026 17:21

Fixes

67f9d79

Sol

666e604

Add SKIP annotation

c28db19

Exclude memtrace

b80a0a0

Move devcontainer setup into Dockerfile for prebuilding

8846047

Inline make dev into devcontainer

723318a

Avoids error when setting up pre-commit hook.

Remove unused opens in assert analysis

cbde42b

Remove unused interval_to_bool in IntervalSetDomain

37d236f

Remove unused opens from SimplifiedAnalysis

5d95d4c

Avoids warnings on build.

Use prebuilt ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial imag…

59d7a2e

…e for devcontainer

michael-schwarz added 2 commits May 9, 2026 15:19

Notes on TODOs

868ac6a

Progress

8906177

michael-schwarz requested a review from Copilot May 9, 2026 14:47

Copilot started reviewing on behalf of michael-schwarz May 9, 2026 14:48 View session

Copilot AI reviewed May 9, 2026

View reviewed changes

Potential fix for pull request finding

f171080

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

michael-schwarz and others added 3 commits May 9, 2026 23:01

Potential fix for pull request finding

6efecbb

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Add memtrace back to make CI happy

35cbd45

Complete tutorial

0ad89cd

michael-schwarz marked this pull request as ready for review May 11, 2026 06:02

Copilot AI review requested due to automatic review settings May 11, 2026 06:02

Copilot started reviewing on behalf of michael-schwarz May 11, 2026 06:02 View session

Copilot AI reviewed May 11, 2026

View reviewed changes

Typo

2a03209

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

Copilot AI review requested due to automatic review settings May 11, 2026 06:35

Copilot started reviewing on behalf of michael-schwarz May 11, 2026 06:35 View session

Copilot AI reviewed May 11, 2026

View reviewed changes

Conversation

michael-schwarz commented Apr 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michael-schwarz commented Apr 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

michael-schwarz commented May 8, 2026

Uh oh!

sim642 commented May 8, 2026

Uh oh!

michael-schwarz commented May 8, 2026

Uh oh!

sim642 commented May 8, 2026

Uh oh!

michael-schwarz commented May 8, 2026

Uh oh!

michael-schwarz commented May 9, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

michael-schwarz commented Apr 27, 2026 •

edited

Loading

michael-schwarz commented Apr 27, 2026 •

edited

Loading