FM'26 Tutorial#2012
Conversation
Co-authored-by: Copilot <copilot@github.com>
|
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. |
Avoids error when setting up pre-commit hook.
Avoids warnings on build.
…e for devcontainer
|
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? |
|
This is the complete log file |
|
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 |
|
Thanks for the help! The file is: |
|
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
|
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.
| (library | ||
| (name goblint_lib) | ||
| (public_name goblint.lib) | ||
| (modules :standard \ goblint goblint_memtrace privPrecCompare apronPrecCompare messagesCompare) | ||
| (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare) | ||
| (libraries goblint.sites goblint.build-info goblint-cil goblint-cil.pta goblint-cil.syntacticsearch batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_constraint goblint_solver goblint_library goblint_cdomain_value goblint_incremental goblint_tracing goblint_logs domain_shims |
There was a problem hiding this comment.
This was now removed in 8a62196 but it causes compilation to fail.
There is a related dune regression (ocaml/dune#14085) but that doesn't affect locked dependencies and the unlocked ones have a conflict, so there should be no reason to remove this.
There was a problem hiding this comment.
If it is kept there, make fails.
| "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>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
| "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", | ||
| "remoteUser": "opam", | ||
| "postCreateCommand": "make setup; make dev", | ||
| "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .", |
There was a problem hiding this comment.
It is supposed to fail when _opam already exists outside of the devcontainer in the repository root. This doesn't happen for fresh users who clone the repository and use the devcontainer.
It does happen if you're already a Goblint developer and try to use the devcontainer when you have an existing switch on the host at the same location. The -f is very evil: it will simply quietly wipe your _opam repository on the host by replacing it with a symlink.
Also, this is postCreateCommand, not postStartCommand/postAttachCommand, so this doesn't re-execute when reopening the devcontainer. It only happens once when creating it.
The currently committed change for this in 7a069b6 is from #2012 (comment) but how is it a problem in the first place?
That variant also leads to strange things for those who have an _opam directory on the host: if it exists and the symlink isn't added, then the devcontainer will not use the packages installed into the container but the ones installed on the host, because they happen to be in the _opam directory.
| "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 |
|
@sim642: Can you push Ali's container to the registry? It seems he lacks the rights to do it. |
| "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .", | ||
| "updateRemoteUserUID": true, | ||
|
|
||
| "runArgs": ["--init", "--env-file", ".devcontainer/devcontainer.env"], // TODO: why --init added by default? |
There was a problem hiding this comment.
Why is the environment now removed? I think the point of it is that no eval $(opam env) is needed after opening the devcontainer to make things convenient. Also, I think it's needed for the OCaml plugin to work correctly because there's no way to run VSCode with the right opam switch when opening the devcontainer otherwise.
There was a problem hiding this comment.
Was not intentional, reverting.
| "image": "ghcr.io/goblint/analyzer-devcontainer:fm26-tutorial", | ||
| "remoteUser": "opam", | ||
| "postCreateCommand": "ln -s /home/opam/docker/analyzer/_opam .", | ||
| "updateRemoteUserUID": true, |
There was a problem hiding this comment.
But this is true by default. Was there some intermediate attempt to disable it to fix the issue @michael-schwarz had?
There was a problem hiding this comment.
Yes, specifically with permissions. I did not realize this was the default and assumed this has fixed the issue, removing
| # otherwise perl (not ruby!) complains during regression testing | ||
| ENV LC_ALL=C.UTF-8 | ||
|
|
||
| USER opam |
There was a problem hiding this comment.
Why is this added here? The ocaml/opam:ubuntu-22.04-opam base image already does this.
There was a problem hiding this comment.
Since this Dockerfile is accompanying the dev-container and I had issues with mounts/users; it does not hurt to make it explicit. (since we do not see the base image Dockerfile from here)
| && opam -y install ocaml-lsp-server ocamlformat \ | ||
| && sudo gem install parallel os | ||
|
|
||
| RUN sudo apt-get install -y python3-pygments graphviz |
There was a problem hiding this comment.
These should probably be moved up to the existing apt-get install to avoid an extra layer which increases image size.
| && make setup | ||
|
|
||
| RUN cd /home/opam/docker/analyzer \ |
There was a problem hiding this comment.
What's the purpose of having this extra layer which increases image size?
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: