Skip to content

unlocked

unlocked #2466

Workflow file for this run

name: unlocked
on:
# pull_request: # save CI time on PRs, run manually if needed (before merge) or find out failures from scheduled run (after merge)
# paths-ignore:
# - 'docs/**'
workflow_dispatch:
schedule:
# nightly
- cron: '31 1 * * *' # 01:31 UTC, 02:31/03:31 Munich, 03:31/04:31 Tartu
# GitHub Actions load is high at minute 0, so avoid that
jobs:
regression:
strategy:
fail-fast: false
matrix:
# We don't want a full matrix because it is too slow, so we only have linear axes overriding these below.
include:
# Common configuration
- os: ubuntu-24.04
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: true
z3: false
# OCaml versions
- os: ubuntu-24.04
ocaml-compiler: 5.4.x
apron: true
z3: false
- os: ubuntu-24.04
ocaml-compiler: 5.3.x
apron: true
z3: false
- os: ubuntu-24.04
ocaml-compiler: 5.2.x
apron: true
z3: false
- os: ubuntu-24.04
ocaml-compiler: 5.1.x
apron: true
z3: false
- os: ubuntu-24.04
ocaml-compiler: 5.0.x
apron: true
z3: false
- os: ubuntu-24.04
ocaml-compiler: 4.14.x
apron: true
z3: false
# OS-s
- os: ubuntu-22.04
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: true
z3: false
- os: macos-26
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: true
z3: false
- os: macos-15-intel
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: true
z3: false
- os: macos-15
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: true
z3: false
- os: macos-14
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: true
z3: false
# Optional dependencies
- os: ubuntu-24.04
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: false
z3: false
- os: ubuntu-24.04
ocaml-compiler: ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
apron: true
z3: true
# customize name to use readable string for apron instead of just a boolean
# workaround for missing ternary operator: https://github.com/actions/runner/issues/409
name: regression (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}${{ matrix.apron && ', apron' || '' }}${{ matrix.z3 && ', z3' || '' }})
runs-on: ${{ matrix.os }}
steps:
- name: Checkout code
uses: actions/checkout@v6
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
if: ${{ startsWith(matrix.os, 'ubuntu') }}
run: sudo apt install -y libgraph-easy-perl
- name: Install dependencies
run: opam install . --deps-only --with-test
- name: Install os gem for operating system detection
run: sudo gem install os
- name: Install Apron dependencies
if: ${{ matrix.apron }}
run: opam install apron mlgmpidl
- name: Install Z3 dependencies
if: ${{ matrix.z3 }}
run: opam install z3
- name: Build
run: ./make.sh nat
- name: Download Linux headers
run: ./make.sh headers
- name: Test
run: opam exec -- dune runtest
- name: Test marshal regression # not part of @runtest due to time
run: ruby scripts/update_suite.rb -m
lower-bounds-downgrade:
strategy:
fail-fast: false
matrix:
os:
- ubuntu-latest
- macos-latest
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
name: lower-bounds (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}, downgrade)
runs-on: ${{ matrix.os }}
steps:
- name: Checkout code
uses: actions/checkout@v6
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
if: ${{ startsWith(matrix.os, 'ubuntu') }}
run: sudo apt install -y libgraph-easy-perl
- name: Install dependencies
run: opam install . --deps-only --with-test
- name: Install os gem for operating system detection
run: sudo gem install os
- name: Install Apron dependencies
run: opam install apron mlgmpidl
- name: Downgrade dependencies
# without "+removed" in criteria, because it also removes optional apron
run: opam install --solver=builtin-0install --criteria="+count[version-lag,solution]" . --deps-only --with-test
- name: Build
run: ./make.sh nat
- name: Download Linux headers
run: ./make.sh headers
- name: Test
run: opam exec -- dune runtest
- name: Test marshal regression # not part of @runtest due to time
run: ruby scripts/update_suite.rb -m
opam-install:
strategy:
fail-fast: false
matrix:
os:
- ubuntu-latest
- macos-latest
ocaml-compiler:
- ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
runs-on: ${{ matrix.os }}
steps:
- name: Checkout code
uses: actions/checkout@v6
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}
- name: Install graph-easy # TODO: remove if depext --with-test works (https://github.com/ocaml/opam/issues/5836)
if: ${{ startsWith(matrix.os, 'ubuntu') }}
run: sudo apt install -y libgraph-easy-perl
- name: Install Goblint with test
run: opam install goblint --with-test
- name: Install Apron dependencies
run: opam install apron mlgmpidl
- name: Symlink installed goblint to repository # because tests want to use locally built one
run: ln -s $(opam exec -- which goblint) goblint
- name: Download Linux headers
run: ./make.sh headers
- name: Set gobopt with pre.kernel-root # because linux-headers are not installed
run: echo "gobopt=--set pre.kernel-root $PWD/linux-headers" >> $GITHUB_ENV
- name: Test regression
run: ruby scripts/update_suite.rb -s
- name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
# if: ${{ matrix.apron }}
run: |
ruby scripts/update_suite.rb group apron -s
ruby scripts/update_suite.rb group apron2 -s
- name: Test apron octagon regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
run: ruby scripts/update_suite.rb group octagon -s
- name: Test apron affeq regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
run: ruby scripts/update_suite.rb group affeq -s
- name: Test apron regression (Mukherjee et. al SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
# if: ${{ matrix.apron }}
run: ruby scripts/update_suite.rb group apron-mukherjee -s
- name: Test marshal regression
run: ruby scripts/update_suite.rb -m -s
- name: Test incremental regression
run: ruby scripts/update_suite.rb -i -s
- name: Test incremental regression with cfg comparison
run: ruby scripts/update_suite.rb -c -s
gobview:
strategy:
fail-fast: false
matrix:
os:
- ubuntu-latest
ocaml-compiler:
- ocaml-variants.5.0.0+options,ocaml-option-flambda
node-version:
- 14
runs-on: ${{ matrix.os }}
steps:
- name: Checkout code
uses: actions/checkout@v6
- name: Set up OCaml ${{ matrix.ocaml-compiler }}
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: ${{ matrix.ocaml-compiler }}
- name: Set up Node.js ${{ matrix.node-version }}
uses: actions/setup-node@v6
with:
node-version: ${{ matrix.node-version }}
- name: Install dependencies
run: opam install . --deps-only
- name: Setup Gobview
run: ./make.sh setup_gobview
- name: Build
run: ./make.sh nat
- name: Build Gobview
run: ./make.sh view
- name: Install selenium
run: pip3 install selenium webdriver-manager
- name: Test Gobview
run: |
python3 scripts/test-gobview.py