Add missing changes after a bad rebase

qinheping · Jan 24, 2024 · 75c58be · 75c58be
1 parent 59d5921
commit 75c58be
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 11 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -302,7 +302,11 @@ impl<'tcx> GotocCtx<'tcx> {
             kind: ty::BoundRegionKind::BrEnv,
         };
         let env_region = ty::Region::new_bound(self.tcx, ty::INNERMOST, br);
-        let env_ty = self.tcx.closure_env_ty(def_id, args, env_region).unwrap();
+        let env_ty = self.tcx.closure_env_ty(
+            Ty::new_closure(self.tcx, def_id, args),
+            args.as_closure().kind(),
+            env_region,
+        );
 
         let sig = sig.skip_binder();
 

diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
@@ -16,7 +16,7 @@ use tracing::debug;
 // Use a thread-local global variable to track the current codegen item for debugging.
 // If Kani panics during codegen, we can grab this item to include the problematic
 // codegen item in the panic trace.
-thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<String>, Option<Location>)> = RefCell::new((None, None)));
+thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<String>, Option<Location>)> = const { RefCell::new((None, None)) });
 
 pub fn init() {
     // Install panic hook

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -348,12 +348,12 @@ impl<'tcx> KaniAttributes<'tcx> {
                 "Use of unstable feature `{}`: {}",
                 unstable_attr.feature, unstable_attr.reason
             ))
-            .span_note(
+            .with_span_note(
                 self.tcx.def_span(self.item),
                 format!("the function `{fn_name}` is unstable:"),
             )
-            .note(format!("see issue {} for more information", unstable_attr.issue))
-            .help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
+            .with_note(format!("see issue {} for more information", unstable_attr.issue))
+            .with_help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
             .emit()
     }
 
@@ -422,7 +422,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                     self.item_name(),
                 ),
             )
-            .span_note(self.tcx.def_span(id), "Try adding a contract to this function.")
+            .with_span_note(self.tcx.def_span(id), "Try adding a contract to this function.")
             .emit();
             return;
         };
@@ -448,7 +448,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                             self.item_name(),
                         ),
                     )
-                    .span_note(
+                    .with_span_note(
                         self.tcx.def_span(def_id),
                         format!(
                             "Try adding a contract to this function or use the unsound `{}` attribute instead.", 
@@ -624,7 +624,7 @@ impl<'a> UnstableAttrParseError<'a> {
                 self.attr.span,
                 format!("failed to parse `#[kani::unstable]`: {}", self.reason),
             )
-            .note(format!(
+            .with_note(format!(
                 "expected format: #[kani::unstable({}, {}, {})]",
                 r#"feature="<IDENTIFIER>""#, r#"issue="<ISSUE>""#, r#"reason="<DESCRIPTION>""#
             ))
@@ -665,7 +665,7 @@ 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()))
-            .help("remove the extra argument")
+            .with_help("remove the extra argument")
             .emit();
     }
 }

diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs
@@ -7,6 +7,7 @@ use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, Terminator
 use rustc_middle::mir::{Local, LocalDecl};
 use rustc_middle::ty::{self, Ty, TyCtxt};
 use rustc_middle::ty::{Const, GenericArgsRef};
+use rustc_span::source_map::Spanned;
 use rustc_span::symbol::{sym, Symbol};
 use tracing::{debug, trace};
 
@@ -48,12 +49,12 @@ impl<'tcx> ModelIntrinsics<'tcx> {
     fn replace_simd_bitmask(
         &self,
         func: &mut Operand<'tcx>,
-        args: &[Operand<'tcx>],
+        args: &[Spanned<Operand<'tcx>>],
         gen_args: GenericArgsRef<'tcx>,
     ) {
         assert_eq!(args.len(), 1);
         let tcx = self.tcx;
-        let arg_ty = args[0].ty(&self.local_decls, tcx);
+        let arg_ty = args[0].node.ty(&self.local_decls, tcx);
         if arg_ty.is_simd() {
             // Get the stub definition.
             let stub_id = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask")).unwrap();