Codex/decompose wrapper kill aiger #143

Workflow file for this run

	name: CI

	on:
	push:
	branches: [ main ]
	pull_request:
	branches: [ main ]
	workflow_dispatch:

	jobs:
	format:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5
	- uses: actions/setup-python@v6
	with:
	python-version: '3.12'
	# Pin clang-format via the PyPI package so the formatting check is
	# reproducible across machines (distro clang-format versions disagree).
	- name: Install clang-format
	run: pip install 'clang-format==18.1.8'
	- name: Check formatting
	run: \|
	clang-format --version
	clang-format --dry-run --Werror src/.c include/tlsf/.h

	# Build the vendored OxiDD C FFI (Rust staticlib + cbindgen header) exactly
	# once and share it with the OxiDD-enabled jobs as an artifact, so cargo runs
	# a single time per CI run. The frontend-only jobs (build-test, build-clang,
	# coverage, perf-regression) pass -Doxidd=disabled deliberately to keep
	# proving the reduced no-Rust developer build path stays alive.
	oxidd:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5
	with:
	submodules: recursive
	- name: Install Rust
	run: \|
	rustup toolchain install stable --profile minimal
	rustup default stable
	- name: OxiDD submodule revision
	id: rev
	run: echo "sha=$(git -C external/oxidd rev-parse HEAD)" >> "$GITHUB_OUTPUT"
	- name: Cache cargo + OxiDD build
	uses: actions/cache@v4
	with:
	path: \|
	~/.cargo/registry
	~/.cargo/git
	~/.cargo/bin
	external/oxidd/target
	key: oxidd-${{ runner.os }}-${{ steps.rev.outputs.sha }}
	restore-keys: \|
	oxidd-${{ runner.os }}-
	- name: Install cbindgen
	# ~/.cargo/bin is cached, so a restored cache already has cbindgen and a
	# plain `cargo install` would fail with "binary already exists"; skip it
	# when present (and --force on the rare miss to stay idempotent).
	run: command -v cbindgen >/dev/null \|\| cargo install cbindgen --locked --force
	- name: Build OxiDD FFI
	run: scripts/build_oxidd.sh
	- name: Upload OxiDD FFI artifact
	uses: actions/upload-artifact@v4
	with:
	name: oxidd-ffi
	path: \|
	external/oxidd/target/release/liboxidd_ffi_c.a
	external/oxidd/build/include
	if-no-files-found: error
	retention-days: 1

	build-test:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5
	- name: Install toolchain
	run: \|
	sudo apt-get update
	sudo apt-get install -y --no-install-recommends \
	meson ninja-build flex bison gcc-14 valgrind
	- name: Configure
	env:
	CC: gcc-14
	run: meson setup build -Doxidd=disabled
	- name: Build
	run: ninja -C build
	- name: Run regression tests
	run: meson test -C build --print-errorlogs
	- name: Memory check (valgrind, no leaks/errors)
	run: \|
	set -e
	for args in \
	"tlsf2ltl test/cases/Patterns_Uright_uright06.tlsf" \
	"tlsf2ltl --parenthesize test/cases/Random_Lydia_case_03_50_05.tlsf" \
	"tlsf2ltl test/cases/operators.tlsf" \
	"tlsf2tlsf test/cases/defs.tlsf" \
	"tlsfinfo --generalized-reactivity test/cases/gr4_spec.tlsf" \
	"tlsf2tlsf --param n=5 test/cases/param_demo.tlsf"; do
	echo "valgrind: $args"
	valgrind --error-exitcode=1 --leak-check=full \
	--errors-for-leak-kinds=definite,indirect ./build/$args >/dev/null
	done

	build-clang:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5
	- name: Install toolchain
	run: \|
	sudo apt-get update
	sudo apt-get install -y --no-install-recommends \
	meson ninja-build flex bison clang
	- name: Configure, build and test
	env:
	CC: clang
	run: \|
	meson setup build-clang -Doxidd=disabled
	ninja -C build-clang
	meson test -C build-clang --print-errorlogs

	simd-matrix:
	runs-on: ubuntu-24.04
	strategy:
	fail-fast: false
	matrix:
	cpu: [baseline, x86-64-v2, avx2]
	steps:
	- uses: actions/checkout@v5
	- name: Install toolchain
	run: \|
	sudo apt-get update
	sudo apt-get install -y --no-install-recommends \
	meson ninja-build flex bison gcc-14
	- name: Configure, build, and test SIMD kernels
	env:
	CC: gcc-14
	run: \|
	meson setup build-simd-${{ matrix.cpu }} -Doxidd=disabled -Dcpu=${{ matrix.cpu }}
	ninja -C build-simd-${{ matrix.cpu }} simd_check
	meson test -C build-simd-${{ matrix.cpu }} simd_kernels --print-errorlogs

	# OxiDD-enabled build: links the shared FFI artifact, compiles the in-process
	# safety + GR(1) solvers (src/safety_oxidd.c, src/gr1_oxidd.c, src/aiger.c via
	# tlsfcompose/tlsfsolve) and runs the full suite. The Spot-verified
	# verify_aiger_oxidd* tests auto-gate on Spot (absent here) and run locally;
	# bounded_synthesis_harness still exercises a real in-process solve.
	build-oxidd:
	needs: oxidd
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5
	- name: Install toolchain
	run: \|
	sudo apt-get update
	sudo apt-get install -y --no-install-recommends \
	meson ninja-build flex bison gcc-14 python3
	- name: Download OxiDD FFI artifact
	uses: actions/download-artifact@v4
	with:
	name: oxidd-ffi
	path: external/oxidd
	- name: Configure, build and test (OxiDD enabled, AVX2 SIMD)
	env:
	CC: gcc-14
	run: \|
	# GitHub x86 runners are Haswell+ (AVX2-safe); exercises the
	# compile-time SIMD path in include/tlsf/simd.h.
	meson setup build-oxidd -Doxidd=enabled -Dcpu=avx2
	ninja -C build-oxidd
	meson test -C build-oxidd --print-errorlogs

	coverage:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5
	- name: Install toolchain
	run: \|
	sudo apt-get update
	sudo apt-get install -y --no-install-recommends \
	meson ninja-build flex bison gcc gcovr
	- name: Build with coverage and report
	run: \|
	# Coverage is measured on the dependency-free build with the
	# research CLIs enabled: they exercise graph/WL/template code without
	# requiring Rust/OxiDD. The OxiDD solver files compile only with
	# -Doxidd=enabled, and their correctness paths are exercised by the
	# Spot-verified suite (local). Enabling OxiDD here would add ~4k solver
	# lines to the denominator without Spot to cover them. Build and
	# measure with the runner's default gcc and its matching gcov; mixing
	# default gcc with gcov-14 makes gcov exit 3 and crashes gcovr. Gate on
	# the parsed line percentage.
	# aiger.c is excluded for the same reason as the solver files: it is an
	# OxiDD-path TU (the AIG game model) whose only callers
	# (main_tlsfcompose / csnf_emit_local_aiger) need -DHAVE_OXIDD, so it is
	# never exercised in this dependency-free build (0% here), yet it links
	# into the shared lib. It is covered by the local verify_aiger_oxidd*
	# suite. Counting its ~780 untestable-here lines just makes the gate
	# spuriously fragile.
	meson setup build-cov -Db_coverage=true -Dresearch_tools=true -Doxidd=disabled
	meson test -C build-cov
	summary=$(gcovr --root . \
	--filter 'src/' --exclude '.tlsf_(lex\|parse).' \
	--exclude '.*aiger\.c' \
	--print-summary 2>&1) \|\| true
	echo "$summary"
	pct=$(echo "$summary" \| grep -oE 'lines: [0-9.]+%' \| grep -oE '[0-9.]+')
	echo "parsed line coverage: ${pct}%"
	awk -v p="$pct" 'BEGIN{ if (p+0 < 75) { print "FAIL: line coverage below 75%"; exit 1 } }'

	perf-regression:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5
	- name: Install toolchain
	run: \|
	sudo apt-get update
	sudo apt-get install -y --no-install-recommends \
	meson ninja-build flex bison gcc-14 time
	- name: Build
	env:
	CC: gcc-14
	run: \|
	meson setup build -Doxidd=disabled
	ninja -C build
	- name: Perf regression guard (no syfco needed)
	run: bench/bench.sh --check

Navigation Menu

Uh oh!

Codex/decompose wrapper kill aiger #143

Workflow file

Codex/decompose wrapper kill aiger #143

Uh oh!

Workflow file for this run