CI Formatting Fixes (model-checking#4028)

The majority of the changes in this PR were made automatically by
running the command specified in
5314a5d, so the actual diff to review
is much smaller than it initially appears.

1. If `--check` was provided to`kani-fmt.sh`, it would run `cargo fmt
--check` but not `rustfmt --check`. This meant that our regression would
catch formatting errors from `cargo fmt` but not `rustfmt` (it would
just format the problematic files, which isn't useful in CI--we want it
to fail instead). So add the `--check` flag to the `rustfmt` calls as
well.
2. Run clippy with `kani_sysroot` feature enabled as well to catch more
formatting errors.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

.github/workflows/format-check.yml

@@ -48,6 +48,7 @@ jobs:
       - name: 'Run Clippy'
         run: |
           cargo clippy --workspace -- -D warnings
+          RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings
 
       - name: 'Print Clippy Statistics'
         run: |

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -275,7 +275,7 @@ impl IrepNumbering {
             return self.inv_cache.index[*number];
         }
         // This is where the key gets its unique number assigned.
-        let number = self.inv_cache.add_key(&key);
+        let number = self.inv_cache.add_key(key);
         self.cache.insert(key.clone(), number);
         self.inv_cache.index[number]
     }
@@ -449,17 +449,17 @@ where
         self.write_usize_varenc(num);
 
         if self.is_first_write_irep(num) {
-            let id = &self.numbering.id(&irep);
+            let id = &self.numbering.id(irep);
             self.write_numbered_string_ref(id);
 
-            for sub_idx in 0..(self.numbering.nof_sub(&irep)) {
+            for sub_idx in 0..(self.numbering.nof_sub(irep)) {
                 self.write_u8(b'S');
-                self.write_numbered_irep_ref(&self.numbering.sub(&irep, sub_idx));
+                self.write_numbered_irep_ref(&self.numbering.sub(irep, sub_idx));
             }
 
-            for named_sub_idx in 0..(self.numbering.nof_named_sub(&irep)) {
+            for named_sub_idx in 0..(self.numbering.nof_named_sub(irep)) {
                 self.write_u8(b'N');
-                let (k, v) = self.numbering.named_sub(&irep, named_sub_idx);
+                let (k, v) = self.numbering.named_sub(irep, named_sub_idx);
                 self.write_numbered_string_ref(&k);
                 self.write_numbered_irep_ref(&v);
             }
@@ -1339,7 +1339,7 @@ mod tests {
             let mut writer = BufWriter::new(&mut vec);
             let mut serializer = GotoBinarySerializer::new(&mut writer);
             for string in strings.iter() {
-                serializer.write_string_ref(&string);
+                serializer.write_string_ref(string);
             }
             println!("Serializer stats {:?}", serializer.get_stats());
         }
@@ -1365,12 +1365,12 @@ mod tests {
             let mut serializer = GotoBinarySerializer::new(&mut writer);
 
             // Number an irep
-            let num1 = serializer.numbering.number_irep(&irep1);
+            let num1 = serializer.numbering.number_irep(irep1);
 
             // Number an structurally different irep
             let identifiers2 = vec!["foo", "bar", "baz", "different", "zab", "rab", "oof"];
             let irep2 = &fold_with_op(&identifiers2, IrepId::And);
-            let num2 = serializer.numbering.number_irep(&irep2);
+            let num2 = serializer.numbering.number_irep(irep2);
 
             // Check that they have the different numbers.
             assert_ne!(num1, num2);

cprover_bindings/src/irep/symbol_table.rs

@@ -12,6 +12,12 @@ pub struct SymbolTable {
 }
 
 /// Constructors
+impl Default for SymbolTable {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
 impl SymbolTable {
     pub fn new() -> SymbolTable {
         SymbolTable { symbol_table: BTreeMap::new() }

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

@@ -564,7 +564,7 @@ impl GotocCtx<'_> {
             self.intrinsics_typecheck_fail(span, "ctpop", "integer type", arg_rust_ty)
         } else {
             let loc = self.codegen_span_stable(span);
-            self.codegen_expr_to_place_stable(&target_place, arg.popcount(), loc)
+            self.codegen_expr_to_place_stable(target_place, arg.popcount(), loc)
         }
     }
 

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

@@ -335,7 +335,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     let typ = self.codegen_ty_stable(ty);
                     let operation_name = "C string literal";
                     self.codegen_unimplemented_expr(
-                        &operation_name,
+                        operation_name,
                         typ,
                         loc,
                         "https://github.com/model-checking/kani/issues/2549",

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

@@ -731,7 +731,7 @@ impl GotocCtx<'_> {
                     }
                 }
             }
-            AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty),
+            AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(operands, res_ty),
             AggregateKind::CoroutineClosure(_, _) => {
                 let ty = self.codegen_ty_stable(res_ty);
                 self.codegen_unimplemented_expr(
@@ -751,10 +751,10 @@ impl GotocCtx<'_> {
             Rvalue::Use(p) => self.codegen_operand_stable(p),
             Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
-                let place_ref = self.codegen_place_ref_stable(&p, loc);
+                let place_ref = self.codegen_place_ref_stable(p, loc);
                 let place_ref_type = place_ref.typ().clone();
                 match self.codegen_raw_ptr_deref_validity_check(
-                    &p,
+                    p,
                     place_ref.clone(),
                     self.place_ty_stable(p),
                     &loc,

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

@@ -59,10 +59,8 @@ impl GotocCtx<'_> {
                     let arg = parse_word(attr).expect(
                         "incorrect value passed to `disable_checks`, expected a single identifier",
                     );
-                    *PRAGMAS.get(arg.as_str()).expect(format!(
-                        "attempting to disable an unexisting check, the possible options are {:?}",
-                        PRAGMAS.keys()
-                    ).as_str())
+                    *PRAGMAS.get(arg.as_str()).unwrap_or_else(|| panic!("attempting to disable an unexisting check, the possible options are {:?}",
+                        PRAGMAS.keys()))
                 })
                 .collect::<Vec<_>>()
                 .leak() // This is to preserve `Location` being Copy, but could blow up the memory utilization of compiler. 

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

@@ -148,7 +148,7 @@ impl GotocCtx<'_> {
                 // Pack the operands and their types, then call `codegen_copy`
                 let fargs =
                     operands.iter().map(|op| self.codegen_operand_stable(op)).collect::<Vec<_>>();
-                let farg_types = operands.map(|op| self.operand_ty_stable(&op));
+                let farg_types = operands.map(|op| self.operand_ty_stable(op));
                 self.codegen_copy("copy_nonoverlapping", true, fargs, &farg_types, None, location)
             }
             // https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.NonDivergingIntrinsic.html#variant.Assume
@@ -168,7 +168,7 @@ impl GotocCtx<'_> {
                 let instance = self.current_fn().instance_stable();
                 let counter_data = format!("{coverage_opaque:?} ${function_name}$");
                 let maybe_source_region =
-                    region_from_coverage_opaque(self.tcx, &coverage_opaque, instance);
+                    region_from_coverage_opaque(self.tcx, coverage_opaque, instance);
                 if let Some((source_region, file_name)) = maybe_source_region {
                     let coverage_stmt =
                         self.codegen_coverage(&counter_data, stmt.span, source_region, &file_name);
@@ -621,8 +621,8 @@ impl GotocCtx<'_> {
             if def.as_intrinsic().unwrap().must_be_overridden() || !instance.has_body() {
                 return self.codegen_funcall_of_intrinsic(
                     instance,
-                    &args,
-                    &destination,
+                    args,
+                    destination,
                     target.map(|bb| bb),
                     span,
                 );
@@ -638,10 +638,10 @@ impl GotocCtx<'_> {
                 let mut fargs = if args.is_empty()
                     || fn_def.fn_sig().unwrap().value.abi != Abi::RustCall
                 {
-                    self.codegen_funcall_args(&fn_abi, &args)
+                    self.codegen_funcall_args(&fn_abi, args)
                 } else {
                     let (untupled, first_args) = args.split_last().unwrap();
-                    let mut fargs = self.codegen_funcall_args(&fn_abi, &first_args);
+                    let mut fargs = self.codegen_funcall_args(&fn_abi, first_args);
                     fargs.append(
                         &mut self.codegen_untupled_args(untupled, &fn_abi.args[first_args.len()..]),
                     );
@@ -688,11 +688,11 @@ impl GotocCtx<'_> {
                     self.tcx
                         .fn_abi_of_fn_ptr(
                             TypingEnv::fully_monomorphized()
-                                .as_query_input((fn_sig_internal, &List::empty())),
+                                .as_query_input((fn_sig_internal, List::empty())),
                         )
                         .unwrap(),
                 );
-                let fargs = self.codegen_funcall_args(&fn_ptr_abi, &args);
+                let fargs = self.codegen_funcall_args(&fn_ptr_abi, args);
                 let func_expr = self.codegen_operand_stable(func).dereference();
                 // Actually generate the function call and return.
                 Stmt::block(

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -201,12 +201,12 @@ impl GotocCodegenBackend {
         // No output should be generated if user selected no_codegen.
         if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() {
             let pretty = self.queries.lock().unwrap().args().output_pretty_json;
-            write_file(&symtab_goto, ArtifactType::PrettyNameMap, &pretty_name_map, pretty);
+            write_file(symtab_goto, ArtifactType::PrettyNameMap, &pretty_name_map, pretty);
             write_goto_binary_file(symtab_goto, &gcx.symbol_table);
-            write_file(&symtab_goto, ArtifactType::TypeMap, &type_map, pretty);
+            write_file(symtab_goto, ArtifactType::TypeMap, &type_map, pretty);
             // If they exist, write out vtable virtual call function pointer restrictions
             if let Some(restrictions) = vtable_restrictions {
-                write_file(&symtab_goto, ArtifactType::VTableRestriction, &restrictions, pretty);
+                write_file(symtab_goto, ArtifactType::VTableRestriction, &restrictions, pretty);
             }
         }
 
@@ -294,7 +294,7 @@ impl CodegenBackend for GotocCodegenBackend {
                         // We reset the body cache for now because each codegen unit has different
                         // configurations that affect how we transform the instance body.
                         for harness in &unit.harnesses {
-                            let transformer = BodyTransformation::new(&queries, tcx, &unit);
+                            let transformer = BodyTransformation::new(&queries, tcx, unit);
                             let model_path = units.harness_model_path(*harness).unwrap();
                             let is_automatic_harness = units.is_automatic_harness(harness);
                             let contract_metadata =
@@ -355,14 +355,15 @@ impl CodegenBackend for GotocCodegenBackend {
                     for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
                         let instance =
                             if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
-                        let metadata =
-                            gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
+                        let metadata = gen_test_metadata(tcx, *test_desc, *instance, base_filename);
                         let test_model_path = &metadata.goto_file.as_ref().unwrap();
-                        std::fs::copy(&model_path, test_model_path).expect(&format!(
-                            "Failed to copy {} to {}",
-                            model_path.display(),
-                            test_model_path.display()
-                        ));
+                        std::fs::copy(&model_path, test_model_path).unwrap_or_else(|_| {
+                            panic!(
+                                "Failed to copy {} to {}",
+                                model_path.display(),
+                                test_model_path.display()
+                            )
+                        });
                         results.harnesses.push(metadata);
                     }
                 }
@@ -405,7 +406,7 @@ impl CodegenBackend for GotocCodegenBackend {
                     // To avoid overriding the metadata for its verification, we skip this step when
                     // reachability is None, even because there is nothing to record.
                     write_file(
-                        &base_filename,
+                        base_filename,
                         ArtifactType::Metadata,
                         &results.generate_metadata(),
                         queries.args().output_pretty_json,

kani-compiler/src/kani_middle/attributes.rs

@@ -357,19 +357,19 @@ impl<'tcx> KaniAttributes<'tcx> {
             }
             match kind {
                 KaniAttributeKind::ShouldPanic => {
-                    expect_single(self.tcx, kind, &attrs);
+                    expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| {
                         expect_no_args(self.tcx, kind, attr);
                     })
                 }
                 KaniAttributeKind::Recursion => {
-                    expect_single(self.tcx, kind, &attrs);
+                    expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| {
                         expect_no_args(self.tcx, kind, attr);
                     })
                 }
                 KaniAttributeKind::Solver => {
-                    expect_single(self.tcx, kind, &attrs);
+                    expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| {
                         parse_solver(self.tcx, attr);
                     })
@@ -378,7 +378,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                     parse_stubs(self.tcx, self.item, attrs);
                 }
                 KaniAttributeKind::Unwind => {
-                    expect_single(self.tcx, kind, &attrs);
+                    expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| {
                         parse_unwind(self.tcx, attr);
                     })
@@ -389,7 +389,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                             "`proof` and `proof_for_contract` may not be used on the same function.".to_string(),
                         );
                     }
-                    expect_single(self.tcx, kind, &attrs);
+                    expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr))
                 }
                 KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| {
@@ -401,7 +401,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                             "`proof` and `proof_for_contract` may not be used on the same function.".to_string(),
                         );
                     }
-                    expect_single(self.tcx, kind, &attrs);
+                    expect_single(self.tcx, kind, attrs);
                     attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr))
                 }
                 KaniAttributeKind::StubVerified => {
@@ -721,7 +721,7 @@ pub fn test_harness_name(tcx: TyCtxt, def: &impl CrateDef) -> String {
     let def_id = rustc_internal::internal(tcx, def.def_id());
     let attrs = tcx.get_attrs_unchecked(def_id);
     let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap();
-    parse_str_value(&marker).unwrap()
+    parse_str_value(marker).unwrap()
 }
 
 /// Expect the contents of this attribute to be of the format #[attribute =
@@ -749,9 +749,9 @@ fn expect_single<'a>(
     kind: KaniAttributeKind,
     attributes: &'a Vec<&'a Attribute>,
 ) -> &'a Attribute {
-    let attr = attributes
-        .first()
-        .expect(&format!("expected at least one attribute {} in {attributes:?}", kind.as_ref()));
+    let attr = attributes.first().unwrap_or_else(|| {
+        panic!("expected at least one attribute {} in {attributes:?}", kind.as_ref())
+    });
     if attributes.len() > 1 {
         tcx.dcx().span_err(
             attr.span(),
@@ -1061,7 +1061,7 @@ fn syn_attr(tcx: TyCtxt, attr: &Attribute) -> syn::Attribute {
 /// Parse a stable attribute using `syn`.
 fn syn_attr_stable(attr: &AttributeStable) -> syn::Attribute {
     let parser = syn::Attribute::parse_outer;
-    parser.parse_str(&attr.as_str()).unwrap().pop().unwrap()
+    parser.parse_str(attr.as_str()).unwrap().pop().unwrap()
 }
 
 /// Return a more user-friendly string for path by trying to remove unneeded whitespace.