From c89426c73cf71c193abb2fb88f2d1e61d74c2534 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 29 Mar 2024 16:25:42 +0000 Subject: [PATCH 01/18] Upgrade Rust toolchain to nightly-2024-03-29 Signed-off-by: Felipe R. Monteiro --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index d08e3a84f0ad..eee073e29a89 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-03-21" +channel = "nightly-2024-03-29" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 6e33108ec685bfe2d92153f318231a218309805a Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 29 Mar 2024 16:26:27 +0000 Subject: [PATCH 02/18] Correctly use NullOp::UbChecks Signed-off-by: Felipe R. Monteiro --- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 5867448d9973..74622d41ed50 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> { .bytes(), Type::size_t(), ), - NullOp::UbCheck(_) => Expr::c_false(), + NullOp::UbChecks => Expr::c_false(), } } Rvalue::ShallowInitBox(ref operand, content_ty) => { From 7d69cab86ea726acb676688c23e37cc8d3ef8385 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 29 Mar 2024 16:28:20 +0000 Subject: [PATCH 03/18] Update calls to ty::RawPtr Signed-off-by: Felipe R. Monteiro --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 089d871d22b4..b5ccf1a83716 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -570,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> { // Note: This is not valid C but CBMC seems to be ok with it. ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(), ty::Str => Type::unsigned_int(8).flexible_array_of(), - ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t), + ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t), ty::FnDef(def_id, args) => { let instance = Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args) @@ -993,7 +993,7 @@ impl<'tcx> GotocCtx<'tcx> { | ty::Foreign(_) | ty::Coroutine(..) | ty::Int(_) - | ty::RawPtr(_) + | ty::RawPtr(_, _) | ty::Ref(..) | ty::Tuple(_) | ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(), @@ -1352,10 +1352,7 @@ impl<'tcx> GotocCtx<'tcx> { // `F16` and `F128` are not yet handled. // Tracked here: Primitive::F16 | Primitive::F128 => unimplemented!(), - Primitive::Pointer(_) => Ty::new_ptr( - self.tcx, - ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not }, - ), + Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not), } } @@ -1659,7 +1656,7 @@ fn common_vtable_fields(drop_in_place: Type) -> Vec { pub fn pointee_type(mir_type: Ty) -> Option { match mir_type.kind() { ty::Ref(_, pointee_type, _) => Some(*pointee_type), - ty::RawPtr(ty::TypeAndMut { ty: pointee_type, .. }) => Some(*pointee_type), + ty::RawPtr(pointee_type, _) => Some(*pointee_type), _ => None, } } From 0e52fed40b664da5659daf0af18552a1ae041c12 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 29 Mar 2024 16:29:17 +0000 Subject: [PATCH 04/18] Remove use of pretty_ty Signed-off-by: Felipe R. Monteiro --- kani-compiler/src/kani_middle/mod.rs | 6 +++--- kani-compiler/src/kani_middle/reachability.rs | 3 +-- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 4cd2d4a357d7..48c8a11fbded 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -22,7 +22,6 @@ use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem}; -use stable_mir::mir::pretty::pretty_ty; use stable_mir::ty::{BoundVariableKind, FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TypeVisitor}; use stable_mir::{CrateDef, DefId}; @@ -48,7 +47,7 @@ pub mod transform; /// error was found. pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { let krate = tcx.crate_name(LOCAL_CRATE); - for item in tcx.hir_crate_items(()).items() { + for item in tcx.hir().items() { let def_id = item.owner_id.def_id.to_def_id(); KaniAttributes::for_item(tcx, def_id).check_attributes(); if tcx.def_kind(def_id) == DefKind::GlobalAsm { @@ -129,7 +128,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) { self.tcx.dcx().err(format!( "{} contains a {}pointer ({}). This is prohibited for functions with contracts, \ as they cannot yet reason about the pointer behavior.", self.r#where, self.what, - pretty_ty(ty.kind()))); + ty)); } // Rust's type visitor only recurses into type arguments, (e.g. @@ -224,6 +223,7 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { /// Structure that represents the source location of a definition. /// TODO: Use `InternedString` once we move it out of the cprover_bindings. /// +#[allow(dead_code)] pub struct SourceLocation { pub filename: String, pub start_line: usize, diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 52b55d6b947c..6d711f05b4b4 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -25,7 +25,6 @@ use rustc_middle::ty::{TyCtxt, VtblEntry}; use rustc_smir::rustc_internal; use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef}; -use stable_mir::mir::pretty::pretty_ty; use stable_mir::mir::{ visit::Location, Body, CastKind, Constant, MirVisitor, PointerCoercion, Rvalue, Terminator, TerminatorKind, @@ -433,7 +432,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { `{}`. The function `{}` \ cannot be stubbed by `{}` due to \ generic bounds not being met. Callee: {}", - pretty_ty(receiver_ty.kind()), + receiver_ty, trait_, caller, self.tcx.def_path_str(stub), From fdf28f6aa50cda6b3c07a0a83b441735eff0774a Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 29 Mar 2024 16:30:07 +0000 Subject: [PATCH 05/18] Add #[allow(dead_code)] to avoid spurious warnings Signed-off-by: Felipe R. Monteiro --- kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | 1 + kani-compiler/src/kani_middle/transform/body.rs | 1 + kani-driver/src/call_cbmc.rs | 1 + kani-driver/src/cbmc_output_parser.rs | 2 ++ 4 files changed, 5 insertions(+) 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 a25e502aa574..db0377a3b82e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -39,6 +39,7 @@ use stable_mir::mir::mono::Instance; use stable_mir::mir::Body; use stable_mir::ty::Allocation; +#[allow(dead_code)] pub struct GotocCtx<'tcx> { /// the typing context pub tcx: TyCtxt<'tcx>, diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 32ffb373d767..a1d89b02ac4a 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -227,6 +227,7 @@ impl MutableBody { } #[derive(Clone, Debug)] +#[allow(dead_code)] pub enum CheckType { /// This is used by default when the `kani` crate is available. Assert(Instance), diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index a806331401cd..285043b3a9d7 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -40,6 +40,7 @@ pub enum FailedProperties { /// Our (kani-driver) notions of CBMC results. #[derive(Debug)] +#[allow(dead_code)] pub struct VerificationResult { /// Whether verification should be considered to have succeeded, or have failed. pub status: VerificationStatus, diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 1bb353d7d4c0..27e4179666e8 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -286,6 +286,7 @@ fn filepath(file: String) -> String { /// documented anywhere. So we ignore the rest for now. #[derive(Clone, Debug, Deserialize)] #[serde(rename_all = "camelCase")] +#[allow(dead_code)] pub struct TraceItem { pub thread: u32, pub step_type: String, @@ -300,6 +301,7 @@ pub struct TraceItem { /// Note: this struct can have a lot of different fields depending on the value type. /// The fields included right now are relevant to primitive types. #[derive(Clone, Debug, Deserialize)] +#[allow(dead_code)] pub struct TraceValue { pub name: String, pub binary: Option, From cd134a82af11486196f9397fc9ba2c11513e71f6 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 29 Mar 2024 18:19:21 +0000 Subject: [PATCH 06/18] Remove dead code Signed-off-by: Felipe R. Monteiro --- .../src/codegen_cprover_gotoc/context/goto_ctx.rs | 6 ------ kani-compiler/src/kani_middle/mod.rs | 7 +------ kani-compiler/src/kani_middle/transform/body.rs | 7 +++---- kani-driver/src/call_cbmc.rs | 12 ++---------- kani-driver/src/cbmc_output_parser.rs | 5 ----- kani-driver/src/concrete_playback/test_generator.rs | 3 --- 6 files changed, 6 insertions(+), 34 deletions(-) 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 db0377a3b82e..3a6501d544d8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -23,7 +23,6 @@ use crate::kani_queries::QueryDb; use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type}; use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; -use kani_metadata::HarnessMetadata; use rustc_data_structures::fx::FxHashMap; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ @@ -39,7 +38,6 @@ use stable_mir::mir::mono::Instance; use stable_mir::mir::Body; use stable_mir::ty::Allocation; -#[allow(dead_code)] pub struct GotocCtx<'tcx> { /// the typing context pub tcx: TyCtxt<'tcx>, @@ -62,8 +60,6 @@ pub struct GotocCtx<'tcx> { /// map from symbol identifier to string literal /// TODO: consider making the map from Expr to String instead pub str_literals: FxHashMap, - pub proof_harnesses: Vec, - pub test_harnesses: Vec, /// a global counter for generating unique IDs for checks pub global_checks_count: u64, /// A map of unsupported constructs that were found while codegen @@ -99,8 +95,6 @@ impl<'tcx> GotocCtx<'tcx> { current_fn: None, type_map: FxHashMap::default(), str_literals: FxHashMap::default(), - proof_harnesses: vec![], - test_harnesses: vec![], global_checks_count: 0, unsupported_constructs: FxHashMap::default(), concurrent_constructs: FxHashMap::default(), diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 48c8a11fbded..791c54e512c4 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -223,13 +223,10 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { /// Structure that represents the source location of a definition. /// TODO: Use `InternedString` once we move it out of the cprover_bindings. /// -#[allow(dead_code)] pub struct SourceLocation { pub filename: String, pub start_line: usize, - pub start_col: usize, pub end_line: usize, - pub end_col: usize, } impl SourceLocation { @@ -237,10 +234,8 @@ impl SourceLocation { let loc = span.get_lines(); let filename = span.get_filename().to_string(); let start_line = loc.start_line; - let start_col = loc.start_col; let end_line = loc.end_line; - let end_col = loc.end_col; - SourceLocation { filename, start_line, start_col, end_line, end_col } + SourceLocation { filename, start_line, end_line } } } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index a1d89b02ac4a..98c2f6df8800 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -227,12 +227,11 @@ impl MutableBody { } #[derive(Clone, Debug)] -#[allow(dead_code)] pub enum CheckType { /// This is used by default when the `kani` crate is available. Assert(Instance), /// When the `kani` crate is not available, we have to model the check as an `if { panic!() }`. - Panic(Instance), + Panic(), /// When building non-core crate, such as `rustc-std-workspace-core`, we cannot /// instrument code, but we can still compile them. NoCore, @@ -247,8 +246,8 @@ impl CheckType { pub fn new(tcx: TyCtxt) -> CheckType { if let Some(instance) = find_instance(tcx, "KaniAssert") { CheckType::Assert(instance) - } else if let Some(instance) = find_instance(tcx, "panic_str") { - CheckType::Panic(instance) + } else if let Some(_) = find_instance(tcx, "panic_str") { + CheckType::Panic() } else { CheckType::NoCore } diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 285043b3a9d7..7d0edf6f50e5 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -11,7 +11,7 @@ use std::time::{Duration, Instant}; use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ - extract_results, process_cbmc_output, CheckStatus, ParserItem, Property, VerificationOutput, + extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput, }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; use crate::session::KaniSession; @@ -40,15 +40,11 @@ pub enum FailedProperties { /// Our (kani-driver) notions of CBMC results. #[derive(Debug)] -#[allow(dead_code)] pub struct VerificationResult { /// Whether verification should be considered to have succeeded, or have failed. pub status: VerificationStatus, /// The compact representation for failed properties pub failed_properties: FailedProperties, - /// The parsed output, message by message, of CBMC. However, the `Result` message has been - /// removed and is available in `results` instead. - pub messages: Option>, /// The `Result` properties in detail or the exit_status of CBMC. /// Note: CBMC process exit status is only potentially useful if `status` is `Failure`. /// Kani will see CBMC report "failure" that's actually success (interpreting "failed" @@ -255,7 +251,7 @@ impl VerificationResult { start_time: Instant, ) -> VerificationResult { let runtime = start_time.elapsed(); - let (items, results) = extract_results(output.processed_items); + let (_, results) = extract_results(output.processed_items); if let Some(results) = results { let (status, failed_properties) = @@ -263,7 +259,6 @@ impl VerificationResult { VerificationResult { status, failed_properties, - messages: Some(items), results: Ok(results), runtime, generated_concrete_test: false, @@ -273,7 +268,6 @@ impl VerificationResult { VerificationResult { status: VerificationStatus::Failure, failed_properties: FailedProperties::Other, - messages: Some(items), results: Err(output.process_status), runtime, generated_concrete_test: false, @@ -285,7 +279,6 @@ impl VerificationResult { VerificationResult { status: VerificationStatus::Success, failed_properties: FailedProperties::None, - messages: None, results: Ok(vec![]), runtime: Duration::from_secs(0), generated_concrete_test: false, @@ -296,7 +289,6 @@ impl VerificationResult { VerificationResult { status: VerificationStatus::Failure, failed_properties: FailedProperties::Other, - messages: None, // on failure, exit codes in theory might be used, // but `mock_failure` should never be used in a context where they will, // so again use something weird: diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 27e4179666e8..127f98beab56 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -286,11 +286,8 @@ fn filepath(file: String) -> String { /// documented anywhere. So we ignore the rest for now. #[derive(Clone, Debug, Deserialize)] #[serde(rename_all = "camelCase")] -#[allow(dead_code)] pub struct TraceItem { - pub thread: u32, pub step_type: String, - pub hidden: bool, pub lhs: Option, pub source_location: Option, pub value: Option, @@ -301,9 +298,7 @@ pub struct TraceItem { /// Note: this struct can have a lot of different fields depending on the value type. /// The fields included right now are relevant to primitive types. #[derive(Clone, Debug, Deserialize)] -#[allow(dead_code)] pub struct TraceValue { - pub name: String, pub binary: Option, pub data: Option, pub width: Option, diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 53c3a92dd94c..dbd2fb9e03d2 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -588,9 +588,7 @@ mod tests { line: None, }, trace: Some(vec![TraceItem { - thread: 0, step_type: "assignment".to_string(), - hidden: false, lhs: Some("goto_symex$$return_value".to_string()), source_location: Some(SourceLocation { column: None, @@ -599,7 +597,6 @@ mod tests { line: None, }), value: Some(TraceValue { - name: "".to_string(), binary: Some("0000001100000001".to_string()), data: Some(TraceData::NonBool("385".to_string())), width: Some(16), From 851362e2543dc193e30c9eb270b50722443845fc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2024 11:33:58 +0200 Subject: [PATCH 07/18] Update kani-compiler/src/kani_middle/transform/body.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-compiler/src/kani_middle/transform/body.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 98c2f6df8800..afbfbd07a68c 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -231,7 +231,7 @@ pub enum CheckType { /// This is used by default when the `kani` crate is available. Assert(Instance), /// When the `kani` crate is not available, we have to model the check as an `if { panic!() }`. - Panic(), + Panic, /// When building non-core crate, such as `rustc-std-workspace-core`, we cannot /// instrument code, but we can still compile them. NoCore, From f93193c22db94718176b6ccb7f3dc964fed4f5ff Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2024 15:36:02 +0000 Subject: [PATCH 08/18] fixup! Update kani-compiler/src/kani_middle/transform/body.rs --- kani-compiler/src/kani_middle/transform/body.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index afbfbd07a68c..73a3dcb74c5a 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -173,7 +173,7 @@ impl MutableBody { let terminator = Terminator { kind, span }; self.split_bb(source, terminator); } - CheckType::Panic(..) | CheckType::NoCore => { + CheckType::Panic | CheckType::NoCore => { tcx.sess .dcx() .struct_err("Failed to instrument the code. Cannot find `kani::assert`") @@ -247,7 +247,7 @@ impl CheckType { if let Some(instance) = find_instance(tcx, "KaniAssert") { CheckType::Assert(instance) } else if let Some(_) = find_instance(tcx, "panic_str") { - CheckType::Panic() + CheckType::Panic } else { CheckType::NoCore } From 31c549d60f9bb3ec5f3cd0c4d1c870085aeb6263 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2024 15:36:10 +0000 Subject: [PATCH 09/18] Implement typed_swap intrinsic --- .../codegen/intrinsic.rs | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 8fce4b309820..1cff128794c4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -580,6 +580,7 @@ impl<'tcx> GotocCtx<'tcx> { "truncf64" => codegen_simple_intrinsic!(Trunc), "type_id" => codegen_intrinsic_const!(), "type_name" => codegen_intrinsic_const!(), + "typed_swap" => self.codegen_swap(fargs, loc), "unaligned_volatile_load" => { unstable_codegen!( self.codegen_expr_to_place_stable(place, fargs.remove(0).dereference()) @@ -1943,6 +1944,47 @@ impl<'tcx> GotocCtx<'tcx> { let zero = Type::size_t().zero(); cast_ptr.rem(align).eq(zero) } + + /// Swaps the memory contents pointed to by arguments `x` and `y`, respectively, which is + /// required for the `typed_swap` intrinsic. + /// + /// The standard library API requires that `x` and `y` are readable and writable as their + /// (common) type (which auto-generated checks for dereferencing will take care of), and the + /// memory regions pointed to must be non-overlapping. + pub fn codegen_swap(&mut self, fargs: Vec, loc: Location) -> Stmt { + // if(same_object(x, y)) { + // assert(x + 1 <= y || y + 1 <= x); + // assume(x + 1 <= y || y + 1 <= x); + // } + let one = Expr::int_constant(1, Type::c_int()); + let non_overlapping = fargs[0] + .clone() + .plus(one.clone()) + .le(fargs[1].clone()) + .or(fargs[1].clone().plus(one.clone()).le(fargs[0].clone())); + let non_overlapping_check = self.codegen_assert_assume( + non_overlapping, + PropertyClass::SafetyCheck, + "memory regions pointed to by `x` and `y` must not overlap", + loc, + ); + let non_overlapping_stmt = Stmt::if_then_else( + fargs[0].clone().same_object(fargs[1].clone()), + non_overlapping_check, + None, + loc, + ); + + // T t = *y; *y = *x; *x = t; + let deref_y = fargs[1].clone().dereference(); + let (temp_var, assign_to_t) = + self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc); + let assign_to_y = + fargs[1].clone().dereference().assign(fargs[0].clone().dereference(), loc); + let assign_to_x = fargs[0].clone().dereference().assign(temp_var, loc); + + Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) + } } fn instance_args(instance: &Instance) -> GenericArgs { From c270426e0a07fc4bb3210013273a1571cba6df70 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2024 15:42:58 +0000 Subject: [PATCH 10/18] fixup! Remove use of pretty_ty --- kani-compiler/src/kani_middle/reachability.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 791befa31c1c..456d5425b245 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -452,10 +452,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { objects in the modifies clause (including return types) \ implement `{}`.\nThis is a strict condition to use \ function contracts as verified stubs.", - pretty_ty(receiver_ty.kind()), - trait_, - callee, - trait_, + receiver_ty, trait_, callee, trait_, ), ); } else { From 1b4a535248c095dfc0805bd4c60d51afa87ea91d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2024 16:01:03 +0000 Subject: [PATCH 11/18] Add #[allow(dead_code)] to keep clippy happy --- tools/bookrunner/src/litani.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/tools/bookrunner/src/litani.rs b/tools/bookrunner/src/litani.rs index 620aa9c9f0d0..c51bc3935117 100644 --- a/tools/bookrunner/src/litani.rs +++ b/tools/bookrunner/src/litani.rs @@ -16,6 +16,7 @@ use std::process::{Child, Command}; /// attributes in such files, but it may require you to /// extend it if advanced features are used (e.g., pools) #[derive(Debug, Deserialize)] +#[allow(dead_code)] pub struct LitaniRun { pub aux: Option>, pub project: String, @@ -39,6 +40,7 @@ impl LitaniRun { } #[derive(Debug, Deserialize)] +#[allow(dead_code)] pub struct LitaniParalellism { pub trace: Vec, pub max_paralellism: Option, @@ -46,6 +48,7 @@ pub struct LitaniParalellism { } #[derive(Debug, Deserialize)] +#[allow(dead_code)] pub struct LitaniTrace { pub running: u32, pub finished: u32, @@ -54,6 +57,7 @@ pub struct LitaniTrace { } #[derive(Debug, Deserialize)] +#[allow(dead_code)] pub struct LitaniPipeline { pub name: String, pub ci_stages: Vec, @@ -76,6 +80,7 @@ impl LitaniPipeline { } #[derive(Debug, Deserialize)] +#[allow(dead_code)] pub struct LitaniStage { pub jobs: Vec, pub progress: u32, @@ -88,6 +93,7 @@ pub struct LitaniStage { // Some attributes in litani's `jobs` are not always included // or they are null, so we use `Option<...>` to deserialize them #[derive(Debug, Deserialize)] +#[allow(dead_code)] pub struct LitaniJob { pub wrapper_arguments: LitaniWrapperArguments, pub complete: bool, @@ -108,6 +114,7 @@ pub struct LitaniJob { // Some attributes in litani's `wrapper_arguments` are not always included // or they are null, so we use `Option<...>` to deserialize them #[derive(Debug, Deserialize)] +#[allow(dead_code)] pub struct LitaniWrapperArguments { pub subcommand: String, pub verbose: bool, From 307701407bbd0f753ca2400d4e432e5f586bcf53 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 4 Apr 2024 16:02:22 +0000 Subject: [PATCH 12/18] fixup! fixup! Update kani-compiler/src/kani_middle/transform/body.rs --- kani-compiler/src/kani_middle/transform/body.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 73a3dcb74c5a..d14aca3a7c5b 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -246,7 +246,7 @@ impl CheckType { pub fn new(tcx: TyCtxt) -> CheckType { if let Some(instance) = find_instance(tcx, "KaniAssert") { CheckType::Assert(instance) - } else if let Some(_) = find_instance(tcx, "panic_str") { + } else if find_instance(tcx, "panic_str").is_some() { CheckType::Panic } else { CheckType::NoCore From d4abc03ed9219b4bbc97bf75440d59e06cb4d11a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Apr 2024 09:55:43 +0000 Subject: [PATCH 13/18] Add test for typed_swap --- tests/kani/Intrinsics/typed_swap.rs | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 tests/kani/Intrinsics/typed_swap.rs diff --git a/tests/kani/Intrinsics/typed_swap.rs b/tests/kani/Intrinsics/typed_swap.rs new file mode 100644 index 000000000000..7db35289bcdb --- /dev/null +++ b/tests/kani/Intrinsics/typed_swap.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `typed_swap` yields the expected results. +// https://doc.rust-lang.org/nightly/std/intrinsics/fn.typed_swap.html + +#![feature(core_intrinsics)] +#![allow(internal_features)] + +#[kani::proof] +fn test_typed_swap_u32() { + let mut a: u32 = kani::any(); + let a_before = a; + let mut b: u32 = kani::any(); + let b_before = b; + unsafe { std::intrinsics::typed_swap(&mut a, &mut b); } + assert!(b == a_before); + assert!(a == b_before); +} From fc083d65457e437f8bd26959e9542834edba3535 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Apr 2024 09:55:58 +0000 Subject: [PATCH 14/18] Add typed_swap to documentation --- docs/src/rust-feature-support/intrinsics.md | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 7df1a093943f..49a1f0845ecc 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -220,6 +220,7 @@ truncf64 | Yes | | try | No | [#267](https://github.com/model-checking/kani/issues/267) | type_id | Yes | | type_name | Yes | | +typed_swap | Yes | | unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) | unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) | unchecked_add | Yes | | From 7344be86ad31df624f657d95f98624f0bc439010 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Apr 2024 09:56:28 +0000 Subject: [PATCH 15/18] fixup! Add test for typed_swap --- tests/kani/Intrinsics/typed_swap.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/kani/Intrinsics/typed_swap.rs b/tests/kani/Intrinsics/typed_swap.rs index 7db35289bcdb..4279bb713ece 100644 --- a/tests/kani/Intrinsics/typed_swap.rs +++ b/tests/kani/Intrinsics/typed_swap.rs @@ -13,7 +13,9 @@ fn test_typed_swap_u32() { let a_before = a; let mut b: u32 = kani::any(); let b_before = b; - unsafe { std::intrinsics::typed_swap(&mut a, &mut b); } + unsafe { + std::intrinsics::typed_swap(&mut a, &mut b); + } assert!(b == a_before); assert!(a == b_before); } From 518fd078027162969f0cb19975d977706717a407 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Apr 2024 10:00:49 +0000 Subject: [PATCH 16/18] typed_swap: use x, y --- .../codegen/intrinsic.rs | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 1cff128794c4..2ee759eb0409 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1951,17 +1951,18 @@ impl<'tcx> GotocCtx<'tcx> { /// The standard library API requires that `x` and `y` are readable and writable as their /// (common) type (which auto-generated checks for dereferencing will take care of), and the /// memory regions pointed to must be non-overlapping. - pub fn codegen_swap(&mut self, fargs: Vec, loc: Location) -> Stmt { + pub fn codegen_swap(&mut self, mut fargs: Vec, loc: Location) -> Stmt { + let x = fargs.remove(0); + let y = fargs.remove(0); + // if(same_object(x, y)) { // assert(x + 1 <= y || y + 1 <= x); // assume(x + 1 <= y || y + 1 <= x); // } let one = Expr::int_constant(1, Type::c_int()); - let non_overlapping = fargs[0] - .clone() - .plus(one.clone()) - .le(fargs[1].clone()) - .or(fargs[1].clone().plus(one.clone()).le(fargs[0].clone())); + let non_overlapping = x.clone().plus(one.clone()) + .le(y.clone()) + .or(y.clone().plus(one.clone()).le(x.clone())); let non_overlapping_check = self.codegen_assert_assume( non_overlapping, PropertyClass::SafetyCheck, @@ -1969,19 +1970,19 @@ impl<'tcx> GotocCtx<'tcx> { loc, ); let non_overlapping_stmt = Stmt::if_then_else( - fargs[0].clone().same_object(fargs[1].clone()), + x.clone().same_object(y.clone()), non_overlapping_check, None, loc, ); // T t = *y; *y = *x; *x = t; - let deref_y = fargs[1].clone().dereference(); + let deref_y = y.clone().dereference(); let (temp_var, assign_to_t) = self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc); let assign_to_y = - fargs[1].clone().dereference().assign(fargs[0].clone().dereference(), loc); - let assign_to_x = fargs[0].clone().dereference().assign(temp_var, loc); + y.dereference().assign(x.clone().dereference(), loc); + let assign_to_x = x.dereference().assign(temp_var, loc); Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) } From 4dc6be4965dfc8fd3d8a25381b390531c3234f20 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Apr 2024 10:05:07 +0000 Subject: [PATCH 17/18] Check types --- .../codegen/intrinsic.rs | 25 +++++++++---------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 2ee759eb0409..8a61d46ed518 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -580,7 +580,7 @@ impl<'tcx> GotocCtx<'tcx> { "truncf64" => codegen_simple_intrinsic!(Trunc), "type_id" => codegen_intrinsic_const!(), "type_name" => codegen_intrinsic_const!(), - "typed_swap" => self.codegen_swap(fargs, loc), + "typed_swap" => self.codegen_swap(fargs, farg_types, loc), "unaligned_volatile_load" => { unstable_codegen!( self.codegen_expr_to_place_stable(place, fargs.remove(0).dereference()) @@ -1951,7 +1951,12 @@ impl<'tcx> GotocCtx<'tcx> { /// The standard library API requires that `x` and `y` are readable and writable as their /// (common) type (which auto-generated checks for dereferencing will take care of), and the /// memory regions pointed to must be non-overlapping. - pub fn codegen_swap(&mut self, mut fargs: Vec, loc: Location) -> Stmt { + pub fn codegen_swap(&mut self, mut fargs: Vec, farg_types: &[Ty], loc: Location) -> Stmt { + // two parameters, and both must be raw pointers with the same base type + assert!(fargs.len() == 2); + assert!(farg_types[0].kind().is_raw_ptr()); + assert!(farg_types[0] == farg_types[1]); + let x = fargs.remove(0); let y = fargs.remove(0); @@ -1960,28 +1965,22 @@ impl<'tcx> GotocCtx<'tcx> { // assume(x + 1 <= y || y + 1 <= x); // } let one = Expr::int_constant(1, Type::c_int()); - let non_overlapping = x.clone().plus(one.clone()) - .le(y.clone()) - .or(y.clone().plus(one.clone()).le(x.clone())); + let non_overlapping = + x.clone().plus(one.clone()).le(y.clone()).or(y.clone().plus(one.clone()).le(x.clone())); let non_overlapping_check = self.codegen_assert_assume( non_overlapping, PropertyClass::SafetyCheck, "memory regions pointed to by `x` and `y` must not overlap", loc, ); - let non_overlapping_stmt = Stmt::if_then_else( - x.clone().same_object(y.clone()), - non_overlapping_check, - None, - loc, - ); + let non_overlapping_stmt = + Stmt::if_then_else(x.clone().same_object(y.clone()), non_overlapping_check, None, loc); // T t = *y; *y = *x; *x = t; let deref_y = y.clone().dereference(); let (temp_var, assign_to_t) = self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc); - let assign_to_y = - y.dereference().assign(x.clone().dereference(), loc); + let assign_to_y = y.dereference().assign(x.clone().dereference(), loc); let assign_to_x = x.dereference().assign(temp_var, loc); Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc) From 50d34e6a3a61084d4199db84566468267c6e3e8d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 5 Apr 2024 10:12:49 +0000 Subject: [PATCH 18/18] Restore start/end column fields --- kani-compiler/src/kani_middle/mod.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 1730d5587334..17992953d5c7 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -127,7 +127,11 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { pub struct SourceLocation { pub filename: String, pub start_line: usize, + #[allow(dead_code)] + pub start_col: usize, // set, but not currently used in Goto output pub end_line: usize, + #[allow(dead_code)] + pub end_col: usize, // set, but not currently used in Goto output } impl SourceLocation { @@ -135,8 +139,10 @@ impl SourceLocation { let loc = span.get_lines(); let filename = span.get_filename().to_string(); let start_line = loc.start_line; + let start_col = loc.start_col; let end_line = loc.end_line; - SourceLocation { filename, start_line, end_line } + let end_col = loc.end_col; + SourceLocation { filename, start_line, start_col, end_line, end_col } } }