From 07092ded6699cfdcb159138eae1f25b160dca529 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 3 Oct 2022 16:34:08 -0700 Subject: [PATCH] Upgrade toolchain to nightly-2022-09-13 (#1737) Fixes #1615 Relevant changes to rustc: - https://github.com/rust-lang/rust/pull/101483: Change to intrinsics. - https://github.com/rust-lang/rust/pull/94075: Change to niche opt. - https://github.com/rust-lang/rust/pull/101101: Method rename. Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .cargo/config.toml | 4 + .../codegen/intrinsic.rs | 30 ++-- .../codegen_cprover_gotoc/codegen/operand.rs | 4 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 4 +- .../codegen/statement.rs | 25 ++-- .../src/codegen_cprover_gotoc/codegen/typ.rs | 131 ++++++++++-------- .../src/codegen_cprover_gotoc/reachability.rs | 6 +- kani-compiler/src/main.rs | 1 + kani-driver/src/main.rs | 1 + rust-toolchain.toml | 2 +- src/lib.rs | 2 - tests/kani/Enum/niche_variants_with_data.rs | 35 +++++ .../PtrGuaranteedCmp/{eq.rs => cmp.rs} | 10 +- tests/kani/Intrinsics/PtrGuaranteedCmp/ne.rs | 19 --- 14 files changed, 163 insertions(+), 111 deletions(-) create mode 100644 tests/kani/Enum/niche_variants_with_data.rs rename tests/kani/Intrinsics/PtrGuaranteedCmp/{eq.rs => cmp.rs} (55%) delete mode 100644 tests/kani/Intrinsics/PtrGuaranteedCmp/ne.rs diff --git a/.cargo/config.toml b/.cargo/config.toml index 949746371898..6d501b0c3154 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -28,4 +28,8 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -. "-Aclippy::expect_fun_call", "-Aclippy::or_fun_call", "-Aclippy::new_without_default", + + # New lints that we are not compliant yet + "-Aclippy::needless-borrow", + "-Aclippy::bool-to-int-with-if", ] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 37cbee6d2782..def8c2275e8b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -313,13 +313,6 @@ impl<'tcx> GotocCtx<'tcx> { ($f:ident) => {{ codegen_intrinsic_binop!($f) }}; } - // Intrinsics which encode a pointer comparison (e.g., `ptr_guaranteed_eq`). - // These behave as regular pointer comparison at runtime: - // https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq - macro_rules! codegen_ptr_guaranteed_cmp { - ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b).cast_to(Type::c_bool())) }}; - } - // Intrinsics which encode a simple binary operation macro_rules! codegen_intrinsic_binop { ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b)) }}; @@ -596,8 +589,7 @@ impl<'tcx> GotocCtx<'tcx> { "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)), "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)), "pref_align_of" => codegen_intrinsic_const!(), - "ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq), - "ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq), + "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, p), "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc), "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, p, loc), "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc), @@ -1012,6 +1004,26 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc) } + // In some contexts (e.g., compilation-time evaluation), + // `ptr_guaranteed_cmp` compares two pointers and returns: + // * 2 if the result is unknown. + // * 1 if they are guaranteed to be equal. + // * 0 if they are guaranteed to be not equal. + // But at runtime, this intrinsic behaves as a regular pointer comparison. + // Therefore, we return 1 if the pointers are equal and 0 otherwise. + // + // This intrinsic replaces `ptr_guaranteed_eq` and `ptr_guaranteed_ne`: + // https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq + fn codegen_ptr_guaranteed_cmp(&mut self, mut fargs: Vec, p: &Place<'tcx>) -> Stmt { + let a = fargs.remove(0); + let b = fargs.remove(0); + let place_type = self.place_ty(p); + let res_type = self.codegen_ty(place_type); + let eq_expr = a.eq(b); + let cmp_expr = eq_expr.ternary(res_type.one(), res_type.zero()); + self.codegen_expr_to_place(p, cmp_expr) + } + /// Computes the offset from a pointer. /// /// Note that this function handles code generation for: diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 814c5c8a0cdd..b04565df1e67 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -466,12 +466,12 @@ impl<'tcx> GotocCtx<'tcx> { } fn codegen_allocation_data(&mut self, alloc: &'tcx Allocation) -> Vec> { - let mut alloc_vals = Vec::with_capacity(alloc.relocations().len() + 1); + let mut alloc_vals = Vec::with_capacity(alloc.provenance().len() + 1); let pointer_size = Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); let mut next_offset = Size::ZERO; - for &(offset, alloc_id) in alloc.relocations().iter() { + for &(offset, alloc_id) in alloc.provenance().iter() { if offset > next_offset { let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( next_offset.bytes_usize()..offset.bytes_usize(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 68e032dc52fa..531f3a79c355 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -504,7 +504,7 @@ impl<'tcx> GotocCtx<'tcx> { TagEncoding::Direct => { self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty)) } - TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { + TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { // This code follows the logic in the ssa codegen backend: // https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247 // See also the cranelift backend: @@ -550,7 +550,7 @@ impl<'tcx> GotocCtx<'tcx> { }; is_niche.ternary( niche_discr, - Expr::int_constant(dataful_variant.as_u32(), result_type), + Expr::int_constant(untagged_variant.as_u32(), result_type), ) } }, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 526447f52bca..477bdd206d7c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -11,8 +11,8 @@ use kani_queries::UserInput; use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ - AssertKind, BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator, - TerminatorKind, + AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, + SwitchTargets, Terminator, TerminatorKind, }; use rustc_middle::ty; use rustc_middle::ty::layout::LayoutOf; @@ -89,8 +89,8 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_discriminant_field(place_goto_expr, pt) .assign(discr, location) } - TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { - if dataful_variant != variant_index { + TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { + if untagged_variant != variant_index { let offset = match &layout.fields { FieldsShape::Arbitrary { offsets, .. } => offsets[0], _ => unreachable!("niche encoding must have arbitrary fields"), @@ -122,11 +122,9 @@ impl<'tcx> GotocCtx<'tcx> { } StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me - StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping { - ref src, - ref dst, - ref count, - }) => { + StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping( + mir::CopyNonOverlapping { ref src, ref dst, ref count }, + )) => { // Pack the operands and their types, then call `codegen_copy` let fargs = vec![ self.codegen_operand(src), @@ -137,6 +135,15 @@ impl<'tcx> GotocCtx<'tcx> { &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)]; self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location) } + StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => { + let cond = self.codegen_operand(op).cast_to(Type::bool()); + self.codegen_assert_assume( + cond, + PropertyClass::Assume, + "assumption failed", + location, + ) + } StatementKind::FakeRead(_) | StatementKind::Retag(_, _) | StatementKind::AscribeUserType(_, _) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 30efda5f3b73..4e27184858c8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1418,13 +1418,13 @@ impl<'tcx> GotocCtx<'tcx> { subst: &'tcx InternalSubsts<'tcx>, ) -> Type { let pretty_name = self.ty_pretty_name(ty); - self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |ctx, name| { - // variants appearing in source code (in source code order) - let source_variants = &adtdef.variants(); - let layout = ctx.layout_of(ty); - // variants appearing in mir code - match &layout.variants { - Variants::Single { index } => { + // variants appearing in source code (in source code order) + let source_variants = &adtdef.variants(); + let layout = self.layout_of(ty); + // variants appearing in mir code + match &layout.variants { + Variants::Single { index } => { + self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, _| { match source_variants.get(*index) { None => { // an empty enum with no variants (its value cannot be instantiated) @@ -1432,18 +1432,20 @@ impl<'tcx> GotocCtx<'tcx> { } Some(variant) => { // a single enum is pretty much like a struct - let layout = ctx.layout_of(ty).layout; - ctx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO) + let layout = gcx.layout_of(ty).layout; + gcx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO) } } - } - Variants::Multiple { tag_encoding, variants, tag_field, .. } => { - // Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants: - assert!(layout.fields.count() <= 1); - // Contrary to generators, the discriminant is the first (and only) field for enums: - assert_eq!(*tag_field, 0); - match tag_encoding { - TagEncoding::Direct => { + }) + } + Variants::Multiple { tag_encoding, variants, tag_field, .. } => { + // Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants: + assert!(layout.fields.count() <= 1); + // Contrary to generators, the discriminant is the first (and only) field for enums: + assert_eq!(*tag_field, 0); + match tag_encoding { + TagEncoding::Direct => { + self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, name| { // For direct encoding of tags, we generate a type with two fields: // ``` // struct tag-<> { // enum type @@ -1455,14 +1457,14 @@ impl<'tcx> GotocCtx<'tcx> { // (`#[repr]`) and it represents which variant is being used. // The `cases` field is a union of all variant types where the name // of each union field is the name of the corresponding discriminant. - let discr_t = ctx.codegen_enum_discr_typ(ty); - let int = ctx.codegen_ty(discr_t); - let discr_offset = ctx.layout_of(discr_t).size; + let discr_t = gcx.codegen_enum_discr_typ(ty); + let int = gcx.codegen_ty(discr_t); + let discr_offset = gcx.layout_of(discr_t).size; let initial_offset = - ctx.variant_min_offset(variants).unwrap_or(discr_offset); + gcx.variant_min_offset(variants).unwrap_or(discr_offset); let mut fields = vec![DatatypeComponent::field("case", int)]; if let Some(padding) = - ctx.codegen_struct_padding(discr_offset, initial_offset, 0) + gcx.codegen_struct_padding(discr_offset, initial_offset, 0) { fields.push(padding); } @@ -1470,7 +1472,7 @@ impl<'tcx> GotocCtx<'tcx> { let union_pretty_name = format!("{}-union", pretty_name); fields.push(DatatypeComponent::field( "cases", - ctx.ensure_union(&union_name, &union_pretty_name, |ctx, name| { + gcx.ensure_union(&union_name, &union_pretty_name, |ctx, name| { ctx.codegen_enum_cases( name, pretty_name, @@ -1482,45 +1484,56 @@ impl<'tcx> GotocCtx<'tcx> { }), )); fields - } - TagEncoding::Niche { dataful_variant, .. } => { - // Enumerations with multiple variants and niche encoding have a - // specific format that can be used to optimize its layout and reduce - // memory consumption. - // - // These enumerations have one and only one variant with non-ZST - // fields which is referred to by the `dataful_variant` index. Their - // final size and alignment is equal to the one from the - // `dataful_variant`. All other variants either don't have any field - // or all fields types are ZST. - // - // Because of that, we can represent these enums as simple structures - // where each field represent one variant. This allows them to be - // referred to correctly. - // - // Note: I tried using a union instead but it had a significant runtime - // penalty. - tracing::trace!( - ?name, - ?variants, - ?dataful_variant, - ?tag_encoding, - ?subst, - "codegen_enum: Niche" - ); - ctx.codegen_enum_cases( - name, - pretty_name, - adtdef, - subst, - variants, - Size::ZERO, - ) - } + }) + } + TagEncoding::Niche { .. } => { + self.codegen_enum_niche(ty, adtdef, subst, variants) } } } - }) + } + } + + /// Codegen an enumeration that is encoded using niche optimization. + /// + /// Enumerations with multiple variants and niche encoding have a + /// specific format that can be used to optimize its layout and reduce + /// memory consumption. + /// + /// The niche is a location in the entire type where some bit pattern + /// isn't valid. The compiler uses the `untagged_variant` index to + /// access this field. + /// The final size and alignment is also equal to the one from the + /// `untagged_variant`. All other variants either don't have any field, + /// or their size is smaller than the `untagged_variant`. + /// See for more details. + /// + /// Because of that, we usually represent these enums as simple unions + /// where each field represent one variant. This allows them to be + /// referred to correctly. + /// + /// The one exception is the case where only one variant has data. + /// We use a struct instead because it is more performant. + fn codegen_enum_niche( + &mut self, + ty: Ty<'tcx>, + adtdef: &'tcx AdtDef, + subst: &'tcx InternalSubsts<'tcx>, + variants: &IndexVec, + ) -> Type { + let non_zst_count = variants.iter().filter(|layout| layout.size().bytes() > 0).count(); + let mangled_name = self.ty_mangled_name(ty); + let pretty_name = self.ty_pretty_name(ty); + tracing::trace!(?pretty_name, ?variants, ?subst, ?non_zst_count, "codegen_enum: Niche"); + if non_zst_count > 1 { + self.ensure_union(mangled_name, pretty_name, |gcx, name| { + gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO) + }) + } else { + self.ensure_struct(mangled_name, pretty_name, |gcx, name| { + gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO) + }) + } } pub(crate) fn variant_min_offset( diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs index 7da8b5d603a1..78f64c562b0d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -96,7 +96,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { // Collect initialization. let alloc = self.tcx.eval_static_initializer(def_id).unwrap(); - for &id in alloc.inner().relocations().values() { + for &id in alloc.inner().provenance().values() { self.queue.extend(collect_alloc_items(self.tcx, id).iter()); } } @@ -202,7 +202,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { } ConstValue::Slice { data: alloc, start: _, end: _ } | ConstValue::ByRef { alloc, .. } => { - for &id in alloc.inner().relocations().values() { + for &id in alloc.inner().provenance().values() { self.collected.extend(collect_alloc_items(self.tcx, id).iter()) } } @@ -542,7 +542,7 @@ fn collect_alloc_items<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec { trace!(?alloc_id, "global_alloc memory"); items.extend( - alloc.inner().relocations().values().flat_map(|id| collect_alloc_items(tcx, *id)), + alloc.inner().provenance().values().flat_map(|id| collect_alloc_items(tcx, *id)), ); } GlobalAlloc::VTable(ty, trait_ref) => { diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index d8aac04bd50d..e5adb2415ad8 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -12,6 +12,7 @@ #![feature(box_patterns)] #![feature(once_cell)] #![feature(rustc_private)] +#![feature(more_qualified_paths)] extern crate rustc_ast; extern crate rustc_codegen_ssa; extern crate rustc_data_structures; diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 6e00dfb96604..e913fc2afbd9 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(let_chains)] use anyhow::Result; use args_toml::join_args; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0bb937d962a9..15c481946b65 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-08-30" +channel = "nightly-2022-09-13" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/src/lib.rs b/src/lib.rs index 131bb04b7de1..dc11345117e9 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -12,8 +12,6 @@ //! binaries will download the appropriate Kani release bundle and invoke //! the "real" `kani` and `cargo-kani` binaries. -#![warn(clippy::all, clippy::cargo)] - mod cmd; mod os_hacks; mod setup; diff --git a/tests/kani/Enum/niche_variants_with_data.rs b/tests/kani/Enum/niche_variants_with_data.rs new file mode 100644 index 000000000000..71edb098b0fe --- /dev/null +++ b/tests/kani/Enum/niche_variants_with_data.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test checks the layout of the niche optimization with multiple data. + +enum MyEnum { + Flag1(Option), + Flag2(u8, Option), +} + +trait IsTrue { + fn check(&self) -> bool; +} + +impl IsTrue for MyEnum { + fn check(&self) -> bool { + match self { + MyEnum::Flag1(Some(val)) | MyEnum::Flag2(_, Some(val)) => *val, + _ => false, + } + } +} + +#[kani::proof] +pub fn check_size() { + let flag = MyEnum::Flag1(Some(true)); + assert_eq!(std::mem::size_of_val(&flag), 2); +} + +#[kani::proof] +pub fn check_val() { + let flag = MyEnum::Flag2(0, None); + let is_true: &dyn IsTrue = &flag; + assert_eq!(is_true.check(), false); +} diff --git a/tests/kani/Intrinsics/PtrGuaranteedCmp/eq.rs b/tests/kani/Intrinsics/PtrGuaranteedCmp/cmp.rs similarity index 55% rename from tests/kani/Intrinsics/PtrGuaranteedCmp/eq.rs rename to tests/kani/Intrinsics/PtrGuaranteedCmp/cmp.rs index aaf93928cb0a..cdfebf108869 100644 --- a/tests/kani/Intrinsics/PtrGuaranteedCmp/eq.rs +++ b/tests/kani/Intrinsics/PtrGuaranteedCmp/cmp.rs @@ -4,16 +4,16 @@ // Checks that `ptr_guaranteed_eq` returns true if the pointers are equal, false // otherwise. #![feature(core_intrinsics)] -use std::intrinsics::ptr_guaranteed_eq; +use std::intrinsics::ptr_guaranteed_cmp; #[kani::proof] -fn test_ptr_eq_eq(ptr1: *const u8, ptr2: *const u8) { +fn test_ptr_eq(ptr1: *const u8, ptr2: *const u8) { kani::assume(ptr1 == ptr2); - assert!(ptr_guaranteed_eq(ptr1, ptr2)); + assert_eq!(ptr_guaranteed_cmp(ptr1, ptr2), 1); } #[kani::proof] -fn test_ptr_eq_ne(ptr1: *const u8, ptr2: *const u8) { +fn test_ptr_ne(ptr1: *const u8, ptr2: *const u8) { kani::assume(ptr1 != ptr2); - assert!(!ptr_guaranteed_eq(ptr1, ptr2)); + assert_eq!(ptr_guaranteed_cmp(ptr1, ptr2), 0); } diff --git a/tests/kani/Intrinsics/PtrGuaranteedCmp/ne.rs b/tests/kani/Intrinsics/PtrGuaranteedCmp/ne.rs deleted file mode 100644 index 15336d925781..000000000000 --- a/tests/kani/Intrinsics/PtrGuaranteedCmp/ne.rs +++ /dev/null @@ -1,19 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Checks that `ptr_guaranteed_ne` returns true if the pointers are different, -// false otherwise. -#![feature(core_intrinsics)] -use std::intrinsics::ptr_guaranteed_ne; - -#[kani::proof] -fn test_ptr_ne_ne(ptr1: *const u8, ptr2: *const u8) { - kani::assume(ptr1 != ptr2); - assert!(ptr_guaranteed_ne(ptr1, ptr2)); -} - -#[kani::proof] -fn test_ptr_ne_eq(ptr1: *const u8, ptr2: *const u8) { - kani::assume(ptr1 == ptr2); - assert!(!ptr_guaranteed_ne(ptr1, ptr2)); -}