Skip to content

Commit ffd8bdd

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #7498 from NlightNFotis/test_rust_api_ci
Add Github Actions jobs for testing the Rust API in CI
2 parents caf5b94 + 2b90d64 commit ffd8bdd

File tree

4 files changed

+118
-6
lines changed

4 files changed

+118
-6
lines changed

‎.github/workflows/pull-request-check-rust-api.yaml

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
name: Build and Test the Rust API
2+
on:
3+
push:
4+
branches: [ develop ]
5+
pull_request:
6+
branches: [ develop ]
7+
env:
8+
default_build_dir: "build/"
9+
default_solver: "minisat2"
10+
11+
# For now, we support two jobs: A Linux and a MacOS based one.
12+
# Both of the jobs use CMake, as we only support building the Rust
13+
# API with CMake (due to dependencies on CMake plugins).
14+
jobs:
15+
check-ubuntu-22_04-cmake-clang-rust:
16+
runs-on: ubuntu-22.04
17+
env:
18+
CC: "ccache /usr/bin/clang-13"
19+
CXX: "ccache /usr/bin/clang++-13"
20+
steps:
21+
- uses: actions/checkout@v3
22+
with:
23+
submodules: recursive
24+
- name: Fetch dependencies
25+
env:
26+
# This is needed in addition to -yq to prevent apt-get from asking for
27+
# user input
28+
DEBIAN_FRONTEND: noninteractive
29+
run: |
30+
sudo apt-get update
31+
sudo apt-get install --no-install-recommends -yq clang-13 clang++-13 maven flex bison libxml2-utils ccache
32+
- name: Log cargo/rust version
33+
run: cargo --version
34+
- name: Prepare ccache
35+
uses: actions/cache@v3
36+
with:
37+
path: .ccache
38+
key: ${{ runner.os }}-22.04-cmake-clang-${{ github.ref }}-${{ github.sha }}-PR
39+
restore-keys: |
40+
${{ runner.os }}-22.04-cmake-clang-${{ github.ref }}
41+
${{ runner.os }}-22.04-cmake-clang
42+
- name: ccache environment
43+
run: |
44+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
45+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
46+
- name: Zero ccache stats and limit in size
47+
run: ccache -z --max-size=500M
48+
# In our experiments while building this action script, the Ubuntu 22.04 build was failing with
49+
# the compiler indicating that it wanted the libraries to be built with `-fPIE` while it was
50+
# trying to link the Rust project. This was remedied by adding the `Position Independent Code`
51+
# directive during CBMC build time. It's worth mentioning that this wasn't observed on our
52+
# local experiments on the same platform, but it seems to be doing no harm to the build overall
53+
# and allows us to test the Rust API on Linux without issues.
54+
- name: Configure using CMake
55+
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_RUST_API=ON
56+
- name: Build with CMake
57+
run: cmake --build ${{env.default_build_dir}} -j2
58+
- name: Print ccache stats
59+
run: ccache -s
60+
# We won't be running any of the regular regression tests, as these are covered
61+
# by the other jobs already present in `pull-request-checks.yaml`.
62+
- name: Run Rust API tests
63+
run: |
64+
cd src/libcprover-rust;\
65+
cargo clean;\
66+
CBMC_BUILD_DIR=../../${{env.default_build_dir}} SAT_IMPL=${{env.default_solver}} cargo test -- --test-threads=1
67+
68+
69+
check-macos-12-cmake-clang-rust:
70+
runs-on: macos-12
71+
steps:
72+
- uses: actions/checkout@v3
73+
with:
74+
submodules: recursive
75+
- name: Fetch dependencies
76+
run: brew install cmake ninja maven flex bison ccache
77+
- name: Log cargo/rust version
78+
run: cargo --version
79+
- name: Prepare ccache
80+
uses: actions/cache@v3
81+
with:
82+
path: .ccache
83+
key: ${{ runner.os }}-Release-${{ github.ref }}-${{ github.sha }}-PR-Rust-API
84+
restore-keys: |
85+
${{ runner.os }}-Release-${{ github.ref }}
86+
${{ runner.os }}-Release
87+
- name: ccache environment
88+
run: |
89+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
90+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
91+
- name: Zero ccache stats and limit in size
92+
run: ccache -z --max-size=500M
93+
- name: Configure using CMake
94+
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_RUST_API=ON
95+
- name: Build with Ninja
96+
run: cd ${{env.default_build_dir}}; ninja -j3
97+
- name: Print ccache stats
98+
run: ccache -s
99+
# We won't be running any of the regular regression tests, as these are covered
100+
# by the other jobs already present in `pull-request-checks.yaml`.
101+
- name: Run Rust API tests
102+
run: |
103+
cd src/libcprover-rust;\
104+
cargo clean;\
105+
CBMC_BUILD_DIR=../../${{env.default_build_dir}} SAT_IMPL=${{env.default_solver}} cargo test -- --test-threads=1

‎.github/workflows/pull-request-checks.yaml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -521,9 +521,9 @@ jobs:
521521
uses: actions/cache@v3
522522
with:
523523
path: .ccache
524-
key: ${{ runner.os }}-Release-${{ github.ref }}-${{ github.sha }}-PR
524+
key: ${{ runner.os }}-Release-Glucose${{ github.ref }}-${{ github.sha }}-PR
525525
restore-keys: |
526-
${{ runner.os }}-Release-${{ github.ref }}
526+
${{ runner.os }}-Release-Glucose${{ github.ref }}
527527
${{ runner.os }}-Release
528528
- name: ccache environment
529529
run: |

‎src/libcprover-rust/other/example.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
// File just to allow smoke testing of Rust API while tests are run.
2+
3+
int main(int argc, char *argv[])
4+
{
5+
int arr[] = {0, 1, 2, 3};
6+
__CPROVER_assert(arr[3] != 3, "expected failure: arr[3] == 3");
7+
}

‎src/libcprover-rust/src/lib.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ mod tests {
5555
#[test]
5656
fn translate_vector_of_rust_string_to_cpp() {
5757
let vec: Vec<String> = vec![
58-
"/tmp/example.c".to_owned(),
58+
"other/example.c".to_owned(),
5959
"/tmp/example2.c".to_owned()];
6060

6161
let vect = ffi::translate_vector_of_string(vec);
@@ -71,7 +71,7 @@ mod tests {
7171
};
7272

7373
let vec: Vec<String> = vec![
74-
"/tmp/example.c".to_owned()];
74+
"other/example.c".to_owned()];
7575

7676
let vect = ffi::translate_vector_of_string(vec);
7777
assert_eq!(vect.len(), 1);
@@ -91,7 +91,7 @@ mod tests {
9191
let client = ffi::new_api_session();
9292

9393
let vec: Vec<String> = vec![
94-
"/tmp/example.c".to_owned()];
94+
"other/example.c".to_owned()];
9595

9696
let vect = ffi::translate_vector_of_string(vec);
9797
client.load_model_from_files(vect);
@@ -114,7 +114,7 @@ mod tests {
114114
};
115115

116116
let vec: Vec<String> = vec![
117-
"/tmp/example.c".to_owned()];
117+
"other/example.c".to_owned()];
118118

119119
let vect = ffi::translate_vector_of_string(vec);
120120
assert_eq!(vect.len(), 1);

0 commit comments

Comments
 (0)