From 8aeefd5e751f7db238b9aff7fc7ccf16690cd96e Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 13 Nov 2023 17:12:28 +0000 Subject: [PATCH 1/7] Change `cxx bridge` to build with the flag for C++17 for files acompanying Rust API. --- src/libcprover-rust/build.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/libcprover-rust/build.rs b/src/libcprover-rust/build.rs index 338c4c77931..f5234f93d3f 100644 --- a/src/libcprover-rust/build.rs +++ b/src/libcprover-rust/build.rs @@ -72,7 +72,7 @@ fn main() { .include(cpp_api_include_path) .include(get_current_working_dir().unwrap()) .file("src/c_api.cc") - .flag_if_supported("-std=c++11") + .flag_if_supported("-std=c++17") .compile("cprover-rust-api"); println!("cargo:rerun-if-changed=src/c_api.cc"); From 1a5de732bf49d5480e83ea3d6ac9f9317bee09e6 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 13 Nov 2023 17:14:34 +0000 Subject: [PATCH 2/7] Change CI runner for macos Rust API test runner to macos13 instead of 12 --- .github/workflows/pull-request-check-rust-api.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml index a3faf73c8eb..533558d7e0b 100644 --- a/.github/workflows/pull-request-check-rust-api.yaml +++ b/.github/workflows/pull-request-check-rust-api.yaml @@ -68,8 +68,8 @@ jobs: 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-12-cmake-clang-rust: - runs-on: macos-12 + check-macos-13-cmake-clang-rust: + runs-on: macos-13 steps: - uses: actions/checkout@v3 with: From 206b1913663c1d94d54148124318af83e74e6519 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 14 Nov 2023 10:37:09 +0000 Subject: [PATCH 3/7] Change `cxx.rs` dependency feature-set at build time to bring inline with C++17 move. --- src/libcprover-rust/Cargo.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/libcprover-rust/Cargo.toml b/src/libcprover-rust/Cargo.toml index 37a3e866325..351345b5ff3 100644 --- a/src/libcprover-rust/Cargo.toml +++ b/src/libcprover-rust/Cargo.toml @@ -12,7 +12,7 @@ readme = "readme.md" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -cxx = "1.0" +cxx = { version = "1.0", default-features = false, features = ["std", "c++17"] } [build-dependencies] cxx-build = "1.0" From b87d4428b93021013212e8aa7baed95eb2e35536 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 14 Nov 2023 10:38:59 +0000 Subject: [PATCH 4/7] Minor change to test to silence warning about unused binding in pattern matching during build. --- src/libcprover-rust/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/libcprover-rust/src/lib.rs b/src/libcprover-rust/src/lib.rs index a683a55d878..57d9e97c146 100644 --- a/src/libcprover-rust/src/lib.rs +++ b/src/libcprover-rust/src/lib.rs @@ -517,7 +517,7 @@ mod tests { if let Ok(el) = results { let_cxx_string!(non_existing_property = "main.the.jabberwocky"); let prop_status = cprover_api::get_property_status(&el, &non_existing_property); - if let Err(status) = prop_status { + if let Err(_status) = prop_status { Ok(()) } else { let error_msg = format!( From 732ab7ff8cd9d677c443a519c7caca5dd1776dd7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 13 Nov 2023 16:38:06 +0000 Subject: [PATCH 5/7] Fix invalid-escape-sequence warning Python warns about the use of `\d`: we should use raw strings here as that's not meant to be an escape sequence. --- .github/workflows/pull-request-check-rust-api.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml index 533558d7e0b..a66a0ef6ecf 100644 --- a/.github/workflows/pull-request-check-rust-api.yaml +++ b/.github/workflows/pull-request-check-rust-api.yaml @@ -62,7 +62,7 @@ jobs: # 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('CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))") + 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 @@ -102,7 +102,7 @@ jobs: # 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('CBMC_VERSION = (\d+\.\d+\.\d+)', line)];sys.stdout.write(re.search('CBMC_VERSION = (\d+\.\d+\.\d+)', line[0]).group(1))") + 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 From b2549cb41e24987500a0ca27b521d7ea29039e2b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 14 Nov 2023 12:08:16 +0000 Subject: [PATCH 6/7] Fix libstdc++-not-found error See https://github.com/diffblue/cbmc/actions/runs/6856483568/job/18643716705?pr=6749 for one example of the failure: cargo-induced clang runs (via the cc crate) weren't finding the C++ library (which ought to be libc++ and not libstdc++ on this MacOS target). This appears to be caused by the minimum build target being too low (where the cc crate is the one setting that minimum). Override that by setting an environment variable. See https://github.com/rust-lang/cc-rs/blob/2d6a3b2119cf5eacc01e1f2877e064a7aede7819/src/lib.rs#L3497C52-L3497C76 for the Rust code implementing the logic. --- .github/workflows/pull-request-check-rust-api.yaml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml index a66a0ef6ecf..35865abac33 100644 --- a/.github/workflows/pull-request-check-rust-api.yaml +++ b/.github/workflows/pull-request-check-rust-api.yaml @@ -102,6 +102,7 @@ jobs: # 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;\ From 5f0d5dfa302f0f3f63accb8fa2bfaaac57f50501 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 14 Nov 2023 12:38:54 +0000 Subject: [PATCH 7/7] Fix ccache configuration of check-macos-12-cmake-clang-rust The prefix lookup resulted in picking up the Release-Glucose cache from check-macos-12-cmake-clang. This cache, however, was established with Glucose as a SAT solver, which implies different compiler command lines. Consequently, there would be 0 cache hits. --- .github/workflows/pull-request-check-rust-api.yaml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/pull-request-check-rust-api.yaml b/.github/workflows/pull-request-check-rust-api.yaml index 35865abac33..710ac1e21d1 100644 --- a/.github/workflows/pull-request-check-rust-api.yaml +++ b/.github/workflows/pull-request-check-rust-api.yaml @@ -82,10 +82,10 @@ jobs: uses: actions/cache@v3 with: path: .ccache - key: ${{ runner.os }}-Release-${{ github.ref }}-${{ github.sha }}-PR-Rust-API + key: ${{ runner.os }}-Release-Minisat-${{ github.ref }}-${{ github.sha }}-PR-Rust-API restore-keys: | - ${{ runner.os }}-Release-${{ github.ref }} - ${{ runner.os }}-Release + ${{ runner.os }}-Release-Minisat-${{ github.ref }} + ${{ runner.os }}-Release-Minisat - name: ccache environment run: | echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV