Move clippy into CI

.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

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())

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);
 

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<Bool>,
     ) {
         assert_eq!(goal.get_formulas::<Bool>(), 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(&params));
         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);
 }

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)
         );
     }

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);
 }
 

z3/tests/semver_tests.rs

@@ -30,10 +30,7 @@ impl Spec {
 type SpecMap = HashMap<String, Vec<Spec>>;
 
 fn get_version(sm: &SpecMap, pkg: &str, ver: usize) -> Option<Version> {
-    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<usize> {
@@ -191,15 +188,15 @@ 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")
         });
     }
     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