FM'26 Tutorial#2012
Merged
Merged
Conversation
Member
Author
|
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 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. |
Member
Author
Member
|
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? |
Member
Author
|
This is the complete log file |
Member
|
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 |
Member
Author
|
Thanks for the help! The file is: |
Member
Author
|
I tied again today, and this time it worked, maybe it has to do something with the reboot. However, I noticed another issue For
For
|
Contributor
There was a problem hiding this comment.
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
SimplifiedAnalysisandSimplifiedLifterto 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 queryTutorialEffectivelyLocal. - 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.
Member
Author
|
@sim642: Can you push Ali's container to the registry? It seems he lacks the rights to do it. |
sim642
reviewed
May 13, 2026
sim642
reviewed
May 13, 2026
sim642
reviewed
May 13, 2026
sim642
reviewed
May 13, 2026
sim642
reviewed
May 13, 2026
Comment on lines
+27
to
+29
| && make setup | ||
|
|
||
| RUN cd /home/opam/docker/analyzer \ |
Member
There was a problem hiding this comment.
What's the purpose of having this extra layer which increases image size?
Member
Author
|
Should we try to merge this now? I think the devcontainers are useful beyond the tutorial. And do we have to change something about the devcontainer before we can merge this? |
Co-authored-by: Copilot <copilot@github.com>
Avoids error when setting up pre-commit hook.
Avoids warnings on build.
…e for devcontainer
…ial image for devcontainer" This reverts commit 7f52781.
Member
|
I tagged the used version as a release: https://github.com/goblint/analyzer/releases/tag/fm26-tutorial. |
sim642
approved these changes
May 20, 2026
Contributor
There was a problem hiding this comment.
Pull request overview
Copilot reviewed 13 out of 13 changed files in this pull request and generated 5 comments.
Comments suppressed due to low confidence (1)
src/analyses/tutorials/gStoreWideningSol.ml:234
- This query path assumes
ThreadId.get_current_unliftsucceeds, but it can fail whenCurrentThreadIdis unknown (Top/Bot). Consider pattern matching onman.ask Queries.CurrentThreadIdand returning a conservativeMustBool.top ()when the thread ID isn’t precisely known to avoid runtime exceptions.
let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in
let singleton_set = ThreadSet.singleton tid in
let writers = man.global v in
ThreadSet.equal singleton_set writers
Comment on lines
+27
to
+33
| RUN cd /home/opam/docker/analyzer \ | ||
| && OPAMWITHTEST=true make setup | ||
|
|
||
| RUN cd /home/opam/docker/analyzer \ | ||
| && eval $(opam env) \ | ||
| && opam install -y ocaml-lsp-server ocamlformat dune=3.19.1 \ | ||
| && sudo gem install parallel os |
| "remoteUser": "opam", | ||
| "postCreateCommand": "make setup; make dev", | ||
|
|
||
| "postCreateCommand": "if [ -e _opam ] && [ ! -L _opam ]; then echo 'ERROR: _opam already exists and is not a symlink. Delete it manually on the host and rebuild the container.' >&2; exit 1; elif [ ! -e _opam ]; then ln -s /home/opam/docker/analyzer/_opam .; fi", |
Comment on lines
+214
to
+216
| let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in | ||
| let singleton_set = ThreadSet.singleton tid in | ||
| match is_tracked_lval lval with |
Comment on lines
+261
to
+268
| let tid = ThreadId.get_current_unlift (SimplifiedAnalysis.ask_of_man man) in | ||
| let singleton_set = ThreadSet.singleton tid in | ||
| match is_tracked_lval lval with | ||
| | Some v -> | ||
| (* TODO: 3) check if this is a global variable and if it is, record the thread id *) | ||
| state | ||
| | None -> | ||
| state |
Comment on lines
+52
to
+59
| let registered_simplified_analysis (module S:SimplifiedAnalysis.SimplifiedSpec) = | ||
| let module S':MCPSpec = struct | ||
| include SimplifiedLifter.FromSimplifiedSpec(S) | ||
| module A = UnitA | ||
| let access _ _ = () | ||
| end | ||
| in | ||
| register_analysis (module S') |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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: