[DO NOT MERGE] Use stable Rust 1.85.0 release

.cargo/config.toml

@@ -20,6 +20,7 @@ KANI_SYSROOT ={value = "target/kani", relative = true}
 KANI_BUILD_LIBS ={value = "target/build-libs", relative = true}
 # Build Kani library without `build-std`.
 KANI_LEGACY_LIBS ={value = "target/legacy-libs", relative = true}
+RUSTC_BOOTSTRAP ={value="1"}
 
 [target.'cfg(all())']
 rustflags = [ # Global lints/warnings. Need to use underscore instead of -.

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, PartialEq)]
+#[derive(Debug, Clone, Copy)]
 pub enum BuiltinFn {
     Abort,
     Assert,

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -84,7 +84,7 @@ use std::collections::HashMap;
 use std::fs::File;
 use std::hash::Hash;
 use std::io::{self, BufReader};
-use std::io::{BufWriter, Bytes, Error, Read, Write};
+use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write};
 use std::path::Path;
 
 /// Writes a symbol table to a file in goto binary format in version 6.
@@ -557,7 +557,7 @@ where
     R: Read,
 {
     /// Stream of bytes from which GOTO objects are read.
-    bytes: Bytes<BufReader<R>>,
+    bytes: Bytes<R>,
 
     /// Numbering for ireps
     numbering: IrepNumbering,
@@ -584,9 +584,8 @@ where
     /// Constructor. The reader is moved into this object and cannot be used
     /// afterwards.
     fn new(reader: R) -> Self {
-        let buffered_reader = BufReader::new(reader);
         GotoBinaryDeserializer {
-            bytes: buffered_reader.bytes(),
+            bytes: reader.bytes(),
             numbering: IrepNumbering::new(),
             string_count: Vec::new(),
             string_map: Vec::new(),
@@ -598,9 +597,12 @@ where
     /// Returns Err if the found value is not the expected value.
     fn expect<T: Eq + std::fmt::Display>(found: T, expected: T) -> io::Result<T> {
         if found != expected {
-            return Err(Error::other(format!(
-                "Invalid goto binary input: expected {expected} in byte stream, found {found} instead)"
-            )));
+            return Err(Error::new(
+                ErrorKind::Other,
+                format!(
+                    "Invalid goto binary input: expected {expected} in byte stream, found {found} instead)"
+                ),
+            ));
         }
         Ok(found)
     }
@@ -658,7 +660,10 @@ where
         match self.bytes.next() {
             Some(Ok(u)) => Ok(u),
             Some(Err(error)) => Err(error),
-            None => Err(Error::other("Invalid goto binary input: unexpected end of input")),
+            None => Err(Error::new(
+                ErrorKind::Other,
+                "Invalid goto binary input: unexpected end of input",
+            )),
         }
     }
 
@@ -672,7 +677,8 @@ where
             match self.bytes.next() {
                 Some(Ok(u)) => {
                     if shift >= max_shift {
-                        return Err(Error::other(
+                        return Err(Error::new(
+                            ErrorKind::Other,
                             "Invalid goto binary input: serialized value is too large to fit in usize",
                         ));
                     };
@@ -686,7 +692,10 @@ where
                     return Err(error);
                 }
                 None => {
-                    return Err(Error::other("Invalid goto binary input: unexpected end of input"));
+                    return Err(Error::new(
+                        ErrorKind::Other,
+                        "Invalid goto binary input: unexpected end of input",
+                    ));
                 }
             }
         }
@@ -712,7 +721,10 @@ where
                                         return Ok(numbered);
                                     }
                                     Err(error) => {
-                                        return Err(Error::other(error.to_string()));
+                                        return Err(Error::new(
+                                            ErrorKind::Other,
+                                            error.to_string(),
+                                        ));
                                     }
                                 }
                             }
@@ -726,7 +738,8 @@ where
                                         return Err(error);
                                     }
                                     None => {
-                                        return Err(Error::other(
+                                        return Err(Error::new(
+                                            ErrorKind::Other,
                                             "Invalid goto binary input: unexpected end of input",
                                         ));
                                     }
@@ -744,7 +757,8 @@ where
                     }
                     None => {
                         // No more bytes left
-                        return Err(Error::other(
+                        return Err(Error::new(
+                            ErrorKind::Other,
                             "Invalid goto binary input: unexpected end of input",
                         ));
                     }
@@ -775,7 +789,8 @@ where
                 match c {
                     b'S' => {
                         if sub_done {
-                            return Err(Error::other(
+                            return Err(Error::new(
+                                ErrorKind::Other,
                                 "Invalid goto binary input: incorrect binary structure",
                             ));
                         }
@@ -801,10 +816,13 @@ where
                         return Ok(numbered);
                     }
                     other => {
-                        return Err(Error::other(format!(
-                            "Invalid goto binary input: unexpected character in input stream {}",
-                            other as char
-                        )));
+                        return Err(Error::new(
+                            ErrorKind::Other,
+                            format!(
+                                "Invalid goto binary input: unexpected character in input stream {}",
+                                other as char
+                            ),
+                        ));
                     }
                 }
             }
@@ -859,7 +877,8 @@ where
         let shifted_flags = flags >> 16;
 
         if shifted_flags != 0 {
-            return Err(Error::other(
+            return Err(Error::new(
+                ErrorKind::Other,
                 "incorrect binary format: true bits remain in decoded symbol flags",
             ));
         }
@@ -897,10 +916,13 @@ where
         // Read goto binary version
         let goto_binary_version = self.read_usize_varenc()?;
         if goto_binary_version != 6 {
-            return Err(Error::other(format!(
-                "Unsupported GOTO binary version: {}. Supported version: {}",
-                goto_binary_version, 6
-            )));
+            return Err(Error::new(
+                ErrorKind::Other,
+                format!(
+                    "Unsupported GOTO binary version: {}. Supported version: {}",
+                    goto_binary_version, 6
+                ),
+            ));
         }
         Ok(())
     }

cprover_bindings/src/machine_model.rs

@@ -45,7 +45,6 @@ pub enum RoundingMode {
     Downward = 1,
     Upward = 2,
     TowardsZero = 3,
-    ToAway = 4,
 }
 
 impl From<RoundingMode> for BigInt {

docs/src/rust-feature-support/intrinsics.md

@@ -180,6 +180,8 @@ 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) |
@@ -196,10 +198,8 @@ 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) |
-round_ties_even_f16 | No | |
-round_ties_even_f32 | Yes | |
-round_ties_even_f64 | Yes | |
-round_ties_even_f128 | No | |
+rintf32 | Yes | |
+rintf64 | Yes | |
 rotate_left | Yes | |
 rotate_right | Yes | |
 roundf32 | Yes | |

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -813,7 +813,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
             use rustc_hir::definitions::DefPathData;
             match &data.data {
-                DefPathData::TypeNs(Some(symbol)) => {
+                DefPathData::TypeNs(symbol) => {
                     error_assert!(self, span, data.disambiguator == 0); // Sanity check
                     name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }
@@ -956,7 +956,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
             use rustc_hir::definitions::DefPathData;
             match &data.data {
-                DefPathData::TypeNs(Some(symbol)) => {
+                DefPathData::TypeNs(symbol) => {
                     error_assert!(self, span, data.disambiguator == 0); // Sanity check
                     name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }
@@ -1063,7 +1063,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             let disambiguator = CharonDisambiguator::new(data.disambiguator as usize);
             use rustc_hir::definitions::DefPathData;
             match &data.data {
-                DefPathData::TypeNs(Some(symbol)) => {
+                DefPathData::TypeNs(symbol) => {
                     error_assert!(self, span, data.disambiguator == 0); // Sanity check
                     name.push(CharonPathElem::Ident(symbol.to_string(), disambiguator));
                 }

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

@@ -63,7 +63,9 @@ 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.tool_attrs(&["kanitool".into(), "recursion_tracker".into()]).is_empty()
+            if !static_item
+                .attrs_by_path(&["kanitool".into(), "recursion_tracker".into()])
+                .is_empty()
             {
                 let span = static_item.span();
                 let loc = self.codegen_span_stable(span);

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

@@ -227,7 +227,7 @@ impl GotocCtx<'_> {
 pub mod rustc_smir {
     use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region};
     use crate::stable_mir::CrateDef;
-    use rustc_middle::mir::coverage::BasicCoverageBlock;
+    use rustc_middle::mir::coverage::CovTerm;
     use rustc_middle::mir::coverage::MappingKind::Code;
     use rustc_middle::ty::TyCtxt;
     use rustc_smir::rustc_internal;
@@ -243,16 +243,16 @@ pub mod rustc_smir {
         coverage_opaque: &CoverageOpaque,
         instance: Instance,
     ) -> Option<(SourceRegion, Filename)> {
-        let bcb = parse_coverage_opaque(coverage_opaque);
-        region_from_coverage(tcx, bcb, instance)
+        let cov_term = parse_coverage_opaque(coverage_opaque);
+        region_from_coverage(tcx, cov_term, instance)
     }
 
-    /// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object.
+    /// Retrieves the `SourceRegion` associated with a `CovTerm` object.
     ///
     /// Note: This function could be in the internal `rustc` impl for `Coverage`.
     pub fn region_from_coverage(
         tcx: TyCtxt<'_>,
-        coverage: BasicCoverageBlock,
+        coverage: CovTerm,
         instance: Instance,
     ) -> Option<(SourceRegion, Filename)> {
         // We need to pull the coverage info from the internal MIR instance.
@@ -264,10 +264,10 @@ pub mod rustc_smir {
         if let Some(cov_info) = &body.function_coverage_info {
             // Iterate over the coverage mappings and match with the coverage term.
             for mapping in &cov_info.mappings {
-                let Code { bcb } = mapping.kind else { unreachable!() };
+                let Code(term) = mapping.kind else { unreachable!() };
                 let source_map = tcx.sess.source_map();
                 let file = source_map.lookup_source_file(cov_info.body_span.lo());
-                if bcb == coverage {
+                if term == coverage {
                     return Some((
                         make_source_region(source_map, cov_info, &file, mapping.span).unwrap(),
                         rustc_internal::stable(cov_info.body_span).get_filename(),
@@ -278,17 +278,25 @@ pub mod rustc_smir {
         None
     }
 
-    /// Parse a `CoverageOpaque` item and return the corresponding `BasicCoverageBlock`:
-    fn parse_coverage_opaque(coverage_opaque: &Opaque) -> BasicCoverageBlock {
+    /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`:
+    /// <https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CovTerm.html>
+    ///
+    /// At present, a `CovTerm` can be one of the following:
+    ///  - `CounterIncrement(<num>)`: A physical counter.
+    ///  - `ExpressionUsed(<num>)`: An expression-based counter.
+    ///  - `Zero`: A counter with a constant zero value.
+    fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm {
         let coverage_str = coverage_opaque.to_string();
-        if let Some(rest) = coverage_str.strip_prefix("VirtualCounter(bcb") {
+        if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") {
+            let (num_str, _rest) = rest.split_once(')').unwrap();
+            let num = num_str.parse::<u32>().unwrap();
+            CovTerm::Counter(num.into())
+        } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") {
             let (num_str, _rest) = rest.split_once(')').unwrap();
             let num = num_str.parse::<u32>().unwrap();
-            BasicCoverageBlock::from_u32(num)
+            CovTerm::Expression(num.into())
         } else {
-            // When the coverage statement is injected into mir_body, it always has the form CoverageKind::VirtualCounter { bcb }
-            // https://github.com/rust-lang/rust/pull/136053/files#diff-c99ec9a281dce4a381fa7e11cf2d04f55dba5573d1d14389d47929fe0a154d24R209-R212
-            unreachable!();
+            CovTerm::Zero
         }
     }
 }

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

@@ -414,6 +414,8 @@ 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),
@@ -423,13 +425,12 @@ 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 | Intrinsic::RoundTiesEvenF64 => {
-                self.codegen_round_to_integral(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),
@@ -637,23 +638,6 @@ impl GotocCtx<'_> {
         dividend_is_int_min.and(divisor_is_minus_one).not()
     }
 
-    // Builds a floatbv_round_to_integral expression with specified cbmc::RoundingMode.
-    fn codegen_round_to_integral(
-        &mut self,
-        rounding_mode: cbmc::RoundingMode,
-        mut fargs: Vec<Expr>,
-        place: &Place,
-        loc: Location,
-    ) -> Stmt {
-        let place_ty = self.place_ty_stable(place);
-        let result_type = self.codegen_ty_stable(place_ty);
-        let f = fargs.remove(0);
-        assert!(fargs.is_empty());
-        let rm = Expr::int_constant(rounding_mode, Type::c_int());
-        let expr = Expr::floatbv_round_to_integral(f, rm, result_type);
-        self.codegen_expr_to_place_stable(place, expr, loc)
-    }
-
     /// Intrinsics of the form *_with_overflow
     fn codegen_op_with_overflow(
         &mut self,