From 26706b48a9f44570ff59ff3db301e2f33dbe0d83 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Wed, 26 Feb 2025 17:49:19 -0500 Subject: [PATCH 01/10] Update toolchain to 2025-02-27 Changes to attribute parsing and representation https://github.com/rust-lang/rust/pull/135726 Map methods moved to `TyCtx` https://github.com/rust-lang/rust/pull/137162 https://github.com/rust-lang/rust/pull/137397 Remove `BackendRepr::Unihabited` https://github.com/rust-lang/rust/pull/136985 --- .../codegen_cprover_gotoc/codegen/contract.rs | 4 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 6 +- .../codegen/statement.rs | 7 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 8 +- kani-compiler/src/kani_middle/attributes.rs | 102 +++++++++++------- kani-compiler/src/kani_middle/intrinsics.rs | 2 +- kani-compiler/src/kani_middle/resolve.rs | 4 +- .../src/kani_middle/transform/check_values.rs | 1 - rust-toolchain.toml | 2 +- 9 files changed, 79 insertions(+), 57 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 254fc854e8b5..d3d4481bf258 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -63,9 +63,7 @@ impl GotocCtx<'_> { // Return item tagged with `#[kanitool::recursion_tracker]` let mut recursion_trackers = items.iter().filter_map(|item| { let MonoItem::Static(static_item) = item else { return None }; - if !static_item - .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()]) - .is_empty() + if !static_item.tool_attrs(&["kanitool".into(), "recursion_tracker".into()]).is_empty() { let span = static_item.span(); let loc = self.codegen_span_stable(span); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 0c2a81c3082c..f2327b51b6ad 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1002,8 +1002,10 @@ impl GotocCtx<'_> { // https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247 // See also the cranelift backend: // https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116 - let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()], + let offset: rustc_abi::Size = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => { + offsets[rustc_abi::FieldIdx::from_usize(0)] + } _ => unreachable!("niche encoding must have arbitrary fields"), }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 813e07d06723..0ffa893056be 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -7,6 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_cov use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; +use rustc_abi::Size; use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{List, TypingEnv}; @@ -350,8 +351,10 @@ impl GotocCtx<'_> { } TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { if *untagged_variant != variant_index_internal { - let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()], + let offset: Size = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => { + offsets[rustc_abi::FieldIdx::from_usize(0)] + } _ => unreachable!("niche encoding must have arbitrary fields"), }; let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index a22528d55407..efbcbe2e06e5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -718,7 +718,7 @@ impl<'tcx> GotocCtx<'tcx> { let mut final_fields = Vec::with_capacity(flds.len()); let mut offset = initial_offset; for idx in layout.fields.index_by_increasing_offset() { - let fld_offset = offsets[idx.into()]; + let fld_offset = offsets[rustc_abi::FieldIdx::from(idx)]; let (fld_name, fld_ty) = &flds[idx]; if let Some(padding) = self.codegen_struct_padding(offset, fld_offset, final_fields.len()) @@ -1557,9 +1557,9 @@ impl<'tcx> GotocCtx<'tcx> { let components = fields_shape .index_by_increasing_offset() .map(|idx| { - let idx = idx.into(); - let name = fields[idx].name.to_string().intern(); - let field_ty = fields[idx].ty(ctx.tcx, adt_args); + let fidx = FieldIdx::from(idx); + let name = fields[fidx].name.to_string().intern(); + let field_ty = fields[fidx].ty(ctx.tcx, adt_args); let typ = if !ctx.is_zst(field_ty) { last_type.clone() } else { diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index bdd6db831d6c..5f38beb66202 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -8,7 +8,7 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr}; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{AttrArgs, AttrKind, Attribute, def::DefKind, def_id::DefId}; +use rustc_hir::{AttrArgs, Attribute, def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; @@ -214,7 +214,7 @@ impl<'tcx> KaniAttributes<'tcx> { .resolve_from_mod(name.as_str()) .map_err(|e| { let mut err = self.tcx.dcx().struct_span_err( - attr.span, + attr.span(), format!( "Failed to resolve replacement function {}: {e}", name.as_str() @@ -229,7 +229,7 @@ impl<'tcx> KaniAttributes<'tcx> { err.emit(); }) .ok()?; - Some((name, def, attr.span)) + Some((name, def, attr.span())) }) .collect() } @@ -247,10 +247,10 @@ impl<'tcx> KaniAttributes<'tcx> { self.expect_maybe_one(KaniAttributeKind::ProofForContract).and_then(|target| { let name = expect_key_string_value(self.tcx.sess, target).ok()?; self.resolve_from_mod(name.as_str()) - .map(|ok| (name, ok, target.span)) + .map(|ok| (name, ok, target.span())) .map_err(|resolve_err| { let mut err = self.tcx.dcx().struct_span_err( - target.span, + target.span(), format!( "Failed to resolve checking function {} because {resolve_err}", name.as_str() @@ -336,7 +336,7 @@ impl<'tcx> KaniAttributes<'tcx> { // Check that all attributes are correctly used and well formed. let is_harness = self.is_proof_harness(); for (&kind, attrs) in self.map.iter() { - let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg); + let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span(), msg); if !is_harness && kind.is_harness_only() { local_error(format!( @@ -451,7 +451,7 @@ impl<'tcx> KaniAttributes<'tcx> { kind.as_ref() ); if let Some(attr) = self.map.get(&kind).unwrap().first() { - self.tcx.dcx().span_err(attr.span, msg); + self.tcx.dcx().span_err(attr.span(), msg); } else { self.tcx.dcx().err(msg); } @@ -646,7 +646,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Check that if this item is tagged with a proof_attribute, it is a valid harness. fn check_proof_attribute(&self, kind: KaniAttributeKind, proof_attribute: &Attribute) { - let span = proof_attribute.span; + let span = proof_attribute.span(); let tcx = self.tcx; if let KaniAttributeKind::Proof = kind { expect_no_args(tcx, kind, proof_attribute); @@ -719,7 +719,7 @@ fn expect_key_string_value( sess: &Session, attr: &Attribute, ) -> Result { - let span = attr.span; + let span = attr.span(); let AttrArgs::Eq { expr, .. } = &attr.get_normal_item().args else { return Err(sess .dcx() @@ -743,7 +743,7 @@ fn expect_single<'a>( .expect(&format!("expected at least one attribute {} in {attributes:?}", kind.as_ref())); if attributes.len() > 1 { tcx.dcx().span_err( - attr.span, + attr.span(), format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()), ); } @@ -774,7 +774,7 @@ impl UnstableAttrParseError<'_> { fn report(&self, tcx: TyCtxt) -> ErrorGuaranteed { tcx.dcx() .struct_span_err( - self.attr.span, + self.attr.span(), format!("failed to parse `#[kani::unstable_feature]`: {}", self.reason), ) .with_note(format!( @@ -817,7 +817,7 @@ impl<'a> TryFrom<&'a Attribute> for UnstableAttribute { fn expect_no_args(tcx: TyCtxt, kind: KaniAttributeKind, attr: &Attribute) { if !attr.is_word() { tcx.dcx() - .struct_span_err(attr.span, format!("unexpected argument for `{}`", kind.as_ref())) + .struct_span_err(attr.span(), format!("unexpected argument for `{}`", kind.as_ref())) .with_help("remove the extra argument") .emit(); } @@ -830,7 +830,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { None => { // There are no integers or too many arguments given to the attribute tcx.dcx().span_err( - attr.span, + attr.span(), "invalid argument for `unwind` attribute, expected an integer", ); None @@ -839,7 +839,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option { if let Ok(val) = unwind_integer_value.try_into() { Some(val) } else { - tcx.dcx().span_err(attr.span, "value above maximum permitted value - u32::MAX"); + tcx.dcx().span_err(attr.span(), "value above maximum permitted value - u32::MAX"); None } } @@ -854,13 +854,13 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec { /* no-op */ } Ok(FnResolution::FnImpl { .. }) => { tcx.dcx().span_err( - attr.span, + attr.span(), "Kani currently does not support stubbing trait implementations.", ); } Err(err) => { tcx.dcx().span_err( - attr.span, + attr.span(), format!("failed to resolve `{}`: {err}", pretty_type_path(path)), ); } @@ -871,7 +871,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec Vec { tcx.dcx().span_err( - attr.span, + attr.span(), format!( "attribute `kani::stub` takes two path arguments; found {}", paths.len() @@ -912,7 +912,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { const ATTRIBUTE: &str = "#[kani::solver]"; let invalid_arg_err = |attr: &Attribute| { tcx.dcx().span_err( - attr.span, + attr.span(), format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"\"`)"), ) }; @@ -920,7 +920,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { let attr_args = attr.meta_item_list().unwrap(); if attr_args.len() != 1 { tcx.dcx().span_err( - attr.span, + attr.span(), format!( "the `{ATTRIBUTE}` attribute expects a single argument. Got {} arguments.", attr_args.len() @@ -943,7 +943,7 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option { match solver { Ok(solver) => Some(solver), Err(_) => { - tcx.dcx().span_err(attr.span, format!("unknown solver `{ident_str}`")); + tcx.dcx().span_err(attr.span(), format!("unknown solver `{ident_str}`")); None } } @@ -1016,27 +1016,47 @@ fn parse_str_value(attr: &Attribute) -> Option { /// If the attribute is named `kanitool::name`, this extracts `name` fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { - match &attr.kind { - AttrKind::Normal(normal) => { - let segments = &normal.path.segments; - if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { - let ident_str = segments[1..] - .iter() - .map(|segment| segment.as_str()) - .intersperse("::") - .collect::(); - KaniAttributeKind::try_from(ident_str.as_str()) - .inspect_err(|&err| { - debug!(?err, "attr_kind_failed"); - tcx.dcx().span_err(attr.span, format!("unknown attribute `{ident_str}`")); - }) - .ok() - } else { - None - } + if let Attribute::Unparsed(normal) = attr { + let segments = &normal.path.segments; + if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { + let ident_str = segments[1..] + .iter() + .map(|segment| segment.as_str()) + .intersperse("::") + .collect::(); + KaniAttributeKind::try_from(ident_str.as_str()) + .inspect_err(|&err| { + debug!(?err, "attr_kind_failed"); + tcx.dcx().span_err(attr.span(), format!("unknown attribute `{ident_str}`")); + }) + .ok() + } else { + None } - _ => None, + } else { + None } + // match &attr.kind { + // AttrKind::Normal(normal) => { + // let segments = &normal.path.segments; + // if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { + // let ident_str = segments[1..] + // .iter() + // .map(|segment| segment.as_str()) + // .intersperse("::") + // .collect::(); + // KaniAttributeKind::try_from(ident_str.as_str()) + // .inspect_err(|&err| { + // debug!(?err, "attr_kind_failed"); + // tcx.dcx().span_err(attr.span(), format!("unknown attribute `{ident_str}`")); + // }) + // .ok() + // } else { + // None + // } + // } + // _ => None, + // } } /// Parse an attribute using `syn`. @@ -1099,7 +1119,7 @@ fn pretty_type_path(path: &TypePath) -> String { /// Retrieve the value of the `fn_marker` attribute for the given definition if it has one. pub(crate) fn fn_marker(def: T) -> Option { let fn_marker: [SymbolStable; 2] = ["kanitool".into(), "fn_marker".into()]; - let marker = def.attrs_by_path(&fn_marker).pop()?; + let marker = def.tool_attrs(&fn_marker).pop()?; let attribute = syn_attr_stable(&marker); let meta_name = attribute.meta.require_name_value().unwrap_or_else(|_| { panic!("Expected name value attribute for `kanitool::fn_marker`, but found: `{:?}`", marker) diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index a3451c99e029..a53abef90e88 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -93,7 +93,7 @@ fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx> ty::Adt(def, args) => { assert!(def.repr().simd(), "`simd_size_and_type` called on non-SIMD type"); let variant = def.non_enum_variant(); - let f0_ty = variant.fields[0u32.into()].ty(tcx, args); + let f0_ty = variant.fields[rustc_abi::FieldIdx::from_usize(0)].ty(tcx, args); match f0_ty.kind() { ty::Array(elem_ty, len) => (*len, *elem_ty), diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 8f278ae20ed8..accb4807f00e 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -307,7 +307,7 @@ fn resolve_prefix<'tcx>( (None, Some(segment)) if segment.ident == CRATE => { // Find the module at the root of the crate. let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module); - let crate_root = match tcx.hir().parent_iter(current_module_hir_id).last() { + let crate_root = match tcx.hir_parent_iter(current_module_hir_id).last() { None => current_module, Some((hir_id, _)) => hir_id.owner.def_id, }; @@ -366,7 +366,7 @@ where I: Iterator, { let current_module_hir_id = tcx.local_def_id_to_hir_id(current_module); - let mut parents = tcx.hir().parent_iter(current_module_hir_id); + let mut parents = tcx.hir_parent_iter(current_module_hir_id); let mut base_module = current_module; while segments.next_if(|segment| segment.ident == SUPER).is_some() { if let Some((parent, _)) = parents.next() { diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 8689bf6c59ac..b536de1e2695 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -213,7 +213,6 @@ impl ValidValueReq { } ValueAbi::Scalar(_) | ValueAbi::ScalarPair(_, _) - | ValueAbi::Uninhabited | ValueAbi::Vector { .. } | ValueAbi::Aggregate { .. } => None, } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 8078beff6d73..199e68771cbc 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-02-21" +channel = "nightly-2025-02-27" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From d9ad6e17d6cef2e6f49161ab70e327a96525fb13 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 27 Feb 2025 12:51:01 -0500 Subject: [PATCH 02/10] Intrinsics `rint`, `roundeven`, `nearbyint` replaced by `round_ties_even`. Propagate changes from https://github.com/rust-lang/rust/pull/136543 Use `__sort_of_CPROVER_round_to_integral` to model `round_ties_even`. Update tests. --- cprover_bindings/src/goto_program/builtin.rs | 13 ++- cprover_bindings/src/machine_model.rs | 1 + docs/src/rust-feature-support/intrinsics.md | 8 +- .../codegen/intrinsic.rs | 39 ++++++- kani-compiler/src/intrinsics.rs | 30 ++--- .../points_to/points_to_analysis.rs | 4 - .../check_uninit/ptr_uninit/uninit_visitor.rs | 4 - .../Intrinsics/Math/Rounding/RInt/rintf32.rs | 104 ------------------ .../Intrinsics/Math/Rounding/RInt/rintf64.rs | 104 ------------------ .../round_ties_even_f32.rs} | 20 ++-- .../round_ties_even_f64.rs} | 20 ++-- 11 files changed, 82 insertions(+), 265 deletions(-) delete mode 100644 tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs delete mode 100644 tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs rename tests/kani/Intrinsics/Math/Rounding/{NearbyInt/nearbyintf32.rs => RoundTiesEven/round_ties_even_f32.rs} (79%) rename tests/kani/Intrinsics/Math/Rounding/{NearbyInt/nearbyintf64.rs => RoundTiesEven/round_ties_even_f64.rs} (79%) diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index a0c1f211b5e2..0ff2296a1024 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -6,7 +6,7 @@ use super::{Expr, Location, Symbol, Type}; use std::fmt::Display; -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone, Copy, PartialEq)] pub enum BuiltinFn { Abort, Assert, @@ -59,6 +59,8 @@ pub enum BuiltinFn { Rintf, Round, Roundf, + RoundToIntegralF, + RoundToIntegral, Sin, Sinf, Sqrt, @@ -123,6 +125,9 @@ impl Display for BuiltinFn { Rintf => "rintf", Round => "round", Roundf => "roundf", + // TODO remove the sort_of prefix once we move up from CBMC 6.4.1 + RoundToIntegralF => "__sort_of_CPROVER_round_to_integralf", + RoundToIntegral => "__sort_of_CPROVER_round_to_integral", Sin => "sin", Sinf => "sinf", Sqrt => "sqrt", @@ -188,6 +193,8 @@ impl BuiltinFn { Rintf => vec![Type::float()], Round => vec![Type::double()], Roundf => vec![Type::float()], + RoundToIntegralF => vec![Type::c_int(), Type::float()], + RoundToIntegral => vec![Type::c_int(), Type::double()], Sin => vec![Type::double()], Sinf => vec![Type::float()], Sqrt => vec![Type::double()], @@ -252,6 +259,8 @@ impl BuiltinFn { Rintf => Type::float(), Round => Type::double(), Roundf => Type::float(), + RoundToIntegralF => Type::float(), + RoundToIntegral => Type::double(), Sin => Type::double(), Sinf => Type::float(), Sqrt => Type::double(), @@ -316,6 +325,8 @@ impl BuiltinFn { Rintf, Round, Roundf, + RoundToIntegralF, + RoundToIntegral, Sin, Sinf, Sqrt, diff --git a/cprover_bindings/src/machine_model.rs b/cprover_bindings/src/machine_model.rs index 31427a83a629..463fe8f047e6 100644 --- a/cprover_bindings/src/machine_model.rs +++ b/cprover_bindings/src/machine_model.rs @@ -45,6 +45,7 @@ pub enum RoundingMode { Downward = 1, Upward = 2, TowardsZero = 3, + ToAway = 4, } impl From for BigInt { diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 9f3495da0adc..2fa8b54094fc 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -180,8 +180,6 @@ minnumf32 | Yes | | minnumf64 | Yes | | move_val_init | No | | mul_with_overflow | Yes | | -nearbyintf32 | Yes | | -nearbyintf64 | Yes | | needs_drop | Yes | | nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | @@ -198,8 +196,10 @@ ptr_guaranteed_eq | Yes | | ptr_guaranteed_ne | Yes | | ptr_offset_from | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-4) | raw_eq | Partial | Cannot detect [uninitialized memory](#uninitialized-memory) | -rintf32 | Yes | | -rintf64 | Yes | | +round_ties_even_f16 | No | | +round_ties_even_f32 | Yes | | +round_ties_even_f64 | Yes | | +round_ties_even_f128 | No | | rotate_left | Yes | | rotate_right | Yes | | roundf32 | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index bbdc0be7910a..ac5b44ec4163 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -414,8 +414,6 @@ impl GotocCtx<'_> { Intrinsic::MulWithOverflow => { self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc) } - Intrinsic::NearbyIntF32 => codegen_simple_intrinsic!(Nearbyintf), - Intrinsic::NearbyIntF64 => codegen_simple_intrinsic!(Nearbyint), Intrinsic::NeedsDrop => codegen_intrinsic_const!(), Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf), Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow), @@ -425,12 +423,24 @@ impl GotocCtx<'_> { Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), - Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), - Intrinsic::RintF64 => codegen_simple_intrinsic!(Rint), Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol), Intrinsic::RotateRight => codegen_intrinsic_binop!(ror), Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf), Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round), + Intrinsic::RoundTiesEvenF32 => self.codegen_round_to_integral( + BuiltinFn::RoundToIntegralF, + cbmc::RoundingMode::ToNearest, + fargs, + place, + loc, + ), + Intrinsic::RoundTiesEvenF64 => self.codegen_round_to_integral( + BuiltinFn::RoundToIntegral, + cbmc::RoundingMode::ToNearest, + fargs, + place, + loc, + ), Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add), Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub), Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf), @@ -638,6 +648,27 @@ impl GotocCtx<'_> { dividend_is_int_min.and(divisor_is_minus_one).not() } + // Builds a call to the round_to_integral CPROVER function with specified cbmc::RoundingMode. + fn codegen_round_to_integral( + &mut self, + function: BuiltinFn, + rounding_mode: cbmc::RoundingMode, + mut fargs: Vec, + place: &Place, + loc: Location, + ) -> Stmt { + assert!(function == BuiltinFn::RoundToIntegralF || function == BuiltinFn::RoundToIntegral); + let mm = self.symbol_table.machine_model(); + fargs.insert(0, Expr::int_constant(rounding_mode, Type::c_int())); + let casted_fargs = Expr::cast_arguments_to_target_equivalent_function_parameter_types( + &function.as_expr(), + fargs, + mm, + ); + let expr = function.call(casted_fargs, loc); + self.codegen_expr_to_place_stable(place, expr, loc) + } + /// Intrinsics of the form *_with_overflow fn codegen_op_with_overflow( &mut self, diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index f58a40bf8cb6..5d9ab8221453 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -86,8 +86,6 @@ pub enum Intrinsic { MinNumF32, MinNumF64, MulWithOverflow, - NearbyIntF32, - NearbyIntF64, NeedsDrop, PowF32, PowF64, @@ -99,12 +97,12 @@ pub enum Intrinsic { PtrOffsetFromUnsigned, RawEq, RetagBoxToRaw, - RintF32, - RintF64, RotateLeft, RotateRight, RoundF32, RoundF64, + RoundTiesEvenF32, + RoundTiesEvenF64, SaturatingAdd, SaturatingSub, SinF32, @@ -676,10 +674,6 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::MinNumF32) } - "nearbyintf32" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); - Some(Intrinsic::NearbyIntF32) - } "powf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::PowF32) @@ -688,14 +682,14 @@ fn try_match_f32(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::PowIF32) } - "rintf32" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); - Some(Intrinsic::RintF32) - } "roundf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::RoundF32) } + "round_ties_even_f32" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); + Some(Intrinsic::RoundTiesEvenF32) + } "sinf32" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32)); Some(Intrinsic::SinF32) @@ -770,10 +764,6 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::MinNumF64) } - "nearbyintf64" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); - Some(Intrinsic::NearbyIntF64) - } "powf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::PowF64) @@ -782,14 +772,14 @@ fn try_match_f64(intrinsic_instance: &Instance) -> Option { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::PowIF64) } - "rintf64" => { - assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); - Some(Intrinsic::RintF64) - } "roundf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::RoundF64) } + "round_ties_even_f64" => { + assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); + Some(Intrinsic::RoundTiesEvenF64) + } "sinf64" => { assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64)); Some(Intrinsic::SinF64) 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 a89baf963e7f..591d8c3574ff 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 @@ -664,8 +664,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::MinNumF32 | Intrinsic::MinNumF64 | Intrinsic::MulWithOverflow - | Intrinsic::NearbyIntF32 - | Intrinsic::NearbyIntF64 | Intrinsic::NeedsDrop | Intrinsic::PowF32 | Intrinsic::PowF64 @@ -677,8 +675,6 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PtrOffsetFromUnsigned | Intrinsic::RawEq | Intrinsic::RetagBoxToRaw - | Intrinsic::RintF32 - | Intrinsic::RintF64 | Intrinsic::RotateLeft | Intrinsic::RotateRight | Intrinsic::RoundF32 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 20f4538453b5..02d928eff75e 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 @@ -625,8 +625,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::MinNumF32 | Intrinsic::MinNumF64 | Intrinsic::MulWithOverflow - | Intrinsic::NearbyIntF32 - | Intrinsic::NearbyIntF64 | Intrinsic::NeedsDrop | Intrinsic::PowF32 | Intrinsic::PowF64 @@ -634,8 +632,6 @@ fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::PowIF64 | Intrinsic::PrefAlignOf | Intrinsic::RawEq - | Intrinsic::RintF32 - | Intrinsic::RintF64 | Intrinsic::RotateLeft | Intrinsic::RotateRight | Intrinsic::RoundF32 diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs deleted file mode 100644 index 79a0a4f9be2c..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs +++ /dev/null @@ -1,104 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Checks that `rintf32` returns the nearest integer to the argument. The -// default rounding mode is rounding half to even, which is described here: -// https://en.wikipedia.org/wiki/Rounding#Round_half_to_even -// -// `rintf32` works like `nearbyintf32`, but it may raise an inexact -// floating-point exception which isn't supported in Rust: -// https://github.com/rust-lang/rust/issues/10186 -// So in practice, `rintf32` and `nearbyintf32` work the same way. -#![feature(core_intrinsics)] -use std::intrinsics::rintf32; - -#[kani::proof] -fn test_one() { - let one = 1.0; - let result = unsafe { rintf32(one) }; - assert!(result == 1.0); -} - -#[kani::proof] -fn test_one_frac() { - let one_frac = 1.9; - let result = unsafe { rintf32(one_frac) }; - assert!(result == 2.0); -} - -#[kani::proof] -fn test_half_down() { - let one_frac = 2.5; - let result = unsafe { rintf32(one_frac) }; - assert!(result == 2.0); -} - -#[kani::proof] -fn test_half_up() { - let one_frac = 3.5; - let result = unsafe { rintf32(one_frac) }; - assert!(result == 4.0); -} - -#[kani::proof] -fn test_conc() { - let conc = -42.6; - let result = unsafe { rintf32(conc) }; - assert!(result == -43.0); -} - -#[kani::proof] -fn test_conc_sci() { - let conc = 5.4e-2; - let result = unsafe { rintf32(conc) }; - assert!(result == 0.0); -} - -#[kani::proof] -fn test_towards_nearest() { - let x: f32 = kani::any(); - kani::assume(!x.is_nan()); - kani::assume(!x.is_infinite()); - let result = unsafe { rintf32(x) }; - let frac = x.fract().abs(); - if x.is_sign_positive() { - if frac > 0.5 { - assert!(result > x); - } else if frac < 0.5 { - assert!(result <= x); - } else { - // This would fail if conversion checks were on - let integer = x as i64; - if integer % 2 == 0 { - assert!(result < x); - } else { - assert!(result > x); - } - } - } else { - if frac > 0.5 { - assert!(result < x); - } else if frac < 0.5 { - assert!(result >= x); - } else { - // This would fail if conversion checks were on - let integer = x as i64; - if integer % 2 == 0 { - assert!(result > x); - } else { - assert!(result < x); - } - } - } -} - -#[kani::proof] -fn test_diff_half_one() { - let x: f32 = kani::any(); - kani::assume(!x.is_nan()); - kani::assume(!x.is_infinite()); - let result = unsafe { rintf32(x) }; - let diff = (x - result).abs(); - assert!(diff <= 0.5); - assert!(diff >= 0.0); -} diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs deleted file mode 100644 index 8c8ea583a2d5..000000000000 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs +++ /dev/null @@ -1,104 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// Checks that `rintf64` returns the nearest integer to the argument. The -// default rounding mode is rounding half to even, which is described here: -// https://en.wikipedia.org/wiki/Rounding#Round_half_to_even -// -// `rintf64` works like `nearbyintf64`, but it may raise an inexact -// floating-point exception which isn't supported in Rust: -// https://github.com/rust-lang/rust/issues/10186 -// So in practice, `rintf64` and `nearbyintf64` work the same way. -#![feature(core_intrinsics)] -use std::intrinsics::rintf64; - -#[kani::proof] -fn test_one() { - let one = 1.0; - let result = unsafe { rintf64(one) }; - assert!(result == 1.0); -} - -#[kani::proof] -fn test_one_frac() { - let one_frac = 1.9; - let result = unsafe { rintf64(one_frac) }; - assert!(result == 2.0); -} - -#[kani::proof] -fn test_half_down() { - let one_frac = 2.5; - let result = unsafe { rintf64(one_frac) }; - assert!(result == 2.0); -} - -#[kani::proof] -fn test_half_up() { - let one_frac = 3.5; - let result = unsafe { rintf64(one_frac) }; - assert!(result == 4.0); -} - -#[kani::proof] -fn test_conc() { - let conc = -42.6; - let result = unsafe { rintf64(conc) }; - assert!(result == -43.0); -} - -#[kani::proof] -fn test_conc_sci() { - let conc = 5.4e-2; - let result = unsafe { rintf64(conc) }; - assert!(result == 0.0); -} - -#[kani::proof] -fn test_towards_nearest() { - let x: f64 = kani::any(); - kani::assume(!x.is_nan()); - kani::assume(!x.is_infinite()); - let result = unsafe { rintf64(x) }; - let frac = x.fract().abs(); - if x.is_sign_positive() { - if frac > 0.5 { - assert!(result > x); - } else if frac < 0.5 { - assert!(result <= x); - } else { - // This would fail if conversion checks were on - let integer = x as i64; - if integer % 2 == 0 { - assert!(result < x); - } else { - assert!(result > x); - } - } - } else { - if frac > 0.5 { - assert!(result < x); - } else if frac < 0.5 { - assert!(result >= x); - } else { - // This would fail if conversion checks were on - let integer = x as i64; - if integer % 2 == 0 { - assert!(result > x); - } else { - assert!(result < x); - } - } - } -} - -#[kani::proof] -fn test_diff_half_one() { - let x: f64 = kani::any(); - kani::assume(!x.is_nan()); - kani::assume(!x.is_infinite()); - let result = unsafe { rintf64(x) }; - let diff = (x - result).abs(); - assert!(diff <= 0.5); - assert!(diff >= 0.0); -} diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs similarity index 79% rename from tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs rename to tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs index 25e02f45a943..057483b3b0cc 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f32.rs @@ -1,51 +1,51 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `nearbyintf32` returns the nearest integer to the argument. The +// Checks that `round_ties_even_f32` returns the nearest integer to the argument. The // default rounding mode is rounding half to even, which is described here: // https://en.wikipedia.org/wiki/Rounding#Round_half_to_even #![feature(core_intrinsics)] -use std::intrinsics::nearbyintf32; +use std::intrinsics::round_ties_even_f32; #[kani::proof] fn test_one() { let one = 1.0; - let result = unsafe { nearbyintf32(one) }; + let result = round_ties_even_f32(one); assert!(result == 1.0); } #[kani::proof] fn test_one_frac() { let one_frac = 1.9; - let result = unsafe { nearbyintf32(one_frac) }; + let result = round_ties_even_f32(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_down() { let one_frac = 2.5; - let result = unsafe { nearbyintf32(one_frac) }; + let result = round_ties_even_f32(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_up() { let one_frac = 3.5; - let result = unsafe { nearbyintf32(one_frac) }; + let result = round_ties_even_f32(one_frac); assert!(result == 4.0); } #[kani::proof] fn test_conc() { let conc = -42.6; - let result = unsafe { nearbyintf32(conc) }; + let result = round_ties_even_f32(conc); assert!(result == -43.0); } #[kani::proof] fn test_conc_sci() { let conc = 5.4e-2; - let result = unsafe { nearbyintf32(conc) }; + let result = round_ties_even_f32(conc); assert!(result == 0.0); } @@ -54,7 +54,7 @@ fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = unsafe { nearbyintf32(x) }; + let result = round_ties_even_f32(x); let frac = x.fract().abs(); if x.is_sign_positive() { if frac > 0.5 { @@ -92,7 +92,7 @@ fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = unsafe { nearbyintf32(x) }; + let result = round_ties_even_f32(x); let diff = (x - result).abs(); assert!(diff <= 0.5); assert!(diff >= 0.0); diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs similarity index 79% rename from tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs rename to tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs index 589a44a4d1ac..c7c1a9611bae 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RoundTiesEven/round_ties_even_f64.rs @@ -1,51 +1,51 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Checks that `nearbyintf64` returns the nearest integer to the argument. The +// Checks that `round_ties_even_f64` returns the nearest integer to the argument. The // default rounding mode is rounding half to even, which is described here: // https://en.wikipedia.org/wiki/Rounding#Round_half_to_even #![feature(core_intrinsics)] -use std::intrinsics::nearbyintf64; +use std::intrinsics::round_ties_even_f64; #[kani::proof] fn test_one() { let one = 1.0; - let result = unsafe { nearbyintf64(one) }; + let result = round_ties_even_f64(one); assert!(result == 1.0); } #[kani::proof] fn test_one_frac() { let one_frac = 1.9; - let result = unsafe { nearbyintf64(one_frac) }; + let result = round_ties_even_f64(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_down() { let one_frac = 2.5; - let result = unsafe { nearbyintf64(one_frac) }; + let result = round_ties_even_f64(one_frac); assert!(result == 2.0); } #[kani::proof] fn test_half_up() { let one_frac = 3.5; - let result = unsafe { nearbyintf64(one_frac) }; + let result = round_ties_even_f64(one_frac); assert!(result == 4.0); } #[kani::proof] fn test_conc() { let conc = -42.6; - let result = unsafe { nearbyintf64(conc) }; + let result = round_ties_even_f64(conc); assert!(result == -43.0); } #[kani::proof] fn test_conc_sci() { let conc = 5.4e-2; - let result = unsafe { nearbyintf64(conc) }; + let result = round_ties_even_f64(conc); assert!(result == 0.0); } @@ -54,7 +54,7 @@ fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = unsafe { nearbyintf64(x) }; + let result = round_ties_even_f64(x); let frac = x.fract().abs(); if x.is_sign_positive() { if frac > 0.5 { @@ -92,7 +92,7 @@ fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); kani::assume(!x.is_infinite()); - let result = unsafe { nearbyintf64(x) }; + let result = round_ties_even_f64(x); let diff = (x - result).abs(); assert!(diff <= 0.5); assert!(diff >= 0.0); From 80fd315c91584416f31efc79d532bcdd3fc138b5 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 27 Feb 2025 13:00:36 -0500 Subject: [PATCH 03/10] Rename `sub_ptr` to `offset_from_unsigned`. Propagate changes from https://github.com/rust-lang/rust/pull/137483 The feature gate is still `ptr_sub_ptr`. --- .../src/kani_middle/kani_functions.rs | 4 +-- .../kani_middle/transform/rustc_intrinsics.rs | 4 ++- library/kani_core/src/models.rs | 4 +-- ...expected => offset_from_unsigned.expected} | 20 ++++++------- .../{sub_ptr.rs => offset_from_unsigned.rs} | 28 +++++++++---------- tests/kani/PointerOffset/offset_from_vec.rs | 2 +- 6 files changed, 32 insertions(+), 30 deletions(-) rename tests/expected/offset-bounds-check/{sub_ptr.expected => offset_from_unsigned.expected} (52%) rename tests/expected/offset-bounds-check/{sub_ptr.rs => offset_from_unsigned.rs} (62%) diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 01d237bf0773..85936041cc38 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -87,8 +87,8 @@ pub enum KaniModel { Offset, #[strum(serialize = "PtrOffsetFromModel")] PtrOffsetFrom, - #[strum(serialize = "PtrSubPtrModel")] - PtrSubPtr, + #[strum(serialize = "PtrOffsetFromUnsignedModel")] + PtrOffsetFromUnsigned, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 79238e423e62..43f8e5b7013f 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -168,7 +168,9 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom], - Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr], + Intrinsic::PtrOffsetFromUnsigned => { + self.models[&KaniModel::PtrOffsetFromUnsigned] + } // The rest is handled in codegen. _ => { return self.super_terminator(term); diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 8913c399c959..39fd786f0249 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -89,8 +89,8 @@ macro_rules! generate_models { } } - #[kanitool::fn_marker = "PtrSubPtrModel"] - pub unsafe fn ptr_sub_ptr(ptr1: *const T, ptr2: *const T) -> usize { + #[kanitool::fn_marker = "PtrOffsetFromUnsignedModel"] + pub unsafe fn ptr_offset_from_unsigned(ptr1: *const T, ptr2: *const T) -> usize { let offset = ptr_offset_from(ptr1, ptr2); kani::safety_check(offset >= 0, "Expected non-negative distance between pointers"); offset as usize diff --git a/tests/expected/offset-bounds-check/sub_ptr.expected b/tests/expected/offset-bounds-check/offset_from_unsigned.expected similarity index 52% rename from tests/expected/offset-bounds-check/sub_ptr.expected rename to tests/expected/offset-bounds-check/offset_from_unsigned.expected index 611fe2e565c7..fff02a3d96af 100644 --- a/tests/expected/offset-bounds-check/sub_ptr.expected +++ b/tests/expected/offset-bounds-check/offset_from_unsigned.expected @@ -1,29 +1,29 @@ -Checking harness check_sub_ptr_same_dangling... +Checking harness check_offset_from_unsigned_same_dangling... VERIFICATION:- SUCCESSFUL -Checking harness check_sub_ptr_unit_panic... +Checking harness check_offset_from_unsigned_unit_panic... Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) -Checking harness check_sub_ptr_negative_result... +Checking harness check_offset_from_unsigned_negative_result... Failed Checks: Expected non-negative distance between pointers VERIFICATION:- FAILED -Checking harness check_sub_ptr_diff_alloc... +Checking harness check_offset_from_unsigned_diff_alloc... Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED -Checking harness check_sub_ptr_oob_ptr... +Checking harness check_offset_from_unsigned_oob_ptr... Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED -Checking harness check_sub_ptr_self_oob... +Checking harness check_offset_from_unsigned_self_oob... Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED Summary: -Verification failed for - check_sub_ptr_negative_result -Verification failed for - check_sub_ptr_diff_alloc -Verification failed for - check_sub_ptr_oob_ptr -Verification failed for - check_sub_ptr_self_oob +Verification failed for - check_offset_from_unsigned_negative_result +Verification failed for - check_offset_from_unsigned_diff_alloc +Verification failed for - check_offset_from_unsigned_oob_ptr +Verification failed for - check_offset_from_unsigned_self_oob Complete - 2 successfully verified harnesses, 4 failures, 6 total. diff --git a/tests/expected/offset-bounds-check/sub_ptr.rs b/tests/expected/offset-bounds-check/offset_from_unsigned.rs similarity index 62% rename from tests/expected/offset-bounds-check/sub_ptr.rs rename to tests/expected/offset-bounds-check/offset_from_unsigned.rs index 7ddfa96d94f8..f5b11a741403 100644 --- a/tests/expected/offset-bounds-check/sub_ptr.rs +++ b/tests/expected/offset-bounds-check/offset_from_unsigned.rs @@ -1,47 +1,47 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that Kani can detect UB due to `sub_ptr` with out-of-bounds pointer or wrong order. +//! Check that Kani can detect UB due to `offset_from_unsigned` with out-of-bounds pointer or wrong order. #![feature(ptr_sub_ptr)] #[kani::proof] -fn check_sub_ptr_self_oob() { +fn check_offset_from_unsigned_self_oob() { let val = 10u128; let ptr: *const u128 = &val; let ptr_oob: *const u128 = ptr.wrapping_add(10); // SAFETY: This is not safe! - let _offset = unsafe { ptr_oob.sub_ptr(ptr) }; + let _offset = unsafe { ptr_oob.offset_from_unsigned(ptr) }; } #[kani::proof] -fn check_sub_ptr_oob_ptr() { +fn check_offset_from_unsigned_oob_ptr() { let val = 10u128; let ptr: *const u128 = &val; let ptr_oob: *const u128 = ptr.wrapping_sub(10); // SAFETY: This is not safe! - let _offset = unsafe { ptr.sub_ptr(ptr_oob) }; + let _offset = unsafe { ptr.offset_from_unsigned(ptr_oob) }; } #[kani::proof] -fn check_sub_ptr_diff_alloc() { +fn check_offset_from_unsigned_diff_alloc() { let val1 = kani::any(); let val2 = kani::any(); let ptr1: *const u128 = &val1; let ptr2: *const u128 = &val2; // SAFETY: This is not safe! - let _offset = unsafe { ptr1.sub_ptr(ptr2) }; + let _offset = unsafe { ptr1.offset_from_unsigned(ptr2) }; } #[kani::proof] -fn check_sub_ptr_negative_result() { +fn check_offset_from_unsigned_negative_result() { let val: [u8; 10] = kani::any(); let ptr_first: *const _ = &val[0]; let ptr_last: *const _ = &val[9]; // SAFETY: This is safe! - let offset_ok = unsafe { ptr_last.sub_ptr(ptr_first) }; + let offset_ok = unsafe { ptr_last.offset_from_unsigned(ptr_first) }; // SAFETY: This is not safe! - let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) }; + let offset_not_ok = unsafe { ptr_first.offset_from_unsigned(ptr_last) }; // Just use the result. assert!(offset_ok != offset_not_ok); @@ -49,22 +49,22 @@ fn check_sub_ptr_negative_result() { #[kani::proof] #[kani::should_panic] -fn check_sub_ptr_unit_panic() { +fn check_offset_from_unsigned_unit_panic() { let val1 = kani::any(); let val2 = kani::any(); let ptr1: *const () = &val1 as *const _ as *const (); let ptr2: *const () = &val2 as *const _ as *const (); // SAFETY: This is safe but will panic... - let _offset = unsafe { ptr1.sub_ptr(ptr2) }; + let _offset = unsafe { ptr1.offset_from_unsigned(ptr2) }; } #[kani::proof] -fn check_sub_ptr_same_dangling() { +fn check_offset_from_unsigned_same_dangling() { let val = 10u128; let ptr: *const u128 = &val; let ptr_oob_1: *const u128 = ptr.wrapping_add(10); let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); // SAFETY: This is safe since the pointer is the same! - let offset = unsafe { ptr_oob_1.sub_ptr(ptr_oob_2) }; + let offset = unsafe { ptr_oob_1.offset_from_unsigned(ptr_oob_2) }; assert_eq!(offset, 0); } diff --git a/tests/kani/PointerOffset/offset_from_vec.rs b/tests/kani/PointerOffset/offset_from_vec.rs index 482b4905df3c..29865e2c8f81 100644 --- a/tests/kani/PointerOffset/offset_from_vec.rs +++ b/tests/kani/PointerOffset/offset_from_vec.rs @@ -18,6 +18,6 @@ fn offset_non_power_two() { let offset = kani::any_where(|o: &usize| *o <= v.len()); let begin = v.as_mut_ptr(); let end = begin.add(offset); - assert_eq!(end.sub_ptr(begin), offset); + assert_eq!(end.offset_from_unsigned(begin), offset); } } From 15fb14ddaff3165024daa55b31c47faf22348d0d Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Mon, 3 Mar 2025 09:50:04 -0500 Subject: [PATCH 04/10] Dump toolchain to 2025-03-02 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 199e68771cbc..4167255ebd78 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-02-27" +channel = "nightly-2025-03-02" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 5143a9b59bb3530dfa16c7c9a502bfcbf7a9307a Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 4 Mar 2025 19:56:18 +0000 Subject: [PATCH 05/10] Skip CrateItems that of GlobalAsm kind to avoid triggering a panic in stable MIR --- kani-compiler/src/kani_middle/reachability.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index fdc81e177d1f..00235f614f94 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -83,6 +83,14 @@ where crate_items .iter() .filter_map(|item| { + // avoid stable MIR panic + // https://github.com/rust-lang/project-stable-mir/issues/95 + if let Some(instance) = Instance::try_from(*item).ok() { + let int_def_id = rustc_internal::internal(tcx, instance.def.def_id()); + if matches!(tcx.def_kind(int_def_id), rustc_hir::def::DefKind::GlobalAsm) { + return None; + } + }; // Only collect monomorphic items. matches!(item.kind(), ItemKind::Fn) .then(|| { From bc9a8579776b0ced41f4c7aef68b6515c5aaa0d0 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 4 Mar 2025 21:40:29 +0000 Subject: [PATCH 06/10] Fix test message --- tests/expected/arbitrary/ptrs/pointer_generator_error.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected index a0592c586a03..06496f4313d7 100644 --- a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected +++ b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected @@ -1,6 +1,6 @@ error[E0080]: evaluation of `kani::PointerGenerator::<0>::VALID` failed\ -the evaluated program panicked at 'PointerGenerator requires at least one byte.' +evaluation panicked: PointerGenerator requires at least one byte.\ note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\ pointer_generator_error.rs\ From dbbad5f0ad67f2d49429a726821e5f742610720f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Tue, 4 Mar 2025 21:59:25 -0500 Subject: [PATCH 07/10] Update attributes.rs Delete commented code --- kani-compiler/src/kani_middle/attributes.rs | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 5f38beb66202..0e27a3bdc3b6 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -1036,27 +1036,6 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { } else { None } - // match &attr.kind { - // AttrKind::Normal(normal) => { - // let segments = &normal.path.segments; - // if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { - // let ident_str = segments[1..] - // .iter() - // .map(|segment| segment.as_str()) - // .intersperse("::") - // .collect::(); - // KaniAttributeKind::try_from(ident_str.as_str()) - // .inspect_err(|&err| { - // debug!(?err, "attr_kind_failed"); - // tcx.dcx().span_err(attr.span(), format!("unknown attribute `{ident_str}`")); - // }) - // .ok() - // } else { - // None - // } - // } - // _ => None, - // } } /// Parse an attribute using `syn`. From f7ed449904dcd001ba81733707c71ade942ea81b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Tue, 4 Mar 2025 22:02:48 -0500 Subject: [PATCH 08/10] Tracking issue for stable MIR panic --- kani-compiler/src/kani_middle/reachability.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 00235f614f94..4efa3854c09a 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -84,7 +84,7 @@ where .iter() .filter_map(|item| { // avoid stable MIR panic - // https://github.com/rust-lang/project-stable-mir/issues/95 + // https://github.com/model-checking/kani/issues/3919 if let Some(instance) = Instance::try_from(*item).ok() { let int_def_id = rustc_internal::internal(tcx, instance.def.def_id()); if matches!(tcx.def_kind(int_def_id), rustc_hir::def::DefKind::GlobalAsm) { From 6ef84dd44d7361122e27fd074bbf2d3e937f3dcd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Tue, 4 Mar 2025 22:10:26 -0500 Subject: [PATCH 09/10] Handle new intrinsic in alias analysis --- kani-compiler/src/kani_middle/points_to/points_to_analysis.rs | 2 ++ 1 file changed, 2 insertions(+) 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 591d8c3574ff..2008ef1eb0b8 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 @@ -679,6 +679,8 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::RotateRight | Intrinsic::RoundF32 | Intrinsic::RoundF64 + | Intrinsic::RoundTiesEvenF32 + | Intrinsic::RoundTiesEvenF64 | Intrinsic::SaturatingAdd | Intrinsic::SaturatingSub | Intrinsic::SinF32 From 7f9397907e80d25f261a1a97b1de3e4ba8a2de2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Tue, 4 Mar 2025 22:12:43 -0500 Subject: [PATCH 10/10] Clippy fix --- kani-compiler/src/kani_middle/reachability.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 4efa3854c09a..e8bff532f1e7 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -85,7 +85,7 @@ where .filter_map(|item| { // avoid stable MIR panic // https://github.com/model-checking/kani/issues/3919 - if let Some(instance) = Instance::try_from(*item).ok() { + if let Ok(instance) = Instance::try_from(*item) { let int_def_id = rustc_internal::internal(tcx, instance.def.def_id()); if matches!(tcx.def_kind(int_def_id), rustc_hir::def::DefKind::GlobalAsm) { return None;