c2rtl

.bazelrc

@@ -8,6 +8,12 @@ build --host_cxxopt=-std=c++20
 # host toolchain, so the guard is Linux-scoped.
 common:linux --repo_env=BAZEL_DO_NOT_DETECT_CPP_TOOLCHAIN=1
 
+# rules_foreign_cc invokes host tools such as cmake from sandboxed actions.
+# On macOS those tools usually live under Homebrew, which is not always present
+# in Bazel's default action PATH.
+build:macos --action_env=PATH=/opt/homebrew/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin
+build:macos --repo_env=PATH=/opt/homebrew/bin:/usr/local/bin:/usr/bin:/bin:/usr/sbin:/sbin
+
 # Force C11 for host tools to work around rules_foreign_cc pkg-config
 # bootstrap failure: bundled glib uses 'bool' as a struct field name,
 # which is a keyword in GCC 15's default C23 mode.

.github/scripts/install-cmake-deps-ubuntu.sh

@@ -0,0 +1,159 @@
+#!/usr/bin/env bash
+# Copyright 2026 keplertech.io
+# SPDX-License-Identifier: GPL-3.0-only
+
+set -euo pipefail
+
+llvm_version="${KEPLER_LLVM_VERSION:-22}"
+# shellcheck disable=SC1091
+source /etc/os-release
+ubuntu_codename="${VERSION_CODENAME:-jammy}"
+llvm_keyring="/usr/share/keyrings/llvm-snapshot.gpg"
+llvm_list="/etc/apt/sources.list.d/llvm-toolchain-${ubuntu_codename}-${llvm_version}.list"
+
+sudo apt-get update
+sudo apt-get install -yq ca-certificates curl gnupg lsb-release
+
+if [[ ! -f "${llvm_keyring}" ]]; then
+  curl -fsSL https://apt.llvm.org/llvm-snapshot.gpg.key \
+    | sudo gpg --dearmor -o "${llvm_keyring}"
+fi
+printf 'deb [signed-by=%s] https://apt.llvm.org/%s/ llvm-toolchain-%s-%s main\n' \
+  "${llvm_keyring}" "${ubuntu_codename}" "${ubuntu_codename}" "${llvm_version}" \
+  | sudo tee "${llvm_list}" >/dev/null
+
+sudo apt-get update
+sudo apt-get install -yq \
+  build-essential cmake ninja-build pkg-config curl ca-certificates \
+  bison flex doxygen python3-dev \
+  "clang-${llvm_version}" "clang-tools-${llvm_version}" \
+  "llvm-${llvm_version}-dev" \
+  "libclang-${llvm_version}-dev" "libclang-cpp${llvm_version}-dev" \
+  libboost-dev libboost-iostreams-dev libfl-dev \
+  capnproto libcapnp-dev libtbb-dev libspdlog-dev libfmt-dev \
+  libgtest-dev libssl-dev \
+  libz3-dev zlib1g-dev \
+  "$@"
+
+absl_version="20260107.0"
+protobuf_version="${KEPLER_PROTOBUF_VERSION:-35.1}"
+re2_version="${KEPLER_RE2_VERSION:-2025-11-05}"
+ortools_version="${KEPLER_ORTOOLS_VERSION:-9.15}"
+absl_prefix="/usr/local"
+absl_config="${absl_prefix}/lib/cmake/absl/abslConfig.cmake"
+
+if [[ ! -f "${absl_config}" ]]; then
+  work_dir="${RUNNER_TEMP:-/tmp}/abseil-cpp-${absl_version}"
+  src_dir="${work_dir}/src"
+  build_dir="${work_dir}/build"
+
+  rm -rf "${work_dir}"
+  mkdir -p "${work_dir}"
+  curl -L "https://github.com/abseil/abseil-cpp/archive/refs/tags/${absl_version}.tar.gz" \
+    -o "${work_dir}/abseil-cpp.tar.gz"
+  tar -xzf "${work_dir}/abseil-cpp.tar.gz" -C "${work_dir}"
+  mv "${work_dir}/abseil-cpp-${absl_version}" "${src_dir}"
+
+  cmake -S "${src_dir}" -B "${build_dir}" \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DCMAKE_CXX_STANDARD=20 \
+    -DCMAKE_C_COMPILER="clang-${llvm_version}" \
+    -DCMAKE_CXX_COMPILER="clang++-${llvm_version}" \
+    -DCMAKE_POSITION_INDEPENDENT_CODE=ON \
+    -DABSL_BUILD_TESTING=OFF \
+    -DABSL_ENABLE_INSTALL=ON \
+    -DABSL_PROPAGATE_CXX_STD=ON \
+    -DCMAKE_INSTALL_PREFIX="${absl_prefix}"
+  cmake --build "${build_dir}" -j "$(nproc)"
+  sudo cmake --install "${build_dir}"
+  sudo ldconfig
+fi
+
+re2_prefix="/usr/local"
+re2_header="${re2_prefix}/include/re2/re2.h"
+
+if [[ ! -f "${re2_header}" ]]; then
+  work_dir="${RUNNER_TEMP:-/tmp}/re2-${re2_version}"
+  src_dir="${work_dir}/src"
+  build_dir="${work_dir}/build"
+
+  rm -rf "${work_dir}"
+  mkdir -p "${work_dir}"
+  curl -L "https://github.com/google/re2/archive/refs/tags/${re2_version}.tar.gz" \
+    -o "${work_dir}/re2.tar.gz"
+  tar -xzf "${work_dir}/re2.tar.gz" -C "${work_dir}"
+  mv "${work_dir}/re2-${re2_version}" "${src_dir}"
+
+  cmake -S "${src_dir}" -B "${build_dir}" \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DCMAKE_CXX_STANDARD=20 \
+    -DCMAKE_C_COMPILER="clang-${llvm_version}" \
+    -DCMAKE_CXX_COMPILER="clang++-${llvm_version}" \
+    -DCMAKE_POSITION_INDEPENDENT_CODE=ON \
+    -DRE2_BUILD_TESTING=OFF \
+    -DCMAKE_PREFIX_PATH="${absl_prefix}" \
+    -DCMAKE_INSTALL_PREFIX="${re2_prefix}"
+  cmake --build "${build_dir}" -j "$(nproc)"
+  sudo cmake --install "${build_dir}"
+  sudo ldconfig
+fi
+
+protobuf_prefix="/usr/local"
+protobuf_config="${protobuf_prefix}/lib/cmake/protobuf/protobuf-config.cmake"
+
+if [[ ! -f "${protobuf_config}" ]]; then
+  work_dir="${RUNNER_TEMP:-/tmp}/protobuf-${protobuf_version}"
+  src_dir="${work_dir}/src"
+  build_dir="${work_dir}/build"
+
+  rm -rf "${work_dir}"
+  mkdir -p "${work_dir}"
+  curl -L "https://github.com/protocolbuffers/protobuf/releases/download/v${protobuf_version}/protobuf-${protobuf_version}.tar.gz" \
+    -o "${work_dir}/protobuf.tar.gz"
+  tar -xzf "${work_dir}/protobuf.tar.gz" -C "${work_dir}"
+  mv "${work_dir}/protobuf-${protobuf_version}" "${src_dir}"
+
+  cmake -S "${src_dir}" -B "${build_dir}" \
+    -DCMAKE_BUILD_TYPE=Release \
+    -DCMAKE_CXX_STANDARD=20 \
+    -DCMAKE_C_COMPILER="clang-${llvm_version}" \
+    -DCMAKE_CXX_COMPILER="clang++-${llvm_version}" \
+    -DCMAKE_POSITION_INDEPENDENT_CODE=ON \
+    -Dprotobuf_BUILD_TESTS=OFF \
+    -DBUILD_SHARED_LIBS=ON \
+    -Dprotobuf_BUILD_SHARED_LIBS=ON \
+    -Dprotobuf_ABSL_PROVIDER=package \
+    -Dprotobuf_BUILD_PROTOC_BINARIES=ON \
+    -Dprotobuf_INSTALL=ON \
+    -DCMAKE_PREFIX_PATH="${absl_prefix}" \
+    -DCMAKE_INSTALL_PREFIX="${protobuf_prefix}"
+  cmake --build "${build_dir}" -j "$(nproc)"
+  sudo cmake --install "${build_dir}"
+  sudo ldconfig
+fi
+
+ortools_prefix="/usr/local"
+ortools_header="${ortools_prefix}/include/ortools/graph/graph.h"
+
+if [[ ! -f "${ortools_header}" ]]; then
+  work_dir="${RUNNER_TEMP:-/tmp}/or-tools-${ortools_version}"
+  src_dir="${work_dir}/src"
+
+  rm -rf "${work_dir}"
+  mkdir -p "${src_dir}"
+  curl -L \
+    "https://github.com/google/or-tools/releases/download/v${ortools_version}/or-tools-${ortools_version}.tar.gz" \
+    -o "${work_dir}/or-tools.tar.gz"
+  tar -xzf "${work_dir}/or-tools.tar.gz" \
+    -C "${src_dir}" \
+    --strip-components=1
+
+  sudo mkdir -p "${ortools_prefix}/include"
+  sudo cp -R "${src_dir}/ortools" "${ortools_prefix}/include/"
+fi
+
+if [[ -n "${GITHUB_ENV:-}" ]]; then
+  echo "CPATH=${ortools_prefix}/include${CPATH:+:${CPATH}}" >> "${GITHUB_ENV}"
+  echo "CPLUS_INCLUDE_PATH=${ortools_prefix}/include${CPLUS_INCLUDE_PATH:+:${CPLUS_INCLUDE_PATH}}" >> "${GITHUB_ENV}"
+  echo "CXXFLAGS=-I${ortools_prefix}/include${CXXFLAGS:+ ${CXXFLAGS}}" >> "${GITHUB_ENV}"
+fi

.github/workflows/bazel.yml

@@ -13,13 +13,16 @@ jobs:
 
     steps:
     - uses: actions/checkout@v4
-      # No submodules needed — Bazel fetches deps via http_archive
+      with:
+        submodules: true
+      # Bazel fetches most deps via http_archive/BCR, but the C2RTL overlay
+      # deliberately builds from the pinned thirdparty/xls checkout.
 
     - name: Cache Bazel outputs
       uses: actions/cache@v4
       with:
         path: ~/.cache/bazel
-        key: bazel-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel') }}
+        key: bazel-${{ runner.os }}-${{ hashFiles('MODULE.bazel', 'bazel/deps.bzl', 'bazel/*.BUILD.bazel', 'bazel/*.bzl') }}
         restore-keys: |
           bazel-${{ runner.os }}-
 
@@ -28,7 +31,7 @@ jobs:
         sudo apt-get update
         sudo apt-get install -yq \
           build-essential pkg-config \
-          bison flex python3-dev
+          bison cmake flex ninja-build python3-dev
 
     - name: Build kepler-formal
       run: bazelisk build //src/bin:kepler-formal

.github/workflows/c-cpp.yml

@@ -18,25 +18,17 @@ jobs:
     - uses: actions/checkout@v4
       with:
         submodules: true
-     # install dependencies
-    - name: Install GoogleTest
-      run: sudo apt-get update && sudo apt-get install -y libgtest-dev cmake
     - name: Checkout submodules
       run: git submodule update --init --recursive
 
     - name: Install system dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -yq \
-          build-essential cmake ninja-build clang pkg-config \
-          libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
-          libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev
+      run: bash .github/scripts/install-cmake-deps-ubuntu.sh
 
     - name: Configure CMake
       working-directory: ${{github.workspace}}/
       run: |
         rm -rf build
-        cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
+        cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang-22 -DCMAKE_CXX_COMPILER=clang++-22 -DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" -DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
 
 
     - name: Build
@@ -47,4 +39,3 @@ jobs:
       env:
         PYTHONMALLOC: malloc
       run: ctest -VV -E ".*[p|P]ython.*" -C ${{ env.BUILD_TYPE }}
-

.github/workflows/coverage.yml

@@ -20,31 +20,23 @@ jobs:
         fetch-depth: 0
         submodules: true
 
-     # install dependencies
-    - name: Install GoogleTest
-      run: sudo apt-get update && sudo apt-get install -y libgtest-dev cmake
     - name: Checkout submodules
       run: git submodule update --init --recursive
 
     - name: Install system dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -yq \
-          build-essential cmake ninja-build clang pkg-config \
-          libboost-dev libfl-dev libtbb-dev capnproto libcapnp-dev \
-          libgtest-dev libspdlog-dev libfmt-dev libboost-iostreams-dev zlib1g-dev lcov
+      run: bash .github/scripts/install-cmake-deps-ubuntu.sh lcov
 
     - name: Configure CMake
       # Configure CMake in a 'build' subdirectory. `CMAKE_BUILD_TYPE` is only required if you are using a single-configuration generator such as make.
       # See https://cmake.org/cmake/help/latest/variable/CMAKE_BUILD_TYPE.html?highlight=cmake_build_type
-      run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DCODE_COVERAGE=ON -DLONG_TESTS=ON
+      run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -DCMAKE_C_COMPILER=clang-22 -DCMAKE_CXX_COMPILER=clang++-22 -DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" -DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 -DCODE_COVERAGE=ON -DLONG_TESTS=ON -DCMAKE_CXX_STANDARD=20
 
     - name: Build
       # Build your program with the given configuration
       run: cmake --build ${{github.workspace}}/build -j 4 --config ${{env.BUILD_TYPE}}
       env:
-        CC:   clang
-        CXX:  clang++
+        CC:   clang-22
+        CXX:  clang++-22
 
     - name: Test
       working-directory: ${{github.workspace}}/build

.github/workflows/cva6imc.yml

@@ -17,12 +17,7 @@ jobs:
         submodules: true
 
     - name: Install dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -y \
-          libgtest-dev cmake pkg-config libboost-dev libfl-dev \
-          capnproto libcapnp-dev ninja-build libtbb-dev libspdlog-dev \
-          libboost-iostreams-dev zlib1g-dev
+      run: bash .github/scripts/install-cmake-deps-ubuntu.sh
 
     - name: Checkout submodules
       run: git submodule update --init --recursive
@@ -31,6 +26,10 @@ jobs:
       run: |
         cmake -B ${{github.workspace}}/build \
           -GNinja \
+          -DCMAKE_C_COMPILER=clang-22 \
+          -DCMAKE_CXX_COMPILER=clang++-22 \
+          -DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" \
+          -DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 \
           -DPYTHON_INTERFACE=OFF \
           -DCMAKE_BUILD_TYPE=Release \
           -DCMAKE_CXX_STANDARD=20 \

.github/workflows/cva6ki.yml

@@ -17,12 +17,7 @@ jobs:
         submodules: true
 
     - name: Install dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -y \
-          libgtest-dev cmake pkg-config libboost-dev libfl-dev \
-          capnproto libcapnp-dev ninja-build libtbb-dev libspdlog-dev \
-          libboost-iostreams-dev zlib1g-dev
+      run: bash .github/scripts/install-cmake-deps-ubuntu.sh
 
     - name: Checkout submodules
       run: git submodule update --init --recursive
@@ -31,6 +26,10 @@ jobs:
       run: |
         cmake -B ${{github.workspace}}/build \
           -GNinja \
+          -DCMAKE_C_COMPILER=clang-22 \
+          -DCMAKE_CXX_COMPILER=clang++-22 \
+          -DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" \
+          -DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 \
           -DPYTHON_INTERFACE=OFF \
           -DCMAKE_BUILD_TYPE=Release \
           -DCMAKE_CXX_STANDARD=20 \

.github/workflows/cva6pdr.yml

@@ -17,12 +17,7 @@ jobs:
         submodules: true
 
     - name: Install dependencies
-      run: |
-        sudo apt-get update
-        sudo apt-get install -y \
-          libgtest-dev cmake pkg-config libboost-dev libfl-dev \
-          capnproto libcapnp-dev ninja-build libtbb-dev libspdlog-dev \
-          libboost-iostreams-dev zlib1g-dev
+      run: bash .github/scripts/install-cmake-deps-ubuntu.sh
 
     - name: Checkout submodules
       run: git submodule update --init --recursive
@@ -31,6 +26,10 @@ jobs:
       run: |
         cmake -B ${{github.workspace}}/build \
           -GNinja \
+          -DCMAKE_C_COMPILER=clang-22 \
+          -DCMAKE_CXX_COMPILER=clang++-22 \
+          -DCMAKE_PREFIX_PATH="/usr/local;/usr/lib/llvm-22" \
+          -DCMAKE_CXX_COMPILER_CLANG_SCAN_DEPS=clang-scan-deps-22 \
           -DPYTHON_INTERFACE=OFF \
           -DCMAKE_BUILD_TYPE=Release \
           -DCMAKE_CXX_STANDARD=20 \

.github/workflows/macOS.yml

@@ -27,15 +27,38 @@ jobs:
       run: git submodule update --init --recursive
     # install dependencies
     - name: Install dependencies
-      run: brew install cmake doxygen capnp tbb bison flex boost spdlog zlib
+      run: brew install cmake doxygen capnp tbb bison flex boost spdlog zlib abseil protobuf openssl@3 llvm z3 re2 googletest
     - name: set env variable
       run: |
         echo "/usr/local/opt/flex/bin" >> $GITHUB_PATH; echo "/usr/local/opt/bison/bin" >> $GITHUB_PATH;
         echo "/opt/homebrew/opt/flex/bin" >> $GITHUB_PATH; echo "/opt/homebrew/opt/bison/bin" >> $GITHUB_PATH
-    - name: Install GTest
-      run: brew install googletest
+        echo "GTEST_PREFIX=$(brew --prefix googletest)" >> $GITHUB_ENV
+        echo "CMAKE_PREFIX_PATH=$(brew --prefix llvm);$(brew --prefix openssl@3);$(brew --prefix abseil);$(brew --prefix protobuf);$(brew --prefix re2);$(brew --prefix z3);$(brew --prefix googletest)" >> $GITHUB_ENV
+        echo "CPATH=$(brew --prefix googletest)/include${CPATH:+:${CPATH}}" >> $GITHUB_ENV
+        echo "CPLUS_INCLUDE_PATH=$(brew --prefix googletest)/include${CPLUS_INCLUDE_PATH:+:${CPLUS_INCLUDE_PATH}}" >> $GITHUB_ENV
+    - name: Install OR-Tools headers
+      run: |
+        ORTOOLS_VERSION=9.15
+        ORTOOLS_HEADER=/usr/local/include/ortools/graph/graph.h
+        if [ ! -f "${ORTOOLS_HEADER}" ]; then
+          WORK_DIR="${RUNNER_TEMP}/or-tools-${ORTOOLS_VERSION}"
+          SRC_DIR="${WORK_DIR}/src"
+          rm -rf "${WORK_DIR}"
+          mkdir -p "${SRC_DIR}"
+          curl -L \
+            "https://github.com/google/or-tools/releases/download/v${ORTOOLS_VERSION}/or-tools-${ORTOOLS_VERSION}.tar.gz" \
+            -o "${WORK_DIR}/or-tools.tar.gz"
+          tar -xzf "${WORK_DIR}/or-tools.tar.gz" \
+            -C "${SRC_DIR}" \
+            --strip-components=1
+          sudo mkdir -p /usr/local/include
+          sudo cp -R "${SRC_DIR}/ortools" /usr/local/include/
+        fi
+        echo "CPATH=/usr/local/include${CPATH:+:${CPATH}}" >> "${GITHUB_ENV}"
+        echo "CPLUS_INCLUDE_PATH=/usr/local/include${CPLUS_INCLUDE_PATH:+:${CPLUS_INCLUDE_PATH}}" >> "${GITHUB_ENV}"
+        echo "CXXFLAGS=-I/usr/local/include${CXXFLAGS:+ ${CXXFLAGS}}" >> "${GITHUB_ENV}"
     - name: Configure CMake
-      run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=clang -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
+      run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}} -GNinja -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -DCMAKE_CXX_FLAGS="-I/usr/local/include -I${GTEST_PREFIX}/include" -DCMAKE_PREFIX_PATH="${CMAKE_PREFIX_PATH}" -DENABLE_SANITIZERS=ON -DPYTHON_INTERFACE=OFF -DCMAKE_CXX_STANDARD=20
     - name: Build
       # Build your program with the given configuration
       run: cmake --build ${{github.workspace}}/build --config ${{env.BUILD_TYPE}}