Clippy in Regressions. (#1403)

* Added jq for json querying.

* Added clippy to regression.

* Added error ignore and todo to kani-compiler.

* Added clippy todo to cprover_bindings.

* Forced failure on warnings (Werror for clippy).

* Added clippy todo to compiletest.

* Clippy supression for bookrunner.

* Resolved metadata warnings with publish = false.

* Clippy todo for kani library.

* Clippy todos and publish fix for kani_macros.

* Cargo fmt.

* Temporally turned off clippy fail.

* Moved clippy to format checks.

* Moved clippy to the format check.

* Added missing dependency.

* Fixed yaml overwrite problem.

* Gather stats on clippy warnings.

* jq install for osx not needed.

* Moved clippy control to a central config file.

* Fixed clippy warnings under library/

* Adjusted actions to print stats by removing lint supression.

* Ignored 3 clippy warnings that regressed after merge.

* Forgot to remove manual -A

* got rid of redundant allowed lints.

* Moved jq install to workflow side.

* removed .cargo from gitignore

.cargo/config.toml

@@ -0,0 +1,37 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[target.'cfg(all())']
+rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
+
+    # Purposefully disabled lints
+    "-Aclippy::expect_fun_call",
+    "-Aclippy::or_fun_call",
+
+    # todo address the following lints.
+    "-Aclippy::cargo_common_metadata",
+    "-Aclippy::derive_partial_eq_without_eq",
+    "-Aclippy::explicit_auto_deref",
+    "-Aclippy::if_same_then_else",
+    "-Aclippy::iter_nth_zero",
+    "-Aclippy::let_and_return",
+    "-Aclippy::manual_map",
+    "-Aclippy::manual_range_contains",
+    "-Aclippy::manual_strip",
+    "-Aclippy::map_entry",
+    "-Aclippy::match_like_matches_macro",
+    "-Aclippy::missing_safety_doc",
+    "-Aclippy::module_inception",
+    "-Aclippy::needless_arbitrary_self_type",
+    "-Aclippy::needless_bool",
+    "-Aclippy::needless_return",
+    "-Aclippy::new_ret_no_self",
+    "-Aclippy::new_without_default",
+    "-Aclippy::redundant_clone",
+    "-Aclippy::too_many_arguments",
+    "-Aclippy::type_complexity",
+    "-Aclippy::unnecessary_lazy_evaluations",
+    "-Aclippy::useless_conversion",
+    "-Aclippy::needless_borrow",
+    "-Aclippy::unnecessary_filter_map",
+]

.github/workflows/format-check.yml

@@ -20,3 +20,29 @@ jobs:
         run: |
             pip3 install --upgrade autopep8
             ./scripts/run-autopep8.sh
+
+  clippy-check:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v2
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+            os: ubuntu-20.04
+
+      - name: "Install jq for parsing."
+        run: |
+          sudo apt-get install -y jq
+
+      - name: "Run Clippy"
+        run: |
+          cargo clippy --all -- -D warnings
+
+      - name: "Print Clippy Statistics"
+        run: |
+          rm .cargo/config.toml
+          (cargo clippy --all --message-format=json 2>/dev/null  | \
+          jq 'select(.message!=null) | .message.code.code' | grep -v '^null$' | \
+          sort | uniq -c) || true

.gitignore

@@ -24,9 +24,6 @@ Session.vim
 
 ## Tool
 .valgrindrc
-.cargo
-# Included because it is part of the test case
-!/test/run-make/thumb-none-qemu/example/.cargo
 
 ## Configuration
 /config.toml

cprover_bindings/Cargo.toml

@@ -6,6 +6,7 @@ name = "cprover_bindings"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [lib]
 test = true

kani-compiler/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani-compiler"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 ar = { version = "0.9.0", optional = true }

kani-compiler/kani_queries/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani_queries"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 tracing = {version = "0.1"}

kani-driver/Cargo.toml

@@ -9,6 +9,7 @@ description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
 homepage = "https://github.com/model-checking/kani"
 repository = "https://github.com/model-checking/kani"
+publish = false
 
 [dependencies]
 kani_metadata = { path = "../kani_metadata" }

kani_metadata/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani_metadata"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 

library/kani/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 kani_macros = { path = "../kani_macros" }

library/kani/src/invariant.rs

@@ -67,7 +67,7 @@ unsafe impl Invariant for char {
     fn is_valid(&self) -> bool {
         // Kani translates char into i32.
         let val = *self as i32;
-        val <= 0xD7FF || (val >= 0xE000 && val <= 0x10FFFF)
+        val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val)
     }
 }
 

library/kani/src/slice.rs

@@ -149,6 +149,10 @@ where
     AnySlice::<T, MAX_SLICE_LENGTH>::new()
 }
 
+/// # Safety
+///
+/// TODO: Safety of any_raw_slice is a complex matter. See
+/// https://github.com/model-checking/kani/issues/1394
 pub unsafe fn any_raw_slice<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH> {
     AnySlice::<T, MAX_SLICE_LENGTH>::new_raw()
 }

library/kani_macros/Cargo.toml

@@ -6,6 +6,7 @@ name = "kani_macros"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [lib]
 proc-macro = true

library/kani_macros/src/lib.rs

@@ -39,7 +39,7 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
 pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
     let mut result = TokenStream::new();
 
-    assert!(attr.to_string().len() == 0, "#[kani::proof] does not take any arguments");
+    assert!(attr.to_string().is_empty(), "#[kani::proof] does not take any arguments");
     result.extend("#[kanitool::proof]".parse::<TokenStream>().unwrap());
     // no_mangle is a temporary hack to make the function "public" so it gets codegen'd
     result.extend("#[no_mangle]".parse::<TokenStream>().unwrap());
@@ -67,7 +67,7 @@ pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
     let mut result = TokenStream::new();
 
     // Translate #[kani::unwind(arg)] to #[kanitool::unwind(arg)]
-    let insert_string = "#[kanitool::unwind(".to_owned() + &attr.clone().to_string() + ")]";
+    let insert_string = "#[kanitool::unwind(".to_owned() + &attr.to_string() + ")]";
     result.extend(insert_string.parse::<TokenStream>().unwrap());
 
     result.extend(item);

library/std/Cargo.toml

@@ -8,6 +8,7 @@ name = "std"
 version = "0.6.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 kani = {path="../kani"}

tools/bookrunner/Cargo.toml

@@ -6,6 +6,7 @@ name = "bookrunner"
 version = "0.1.0"
 edition = "2018"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 Inflector = "0.11.4"

tools/bookrunner/librustdoc/Cargo.toml

@@ -7,6 +7,8 @@ name = "rustdoc"
 version = "0.0.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
+
 # From upstream librustdoc:
 # https://github.com/rust-lang/rust/tree/master/src/librustdoc
 # Upstream crate does not list license but Rust statues:

tools/compiletest/Cargo.toml

@@ -8,6 +8,7 @@ name = "compiletest"
 version = "0.0.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
+publish = false
 # From upstream compiletest:
 # https://github.com/rust-lang/rust/tree/master/src/tools/compiletest
 # Upstream crate does not list license but Rust statues:

tools/make-kani-release/Cargo.toml

@@ -7,6 +7,7 @@ version = "0.1.0"
 edition = "2021"
 description = "Contructs a Kani release bundle"
 license = "MIT OR Apache-2.0"
+publish = false
 
 [dependencies]
 anyhow = "1"