diff --git a/Cargo.lock b/Cargo.lock index 404d463ffd6d..c12bf41cb82d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -257,6 +257,15 @@ dependencies = [ "tracing", ] +[[package]] +name = "crc32fast" +version = "1.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a97769d94ddab943e4510d138150169a2758b5ef3eb191a9ee688de3e23ef7b3" +dependencies = [ + "cfg-if", +] + [[package]] name = "crossbeam-deque" version = "0.8.5" @@ -485,6 +494,7 @@ dependencies = [ "kani_metadata", "lazy_static", "num", + "object", "quote", "regex", "serde", @@ -741,6 +751,19 @@ dependencies = [ "autocfg", ] +[[package]] +name = "object" +version = "0.36.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "084f1a5821ac4c651660a94a7153d27ac9d8a53736203f58b31945ded098070a" +dependencies = [ + "crc32fast", + "hashbrown", + "indexmap", + "memchr", + "wasmparser", +] + [[package]] name = "once_cell" version = "1.19.0" @@ -1461,6 +1484,15 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" +[[package]] +name = "wasmparser" +version = "0.216.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bcdee6bea3619d311fb4b299721e89a986c3470f804b6d534340e412589028e3" +dependencies = [ + "bitflags", +] + [[package]] name = "which" version = "6.0.3" diff --git a/cprover_bindings/src/cbmc_string.rs b/cprover_bindings/src/cbmc_string.rs index 4c392f647759..d869b93a8570 100644 --- a/cprover_bindings/src/cbmc_string.rs +++ b/cprover_bindings/src/cbmc_string.rs @@ -3,9 +3,9 @@ use lazy_static::lazy_static; use std::sync::Mutex; +use string_interner::StringInterner; use string_interner::backend::StringBackend; use string_interner::symbol::SymbolU32; -use string_interner::StringInterner; /// This class implements an interner for Strings. /// CBMC objects to have a large number of strings which refer to names: symbols, files, etc. diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs index d31d213aa7d2..e4730c98d34c 100644 --- a/cprover_bindings/src/env.rs +++ b/cprover_bindings/src/env.rs @@ -8,8 +8,8 @@ //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp]. //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\]. -use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type}; use super::MachineModel; +use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type}; use num::bigint::BigInt; fn int_constant(name: &str, value: T) -> Symbol where diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 16f33115e0ff..dad3b06e7753 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -285,13 +285,10 @@ pub fn arithmetic_overflow_result_type(operand_type: Type) -> Type { // give the struct the name "overflow_result_", e.g. // "overflow_result_Unsignedbv" let name: InternedString = format!("overflow_result_{operand_type:?}").into(); - Type::struct_type( - name, - vec![ - DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type), - DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()), - ], - ) + Type::struct_type(name, vec![ + DatatypeComponent::field(ARITH_OVERFLOW_RESULT_FIELD, operand_type), + DatatypeComponent::field(ARITH_OVERFLOW_OVERFLOWED_FIELD, Type::bool()), + ]) } /////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs index 8b61722344fb..4d17be37f081 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/cprover_bindings/src/goto_program/mod.rs @@ -17,8 +17,8 @@ mod typ; pub use builtin::BuiltinFn; pub use expr::{ - arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue, - SelfOperator, UnaryOperator, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, + ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, ArithmeticOverflowResult, + BinaryOperator, Expr, ExprValue, SelfOperator, UnaryOperator, arithmetic_overflow_result_type, }; pub use location::Location; pub use stmt::{Stmt, StmtBody, SwitchCase}; diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index cd5bd8a6d967..97567670dee0 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use super::super::{env, MachineModel}; +use super::super::{MachineModel, env}; use super::{BuiltinFn, FunctionContract, Stmt, Symbol}; use crate::InternedString; use std::collections::BTreeMap; diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index d0cc8821a447..3210dd46e43f 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -2,8 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use self::DatatypeComponent::*; use self::Type::*; -use super::super::utils::{aggr_tag, max_int, min_int}; use super::super::MachineModel; +use super::super::utils::{aggr_tag, max_int, min_int}; use super::{Expr, SymbolTable}; use crate::cbmc_string::InternedString; use std::collections::BTreeMap; @@ -1598,10 +1598,10 @@ mod type_tests { fn check_typedef_struct_properties() { // Create a struct with a random field. let struct_name: InternedString = "MyStruct".into(); - let struct_type = Type::struct_type( - struct_name, - vec![DatatypeComponent::Field { name: "field".into(), typ: Double }], - ); + let struct_type = Type::struct_type(struct_name, vec![DatatypeComponent::Field { + name: "field".into(), + typ: Double, + }]); // Insert a field to the sym table to represent the struct field. let mut sym_table = SymbolTable::new(machine_model_test_stub()); sym_table.ensure(struct_type.type_name().unwrap(), |_, name| { diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index 6f821768f996..bb725de638cf 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/cprover_bindings/src/irep/goto_binary_serde.rs @@ -1205,12 +1205,12 @@ mod sharing_stats { mod tests { use super::GotoBinarySerializer; use super::IrepNumbering; + use crate::InternedString; use crate::cbmc_string::InternString; - use crate::irep::goto_binary_serde::GotoBinaryDeserializer; use crate::irep::Irep; use crate::irep::IrepId; + use crate::irep::goto_binary_serde::GotoBinaryDeserializer; use crate::linear_map; - use crate::InternedString; use linear_map::LinearMap; use std::io::BufWriter; /// Utility function : creates a Irep representing a single symbol. diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs index 0d0c6dc4ace7..89da8e3446f5 100644 --- a/cprover_bindings/src/irep/irep.rs +++ b/cprover_bindings/src/irep/irep.rs @@ -2,8 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! The actual `Irep` structure, and associated constructors, getters, and setters. -use super::super::goto_program::{Location, Type}; use super::super::MachineModel; +use super::super::goto_program::{Location, Type}; use super::{IrepId, ToIrep}; use crate::cbmc_string::InternedString; use crate::linear_map; diff --git a/cprover_bindings/src/irep/serialize.rs b/cprover_bindings/src/irep/serialize.rs index bf3f0b807f61..06cc7bda17b9 100644 --- a/cprover_bindings/src/irep/serialize.rs +++ b/cprover_bindings/src/irep/serialize.rs @@ -1,10 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //! This crate implements irep serialization using serde Serializer. -use crate::irep::{Irep, IrepId, Symbol, SymbolTable}; use crate::InternedString; -use serde::ser::{SerializeMap, Serializer}; +use crate::irep::{Irep, IrepId, Symbol, SymbolTable}; use serde::Serialize; +use serde::ser::{SerializeMap, Serializer}; impl Serialize for Irep { fn serialize(&self, serializer: S) -> Result @@ -145,14 +145,16 @@ impl Serialize for Symbol { #[cfg(test)] mod test { use super::*; - use serde_test::{assert_ser_tokens, Token}; + use serde_test::{Token, assert_ser_tokens}; #[test] fn serialize_irep() { let irep = Irep::empty(); - assert_ser_tokens( - &irep, - &[Token::Map { len: None }, Token::String("id"), Token::String("empty"), Token::MapEnd], - ); + assert_ser_tokens(&irep, &[ + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + ]); } #[test] @@ -187,80 +189,77 @@ mod test { is_weak: false, }; sym_table.insert(symbol); - assert_ser_tokens( - &sym_table, - &[ - Token::Map { len: None }, - Token::String("symbolTable"), - Token::Map { len: Some(1) }, - Token::String("my_name"), - // symbol start - Token::Map { len: None }, - // type irep - Token::String("type"), - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - // value irep - Token::String("value"), - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - // value locaton - Token::String("location"), - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - Token::String("name"), - Token::String("my_name"), - Token::String("module"), - Token::String(""), - Token::String("baseName"), - Token::String(""), - Token::String("prettyName"), - Token::String(""), - Token::String("mode"), - Token::String(""), - Token::String("isType"), - Token::Bool(false), - Token::String("isMacro"), - Token::Bool(false), - Token::String("isExported"), - Token::Bool(false), - Token::String("isInput"), - Token::Bool(false), - Token::String("isOutput"), - Token::Bool(false), - Token::String("isStateVar"), - Token::Bool(false), - Token::String("isProperty"), - Token::Bool(false), - Token::String("isStaticLifetime"), - Token::Bool(false), - Token::String("isThreadLocal"), - Token::Bool(false), - Token::String("isLvalue"), - Token::Bool(false), - Token::String("isFileLocal"), - Token::Bool(false), - Token::String("isExtern"), - Token::Bool(false), - Token::String("isVolatile"), - Token::Bool(false), - Token::String("isParameter"), - Token::Bool(false), - Token::String("isAuxiliary"), - Token::Bool(false), - Token::String("isWeak"), - Token::Bool(false), - Token::MapEnd, - Token::MapEnd, - Token::MapEnd, - ], - ); + assert_ser_tokens(&sym_table, &[ + Token::Map { len: None }, + Token::String("symbolTable"), + Token::Map { len: Some(1) }, + Token::String("my_name"), + // symbol start + Token::Map { len: None }, + // type irep + Token::String("type"), + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + // value irep + Token::String("value"), + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + // value locaton + Token::String("location"), + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + Token::String("name"), + Token::String("my_name"), + Token::String("module"), + Token::String(""), + Token::String("baseName"), + Token::String(""), + Token::String("prettyName"), + Token::String(""), + Token::String("mode"), + Token::String(""), + Token::String("isType"), + Token::Bool(false), + Token::String("isMacro"), + Token::Bool(false), + Token::String("isExported"), + Token::Bool(false), + Token::String("isInput"), + Token::Bool(false), + Token::String("isOutput"), + Token::Bool(false), + Token::String("isStateVar"), + Token::Bool(false), + Token::String("isProperty"), + Token::Bool(false), + Token::String("isStaticLifetime"), + Token::Bool(false), + Token::String("isThreadLocal"), + Token::Bool(false), + Token::String("isLvalue"), + Token::Bool(false), + Token::String("isFileLocal"), + Token::Bool(false), + Token::String("isExtern"), + Token::Bool(false), + Token::String("isVolatile"), + Token::Bool(false), + Token::String("isParameter"), + Token::Bool(false), + Token::String("isAuxiliary"), + Token::Bool(false), + Token::String("isWeak"), + Token::Bool(false), + Token::MapEnd, + Token::MapEnd, + Token::MapEnd, + ]); } #[test] @@ -269,41 +268,38 @@ mod test { let one_irep = Irep::one(); let sub_irep = Irep::just_sub(vec![empty_irep.clone(), one_irep]); let top_irep = Irep::just_sub(vec![sub_irep, empty_irep]); - assert_ser_tokens( - &top_irep, - &[ - // top_irep - Token::Map { len: None }, - Token::String("id"), - Token::String(""), - Token::String("sub"), - Token::Seq { len: Some(2) }, - // sub_irep - Token::Map { len: None }, - Token::String("id"), - Token::String(""), - Token::String("sub"), - Token::Seq { len: Some(2) }, - // empty_irep - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - // one_irep - Token::Map { len: None }, - Token::String("id"), - Token::String("1"), - Token::MapEnd, - Token::SeqEnd, - Token::MapEnd, - // empty_irep - Token::Map { len: None }, - Token::String("id"), - Token::String("empty"), - Token::MapEnd, - Token::SeqEnd, - Token::MapEnd, - ], - ); + assert_ser_tokens(&top_irep, &[ + // top_irep + Token::Map { len: None }, + Token::String("id"), + Token::String(""), + Token::String("sub"), + Token::Seq { len: Some(2) }, + // sub_irep + Token::Map { len: None }, + Token::String("id"), + Token::String(""), + Token::String("sub"), + Token::Seq { len: Some(2) }, + // empty_irep + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + // one_irep + Token::Map { len: None }, + Token::String("id"), + Token::String("1"), + Token::MapEnd, + Token::SeqEnd, + Token::MapEnd, + // empty_irep + Token::Map { len: None }, + Token::String("id"), + Token::String("empty"), + Token::MapEnd, + Token::SeqEnd, + Token::MapEnd, + ]); } } diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index bf0b8ce862dd..788c9f1e79d4 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -2,11 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Converts a typed goto-program into the `Irep` serilization format of CBMC // TODO: consider making a macro to replace `linear_map![])` for initilizing btrees. -use super::super::goto_program; use super::super::MachineModel; +use super::super::goto_program; use super::{Irep, IrepId}; -use crate::linear_map; use crate::InternedString; +use crate::linear_map; use goto_program::{ BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Lambda, Location, Parameter, SelfOperator, Stmt, StmtBody, SwitchCase, SymbolValues, Type, UnaryOperator, @@ -273,10 +273,12 @@ impl ToIrep for ExprValue { )], } } - ExprValue::FunctionCall { function, arguments } => side_effect_irep( - IrepId::FunctionCall, - vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)], - ), + ExprValue::FunctionCall { function, arguments } => { + side_effect_irep(IrepId::FunctionCall, vec![ + function.to_irep(mm), + arguments_irep(arguments.iter(), mm), + ]) + } ExprValue::If { c, t, e } => Irep { id: IrepId::If, sub: vec![c.to_irep(mm), t.to_irep(mm), e.to_irep(mm)], @@ -318,10 +320,11 @@ impl ToIrep for ExprValue { named_sub: linear_map![], }, ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]), - ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep( - IrepId::StatementExpression, - vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)], - ), + ExprValue::StatementExpression { statements: ops, location: loc } => { + side_effect_irep(IrepId::StatementExpression, vec![ + Stmt::block(ops.to_vec(), *loc).to_irep(mm), + ]) + } ExprValue::StringConstant { s } => Irep { id: IrepId::StringConstant, sub: vec![], @@ -488,10 +491,10 @@ impl ToIrep for StmtBody { StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]), StmtBody::Decl { lhs, value } => { if value.is_some() { - code_irep( - IrepId::Decl, - vec![lhs.to_irep(mm), value.as_ref().unwrap().to_irep(mm)], - ) + code_irep(IrepId::Decl, vec![ + lhs.to_irep(mm), + value.as_ref().unwrap().to_irep(mm), + ]) } else { code_irep(IrepId::Decl, vec![lhs.to_irep(mm)]) } @@ -504,28 +507,26 @@ impl ToIrep for StmtBody { .with_comment("deinit") } StmtBody::Expression(e) => code_irep(IrepId::Expression, vec![e.to_irep(mm)]), - StmtBody::For { init, cond, update, body } => code_irep( - IrepId::For, - vec![init.to_irep(mm), cond.to_irep(mm), update.to_irep(mm), body.to_irep(mm)], - ), - StmtBody::FunctionCall { lhs, function, arguments } => code_irep( - IrepId::FunctionCall, - vec![ + StmtBody::For { init, cond, update, body } => code_irep(IrepId::For, vec![ + init.to_irep(mm), + cond.to_irep(mm), + update.to_irep(mm), + body.to_irep(mm), + ]), + StmtBody::FunctionCall { lhs, function, arguments } => { + code_irep(IrepId::FunctionCall, vec![ lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)), function.to_irep(mm), arguments_irep(arguments.iter(), mm), - ], - ), + ]) + } StmtBody::Goto(dest) => code_irep(IrepId::Goto, vec![]) .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())), - StmtBody::Ifthenelse { i, t, e } => code_irep( - IrepId::Ifthenelse, - vec![ - i.to_irep(mm), - t.to_irep(mm), - e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)), - ], - ), + StmtBody::Ifthenelse { i, t, e } => code_irep(IrepId::Ifthenelse, vec![ + i.to_irep(mm), + t.to_irep(mm), + e.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)), + ]), StmtBody::Label { label, body } => code_irep(IrepId::Label, vec![body.to_irep(mm)]) .with_named_sub(IrepId::Label, Irep::just_string_id(label.to_string())), StmtBody::Return(e) => { @@ -537,10 +538,10 @@ impl ToIrep for StmtBody { if default.is_some() { switch_arms.push(switch_default_irep(default.as_ref().unwrap(), mm)); } - code_irep( - IrepId::Switch, - vec![control.to_irep(mm), code_irep(IrepId::Block, switch_arms)], - ) + code_irep(IrepId::Switch, vec![ + control.to_irep(mm), + code_irep(IrepId::Block, switch_arms), + ]) } StmtBody::While { cond, body } => { code_irep(IrepId::While, vec![cond.to_irep(mm), body.to_irep(mm)]) diff --git a/cprover_bindings/src/utils.rs b/cprover_bindings/src/utils.rs index dd1d39ee53d1..4a323277ec9e 100644 --- a/cprover_bindings/src/utils.rs +++ b/cprover_bindings/src/utils.rs @@ -3,8 +3,8 @@ //! Useful utilities for CBMC use crate::InternedString; -use num::bigint::{BigInt, Sign}; use num::Signed; +use num::bigint::{BigInt, Sign}; use num_traits::Zero; /// The aggregate name used in CBMC for aggregates of type `n`. diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9ca8d10f5275..9a4a0de43a34 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -28,6 +28,11 @@ tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_de tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} tracing-tree = "0.4.0" +[dependencies.object] +version = "0.36.2" +default-features = false +features = ["elf", "macho", "pe", "xcoff", "write", "wasm"] + # Future proofing: enable backend dependencies using feature. [features] default = ['cprover'] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index c81d60e40d42..66d6e2eb1ab4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -19,8 +19,8 @@ //! use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::InternedString; +use cbmc::goto_program::{Expr, Location, Stmt, Type}; use rustc_middle::mir::coverage::SourceRegion; use stable_mir::mir::{Place, ProjectionElem}; use stable_mir::ty::{Span as SpanStable, Ty}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index a871cd58f94f..26caf29bea1d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -1,16 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx}; +use crate::codegen_cprover_gotoc::{GotocCtx, codegen::ty_stable::pointee_type_stable}; use crate::kani_middle::attributes::KaniAttributes; use cbmc::goto_program::FunctionContract; use cbmc::goto_program::{Expr, Lambda, Location, Type}; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; +use stable_mir::CrateDef; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::mir::{Local, VarDebugInfoContents}; use stable_mir::ty::{FnDef, RigidTy, TyKind}; -use stable_mir::CrateDef; impl<'tcx> GotocCtx<'tcx> { /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 386a50bc7ebc..1a68533d3dce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -9,17 +9,17 @@ //! linking and usability unless unstable C-FFI support is enabled. use std::collections::HashSet; -use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; +use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; use cbmc::{InternString, InternedString}; use lazy_static::lazy_static; +use stable_mir::CrateDef; use stable_mir::abi::{CallConvention, PassMode}; -use stable_mir::mir::mono::Instance; use stable_mir::mir::Place; +use stable_mir::mir::mono::Instance; use stable_mir::ty::{RigidTy, TyKind}; -use stable_mir::CrateDef; use tracing::{debug, trace}; lazy_static! { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 34f8363f4948..eae547d58a4f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -3,14 +3,14 @@ //! This file contains functions related to codegenning MIR functions into gotoc -use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder; use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{Expr, Stmt, Symbol}; +use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder; use cbmc::InternString; +use cbmc::goto_program::{Expr, Stmt, Symbol}; +use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Body, Local}; use stable_mir::ty::{RigidTy, TyKind}; -use stable_mir::CrateDef; use std::collections::BTreeMap; use tracing::{debug, debug_span}; @@ -223,8 +223,8 @@ pub mod rustc_smir { use rustc_middle::mir::coverage::MappingKind::Code; use rustc_middle::mir::coverage::SourceRegion; use rustc_middle::ty::TyCtxt; - use stable_mir::mir::mono::Instance; use stable_mir::Opaque; + use stable_mir::mir::mono::Instance; type CoverageOpaque = stable_mir::Opaque; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 4b66d60e735b..79afe39fd89e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -2,16 +2,16 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! this module handles intrinsics use super::typ; -use super::{bb_label, PropertyClass}; +use super::{PropertyClass, bb_label}; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; -use crate::codegen_cprover_gotoc::{utils, GotocCtx}; +use crate::codegen_cprover_gotoc::{GotocCtx, utils}; use crate::intrinsics::Intrinsic; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{ ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, }; -use rustc_middle::ty::layout::ValidityRequirement; use rustc_middle::ty::ParamEnv; +use rustc_middle::ty::layout::ValidityRequirement; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{BasicBlockIdx, Operand, Place}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 85bb8292ec67..3c67741667c2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; use crate::codegen_cprover_gotoc::GotocCtx; +use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type}; use rustc_middle::ty::Const as ConstInternal; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index d0e3fc3f442f..fb1ddb76e3a2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -6,10 +6,10 @@ //! in [GotocCtx::codegen_place] below. use super::typ::TypeExt; +use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type; use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; -use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type}; use rustc_middle::ty::layout::LayoutOf; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 7abd949357ff..7a4594a181e3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1,21 +1,21 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; -use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::kani_middle::coercion::{ - extract_unsize_casting_stable, CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable, + CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable, extract_unsize_casting_stable, }; use crate::unwrap_or_return_codegen_unimplemented; +use cbmc::MachineModel; use cbmc::goto_program::{ - arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Type, - ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, + ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, BinaryOperator, Expr, Location, + Stmt, Type, arithmetic_overflow_result_type, }; -use cbmc::MachineModel; -use cbmc::{btree_string_map, InternString, InternedString}; +use cbmc::{InternString, InternedString, btree_string_map}; use num::bigint::BigInt; use rustc_middle::ty::{ParamEnv, TyCtxt, VtblEntry}; use rustc_smir::rustc_internal; @@ -927,10 +927,10 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty) -> Expr { let layout = self.layout_of_stable(ty); assert!( - matches!( - &layout.variants, - Variants::Multiple { tag_encoding: TagEncoding::Direct, .. } - ), + matches!(&layout.variants, Variants::Multiple { + tag_encoding: TagEncoding::Direct, + .. + }), "discriminant field (`case`) only exists for multiple variants and direct encoding" ); let expr = if ty.kind().is_coroutine() { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index ed0178511126..e54f962336d0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use super::typ::TypeExt; use super::typ::FN_RETURN_VOID_VAR_NAME; -use super::{bb_label, PropertyClass}; +use super::typ::TypeExt; +use super::{PropertyClass, bb_label}; use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; @@ -15,7 +15,7 @@ use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::{ AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place, - Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL, + RETURN_LOCAL, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, }; use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx}; use tracing::{debug, debug_span, trace}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index 537fbcb63fbb..a45c3a8d69a0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -5,8 +5,8 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::is_interior_mut; -use stable_mir::mir::mono::{Instance, StaticDef}; use stable_mir::CrateDef; +use stable_mir::mir::mono::{Instance, StaticDef}; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 016bf0d3a261..ae45a2456794 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -6,10 +6,10 @@ use cbmc::utils::aggr_tag; use cbmc::{InternString, InternedString}; use rustc_ast::ast::Mutability; use rustc_index::IndexVec; +use rustc_middle::ty::GenericArgsRef; use rustc_middle::ty::layout::LayoutOf; -use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::print::FmtPrinter; -use rustc_middle::ty::GenericArgsRef; +use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::{ self, AdtDef, Const, CoroutineArgs, CoroutineArgsExt, FloatTy, Instance, IntTy, PolyFnSig, Ty, TyCtxt, TyKind, UintTy, VariantDef, VtblEntry, @@ -22,8 +22,8 @@ use rustc_target::abi::{ TyAndLayout, VariantIdx, Variants, }; use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; -use stable_mir::mir::mono::Instance as InstanceStable; use stable_mir::mir::Body; +use stable_mir::mir::mono::Instance as InstanceStable; use tracing::{debug, trace, warn}; /// Map the unit type to an empty struct diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9f700192f2f2..1efc41785351 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -6,7 +6,7 @@ use crate::args::ReachabilityType; use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::analysis; -use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes}; +use crate::kani_middle::attributes::{KaniAttributes, is_test_harness_description}; use crate::kani_middle::check_reachable_items; use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; use crate::kani_middle::metadata::gen_test_metadata; @@ -16,34 +16,39 @@ use crate::kani_middle::reachability::{ }; use crate::kani_middle::transform::{BodyTransformation, GlobalPasses}; use crate::kani_queries::QueryDb; +use cbmc::RoundingMode; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; -use cbmc::RoundingMode; use cbmc::{InternedString, MachineModel}; -use kani_metadata::artifact::convert_type; use kani_metadata::UnsupportedFeature; +use kani_metadata::artifact::convert_type; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; +use object::write::{self, StandardSegment, Symbol, SymbolSection}; +use object::{ + Architecture, BinaryFormat, Endianness, FileFlags, SectionFlags, SectionKind, SubArchitecture, + SymbolFlags, SymbolKind, SymbolScope, elf, pe, xcoff, +}; use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER}; -use rustc_codegen_ssa::back::metadata::create_wrapper_file; +use rustc_codegen_ssa::back::metadata::create_metadata_file_for_wasm; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_data_structures::temp_dir::MaybeTempDir; -use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; +use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed}; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; -use rustc_metadata::creader::MetadataLoaderDyn; -use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; +use rustc_metadata::fs::{METADATA_FILENAME, emit_wrapper_file}; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::ty::TyCtxt; use rustc_middle::util::Providers; +use rustc_session::Session; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; -use rustc_session::Session; use rustc_smir::rustc_internal; +use rustc_span::sym; use rustc_target::abi::Endian; -use rustc_target::spec::PanicStrategy; +use rustc_target::spec::{PanicStrategy, RelocModel, Target, ef_avr_arch}; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; @@ -224,11 +229,293 @@ impl GotocCodegenBackend { } } -impl CodegenBackend for GotocCodegenBackend { - fn metadata_loader(&self) -> Box { - Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader) +// Copy of macho_object_build_version_for_target from +// rust/compiler/rustc_codegen_ssa/src/back/metadata.rs +fn macho_object_build_version_for_target(target: &Target) -> object::write::MachOBuildVersion { + /// The `object` crate demands "X.Y.Z encoded in nibbles as xxxx.yy.zz" + /// e.g. minOS 14.0 = 0x000E0000, or SDK 16.2 = 0x00100200 + fn pack_version((major, minor, patch): (u16, u8, u8)) -> u32 { + let (major, minor, patch) = (major as u32, minor as u32, patch as u32); + (major << 16) | (minor << 8) | patch } + let platform = + rustc_target::spec::current_apple_platform(target).expect("unknown Apple target OS"); + let min_os = rustc_target::spec::current_apple_deployment_target(target); + let (sdk_major, sdk_minor) = + rustc_target::spec::current_apple_sdk_version(platform).expect("unknown Apple target OS"); + + let mut build_version = object::write::MachOBuildVersion::default(); + build_version.platform = platform; + build_version.minos = pack_version(min_os); + build_version.sdk = pack_version((sdk_major, sdk_minor, 0)); + build_version +} + +// Copy of create_object_file from +// rust/compiler/rustc_codegen_ssa/src/back/metadata.rs +fn create_object_file(sess: &Session) -> Option> { + let endianness = match sess.target.options.endian { + Endian::Little => Endianness::Little, + Endian::Big => Endianness::Big, + }; + let (architecture, sub_architecture) = match &sess.target.arch[..] { + "arm" => (Architecture::Arm, None), + "aarch64" => ( + if sess.target.pointer_width == 32 { + Architecture::Aarch64_Ilp32 + } else { + Architecture::Aarch64 + }, + None, + ), + "x86" => (Architecture::I386, None), + "s390x" => (Architecture::S390x, None), + "mips" | "mips32r6" => (Architecture::Mips, None), + "mips64" | "mips64r6" => (Architecture::Mips64, None), + "x86_64" => ( + if sess.target.pointer_width == 32 { + Architecture::X86_64_X32 + } else { + Architecture::X86_64 + }, + None, + ), + "powerpc" => (Architecture::PowerPc, None), + "powerpc64" => (Architecture::PowerPc64, None), + "riscv32" => (Architecture::Riscv32, None), + "riscv64" => (Architecture::Riscv64, None), + "sparc" => (Architecture::Sparc32Plus, None), + "sparc64" => (Architecture::Sparc64, None), + "avr" => (Architecture::Avr, None), + "msp430" => (Architecture::Msp430, None), + "hexagon" => (Architecture::Hexagon, None), + "bpf" => (Architecture::Bpf, None), + "loongarch64" => (Architecture::LoongArch64, None), + "csky" => (Architecture::Csky, None), + "arm64ec" => (Architecture::Aarch64, Some(SubArchitecture::Arm64EC)), + // Unsupported architecture. + _ => return None, + }; + let binary_format = if sess.target.is_like_osx { + BinaryFormat::MachO + } else if sess.target.is_like_windows { + BinaryFormat::Coff + } else if sess.target.is_like_aix { + BinaryFormat::Xcoff + } else { + BinaryFormat::Elf + }; + + let mut file = write::Object::new(binary_format, architecture, endianness); + file.set_sub_architecture(sub_architecture); + if sess.target.is_like_osx { + if sess.target.llvm_target.starts_with("arm64e") { + file.set_macho_cpu_subtype(object::macho::CPU_SUBTYPE_ARM64E); + } + + file.set_macho_build_version(macho_object_build_version_for_target(&sess.target)) + } + if binary_format == BinaryFormat::Coff { + // Disable the default mangler to avoid mangling the special "@feat.00" symbol name. + let original_mangling = file.mangling(); + file.set_mangling(object::write::Mangling::None); + + let mut feature = 0; + + if file.architecture() == object::Architecture::I386 { + // When linking with /SAFESEH on x86, lld requires that all linker inputs be marked as + // safe exception handling compatible. Metadata files masquerade as regular COFF + // objects and are treated as linker inputs, despite containing no actual code. Thus, + // they still need to be marked as safe exception handling compatible. See #96498. + // Reference: https://docs.microsoft.com/en-us/windows/win32/debug/pe-format + feature |= 1; + } + + file.add_symbol(object::write::Symbol { + name: "@feat.00".into(), + value: feature, + size: 0, + kind: object::SymbolKind::Data, + scope: object::SymbolScope::Compilation, + weak: false, + section: object::write::SymbolSection::Absolute, + flags: object::SymbolFlags::None, + }); + + file.set_mangling(original_mangling); + } + let e_flags = match architecture { + Architecture::Mips => { + let arch = match sess.target.options.cpu.as_ref() { + "mips1" => elf::EF_MIPS_ARCH_1, + "mips2" => elf::EF_MIPS_ARCH_2, + "mips3" => elf::EF_MIPS_ARCH_3, + "mips4" => elf::EF_MIPS_ARCH_4, + "mips5" => elf::EF_MIPS_ARCH_5, + s if s.contains("r6") => elf::EF_MIPS_ARCH_32R6, + _ => elf::EF_MIPS_ARCH_32R2, + }; + + let mut e_flags = elf::EF_MIPS_CPIC | arch; + + // If the ABI is explicitly given, use it or default to O32. + match sess.target.options.llvm_abiname.to_lowercase().as_str() { + "n32" => e_flags |= elf::EF_MIPS_ABI2, + "o32" => e_flags |= elf::EF_MIPS_ABI_O32, + _ => e_flags |= elf::EF_MIPS_ABI_O32, + }; + + if sess.target.options.relocation_model != RelocModel::Static { + e_flags |= elf::EF_MIPS_PIC; + } + if sess.target.options.cpu.contains("r6") { + e_flags |= elf::EF_MIPS_NAN2008; + } + e_flags + } + Architecture::Mips64 => { + // copied from `mips64el-linux-gnuabi64-gcc foo.c -c` + elf::EF_MIPS_CPIC + | elf::EF_MIPS_PIC + | if sess.target.options.cpu.contains("r6") { + elf::EF_MIPS_ARCH_64R6 | elf::EF_MIPS_NAN2008 + } else { + elf::EF_MIPS_ARCH_64R2 + } + } + Architecture::Riscv32 | Architecture::Riscv64 => { + // Source: https://github.com/riscv-non-isa/riscv-elf-psabi-doc/blob/079772828bd10933d34121117a222b4cc0ee2200/riscv-elf.adoc + let mut e_flags: u32 = 0x0; + + // Check if compressed is enabled + // `unstable_target_features` is used here because "c" is gated behind riscv_target_feature. + if sess.unstable_target_features.contains(&sym::c) { + e_flags |= elf::EF_RISCV_RVC; + } + + // Set the appropriate flag based on ABI + // This needs to match LLVM `RISCVELFStreamer.cpp` + match &*sess.target.llvm_abiname { + "" | "ilp32" | "lp64" => (), + "ilp32f" | "lp64f" => e_flags |= elf::EF_RISCV_FLOAT_ABI_SINGLE, + "ilp32d" | "lp64d" => e_flags |= elf::EF_RISCV_FLOAT_ABI_DOUBLE, + "ilp32e" => e_flags |= elf::EF_RISCV_RVE, + _ => panic!("unknown RISC-V ABI name"), + } + + e_flags + } + Architecture::LoongArch64 => { + // Source: https://github.com/loongson/la-abi-specs/blob/release/laelf.adoc#e_flags-identifies-abi-type-and-version + let mut e_flags: u32 = elf::EF_LARCH_OBJABI_V1; + + // Set the appropriate flag based on ABI + // This needs to match LLVM `LoongArchELFStreamer.cpp` + match &*sess.target.llvm_abiname { + "ilp32s" | "lp64s" => e_flags |= elf::EF_LARCH_ABI_SOFT_FLOAT, + "ilp32f" | "lp64f" => e_flags |= elf::EF_LARCH_ABI_SINGLE_FLOAT, + "ilp32d" | "lp64d" => e_flags |= elf::EF_LARCH_ABI_DOUBLE_FLOAT, + _ => panic!("unknown LoongArch ABI name"), + } + + e_flags + } + Architecture::Avr => { + // Resolve the ISA revision and set + // the appropriate EF_AVR_ARCH flag. + ef_avr_arch(&sess.target.options.cpu) + } + Architecture::Csky => { + let e_flags = match sess.target.options.abi.as_ref() { + "abiv2" => elf::EF_CSKY_ABIV2, + _ => elf::EF_CSKY_ABIV1, + }; + e_flags + } + _ => 0, + }; + // adapted from LLVM's `MCELFObjectTargetWriter::getOSABI` + let os_abi = match sess.target.options.os.as_ref() { + "hermit" => elf::ELFOSABI_STANDALONE, + "freebsd" => elf::ELFOSABI_FREEBSD, + "solaris" => elf::ELFOSABI_SOLARIS, + _ => elf::ELFOSABI_NONE, + }; + let abi_version = 0; + // rustc implementation also does: + // add_gnu_property_note(&mut file, architecture, binary_format, endianness); + file.flags = FileFlags::Elf { os_abi, abi_version, e_flags }; + Some(file) +} + +// copy of create_wrapper_file from +// rust/compiler/rustc_codegen_ssa/src/back/metadata.rs +// without the MetadataPosition return value, which we don't need +fn create_wrapper_file(sess: &Session, section_name: String, data: &[u8]) -> Vec { + let Some(mut file) = create_object_file(sess) else { + if sess.target.is_like_wasm { + return create_metadata_file_for_wasm(sess, data, §ion_name); + } + + // Targets using this branch don't have support implemented here yet or + // they're not yet implemented in the `object` crate and will likely + // fill out this module over time. + return data.to_vec(); + }; + let section = if file.format() == BinaryFormat::Xcoff { + file.add_section(Vec::new(), b".info".to_vec(), SectionKind::Debug) + } else { + file.add_section( + file.segment_name(StandardSegment::Debug).to_vec(), + section_name.into_bytes(), + SectionKind::Debug, + ) + }; + match file.format() { + BinaryFormat::Coff => { + file.section_mut(section).flags = + SectionFlags::Coff { characteristics: pe::IMAGE_SCN_LNK_REMOVE }; + } + BinaryFormat::Elf => { + file.section_mut(section).flags = + SectionFlags::Elf { sh_flags: elf::SHF_EXCLUDE as u64 }; + } + BinaryFormat::Xcoff => { + // AIX system linker may aborts if it meets a valid XCOFF file in archive with no .text, no .data and no .bss. + file.add_section(Vec::new(), b".text".to_vec(), SectionKind::Text); + file.section_mut(section).flags = + SectionFlags::Xcoff { s_flags: xcoff::STYP_INFO as u32 }; + // Encode string stored in .info section of XCOFF. + // FIXME: The length of data here is not guaranteed to fit in a u32. + // We may have to split the data into multiple pieces in order to + // store in .info section. + let len: u32 = data.len().try_into().unwrap(); + let offset = file.append_section_data(section, &len.to_be_bytes(), 1); + // Add a symbol referring to the data in .info section. + file.add_symbol(Symbol { + name: "__aix_rust_metadata".into(), + value: offset + 4, + size: 0, + kind: SymbolKind::Unknown, + scope: SymbolScope::Compilation, + weak: false, + section: SymbolSection::Section(section), + flags: SymbolFlags::Xcoff { + n_sclass: xcoff::C_INFO, + x_smtyp: xcoff::C_HIDEXT, + x_smclas: xcoff::C_HIDEXT, + containing_csect: None, + }, + }); + } + _ => {} + }; + file.append_section_data(section, data, 1); + file.write().unwrap() +} + +impl CodegenBackend for GotocCodegenBackend { fn provide(&self, providers: &mut Providers) { provide::provide(providers, &self.queries.lock().unwrap()); } @@ -439,7 +726,7 @@ impl CodegenBackend for GotocCodegenBackend { let mut builder = Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER)); let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap(); let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); - let (metadata, _metadata_position) = create_wrapper_file( + let metadata = create_wrapper_file( sess, ".rmeta".to_string(), codegen_results.metadata.raw_data(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index ea3c9e909eb6..246b6cd94b47 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -2,13 +2,13 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::Stmt; use cbmc::InternedString; +use cbmc::goto_program::Stmt; use rustc_middle::ty::Instance as InstanceInternal; use rustc_smir::rustc_internal; -use stable_mir::mir::mono::Instance; -use stable_mir::mir::{visit::Location, visit::MirVisitor, Body, Local, LocalDecl, Rvalue}; use stable_mir::CrateDef; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{Body, Local, LocalDecl, Rvalue, visit::Location, visit::MirVisitor}; use std::collections::{HashMap, HashSet}; /// This structure represents useful data about the function we are currently compiling. diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 3f17f4b87233..d88506464cf7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -16,9 +16,9 @@ //! this structure as input. use super::current_fn::CurrentFnCtx; use super::vtable_ctx::VtableCtx; -use crate::codegen_cprover_gotoc::overrides::{fn_hooks, GotocHooks}; -use crate::codegen_cprover_gotoc::utils::full_crate_name; use crate::codegen_cprover_gotoc::UnsupportedConstructs; +use crate::codegen_cprover_gotoc::overrides::{GotocHooks, fn_hooks}; +use crate::codegen_cprover_gotoc::utils::full_crate_name; use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; use cbmc::goto_program::{ @@ -33,12 +33,12 @@ use rustc_middle::ty::layout::{ TyAndLayout, }; use rustc_middle::ty::{self, Ty, TyCtxt}; -use rustc_span::source_map::respan; use rustc_span::Span; +use rustc_span::source_map::respan; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use stable_mir::mir::mono::Instance; use stable_mir::mir::Body; +use stable_mir::mir::mono::Instance; use stable_mir::ty::Allocation; use std::fmt::Debug; diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs index 98e78ed2b5fd..854ddf6baa57 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::codegen_cprover_gotoc::GotocCtx; /// We can improve verification performance by conveying semantic information /// about function pointer calls down to the underlying solver. In particular, /// method calls through Rust dynamic trait objects use a vtable (virtual method @@ -16,9 +17,8 @@ /// For the current CBMC implementation of function restrictions, see: /// http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html use crate::codegen_cprover_gotoc::codegen::typ::pointee_type; -use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::{Stmt, Type}; use cbmc::InternedString; +use cbmc::goto_program::{Stmt, Type}; use kani_metadata::{CallSite, PossibleMethodEntry, TraitDefinedMethod, VtableCtxResults}; use rustc_data_structures::fx::FxHashMap; use tracing::debug; diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index c0df279932f6..da3cef9e3564 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -8,8 +8,8 @@ //! It would be too nasty if we spread around these sort of undocumented hooks in place, so //! this module addresses this issue. -use crate::codegen_cprover_gotoc::codegen::{bb_label, PropertyClass}; use crate::codegen_cprover_gotoc::GotocCtx; +use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label}; use crate::kani_middle::attributes::matches_diagnostic as matches_function; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{BuiltinFn, Expr, Stmt, Type}; @@ -17,7 +17,7 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{BasicBlockIdx, Place}; -use stable_mir::{ty::Span, CrateDef}; +use stable_mir::{CrateDef, ty::Span}; use std::rc::Rc; use tracing::debug; diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs index 3dda5076fb89..1ba563527626 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs @@ -8,4 +8,4 @@ mod hooks; -pub use hooks::{fn_hooks, GotocHooks}; +pub use hooks::{GotocHooks, fn_hooks}; diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs index 0c69cb30b37f..fe19c854c2ac 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs @@ -5,9 +5,9 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; -use stable_mir::mir::mono::Instance; -use stable_mir::mir::Body; use stable_mir::CrateDef; +use stable_mir::mir::Body; +use stable_mir::mir::mono::Instance; use std::cell::RefCell; use std::panic; use std::sync::LazyLock; diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs index 16edca2a826c..faf1ed61dc2f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs @@ -3,7 +3,7 @@ use super::super::codegen::TypeExt; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type}; -use cbmc::{btree_string_map, InternedString}; +use cbmc::{InternedString, btree_string_map}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::ty::Span; diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 9485d8525410..13a12751bd07 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -4,7 +4,7 @@ //! Single source of truth about which intrinsics we support. use stable_mir::{ - mir::{mono::Instance, Mutability}, + mir::{Mutability, mono::Instance}, ty::{FloatTy, IntTy, RigidTy, TyKind, UintTy}, }; diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 0adee0e52cca..b232db8feecb 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -9,7 +9,7 @@ use stable_mir::mir::mono::MonoItem; use stable_mir::mir::{ - visit::Location, MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, visit::Location, }; use std::collections::HashMap; use std::fmt::Display; diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 86e97f633dfb..630f818231c9 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -7,7 +7,7 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; use rustc_ast::{ - attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, + AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, attr, }; use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; @@ -25,7 +25,7 @@ use syn::{PathSegment, TypePath}; use tracing::{debug, trace}; -use super::resolve::{resolve_fn, resolve_fn_path, FnResolution, ResolveError}; +use super::resolve::{FnResolution, ResolveError, resolve_fn, resolve_fn_path}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] #[strum(serialize_all = "snake_case")] diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index d16e4d2b93d1..071e880ffd9f 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -19,9 +19,9 @@ use rustc_hir::def_id::DefId; use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; +use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind}; -use stable_mir::CrateDef; use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 38760fca300d..224abef1b02b 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -15,12 +15,12 @@ use rustc_hir::lang_items::LangItem; use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData}; -use rustc_middle::ty::adjustment::CustomCoerceUnsized; use rustc_middle::ty::TraitRef; +use rustc_middle::ty::adjustment::CustomCoerceUnsized; use rustc_middle::ty::{ParamEnv, Ty, TyCtxt}; use rustc_smir::rustc_internal; -use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind}; use stable_mir::Symbol; +use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind}; use tracing::trace; /// Given an unsized coercion (e.g. from `&u8` to `&dyn Debug`), extract the pair of diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index 73e42be00e7b..c32ec38a3696 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -8,7 +8,7 @@ use rustc_middle::mir::{Local, LocalDecl}; use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_middle::ty::{Const, GenericArgsRef, IntrinsicDef}; use rustc_span::source_map::Spanned; -use rustc_span::symbol::{sym, Symbol}; +use rustc_span::symbol::{Symbol, sym}; use tracing::{debug, trace}; pub struct ModelIntrinsics<'tcx> { diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 2f0f22d49e1c..db6b6b06149a 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -8,10 +8,10 @@ use std::path::Path; use crate::kani_middle::attributes::test_harness_name; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; -use stable_mir::mir::mono::Instance; use stable_mir::CrateDef; +use stable_mir::mir::mono::Instance; -use super::{attributes::KaniAttributes, SourceLocation}; +use super::{SourceLocation, attributes::KaniAttributes}; /// Create the harness metadata for a proof harness for a given function. pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata { diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index f281e5de5e88..5f7f4c28068f 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -14,14 +14,14 @@ use rustc_middle::ty::layout::{ }; use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt}; use rustc_smir::rustc_internal; -use rustc_span::source_map::respan; use rustc_span::Span; +use rustc_span::source_map::respan; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use stable_mir::CrateDef; use stable_mir::mir::mono::MonoItem; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; -use stable_mir::CrateDef; use std::ops::ControlFlow; use self::attributes::KaniAttributes; diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 68343ccaad37..040a925e140f 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -42,8 +42,8 @@ use rustc_middle::{ }; use rustc_mir_dataflow::{Analysis, AnalysisDomain, Forward, JoinSemiLattice}; use rustc_smir::rustc_internal; -use rustc_span::{source_map::Spanned, DUMMY_SP}; -use stable_mir::mir::{mono::Instance as StableInstance, Body as StableBody}; +use rustc_span::{DUMMY_SP, source_map::Spanned}; +use stable_mir::mir::{Body as StableBody, mono::Instance as StableInstance}; use std::collections::HashSet; /// Main points-to analysis object. @@ -458,22 +458,19 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { // Sanity check. The first argument is the closure itself and the second argument is the tupled arguments from the caller. assert!(args.len() == 2); // First, connect all upvars. - let lvalue_set = HashSet::from([MemLoc::new_stack_allocation( - instance, - Place { local: 1usize.into(), projection: List::empty() }, - )]); + let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { + local: 1usize.into(), + projection: List::empty(), + })]); let rvalue_set = self.successors_for_operand(state, args[0].node.clone()); initial_graph.extend(&lvalue_set, &rvalue_set); // Then, connect the argument tuple to each of the spread arguments. let spread_arg_operand = args[1].node.clone(); for i in 0..new_body.arg_count { - let lvalue_set = HashSet::from([MemLoc::new_stack_allocation( - instance, - Place { - local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. - projection: List::empty(), - }, - )]); + let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { + local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. + projection: List::empty(), + })]); // This conservatively assumes all arguments alias to all parameters. let rvalue_set = self.successors_for_operand(state, spread_arg_operand.clone()); initial_graph.extend(&lvalue_set, &rvalue_set); @@ -481,13 +478,10 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { } else { // Otherwise, simply connect all arguments to parameters. for (i, arg) in args.iter().enumerate() { - let lvalue_set = HashSet::from([MemLoc::new_stack_allocation( - instance, - Place { - local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. - projection: List::empty(), - }, - )]); + let lvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { + local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. + projection: List::empty(), + })]); let rvalue_set = self.successors_for_operand(state, arg.node.clone()); initial_graph.extend(&lvalue_set, &rvalue_set); } @@ -501,10 +495,10 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { // Connect the return value to the return destination. let lvalue_set = state.resolve_place(*destination, self.instance); - let rvalue_set = HashSet::from([MemLoc::new_stack_allocation( - instance, - Place { local: 0usize.into(), projection: List::empty() }, - )]); + let rvalue_set = HashSet::from([MemLoc::new_stack_allocation(instance, Place { + local: 0usize.into(), + projection: List::empty(), + })]); state.extend(&lvalue_set, &state.successors(&rvalue_set)); } diff --git a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs index 61804d0ff71a..4dd2fba62fb0 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_graph.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_graph.rs @@ -8,11 +8,11 @@ use rustc_middle::{ mir::{Location, Place, ProjectionElem}, ty::{Instance, List, TyCtxt}, }; -use rustc_mir_dataflow::{fmt::DebugWithContext, JoinSemiLattice}; +use rustc_mir_dataflow::{JoinSemiLattice, fmt::DebugWithContext}; use rustc_smir::rustc_internal; use stable_mir::mir::{ - mono::{Instance as StableInstance, StaticDef}, Place as StablePlace, + mono::{Instance as StableInstance, StaticDef}, }; use std::collections::{HashMap, HashSet, VecDeque}; diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index b808a5c5b8ee..6f2e779320f3 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -24,14 +24,14 @@ use rustc_data_structures::stable_hasher::{HashStable, StableHasher}; use rustc_middle::ty::{TyCtxt, VtblEntry}; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; +use stable_mir::CrateItem; use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef}; use stable_mir::mir::{ - visit::Location, Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator, - TerminatorKind, + Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator, TerminatorKind, + visit::Location, }; use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind}; -use stable_mir::CrateItem; use stable_mir::{CrateDef, ItemKind}; use std::fmt::{Display, Formatter}; use std::{ diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index d2b1fcd06471..d71f9710d404 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -14,13 +14,13 @@ use crate::kani_middle::stable_fn_def; use quote::ToTokens; use rustc_errors::ErrorGuaranteed; use rustc_hir::def::{DefKind, Res}; -use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE}; +use rustc_hir::def_id::{CRATE_DEF_INDEX, DefId, LOCAL_CRATE, LocalDefId, LocalModDefId}; use rustc_hir::{ItemKind, UseKind}; -use rustc_middle::ty::fast_reject::{self, TreatParams}; use rustc_middle::ty::TyCtxt; +use rustc_middle::ty::fast_reject::{self, TreatParams}; use rustc_smir::rustc_internal; -use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind}; use stable_mir::CrateDef; +use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind}; use std::collections::HashSet; use std::fmt; use std::iter::Peekable; diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs index 790019ab2998..9e594785a122 100644 --- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs +++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains code used for resolve type / trait names -use crate::kani_middle::resolve::{resolve_path, validate_kind, ResolveError}; +use crate::kani_middle::resolve::{ResolveError, resolve_path, validate_kind}; use quote::ToTokens; use rustc_hir::def::DefKind; use rustc_middle::ty::TyCtxt; diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index f145a4d105e2..4a48c649983c 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -14,9 +14,9 @@ use rustc_hir::def_id::DefId; use rustc_middle::mir::Const; use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable}; use rustc_smir::rustc_internal; +use stable_mir::mir::ConstOperand; use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, MirVisitor}; -use stable_mir::mir::ConstOperand; use stable_mir::ty::{FnDef, RigidTy, TyKind}; use stable_mir::{CrateDef, CrateItem}; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs index 35d0e7041704..dfd16594146f 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs @@ -10,11 +10,11 @@ use crate::{ }; use stable_mir::{ mir::{ + Body, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, Rvalue, + Statement, StatementKind, Terminator, TerminatorKind, alloc::GlobalAlloc, mono::{Instance, InstanceKind, StaticDef}, visit::Location, - Body, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, Rvalue, - Statement, StatementKind, Terminator, TerminatorKind, }, ty::{ConstantKind, RigidTy, TyKind}, }; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs index 41a2b69d1fdf..877ff41ea6d5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs @@ -9,16 +9,16 @@ use crate::kani_middle::{ transform::{ body::{InsertPosition, MutableBody, SourceInstruction}, check_uninit::{ - relevant_instruction::{InitRelevantInstruction, MemoryInitOp}, TargetFinder, + relevant_instruction::{InitRelevantInstruction, MemoryInitOp}, }, }, }; use rustc_middle::ty::TyCtxt; use stable_mir::mir::{ + MirVisitor, Operand, Place, Rvalue, Statement, Terminator, mono::Instance, visit::{Location, PlaceContext}, - MirVisitor, Operand, Place, Rvalue, Statement, Terminator, }; use std::collections::HashSet; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs index c31f72c9b5c3..b2a7ffd13bc1 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs @@ -8,11 +8,11 @@ use std::collections::HashSet; use crate::args::ExtraChecks; use crate::kani_middle::{ - points_to::{run_points_to_analysis, MemLoc, PointsToGraph}, + points_to::{MemLoc, PointsToGraph, run_points_to_analysis}, reachability::CallGraph, transform::{ - body::CheckType, check_uninit::UninitInstrumenter, BodyTransformation, GlobalPass, - TransformationResult, + BodyTransformation, GlobalPass, TransformationResult, body::CheckType, + check_uninit::UninitInstrumenter, }, }; use crate::kani_queries::QueryDb; @@ -22,8 +22,8 @@ use rustc_middle::ty::TyCtxt; use rustc_mir_dataflow::JoinSemiLattice; use rustc_session::config::OutputType; use stable_mir::{ - mir::mono::{Instance, MonoItem}, mir::MirVisitor, + mir::mono::{Instance, MonoItem}, ty::FnDef, }; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 726dc1965770..1ce21ef50669 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -12,12 +12,12 @@ use relevant_instruction::{InitRelevantInstruction, MemoryInitOp}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ + CrateDef, mir::{ - mono::Instance, AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, - Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, + AggregateKind, BasicBlock, Body, ConstOperand, Mutability, Operand, Place, Rvalue, + Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, mono::Instance, }, ty::{FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyConst, TyKind, UintTy}, - CrateDef, }; use std::collections::HashMap; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs index 37f1d94ed744..2408a3b50a6c 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs @@ -6,17 +6,17 @@ use crate::args::ExtraChecks; use crate::kani_middle::transform::{ - body::{CheckType, InsertPosition, MutableBody, SourceInstruction}, - check_uninit::{get_mem_init_fn_def, UninitInstrumenter}, TransformPass, TransformationType, + body::{CheckType, InsertPosition, MutableBody, SourceInstruction}, + check_uninit::{UninitInstrumenter, get_mem_init_fn_def}, }; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::{ - mir::{mono::Instance, Body, Mutability, Place}, - ty::{FnDef, GenericArgs, Ty}, CrateDef, + mir::{Body, Mutability, Place, mono::Instance}, + ty::{FnDef, GenericArgs, Ty}, }; use std::collections::HashMap; use std::fmt::Debug; diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index bd4356017b6b..20f4538453b5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -8,20 +8,20 @@ use crate::{ kani_middle::transform::{ body::{InsertPosition, MutableBody, SourceInstruction}, check_uninit::{ - relevant_instruction::{InitRelevantInstruction, MemoryInitOp}, - ty_layout::{tys_layout_compatible_to_size, LayoutComputationError}, PointeeInfo, TargetFinder, + relevant_instruction::{InitRelevantInstruction, MemoryInitOp}, + ty_layout::{LayoutComputationError, tys_layout_compatible_to_size}, }, }, }; use stable_mir::{ mir::{ - alloc::GlobalAlloc, - mono::{Instance, InstanceKind}, - visit::{Location, PlaceContext}, AggregateKind, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + alloc::GlobalAlloc, + mono::{Instance, InstanceKind}, + visit::{Location, PlaceContext}, }, ty::{AdtKind, ConstantKind, RigidTy, TyKind}, }; diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index a81f76d25393..d0fd553ef5cf 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -22,6 +22,7 @@ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::{Const, TyCtxt}; use rustc_smir::rustc_internal; +use stable_mir::CrateDef; use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, WrappingRange}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; @@ -32,7 +33,6 @@ use stable_mir::mir::{ }; use stable_mir::target::{MachineInfo, MachineSize}; use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Ty, TyKind, UintTy}; -use stable_mir::CrateDef; use std::fmt::Debug; use strum_macros::AsRefStr; use tracing::{debug, trace}; diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 71e06f5c49cd..480c480a0aea 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -12,12 +12,12 @@ use rustc_hir::def_id::DefId as InternalDefId; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use rustc_span::Symbol; +use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ Body, ConstOperand, Operand, Rvalue, Terminator, TerminatorKind, VarDebugInfoContents, }; use stable_mir::ty::{ClosureDef, FnDef, MirConst, RigidTy, TyKind, TypeAndMut, UintTy}; -use stable_mir::CrateDef; use std::collections::HashSet; use std::fmt::Debug; use tracing::{debug, trace}; @@ -420,10 +420,10 @@ impl FunctionWithContractPass { &mut mode_call, InsertPosition::Before, ); - new_body.replace_terminator( - &mode_call, - Terminator { kind: TerminatorKind::Goto { target }, span }, - ); + new_body.replace_terminator(&mode_call, Terminator { + kind: TerminatorKind::Goto { target }, + span, + }); new_body.into() } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 5a026db525a7..845916af5181 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -14,7 +14,7 @@ use crate::kani_middle::transform::body::{ }; use crate::kani_middle::transform::check_uninit::PointeeInfo; use crate::kani_middle::transform::check_uninit::{ - get_mem_init_fn_def, mk_layout_operand, resolve_mem_init_fn, PointeeLayout, + PointeeLayout, get_mem_init_fn_def, mk_layout_operand, resolve_mem_init_fn, }; use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_offset}; use crate::kani_middle::transform::{TransformPass, TransformationType}; @@ -22,8 +22,8 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - BasicBlock, BinOp, Body, ConstOperand, Mutability, Operand, Place, Rvalue, Statement, - StatementKind, Terminator, TerminatorKind, UnwindAction, RETURN_LOCAL, + BasicBlock, BinOp, Body, ConstOperand, Mutability, Operand, Place, RETURN_LOCAL, Rvalue, + Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, }; use stable_mir::target::MachineInfo; use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy}; diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 2d963cd1d6eb..7d97a49f287a 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -27,8 +27,8 @@ use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; use dump_mir_pass::DumpMirPass; use rustc_middle::ty::TyCtxt; -use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::mir::Body; +use stable_mir::mir::mono::{Instance, MonoItem}; use std::collections::HashMap; use std::fmt::Debug; @@ -79,22 +79,16 @@ impl BodyTransformation { // would also make sense to check that the values are initialized before checking their // validity. In the future, it would be nice to have a mechanism to skip automatically // generated code for future instrumentation passes. - transformer.add_pass( - queries, - UninitPass { - // Since this uses demonic non-determinism under the hood, should not assume the assertion. - check_type: CheckType::new_assert(tcx), - mem_init_fn_cache: HashMap::new(), - }, - ); - transformer.add_pass( - queries, - IntrinsicGeneratorPass { - check_type, - mem_init_fn_cache: HashMap::new(), - arguments: queries.args().clone(), - }, - ); + transformer.add_pass(queries, UninitPass { + // Since this uses demonic non-determinism under the hood, should not assume the assertion. + check_type: CheckType::new_assert(tcx), + mem_init_fn_cache: HashMap::new(), + }); + transformer.add_pass(queries, IntrinsicGeneratorPass { + check_type, + mem_init_fn_cache: HashMap::new(), + arguments: queries.args().clone(), + }); transformer } diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 3dbd667c3943..09d6e1fe8520 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -9,11 +9,11 @@ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; +use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, MirVisitor}; use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind}; use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; -use stable_mir::CrateDef; use std::collections::HashMap; use std::fmt::Debug; use tracing::{debug, trace}; diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index f5dd78ff86b0..d56877d11805 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -7,18 +7,18 @@ use crate::args::Arguments; use rustc_data_structures::sync::Lrc; use rustc_errors::emitter::Emitter; use rustc_errors::{ - emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter, ColorConfig, - DiagInner, + ColorConfig, DiagInner, emitter::HumanReadableErrorType, fallback_fluent_bundle, + json::JsonEmitter, }; -use rustc_session::config::ErrorOutputType; use rustc_session::EarlyDiagCtxt; +use rustc_session::config::ErrorOutputType; use rustc_span::source_map::FilePathMapping; use rustc_span::source_map::SourceMap; use std::io; use std::io::IsTerminal; use std::panic; use std::sync::LazyLock; -use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry}; +use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; use tracing_tree::HierarchicalLayer; /// Environment variable used to control this session log tracing. diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index c3cfc113af64..72de44e36014 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -15,7 +15,7 @@ use crate::args::cargo::CargoTargetArgs; use crate::util::warning; use cargo::CargoCommonArgs; use clap::builder::{PossibleValue, TypedValueParser}; -use clap::{error::ContextKind, error::ContextValue, error::Error, error::ErrorKind, ValueEnum}; +use clap::{ValueEnum, error::ContextKind, error::ContextValue, error::Error, error::ErrorKind}; use kani_metadata::CbmcSolver; use std::ffi::OsString; use std::path::PathBuf; diff --git a/kani-driver/src/args_toml.rs b/kani-driver/src/args_toml.rs index 37b38a425597..2fff01c4f5f9 100644 --- a/kani-driver/src/args_toml.rs +++ b/kani-driver/src/args_toml.rs @@ -1,14 +1,14 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{bail, Result}; +use anyhow::{Result, bail}; use clap::Parser; use std::collections::BTreeMap; use std::ffi::OsString; use std::path::PathBuf; use std::process::Command; -use toml::value::Table; use toml::Value; +use toml::value::Table; /// Produce the list of arguments to pass to ourself (cargo-kani). /// diff --git a/kani-driver/src/assess/metadata.rs b/kani-driver/src/assess/metadata.rs index d555f1e4d309..14018541d0e5 100644 --- a/kani-driver/src/assess/metadata.rs +++ b/kani-driver/src/assess/metadata.rs @@ -15,11 +15,11 @@ use std::path::Path; use anyhow::Result; use serde::{Deserialize, Serialize}; +use super::AssessArgs; use super::table_builder::TableBuilder; use super::table_failure_reasons::FailureReasonsTableRow; use super::table_promising_tests::PromisingTestsTableRow; use super::table_unsupported_features::UnsupportedFeaturesTableRow; -use super::AssessArgs; /// The structure of `.kani-assess-metadata.json` files. This is a the structure for both /// assess (standard) and scan. It it meant to hold results for one or more packages. diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs index f5b2ccb63035..4ee82e48389c 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use self::metadata::{write_metadata, AssessMetadata}; -use anyhow::{bail, Result}; +use self::metadata::{AssessMetadata, write_metadata}; +use anyhow::{Result, bail}; use kani_metadata::KaniMetadata; use crate::assess::table_builder::TableBuilder; diff --git a/kani-driver/src/assess/scan.rs b/kani-driver/src/assess/scan.rs index ef33f91eb522..7ce29bb64b33 100644 --- a/kani-driver/src/assess/scan.rs +++ b/kani-driver/src/assess/scan.rs @@ -9,8 +9,8 @@ use std::time::Instant; use anyhow::Result; use cargo_metadata::Package; -use crate::session::setup_cargo_command; use crate::session::KaniSession; +use crate::session::setup_cargo_command; use super::metadata::AssessMetadata; use super::metadata::{aggregate_metadata, read_metadata}; diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index ef289cead4c2..191b104a8c1c 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -2,11 +2,11 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::args::VerificationArgs; -use crate::call_single_file::{to_rustc_arg, LibConfig}; +use crate::call_single_file::{LibConfig, to_rustc_arg}; use crate::project::Artifact; -use crate::session::{lib_folder, lib_no_core_folder, setup_cargo_command, KaniSession}; +use crate::session::{KaniSession, lib_folder, lib_no_core_folder, setup_cargo_command}; use crate::util; -use anyhow::{bail, Context, Result}; +use anyhow::{Context, Result, bail}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{ Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, Target, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index bc4424aeb231..17e99bf17d0f 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -1,12 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{bail, Result}; +use anyhow::{Result, bail}; use kani_metadata::{CbmcSolver, HarnessMetadata}; use regex::Regex; use rustc_demangle::demangle; -use std::collections::btree_map::Entry; use std::collections::BTreeMap; +use std::collections::btree_map::Entry; use std::ffi::OsString; use std::fmt::Write; use std::path::Path; @@ -16,7 +16,7 @@ use std::time::{Duration, Instant}; use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ - extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput, + CheckStatus, Property, VerificationOutput, extract_results, process_cbmc_output, }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; use crate::coverage::cov_results::{CoverageCheck, CoverageResults}; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 868d1adce636..63ca71d5b8d1 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -7,7 +7,7 @@ use std::ffi::OsString; use std::path::{Path, PathBuf}; use std::process::Command; -use crate::session::{lib_folder, KaniSession}; +use crate::session::{KaniSession, lib_folder}; pub struct LibConfig { args: Vec, diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index a0202169863c..145e0c9c63aa 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -22,127 +22,97 @@ static CBMC_ALT_DESCRIPTIONS: Lazy = Lazy::new(|| { map.insert("error_label", vec![]); map.insert("division-by-zero", vec![("division by zero", None)]); map.insert("enum-range-check", vec![("enum range check", None)]); - map.insert( - "undefined-shift", - vec![ - ("shift distance is negative", None), - ("shift distance too large", None), - ("shift operand is negative", None), - ("shift of non-integer type", None), - ], - ); - map.insert( - "overflow", - vec![ - ("result of signed mod is not representable", None), - ("arithmetic overflow on signed type conversion", None), - ("arithmetic overflow on signed division", None), - ("arithmetic overflow on signed unary minus", None), - ("arithmetic overflow on signed shl", None), - ("arithmetic overflow on unsigned unary minus", None), - ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")), - ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")), - ( - "arithmetic overflow on signed *", - Some("arithmetic overflow on signed multiplication"), - ), - ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")), - ( - "arithmetic overflow on unsigned -", - Some("arithmetic overflow on unsigned subtraction"), - ), - ( - "arithmetic overflow on unsigned *", - Some("arithmetic overflow on unsigned multiplication"), - ), - ("arithmetic overflow on floating-point typecast", None), - ("arithmetic overflow on floating-point division", None), - ("arithmetic overflow on floating-point addition", None), - ("arithmetic overflow on floating-point subtraction", None), - ("arithmetic overflow on floating-point multiplication", None), - ("arithmetic overflow on unsigned to signed type conversion", None), - ("arithmetic overflow on float to signed integer type conversion", None), - ("arithmetic overflow on signed to unsigned type conversion", None), - ("arithmetic overflow on unsigned to unsigned type conversion", None), - ("arithmetic overflow on float to unsigned integer type conversion", None), - ], - ); - map.insert( - "NaN", - vec![ - ("NaN on +", Some("NaN on addition")), - ("NaN on -", Some("NaN on subtraction")), - ("NaN on /", Some("NaN on division")), - ("NaN on *", Some("NaN on multiplication")), - ], - ); + map.insert("undefined-shift", vec![ + ("shift distance is negative", None), + ("shift distance too large", None), + ("shift operand is negative", None), + ("shift of non-integer type", None), + ]); + map.insert("overflow", vec![ + ("result of signed mod is not representable", None), + ("arithmetic overflow on signed type conversion", None), + ("arithmetic overflow on signed division", None), + ("arithmetic overflow on signed unary minus", None), + ("arithmetic overflow on signed shl", None), + ("arithmetic overflow on unsigned unary minus", None), + ("arithmetic overflow on signed +", Some("arithmetic overflow on signed addition")), + ("arithmetic overflow on signed -", Some("arithmetic overflow on signed subtraction")), + ("arithmetic overflow on signed *", Some("arithmetic overflow on signed multiplication")), + ("arithmetic overflow on unsigned +", Some("arithmetic overflow on unsigned addition")), + ("arithmetic overflow on unsigned -", Some("arithmetic overflow on unsigned subtraction")), + ( + "arithmetic overflow on unsigned *", + Some("arithmetic overflow on unsigned multiplication"), + ), + ("arithmetic overflow on floating-point typecast", None), + ("arithmetic overflow on floating-point division", None), + ("arithmetic overflow on floating-point addition", None), + ("arithmetic overflow on floating-point subtraction", None), + ("arithmetic overflow on floating-point multiplication", None), + ("arithmetic overflow on unsigned to signed type conversion", None), + ("arithmetic overflow on float to signed integer type conversion", None), + ("arithmetic overflow on signed to unsigned type conversion", None), + ("arithmetic overflow on unsigned to unsigned type conversion", None), + ("arithmetic overflow on float to unsigned integer type conversion", None), + ]); + map.insert("NaN", vec![ + ("NaN on +", Some("NaN on addition")), + ("NaN on -", Some("NaN on subtraction")), + ("NaN on /", Some("NaN on division")), + ("NaN on *", Some("NaN on multiplication")), + ]); map.insert("pointer", vec![("same object violation", None)]); - map.insert( - "pointer_arithmetic", - vec![ - ("pointer relation: deallocated dynamic object", None), - ("pointer relation: dead object", None), - ("pointer relation: pointer NULL", None), - ("pointer relation: pointer invalid", None), - ("pointer relation: pointer outside dynamic object bounds", None), - ("pointer relation: pointer outside object bounds", None), - ("pointer relation: invalid integer address", None), - ("pointer arithmetic: deallocated dynamic object", None), - ("pointer arithmetic: dead object", None), - ("pointer arithmetic: pointer NULL", None), - ("pointer arithmetic: pointer invalid", None), - ("pointer arithmetic: pointer outside dynamic object bounds", None), - ("pointer arithmetic: pointer outside object bounds", None), - ("pointer arithmetic: invalid integer address", None), - ], - ); - map.insert( - "pointer_dereference", - vec![ - ( - "dereferenced function pointer must be", - Some("dereference failure: invalid function pointer"), - ), - ("dereference failure: pointer NULL", None), - ("dereference failure: pointer invalid", None), - ("dereference failure: deallocated dynamic object", None), - ("dereference failure: dead object", None), - ("dereference failure: pointer outside dynamic object bounds", None), - ("dereference failure: pointer outside object bounds", None), - ("dereference failure: invalid integer address", None), - ], - ); + map.insert("pointer_arithmetic", vec![ + ("pointer relation: deallocated dynamic object", None), + ("pointer relation: dead object", None), + ("pointer relation: pointer NULL", None), + ("pointer relation: pointer invalid", None), + ("pointer relation: pointer outside dynamic object bounds", None), + ("pointer relation: pointer outside object bounds", None), + ("pointer relation: invalid integer address", None), + ("pointer arithmetic: deallocated dynamic object", None), + ("pointer arithmetic: dead object", None), + ("pointer arithmetic: pointer NULL", None), + ("pointer arithmetic: pointer invalid", None), + ("pointer arithmetic: pointer outside dynamic object bounds", None), + ("pointer arithmetic: pointer outside object bounds", None), + ("pointer arithmetic: invalid integer address", None), + ]); + map.insert("pointer_dereference", vec![ + ( + "dereferenced function pointer must be", + Some("dereference failure: invalid function pointer"), + ), + ("dereference failure: pointer NULL", None), + ("dereference failure: pointer invalid", None), + ("dereference failure: deallocated dynamic object", None), + ("dereference failure: dead object", None), + ("dereference failure: pointer outside dynamic object bounds", None), + ("dereference failure: pointer outside object bounds", None), + ("dereference failure: invalid integer address", None), + ]); // These are very hard to understand without more context. - map.insert( - "pointer_primitives", - vec![ - ("pointer invalid", None), - ("deallocated dynamic object", Some("pointer to deallocated dynamic object")), - ("dead object", Some("pointer to dead object")), - ("pointer outside dynamic object bounds", None), - ("pointer outside object bounds", None), - ("invalid integer address", None), - ], - ); - map.insert( - "array_bounds", - vec![ - ("lower bound", Some("index out of bounds")), - // This one is redundant: - // ("dynamic object upper bound", Some("access out of bounds")), - ( - "upper bound", - Some("index out of bounds: the length is less than or equal to the given index"), - ), - ], - ); - map.insert( - "bit_count", - vec![ - ("count trailing zeros is undefined for value zero", None), - ("count leading zeros is undefined for value zero", None), - ], - ); + map.insert("pointer_primitives", vec![ + ("pointer invalid", None), + ("deallocated dynamic object", Some("pointer to deallocated dynamic object")), + ("dead object", Some("pointer to dead object")), + ("pointer outside dynamic object bounds", None), + ("pointer outside object bounds", None), + ("invalid integer address", None), + ]); + map.insert("array_bounds", vec![ + ("lower bound", Some("index out of bounds")), + // This one is redundant: + // ("dynamic object upper bound", Some("access out of bounds")), + ( + "upper bound", + Some("index out of bounds: the length is less than or equal to the given index"), + ), + ]); + map.insert("bit_count", vec![ + ("count trailing zeros is undefined for value zero", None), + ("count leading zeros is undefined for value zero", None), + ]); map.insert("memory-leak", vec![("dynamically allocated memory never freed", None)]); // These pre-conditions should not print temporary variables since they are embedded in the libc implementation. // They are added via `__CPROVER_precondition`. diff --git a/kani-driver/src/concrete_playback/playback.rs b/kani-driver/src/concrete_playback/playback.rs index c56694ad32fd..833fdbc02384 100644 --- a/kani-driver/src/concrete_playback/playback.rs +++ b/kani-driver/src/concrete_playback/playback.rs @@ -6,8 +6,8 @@ use crate::args::common::Verbosity; use crate::args::playback_args::{CargoPlaybackArgs, KaniPlaybackArgs, MessageFormat}; use crate::call_cargo::cargo_config_args; -use crate::call_single_file::{base_rustc_flags, LibConfig}; -use crate::session::{lib_playback_folder, setup_cargo_command, InstallType}; +use crate::call_single_file::{LibConfig, base_rustc_flags}; +use crate::session::{InstallType, lib_playback_folder, setup_cargo_command}; use crate::{session, util}; use anyhow::Result; use std::ffi::OsString; diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 5faa6299a5d3..5c4076f13591 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -9,11 +9,11 @@ use crate::call_cbmc::VerificationResult; use crate::cbmc_output_parser::Property; use crate::session::KaniSession; use anyhow::{Context, Result}; -use concrete_vals_extractor::{extract_harness_values, ConcreteVal}; +use concrete_vals_extractor::{ConcreteVal, extract_harness_values}; use kani_metadata::{HarnessKind, HarnessMetadata}; use std::collections::hash_map::DefaultHasher; use std::ffi::OsString; -use std::fs::{read_to_string, File}; +use std::fs::{File, read_to_string}; use std::hash::{Hash, Hasher}; use std::io::{BufRead, BufReader, Write}; use std::path::Path; @@ -500,10 +500,11 @@ mod tests { /// Check that the generated unit tests have the right formatting and indentation #[test] fn format_two_concrete_vals() { - let concrete_vals = [ - ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, - ConcreteVal { byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], interp_val: "0l".to_string() }, - ]; + let concrete_vals = + [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }, ConcreteVal { + byte_arr: vec![0, 0, 0, 0, 0, 0, 0, 0], + interp_val: "0l".to_string(), + }]; let actual: Vec<_> = format_concrete_vals(&concrete_vals).collect(); let expected = vec![ format!("{:<8}// 0", " "), @@ -597,10 +598,11 @@ mod tests { #[test] fn check_rustfmt_args_some_line_ranges() { - let file_line_ranges = [ - FileLineRange { file: "file1".to_string(), line_range: None }, - FileLineRange { file: "path/to/file2".to_string(), line_range: Some((1, 3)) }, - ]; + let file_line_ranges = + [FileLineRange { file: "file1".to_string(), line_range: None }, FileLineRange { + file: "path/to/file2".to_string(), + line_range: Some((1, 3)), + }]; let args = rustfmt_args(&file_line_ranges); let expected: Vec = [ "--unstable-features", diff --git a/kani-driver/src/coverage/cov_session.rs b/kani-driver/src/coverage/cov_session.rs index bf6b34d3cd0b..60fa2f1c242f 100644 --- a/kani-driver/src/coverage/cov_session.rs +++ b/kani-driver/src/coverage/cov_session.rs @@ -5,10 +5,10 @@ use std::fs; use std::fs::File; use std::io::Write; +use crate::KaniSession; use crate::harness_runner::HarnessResult; use crate::project::Project; -use crate::KaniSession; -use anyhow::{bail, Result}; +use anyhow::{Result, bail}; impl KaniSession { /// Saves metadata required for coverage-related features. diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 7e432932ab29..5a77a6a125a3 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{bail, Result}; +use anyhow::{Result, bail}; use kani_metadata::{ArtifactType, HarnessMetadata}; use rayon::prelude::*; use std::path::Path; diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index d3bd697d2ea4..e8ede555f180 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -5,9 +5,9 @@ use std::ffi::OsString; use std::process::ExitCode; use anyhow::Result; -use time::{format_description, OffsetDateTime}; +use time::{OffsetDateTime, format_description}; -use args::{check_is_valid, CargoKaniSubcommand}; +use args::{CargoKaniSubcommand, check_is_valid}; use args_toml::join_args; use crate::args::StandaloneSubcommand; diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 3f9cd8f2bf84..625d8b4bbcaa 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::{bail, Result}; +use anyhow::{Result, bail}; use std::path::Path; use tracing::{debug, trace}; diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index e0d2d2edd139..363050958d61 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -9,7 +9,7 @@ use crate::session::KaniSession; use crate::util::crate_name; use anyhow::{Context, Result}; use kani_metadata::{ - artifact::convert_type, ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, + ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, artifact::convert_type, }; use std::env::current_dir; use std::fs; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 03cfb108e324..2df431eb4587 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -1,10 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::args::common::Verbosity; use crate::args::VerificationArgs; +use crate::args::common::Verbosity; use crate::util::render_command; -use anyhow::{bail, Context, Result}; +use anyhow::{Context, Result, bail}; use std::io::IsTerminal; use std::io::Write; use std::path::{Path, PathBuf}; @@ -13,7 +13,7 @@ use std::sync::Mutex; use std::time::Instant; use strum_macros::Display; use tracing::level_filters::LevelFilter; -use tracing_subscriber::{layer::SubscriberExt, EnvFilter, Registry}; +use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; /// Environment variable used to control this session log tracing. /// This is the same variable used to control `kani-compiler` logs. Note that you can still control diff --git a/kani_metadata/src/artifact.rs b/kani_metadata/src/artifact.rs index 078cad14f679..12f8f9a49566 100644 --- a/kani_metadata/src/artifact.rs +++ b/kani_metadata/src/artifact.rs @@ -94,7 +94,7 @@ impl Deref for ArtifactType { #[cfg(test)] mod test { - use super::{convert_type, ArtifactType::*}; + use super::{ArtifactType::*, convert_type}; use std::path::PathBuf; #[test] diff --git a/library/kani/src/futures.rs b/library/kani/src/futures.rs index 637f24a80f6a..37cab17b0a5b 100644 --- a/library/kani/src/futures.rs +++ b/library/kani/src/futures.rs @@ -163,6 +163,7 @@ pub struct JoinHandle { index: usize, } +#[allow(static_mut_refs)] impl Future for JoinHandle { type Output = (); @@ -180,6 +181,7 @@ impl Future for JoinHandle { /// /// This function can only be called inside a future passed to [`block_on_with_spawn`]. #[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")] +#[allow(static_mut_refs)] pub fn spawn + Sync + 'static>(fut: F) -> JoinHandle { unsafe { if let Some(executor) = GLOBAL_EXECUTOR.as_mut() { @@ -195,6 +197,7 @@ pub fn spawn + Sync + 'static>(fut: F) -> JoinHandle { /// /// Contrary to [`block_on`], this allows `spawn`ing other futures #[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")] +#[allow(static_mut_refs)] pub fn block_on_with_spawn + Sync + 'static>( fut: F, scheduling_plan: impl SchedulingStrategy, diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index c3e9ae5497cc..053af760067b 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -44,7 +44,7 @@ pub fn concrete_playback_run(_: Vec>, _: F) { unreachable!("Concrete playback does not work during verification") } -pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; +pub use futures::{RoundRobin, block_on, block_on_with_spawn, spawn, yield_now}; // Kani proc macros must be in a separate crate pub use kani_macros::*; diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs index a3ec05a9c953..d9da65aa4537 100644 --- a/library/kani/src/vec.rs +++ b/library/kani/src/vec.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::{any, any_where, Arbitrary}; +use crate::{Arbitrary, any, any_where}; /// Generates an arbitrary vector whose length is at most MAX_LENGTH. pub fn any_vec() -> Vec diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index e89f6f089795..04b288069387 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -9,13 +9,13 @@ //! struct S; //! //! ``` -use proc_macro2::{Ident, Span, TokenStream}; use proc_macro_error2::abort; +use proc_macro2::{Ident, Span, TokenStream}; use quote::{quote, quote_spanned}; use syn::spanned::Spanned; use syn::{ - parse_macro_input, parse_quote, Data, DataEnum, DeriveInput, Fields, GenericParam, Generics, - Index, + Data, DataEnum, DeriveInput, Fields, GenericParam, Generics, Index, parse_macro_input, + parse_quote, }; pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream { diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 8a1d2d80f864..3e6c9d018422 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -409,7 +409,7 @@ mod sysroot { use { quote::{format_ident, quote}, syn::parse::{Parse, ParseStream}, - syn::{parse_macro_input, ItemFn}, + syn::{ItemFn, parse_macro_input}, }; /// Annotate the harness with a #[kanitool::] with optional arguments. diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 8ad21e8a9c6b..5a9e12a62ae2 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -8,7 +8,7 @@ use proc_macro2::{Ident, Span, TokenStream}; use quote::quote; use syn::{Expr, ItemFn, Stmt}; -use super::{helpers::*, ContractConditionsHandler, INTERNAL_RESULT_IDENT}; +use super::{ContractConditionsHandler, INTERNAL_RESULT_IDENT, helpers::*}; impl<'a> ContractConditionsHandler<'a> { /// Generate initial contract. diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 314a5e74bc98..863cf882f063 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -6,11 +6,11 @@ use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; use std::mem; -use syn::{parse_quote, Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt}; +use syn::{Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt, parse_quote}; use super::{ - helpers::*, shared::build_ensures, ClosureType, ContractConditionsData, - ContractConditionsHandler, INTERNAL_RESULT_IDENT, + ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, + helpers::*, shared::build_ensures, }; const WRAPPER_ARG: &str = "_wrapper_arg"; diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 8db6218e2693..49d101dad32a 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -9,8 +9,8 @@ use proc_macro2::{Ident, Span}; use std::borrow::Cow; use syn::spanned::Spanned; use syn::{ - parse_quote, Attribute, Expr, ExprBlock, ExprCall, ExprPath, Local, LocalInit, PatIdent, Path, - Stmt, + Attribute, Expr, ExprBlock, ExprCall, ExprPath, Local, LocalInit, PatIdent, Path, Stmt, + parse_quote, }; /// If an explicit return type was provided it is returned, otherwise `()`. diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index 50c63173b601..bd06139b27f5 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -8,9 +8,9 @@ use proc_macro2::TokenStream as TokenStream2; use syn::ItemFn; use super::{ - helpers::{chunks_by, is_token_stream_2_comma, matches_path}, ContractConditionsData, ContractConditionsHandler, ContractConditionsType, ContractFunctionState, + helpers::{chunks_by, is_token_stream_2_comma, matches_path}, }; impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 281960bf041b..41be536ffb6d 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -395,7 +395,7 @@ use proc_macro::TokenStream; use proc_macro2::{Ident, TokenStream as TokenStream2}; use quote::quote; -use syn::{parse_macro_input, parse_quote, Expr, ExprClosure, ItemFn}; +use syn::{Expr, ExprClosure, ItemFn, parse_macro_input, parse_quote}; mod bootstrap; mod check; diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 71913e630622..b28e178bea6d 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -9,9 +9,9 @@ use std::mem; use syn::Stmt; use super::{ + ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, helpers::*, shared::{build_ensures, try_as_result_assign}, - ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, }; impl<'a> ContractConditionsHandler<'a> { diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index f189a9f98b0c..d7e77ee2a8d4 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -12,7 +12,7 @@ use std::collections::HashMap; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; use std::hash::{DefaultHasher, Hash, Hasher}; -use syn::{spanned::Spanned, visit_mut::VisitMut, Expr, ExprCall, ExprClosure, ExprPath, Path}; +use syn::{Expr, ExprCall, ExprClosure, ExprPath, Path, spanned::Spanned, visit_mut::VisitMut}; use super::INTERNAL_RESULT_IDENT; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 7cd260ede123..28cedff1d1de 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-09-17" +channel = "nightly-2024-09-23" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/rustfmt.toml b/rustfmt.toml index 95988ef7f52a..44cbfe4a3dc9 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -3,7 +3,7 @@ # Run rustfmt with this config (it should be picked up automatically). edition = "2021" -version = "Two" +style_edition = "2024" use_small_heuristics = "Max" merge_derives = false diff --git a/src/cmd.rs b/src/cmd.rs index 77204f092e74..1ab9216a4d46 100644 --- a/src/cmd.rs +++ b/src/cmd.rs @@ -7,7 +7,7 @@ use std::ffi::OsString; use std::process::Command; -use anyhow::{bail, Context, Result}; +use anyhow::{Context, Result, bail}; /// Helper trait to fallibly run commands pub trait AutoRun { diff --git a/src/lib.rs b/src/lib.rs index 0015829f61d3..f24163d3213c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -22,7 +22,7 @@ use std::path::{Path, PathBuf}; use std::process::Command; use std::{env, fs}; -use anyhow::{bail, Context, Result}; +use anyhow::{Context, Result, bail}; /// Effectively the entry point (i.e. `main` function) for both our proxy binaries. /// `bin` should be either `kani` or `cargo-kani` diff --git a/src/os_hacks.rs b/src/os_hacks.rs index ca064a662901..8d3a20575d7d 100644 --- a/src/os_hacks.rs +++ b/src/os_hacks.rs @@ -8,7 +8,7 @@ use std::path::Path; use std::process::Command; -use anyhow::{bail, Context, Result}; +use anyhow::{Context, Result, bail}; use os_info::Info; use crate::cmd::AutoRun; diff --git a/src/setup.rs b/src/setup.rs index 58387f7031b7..eb1227269ccc 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -8,7 +8,7 @@ use std::ffi::OsString; use std::path::{Path, PathBuf}; use std::process::Command; -use anyhow::{bail, Context, Result}; +use anyhow::{Context, Result, bail}; use crate::cmd::AutoRun; use crate::os_hacks; diff --git a/tests/cargo-kani/percent-encoding/src/lib.rs b/tests/cargo-kani/percent-encoding/src/lib.rs index 8da898139aa8..e9667b7cb375 100644 --- a/tests/cargo-kani/percent-encoding/src/lib.rs +++ b/tests/cargo-kani/percent-encoding/src/lib.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use percent_encoding::{utf8_percent_encode, NON_ALPHANUMERIC}; +use percent_encoding::{NON_ALPHANUMERIC, utf8_percent_encode}; #[kani::proof] pub fn check_encoding() { diff --git a/tests/cargo-kani/small-vec/src/lib.rs b/tests/cargo-kani/small-vec/src/lib.rs index 45b07a345285..dbf9d7f9065c 100644 --- a/tests/cargo-kani/small-vec/src/lib.rs +++ b/tests/cargo-kani/small-vec/src/lib.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use smallvec::{smallvec, SmallVec}; +use smallvec::{SmallVec, smallvec}; #[kani::proof] #[kani::unwind(4)] diff --git a/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs b/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs index 34d29bb3423d..bac3b9b1390c 100644 --- a/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs +++ b/tests/cargo-kani/stubbing-use-as-foreign/src/lib.rs @@ -5,9 +5,9 @@ //! YYY;`) referring to external code when resolving paths in `kani::stub` //! attributes. +use other_crate::MyType as MyFavoriteType; use other_crate::inner_mod::magic_number42 as forty_two; use other_crate::magic_number13 as thirteen; -use other_crate::MyType as MyFavoriteType; #[kani::proof] #[kani::stub(zero, thirteen)] diff --git a/tests/cargo-kani/stubbing-use-foreign/src/lib.rs b/tests/cargo-kani/stubbing-use-foreign/src/lib.rs index 07e86207a944..def0ce5a73eb 100644 --- a/tests/cargo-kani/stubbing-use-foreign/src/lib.rs +++ b/tests/cargo-kani/stubbing-use-foreign/src/lib.rs @@ -4,9 +4,9 @@ //! This tests whether we take into account use statements (`use XXX;`) //! referring to external code when resolving paths in `kani::stub` attributes. +use other_crate::MyType; use other_crate::inner_mod::magic_number42; use other_crate::magic_number13; -use other_crate::MyType; #[kani::proof] #[kani::stub(zero, magic_number13)] diff --git a/tests/cargo-kani/vecdeque-cve/src/harness.rs b/tests/cargo-kani/vecdeque-cve/src/harness.rs index 5c36450ee36a..f8ec8f5fdbde 100644 --- a/tests/cargo-kani/vecdeque-cve/src/harness.rs +++ b/tests/cargo-kani/vecdeque-cve/src/harness.rs @@ -27,8 +27,8 @@ const MAX_CAPACITY: usize = usize::MAX >> 2; /// This module uses a version of VecDeque that includes the CVE fix. mod fixed_proofs { - use crate::fixed::VecDeque; use crate::MAX_CAPACITY; + use crate::fixed::VecDeque; /// Minimal example that we no longer expect to fail #[kani::proof] @@ -98,8 +98,8 @@ mod fixed_proofs { mod cve_proofs { // Modified version of vec_deque with reserve issue. - use crate::cve::VecDeque; use crate::MAX_CAPACITY; + use crate::cve::VecDeque; /// Minimal example that we expect to fail #[kani::proof] diff --git a/tests/expected/dealloc/stack/test.rs b/tests/expected/dealloc/stack/test.rs index 87da636d8916..a4b1e3f481e3 100644 --- a/tests/expected/dealloc/stack/test.rs +++ b/tests/expected/dealloc/stack/test.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::alloc::{dealloc, Layout}; +use std::alloc::{Layout, dealloc}; // This test checks that Kani flags the deallocation of a stack-allocated // variable diff --git a/tests/expected/realloc/null/main.rs b/tests/expected/realloc/null/main.rs index 668ad4f84c2f..6f5a3b8bd2ab 100644 --- a/tests/expected/realloc/null/main.rs +++ b/tests/expected/realloc/null/main.rs @@ -3,7 +3,7 @@ // Calling realloc with a null pointer fails -use std::alloc::{realloc, Layout}; +use std::alloc::{Layout, realloc}; #[kani::proof] fn main() { diff --git a/tests/expected/realloc/shrink/main.rs b/tests/expected/realloc/shrink/main.rs index 7c4bd377fea7..d7b31244a9f7 100644 --- a/tests/expected/realloc/shrink/main.rs +++ b/tests/expected/realloc/shrink/main.rs @@ -4,7 +4,7 @@ // Use realloc to shrink the size of the allocated block and make sure // out-of-bound accesses result in verification failure -use std::alloc::{alloc, dealloc, realloc, Layout}; +use std::alloc::{Layout, alloc, dealloc, realloc}; #[kani::proof] fn main() { diff --git a/tests/expected/realloc/zero_size/main.rs b/tests/expected/realloc/zero_size/main.rs index 3e347af7512f..620ce17fdd2d 100644 --- a/tests/expected/realloc/zero_size/main.rs +++ b/tests/expected/realloc/zero_size/main.rs @@ -3,7 +3,7 @@ // Calling realloc with a size of zero fails -use std::alloc::{alloc, realloc, Layout}; +use std::alloc::{Layout, alloc, realloc}; #[kani::proof] fn main() { diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs index 8a9536e5a8e8..046d0f9f551f 100644 --- a/tests/expected/shadow/uninit_array/test.rs +++ b/tests/expected/shadow/uninit_array/test.rs @@ -6,7 +6,7 @@ // It checks that shadow memory can be used to track whether a memory location // is initialized. -use std::alloc::{alloc, dealloc, Layout}; +use std::alloc::{Layout, alloc, dealloc}; static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new(false); diff --git a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs index 318f234c31be..d4e4c4b758da 100644 --- a/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs +++ b/tests/expected/uninit/alloc-to-slice/alloc-to-slice.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z uninit-checks -use std::alloc::{alloc, Layout}; +use std::alloc::{Layout, alloc}; use std::slice::from_raw_parts; /// Checks that Kani catches an attempt to form a slice from uninitialized memory. diff --git a/tests/expected/uninit/atomic/atomic.rs b/tests/expected/uninit/atomic/atomic.rs index 63c85af41a3f..78b9dd2fdea0 100644 --- a/tests/expected/uninit/atomic/atomic.rs +++ b/tests/expected/uninit/atomic/atomic.rs @@ -4,7 +4,7 @@ #![feature(core_intrinsics)] -use std::alloc::{alloc, Layout}; +use std::alloc::{Layout, alloc}; use std::sync::atomic::{AtomicU8, Ordering}; // Checks if memory initialization checks correctly fail when uninitialized memory is passed to diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs index b023853b2fbc..33d5e72b1da9 100644 --- a/tests/expected/uninit/intrinsics/intrinsics.rs +++ b/tests/expected/uninit/intrinsics/intrinsics.rs @@ -5,7 +5,7 @@ #![feature(core_intrinsics)] -use std::alloc::{alloc, alloc_zeroed, Layout}; +use std::alloc::{Layout, alloc, alloc_zeroed}; use std::intrinsics::*; #[kani::proof] diff --git a/tests/kani/AsyncAwait/spawn.rs b/tests/kani/AsyncAwait/spawn.rs index 76583f10d615..fa203b2a5c12 100644 --- a/tests/kani/AsyncAwait/spawn.rs +++ b/tests/kani/AsyncAwait/spawn.rs @@ -7,8 +7,8 @@ //! This file tests the executor and spawn infrastructure from the Kani library. use std::sync::{ - atomic::{AtomicI64, Ordering}, Arc, + atomic::{AtomicI64, Ordering}, }; #[kani::proof(schedule = kani::RoundRobin::default())] diff --git a/tests/kani/Coroutines/issue-1593.rs b/tests/kani/Coroutines/issue-1593.rs index 9028dadad3d3..b85aefba9378 100644 --- a/tests/kani/Coroutines/issue-1593.rs +++ b/tests/kani/Coroutines/issue-1593.rs @@ -8,8 +8,8 @@ // in the context of vtables. use std::sync::{ - atomic::{AtomicI64, Ordering}, Arc, + atomic::{AtomicI64, Ordering}, }; #[kani::proof] diff --git a/tests/kani/FatPointers/boxmuttrait.rs b/tests/kani/FatPointers/boxmuttrait.rs index aa965f56c71e..a9469d7273f1 100644 --- a/tests/kani/FatPointers/boxmuttrait.rs +++ b/tests/kani/FatPointers/boxmuttrait.rs @@ -9,7 +9,7 @@ #![feature(ptr_metadata)] use std::any::Any; -use std::io::{sink, Write}; +use std::io::{Write, sink}; use std::ptr::DynMetadata; include!("../Helpers/vtable_utils_ignore.rs"); diff --git a/tests/kani/FatPointers/boxmuttrait_fail.rs b/tests/kani/FatPointers/boxmuttrait_fail.rs index 4d4dc6fc8384..35d05a58c6f8 100644 --- a/tests/kani/FatPointers/boxmuttrait_fail.rs +++ b/tests/kani/FatPointers/boxmuttrait_fail.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-verify-fail -use std::io::{sink, Write}; +use std::io::{Write, sink}; #[kani::proof] fn main() { diff --git a/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs b/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs index a119364f9b42..6ea70ab3b830 100644 --- a/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs +++ b/tests/kani/Intrinsics/Atomic/Stable/Fence/main.rs @@ -4,7 +4,7 @@ // Check that `atomic_fence` and other variants (stable version) can be // processed. -use std::sync::atomic::{fence, Ordering}; +use std::sync::atomic::{Ordering, fence}; #[kani::proof] fn main() { diff --git a/tests/kani/Intrinsics/RawEq/uninit_eq.rs b/tests/kani/Intrinsics/RawEq/uninit_eq.rs index 9e7f81dfaef1..390e0f774a4a 100644 --- a/tests/kani/Intrinsics/RawEq/uninit_eq.rs +++ b/tests/kani/Intrinsics/RawEq/uninit_eq.rs @@ -6,7 +6,7 @@ // uninitialized #![feature(core_intrinsics)] use std::intrinsics::raw_eq; -use std::mem::{zeroed, MaybeUninit}; +use std::mem::{MaybeUninit, zeroed}; #[kani::proof] fn main() { diff --git a/tests/kani/Intrinsics/RawEq/uninit_ne.rs b/tests/kani/Intrinsics/RawEq/uninit_ne.rs index 0f0642976671..73b5715b4846 100644 --- a/tests/kani/Intrinsics/RawEq/uninit_ne.rs +++ b/tests/kani/Intrinsics/RawEq/uninit_ne.rs @@ -6,7 +6,7 @@ // is uninitialized #![feature(core_intrinsics)] use std::intrinsics::raw_eq; -use std::mem::{zeroed, MaybeUninit}; +use std::mem::{MaybeUninit, zeroed}; #[kani::proof] fn main() { diff --git a/tests/kani/Realloc/two_reallocs.rs b/tests/kani/Realloc/two_reallocs.rs index 449e00cce56d..dc7b5ec3cd87 100644 --- a/tests/kani/Realloc/two_reallocs.rs +++ b/tests/kani/Realloc/two_reallocs.rs @@ -3,7 +3,7 @@ // Perform two reallocs in a row and make sure the data is properly copied -use std::alloc::{alloc, dealloc, realloc, Layout}; +use std::alloc::{Layout, alloc, dealloc, realloc}; #[kani::proof] fn main() { diff --git a/tests/kani/Stubbing/resolve_use.rs b/tests/kani/Stubbing/resolve_use.rs index ac1f6f7325f8..20c5faddfdc6 100644 --- a/tests/kani/Stubbing/resolve_use.rs +++ b/tests/kani/Stubbing/resolve_use.rs @@ -20,8 +20,8 @@ impl MyType { mod my_mod { use self::inner_mod::magic_number42; - use super::magic_number13; use super::MyType; + use super::magic_number13; mod inner_mod { pub fn magic_number42() -> u32 { diff --git a/tests/kani/Stubbing/resolve_use_as.rs b/tests/kani/Stubbing/resolve_use_as.rs index 790e26e575e9..5f55b8f7ac59 100644 --- a/tests/kani/Stubbing/resolve_use_as.rs +++ b/tests/kani/Stubbing/resolve_use_as.rs @@ -20,8 +20,8 @@ impl MyType { mod my_mod { use self::inner_mod::magic_number42 as forty_two; - use super::magic_number13 as thirteen; use super::MyType as MyFavoriteType; + use super::magic_number13 as thirteen; mod inner_mod { pub fn magic_number42() -> u32 { diff --git a/tests/kani/Uninit/alloc-to-slice.rs b/tests/kani/Uninit/alloc-to-slice.rs index 863d3b40b390..6f235fa41b51 100644 --- a/tests/kani/Uninit/alloc-to-slice.rs +++ b/tests/kani/Uninit/alloc-to-slice.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z uninit-checks -use std::alloc::{alloc, Layout}; +use std::alloc::{Layout, alloc}; #[kani::proof] fn alloc_to_slice() { diff --git a/tests/kani/Uninit/alloc-zeroed-to-slice.rs b/tests/kani/Uninit/alloc-zeroed-to-slice.rs index d00ca4c6abff..1e463b3227a0 100644 --- a/tests/kani/Uninit/alloc-zeroed-to-slice.rs +++ b/tests/kani/Uninit/alloc-zeroed-to-slice.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z uninit-checks -use std::alloc::{alloc_zeroed, Layout}; +use std::alloc::{Layout, alloc_zeroed}; use std::slice::from_raw_parts; #[kani::proof] diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs index e2f1fc16666a..c9a3c01f93de 100644 --- a/tests/perf/hashset/src/lib.rs +++ b/tests/perf/hashset/src/lib.rs @@ -3,7 +3,7 @@ // kani-flags: -Z stubbing //! Try to verify HashSet basic behavior. -use std::collections::{hash_map::RandomState, HashSet}; +use std::collections::{HashSet, hash_map::RandomState}; use std::mem::{size_of, size_of_val, transmute}; #[allow(dead_code)] diff --git a/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs index 891a97fd8c22..008e7d132f10 100644 --- a/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs +++ b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Z uninit-checks -use std::alloc::{alloc_zeroed, Layout}; +use std::alloc::{Layout, alloc_zeroed}; use std::slice::from_raw_parts; #[kani::proof] diff --git a/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs b/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs index 16b87cfadf5a..d013af942b9b 100644 --- a/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs +++ b/tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs @@ -9,7 +9,7 @@ #![warn(rust_2018_idioms)] #![cfg(feature = "full")] -use tokio::io::{duplex, AsyncReadExt, AsyncWriteExt}; +use tokio::io::{AsyncReadExt, AsyncWriteExt, duplex}; #[cfg(disabled)] // because it timed out after 2h #[kani::proof] diff --git a/tests/slow/tokio-proofs/src/tokio/support/panic.rs b/tests/slow/tokio-proofs/src/tokio/support/panic.rs index 12ae92a521e4..b35fde0ecdd7 100644 --- a/tests/slow/tokio-proofs/src/tokio/support/panic.rs +++ b/tests/slow/tokio-proofs/src/tokio/support/panic.rs @@ -6,7 +6,7 @@ // Original copyright tokio contributors. // origin: tokio/tests/support -use parking_lot::{const_mutex, Mutex}; +use parking_lot::{Mutex, const_mutex}; use std::panic; use std::sync::Arc; diff --git a/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs b/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs index 39cb46077626..72c4d486daf8 100644 --- a/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs +++ b/tests/slow/tokio-proofs/src/tokio_stream/stream_stream_map.rs @@ -7,7 +7,7 @@ // origin: tokio-stream/tests/ at commit b2ada60e701d5c9e6644cf8fc42a100774f8e23f use crate::tokio_stream::support::mpsc; -use tokio_stream::{self as stream, pending, Stream, StreamExt, StreamMap}; +use tokio_stream::{self as stream, Stream, StreamExt, StreamMap, pending}; use tokio_test::{assert_ok, assert_pending, assert_ready, task}; use std::pin::Pin; diff --git a/tests/slow/tokio-proofs/src/tokio_test/block_on.rs b/tests/slow/tokio-proofs/src/tokio_test/block_on.rs index 62b5c0a514a2..3bf00ac0a5a7 100644 --- a/tests/slow/tokio-proofs/src/tokio_test/block_on.rs +++ b/tests/slow/tokio-proofs/src/tokio_test/block_on.rs @@ -8,7 +8,7 @@ #![warn(rust_2018_idioms)] -use tokio::time::{sleep_until, Duration, Instant}; +use tokio::time::{Duration, Instant, sleep_until}; use tokio_test::block_on; #[cfg(disabled)] // because epoll is missing diff --git a/tests/std-checks/std/src/sync/atomic.rs b/tests/std-checks/std/src/sync/atomic.rs index 85c9a3380775..f6fc822bf40a 100644 --- a/tests/std-checks/std/src/sync/atomic.rs +++ b/tests/std-checks/std/src/sync/atomic.rs @@ -3,7 +3,7 @@ extern crate kani; -use std::sync::atomic::{AtomicU16, AtomicU32, AtomicU64, AtomicU8, AtomicUsize}; +use std::sync::atomic::{AtomicU8, AtomicU16, AtomicU32, AtomicU64, AtomicUsize}; /// Create wrapper functions to standard library functions that contains their contract. pub mod contracts { diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs index 2c181d69d6e5..7000ddb045a7 100644 --- a/tools/build-kani/src/main.rs +++ b/tools/build-kani/src/main.rs @@ -11,7 +11,7 @@ mod parser; mod sysroot; use crate::sysroot::{build_bin, build_lib, kani_no_core_lib, kani_playback_lib, kani_sysroot_lib}; -use anyhow::{bail, Result}; +use anyhow::{Result, bail}; use clap::Parser; use std::{ffi::OsString, path::Path, process::Command}; diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index ca42fea3f441..edd2a0973a83 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -11,8 +11,8 @@ //! //! Note: We don't cross-compile. Target is the same as the host. -use crate::{cp, AutoRun}; -use anyhow::{bail, format_err, Result}; +use crate::{AutoRun, cp}; +use anyhow::{Result, bail, format_err}; use cargo_metadata::{Artifact, Message}; use std::ffi::OsStr; use std::fs; diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index d5c4ccf3c116..0ff106c92de3 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -10,8 +10,8 @@ use std::path::{Path, PathBuf}; use std::str::FromStr; use std::time::Duration; -use test::test::TestTimeOptions; use test::ColorConfig; +use test::test::TestTimeOptions; #[derive(Clone, Copy, Eq, PartialEq, Debug)] pub enum Mode { diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs index afbee19e6ade..f49d4f64ce47 100644 --- a/tools/compiletest/src/header.rs +++ b/tools/compiletest/src/header.rs @@ -4,8 +4,8 @@ // See GitHub history for details. use std::fs::File; -use std::io::prelude::*; use std::io::BufReader; +use std::io::prelude::*; use std::path::Path; use tracing::*; diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index dd1284d7a3c9..9027e30121f8 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -10,8 +10,8 @@ extern crate test; -use crate::common::{output_base_dir, output_relative_path}; use crate::common::{Config, Mode, TestPaths}; +use crate::common::{output_base_dir, output_relative_path}; use crate::util::{logv, print_msg, top_level}; use getopts::Options; use std::env; @@ -21,8 +21,8 @@ use std::io::{self}; use std::path::{Path, PathBuf}; use std::str::FromStr; use std::time::{Duration, SystemTime}; -use test::test::TestTimeOptions; use test::ColorConfig; +use test::test::TestTimeOptions; use tracing::*; use walkdir::WalkDir; diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index f9ceaadc2cb5..a55f7efd2be5 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -6,11 +6,11 @@ // ignore-tidy-filelength use crate::common::KaniFailStep; -use crate::common::{output_base_dir, output_base_name}; use crate::common::{ CargoCoverage, CargoKani, CargoKaniTest, CoverageBased, Exec, Expected, Kani, KaniFixme, Stub, }; use crate::common::{Config, TestPaths}; +use crate::common::{output_base_dir, output_base_name}; use crate::header::TestProps; use crate::read2::read2; use crate::util::logv; diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs index b32627939bf5..e0f65929ffdd 100644 --- a/tools/scanner/src/analysis.rs +++ b/tools/scanner/src/analysis.rs @@ -7,7 +7,7 @@ use crate::info; use csv::WriterBuilder; use graph_cycles::Cycles; use petgraph::graph::Graph; -use serde::{ser::SerializeStruct, Serialize, Serializer}; +use serde::{Serialize, Serializer, ser::SerializeStruct}; use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; use stable_mir::mir::{