Update rust toolchain to 2022-05-17 (#1209)

* Update rust toolchain to 2022-05-17

Status: Compilation succeeds but regression fails due to new intrinsic.

Relevant changes:

- rust-lang/rust#95837
- rust-lang/rust#95562
- rust-lang/rust#96883

* Implement new intrinsic ptr_offset_from_unsigned

This new intrinsic is used in many different places in the standard
library and it was failing some tests for vectors.

* Apply suggestions from code review

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

* Address PR comments

 - Fix order of checks.
 - Improve error message.
 - Add comments to the new tests.

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

Author: celinval

cprover_bindings/src/goto_program/expr.rs

@@ -1221,6 +1221,13 @@ impl Expr {
         self.lt(typ.zero())
     }
 
+    /// `self >= 0`
+    pub fn is_non_negative(self) -> Self {
+        assert!(self.typ.is_numeric());
+        let typ = self.typ.clone();
+        self.ge(typ.zero())
+    }
+
     /// `self == 0`
     pub fn is_zero(self) -> Self {
         assert!(self.typ.is_numeric());

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

@@ -83,6 +83,21 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::assert(cond, property_name, message, loc)
     }
 
+    pub fn codegen_assert_assume(
+        &self,
+        cond: Expr,
+        property_class: PropertyClass,
+        message: &str,
+        loc: Location,
+    ) -> Stmt {
+        assert!(cond.typ().is_bool());
+        let property_name = property_class.as_str();
+        Stmt::block(
+            vec![Stmt::assert(cond.clone(), property_name, message, loc), Stmt::assume(cond, loc)],
+            loc,
+        )
+    }
+
     pub fn codegen_assert_false(
         &self,
         property_class: PropertyClass,

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

@@ -243,9 +243,8 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here)
     fn handle_kanitool_attributes(&mut self) {
-        let all_attributes = self.tcx.get_attrs(self.current_fn().instance().def_id());
+        let all_attributes = self.tcx.get_attrs_unchecked(self.current_fn().instance().def_id());
         let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes);
-
         if proof_attributes.is_empty() && !other_attributes.is_empty() {
             self.tcx.sess.span_err(
                 other_attributes[0].1.span,

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

@@ -4,7 +4,7 @@
 use super::typ::pointee_type;
 use super::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
+use cbmc::goto_program::{ArithmeticOverflowResult, BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::mir::{BasicBlock, Operand, Place};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Ty};
@@ -551,6 +551,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq),
             "ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq),
             "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),
             "rintf32" => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/1025"
@@ -1009,33 +1010,77 @@ impl<'tcx> GotocCtx<'tcx> {
     /// https://doc.rust-lang.org/std/intrinsics/fn.ptr_offset_from.html
     fn codegen_ptr_offset_from(
         &mut self,
-        mut fargs: Vec<Expr>,
+        fargs: Vec<Expr>,
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        let dst_ptr = fargs.remove(0);
-        let src_ptr = fargs.remove(0);
-
-        // Compute the offset with standard substraction using `isize`
-        let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t());
-        let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t());
-        let offset = cast_dst_ptr.sub_overflow(cast_src_ptr);
+        let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs);
 
         // Check that computing `offset` in bytes would not overflow an `isize`
         // These checks may allow a wrapping-around behavior in CBMC:
         // https://github.com/model-checking/kani/issues/1150
         let overflow_check = self.codegen_assert(
-            offset.overflowed.not(),
+            offset_overflow.overflowed.not(),
             PropertyClass::ArithmeticOverflow,
             "attempt to compute offset in bytes which would overflow an `isize`",
             loc,
         );
 
-        // Re-compute the offset with standard substraction (no casts this time)
-        let offset_expr = self.codegen_expr_to_place(p, dst_ptr.sub(src_ptr));
+        let offset_expr = self.codegen_expr_to_place(p, offset_expr);
         Stmt::block(vec![overflow_check, offset_expr], loc)
     }
 
+    /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known.
+    /// The logic is similar to `ptr_offset_from` but the return value is a `usize`.
+    /// See https://github.com/rust-lang/rust/issues/95892 for more details
+    fn codegen_ptr_offset_from_unsigned(
+        &mut self,
+        fargs: Vec<Expr>,
+        p: &Place<'tcx>,
+        loc: Location,
+    ) -> Stmt {
+        let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs);
+
+        // Check that computing `offset` in bytes would not overflow an `isize`
+        // These checks may allow a wrapping-around behavior in CBMC:
+        // https://github.com/model-checking/kani/issues/1150
+        let overflow_check = self.codegen_assert_assume(
+            offset_overflow.overflowed.not(),
+            PropertyClass::ArithmeticOverflow,
+            "attempt to compute offset in bytes which would overflow an `isize`",
+            loc,
+        );
+
+        let non_negative_check = self.codegen_assert_assume(
+            offset_overflow.result.is_non_negative(),
+            PropertyClass::KaniCheck,
+            "attempt to compute unsigned offset with negative distance",
+            loc,
+        );
+
+        let offset_expr = self.codegen_expr_to_place(p, offset_expr.cast_to(Type::size_t()));
+        Stmt::block(vec![overflow_check, non_negative_check, offset_expr], loc)
+    }
+
+    /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers.
+    /// This function implements the common logic between them.
+    fn codegen_ptr_offset_from_expr(
+        &mut self,
+        mut fargs: Vec<Expr>,
+    ) -> (Expr, ArithmeticOverflowResult) {
+        let dst_ptr = fargs.remove(0);
+        let src_ptr = fargs.remove(0);
+
+        // Compute the offset with standard substraction using `isize`
+        let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t());
+        let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t());
+        let offset_overflow = cast_dst_ptr.sub_overflow(cast_src_ptr);
+
+        // Re-compute the offset with standard substraction (no casts this time)
+        let ptr_offset_expr = dst_ptr.sub(src_ptr);
+        (ptr_offset_expr, offset_overflow)
+    }
+
     /// A transmute is a bitcast from the argument type to the return type.
     /// https://doc.rust-lang.org/std/intrinsics/fn.transmute.html
     ///

kani-compiler/src/main.rs

@@ -7,7 +7,6 @@
 //! Like miri, clippy, and other tools developed on the top of rustc, we rely on the
 //! rustc_private feature and a specific version of rustc.
 #![deny(warnings)]
-#![feature(bool_to_option)]
 #![feature(crate_visibility_modifier)]
 #![feature(extern_types)]
 #![feature(nll)]

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2022-05-03"
+channel = "nightly-2022-05-17"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/intrinsics/ptr_offset_from_unsigned/check_invariant_violation.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani correctly detects a safety violation when user tries to invoke the
+//! `ptr_offset_from_unsigned` intrinsic in the wrong order.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::ptr_offset_from_unsigned;
+
+#[kani::proof]
+fn check_failure() {
+    let a = [0; 5];
+    let ptr0: *const i32 = &a[0];
+    let ptr1: *const i32 = &a[1];
+    unsafe {
+        let _distance = ptr_offset_from_unsigned(ptr0, ptr1);
+    }
+}

tests/expected/intrinsics/ptr_offset_from_unsigned/expected

@@ -0,0 +1 @@
+Failed Checks: attempt to compute unsigned offset with negative distance

tests/kani/Intrinsics/PtrOffsetFromUnsigned/check_unsigned_ptr_offset_from.rs

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Checks that the ptr_offset_from_unsigned intrinsic returns the expected results.
+
+#![feature(core_intrinsics)]
+use std::intrinsics::ptr_offset_from_unsigned;
+
+#[kani::proof]
+fn check_distance_i32() {
+    let a = [0; 5];
+    let ptr0: *const i32 = &a[0];
+    let ptr1: *const i32 = &a[1];
+    let ptr2: *const i32 = &a[2];
+    unsafe {
+        assert_eq!(ptr_offset_from_unsigned(ptr2, ptr0), 2);
+        assert_eq!(ptr_offset_from_unsigned(ptr1, ptr0), 1);
+        assert_eq!(ptr_offset_from_unsigned(ptr2, ptr2), 0);
+    }
+}
+
+#[kani::proof]
+fn check_distance_i64() {
+    let a = [0i64; 5];
+    let ptr0: *const i64 = &a[0];
+    let ptr1: *const i64 = &a[1];
+    let ptr2: *const i64 = &a[2];
+    unsafe {
+        assert_eq!(ptr_offset_from_unsigned(ptr2, ptr0), 2);
+        assert_eq!(ptr_offset_from_unsigned(ptr1, ptr0), 1);
+        assert_eq!(ptr_offset_from_unsigned(ptr1, ptr1), 0);
+    }
+}

tools/bookrunner/librustdoc/clean/inline.rs

@@ -26,7 +26,7 @@ use crate::clean::{
 use crate::core::DocContext;
 use crate::formats::item_type::ItemType;
 
-type Attrs<'hir> = rustc_middle::ty::Attributes<'hir>;
+type Attrs<'hir> = &'hir [ast::Attribute];
 
 /// Attempt to inline a definition into this AST.
 ///
@@ -159,7 +159,7 @@ crate fn try_inline_glob(
 }
 
 fn load_attrs<'hir>(cx: &DocContext<'hir>, did: DefId) -> Attrs<'hir> {
-    cx.tcx.get_attrs(did)
+    cx.tcx.get_attrs_unchecked(did)
 }
 
 /// Record an external fully qualified name in the external_paths cache.
@@ -685,7 +685,7 @@ crate fn record_extern_trait(cx: &mut DocContext<'_>, did: DefId) {
 
     let trait_ = clean::TraitWithExtraInfo {
         trait_,
-        is_notable: clean::utils::has_doc_flag(cx.tcx.get_attrs(did), sym::notable_trait),
+        is_notable: clean::utils::has_doc_flag(cx.tcx, did, sym::notable_trait),
     };
     cx.external_traits.borrow_mut().insert(did, trait_);
     cx.active_extern_traits.remove(&did);