From 96c5055dd38db58ab9d73f3c2ab46cafcc331e8e Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 17:06:25 -0400 Subject: [PATCH 01/26] Added jq for json querying. --- scripts/setup/macos-10.15/install_deps.sh | 2 +- scripts/setup/ubuntu/install_deps.sh | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/setup/macos-10.15/install_deps.sh b/scripts/setup/macos-10.15/install_deps.sh index 0484b83e1db8..1d28ab4c0326 100755 --- a/scripts/setup/macos-10.15/install_deps.sh +++ b/scripts/setup/macos-10.15/install_deps.sh @@ -10,7 +10,7 @@ set -eux #brew update # Install dependencies via `brew` -brew install universal-ctags wget +brew install universal-ctags wget jq # Add Python package dependencies PYTHON_DEPS=( diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh index 7a6269aecdfa..f4efe642c414 100755 --- a/scripts/setup/ubuntu/install_deps.sh +++ b/scripts/setup/ubuntu/install_deps.sh @@ -26,6 +26,7 @@ DEPS=( wget zlib1g zlib1g-dev + jq ) # Version specific dependencies. From 0547a1d2ae7c8c6544dd6df0070ae7b9ee39d78c Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 19:02:45 -0400 Subject: [PATCH 02/26] Added clippy to regression. --- scripts/kani-regression.sh | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index f9c5a6b9f707..2464c7ed0a0b 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -25,6 +25,11 @@ check-cbmc-viewer-version.py --major 3 --minor 5 # Formatting check ${SCRIPT_DIR}/kani-fmt.sh --check +# Clippy: -A for permanently dismissed lints +cargo clippy --all -- \ + -A "clippy::expect_fun_call" \ + -A "clippy::or_fun_call" + # Parser tests PYTHONPATH=${SCRIPT_DIR} python3 -m unittest ${SCRIPT_DIR}/test_cbmc_json_parser.py From ba12b5590fe9246d97c5ab906807197d2a803f03 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 19:03:11 -0400 Subject: [PATCH 03/26] Added error ignore and todo to kani-compiler. --- kani-compiler/Cargo.toml | 1 + kani-compiler/src/main.rs | 11 +++++++++++ 2 files changed, 12 insertions(+) diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index b94b11a04c36..38414408a792 100644 --- a/kani-compiler/Cargo.toml +++ b/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 } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 6755d4473dcf..3550f818ace8 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -7,6 +7,17 @@ //! Like miri, clippy, and other tools developed on the top of rustc, we rely on the //! rustc_private feature and a specific version of rustc. #![deny(warnings)] + +// todo: fix clippy warnings +#![allow(clippy::expect_fun_call, clippy::explicit_auto_deref, +clippy::if_same_then_else, clippy::iter_nth_zero, +clippy::let_and_return, clippy::manual_map, clippy::map_entry, +clippy::match_like_matches_macro, clippy::module_inception, +clippy::needless_arbitrary_self_type, clippy::needless_bool, +clippy::needless_return, clippy::new_ret_no_self, +clippy::new_without_default, clippy::or_fun_call, +clippy::redundant_clone, clippy::type_complexity)] + #![feature(extern_types)] #![recursion_limit = "256"] #![feature(box_patterns)] From e7b194d033cdb0c1b20e17f51193ef0f58355d05 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 19:19:04 -0400 Subject: [PATCH 04/26] Added clippy todo to cprover_bindings. --- cprover_bindings/Cargo.toml | 1 + cprover_bindings/src/lib.rs | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 38bcf93ec6dc..c4df9573d7e9 100644 --- a/cprover_bindings/Cargo.toml +++ b/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 diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs index cd87dffd75a6..f5e96e30e72e 100644 --- a/cprover_bindings/src/lib.rs +++ b/cprover_bindings/src/lib.rs @@ -29,6 +29,11 @@ //! Speical [irep::Irep::id]s include: //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\]. +// todo: Resolve the following clippy warnings. +#![allow(clippy::needless_bool, clippy::let_and_return, +clippy::manual_map, clippy::module_inception, +clippy::new_without_default)] + mod env; pub mod goto_program; pub mod irep; From a731fa5d2ba0797f84468cdac82ea141cdd1e754 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 19:59:52 -0400 Subject: [PATCH 05/26] Forced failure on warnings (Werror for clippy). --- scripts/kani-regression.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 2464c7ed0a0b..68b1c6677c92 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -26,7 +26,7 @@ check-cbmc-viewer-version.py --major 3 --minor 5 ${SCRIPT_DIR}/kani-fmt.sh --check # Clippy: -A for permanently dismissed lints -cargo clippy --all -- \ +cargo clippy --all -- -D warnings \ -A "clippy::expect_fun_call" \ -A "clippy::or_fun_call" From 05b772869c96ae42ce8b3d21c2cde05deca038b9 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 20:08:07 -0400 Subject: [PATCH 06/26] Added clippy todo to compiletest. --- tools/compiletest/Cargo.toml | 1 + tools/compiletest/src/main.rs | 8 ++++++++ 2 files changed, 9 insertions(+) diff --git a/tools/compiletest/Cargo.toml b/tools/compiletest/Cargo.toml index 83427b1e8e96..c525d2ec2db0 100644 --- a/tools/compiletest/Cargo.toml +++ b/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: diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index f186f5251933..94b178c6a1eb 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -3,6 +3,14 @@ // Modifications Copyright Kani Contributors // See GitHub history for details. +// todo: Resolve the following clippy warnings. +#![allow(clippy::collapsible_else_if, +clippy::derive_partial_eq_without_eq, clippy::into_iter_on_ref, +clippy::iter_skip_next, clippy::manual_strip, clippy::needless_borrow, +clippy::needless_range_loop, clippy::new_without_default, +clippy::ptr_arg, clippy::single_char_pattern, +clippy::vec_init_then_push)] + #![crate_name = "compiletest"] // The `test` crate is the only unstable feature // allowed here, just to share similar code. From 476c88c6a144e1300a3c2155536ff84d24ca037c Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 20:28:10 -0400 Subject: [PATCH 07/26] Clippy supression for bookrunner. --- tools/bookrunner/Cargo.toml | 1 + tools/bookrunner/librustdoc/Cargo.toml | 2 ++ tools/bookrunner/librustdoc/lib.rs | 4 +++- tools/bookrunner/src/main.rs | 1 + 4 files changed, 7 insertions(+), 1 deletion(-) diff --git a/tools/bookrunner/Cargo.toml b/tools/bookrunner/Cargo.toml index bafbbea1ce65..f98b4ec72a83 100644 --- a/tools/bookrunner/Cargo.toml +++ b/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" diff --git a/tools/bookrunner/librustdoc/Cargo.toml b/tools/bookrunner/librustdoc/Cargo.toml index cc65a1e44727..f83c6e25803c 100644 --- a/tools/bookrunner/librustdoc/Cargo.toml +++ b/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: diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs index 0ae9af33782d..1f23cfea3094 100644 --- a/tools/bookrunner/librustdoc/lib.rs +++ b/tools/bookrunner/librustdoc/lib.rs @@ -20,7 +20,9 @@ #![feature(iter_intersperse)] #![recursion_limit = "256"] #![warn(rustc::internal)] -#![allow(clippy::collapsible_if, clippy::collapsible_else_if)] +#![allow(clippy::collapsible_if, +clippy::collapsible_else_if,clippy::derive_partial_eq_without_eq, +clippy::format_push_string)] #[macro_use] extern crate tracing; diff --git a/tools/bookrunner/src/main.rs b/tools/bookrunner/src/main.rs index 65fd9196b365..4e78989c12be 100644 --- a/tools/bookrunner/src/main.rs +++ b/tools/bookrunner/src/main.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(extend_one)] #![feature(rustc_private)] +#![allow(clippy::too_many_arguments,clippy::redundant_clone,clippy::len_zero)] mod bookrunner; mod books; From 0846e955d8f6fb2bf1e39e53050421f65fd5acf7 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 20:42:17 -0400 Subject: [PATCH 08/26] Resolved metadata warnings with publish = false. --- kani-compiler/kani_queries/Cargo.toml | 1 + kani-driver/Cargo.toml | 1 + kani_metadata/Cargo.toml | 1 + library/std/Cargo.toml | 1 + tools/make-kani-release/Cargo.toml | 1 + 5 files changed, 5 insertions(+) diff --git a/kani-compiler/kani_queries/Cargo.toml b/kani-compiler/kani_queries/Cargo.toml index 7910ae6548ef..e4fe9fa7c90d 100644 --- a/kani-compiler/kani_queries/Cargo.toml +++ b/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"} diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index d60ecb2d132f..58391cd5d31a 100644 --- a/kani-driver/Cargo.toml +++ b/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" } diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index dd79fe89571c..e121939ccb7c 100644 --- a/kani_metadata/Cargo.toml +++ b/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 diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 349b50000f3c..bf8edeaf6ffb 100644 --- a/library/std/Cargo.toml +++ b/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"} diff --git a/tools/make-kani-release/Cargo.toml b/tools/make-kani-release/Cargo.toml index b72d1fa654eb..7f3fb7ce8f24 100644 --- a/tools/make-kani-release/Cargo.toml +++ b/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" From dfb712ae37a5261a8cf327ba7b3aca767d5812fc Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 20:52:25 -0400 Subject: [PATCH 09/26] Clippy todo for kani library. --- library/kani/Cargo.toml | 1 + library/kani/src/lib.rs | 3 +++ 2 files changed, 4 insertions(+) diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index d679873278e6..8fd8d8175129 100644 --- a/library/kani/Cargo.toml +++ b/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" } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 25b983e5faba..db94b3f1c304 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -3,6 +3,9 @@ #![feature(rustc_attrs)] // Used for rustc_diagnostic_item. #![feature(min_specialization)] // Used for default implementation of Arbitrary. +// todo: resolve clippy warnings. +#![allow(clippy::manual_range_contains, clippy::missing_safety_doc)] + pub mod arbitrary; pub mod invariant; pub mod slice; From 5b0c1597254d82183dabf5a025a045eabfddf531 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 20:55:36 -0400 Subject: [PATCH 10/26] Clippy todos and publish fix for kani_macros. --- library/kani_macros/Cargo.toml | 1 + library/kani_macros/src/lib.rs | 3 +++ 2 files changed, 4 insertions(+) diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 9f4f7bd9065d..68cf3fbdfafe 100644 --- a/library/kani_macros/Cargo.toml +++ b/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 diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 43c709832a62..2699d135b321 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -8,6 +8,9 @@ // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" +// todo: resolve clippy warnings +#![allow(clippy::len_zero,clippy::redundant_clone)] + // proc_macro::quote is nightly-only, so we'll cobble things together instead use proc_macro::TokenStream; From 7f6d50c5f8dc63d145e7ff62a65e7e63b395bd62 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Fri, 22 Jul 2022 20:56:34 -0400 Subject: [PATCH 11/26] Cargo fmt. --- cprover_bindings/src/lib.rs | 10 +++++++--- kani-compiler/src/main.rs | 29 +++++++++++++++++++---------- library/kani_macros/src/lib.rs | 2 +- tools/bookrunner/librustdoc/lib.rs | 9 ++++++--- tools/bookrunner/src/main.rs | 2 +- tools/compiletest/src/main.rs | 20 +++++++++++++------- 6 files changed, 47 insertions(+), 25 deletions(-) diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs index f5e96e30e72e..7d472754e3fe 100644 --- a/cprover_bindings/src/lib.rs +++ b/cprover_bindings/src/lib.rs @@ -30,9 +30,13 @@ //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\]. // todo: Resolve the following clippy warnings. -#![allow(clippy::needless_bool, clippy::let_and_return, -clippy::manual_map, clippy::module_inception, -clippy::new_without_default)] +#![allow( + clippy::needless_bool, + clippy::let_and_return, + clippy::manual_map, + clippy::module_inception, + clippy::new_without_default +)] mod env; pub mod goto_program; diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 3550f818ace8..808e5afd239e 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -7,17 +7,26 @@ //! Like miri, clippy, and other tools developed on the top of rustc, we rely on the //! rustc_private feature and a specific version of rustc. #![deny(warnings)] - // todo: fix clippy warnings -#![allow(clippy::expect_fun_call, clippy::explicit_auto_deref, -clippy::if_same_then_else, clippy::iter_nth_zero, -clippy::let_and_return, clippy::manual_map, clippy::map_entry, -clippy::match_like_matches_macro, clippy::module_inception, -clippy::needless_arbitrary_self_type, clippy::needless_bool, -clippy::needless_return, clippy::new_ret_no_self, -clippy::new_without_default, clippy::or_fun_call, -clippy::redundant_clone, clippy::type_complexity)] - +#![allow( + clippy::expect_fun_call, + clippy::explicit_auto_deref, + clippy::if_same_then_else, + clippy::iter_nth_zero, + clippy::let_and_return, + clippy::manual_map, + clippy::map_entry, + clippy::match_like_matches_macro, + clippy::module_inception, + clippy::needless_arbitrary_self_type, + clippy::needless_bool, + clippy::needless_return, + clippy::new_ret_no_self, + clippy::new_without_default, + clippy::or_fun_call, + clippy::redundant_clone, + clippy::type_complexity +)] #![feature(extern_types)] #![recursion_limit = "256"] #![feature(box_patterns)] diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 2699d135b321..4238f7d3f508 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -9,7 +9,7 @@ // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" // todo: resolve clippy warnings -#![allow(clippy::len_zero,clippy::redundant_clone)] +#![allow(clippy::len_zero, clippy::redundant_clone)] // proc_macro::quote is nightly-only, so we'll cobble things together instead use proc_macro::TokenStream; diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs index 1f23cfea3094..351066925a31 100644 --- a/tools/bookrunner/librustdoc/lib.rs +++ b/tools/bookrunner/librustdoc/lib.rs @@ -20,9 +20,12 @@ #![feature(iter_intersperse)] #![recursion_limit = "256"] #![warn(rustc::internal)] -#![allow(clippy::collapsible_if, -clippy::collapsible_else_if,clippy::derive_partial_eq_without_eq, -clippy::format_push_string)] +#![allow( + clippy::collapsible_if, + clippy::collapsible_else_if, + clippy::derive_partial_eq_without_eq, + clippy::format_push_string +)] #[macro_use] extern crate tracing; diff --git a/tools/bookrunner/src/main.rs b/tools/bookrunner/src/main.rs index 4e78989c12be..8f4b7ed2cc13 100644 --- a/tools/bookrunner/src/main.rs +++ b/tools/bookrunner/src/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(extend_one)] #![feature(rustc_private)] -#![allow(clippy::too_many_arguments,clippy::redundant_clone,clippy::len_zero)] +#![allow(clippy::too_many_arguments, clippy::redundant_clone, clippy::len_zero)] mod bookrunner; mod books; diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 94b178c6a1eb..2e3ddc02a287 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -4,13 +4,19 @@ // See GitHub history for details. // todo: Resolve the following clippy warnings. -#![allow(clippy::collapsible_else_if, -clippy::derive_partial_eq_without_eq, clippy::into_iter_on_ref, -clippy::iter_skip_next, clippy::manual_strip, clippy::needless_borrow, -clippy::needless_range_loop, clippy::new_without_default, -clippy::ptr_arg, clippy::single_char_pattern, -clippy::vec_init_then_push)] - +#![allow( + clippy::collapsible_else_if, + clippy::derive_partial_eq_without_eq, + clippy::into_iter_on_ref, + clippy::iter_skip_next, + clippy::manual_strip, + clippy::needless_borrow, + clippy::needless_range_loop, + clippy::new_without_default, + clippy::ptr_arg, + clippy::single_char_pattern, + clippy::vec_init_then_push +)] #![crate_name = "compiletest"] // The `test` crate is the only unstable feature // allowed here, just to share similar code. From 18328666170364adbec1f2a19fc2b17c64b9d2bf Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 12:12:34 -0400 Subject: [PATCH 12/26] Temporally turned off clippy fail. --- kani-driver/src/main.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index a264d98ca588..2cfbb714884e 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -1,6 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// todo: resolve clippy warning. +#![allow(clippy::unnecessary_lazy_evaluations)] + use anyhow::Result; use args_toml::join_args; use call_cbmc::VerificationStatus; From df626cf87fa4235f2e78d25710ebec6b77b7873e Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 12:18:40 -0400 Subject: [PATCH 13/26] Moved clippy to format checks. --- .github/workflows/format-check.yml | 10 ++++++++++ scripts/kani-regression.sh | 5 ----- 2 files changed, 10 insertions(+), 5 deletions(-) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 29f1ed612089..479075af6504 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -20,3 +20,13 @@ jobs: run: | pip3 install --upgrade autopep8 ./scripts/run-autopep8.sh + + clippy: + runs-on: ubuntu-latest + steps: + - name: "Run Clippy" + run: | + cargo clippy --all -- -D warnings \ + -A "clippy::expect_fun_call" \ + -A "clippy::or_fun_call" + diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 68b1c6677c92..f9c5a6b9f707 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -25,11 +25,6 @@ check-cbmc-viewer-version.py --major 3 --minor 5 # Formatting check ${SCRIPT_DIR}/kani-fmt.sh --check -# Clippy: -A for permanently dismissed lints -cargo clippy --all -- -D warnings \ - -A "clippy::expect_fun_call" \ - -A "clippy::or_fun_call" - # Parser tests PYTHONPATH=${SCRIPT_DIR} python3 -m unittest ${SCRIPT_DIR}/test_cbmc_json_parser.py From f89f24b7ca34b1922d93379f54210c647d625dba Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 12:31:02 -0400 Subject: [PATCH 14/26] Moved clippy to the format check. --- .github/workflows/format-check.yml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 479075af6504..de1e3fdd06a3 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -21,9 +21,6 @@ jobs: pip3 install --upgrade autopep8 ./scripts/run-autopep8.sh - clippy: - runs-on: ubuntu-latest - steps: - name: "Run Clippy" run: | cargo clippy --all -- -D warnings \ From 9fd55728de89bb04f4da8bf8438f6e852c4257b9 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 12:42:21 -0400 Subject: [PATCH 15/26] Added missing dependency. --- .github/workflows/format-check.yml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index de1e3fdd06a3..d71987229b61 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -21,9 +21,19 @@ jobs: pip3 install --upgrade autopep8 ./scripts/run-autopep8.sh + format-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: "Run Clippy" run: | cargo clippy --all -- -D warnings \ -A "clippy::expect_fun_call" \ -A "clippy::or_fun_call" - From 5c0a9188161f089f941169683256407765806ab9 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 13:36:24 -0400 Subject: [PATCH 16/26] Fixed yaml overwrite problem. --- .github/workflows/format-check.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index d71987229b61..de96089f813b 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -21,7 +21,7 @@ jobs: pip3 install --upgrade autopep8 ./scripts/run-autopep8.sh - format-check: + clippy-check: runs-on: ubuntu-20.04 steps: - name: Checkout Kani From 37cd8030b4492a07630401e74e0ffdf70eb21abd Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 14:51:08 -0400 Subject: [PATCH 17/26] Gather stats on clippy warnings. --- .github/workflows/format-check.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index de96089f813b..73bff8ff77ce 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -37,3 +37,9 @@ jobs: cargo clippy --all -- -D warnings \ -A "clippy::expect_fun_call" \ -A "clippy::or_fun_call" + + - name: "Print Clippy Statistics" + run: | + (cargo clippy --all --message-format=json 2>/dev/null | \ + jq 'select(.message!=null) | .message.code.code' | grep -v '^null$' | \ + sort | uniq -c) || true From 7803971d1f646310f146c3658f284a552feb9af5 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 15:03:06 -0400 Subject: [PATCH 18/26] jq install for osx not needed. --- scripts/setup/macos-10.15/install_deps.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/setup/macos-10.15/install_deps.sh b/scripts/setup/macos-10.15/install_deps.sh index 1d28ab4c0326..0484b83e1db8 100755 --- a/scripts/setup/macos-10.15/install_deps.sh +++ b/scripts/setup/macos-10.15/install_deps.sh @@ -10,7 +10,7 @@ set -eux #brew update # Install dependencies via `brew` -brew install universal-ctags wget jq +brew install universal-ctags wget # Add Python package dependencies PYTHON_DEPS=( From f3d9252bc2d231a7777fd4a6c47bb9435a38358f Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 15:58:57 -0400 Subject: [PATCH 19/26] Moved clippy control to a central config file. --- .cargo/config.toml | 36 ++++++++++++++++++++++++++++++ .gitignore | 1 + cprover_bindings/src/lib.rs | 9 -------- kani-compiler/src/main.rs | 20 ----------------- kani-driver/src/main.rs | 3 --- tools/bookrunner/librustdoc/lib.rs | 7 +----- tools/bookrunner/src/main.rs | 1 - tools/compiletest/src/main.rs | 14 ------------ 8 files changed, 38 insertions(+), 53 deletions(-) create mode 100644 .cargo/config.toml diff --git a/.cargo/config.toml b/.cargo/config.toml new file mode 100644 index 000000000000..f352a0926f17 --- /dev/null +++ b/.cargo/config.toml @@ -0,0 +1,36 @@ +# 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::expect_fun_call", + "-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::or_fun_call", + "-Aclippy::redundant_clone", + "-Aclippy::too_many_arguments", + "-Aclippy::type_complexity", + "-Aclippy::unnecessary_lazy_evaluations", +] \ No newline at end of file diff --git a/.gitignore b/.gitignore index 714cb05350d7..5c44a553fb9a 100644 --- a/.gitignore +++ b/.gitignore @@ -25,6 +25,7 @@ Session.vim ## Tool .valgrindrc .cargo +!/.cargo # Included because it is part of the test case !/test/run-make/thumb-none-qemu/example/.cargo diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs index 7d472754e3fe..cd87dffd75a6 100644 --- a/cprover_bindings/src/lib.rs +++ b/cprover_bindings/src/lib.rs @@ -29,15 +29,6 @@ //! Speical [irep::Irep::id]s include: //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\]. -// todo: Resolve the following clippy warnings. -#![allow( - clippy::needless_bool, - clippy::let_and_return, - clippy::manual_map, - clippy::module_inception, - clippy::new_without_default -)] - mod env; pub mod goto_program; pub mod irep; diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 808e5afd239e..6755d4473dcf 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -7,26 +7,6 @@ //! Like miri, clippy, and other tools developed on the top of rustc, we rely on the //! rustc_private feature and a specific version of rustc. #![deny(warnings)] -// todo: fix clippy warnings -#![allow( - clippy::expect_fun_call, - clippy::explicit_auto_deref, - clippy::if_same_then_else, - clippy::iter_nth_zero, - clippy::let_and_return, - clippy::manual_map, - clippy::map_entry, - clippy::match_like_matches_macro, - clippy::module_inception, - clippy::needless_arbitrary_self_type, - clippy::needless_bool, - clippy::needless_return, - clippy::new_ret_no_self, - clippy::new_without_default, - clippy::or_fun_call, - clippy::redundant_clone, - clippy::type_complexity -)] #![feature(extern_types)] #![recursion_limit = "256"] #![feature(box_patterns)] diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 2cfbb714884e..a264d98ca588 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// todo: resolve clippy warning. -#![allow(clippy::unnecessary_lazy_evaluations)] - use anyhow::Result; use args_toml::join_args; use call_cbmc::VerificationStatus; diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs index 351066925a31..0ae9af33782d 100644 --- a/tools/bookrunner/librustdoc/lib.rs +++ b/tools/bookrunner/librustdoc/lib.rs @@ -20,12 +20,7 @@ #![feature(iter_intersperse)] #![recursion_limit = "256"] #![warn(rustc::internal)] -#![allow( - clippy::collapsible_if, - clippy::collapsible_else_if, - clippy::derive_partial_eq_without_eq, - clippy::format_push_string -)] +#![allow(clippy::collapsible_if, clippy::collapsible_else_if)] #[macro_use] extern crate tracing; diff --git a/tools/bookrunner/src/main.rs b/tools/bookrunner/src/main.rs index 8f4b7ed2cc13..65fd9196b365 100644 --- a/tools/bookrunner/src/main.rs +++ b/tools/bookrunner/src/main.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(extend_one)] #![feature(rustc_private)] -#![allow(clippy::too_many_arguments, clippy::redundant_clone, clippy::len_zero)] mod bookrunner; mod books; diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 58efa75f1838..a87440021250 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -3,20 +3,6 @@ // Modifications Copyright Kani Contributors // See GitHub history for details. -// todo: Resolve the following clippy warnings. -#![allow( - clippy::collapsible_else_if, - clippy::derive_partial_eq_without_eq, - clippy::into_iter_on_ref, - clippy::iter_skip_next, - clippy::manual_strip, - clippy::needless_borrow, - clippy::needless_range_loop, - clippy::new_without_default, - clippy::ptr_arg, - clippy::single_char_pattern, - clippy::vec_init_then_push -)] #![crate_name = "compiletest"] // The `test` crate is the only unstable feature // allowed here, just to share similar code. From 2985448e94db5cfcf4ec59f97749e7e500018ff4 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 16:25:17 -0400 Subject: [PATCH 20/26] Fixed clippy warnings under library/ --- library/kani/src/invariant.rs | 2 +- library/kani/src/lib.rs | 3 --- library/kani/src/slice.rs | 4 ++++ library/kani_macros/src/lib.rs | 7 ++----- 4 files changed, 7 insertions(+), 9 deletions(-) diff --git a/library/kani/src/invariant.rs b/library/kani/src/invariant.rs index dbbcc87d474a..222ba5a60e29 100644 --- a/library/kani/src/invariant.rs +++ b/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) } } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index db94b3f1c304..25b983e5faba 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -3,9 +3,6 @@ #![feature(rustc_attrs)] // Used for rustc_diagnostic_item. #![feature(min_specialization)] // Used for default implementation of Arbitrary. -// todo: resolve clippy warnings. -#![allow(clippy::manual_range_contains, clippy::missing_safety_doc)] - pub mod arbitrary; pub mod invariant; pub mod slice; diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs index a1b50b838ff8..618bb0ad9688 100644 --- a/library/kani/src/slice.rs +++ b/library/kani/src/slice.rs @@ -149,6 +149,10 @@ where AnySlice::::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() -> AnySlice { AnySlice::::new_raw() } diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 4238f7d3f508..97888cdbfdf2 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -8,9 +8,6 @@ // So we have to enable this on the commandline (see kani-rustc) with: // RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)" -// todo: resolve clippy warnings -#![allow(clippy::len_zero, clippy::redundant_clone)] - // proc_macro::quote is nightly-only, so we'll cobble things together instead use proc_macro::TokenStream; @@ -42,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::().unwrap()); // no_mangle is a temporary hack to make the function "public" so it gets codegen'd result.extend("#[no_mangle]".parse::().unwrap()); @@ -70,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::().unwrap()); result.extend(item); From 27557a0449ed2a1d180b595c3ecaef253b641c11 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 16:27:46 -0400 Subject: [PATCH 21/26] Adjusted actions to print stats by removing lint supression. --- .github/workflows/format-check.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 73bff8ff77ce..5629c822a973 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -40,6 +40,7 @@ jobs: - 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 From 6ed08666e3ddc44eedc252cded85779c067f8dbd Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 16:34:29 -0400 Subject: [PATCH 22/26] Ignored 3 clippy warnings that regressed after merge. --- .cargo/config.toml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.cargo/config.toml b/.cargo/config.toml index f352a0926f17..672da74590ae 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -33,4 +33,7 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -. "-Aclippy::too_many_arguments", "-Aclippy::type_complexity", "-Aclippy::unnecessary_lazy_evaluations", + "-Aclippy::useless_conversion", + "-Aclippy::needless_borrow", + "-Aclippy::unnecessary_filter_map", ] \ No newline at end of file From cf7a0ffe1407433a192c0d4f6dd7f426290ecf3f Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Mon, 25 Jul 2022 16:36:38 -0400 Subject: [PATCH 23/26] Forgot to remove manual -A --- .github/workflows/format-check.yml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 5629c822a973..beaeb5bbf6dd 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -34,9 +34,7 @@ jobs: - name: "Run Clippy" run: | - cargo clippy --all -- -D warnings \ - -A "clippy::expect_fun_call" \ - -A "clippy::or_fun_call" + cargo clippy --all -- -D warnings - name: "Print Clippy Statistics" run: | From 88a98da5fd200043b8bc0090b61c8d028db99ddf Mon Sep 17 00:00:00 2001 From: Yoshiki Takashima Date: Mon, 25 Jul 2022 21:06:19 -0400 Subject: [PATCH 24/26] got rid of redundant allowed lints. --- .cargo/config.toml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/.cargo/config.toml b/.cargo/config.toml index 672da74590ae..7b4add9ae883 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -11,7 +11,6 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -. # todo address the following lints. "-Aclippy::cargo_common_metadata", "-Aclippy::derive_partial_eq_without_eq", - "-Aclippy::expect_fun_call", "-Aclippy::explicit_auto_deref", "-Aclippy::if_same_then_else", "-Aclippy::iter_nth_zero", @@ -28,7 +27,6 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -. "-Aclippy::needless_return", "-Aclippy::new_ret_no_self", "-Aclippy::new_without_default", - "-Aclippy::or_fun_call", "-Aclippy::redundant_clone", "-Aclippy::too_many_arguments", "-Aclippy::type_complexity", @@ -36,4 +34,4 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -. "-Aclippy::useless_conversion", "-Aclippy::needless_borrow", "-Aclippy::unnecessary_filter_map", -] \ No newline at end of file +] From 455c42f492c79745e94ceaed92acf8cc0d27ed14 Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Tue, 26 Jul 2022 14:13:24 -0400 Subject: [PATCH 25/26] Moved jq install to workflow side. --- .github/workflows/format-check.yml | 4 ++++ scripts/setup/ubuntu/install_deps.sh | 1 - 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index beaeb5bbf6dd..e3f0d9ff5515 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -32,6 +32,10 @@ jobs: 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 diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh index f4efe642c414..7a6269aecdfa 100755 --- a/scripts/setup/ubuntu/install_deps.sh +++ b/scripts/setup/ubuntu/install_deps.sh @@ -26,7 +26,6 @@ DEPS=( wget zlib1g zlib1g-dev - jq ) # Version specific dependencies. From 806c3db9fcd17dd651f187051cfc84bd2f2a00da Mon Sep 17 00:00:00 2001 From: Yoshi Takashima Date: Tue, 26 Jul 2022 14:25:46 -0400 Subject: [PATCH 26/26] removed .cargo from gitignore --- .gitignore | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.gitignore b/.gitignore index 5c44a553fb9a..f53d5beacf76 100644 --- a/.gitignore +++ b/.gitignore @@ -24,10 +24,6 @@ Session.vim ## Tool .valgrindrc -.cargo -!/.cargo -# Included because it is part of the test case -!/test/run-make/thumb-none-qemu/example/.cargo ## Configuration /config.toml