Use flambda compiler optimization

.github/workflows/unlocked.yml

@@ -18,6 +18,7 @@ jobs:
           - ubuntu-latest
           - macos-latest
         ocaml-compiler:
+          - 4.14.0+options,ocaml-option-flambda
           - 4.14.x
           - 4.13.x
           - 4.12.x

README.md

@@ -1,4 +1,5 @@
 # Goblint
+
 [![locked workflow status](https://github.com/goblint/analyzer/actions/workflows/locked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/locked.yml)
 [![unlocked workflow status](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/unlocked.yml)
 [![docker workflow status](https://github.com/goblint/analyzer/actions/workflows/docker.yml/badge.svg)](https://github.com/goblint/analyzer/actions/workflows/docker.yml)
@@ -8,45 +9,57 @@
 Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/en/latest/) or [GitHub](./docs/).
 
 ## Installing
+
 Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository.
 
 ### Linux
+
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).
-2. Make sure the following are installed: `git patch m4 autoconf libgmp-dev libmpfr-dev pkg-config`.
+2. Make sure the following packages are installed: `git` `patch` `m4` `autoconf` `libgmp-dev` `libmpfr-dev` `pkg-config`.
 3. Run `make setup` to install OCaml and dependencies via opam.
+   1. In case Goblint needs to be compiled with `flambda` optimizations, then run `make setup-flambda` instead
 4. Run `make` to build Goblint itself.
 5. Run `make install` to install Goblint into the opam switch for usage via switch's `PATH`.
 
 ### MacOS
+
 1. Install GCC with `brew install gcc` (first run `xcode-select --install` if you don't want to build it from source). Goblint requires GCC while macOS's default `cpp` is Clang, which will not work.
 2. ONLY for M1 (ARM64) processor: homebrew changed its install location from `/usr/local/` to `/opt/homebrew/`. For packages to find their dependecies execute `sudo ln -s /opt/homebrew/{include,lib} /usr/local/`.
 3. Continue using Linux instructions (the formulae in brew for `patch libgmp-dev libmpfr-dev` are `gpatch gmp mpfr`, respectively).
 
 ### Windows
+
 1. Install [WSL2](https://docs.microsoft.com/en-us/windows/wsl/install-win10). Goblint is not compatible with WSL1.
 2. Continue using Linux instructions in WSL.
 
 ### Other
-* **[opam](https://opam.ocaml.org/packages/goblint/)**. Install [opam](https://opam.ocaml.org/doc/Install.html) and run `opam install goblint`.
-* **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer.
-* **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest` (or `:nightly`).
-* **Docker (repository).** Clone and run `docker build -t goblint .`.
-* **Vagrant.** Clone and run `vagrant up && vagrant ssh`.
 
+- **[opam](https://opam.ocaml.org/packages/goblint/)**. Install [opam](https://opam.ocaml.org/doc/Install.html) and run `opam install goblint`.
+- **[devcontainer](./.devcontainer/).** Select "Reopen in Container" in VS Code and continue with `make` using Linux instructions in devcontainer.
+- **[Docker (GitHub Container Registry)](https://github.com/goblint/analyzer/pkgs/container/analyzer)**. Run `docker pull ghcr.io/goblint/analyzer:latest` (or `:nightly`).
+- **Docker (repository).** Clone and run `docker build -t goblint .`.
+- **Vagrant.** Clone and run `vagrant up && vagrant ssh`.
 
 ## Running
+
 To confirm that building worked, you can try running Goblint as follows:
+
 ```
 ./goblint tests/regression/04-mutex/01-simple_rc.c
 ```
+
 To confirm that installation into the opam switch worked, you can try running Goblint as follows:
+
 ```
 goblint tests/regression/04-mutex/01-simple_rc.c
 ```
+
 To confirm that the Docker container worked, you can try running Goblint as follows:
+
 ```
 docker run -it --rm -v $(pwd):/data goblint /data/tests/regression/04-mutex/01-simple_rc.c
 ```
+
 If pulled from GitHub Container Registry, use the container name `ghcr.io/goblint/analyzer:latest` (or `:nightly`) instead.
 
 For further information, see [documentation](https://goblint.readthedocs.io/en/latest/user-guide/running/).

goblint.opam.locked

@@ -64,10 +64,10 @@ depends: [
   "mlgmpidl" {= "1.2.14"}
   "num" {= "1.4"}
   "ocaml" {= "4.14.0"}
-  "ocaml-base-compiler" {= "4.14.0"}
+  "ocaml-variants" {= "4.14.0+options"}
   "ocaml-compiler-libs" {= "v0.12.4"}
   "ocaml-config" {= "2"}
-  "ocaml-options-vanilla" {= "1"}
+  "ocaml-option-flambda" {= "1"}
   "ocaml-syntax-shims" {= "1.0.0"}
   "ocamlbuild" {= "0.14.1"}
   "ocamlfind" {= "1.9.3"}

make.sh

@@ -11,6 +11,14 @@ opam_setup() {
   opam switch -y create . --deps-only ocaml-base-compiler.4.14.0 --locked
 }
 
+opam_setup_flambda() {
+  set -x
+  opam init -y -a --bare $SANDBOXING # sandboxing is disabled in travis and docker
+  opam update
+  # Note: the `--update-invariant` option is needed for replacement of the previous ocaml compiler switch invariant of Goblint
+  opam switch -y create . --deps-only ocaml-variants.4.14.0+options ocaml-option-flambda --locked --update-invariant
+}
+
 rule() {
   case $1 in
     # new rules using dune
@@ -77,6 +85,12 @@ rule() {
       echo "For running the regression tests you also need: ruby, gem, curl"
       echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
       opam_setup
+    ;; setup-flambda)
+      echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config"
+      echo "For the --html output you also need: javac, ant, dot (graphviz)"
+      echo "For running the regression tests you also need: ruby, gem, curl"
+      echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
+      opam_setup_flambda
     ;; dev)
       eval $(opam env)
       echo "Installing opam packages for development..."

src/dune

@@ -99,6 +99,11 @@
 )
 
 (env
+  (release
+    (flags (:standard -warn-error -A -w -unused-var-strict -w +9)) ; https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal
+  (ocamlopt_flags
+    (:standard -O3))
+  )
   (dev
     (flags (:standard -warn-error -A -w -unused-var-strict -w +9)) ; https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal
   )