Fix all remaining clippy lints (model-checking#1466)

Author: fzaiser

.cargo/config.toml

@@ -7,16 +7,5 @@ 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::derive_partial_eq_without_eq",
-    "-Aclippy::manual_map",
-    "-Aclippy::manual_range_contains",
-    "-Aclippy::map_entry",
-    "-Aclippy::missing_safety_doc",
-    "-Aclippy::module_inception",
-    "-Aclippy::new_ret_no_self",
     "-Aclippy::new_without_default",
-    "-Aclippy::too_many_arguments",
-    "-Aclippy::type_complexity",
 ]

cprover_bindings/src/goto_program/typ.rs

@@ -781,11 +781,8 @@ impl Type {
         &self,
         st: &'a SymbolTable,
     ) -> Option<Vec<&'a DatatypeComponent>> {
-        if let Some(components) = self.lookup_components(st) {
-            Some(components.iter().filter(|x| x.sizeof_in_bits(st) != 0).collect())
-        } else {
-            None
-        }
+        self.lookup_components(st)
+            .map(|components| components.iter().filter(|x| x.sizeof_in_bits(st) != 0).collect())
     }
 
     /// Calculates an under-approximation of whether two types are structurally equivalent.

cprover_bindings/src/irep/mod.rs

@@ -14,6 +14,7 @@
 //! TODO: Parser for json symbol tables into the internal irep format
 //! TODO: Investigate memory usage, and consider using sharing to reduce memory usage
 
+#[allow(clippy::module_inception)]
 mod irep;
 mod irep_id;
 pub mod serialize;

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -713,10 +713,10 @@ impl<'tcx> GotocCtx<'tcx> {
         let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty);
         let goto_typ = self.codegen_ty_inner(normalized);
         if let Some(tag) = goto_typ.tag() {
-            if !self.type_map.contains_key(&tag) {
+            self.type_map.entry(tag).or_insert_with(|| {
                 debug!(mir_type=?normalized, gotoc_name=?tag, ?goto_typ,  "codegen_ty: new type");
-                self.type_map.insert(tag, normalized);
-            }
+                normalized
+            });
         }
         goto_typ
     }

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -37,8 +37,8 @@ pub struct GotocCodegenBackend {
 }
 
 impl GotocCodegenBackend {
-    pub fn new(queries: &Rc<QueryDb>) -> Box<dyn CodegenBackend> {
-        Box::new(GotocCodegenBackend { queries: Rc::clone(queries) })
+    pub fn new(queries: &Rc<QueryDb>) -> Self {
+        GotocCodegenBackend { queries: Rc::clone(queries) }
     }
 }
 

kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs

@@ -24,7 +24,8 @@ pub fn init() {
     LazyLock::force(&DEFAULT_HOOK); // Install ice hook
 }
 
-// Custom panic hook to add more information when panic occurs during goto-c codegen.
+/// Custom panic hook to add more information when panic occurs during goto-c codegen.
+#[allow(clippy::type_complexity)]
 static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
     LazyLock::new(|| {
         let hook = panic::take_hook();

kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs

@@ -5,6 +5,7 @@
 
 mod debug;
 mod names;
+#[allow(clippy::module_inception)]
 mod utils;
 
 // TODO clean this up

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -57,10 +57,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // Save this occurrence so we can emit a warning in the compilation report.
         debug!("codegen_unimplemented: {} at {}", operation_name, loc.short_string());
         let key: InternedString = operation_name.into();
-        if !self.unsupported_constructs.contains_key(&key) {
-            self.unsupported_constructs.insert(key, Vec::new());
-        }
-        self.unsupported_constructs.get_mut(&key).unwrap().push(loc);
+        self.unsupported_constructs.entry(key).or_insert_with(Vec::new).push(loc);
 
         let body = vec![
             // Assert false to alert the user that there is a path that uses an unimplemented feature.

kani-compiler/src/main.rs

@@ -100,7 +100,7 @@ fn main() -> Result<(), &'static str> {
     if matches.is_present("goto-c") {
         if cfg!(feature = "cprover") {
             compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| {
-                codegen_cprover_gotoc::GotocCodegenBackend::new(&Rc::new(queries))
+                Box::new(codegen_cprover_gotoc::GotocCodegenBackend::new(&Rc::new(queries)))
             })));
         } else {
             return Err("Kani was configured without 'cprover' feature. You must enable this \

kani-compiler/src/session.rs

@@ -19,6 +19,7 @@ const BUG_REPORT_URL: &str =
     "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md";
 
 // Custom panic hook.
+#[allow(clippy::type_complexity)]
 static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
     LazyLock::new(|| {
         let hook = panic::take_hook();