From 9f30430d2cbb6111fbbb55a1f2728f851eeee131 Mon Sep 17 00:00:00 2001 From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com> Date: Wed, 29 Mar 2023 18:23:23 -0400 Subject: [PATCH 1/3] Use workspaces and clippy in workflow Run clippy in parallel --- .github/workflows/rust.yml | 35 +++++++++++++++++------------------ 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/.github/workflows/rust.yml b/.github/workflows/rust.yml index 4315c307..59102280 100644 --- a/.github/workflows/rust.yml +++ b/.github/workflows/rust.yml @@ -8,6 +8,7 @@ on: env: CARGO_INCREMENTAL: 0 + CARGO_REGISTRIES_CRATES_IO_PROTOCOL: sparse RUSTFLAGS: "-D warnings" jobs: @@ -39,12 +40,6 @@ jobs: - uses: actions/checkout@v2 with: submodules: recursive - - name: Install LLVM and Clang # required for bindgen to work, see https://github.com/rust-lang/rust-bindgen/issues/1797 - uses: KyleMayes/install-llvm-action@v1 - if: matrix.os == 'windows-latest' - with: - version: "11.0" - directory: ${{ runner.temp }}/llvm - name: Install emscripten run: | cd ~ @@ -56,14 +51,11 @@ jobs: source ./emsdk_env.sh - name: Install wasm32-unknown-emscripten target run: rustup target add wasm32-unknown-emscripten - - name: Build z3-sys with statically linked Z3 - run: | - source ~/emsdk/emsdk_env.sh - cargo build --target=wasm32-unknown-emscripten --manifest-path z3-sys/Cargo.toml -vv --features static-link-z3 - - name: Build z3 with statically linked Z3 + - name: Build z3-sys and z3 with statically linked Z3 run: | source ~/emsdk/emsdk_env.sh - cargo build --target=wasm32-unknown-emscripten --manifest-path z3/Cargo.toml -vv --features static-link-z3 + cargo build --target=wasm32-unknown-emscripten -vv --features static-link-z3 + build_z3_statically: strategy: matrix: @@ -89,11 +81,18 @@ jobs: - name: Set LIBCLANG_PATH run: echo "LIBCLANG_PATH=$((gcm clang).source -replace "clang.exe")" >> $env:GITHUB_ENV if: matrix.os == 'windows-latest' - - name: Build z3-sys with statically linked Z3 - run: cargo build --manifest-path z3-sys/Cargo.toml -vv --features static-link-z3 - - name: Build z3 with statically linked Z3 - run: cargo build --manifest-path z3/Cargo.toml -vv --features static-link-z3 - - name: Test `z3` with statically linked Z3 - run: cargo test --manifest-path z3/Cargo.toml -vv --features static-link-z3 + - name: Build `z3-sys` and `z3` with statically linked Z3 + run: cargo build -vv --features static-link-z3 + - name: Test `z3-sys` and `z3` with statically linked Z3 + run: cargo test -vv --features static-link-z3 - name: Test `z3` with statically linked Z3 and `arbitrary-size-numeral` enabled run: cargo test --manifest-path z3/Cargo.toml -vv --features 'static-link-z3 arbitrary-size-numeral' + + run_clippy: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v2 + with: + submodules: recursive + - name: Run clippy + run: cargo clippy -vv --features static-link-z3 --all-targets \ No newline at end of file From 17a335ffcfe67647976dfdb4186de09f7f80b508 Mon Sep 17 00:00:00 2001 From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com> Date: Thu, 30 Mar 2023 00:02:32 -0400 Subject: [PATCH 2/3] fix build.rs clippy lint --- z3-sys/build.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/z3-sys/build.rs b/z3-sys/build.rs index 18ab9edf..010c1aeb 100644 --- a/z3-sys/build.rs +++ b/z3-sys/build.rs @@ -82,11 +82,10 @@ fn build_z3() { let target = std::env::var("TARGET").unwrap(); if target.contains("msvc") { None - } else if target.contains("apple") { - Some("c++".to_string()) - } else if target.contains("freebsd") { - Some("c++".to_string()) - } else if target.contains("openbsd") { + } else if target.contains("apple") + | target.contains("freebsd") + | target.contains("openbsd") + { Some("c++".to_string()) } else { Some("stdc++".to_string()) From 9d9e56cc837a409f8092687d964b623b099ff3a2 Mon Sep 17 00:00:00 2001 From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com> Date: Fri, 31 Mar 2023 14:32:26 -0400 Subject: [PATCH 3/3] fix clippy lints in tests --- z3-sys/tests/lib.rs | 14 +++-------- z3/tests/lib.rs | 54 ++++++++++++++++++++++------------------ z3/tests/objectives.rs | 4 +-- z3/tests/ops.rs | 2 +- z3/tests/semver_tests.rs | 17 ++++++------- 5 files changed, 44 insertions(+), 47 deletions(-) diff --git a/z3-sys/tests/lib.rs b/z3-sys/tests/lib.rs index 651df3a5..c6b137cb 100644 --- a/z3-sys/tests/lib.rs +++ b/z3-sys/tests/lib.rs @@ -39,19 +39,13 @@ fn smoketest() { // Grab the actual constant values out of the model let mut interp_x: Z3_ast = const_x; let mut interp_y: Z3_ast = const_y; - assert_eq!( - Z3_model_eval(ctx, model, const_x, true, &mut interp_x), - true - ); - assert_eq!( - Z3_model_eval(ctx, model, const_y, true, &mut interp_y), - true - ); + assert!(Z3_model_eval(ctx, model, const_x, true, &mut interp_x)); + assert!(Z3_model_eval(ctx, model, const_y, true, &mut interp_y)); let mut val_x: i32 = -5; let mut val_y: i32 = -5; - assert_eq!(Z3_get_numeral_int(ctx, interp_x, &mut val_x), true); - assert_eq!(Z3_get_numeral_int(ctx, interp_y, &mut val_y), true); + assert!(Z3_get_numeral_int(ctx, interp_x, &mut val_x)); + assert!(Z3_get_numeral_int(ctx, interp_y, &mut val_y)); assert_eq!(val_x, 0); assert_eq!(val_y, -1); diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index 26edaf4c..9a87ba50 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -181,8 +181,8 @@ fn test_floating_point_bits() { assert!(sig64 == Some(53)); assert!(exp128 == Some(15)); assert!(sig128 == Some(113)); - assert!(expi == None); - assert!(sigi == None); + assert!(expi.is_none()); + assert!(sigi.is_none()); } #[test] @@ -361,7 +361,7 @@ fn test_float_add() { let x = ast::Float::new_const_float32(&ctx, "x"); let x_plus_one = ast::Float::round_towards_zero(&ctx).add(&x, &ast::Float::from_f32(&ctx, 1.0)); - let y = ast::Float::from_f32(&ctx, 3.14); + let y = ast::Float::from_f32(&ctx, std::f32::consts::PI); solver.assert(&x_plus_one._eq(&y)); assert_eq!(solver.check(), SatResult::Sat); @@ -994,12 +994,12 @@ fn test_goal_is_inconsistent() { let false_bool = ast::Bool::from_bool(&ctx, false); let goal = Goal::new(&ctx, false, false, false); goal.assert(&false_bool); - assert_eq!(goal.is_inconsistent(), true); + assert!(goal.is_inconsistent()); let true_bool = ast::Bool::from_bool(&ctx, true); let goal = Goal::new(&ctx, false, false, false); goal.assert(&true_bool); - assert_eq!(goal.is_inconsistent(), false); + assert!(!goal.is_inconsistent()); } #[test] @@ -1010,14 +1010,14 @@ fn test_goal_is_sat() { let false_bool = ast::Bool::from_bool(&ctx, false); let goal = Goal::new(&ctx, false, false, false); goal.assert(&false_bool); - assert_eq!(goal.is_decided_sat(), false); - assert_eq!(goal.is_decided_unsat(), true); + assert!(!goal.is_decided_sat()); + assert!(goal.is_decided_unsat()); let true_bool = ast::Bool::from_bool(&ctx, true); let goal = Goal::new(&ctx, false, false, false); goal.assert(&true_bool); - assert_eq!(goal.is_decided_unsat(), false); - assert_eq!(goal.is_decided_sat(), true); + assert!(!goal.is_decided_unsat()); + assert!(goal.is_decided_sat()); } #[test] @@ -1255,10 +1255,10 @@ fn test_goal_apply_tactic() { after_formulas: Vec, ) { assert_eq!(goal.get_formulas::(), before_formulas); - let params = Params::new(&ctx); + let params = Params::new(ctx); - let tactic = Tactic::new(&ctx, "sat-preprocess"); - let repeat_tactic = Tactic::repeat(&ctx, &tactic, 100); + let tactic = Tactic::new(ctx, "sat-preprocess"); + let repeat_tactic = Tactic::repeat(ctx, &tactic, 100); let apply_results = repeat_tactic.apply(&goal, Some(¶ms)); let goal_results = apply_results .unwrap() @@ -1525,11 +1525,11 @@ fn test_ast_safe_decl() { let x_not = x.not(); assert_eq!(x_not.safe_decl().unwrap().kind(), DeclKind::NOT); - let f = FuncDecl::new(&ctx, "f", &[&Sort::int(&ctx)], &Sort::int(ctx)); - let x = ast::Int::new_const(&ctx, "x"); + let f = FuncDecl::new(ctx, "f", &[&Sort::int(ctx)], &Sort::int(ctx)); + let x = ast::Int::new_const(ctx, "x"); let f_x: ast::Int = f.apply(&[&x]).try_into().unwrap(); - let f_x_pattern: Pattern = Pattern::new(&ctx, &[&f_x]); - let forall = ast::forall_const(&ctx, &[&x], &[&f_x_pattern], &x._eq(&f_x)); + let f_x_pattern: Pattern = Pattern::new(ctx, &[&f_x]); + let forall = ast::forall_const(ctx, &[&x], &[&f_x_pattern], &x._eq(&f_x)); assert!(forall.safe_decl().is_err()); assert_eq!( format!("{}", forall.safe_decl().err().unwrap()), @@ -1542,16 +1542,22 @@ fn test_ast_safe_decl() { fn test_regex_capital_foobar_intersect_az_plus_is_unsat() { let cfg = Config::new(); let ctx = &Context::new(&cfg); - let solver = Solver::new(&ctx); + let solver = Solver::new(ctx); let s = ast::String::new_const(ctx, "s"); - let re = ast::Regexp::intersect(ctx, &[ - &ast::Regexp::concat(ctx, &[ - &ast::Regexp::literal(ctx, "FOO"), - &ast::Regexp::literal(ctx, "bar") - ]), - &ast::Regexp::plus(&ast::Regexp::range(ctx, &'a', &'z')) - ]); + let re = ast::Regexp::intersect( + ctx, + &[ + &ast::Regexp::concat( + ctx, + &[ + &ast::Regexp::literal(ctx, "FOO"), + &ast::Regexp::literal(ctx, "bar"), + ], + ), + &ast::Regexp::plus(&ast::Regexp::range(ctx, &'a', &'z')), + ], + ); solver.assert(&s.regex_matches(&re)); assert!(solver.check() == SatResult::Unsat); } diff --git a/z3/tests/objectives.rs b/z3/tests/objectives.rs index c6b59497..1ee40d59 100644 --- a/z3/tests/objectives.rs +++ b/z3/tests/objectives.rs @@ -152,11 +152,11 @@ fn test_optimize_assert_soft_and_get_objectives() { } assert_eq!( - *&ite_children[1].as_real().unwrap().as_real().unwrap(), + ite_children[1].as_real().unwrap().as_real().unwrap(), (0, 1) ); assert_eq!( - *&ite_children[2].as_real().unwrap().as_real().unwrap(), + ite_children[2].as_real().unwrap().as_real().unwrap(), (1, 1) ); } diff --git a/z3/tests/ops.rs b/z3/tests/ops.rs index 6d1e882c..770f3892 100644 --- a/z3/tests/ops.rs +++ b/z3/tests/ops.rs @@ -225,7 +225,7 @@ fn test_ast_children() { fn assert_ast_attributes<'c, T: Ast<'c>>(expr: &T, is_const: bool) { assert_eq!(expr.kind(), AstKind::App); - assert_eq!(expr.is_app(), true); + assert!(expr.is_app()); assert_eq!(expr.is_const(), is_const); } diff --git a/z3/tests/semver_tests.rs b/z3/tests/semver_tests.rs index af358f7d..6717e8e3 100644 --- a/z3/tests/semver_tests.rs +++ b/z3/tests/semver_tests.rs @@ -30,10 +30,7 @@ impl Spec { type SpecMap = HashMap>; fn get_version(sm: &SpecMap, pkg: &str, ver: usize) -> Option { - match sm.get(pkg) { - None => None, - Some(specs) => Some(specs[ver].vers.clone()), - } + sm.get(pkg).map(|specs| specs[ver].vers.clone()) } fn first_version_req_index(sm: &SpecMap, pkg: &str, req: &VersionReq) -> Option { @@ -191,7 +188,7 @@ fn test_solve_simple_semver_example() { )); // Ensure we have a constant for every pkg _or_ dep listed - for k in (&smap).keys() { + for k in (smap).keys() { asts.entry(k.clone()).or_insert_with(|| { info!("new AST for {}", k); ast::Int::fresh_const(&ctx, "pkg") @@ -199,7 +196,7 @@ fn test_solve_simple_semver_example() { } for specs in smap.values() { for spec in specs { - for r in (&spec).reqs.keys() { + for r in (spec).reqs.keys() { asts.entry(r.clone()).or_insert_with(|| { info!("new AST for {}", r); ast::Int::fresh_const(&ctx, "dep-pkg") @@ -223,10 +220,10 @@ fn test_solve_simple_semver_example() { "Asserting: {} == #{} {} => {} >= #{} {}", k, n, - get_version(&smap, k, n as usize).unwrap(), + get_version(&smap, k, n).unwrap(), r, low, - get_version(&smap, r, low as usize).unwrap() + get_version(&smap, r, low).unwrap() ); opt.assert( &k_ast @@ -242,10 +239,10 @@ fn test_solve_simple_semver_example() { "Asserting: {} == #{} {} => {} <= #{} {}", k, n, - get_version(&smap, k, n as usize).unwrap(), + get_version(&smap, k, n).unwrap(), r, high, - get_version(&smap, r, high as usize).unwrap() + get_version(&smap, r, high).unwrap() ); opt.assert( &k_ast