Adding large-step encoding for CHCs in CProver (no [required] changes to the solver) #3379
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Build and Test the Rust API | |
| on: | |
| push: | |
| branches: [ develop ] | |
| pull_request: | |
| branches: [ develop ] | |
| env: | |
| default_build_dir: "build/" | |
| default_solver: "minisat2" | |
| default_include_dir: "src/libcprover-cpp/" | |
| # For now, we support two jobs: A Linux and a MacOS based one. | |
| # Both of the jobs use CMake, as we only support building the Rust | |
| # API with CMake (due to dependencies on CMake plugins). | |
| jobs: | |
| check-ubuntu-22_04-cmake-clang-rust: | |
| runs-on: ubuntu-22.04 | |
| env: | |
| CC: "ccache /usr/bin/clang-13" | |
| CXX: "ccache /usr/bin/clang++-13" | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: Fetch dependencies | |
| env: | |
| # This is needed in addition to -yq to prevent apt-get from asking for | |
| # user input | |
| DEBIAN_FRONTEND: noninteractive | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install --no-install-recommends -yq clang-13 clang++-13 flex bison libxml2-utils ccache | |
| - name: Log cargo/rust version | |
| run: cargo --version | |
| - name: Prepare ccache | |
| uses: actions/cache@v4 | |
| with: | |
| save-always: true | |
| path: .ccache | |
| key: ${{ runner.os }}-22.04-cmake-clang-${{ github.ref }}-${{ github.sha }}-PR | |
| restore-keys: | | |
| ${{ runner.os }}-22.04-cmake-clang-${{ github.ref }} | |
| ${{ runner.os }}-22.04-cmake-clang | |
| - name: ccache environment | |
| run: | | |
| echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
| echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
| - name: Zero ccache stats and limit in size | |
| run: ccache -z --max-size=500M | |
| # In our experiments while building this action script, the Ubuntu 22.04 build was failing with | |
| # the compiler indicating that it wanted the libraries to be built with `-fPIE` while it was | |
| # trying to link the Rust project. This was remedied by adding the `Position Independent Code` | |
| # directive during CBMC build time. It's worth mentioning that this wasn't observed on our | |
| # local experiments on the same platform, but it seems to be doing no harm to the build overall | |
| # and allows us to test the Rust API on Linux without issues. | |
| - name: Configure using CMake | |
| run: cmake -S. -B${{env.default_build_dir}} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DCMAKE_C_COMPILER=/usr/bin/clang-13 -DCMAKE_CXX_COMPILER=/usr/bin/clang++-13 -DWITH_JBMC=OFF | |
| - name: Build with CMake | |
| run: cmake --build ${{env.default_build_dir}} -j4 --target cprover-api-cpp | |
| - name: Print ccache stats | |
| run: ccache -s | |
| # We won't be running any of the regular regression tests, as these are covered | |
| # by the other jobs already present in `pull-request-checks.yaml`. | |
| - name: Run Rust API tests | |
| run: | | |
| VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))") | |
| cd src/libcprover-rust;\ | |
| cargo clean;\ | |
| CBMC_INCLUDE_DIR=../../${{env.default_include_dir}} CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1 | |
| check-macos-13-cmake-clang-rust: | |
| runs-on: macos-13 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: Fetch dependencies | |
| run: brew install cmake ninja flex bison ccache | |
| - name: Log cargo/rust version | |
| run: cargo --version | |
| - name: Prepare ccache | |
| uses: actions/cache@v4 | |
| with: | |
| save-always: true | |
| path: .ccache | |
| key: ${{ runner.os }}-Release-Minisat-${{ github.ref }}-${{ github.sha }}-PR-Rust-API | |
| restore-keys: | | |
| ${{ runner.os }}-Release-Minisat-${{ github.ref }} | |
| ${{ runner.os }}-Release-Minisat | |
| - name: ccache environment | |
| run: | | |
| echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV | |
| echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV | |
| - name: Zero ccache stats and limit in size | |
| run: ccache -z --max-size=500M | |
| - name: Configure using CMake | |
| run: cmake -S. -B${{env.default_build_dir}} -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -DWITH_JBMC=OFF | |
| - name: Build with Ninja | |
| run: cd ${{env.default_build_dir}}; ninja -j4 cprover-api-cpp | |
| - name: Print ccache stats | |
| run: ccache -s | |
| # We won't be running any of the regular regression tests, as these are covered | |
| # by the other jobs already present in `pull-request-checks.yaml`. | |
| - name: Run Rust API tests | |
| run: | | |
| export MACOSX_DEPLOYMENT_TARGET=10.15 | |
| VERSION=$(cat src/config.inc | python3 -c "import sys,re;line = [line for line in sys.stdin if re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search(r'CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))") | |
| cd src/libcprover-rust;\ | |
| cargo clean;\ | |
| CBMC_INCLUDE_DIR=../../${{env.default_include_dir}} CBMC_LIB_DIR=../../${{env.default_build_dir}}/lib CBMC_VERSION=$VERSION cargo test -- --test-threads=1 |