diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 1b5b7c42d..99a7732be 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -501,7 +501,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#1fc4a032540111eb716b0cbc306899f397f443cf" +source = "git+https://github.com/Nadrieril/hax?branch=update-rustc2#8124bf4174cf656ede51ff68370a432f8eda9b4c" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -512,7 +512,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#1fc4a032540111eb716b0cbc306899f397f443cf" +source = "git+https://github.com/Nadrieril/hax?branch=update-rustc2#8124bf4174cf656ede51ff68370a432f8eda9b4c" dependencies = [ "extension-traits", "hax-adt-into", @@ -529,7 +529,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#1fc4a032540111eb716b0cbc306899f397f443cf" +source = "git+https://github.com/Nadrieril/hax?branch=update-rustc2#8124bf4174cf656ede51ff68370a432f8eda9b4c" dependencies = [ "schemars", "serde", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 45c9354f3..6f9700886 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -55,7 +55,7 @@ tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_ walkdir = "2.3.2" which = "6.0.1" -hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main" } +hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "update-rustc2" } # hax-frontend-exporter = { path = "../../hax/frontend/exporter" } macros = { path = "./macros" } diff --git a/charon/src/ast/meta_utils.rs b/charon/src/ast/meta_utils.rs index 5ff4f523f..e723e77eb 100644 --- a/charon/src/ast/meta_utils.rs +++ b/charon/src/ast/meta_utils.rs @@ -3,7 +3,7 @@ use crate::meta::*; use hax_frontend_exporter as hax; use rustc_hir::def_id::DefId; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; +use rustc_span::source_map::SourceMap; use std::cmp::Ordering; use std::iter::Iterator; use std::path::Component; @@ -133,11 +133,7 @@ pub fn convert_loc(loc: hax::Loc) -> Loc { } // TODO: remove? -pub fn span_to_string(sess: &Session, span: rustc_span::Span) -> String { - // Retrieve the source map, which contains information about the source file: - // we need it to be able to interpret the span. - let source_map = sess.source_map(); - +pub fn span_to_string(source_map: &SourceMap, span: rustc_span::Span) -> String { // Convert the span to lines let (beg, end) = source_map.is_valid_span(span).unwrap(); diff --git a/charon/src/ast/names_utils.rs b/charon/src/ast/names_utils.rs index ae755ed80..531820cd9 100644 --- a/charon/src/ast/names_utils.rs +++ b/charon/src/ast/names_utils.rs @@ -250,7 +250,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { kind, })); } - DefPathData::ImplTrait => { + DefPathData::OpaqueTy => { // TODO: do nothing for now } DefPathData::MacroNs(symbol) => { @@ -263,7 +263,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // instance to filter opaque modules. name.push(PathElem::Ident(symbol.to_string(), disambiguator)); } - DefPathData::ClosureExpr => { + DefPathData::Closure => { // TODO: this is not very satisfactory, but on the other hand // we should be able to extract closures in local let-bindings // (i.e., we shouldn't have to introduce top-level let-bindings). diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index 51e4adaba..f6c5ec39a 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -9,7 +9,6 @@ use regex::Regex; use rustc_driver::{Callbacks, Compilation}; use rustc_interface::{interface::Compiler, Queries}; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; use std::fmt; use std::ops::Deref; use std::panic::{self, AssertUnwindSafe}; @@ -101,7 +100,7 @@ impl Callbacks for CharonCallbacks { /// possible (i.e., after parsing). See [charon_lib::get_mir]. fn after_crate_root_parsing<'tcx>( &mut self, - c: &Compiler, + _c: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { // Set up our own `DefId` debug routine. @@ -113,8 +112,7 @@ impl Callbacks for CharonCallbacks { .unwrap() .get_mut() .enter(|tcx| { - let session = c.session(); - let crate_data = translate(session, tcx, self)?; + let crate_data = translate(tcx, self)?; self.crate_data = Some(crate_data); Ok::<(), ()>(()) }) @@ -208,11 +206,7 @@ pub fn get_args_crate_index>(args: &[T]) -> Option /// /// This function is a callback function for the Rust compiler. #[allow(clippy::result_unit_err)] -pub fn translate( - sess: &Session, - tcx: TyCtxt, - internal: &mut CharonCallbacks, -) -> Result { +pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> Result { trace!(); let options = &internal.options; @@ -246,11 +240,10 @@ pub fn translate( // # Translate the declarations in the crate. // We translate the declarations in an ad-hoc order, and do not group // the mutually recursive groups - we do this in the next step. - let mut ctx = - match translate_crate_to_ullbc::translate(crate_name, options, sess, tcx, mir_level) { - Ok(ctx) => ctx, - Err(_) => return Err(()), - }; + let mut ctx = match translate_crate_to_ullbc::translate(crate_name, options, tcx, mir_level) { + Ok(ctx) => ctx, + Err(_) => return Err(()), + }; if options.print_ullbc { info!("# ULLBC after translation from MIR:\n\n{ctx}\n"); diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs index 14add4a86..ec69ac16e 100644 --- a/charon/src/bin/charon-driver/main.rs +++ b/charon/src/bin/charon-driver/main.rs @@ -6,7 +6,6 @@ extern crate rustc_driver; extern crate rustc_hir; extern crate rustc_interface; extern crate rustc_middle; -extern crate rustc_session; extern crate rustc_span; #[macro_use] diff --git a/charon/src/lib.rs b/charon/src/lib.rs index 35a862b97..34ab8bb9d 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -26,10 +26,10 @@ extern crate rustc_ast; extern crate rustc_ast_pretty; extern crate rustc_attr; extern crate rustc_error_messages; +extern crate rustc_errors; extern crate rustc_hir; extern crate rustc_index; extern crate rustc_middle; -extern crate rustc_session; extern crate rustc_span; extern crate rustc_target; diff --git a/charon/src/translate/translate_crate_to_ullbc.rs b/charon/src/translate/translate_crate_to_ullbc.rs index 05940e32d..f69badbbe 100644 --- a/charon/src/translate/translate_crate_to_ullbc.rs +++ b/charon/src/translate/translate_crate_to_ullbc.rs @@ -9,7 +9,6 @@ use hax_frontend_exporter::SInto; use rustc_hir::def_id::DefId; use rustc_hir::{ForeignItemKind, ImplItemKind, Item, ItemKind}; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; use std::collections::{HashMap, HashSet}; impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { @@ -342,10 +341,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { pub fn translate<'tcx, 'ctx>( crate_name: String, options: &CliOpts, - session: &'ctx Session, tcx: TyCtxt<'tcx>, mir_level: MirLevel, -) -> Result, Error> { +) -> Result, Error> { let hax_state = hax::state::State::new( tcx, hax::options::Options { @@ -364,7 +362,7 @@ pub fn translate<'tcx, 'ctx>( errors: ErrorCtx { continue_on_failure: !options.abort_on_error, errors_as_warnings: options.errors_as_warnings, - session, + dcx: tcx.dcx(), decls_with_errors: HashSet::new(), ignored_failed_decls: HashSet::new(), dep_sources: HashMap::new(), @@ -397,10 +395,8 @@ pub fn translate<'tcx, 'ctx>( let hir = tcx.hir(); for item_id in hir.root_module().item_ids { let item_id = item_id.hir_id(); - let node = hir.find(item_id).unwrap(); - let item = match node { - rustc_hir::Node::Item(item) => item, - _ => unreachable!(), + let rustc_hir::Node::Item(item) = tcx.hir_node(item_id) else { + unreachable!() }; ctx.register_local_hir_item(true, item)?; } diff --git a/charon/src/translate/translate_ctx.rs b/charon/src/translate/translate_ctx.rs index 64af9ea66..d2561b03d 100644 --- a/charon/src/translate/translate_ctx.rs +++ b/charon/src/translate/translate_ctx.rs @@ -19,10 +19,10 @@ use hax_frontend_exporter::SInto; use linked_hash_set::LinkedHashSet; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use rustc_error_messages::MultiSpan; +use rustc_errors::DiagCtxt; use rustc_hir::def_id::DefId; use rustc_hir::Node as HirNode; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; use serde::{Deserialize, Serialize}; use std::cmp::{Ord, Ordering, PartialOrd}; use std::collections::{BTreeMap, HashMap, HashSet, VecDeque}; @@ -251,7 +251,7 @@ pub struct ErrorCtx<'ctx> { pub errors_as_warnings: bool, /// The compiler session, used for displaying errors. - pub session: &'ctx Session, + pub dcx: &'ctx DiagCtxt, /// The ids of the declarations for which extraction we encountered errors. pub decls_with_errors: HashSet, /// The ids of the declarations we completely failed to extract and had to ignore. @@ -389,9 +389,9 @@ impl ErrorCtx<'_> { pub(crate) fn span_err_no_register>(&self, span: S, msg: &str) { let msg = msg.to_string(); if self.errors_as_warnings { - self.session.span_warn(span, msg); + self.dcx.span_warn(span, msg); } else { - self.session.span_err(span, msg); + self.dcx.span_err(span, msg); } } @@ -596,9 +596,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// Returns the attributes (`#[...]`) of this node. pub(crate) fn node_attributes(&self, id: DefId) -> &[rustc_ast::Attribute] { - let hir = self.tcx.hir(); id.as_local() - .map(|local_def_id| hir.attrs(hir.local_def_id_to_hir_id(local_def_id))) + .map(|local_def_id| { + self.tcx + .hir() + .attrs(self.tcx.local_def_id_to_hir_id(local_def_id)) + }) .unwrap_or_default() } @@ -684,7 +687,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { | Ctor { .. } | ExternCrate | ForeignMod - | Coroutine | GlobalAsm | InlineConst | LifetimeParam @@ -702,10 +704,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// Whether this item is in an `extern { .. }` block, in which case it has no body. pub(crate) fn id_is_extern_item(&mut self, id: DefId) -> bool { - id.as_local().is_some_and(|local_def_id| { - let node = self.tcx.hir().find_by_def_id(local_def_id); - matches!(node, Some(HirNode::ForeignItem(_))) - }) + self.tcx + .hir() + .get_if_local(id) + .is_some_and(|node| matches!(node, HirNode::ForeignItem(_))) } pub(crate) fn is_opaque_name(&self, name: &Name) -> bool { diff --git a/charon/src/translate/translate_functions_to_ullbc.rs b/charon/src/translate/translate_functions_to_ullbc.rs index 2467a0b24..915efccb5 100644 --- a/charon/src/translate/translate_functions_to_ullbc.rs +++ b/charon/src/translate/translate_functions_to_ullbc.rs @@ -824,7 +824,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { Ok(Rvalue::Aggregate(akind, operands_t)) } - hax::AggregateKind::Coroutine(_def_id, _subst, _movability) => { + hax::AggregateKind::Coroutine(..) => { error_or_panic!(self, span, "Coroutines are not supported"); } } @@ -869,7 +869,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // sometimes introduces very low-level functions, which we need to // catch early - in particular, before we start translating types and // arguments, because we won't be able to translate some of them. - if matches!(builtin_fun, Some(BuiltinFun::BoxFree)) { + let sfid = if matches!(builtin_fun, Some(BuiltinFun::BoxFree)) { assert!(!is_local); // This deallocates a box. @@ -903,8 +903,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { func: FunIdOrTraitMethodRef::mk_assumed(AssumedFunId::BoxFree), generics: GenericArgs::new_from_types(vec![t_ty]), }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + SubstFunId { func, args } } else { // Retrieve the lists of used parameters, in case of non-local // definitions @@ -945,7 +944,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Check if the function is considered primitive: primitive // functions benefit from special treatment. - if let Some(builtin_fun) = builtin_fun { + let func = if let Some(builtin_fun) = builtin_fun { // Primitive function. // // Note that there are subtleties with regards to the way types parameters @@ -992,22 +991,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } }; - let func = FnPtr { - func: FunIdOrTraitMethodRef::Fun(FunId::Assumed(aid)), - generics, - }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + FunIdOrTraitMethodRef::Fun(FunId::Assumed(aid)) } else { // Two cases depending on whether we call a trait method or not match trait_info { None => { // "Regular" function call let def_id = self.register_fun_decl_id(span, rust_id); - let func = FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id)); - let func = FnPtr { func, generics }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id)) } Some(trait_info) => { // Trait method @@ -1023,18 +1014,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let trait_method_fun_id = self.register_fun_decl_id(span, rust_id); let method_name = self.t_ctx.translate_trait_item_name(rust_id)?; - let func = FunIdOrTraitMethodRef::Trait( - impl_expr, - method_name, - trait_method_fun_id, - ); - let func = FnPtr { func, generics }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + FunIdOrTraitMethodRef::Trait(impl_expr, method_name, trait_method_fun_id) } } + }; + SubstFunId { + func: FnPtr { func, generics }, + args, } - } + }; + Ok(SubstFunIdOrPanic::Fun(sfid)) } /// Translate a statement diff --git a/charon/src/translate/translate_predicates.rs b/charon/src/translate/translate_predicates.rs index df504353e..920633449 100644 --- a/charon/src/translate/translate_predicates.rs +++ b/charon/src/translate/translate_predicates.rs @@ -537,10 +537,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } PredicateKind::AliasRelate(..) | PredicateKind::Ambiguous - | PredicateKind::ClosureKind(_, _, _) | PredicateKind::Coerce(_) | PredicateKind::ConstEquate(_, _) | PredicateKind::ObjectSafe(_) + | PredicateKind::NormalizesTo(_) | PredicateKind::Subtype(_) => error_or_panic!( self, span, diff --git a/charon/src/translate/translate_traits.rs b/charon/src/translate/translate_traits.rs index 2ab213386..cf8e50219 100644 --- a/charon/src/translate/translate_traits.rs +++ b/charon/src/translate/translate_traits.rs @@ -393,7 +393,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } if item_meta.opacity.is_opaque() { let ctx = bt_ctx.into_fmt(); - bt_ctx.t_ctx.errors.session.span_warn( + bt_ctx.t_ctx.errors.dcx.span_warn( item_meta.span, format!( "Trait declarations cannot be \"opaque\"; the trait `{}` will be translated as normal.", @@ -598,7 +598,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } if item_meta.opacity.is_opaque() { let ctx = bt_ctx.into_fmt(); - bt_ctx.t_ctx.errors.session.span_warn( + bt_ctx.t_ctx.errors.dcx.span_warn( item_meta.span, format!( "Trait implementations cannot be \"opaque\"; the impl `{}` will be translated as normal.", diff --git a/charon/src/translate/translate_types.rs b/charon/src/translate/translate_types.rs index 10a3951b6..50f216442 100644 --- a/charon/src/translate/translate_types.rs +++ b/charon/src/translate/translate_types.rs @@ -342,7 +342,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { error_or_panic!(self, span, "Dynamic types are not supported yet") } - hax::Ty::Coroutine(_, _, _) => { + hax::Ty::Coroutine(..) => { trace!("Coroutine"); error_or_panic!(self, span, "Coroutine types are not supported yet") } @@ -436,16 +436,17 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let mut regions: Vec = vec![]; let mut params = vec![]; let mut cgs = vec![]; + use hax::GenericArg::*; for param in substs.iter() { match param { - hax::GenericArg::Type(param_ty) => { + Type(param_ty) => { let param_ty = self.translate_ty(span, erase_regions, param_ty)?; params.push(param_ty); } - hax::GenericArg::Lifetime(region) => { + Lifetime(region) => { regions.push(self.translate_region(span, erase_regions, region)?); } - hax::GenericArg::Const(c) => { + Const(c) => { cgs.push(self.translate_constant_expr_to_const_generic(span, c)?); } } @@ -522,9 +523,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } // Separate path for type aliases because they're not an `AdtDef`. - if let Some(local_def_id) = rust_id.as_local() { - let hir_id = tcx.hir().local_def_id_to_hir_id(local_def_id); - let rustc_hir::Node::Item(item) = tcx.hir().get(hir_id) else { + if let Some(node) = tcx.hir().get_if_local(rust_id) { + let rustc_hir::Node::Item(item) = node else { error_or_panic!(self, def_span, "Type is not an item?") }; if let rustc_hir::ItemKind::TyAlias(ty, _generics) = &item.kind { diff --git a/charon/tests/cargo/toml.out b/charon/tests/cargo/toml.out index 251fa78eb..882565dc6 100644 --- a/charon/tests/cargo/toml.out +++ b/charon/tests/cargo/toml.out @@ -5,7 +5,7 @@ enum core::option::Option = | Some(T) -fn core::option::{core::option::Option}::is_some<'_0, T>(@1: &'_0 (core::option::Option)) -> bool +fn core::option::{core::option::Option}::is_some<'_0, T, const host : bool>(@1: &'_0 (core::option::Option)) -> bool { let @0: bool; // return let self@1: &'_ (core::option::Option); // arg #1 @@ -33,7 +33,7 @@ fn test_cargo_toml::main() @3 := core::option::Option::Some { 0: const (false) } @2 := &@3 - @1 := core::option::{core::option::Option}::is_some(move (@2)) + @1 := core::option::{core::option::Option}::is_some(move (@2)) drop @2 @fake_read(@1) drop @3 diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 94d422aa1..5e5785b26 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -45,7 +45,7 @@ fn test_crate::array_to_mut_slice_<'_0, T>(@1: &'_0 mut (Array)) return } -fn core::slice::{Slice}::len<'_0, T>(@1: &'_0 (Slice)) -> usize +fn core::slice::{Slice}::len<'_0, T, const host : bool>(@1: &'_0 (Slice)) -> usize fn test_crate::array_len(@1: Array) -> usize { @@ -57,7 +57,7 @@ fn test_crate::array_len(@1: Array) -> usize @3 := &s@1 @2 := @ArrayToSliceShared<'_, T, 32 : usize>(move (@3)) drop @3 - @0 := core::slice::{Slice}::len(move (@2)) + @0 := core::slice::{Slice}::len(move (@2)) drop @2 drop s@1 return @@ -73,7 +73,7 @@ fn test_crate::shared_array_len<'_0, T>(@1: &'_0 (Array)) -> usiz @3 := &*(s@1) @2 := @ArrayToSliceShared<'_, T, 32 : usize>(move (@3)) drop @3 - @0 := core::slice::{Slice}::len(move (@2)) + @0 := core::slice::{Slice}::len(move (@2)) drop @2 return } @@ -85,7 +85,7 @@ fn test_crate::shared_slice_len<'_0, T>(@1: &'_0 (Slice)) -> usize let @2: &'_ (Slice); // anonymous local @2 := &*(s@1) - @0 := core::slice::{Slice}::len(move (@2)) + @0 := core::slice::{Slice}::len(move (@2)) drop @2 return } @@ -1125,7 +1125,7 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice)) -> u32 loop { @7 := copy (i@3) @9 := &*(s@1) - @8 := core::slice::{Slice}::len(move (@9)) + @8 := core::slice::{Slice}::len(move (@9)) drop @9 @6 := move (@7) < move (@8) if move (@6) { @@ -1198,10 +1198,10 @@ fn test_crate::sum2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) -> u sum@3 := const (0 : u32) @fake_read(sum@3) @7 := &*(s@1) - @6 := core::slice::{Slice}::len(move (@7)) + @6 := core::slice::{Slice}::len(move (@7)) drop @7 @9 := &*(s2@2) - @8 := core::slice::{Slice}::len(move (@9)) + @8 := core::slice::{Slice}::len(move (@9)) drop @9 @5 := move (@6) == move (@8) if move (@5) { @@ -1223,7 +1223,7 @@ fn test_crate::sum2<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) -> u loop { @14 := copy (i@10) @16 := &*(s@1) - @15 := core::slice::{Slice}::len(move (@16)) + @15 := core::slice::{Slice}::len(move (@16)) drop @16 @13 := move (@14) < move (@15) if move (@13) { @@ -1511,7 +1511,7 @@ fn test_crate::zero_slice<'_0>(@1: &'_0 mut (Slice)) i@2 := const (0 : usize) @fake_read(i@2) @4 := &*(a@1) - len@3 := core::slice::{Slice}::len(move (@4)) + len@3 := core::slice::{Slice}::len(move (@4)) drop @4 @fake_read(len@3) loop { @@ -1565,7 +1565,7 @@ fn test_crate::iter_mut_slice<'_0>(@1: &'_0 mut (Slice)) let @11: (); // anonymous local @3 := &*(a@1) - len@2 := core::slice::{Slice}::len(move (@3)) + len@2 := core::slice::{Slice}::len(move (@3)) drop @3 @fake_read(len@2) i@4 := const (0 : usize) @@ -1627,7 +1627,7 @@ fn test_crate::sum_mut_slice<'_0>(@1: &'_0 mut (Slice)) -> u32 loop { @7 := copy (i@2) @9 := &*(a@1) - @8 := core::slice::{Slice}::len(move (@9)) + @8 := core::slice::{Slice}::len(move (@9)) drop @9 @6 := move (@7) < move (@8) if move (@6) { diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out index 1c8743a5c..8a29279c3 100644 --- a/charon/tests/ui/external.out +++ b/charon/tests/ui/external.out @@ -1,6 +1,6 @@ # Final LLBC before serialization: -fn core::mem::swap<'_0, '_1, T>(@1: &'_0 mut (T), @2: &'_1 mut (T)) +fn core::mem::swap<'_0, '_1, T, const host : bool>(@1: &'_0 mut (T), @2: &'_1 mut (T)) fn test_crate::swap<'a, T>(@1: &'a mut (T), @2: &'a mut (T)) { @@ -12,7 +12,7 @@ fn test_crate::swap<'a, T>(@1: &'a mut (T), @2: &'a mut (T)) @3 := &two-phase-mut *(x@1) @4 := &two-phase-mut *(y@2) - @0 := core::mem::swap(move (@3), move (@4)) + @0 := core::mem::swap(move (@3), move (@4)) drop @4 drop @3 @0 := () @@ -26,9 +26,9 @@ enum core::option::Option = | Some(T) -fn core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new(@1: u32) -> core::option::Option +fn core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new(@1: u32) -> core::option::Option -fn core::option::{core::option::Option}::unwrap(@1: core::option::Option) -> T +fn core::option::{core::option::Option}::unwrap(@1: core::option::Option) -> T fn test_crate::test_new_non_zero_u32(@1: u32) -> core::num::nonzero::NonZeroU32 { @@ -38,9 +38,9 @@ fn test_crate::test_new_non_zero_u32(@1: u32) -> core::num::nonzero::NonZeroU32 let @3: u32; // anonymous local @3 := copy (x@1) - @2 := core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new(move (@3)) + @2 := core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new(move (@3)) drop @3 - @0 := core::option::{core::option::Option}::unwrap(move (@2)) + @0 := core::option::{core::option::Option}::unwrap(move (@2)) drop @2 return } diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index e3d3bee61..0b1d07e2e 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -145,10 +145,15 @@ struct core::ptr::unique::Unique = _marker: core::marker::PhantomData } +struct alloc::raw_vec::Cap = +{ + usize +} + struct alloc::raw_vec::RawVec = { ptr: core::ptr::unique::Unique, - cap: usize, + cap: alloc::raw_vec::Cap, alloc: A } @@ -190,7 +195,7 @@ fn test_crate::max() -> usize return } -trait core::cmp::PartialEq +trait core::cmp::PartialEq { fn eq : core::cmp::PartialEq::eq fn ne : core::cmp::PartialEq::ne @@ -198,7 +203,7 @@ trait core::cmp::PartialEq fn test_crate::partial_eq(@1: T) where - [@TraitClause0]: core::cmp::PartialEq, + [@TraitClause0]: core::cmp::PartialEq, { let @0: (); // return let _x@1: T; // arg #1 @@ -211,9 +216,9 @@ where return } -fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs, const host : bool>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool -fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +fn core::cmp::PartialEq::ne<'_0, '_1, Self, Rhs, const host : bool>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool { let @0: bool; // return let self@1: &'_ (Self); // arg #1 diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 6801961fe..ec91d0332 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -174,7 +174,7 @@ trait core::clone::Clone fn clone_from } -trait core::cmp::PartialEq +trait core::cmp::PartialEq { fn eq : core::cmp::PartialEq::eq fn ne @@ -188,7 +188,7 @@ enum core::cmp::Ordering = trait core::cmp::PartialOrd { - parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq + parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq fn partial_cmp : core::cmp::PartialOrd::partial_cmp fn lt fn le @@ -236,7 +236,7 @@ where trait core::cmp::Eq { - parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq + parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq fn assert_receiver_is_total_eq } @@ -318,14 +318,14 @@ impl core::clone::impls::{impl core::clone::Clone for u8#6} : core::clone::Clone fn clone = core::clone::impls::{impl core::clone::Clone for u8#6}::clone } -fn core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::eq<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::eq<'_0, '_1, const host : bool>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::ne<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::ne<'_0, '_1, const host : bool>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialEq for u8#22} : core::cmp::PartialEq +impl core::cmp::impls::{impl core::cmp::PartialEq for u8#22} : core::cmp::PartialEq { - fn eq = core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::eq - fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::ne + fn eq = core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::eq + fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::ne } fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::partial_cmp<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option @@ -340,7 +340,7 @@ fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::gt<'_0, '_1>(@1 impl core::cmp::impls::{impl core::cmp::PartialOrd for u8#56} : core::cmp::PartialOrd { - parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u8#22} + parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u8#22} fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::partial_cmp fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::lt fn le = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::le @@ -457,7 +457,7 @@ opaque type core::fmt::Arguments<'a> where 'a : 'a, -fn core::slice::{Slice}::len<'_0, T>(@1: &'_0 (Slice)) -> usize +fn core::slice::{Slice}::len<'_0, T, const host : bool>(@1: &'_0 (Slice)) -> usize fn test_crate::select<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) { @@ -494,11 +494,11 @@ fn test_crate::select<'_0, '_1>(@1: &'_0 (Slice), @2: &'_1 (Slice)) @4 := const (false) if move (@4) { @9 := &*(lhs@1) - @8 := core::slice::{Slice}::len(move (@9)) + @8 := core::slice::{Slice}::len(move (@9)) drop @9 @7 := &@8 @12 := &*(rhs@2) - @11 := core::slice::{Slice}::len(move (@12)) + @11 := core::slice::{Slice}::len(move (@12)) drop @12 @10 := &@11 @6 := (move (@7), move (@10)) @@ -565,7 +565,7 @@ fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> core::option::Option -fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs, const host : bool>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out index cca7bd8d9..dd0876c50 100644 --- a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out +++ b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out @@ -4,7 +4,7 @@ error: Unsupported statement kind: intrinsic 16 | let _ = x as isize; | ^^^^^^^^^^ -error: aborting due to previous error +error: aborting due to 1 previous error -[ ERROR charon_driver:231] The extraction encountered 1 errors +[ ERROR charon_driver:230] The extraction encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index a15833fdc..345e99808 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -903,7 +903,7 @@ trait core::clone::Clone fn clone_from } -trait core::cmp::PartialEq +trait core::cmp::PartialEq { fn eq : core::cmp::PartialEq::eq fn ne @@ -917,7 +917,7 @@ enum core::cmp::Ordering = trait core::cmp::PartialOrd { - parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq + parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq fn partial_cmp : core::cmp::PartialOrd::partial_cmp fn lt fn le @@ -965,7 +965,7 @@ where trait core::cmp::Eq { - parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq + parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq fn assert_receiver_is_total_eq } @@ -1047,14 +1047,14 @@ impl core::clone::impls::{impl core::clone::Clone for i32#14} : core::clone::Clo fn clone = core::clone::impls::{impl core::clone::Clone for i32#14}::clone } -fn core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::eq<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::eq<'_0, '_1, const host : bool>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::ne<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::ne<'_0, '_1, const host : bool>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialEq for i32#30} : core::cmp::PartialEq +impl core::cmp::impls::{impl core::cmp::PartialEq for i32#30} : core::cmp::PartialEq { - fn eq = core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::eq - fn ne = core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::ne + fn eq = core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::eq + fn ne = core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::ne } fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::partial_cmp<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option @@ -1069,7 +1069,7 @@ fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::gt<'_0, '_1>( impl core::cmp::impls::{impl core::cmp::PartialOrd for i32#72} : core::cmp::PartialOrd { - parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for i32#30} + parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for i32#30} fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::partial_cmp fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::lt fn le = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::le @@ -1115,14 +1115,14 @@ impl core::clone::impls::{impl core::clone::Clone for usize#5} : core::clone::Cl fn clone = core::clone::impls::{impl core::clone::Clone for usize#5}::clone } -fn core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::eq<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::eq<'_0, '_1, const host : bool>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::ne<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::ne<'_0, '_1, const host : bool>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialEq for usize#21} : core::cmp::PartialEq +impl core::cmp::impls::{impl core::cmp::PartialEq for usize#21} : core::cmp::PartialEq { - fn eq = core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::eq - fn ne = core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::ne + fn eq = core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::eq + fn ne = core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::ne } fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::partial_cmp<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option @@ -1137,7 +1137,7 @@ fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::gt<'_0, ' impl core::cmp::impls::{impl core::cmp::PartialOrd for usize#54} : core::cmp::PartialOrd { - parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for usize#21} + parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for usize#21} fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::partial_cmp fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::lt fn le = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::le @@ -1335,14 +1335,14 @@ impl core::clone::impls::{impl core::clone::Clone for u32#8} : core::clone::Clon fn clone = core::clone::impls::{impl core::clone::Clone for u32#8}::clone } -fn core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::eq<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::eq<'_0, '_1, const host : bool>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne<'_0, '_1, const host : bool>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialEq for u32#24} : core::cmp::PartialEq +impl core::cmp::impls::{impl core::cmp::PartialEq for u32#24} : core::cmp::PartialEq { - fn eq = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::eq - fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne + fn eq = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::eq + fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne } fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::partial_cmp<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option @@ -1357,7 +1357,7 @@ fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::gt<'_0, '_1>( impl core::cmp::impls::{impl core::cmp::PartialOrd for u32#60} : core::cmp::PartialOrd { - parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32#24} + parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32#24} fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::partial_cmp fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::lt fn le = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::le @@ -1862,7 +1862,7 @@ fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> core::option::Option -fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs, const host : bool>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output) diff --git a/charon/tests/ui/name-matcher-tests.out b/charon/tests/ui/name-matcher-tests.out index a16dfefc7..6bfbfe8b3 100644 --- a/charon/tests/ui/name-matcher-tests.out +++ b/charon/tests/ui/name-matcher-tests.out @@ -58,7 +58,7 @@ struct core::ops::range::RangeFrom = start: Idx } -fn core::option::{core::option::Option}::is_some<'_0, T>(@1: &'_0 (core::option::Option)) -> bool +fn core::option::{core::option::Option}::is_some<'_0, T, const host : bool>(@1: &'_0 (core::option::Option)) -> bool trait core::slice::index::private_slice_index::Sealed @@ -139,7 +139,7 @@ fn test_crate::foo() @3 := core::option::Option::Some { 0: const (0 : i32) } @2 := &@3 - @1 := core::option::{core::option::Option}::is_some(move (@2)) + @1 := core::option::{core::option::Option}::is_some(move (@2)) drop @2 @fake_read(@1) drop @3 diff --git a/charon/tests/ui/name-matcher-tests.rs b/charon/tests/ui/name-matcher-tests.rs index fb5ffd016..58291b05f 100644 --- a/charon/tests/ui/name-matcher-tests.rs +++ b/charon/tests/ui/name-matcher-tests.rs @@ -45,8 +45,8 @@ impl Trait> for Option { } // `call[i]` is a hack to be able to refer to `Call` statements inside the function body. -#[pattern::pass(call[0], "core::option::{core::option::Option<@T>}::is_some")] -#[pattern::pass(call[0], "core::option::{core::option::Option<@T>}::is_some<@T>")] +#[pattern::pass(call[0], "core::option::{core::option::Option<@T>}::is_some")] +#[pattern::pass(call[0], "core::option::{core::option::Option<@T>}::is_some<@T, @>")] // Generic arguments are required. #[pattern::fail(call[0], "core::option::{core::option::Option<@T>}::is_some")] #[pattern::pass(call[1], "ArrayToSliceShared<'_, bool, 1>")] diff --git a/charon/tests/ui/panics.out b/charon/tests/ui/panics.out index 394a82d8f..eb5a5011e 100644 --- a/charon/tests/ui/panics.out +++ b/charon/tests/ui/panics.out @@ -13,7 +13,7 @@ opaque type core::fmt::Arguments<'a> where 'a : 'a, -fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a>(@1: &'a (Slice<&'static (Str)>)) -> core::fmt::Arguments<'a> +fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a, const host : bool>(@1: &'a (Slice<&'static (Str)>)) -> core::fmt::Arguments<'a> fn test_crate::panic2() { @@ -29,7 +29,7 @@ fn test_crate::panic2() @3 := &*(@4) @2 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@3)) drop @3 - @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_>(move (@2)) + @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_, true>(move (@2)) drop @2 panic(core::panicking::panic_fmt) } @@ -117,7 +117,7 @@ fn test_crate::panic5() @5 := &*(@6) @4 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@5)) drop @5 - @3 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_>(move (@4)) + @3 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_, true>(move (@4)) drop @4 panic(core::panicking::panic_fmt) } diff --git a/charon/tests/ui/plain-panic-str.out b/charon/tests/ui/plain-panic-str.out index 350574917..2db66489f 100644 --- a/charon/tests/ui/plain-panic-str.out +++ b/charon/tests/ui/plain-panic-str.out @@ -4,7 +4,7 @@ opaque type core::fmt::Arguments<'a> where 'a : 'a, -fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a>(@1: &'a (Slice<&'static (Str)>)) -> core::fmt::Arguments<'a> +fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a, const host : bool>(@1: &'a (Slice<&'static (Str)>)) -> core::fmt::Arguments<'a> fn test_crate::main() { @@ -20,7 +20,7 @@ fn test_crate::main() @3 := &*(@4) @2 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@3)) drop @3 - @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_>(move (@2)) + @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_, true>(move (@2)) drop @2 panic(core::panicking::panic_fmt) } diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index f6d368467..fb1987199 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -9,7 +9,7 @@ enum core::option::Option = | Some(T) -trait core::cmp::PartialEq +trait core::cmp::PartialEq { fn eq : core::cmp::PartialEq::eq fn ne @@ -17,7 +17,7 @@ trait core::cmp::PartialEq trait core::cmp::Eq { - parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq + parent_clause_0 : [@TraitClause0]: core::cmp::PartialEq fn assert_receiver_is_total_eq } @@ -91,19 +91,19 @@ impl core::hash::impls::{impl core::hash::Hash for u32#11} : core::hash::Hash for u32#24}::eq<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::eq<'_0, '_1, const host : bool>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne<'_0, '_1, const host : bool>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialEq for u32#24} : core::cmp::PartialEq +impl core::cmp::impls::{impl core::cmp::PartialEq for u32#24} : core::cmp::PartialEq { - fn eq = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::eq - fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne + fn eq = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::eq + fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne } impl core::cmp::impls::{impl core::cmp::Eq for u32#41} : core::cmp::Eq { - parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32#24} + parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32#24} } opaque type std::hash::random::DefaultHasher @@ -227,7 +227,7 @@ fn test_crate::get_or_insert<'_0>(@1: &'_0 mut (std::collections::hash::map::Has fn core::borrow::Borrow::borrow<'_0, Self, Borrowed>(@1: &'_0 (Self)) -> &'_0 (Borrowed) -fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool +fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs, const host : bool>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool fn core::hash::Hash::hash<'_0, '_1, Self, H>(@1: &'_0 (Self), @2: &'_1 mut (H)) where diff --git a/charon/tests/ui/predicates-on-late-bound-vars.out b/charon/tests/ui/predicates-on-late-bound-vars.out index 965a7182a..b7138f25b 100644 --- a/charon/tests/ui/predicates-on-late-bound-vars.out +++ b/charon/tests/ui/predicates-on-late-bound-vars.out @@ -50,7 +50,7 @@ opaque type core::cell::Ref<'b, T> struct core::cell::BorrowError = {} -fn core::cell::{core::cell::RefCell#21}::new(@1: T) -> core::cell::RefCell +fn core::cell::{core::cell::RefCell#21}::new(@1: T) -> core::cell::RefCell fn core::cell::{core::cell::RefCell#22}::try_borrow<'_0, T>(@1: &'_0 (core::cell::RefCell)) -> core::result::Result, core::cell::BorrowError> @@ -62,7 +62,7 @@ fn test_crate::foo() let @3: &'_ (core::cell::RefCell); // anonymous local let @4: (); // anonymous local - ref_b@1 := core::cell::{core::cell::RefCell#21}::new(const (false)) + ref_b@1 := core::cell::{core::cell::RefCell#21}::new(const (false)) @fake_read(ref_b@1) @3 := &ref_b@1 @2 := core::cell::{core::cell::RefCell#22}::try_borrow(move (@3)) diff --git a/charon/tests/ui/rename_attribute_failure.out b/charon/tests/ui/rename_attribute_failure.out index 4ed9f0843..8894bc0b7 100644 --- a/charon/tests/ui/rename_attribute_failure.out +++ b/charon/tests/ui/rename_attribute_failure.out @@ -36,5 +36,5 @@ error: Error parsing attribute: Unrecognized attribute: `something_else("_Type36 error: aborting due to 6 previous errors -[ ERROR charon_driver:231] The extraction encountered 6 errors +[ ERROR charon_driver:230] The extraction encountered 6 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/issue-165-vec-macro.out b/charon/tests/ui/unsupported/issue-165-vec-macro.out index 2b350d429..8b270a0ce 100644 --- a/charon/tests/ui/unsupported/issue-165-vec-macro.out +++ b/charon/tests/ui/unsupported/issue-165-vec-macro.out @@ -6,7 +6,7 @@ error: Nullary operations are not supported | = note: this error originates in the macro `vec` (in Nightly builds, run with -Z macro-backtrace for more info) -error: aborting due to previous error +error: aborting due to 1 previous error -[ ERROR charon_driver:231] The extraction encountered 1 errors +[ ERROR charon_driver:230] The extraction encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/projection-index-from-end.out b/charon/tests/ui/unsupported/projection-index-from-end.out index fc28cb565..d42f5898f 100644 --- a/charon/tests/ui/unsupported/projection-index-from-end.out +++ b/charon/tests/ui/unsupported/projection-index-from-end.out @@ -4,7 +4,7 @@ error: Unexpected ProjectionElem::ConstantIndex 4 | [.., _named] => (), | ^^^^^^ -error: aborting due to previous error +error: aborting due to 1 previous error -[ ERROR charon_driver:231] The extraction encountered 1 errors +[ ERROR charon_driver:230] The extraction encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/unbound-lifetime.out b/charon/tests/ui/unsupported/unbound-lifetime.out index 0a7cd7f14..a8910f71c 100644 --- a/charon/tests/ui/unsupported/unbound-lifetime.out +++ b/charon/tests/ui/unsupported/unbound-lifetime.out @@ -27,5 +27,5 @@ error: Ignoring the following item due to an error: test_crate::get error: aborting due to 3 previous errors For more information about this error, try `rustc --explain E0261`. -[ ERROR charon_driver:231] The extraction encountered 2 errors +[ ERROR charon_driver:230] The extraction encountered 2 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/well-formedness-bound.out b/charon/tests/ui/unsupported/well-formedness-bound.out index d45e26bfa..99caa3ad0 100644 --- a/charon/tests/ui/unsupported/well-formedness-bound.out +++ b/charon/tests/ui/unsupported/well-formedness-bound.out @@ -14,5 +14,5 @@ error: Ignoring the following item due to an error: test_crate::get error: aborting due to 2 previous errors -[ ERROR charon_driver:231] The extraction encountered 2 errors +[ ERROR charon_driver:230] The extraction encountered 2 errors Error: Charon driver exited with code 1 diff --git a/flake.lock b/flake.lock index 95d20de5e..2b2c04ac6 100644 --- a/flake.lock +++ b/flake.lock @@ -87,11 +87,11 @@ ] }, "locked": { - "lastModified": 1701656211, - "narHash": "sha256-lfFXsLWH4hVbEKR6K+UcDiKxeS6Lz4FkC1DZ9LHqf9Y=", + "lastModified": 1718245100, + "narHash": "sha256-ETm3A2nUVEUwVQ30fj3ePK4rqsSbSnY4uP4LYrFrDNE=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "47a276e820ae4ae1b8d98a503bf09d2ceb52dfd8", + "rev": "4cbc2810d1dfb5960791be92df6a5f842a79bdfb", "type": "github" }, "original": { diff --git a/rust-toolchain b/rust-toolchain index 94321c67a..10e5aac92 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-11-16" +channel = "nightly-2024-01-01" components = [ "rustc-dev", "llvm-tools-preview" ]