diff --git a/rust-toolchain.toml b/rust-toolchain.toml index ff2b9dc75..55247438b 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,4 +1,4 @@ [toolchain] -channel = "1.76.0" -# channel = "nightly-2023-09-29" # (not officially supported) +channel = "1.79.0" +# channel = "nightly-2023-09-29" # TODO update to match 1.79.0 (not officially supported) components = [ "rustc", "rust-std", "cargo", "rustfmt", "rustc-dev", "llvm-tools" ] diff --git a/source/builtin/src/lib.rs b/source/builtin/src/lib.rs index cb2a66626..fbbdd5e89 100644 --- a/source/builtin/src/lib.rs +++ b/source/builtin/src/lib.rs @@ -167,9 +167,7 @@ pub fn no_unwind_when(_b: bool) { #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::reveal_hide"] #[verifier::proof] -pub fn reveal_hide_(_f: fn(), _n: u32) { - unimplemented!(); -} +pub const fn reveal_hide_(_f: fn(), _n: u32) {} #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::reveal_hide_internal_path"] @@ -377,14 +375,15 @@ impl Ghost { #[rustc_diagnostic_item = "verus::builtin::Ghost::view"] #[verifier::spec] pub fn view(self) -> A { - unimplemented!() + unsafe { core::mem::MaybeUninit::uninit().assume_init() } } #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::Ghost::new"] #[verifier::spec] #[verifier::external_body] - pub fn new(_a: A) -> Ghost { + pub const fn new(_a: A) -> Ghost { + core::mem::forget(_a); Ghost { phantom: PhantomData } } @@ -411,7 +410,10 @@ impl Ghost { #[verifier::spec] #[verifier::external_body] pub fn borrow(&self) -> &A { - unimplemented!() + #[allow(deref_nullptr)] + unsafe { + &*(0 as *const A) + } } // note that because we return #[verifier::spec], not #[verifier::exec], we do not implement the BorrowMut trait @@ -420,7 +422,10 @@ impl Ghost { #[verifier::proof] #[verifier::external] pub fn borrow_mut(#[verifier::proof] &mut self) -> &mut A { - unimplemented!() + #[allow(deref_nullptr)] + unsafe { + &mut *(0 as *mut A) + } } } @@ -429,14 +434,15 @@ impl Tracked { #[rustc_diagnostic_item = "verus::builtin::Tracked::view"] #[verifier::spec] pub fn view(self) -> A { - unimplemented!() + unsafe { core::mem::MaybeUninit::uninit().assume_init() } } #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::Tracked::new"] #[verifier::proof] #[verifier::external_body] - pub fn new(#[verifier::proof] _a: A) -> Tracked { + pub const fn new(#[verifier::proof] _a: A) -> Tracked { + core::mem::forget(_a); Tracked { phantom: PhantomData } } @@ -459,8 +465,8 @@ impl Tracked { #[verifier::proof] #[verifier::external_body] #[verifier::returns(proof)] - pub fn get(#[verifier::proof] self) -> A { - unimplemented!() + pub const fn get(#[verifier::proof] self) -> A { + unsafe { core::mem::MaybeUninit::uninit().assume_init() } } // note that because we return #[verifier::proof], not #[verifier::exec], we do not implement the Borrow trait @@ -470,7 +476,10 @@ impl Tracked { #[verifier::external_body] #[verifier::returns(proof)] pub fn borrow(#[verifier::proof] &self) -> &A { - unimplemented!() + #[allow(deref_nullptr)] + unsafe { + &*(0 as *const A) + } } // note that because we return #[verifier::proof], not #[verifier::exec], we do not implement the BorrowMut trait @@ -480,7 +489,10 @@ impl Tracked { #[verifier::external_body] #[verifier::returns(proof)] pub fn borrow_mut(#[verifier::proof] &mut self) -> &mut A { - unimplemented!() + #[allow(deref_nullptr)] + unsafe { + &mut *(0 as *mut A) + } } } @@ -507,14 +519,16 @@ impl Copy for Tracked {} #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::ghost_exec"] #[verifier::external_body] -pub fn ghost_exec(#[verifier::spec] _a: A) -> Ghost { +pub const fn ghost_exec(#[verifier::spec] _a: A) -> Ghost { + core::mem::forget(_a); Ghost::assume_new() } #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::tracked_exec"] #[verifier::external_body] -pub fn tracked_exec(#[verifier::proof] _a: A) -> Tracked { +pub const fn tracked_exec(#[verifier::proof] _a: A) -> Tracked { + core::mem::forget(_a); Tracked::assume_new() } @@ -1466,9 +1480,7 @@ pub fn infer_spec_for_loop_iter(_: A, _print_hint: bool) -> Option { #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::global_size_of"] #[verifier::spec] -pub const fn global_size_of(_bytes: usize) { - unimplemented!() -} +pub const fn global_size_of(_bytes: usize) {} #[cfg(verus_keep_ghost)] #[rustc_diagnostic_item = "verus::builtin::inline_air_stmt"] diff --git a/source/builtin_macros/src/attr_block_trait.rs b/source/builtin_macros/src/attr_block_trait.rs index 744e61456..3d7ddb090 100644 --- a/source/builtin_macros/src/attr_block_trait.rs +++ b/source/builtin_macros/src/attr_block_trait.rs @@ -3,6 +3,7 @@ use syn::{ }; pub trait AnyAttrBlock { + #[allow(dead_code)] fn attrs_mut(&mut self) -> &mut Vec; fn block_mut(&mut self) -> Option<&mut Block>; } diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index 283a2fe7b..2dab1230b 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -419,13 +419,15 @@ impl Visitor { let decreases = self.take_ghost(&mut sig.decreases); let opens_invariants = self.take_ghost(&mut sig.invariants); let unwind = self.take_ghost(&mut sig.unwind); + + let mut spec_stmts = Vec::new(); // TODO: wrap specs inside ghost blocks if let Some(Requires { token, mut exprs }) = requires { if exprs.exprs.len() > 0 { for expr in exprs.exprs.iter_mut() { self.visit_expr_mut(expr); } - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, token.span => #builtin::requires([#exprs])), ), @@ -438,13 +440,13 @@ impl Visitor { for expr in exprs.exprs.iter_mut() { self.visit_expr_mut(expr); } - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim(quote_spanned_builtin!(builtin, token.span => #builtin::recommends([#exprs]))), Semi { spans: [token.span] }, )); } if let Some((via_token, via_expr)) = via { - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, via_expr.span() => #builtin::recommends_by(#via_expr)), ), @@ -468,7 +470,7 @@ impl Visitor { "when using #![trigger f(x)], at least one ensures is required"; let expr = Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err))); - stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] })); + spec_stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] })); false } else { let e = take_expr(&mut exprs.exprs[0]); @@ -501,14 +503,14 @@ impl Visitor { }; if cont { if let Some((p, ty)) = ret_pat { - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, token.span => #builtin::ensures(|#p: #ty| [#exprs])), ), Semi { spans: [token.span] }, )); } else { - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, token.span => #builtin::ensures([#exprs])), ), @@ -539,7 +541,7 @@ impl Visitor { if matches!(expr, Expr::Tuple(..)) { let err = "decreases cannot be a tuple; use `decreases x, y` rather than `decreases (x, y)`"; let expr = Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err))); - stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] })); + spec_stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] })); } } stmts.push(Stmt::Semi( @@ -550,7 +552,7 @@ impl Visitor { )); if let Some((when_token, mut when_expr)) = when { self.visit_expr_mut(&mut when_expr); - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, when_expr.span() => #builtin::decreases_when(#when_expr)), ), @@ -558,7 +560,7 @@ impl Visitor { )); } if let Some((via_token, via_expr)) = via { - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, via_expr.span() => #builtin::decreases_by(#via_expr)), ), @@ -569,7 +571,7 @@ impl Visitor { if let Some(SignatureInvariants { token: _, set }) = opens_invariants { match set { InvariantNameSet::Any(any) => { - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, any.span() => #builtin::opens_invariants_any()), ), @@ -577,7 +579,7 @@ impl Visitor { )); } InvariantNameSet::None(none) => { - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, none.span() => #builtin::opens_invariants_none()), ), @@ -588,7 +590,7 @@ impl Visitor { for expr in exprs.iter_mut() { self.visit_expr_mut(expr); } - stmts.push(Stmt::Semi( + spec_stmts.push(Stmt::Semi( Expr::Verbatim( quote_spanned_builtin!(builtin, bracket_token.span => #builtin::opens_invariants([#exprs])), ), @@ -597,6 +599,15 @@ impl Visitor { } } } + + if !self.erase_ghost.erase() { + if sig.constness.is_some() { + stmts.push(Stmt::Expr(Expr::Verbatim(quote_spanned!(sig.span() => #[verus::internal(const_header_wrapper)] || { #(#spec_stmts)* };)))); + } else { + stmts.extend(spec_stmts); + } + } + if let Some(SignatureUnwind { token, when }) = unwind { if let Some((when_token, mut when_expr)) = when { self.visit_expr_mut(&mut when_expr); @@ -635,41 +646,61 @@ impl Visitor { pub fn desugar_const_or_static( &mut self, + con_mode: &FnMode, con_ensures: &mut Option, con_block: &mut Option>, con_expr: &mut Option>, con_eq_token: &mut Option, con_semi_token: &mut Option, + con_ty: &Type, con_span: Span, ) { - let ensures = self.take_ghost(con_ensures); - if let Some(Ensures { token, mut exprs, attrs }) = ensures { - self.inside_ghost += 1; - let mut stmts: Vec = Vec::new(); - if attrs.len() > 0 { - let err = "outer attributes only allowed on function's ensures"; - let expr = Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err))); - stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] })); - } else if exprs.exprs.len() > 0 { - for expr in exprs.exprs.iter_mut() { - self.visit_expr_mut(expr); + if matches!(con_mode, FnMode::Spec(_) | FnMode::SpecChecked(_)) { + if let Some(mut expr) = con_expr.take() { + let mut stmts = Vec::new(); + self.inside_ghost += 1; + self.visit_expr_mut(&mut expr); + self.inside_ghost -= 1; + stmts.push(Stmt::Expr(Expr::Verbatim(quote_spanned!(con_span => #[verus::internal(verus_macro)] #[verus::internal(const_body)] fn __VERUS_CONST_BODY__() -> #con_ty { #expr } )))); + stmts.push(Stmt::Expr(Expr::Verbatim( + quote_spanned!(con_span => unsafe { core::mem::zeroed() }), + ))); + *con_expr = Some(Box::new(Expr::Block(syn_verus::ExprBlock { + attrs: vec![], + label: None, + block: Block { brace_token: token::Brace(expr.span()), stmts }, + }))); + } + } else { + let ensures = self.take_ghost(con_ensures); + if let Some(Ensures { token, mut exprs, attrs }) = ensures { + self.inside_ghost += 1; + let mut stmts: Vec = Vec::new(); + if attrs.len() > 0 { + let err = "outer attributes only allowed on function's ensures"; + let expr = Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err))); + stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] })); + } else if exprs.exprs.len() > 0 { + for expr in exprs.exprs.iter_mut() { + self.visit_expr_mut(expr); + } + // Use a closure in the ensures to avoid circular const definition. + // Note: we can't use con.ident as the closure pattern, + // because Rust would treat this as a const path pattern. + // So we use a 0-parameter closure. + stmts.push(stmt_with_semi!(builtin, token.span => #[verus::internal(const_header_wrapper)] || { #builtin::ensures(|| [#exprs]); })); } - // Use a closure in the ensures to avoid circular const definition. - // Note: we can't use con.ident as the closure pattern, - // because Rust would treat this as a const path pattern. - // So we use a 0-parameter closure. - stmts.push(stmt_with_semi!(builtin, token.span => #builtin::ensures(|| [#exprs]))); + let mut block = std::mem::take(con_block).expect("const-with-ensures block"); + block.stmts.splice(0..0, stmts); + *con_block = Some(block); + self.inside_ghost -= 1; + } + if let Some(block) = std::mem::take(con_block) { + let expr_block = syn_verus::ExprBlock { attrs: vec![], label: None, block: *block }; + *con_expr = Some(Box::new(Expr::Block(expr_block))); + *con_eq_token = Some(syn_verus::token::Eq { spans: [con_span] }); + *con_semi_token = Some(Semi { spans: [con_span] }); } - let mut block = std::mem::take(con_block).expect("const-with-ensures block"); - block.stmts.splice(0..0, stmts); - *con_block = Some(block); - self.inside_ghost -= 1; - } - if let Some(block) = std::mem::take(con_block) { - let expr_block = syn_verus::ExprBlock { attrs: vec![], label: None, block: *block }; - *con_expr = Some(Box::new(Expr::Block(expr_block))); - *con_eq_token = Some(syn_verus::token::Eq { spans: [con_span] }); - *con_semi_token = Some(Semi { spans: [con_span] }); } } @@ -680,7 +711,7 @@ impl Visitor { vis: Option<&Visibility>, publish: &mut Publish, mode: &mut FnMode, - ) { + ) -> FnMode { if self.erase_ghost.keep() { attrs.push(mk_verus_attr(span, quote! { verus_macro })); } @@ -714,10 +745,12 @@ impl Visitor { self.inside_ghost = inside_ghost; self.inside_const = true; *publish = Publish::Default; + let orig_mode = mode.clone(); *mode = FnMode::Default; attrs.extend(publish_attrs); attrs.extend(mode_attrs); self.filter_attrs(attrs); + orig_mode } } @@ -1063,16 +1096,24 @@ impl Visitor { } }; let span = item.span(); - let static_assert_size = quote! { - if ::core::mem::size_of::<#type_>() != #size_lit { - panic!("does not have the expected size"); + let static_assert_size = if self.erase_ghost.erase() { + quote! { + if ::core::mem::size_of::<#type_>() != #size_lit { + panic!("does not have the expected size"); + } } + } else { + quote! {} }; let static_assert_align = if let Some(align_lit) = align_lit { - quote! { - if ::core::mem::align_of::<#type_>() != #align_lit { - panic!("does not have the expected alignment"); + if self.erase_ghost.erase() { + quote! { + if ::core::mem::align_of::<#type_>() != #align_lit { + panic!("does not have the expected alignment"); + } } + } else { + quote! {} } } else { quote! {} @@ -2994,7 +3035,7 @@ impl VisitMut for Visitor { } fn visit_item_const_mut(&mut self, con: &mut ItemConst) { - self.visit_const_or_static( + let mode = self.visit_const_or_static( con.const_token.span, &mut con.attrs, Some(&con.vis), @@ -3002,18 +3043,20 @@ impl VisitMut for Visitor { &mut con.mode, ); self.desugar_const_or_static( + &mode, &mut con.ensures, &mut con.block, &mut con.expr, &mut con.eq_token, &mut con.semi_token, + &con.ty, con.const_token.span, ); visit_item_const_mut(self, con); } fn visit_item_static_mut(&mut self, sta: &mut ItemStatic) { - self.visit_const_or_static( + let mode = self.visit_const_or_static( sta.static_token.span, &mut sta.attrs, Some(&sta.vis), @@ -3021,11 +3064,13 @@ impl VisitMut for Visitor { &mut sta.mode, ); self.desugar_const_or_static( + &mode, &mut sta.ensures, &mut sta.block, &mut sta.expr, &mut sta.eq_token, &mut sta.semi_token, + &sta.ty, sta.static_token.span, ); visit_item_static_mut(self, sta); diff --git a/source/lifetime_generate_works.txt b/source/lifetime_generate_works.txt new file mode 100644 index 000000000..6ed22c96f --- /dev/null +++ b/source/lifetime_generate_works.txt @@ -0,0 +1 @@ +42305cc9 diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs index e74398a9a..dfb019b4f 100644 --- a/source/rust_verify/src/attributes.rs +++ b/source/rust_verify/src/attributes.rs @@ -293,6 +293,10 @@ pub(crate) enum Attr { UnwrappedBinding, // Marks the auxiliary function constructed by reveal/hide InternalRevealFn, + // Marks the auxiliary function constructed by spec const + InternalConstBody, + // Marks the auxiliary function constructed to wrap the ensures of a const + InternalEnsuresWrapper, // Marks trusted code Trusted, // global size_of @@ -614,6 +618,12 @@ pub(crate) fn parse_attrs( AttrTree::Fun(_, arg, None) if arg == "reveal_fn" => { v.push(Attr::InternalRevealFn) } + AttrTree::Fun(_, arg, None) if arg == "const_body" => { + v.push(Attr::InternalConstBody) + } + AttrTree::Fun(_, arg, None) if arg == "const_header_wrapper" => { + v.push(Attr::InternalEnsuresWrapper) + } AttrTree::Fun(_, arg, None) if arg == "broadcast_use_reveal" => { v.push(Attr::BroadcastUseReveal) } @@ -828,6 +838,8 @@ pub(crate) struct VerifierAttrs { pub(crate) unwrapped_binding: bool, pub(crate) sets_mode: bool, pub(crate) internal_reveal_fn: bool, + pub(crate) internal_const_body: bool, + pub(crate) internal_const_header_wrapper: bool, pub(crate) broadcast_use_reveal: bool, pub(crate) trusted: bool, pub(crate) internal_get_field_many_variants: bool, @@ -932,6 +944,8 @@ pub(crate) fn get_verifier_attrs( unwrapped_binding: false, sets_mode: false, internal_reveal_fn: false, + internal_const_body: false, + internal_const_header_wrapper: false, broadcast_use_reveal: false, trusted: false, size_of_global: false, @@ -996,6 +1010,8 @@ pub(crate) fn get_verifier_attrs( Attr::UnwrappedBinding => vs.unwrapped_binding = true, Attr::Mode(_) => vs.sets_mode = true, Attr::InternalRevealFn => vs.internal_reveal_fn = true, + Attr::InternalConstBody => vs.internal_const_body = true, + Attr::InternalEnsuresWrapper => vs.internal_const_header_wrapper = true, Attr::BroadcastUseReveal => vs.broadcast_use_reveal = true, Attr::Trusted => vs.trusted = true, Attr::SizeOfGlobal => vs.size_of_global = true, diff --git a/source/rust_verify/src/hir_hide_reveal_rewrite.rs b/source/rust_verify/src/hir_hide_reveal_rewrite.rs index ea22c7a62..d0f397ea5 100644 --- a/source/rust_verify/src/hir_hide_reveal_rewrite.rs +++ b/source/rust_verify/src/hir_hide_reveal_rewrite.rs @@ -169,7 +169,6 @@ pub(crate) fn hir_hide_reveal_rewrite<'tcx>( let body = tcx.hir_arena.alloc(rustc_hir::Body { params: old_body.params, value: expr, - coroutine_kind: old_body.coroutine_kind, }); bodies[&body_id.hir_id.local_id] = body; diff --git a/source/rust_verify/src/lifetime.rs b/source/rust_verify/src/lifetime.rs index 41405bbcd..f7cb19e92 100644 --- a/source/rust_verify/src/lifetime.rs +++ b/source/rust_verify/src/lifetime.rs @@ -173,11 +173,9 @@ pub(crate) fn check<'tcx>(queries: &'tcx rustc_interface::Queries<'tcx>) { queries.global_ctxt().expect("global_ctxt").enter(|tcx| { let hir = tcx.hir(); let krate = hir.krate(); - match rustc_hir_analysis::check_crate(tcx) { - Ok(()) => {} - Err(_) => { - return; - } + rustc_hir_analysis::check_crate(tcx); + if tcx.dcx().err_count() != 0 { + return; } for owner in &krate.owners { if let MaybeOwner::Owner(owner) = owner { diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 49a87d5ac..2e3bd9aa6 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -5,13 +5,13 @@ use crate::rust_to_vir_expr::{get_adt_res_struct_enum, get_adt_res_struct_enum_u use crate::verus_items::{BuiltinTypeItem, RustItem, VerusItem, VerusItems}; use crate::{lifetime_ast::*, verus_items}; use air::ast_util::str_ident; -use rustc_ast::{BorrowKind, IsAuto, Mutability}; +use rustc_ast::{BindingMode, BorrowKind, IsAuto, Mutability}; use rustc_hir::def::{CtorKind, DefKind, Res}; use rustc_hir::{ - AssocItemKind, BindingAnnotation, Block, BlockCheckMode, BodyId, Closure, Crate, Expr, - ExprKind, FnSig, HirId, Impl, ImplItem, ImplItemKind, ItemKind, Let, MaybeOwner, Node, - OpaqueTy, OpaqueTyOrigin, OwnerNode, Pat, PatKind, Stmt, StmtKind, TraitFn, TraitItem, - TraitItemKind, TraitItemRef, UnOp, Unsafety, + AssocItemKind, Block, BlockCheckMode, BodyId, Closure, Crate, Expr, ExprKind, FnSig, HirId, + Impl, ImplItem, ImplItemKind, ItemKind, LetExpr, LetStmt, MaybeOwner, Node, OpaqueTy, + OpaqueTyOrigin, OwnerNode, Pat, PatKind, Stmt, StmtKind, TraitFn, TraitItem, TraitItemKind, + TraitItemRef, UnOp, Unsafety, }; use rustc_middle::ty::{ AdtDef, BoundRegionKind, BoundVariableKind, ClauseKind, Const, GenericArgKind, @@ -503,7 +503,7 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ TyKind::Tuple(_) => Box::new(TypX::Tuple( ty.tuple_fields().iter().map(|t| erase_ty(ctxt, state, &t)).collect(), )), - TyKind::RawPtr(rustc_middle::ty::TypeAndMut { ty: t, mutbl }) => { + TyKind::RawPtr(t, mutbl) => { let ty = erase_ty(ctxt, state, t); Box::new(TypX::RawPtr(ty, *mutbl)) } @@ -675,7 +675,7 @@ fn erase_pat<'tcx>(ctxt: &Context<'tcx>, state: &mut State, pat: &Pat<'tcx>) -> mk_pat(PatternX::Wildcard) } else { let id = state.local(&x.to_string(), hir_id.local_id.index()); - let BindingAnnotation(_, mutability) = ann; + let BindingMode(_, mutability) = ann; mk_pat(PatternX::Binding(id, mutability.to_owned(), None)) } } @@ -684,7 +684,7 @@ fn erase_pat<'tcx>(ctxt: &Context<'tcx>, state: &mut State, pat: &Pat<'tcx>) -> erase_pat(ctxt, state, subpat) } else { let id = state.local(&x.to_string(), hir_id.local_id.index()); - let BindingAnnotation(_, mutability) = ann; + let BindingMode(_, mutability) = ann; let subpat = erase_pat(ctxt, state, subpat); mk_pat(PatternX::Binding(id, mutability.to_owned(), Some(subpat))) } @@ -1106,7 +1106,7 @@ fn erase_match<'tcx>( expect_spec: bool, expr: &Expr<'tcx>, cond: &Expr<'tcx>, - arms: Vec<(Option<&Pat<'tcx>>, &Option>, Option<&Expr<'tcx>>)>, + arms: Vec<(Option<&Pat<'tcx>>, &Option<&Expr<'tcx>>, Option<&Expr<'tcx>>)>, ) -> Option { let expr_typ = |state: &mut State| erase_ty(ctxt, state, &ctxt.types().node_type(expr.hir_id)); let mk_exp1 = |e: ExpX| Box::new((expr.span, e)); @@ -1123,8 +1123,7 @@ fn erase_match<'tcx>( }; let guard = match guard_opt { None => None, - Some(rustc_hir::Guard::If(guard)) => erase_expr(ctxt, state, cond_spec, guard), - _ => panic!("unexpected guard"), + Some(guard) => erase_expr(ctxt, state, cond_spec, guard), }; let (body, body_span) = if let Some(b) = body_expr { (erase_expr(ctxt, state, expect_spec, b), b.span) @@ -1175,7 +1174,7 @@ fn erase_inv_block<'tcx>( let inner_pat = match &inner_pat.kind { PatKind::Binding(ann, hir_id, x, None) => { let id = state.local(&x.to_string(), hir_id.local_id.index()); - let BindingAnnotation(_, mutability) = ann; + let BindingMode(_, mutability) = ann; Box::new((inner_pat.span, PatternX::Binding(id, mutability.to_owned(), None))) } _ => { @@ -1210,6 +1209,9 @@ fn erase_expr<'tcx>( match res { Res::Local(id) => match ctxt.tcx.hir_node(id) { Node::Pat(Pat { kind: PatKind::Binding(_ann, id, ident, _pat), .. }) => { + if !ctxt.var_modes.contains_key(&expr.hir_id) { + dbg!(expr); + } if expect_spec || ctxt.var_modes[&expr.hir_id] == Mode::Spec { None } else { @@ -1270,7 +1272,7 @@ fn erase_expr<'tcx>( return mk_exp(ExpX::Call(fun_exp, vec![], vec![])); } } - Res::Def(DefKind::Static(_), id) => { + Res::Def(DefKind::Static { mutability: Mutability::Not, nested: false }, id) => { if expect_spec || ctxt.var_modes[&expr.hir_id] == Mode::Spec { None } else { @@ -1539,7 +1541,7 @@ fn erase_expr<'tcx>( let cond_spec = ctxt.condition_modes[&expr.hir_id] == Mode::Spec; let cond = cond.peel_drop_temps(); match cond.kind { - ExprKind::Let(Let { pat, init: src_expr, .. }) => { + ExprKind::Let(LetExpr { pat, init: src_expr, .. }) => { let arm1 = (Some(pat.to_owned()), &None, Some(*lhs)); let arm2 = (None, &None, *rhs); erase_match(ctxt, state, expect_spec, expr, src_expr, vec![arm1, arm2]) @@ -1603,12 +1605,7 @@ fn erase_expr<'tcx>( let exp = erase_expr(ctxt, state, ctxt.ret_spec.expect("ret_spec"), expr); mk_exp(ExpX::Ret(exp)) } - ExprKind::Closure(Closure { - capture_clause: capture_by, - body: body_id, - movability, - .. - }) => { + ExprKind::Closure(Closure { capture_clause: capture_by, body: body_id, .. }) => { let mut params: Vec<(Span, Id, Typ)> = Vec::new(); let body = ctxt.tcx.hir().body(*body_id); let ps = &body.params; @@ -1626,7 +1623,7 @@ fn erase_expr<'tcx>( } let body_exp = erase_expr(ctxt, state, expect_spec, &body.value); let body_exp = force_block(body_exp, body.value.span); - mk_exp(ExpX::Closure(*capture_by, *movability, params, body_exp)) + mk_exp(ExpX::Closure(*capture_by, None, params, body_exp)) } ExprKind::Block(block, None) => { let attrs = ctxt.tcx.hir().attrs(expr.hir_id); @@ -1677,10 +1674,10 @@ fn erase_stmt<'tcx>(ctxt: &Context<'tcx>, state: &mut State, stmt: &Stmt<'tcx>) vec![] } } - StmtKind::Local(local) => { - let mode = ctxt.var_modes[&local.pat.hir_id]; + StmtKind::Let(LetStmt { pat, ty: _, init, els: _, hir_id, span: _, source: _ }) => { + let mode = ctxt.var_modes[&pat.hir_id]; if mode == Mode::Spec { - if let Some(init) = local.init { + if let Some(init) = init { if let Some(e) = erase_expr(ctxt, state, true, init) { vec![Box::new((stmt.span, StmX::Expr(e)))] } else { @@ -1690,13 +1687,10 @@ fn erase_stmt<'tcx>(ctxt: &Context<'tcx>, state: &mut State, stmt: &Stmt<'tcx>) vec![] } } else { - let pat = erase_pat(ctxt, state, &local.pat); - let typ = erase_ty(ctxt, state, &ctxt.types().node_type(local.pat.hir_id)); - let init_exp = if let Some(init) = local.init { - erase_expr(ctxt, state, false, init) - } else { - None - }; + let pat: Pattern = erase_pat(ctxt, state, pat); + let typ = erase_ty(ctxt, state, &ctxt.types().node_type(*hir_id)); + let init_exp = + if let Some(init) = init { erase_expr(ctxt, state, false, init) } else { None }; vec![Box::new((stmt.span, StmX::Let(pat, typ, init_exp)))] } } @@ -2056,7 +2050,7 @@ fn erase_fn_common<'tcx>( .iter() .map(|p| { let is_mut_var = match p.pat.kind { - PatKind::Binding(rustc_hir::BindingAnnotation(_, mutability), _, _, _) => { + PatKind::Binding(BindingMode(_, mutability), _, _, _) => { mutability == rustc_hir::Mutability::Mut } _ => panic!("expected binding pattern"), @@ -2816,7 +2810,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( let attrs = tcx.hir().attrs(item.hir_id()); let vattrs = get_verifier_attrs(attrs, None, Some(&ctxt.cmd_line_args)) .expect("get_verifier_attrs"); - if vattrs.external || vattrs.internal_reveal_fn { + if vattrs.external || vattrs.internal_reveal_fn || vattrs.internal_const_body { continue; } let id = item.owner_id.to_def_id(); @@ -2947,6 +2941,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( origin: OpaqueTyOrigin::AsyncFn(_), in_trait: _, lifetime_mapping: _, + precise_capturing_args: None, }) => { continue; } @@ -2965,6 +2960,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( OwnerNode::Crate(_mod_) => {} OwnerNode::ImplItem(_) => {} OwnerNode::ForeignItem(_foreign_item) => {} + OwnerNode::Synthetic => {} } } } diff --git a/source/rust_verify/src/reveal_hide.rs b/source/rust_verify/src/reveal_hide.rs index 8cb38e7b7..50b85a2a4 100644 --- a/source/rust_verify/src/reveal_hide.rs +++ b/source/rust_verify/src/reveal_hide.rs @@ -72,6 +72,7 @@ pub(crate) fn handle_reveal_hide<'ctxt>( crate::hir_hide_reveal_rewrite::ResOrSymbol::Symbol(sym) => { let matching_impls: Vec<_> = tcx .inherent_impls(ty_res.def_id()) + .expect("found inherent impls") .iter() .filter_map(|impl_def_id| { let ident = rustc_span::symbol::Ident::from_str(sym.as_str()); @@ -118,8 +119,10 @@ pub(crate) fn handle_reveal_hide<'ctxt>( let rustc_ast::LitKind::Int(fuel_val, rustc_ast::LitIntType::Unsuffixed) = fuel_lit.node else { return Err(vir::messages::error(span, "Fuel must be a u32 value")); }; - let fuel_n: u32 = - fuel_val.try_into().map_err(|_| vir::messages::error(span, "Fuel must be a u32 value"))?; + let fuel_n: u32 = fuel_val + .get() + .try_into() + .map_err(|_| vir::messages::error(span, "Fuel must be a u32 value"))?; let fun = Arc::new(FunX { path }); if let Some(mk_expr) = mk_expr { diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index cce9413c9..eeae6f691 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -55,6 +55,9 @@ fn check_item<'tcx>( if vattrs.internal_reveal_fn { return Ok(()); } + if vattrs.internal_const_body { + return Ok(()); + } if vattrs.external_fn_specification && !matches!(&item.kind, ItemKind::Fn(..)) { return err_span(item.span, "`external_fn_specification` attribute not supported here"); } @@ -405,6 +408,7 @@ fn check_item<'tcx>( origin: OpaqueTyOrigin::AsyncFn(_), in_trait: _, lifetime_mapping: _, + precise_capturing_args: None, }) => { return Ok(()); } @@ -630,6 +634,7 @@ pub fn crate_to_vir<'tcx>( } }, OwnerNode::Crate(_mod_) => (), + OwnerNode::Synthetic => (), } } } diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs index 485e1147b..25b372291 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs @@ -4,11 +4,12 @@ use crate::rust_to_vir_impl::ExternalInfo; use crate::util::{err_span, unsupported_err_span}; use crate::verus_items::{self, BuiltinTypeItem, RustItem, VerusItem}; use crate::{unsupported_err, unsupported_err_unless}; -use rustc_ast::{ByRef, Mutability}; +use rustc_ast::{BindingMode, ByRef, Mutability}; use rustc_hir::definitions::DefPath; use rustc_hir::{GenericParam, GenericParamKind, Generics, HirId, LifetimeParamKind, QPath, Ty}; use rustc_infer::infer::TyCtxtInferExt; use rustc_middle::ty::fold::BoundVarReplacerDelegate; +use rustc_middle::ty::TraitPredicate; use rustc_middle::ty::Visibility; use rustc_middle::ty::{AdtDef, TyCtxt, TyKind}; use rustc_middle::ty::{Clause, ClauseKind, GenericParamDefKind}; @@ -16,7 +17,6 @@ use rustc_middle::ty::{ ConstKind, GenericArg, GenericArgKind, GenericArgsRef, ParamConst, TypeFoldable, TypeFolder, TypeSuperFoldable, TypeVisitableExt, ValTree, }; -use rustc_middle::ty::{ImplPolarity, TraitPredicate}; use rustc_span::def_id::{DefId, LOCAL_CRATE}; use rustc_span::symbol::{kw, Ident}; use rustc_span::Span; @@ -89,7 +89,8 @@ fn register_friendly_path_as_rust_name<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, p if !is_impl_item_fn { return; } - let parent_node = tcx.hir().get_parent(hir_id); + let mut parent_node = tcx.hir().parent_iter(hir_id); + let (_, parent_node) = parent_node.next().expect("unexpected empty impl path"); let friendly_self_ty = match parent_node { rustc_hir::Node::Item(rustc_hir::Item { kind: rustc_hir::ItemKind::Impl(impll), @@ -193,10 +194,10 @@ pub(crate) fn qpath_to_ident<'tcx>( qpath: &QPath<'tcx>, ) -> Option { use rustc_hir::def::Res; - use rustc_hir::{BindingAnnotation, Node, Pat, PatKind}; + use rustc_hir::{Node, Pat, PatKind}; if let QPath::Resolved(None, rustc_hir::Path { res: Res::Local(id), .. }) = qpath { if let Node::Pat(Pat { - kind: PatKind::Binding(BindingAnnotation(ByRef::No, Mutability::Not), hir_id, x, None), + kind: PatKind::Binding(BindingMode(ByRef::No, Mutability::Not), hir_id, x, None), .. }) = tcx.hir_node(*id) { @@ -507,7 +508,7 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>( args: trait_args, .. }, - polarity: ImplPolarity::Positive, + polarity: rustc_middle::ty::PredicatePolarity::Positive, }) => { if Some(trait_def_id) == tcx.lang_items().fn_trait() || Some(trait_def_id) == tcx.lang_items().fn_mut_trait() @@ -683,7 +684,7 @@ pub(crate) fn mid_ty_filter_for_external_impls<'tcx>( TyKind::Param(_) => true, TyKind::Tuple(_) => true, TyKind::Slice(_) => true, - TyKind::RawPtr(_) => true, + TyKind::RawPtr(_, _) => true, TyKind::Array(..) => true, TyKind::Closure(..) => true, TyKind::FnDef(..) => true, @@ -723,6 +724,9 @@ pub(crate) fn mid_ty_filter_for_external_impls<'tcx>( && trait_def.is_some() && t_args.len() >= 1 } + + TyKind::CoroutineClosure(_, _) => false, + TyKind::Pat(_, _) => false, } } @@ -772,7 +776,10 @@ pub(crate) fn mid_generics_filter_for_external_impls<'tcx>( for (predicate, _span) in predicates.predicates.iter() { match predicate.kind().skip_binder() { ClauseKind::RegionOutlives(_) | ClauseKind::TypeOutlives(_) => {} - ClauseKind::Trait(TraitPredicate { trait_ref, polarity: ImplPolarity::Positive }) => { + ClauseKind::Trait(TraitPredicate { + trait_ref, + polarity: rustc_middle::ty::PredicatePolarity::Positive, + }) => { let trait_def_id = trait_ref.def_id; if Some(trait_def_id) == tcx.lang_items().fn_trait() || Some(trait_def_id) == tcx.lang_items().fn_mut_trait() @@ -867,7 +874,7 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>( (Arc::new(TypX::Primitive(Primitive::Slice, typs)), false) } TyKind::Str => (Arc::new(TypX::Primitive(Primitive::StrSlice, Arc::new(vec![]))), false), - TyKind::RawPtr(rustc_middle::ty::TypeAndMut { ty, mutbl }) => { + TyKind::RawPtr(ty, mutbl) => { let typ = t_rec(ty)?.0; let typs = Arc::new(vec![typ]); @@ -1108,6 +1115,8 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>( TyKind::Placeholder(..) => unsupported_err!(span, "type inference Placeholder types"), TyKind::Infer(..) => unsupported_err!(span, "type inference Infer types"), TyKind::Error(..) => unsupported_err!(span, "type inference error types"), + TyKind::CoroutineClosure(_, _) => unsupported_err!(span, "coroutine closure types"), + TyKind::Pat(_, _) => unsupported_err!(span, "pattern types"), }; Ok(t) } @@ -1143,7 +1152,11 @@ pub(crate) fn mid_ty_const_to_vir<'tcx>( ) -> Result { let cnst_kind = match cnst.kind() { ConstKind::Unevaluated(unevaluated) => { - let valtree = cnst.eval(tcx, tcx.param_env(unevaluated.def), span); + let valtree = cnst.eval( + tcx, + tcx.param_env(unevaluated.def), + span.expect("expected span since 1.79.0"), + ); if valtree.is_err() { unsupported_err!(span.expect("span"), format!("error evaluating const")); } @@ -1383,7 +1396,10 @@ where ClauseKind::RegionOutlives(_) | ClauseKind::TypeOutlives(_) => { // can ignore lifetime bounds } - ClauseKind::Trait(TraitPredicate { trait_ref, polarity: ImplPolarity::Positive }) => { + ClauseKind::Trait(TraitPredicate { + trait_ref, + polarity: rustc_middle::ty::PredicatePolarity::Positive, + }) => { let substs = trait_ref.args; // For a bound like `T: SomeTrait`, then: @@ -1511,7 +1527,10 @@ pub(crate) fn check_item_external_generics<'tcx>( generics_params = generics_params .into_iter() .filter(|gp| { - !matches!(gp.kind, GenericParamKind::Lifetime { kind: LifetimeParamKind::Elided }) + !matches!( + gp.kind, + GenericParamKind::Lifetime { kind: LifetimeParamKind::Elided(_) } + ) }) .collect(); } diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index 3b923e70d..992d7e6c0 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -11,6 +11,7 @@ use crate::rust_to_vir_base::{ mid_ty_simplify, mid_ty_to_vir, mid_ty_to_vir_ghost, mk_range, typ_of_node, typ_of_node_expect_mut_ref, }; +use crate::rust_to_vir_func::find_body; use crate::spans::err_air_span; use crate::util::{ err_span, err_span_bare, slice_vec_map_result, unsupported_err_span, vec_map_result, @@ -22,18 +23,18 @@ use crate::verus_items::{ use crate::{fn_call_to_vir::fn_call_to_vir, unsupported_err, unsupported_err_unless}; use air::ast::Binder; use air::ast_util::str_ident; -use rustc_ast::{Attribute, BorrowKind, ByRef, LitKind, Mutability}; +use rustc_ast::{Attribute, BindingMode, BorrowKind, ByRef, LitKind, Mutability}; use rustc_hir::def::{CtorKind, CtorOf, DefKind, Res}; use rustc_hir::{ - BinOpKind, BindingAnnotation, Block, Closure, Destination, Expr, ExprKind, Guard, HirId, Let, - Local, LoopSource, Node, Pat, PatKind, QPath, Stmt, StmtKind, UnOp, + BinOpKind, Block, Closure, Destination, Expr, ExprKind, HirId, LetExpr, LetStmt, LoopSource, + Node, Pat, PatKind, QPath, Stmt, StmtKind, UnOp, }; use rustc_middle::ty::adjustment::{ Adjust, Adjustment, AutoBorrow, AutoBorrowMutability, PointerCoercion, }; use rustc_middle::ty::{ - AdtDef, ClauseKind, GenericArg, ImplPolarity, ToPredicate, TraitPredicate, TraitRef, TyCtxt, - TyKind, VariantDef, + AdtDef, ClauseKind, GenericArg, ToPredicate, TraitPredicate, TraitRef, TyCtxt, TyKind, + VariantDef, }; use rustc_span::def_id::DefId; use rustc_span::source_map::Spanned; @@ -56,7 +57,7 @@ pub(crate) fn pat_to_mut_var<'tcx>(pat: &Pat) -> Result<(bool, VarIdent), VirErr unsupported_err_unless!(default_binding_modes, *span, "default_binding_modes"); match kind { PatKind::Binding(annotation, id, ident, _subpat) => { - let BindingAnnotation(_, mutability) = annotation; + let BindingMode(_, mutability) = annotation; let mutable = match mutability { rustc_hir::Mutability::Mut => true, rustc_hir::Mutability::Not => false, @@ -209,7 +210,7 @@ pub(crate) fn expr_to_vir_inner<'tcx>( if bctx.external_body { // we want just requires/ensures, not the whole body match &expr.kind { - ExprKind::Block(..) | ExprKind::Call(..) => {} + ExprKind::Block(..) | ExprKind::Call(..) | ExprKind::Closure(_) => {} _ => { return Ok(bctx.spanned_typed_new( expr.span, @@ -471,7 +472,7 @@ pub(crate) fn pattern_to_vir_inner<'tcx>( unsupported_err_unless!(pat.default_binding_modes, pat.span, "complex pattern"); let pattern = match &pat.kind { PatKind::Wild => PatternX::Wildcard(false), - PatKind::Binding(BindingAnnotation(_, mutability), canonical, x, subpat) => { + PatKind::Binding(BindingMode(_, mutability), canonical, x, subpat) => { let mutable = match mutability { Mutability::Not => false, Mutability::Mut => true, @@ -631,6 +632,8 @@ pub(crate) fn pattern_to_vir_inner<'tcx>( PatKind::Ref(..) => unsupported_err!(pat.span, "ref patterns", pat), PatKind::Slice(..) => unsupported_err!(pat.span, "slice patterns", pat), PatKind::Never => unsupported_err!(pat.span, "never patterns", pat), + PatKind::Deref(_) => unsupported_err!(pat.span, "deref patterns", pat), + PatKind::Err(_) => unsupported_err!(pat.span, "err patterns", pat), }; let pattern = bctx.spanned_typed_new(pat.span, &pat_typ, pattern); let mut erasure_info = bctx.ctxt.erasure_info.borrow_mut(); @@ -735,7 +738,7 @@ pub(crate) fn invariant_block_open<'a>( open_stmt: &'a Stmt, ) -> Option<(HirId, HirId, &'a rustc_hir::Pat<'a>, &'a rustc_hir::Expr<'a>, InvAtomicity)> { match open_stmt.kind { - StmtKind::Local(Local { + StmtKind::Let(LetStmt { pat: Pat { kind: @@ -744,7 +747,7 @@ pub(crate) fn invariant_block_open<'a>( Pat { kind: PatKind::Binding( - BindingAnnotation(_, Mutability::Not), + BindingMode(_, Mutability::Not), guard_hir, _, None, @@ -755,7 +758,7 @@ pub(crate) fn invariant_block_open<'a>( inner_pat @ Pat { kind: PatKind::Binding( - BindingAnnotation(_, Mutability::Mut), + BindingMode(_, Mutability::Mut), inner_hir, _, None, @@ -802,7 +805,10 @@ pub(crate) fn invariant_block_open<'a>( }; Some((*guard_hir, *inner_hir, inner_pat, arg, atomicity)) } - _ => None, + _ => { + dbg!(&open_stmt); + None + } } } @@ -1155,10 +1161,7 @@ pub(crate) fn expr_to_vir_with_adjustments<'tcx>( )?; let f = match (ty1.kind(), ty2.kind()) { - ( - TyKind::RawPtr(rustc_middle::ty::TypeAndMut { ty: t1, mutbl: _ }), - TyKind::RawPtr(rustc_middle::ty::TypeAndMut { ty: t2, mutbl: _ }), - ) => { + (TyKind::RawPtr(t1, _), TyKind::RawPtr(t2, _)) => { match (t1.kind(), t2.kind()) { (TyKind::Array(el_ty1, _const_len), TyKind::Slice(el_ty2)) => { if el_ty1 == el_ty2 { @@ -1539,7 +1542,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( tcx.lang_items().fn_once_trait().unwrap(), [generic_arg0, generic_arg1], ), - polarity: ImplPolarity::Positive, + polarity: rustc_middle::ty::PredicatePolarity::Positive, })) .to_predicate(tcx); let impl_paths = get_impl_paths_for_clauses( @@ -1644,7 +1647,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( mk_expr(ExprX::Const(c)) } LitKind::Int(i, _) => { - mk_lit_int(false, i, typ_of_node(bctx, expr.span, &expr.hir_id, false)?) + mk_lit_int(false, i.get(), typ_of_node(bctx, expr.span, &expr.hir_id, false)?) } LitKind::Char(c) => { let c = vir::ast::Constant::Char(c); @@ -1730,12 +1733,13 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( UnOp::Neg => { let zero_const = vir::ast_util::const_int_from_u128(0); let zero = mk_expr(ExprX::Const(zero_const))?; - let varg = - if let ExprKind::Lit(Spanned { node: LitKind::Int(i, _), .. }) = &arg.kind { - mk_lit_int(true, *i, typ_of_node(bctx, expr.span, &expr.hir_id, false)?)? - } else { - expr_to_vir(bctx, arg, modifier)? - }; + let varg = if let ExprKind::Lit(Spanned { node: LitKind::Int(i, _), .. }) = + &arg.kind + { + mk_lit_int(true, i.get(), typ_of_node(bctx, expr.span, &expr.hir_id, false)?)? + } else { + expr_to_vir(bctx, arg, modifier)? + }; let mode_for_ghostness = if bctx.in_ghost { Mode::Spec } else { Mode::Exec }; mk_expr(ExprX::Binary( BinaryOp::Arith(ArithOp::Sub, mode_for_ghostness), @@ -1883,7 +1887,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( if bctx.in_ghost { AutospecUsage::IfMarked } else { AutospecUsage::Final }; mk_expr(ExprX::ConstVar(Arc::new(fun), autospec_usage)) } - Res::Def(DefKind::Static(Mutability::Not), id) => { + Res::Def(DefKind::Static { mutability: Mutability::Not, nested: false }, id) => { let path = def_id_to_vir_path(tcx, &bctx.ctxt.verus_items, id); let fun = FunX { path }; mk_expr(ExprX::StaticVar(Arc::new(fun))) @@ -1998,14 +2002,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( ExprKind::If(cond, lhs, rhs) => { let cond = cond.peel_drop_temps(); match cond.kind { - ExprKind::Let(Let { - hir_id: _, - pat, - init: expr, - ty: _, - span: _, - is_recovered: None, - }) => { + ExprKind::Let(LetExpr { pat, init: expr, ty: _, span: _, is_recovered: None }) => { // if let let vir_expr = expr_to_vir(bctx, expr, modifier)?; let mut vir_arms: Vec = Vec::new(); @@ -2052,8 +2049,7 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( let pattern = pattern_to_vir(bctx, &arm.pat)?; let guard = match &arm.guard { None => mk_expr(ExprX::Const(Constant::Bool(true)))?, - Some(Guard::If(guard)) => expr_to_vir(bctx, guard, modifier)?, - Some(Guard::IfLet(_)) => unsupported_err!(expr.span, "Guard IfLet"), + Some(guard_expr) => expr_to_vir(bctx, guard_expr, modifier)?, }; let body = expr_to_vir(bctx, &arm.body, modifier)?; let vir_arm = ArmX { pattern, guard, body }; @@ -2194,7 +2190,14 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( true, ) } - ExprKind::Closure(..) => closure_to_vir(bctx, expr, expr_typ()?, false, modifier), + ExprKind::Closure(Closure { fn_decl: _, body: body_id, .. }) => { + if expr_vattrs.internal_const_header_wrapper { + let closure_body = find_body(&bctx.ctxt, body_id); + expr_to_vir(bctx, closure_body.value, modifier) + } else { + closure_to_vir(bctx, expr, expr_typ()?, false, modifier) + } + } ExprKind::Index(tgt_expr, idx_expr, _span) => { // Determine if this is Index or IndexMut // Based on ./rustc_mir_build/src/thir/cx/expr.rs in rustc @@ -2401,9 +2404,11 @@ fn expr_assign_to_vir_innermost<'tcx>( panic!("assignment to non-local"); }; if not_mut { - match bctx.ctxt.tcx.hir().get_parent(*id) { + let mut parent = bctx.ctxt.tcx.hir().parent_iter(*id); + let (_, parent) = parent.next().expect("one parent for local"); + match parent { Node::Param(_) => err_span(lhs.span, "cannot assign to non-mut parameter")?, - Node::Local(_) => (), + Node::LetStmt(_) => (), other => unsupported_err!(lhs.span, "assignee node", other), } } @@ -2506,11 +2511,10 @@ fn unwrap_parameter_to_vir<'tcx>( stmt2: &Stmt<'tcx>, ) -> Result, VirErr> { // match "let x;" - let x = if let StmtKind::Local(Local { + let x = if let StmtKind::Let(LetStmt { pat: pat @ Pat { - kind: - PatKind::Binding(BindingAnnotation(ByRef::No, Mutability::Not), hir_id, x, None), + kind: PatKind::Binding(BindingMode(ByRef::No, Mutability::Not), hir_id, x, None), .. }, ty: None, @@ -2618,19 +2622,22 @@ pub(crate) fn stmt_to_vir<'tcx>( let vir_expr = expr_to_vir(bctx, expr, ExprModifier::REGULAR)?; Ok(vec![bctx.spanned_new(expr.span, StmtX::Expr(vir_expr))]) } - StmtKind::Local(Local { pat, init, .. }) => { - let_stmt_to_vir(bctx, pat, init, bctx.ctxt.tcx.hir().attrs(stmt.hir_id)) - } StmtKind::Item(item_id) => { let attrs = bctx.ctxt.tcx.hir().attrs(item_id.hir_id()); let vattrs = bctx.ctxt.get_verifier_attrs(attrs)?; if vattrs.internal_reveal_fn { dbg!(&item_id.hir_id()); unreachable!(); + } else if vattrs.internal_const_body { + dbg!(&item_id.hir_id()); + unreachable!(); } else { unsupported_err!(stmt.span, "internal item statements", stmt) } } + StmtKind::Let(LetStmt { pat, ty: _, init, els: _, hir_id: _, span: _, source: _ }) => { + let_stmt_to_vir(bctx, pat, init, bctx.ctxt.tcx.hir().attrs(stmt.hir_id)) + } } } @@ -2779,10 +2786,7 @@ fn is_ptr_cast<'tcx>( ) -> Result, VirErr> { // Mutability can always be ignored match (src.kind(), dst.kind()) { - ( - TyKind::RawPtr(rustc_middle::ty::TypeAndMut { ty: ty1, mutbl: _ }), - TyKind::RawPtr(rustc_middle::ty::TypeAndMut { ty: ty2, mutbl: _ }), - ) => { + (TyKind::RawPtr(ty1, _), TyKind::RawPtr(ty2, _)) => { if ty1 == ty2 { return Ok(Some(PtrCastKind::Trivial)); } else if ty2.is_sized(bctx.ctxt.tcx, bctx.ctxt.tcx.param_env(bctx.fun_id)) { @@ -2812,7 +2816,7 @@ fn is_ptr_cast<'tcx>( //} return Ok(None); } - (TyKind::RawPtr(rustc_middle::ty::TypeAndMut { ty: ty1, mutbl: _ }), _ty2) + (TyKind::RawPtr(ty1, _), _ty2) if crate::rust_to_vir_base::is_integer_ty(&bctx.ctxt.verus_items, &dst) => { let src_ty = mid_ty_to_vir( diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs index f54ad6ce4..cbac7e036 100644 --- a/source/rust_verify/src/rust_to_vir_func.rs +++ b/source/rust_verify/src/rust_to_vir_func.rs @@ -83,8 +83,8 @@ fn check_fn_decl<'tcx>( match implicit_self { rustc_hir::ImplicitSelfKind::None => {} rustc_hir::ImplicitSelfKind::Imm => {} - rustc_hir::ImplicitSelfKind::ImmRef => {} - rustc_hir::ImplicitSelfKind::MutRef => {} + rustc_hir::ImplicitSelfKind::RefImm => {} + rustc_hir::ImplicitSelfKind::RefMut => {} rustc_hir::ImplicitSelfKind::Mut => unsupported_err!(span, "mut self"), } match output { @@ -682,13 +682,7 @@ pub(crate) fn check_item_fn<'tcx>( match body_id { CheckItemFnEither::BodyId(body_id) => { let body = find_body(ctxt, body_id); - let Body { params, value: _, coroutine_kind } = body; - match coroutine_kind { - None => {} - _ => { - unsupported_err!(sig.span, "coroutine_kind", coroutine_kind); - } - } + let Body { params, value: _ } = body; let mut ps = Vec::new(); for Param { hir_id, pat, ty_span: _, span } in params.iter() { let (is_mut_var, name) = pat_to_mut_var(pat)?; @@ -1653,7 +1647,27 @@ pub(crate) fn check_item_const_or_static<'tcx>( let fuel = get_fuel(&vattrs); let body = find_body(ctxt, body_id); - let mut vir_body = body_to_vir(ctxt, id, body_id, body, body_mode, vattrs.external_body)?; + let (actual_body_id, actual_body) = if let ExprKind::Block(block, _) = body.value.kind { + let first_stmt = block.stmts.iter().next(); + if let Some(rustc_hir::StmtKind::Item(item)) = first_stmt.map(|stmt| &stmt.kind) { + let attrs = ctxt.tcx.hir().attrs(item.hir_id()); + let vattrs = ctxt.get_verifier_attrs(attrs)?; + if vattrs.internal_const_body { + let body_id = ctxt.tcx.hir().body_owned_by(item.owner_id.def_id); + let body = find_body(ctxt, &body_id); + Some((body_id, body)) + } else { + None + } + } else { + None + } + } else { + None + } + .unwrap_or((*body_id, body)); + let mut vir_body = + body_to_vir(ctxt, id, &actual_body_id, actual_body, body_mode, vattrs.external_body)?; let header = vir::headers::read_header(&mut vir_body)?; if header.require.len() + header.recommend.len() > 0 { return err_span(span, "consts cannot have requires/recommends"); diff --git a/source/rust_verify/src/rust_to_vir_global.rs b/source/rust_verify/src/rust_to_vir_global.rs index 26c40f398..2a7e532ae 100644 --- a/source/rust_verify/src/rust_to_vir_global.rs +++ b/source/rust_verify/src/rust_to_vir_global.rs @@ -81,6 +81,7 @@ pub(crate) fn process_const_early<'tcx>( let rustc_ast::LitKind::Int(size, rustc_ast::LitIntType::Unsuffixed) = lit.node else { return err; }; + let size = size.get(); vir::layout::layout_of_typ_supported(&ty, &crate::spans::err_air_span(item.span))?; diff --git a/source/rust_verify/src/rust_to_vir_impl.rs b/source/rust_verify/src/rust_to_vir_impl.rs index d37dc39ff..8dd136755 100644 --- a/source/rust_verify/src/rust_to_vir_impl.rs +++ b/source/rust_verify/src/rust_to_vir_impl.rs @@ -288,12 +288,8 @@ pub(crate) fn translate_impl<'tcx>( ty ); true - } else if let Some( - RustItem::StructuralEq - | RustItem::StructuralPartialEq - | RustItem::PartialEq - | RustItem::Eq, - ) = rust_item + } else if let Some(RustItem::StructuralPartialEq | RustItem::PartialEq | RustItem::Eq) = + rust_item { // TODO SOUNDNESS additional checks of the implementation true diff --git a/source/rust_verify/src/rust_to_vir_trait.rs b/source/rust_verify/src/rust_to_vir_trait.rs index 552208250..fb4561efb 100644 --- a/source/rust_verify/src/rust_to_vir_trait.rs +++ b/source/rust_verify/src/rust_to_vir_trait.rs @@ -8,7 +8,7 @@ use crate::rust_to_vir_impl::ExternalInfo; use crate::unsupported_err_unless; use crate::util::{err_span, err_span_bare}; use rustc_hir::{Generics, TraitFn, TraitItem, TraitItemKind, TraitItemRef}; -use rustc_middle::ty::{ClauseKind, ImplPolarity, TraitPredicate, TraitRef, TyCtxt}; +use rustc_middle::ty::{ClauseKind, TraitPredicate, TraitRef, TyCtxt}; use rustc_span::def_id::DefId; use rustc_span::Span; use std::sync::Arc; @@ -37,7 +37,7 @@ pub(crate) fn external_trait_specification_of<'tcx>( match bound.kind().skip_binder() { ClauseKind::Trait(TraitPredicate { trait_ref, - polarity: ImplPolarity::Positive, + polarity: rustc_middle::ty::PredicatePolarity::Positive, }) => { let trait_def_id = trait_ref.def_id; if Some(trait_def_id) == tcx.lang_items().sized_trait() { @@ -310,14 +310,48 @@ pub(crate) fn translate_trait<'tcx>( // crate::rust_to_vir_func::predicates_match(tcx, true, &preds1.iter().collect(), &preds2.iter().collect())?; // (would need to fix up the TyKind::Alias projections inside the clauses) + let mut preds1 = preds1.to_vec(); + let mut preds2 = preds2.to_vec(); + preds1.sort_by(|a, b| a.to_string().cmp(&b.to_string())); + preds2.sort_by(|a, b| a.to_string().cmp(&b.to_string())); + if preds1.len() != preds2.len() { - return err_span( - trait_span, - format!( - "Mismatched bounds on associated type\n{:?}\n vs.\n{:?}", - preds1, preds2 - ), + let mut t = format!( + "Mismatched bounds on associated type ({} != {})\n", + preds1.len(), + preds2.len(), ); + t.push_str("Target:\n"); + for p1 in preds1.iter() { + t.push_str(&format!(" - {}\n", p1)); + } + t.push_str("External specification:\n"); + for p2 in preds2.iter() { + t.push_str(&format!(" - {}\n", p2)); + } + return err_span(trait_span, t); + } + + for (p1, p2) in preds1.iter().zip(preds2.iter()) { + match (p1.kind().skip_binder(), p2.kind().skip_binder()) { + (ClauseKind::Trait(p1), ClauseKind::Trait(p2)) => { + if p1.def_id() != p2.def_id() { + return err_span( + trait_span, + format!( + "Mismatched bounds on associated type ({} != {})", + p1, p2 + ), + ); + } + } + _ => { + return err_span( + trait_span, + "Verus does not yet support this bound on external specs", + ); + } + } } } } diff --git a/source/rust_verify/src/util.rs b/source/rust_verify/src/util.rs index 036c584de..a908fc719 100644 --- a/source/rust_verify/src/util.rs +++ b/source/rust_verify/src/util.rs @@ -229,8 +229,10 @@ pub fn hir_prim_ty_to_mir_ty<'tcx>( rustc_ast::UintTy::U128 => tcx.types.u128, }, rustc_hir::PrimTy::Float(float_ty) => match float_ty { + rustc_ast::FloatTy::F16 => tcx.types.f16, rustc_ast::FloatTy::F32 => tcx.types.f32, rustc_ast::FloatTy::F64 => tcx.types.f64, + rustc_ast::FloatTy::F128 => tcx.types.f128, }, rustc_hir::PrimTy::Str => tcx.types.str_, rustc_hir::PrimTy::Bool => tcx.types.bool, diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index c95c6fec7..0ce991bd8 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -11,7 +11,7 @@ use air::ast::{Command, CommandX, Commands}; use air::context::{QueryContext, SmtSolver, ValidityResult}; use air::messages::{ArcDynMessage, Diagnostics as _}; use air::profiler::Profiler; -use rustc_errors::{DiagnosticBuilder, EmissionGuarantee}; +use rustc_errors::{Diag, EmissionGuarantee}; use rustc_hir::OwnerNode; use rustc_interface::interface::Compiler; use rustc_session::config::ErrorOutputType; @@ -99,7 +99,7 @@ impl air::messages::Diagnostics for Reporter<'_> { } fn emit_with_diagnostic_details<'a, G: EmissionGuarantee>( - mut diag: DiagnosticBuilder<'a, G>, + mut diag: Diag<'a, G>, multispan: MultiSpan, help: &Option, ) { @@ -2519,11 +2519,9 @@ impl Verifier { ) -> Result)> { let time_hir0 = Instant::now(); - match rustc_hir_analysis::check_crate(tcx) { - Ok(()) => {} - Err(_) => { - return Ok(false); - } + rustc_hir_analysis::check_crate(tcx); + if tcx.dcx().err_count() != 0 { + return Ok(false); } let hir = tcx.hir(); @@ -2785,6 +2783,24 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro { fn config(&mut self, config: &mut rustc_interface::interface::Config) { config.override_queries = Some(|_session, providers| { providers.hir_crate = hir_crate; + + // Do not actually evaluate consts if we are not compiling, as doing so triggers the + // constness checker, which is more restrictive than necessary for verification. + // Doing this will delay some const-ness errors to when verus is run with `--compile`. + providers.eval_to_const_value_raw = + |_tcx, _key| Ok(rustc_middle::mir::ConstValue::ZeroSized); + + // Prevent the borrow checker from running, as we will run our own lifetime analysis. + // Stopping after `after_expansion` used to be enough, but now borrow check is triggered + // by const evaluation through the mir interpreter. + providers.mir_borrowck = |tcx, _local_def_id| { + tcx.arena.alloc(rustc_middle::mir::BorrowCheckResult { + concrete_opaque_types: rustc_data_structures::fx::FxIndexMap::default(), + closure_requirements: None, + used_mut_upvars: smallvec::SmallVec::new(), + tainted_by_errors: None, + }) + }; }); } @@ -2795,7 +2811,7 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro { ) -> rustc_driver::Compilation { self.rust_end_time = Some(Instant::now()); - if !compiler.sess.compile_status().is_ok() { + if let Some(_guar) = compiler.sess.dcx().has_errors() { return rustc_driver::Compilation::Stop; } @@ -2860,7 +2876,7 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro { } return; } - if !compiler.sess.compile_status().is_ok() { + if let Some(_guar) = compiler.sess.dcx().has_errors() { return; } self.lifetime_start_time = Some(Instant::now()); @@ -2930,7 +2946,7 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro { } } - if !compiler.sess.compile_status().is_ok() { + if let Some(_guar) = compiler.sess.dcx().has_errors() { return; } diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index 248031f1b..b4ae97d41 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -15,13 +15,13 @@ fn ty_to_stable_string_partial<'tcx>( TyKind::Int(t) => format!("{}", t.name_str()), TyKind::Uint(t) => format!("{}", t.name_str()), TyKind::Float(t) => format!("{}", t.name_str()), - TyKind::RawPtr(ref tm) => format!( + TyKind::RawPtr(ref ty, ref tm) => format!( "*{} {}", - match tm.mutbl { + match tm { rustc_ast::Mutability::Mut => "mut", rustc_ast::Mutability::Not => "const", }, - ty_to_stable_string_partial(tcx, &tm.ty)?, + ty_to_stable_string_partial(tcx, ty)?, ), TyKind::Ref(_r, ty, mutbl) => format!( "&{} {}", @@ -579,7 +579,6 @@ pub(crate) enum RustItem { Sized, Copy, Clone, - StructuralEq, StructuralPartialEq, Eq, PartialEq, @@ -621,9 +620,6 @@ pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option test_body( &ATOMIC_U32.replace("u32", "usize").replace("PAtomicU32", "PAtomicUsize"), false, Some(4)) => Ok(()) } -test_verify_one_file! { - #[test] test_atomic_usize_32_fail test_body( +test_verify_one_file_with_options! { + #[test] test_atomic_usize_32_fail ["--no-lifetime"] => test_body( &ATOMIC_U32.replace("u32", "usize").replace("PAtomicU32", "PAtomicUsize"), true, Some(4)) => Err(e) => assert_one_fails(e) } - -test_verify_one_file! { - #[test] test_atomic_isize_32_pass test_body( +test_verify_one_file_with_options! { + #[test] test_atomic_isize_32_pass ["--no-lifetime"] => test_body( &ATOMIC_I32.replace("i32", "isize").replace("PAtomicI32", "PAtomicIsize"), false, Some(4)) => Ok(()) } -test_verify_one_file! { - #[test] test_atomic_isize_32_fail test_body( +test_verify_one_file_with_options! { + #[test] test_atomic_isize_32_fail ["--no-lifetime"] => test_body( &ATOMIC_I32.replace("i32", "isize").replace("PAtomicI32", "PAtomicIsize"), true, Some(4)) => Err(e) => assert_one_fails(e) diff --git a/source/rust_verify_test/tests/common/mod.rs b/source/rust_verify_test/tests/common/mod.rs index 698697fea..03f824dfd 100644 --- a/source/rust_verify_test/tests/common/mod.rs +++ b/source/rust_verify_test/tests/common/mod.rs @@ -1,3 +1,5 @@ +#![allow(dead_code)] + extern crate rustc_driver; extern crate rustc_errors; extern crate rustc_span; diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs index 2bb6cdb9e..ca53f7d3c 100644 --- a/source/rust_verify_test/tests/consts.rs +++ b/source/rust_verify_test/tests/consts.rs @@ -8,7 +8,7 @@ test_verify_one_file! { spec fn f() -> int { 1 } const C: u64 = 3 + 5; spec const S: int = C as int + f(); - fn e() -> (u: u64) ensures u == 1 { 1 } + const fn e() -> (u: u64) ensures u == 1 { 1 } exec const E: u64 ensures E == 2 { 1 + e() } fn test1() { @@ -58,14 +58,14 @@ test_verify_one_file! { test_verify_one_file! { #[test] test1_fails5 verus_code! { - fn f() -> u64 { 1 } + const fn f() -> u64 { 1 } const S: u64 = 1 + f(); } => Err(err) => assert_vir_error_msg(err, "cannot call function `crate::f` with mode exec") } test_verify_one_file! { #[test] test1_fails6 verus_code! { - fn e() -> (u: u64) ensures u >= 1 { 1 } + const fn e() -> (u: u64) ensures u >= 1 { 1 } exec const E: u64 = 1 + e(); // FAILS } => Err(e) => assert_vir_error_msg(e, "possible arithmetic underflow/overflow") } @@ -226,7 +226,7 @@ test_verify_one_file! { proof { let x = E; } 0 } - } => Err(e) => assert_vir_error_msg(e, "cannot read static with mode exec") + } => Err(err) => assert_rust_error_msg(err, "cycle detected when evaluating initializer of static `E`") } test_verify_one_file! { @@ -239,7 +239,7 @@ test_verify_one_file! { proof { let x = E; } 0 } - } => Err(e) => assert_vir_error_msg(e, "cannot read const with mode exec") + } => Err(err) => assert_vir_error_msg(err, "cannot read const with mode exec") } test_verify_one_file! { @@ -341,3 +341,14 @@ test_verify_one_file! { } } => Err(err) => assert_one_fails(err) } + +test_verify_one_file! { + #[test] exec_const_body_with_proof verus_code! { + spec fn f() -> int { 1 } + const fn e() -> (u: u64) ensures u == 1 { 1 } + exec const E: u64 ensures E == 2 { + assert(f() == 1); + 1 + e() + } + } => Ok(()) +} diff --git a/source/rust_verify_test/tests/lifetime.rs b/source/rust_verify_test/tests/lifetime.rs index f2d19c406..ce456f6a3 100644 --- a/source/rust_verify_test/tests/lifetime.rs +++ b/source/rust_verify_test/tests/lifetime.rs @@ -758,7 +758,7 @@ test_verify_one_file! { _ => { } } } - } => Err(err) => assert_vir_error_msg(err, "use of moved value") + } => Err(err) => assert_vir_error_msg(err, "use of partially moved value") } test_verify_one_file! { diff --git a/source/vir/src/ast_visitor.rs b/source/vir/src/ast_visitor.rs index 57f1d10da..b95ac6304 100644 --- a/source/vir/src/ast_visitor.rs +++ b/source/vir/src/ast_visitor.rs @@ -13,6 +13,7 @@ use air::scope_map::ScopeMap; use std::sync::Arc; pub struct ScopeEntry { + #[allow(dead_code)] pub typ: Typ, pub is_mut: bool, pub init: bool, diff --git a/source/vir/src/expand_errors.rs b/source/vir/src/expand_errors.rs index f990a620b..adcf38491 100644 --- a/source/vir/src/expand_errors.rs +++ b/source/vir/src/expand_errors.rs @@ -1017,6 +1017,7 @@ fn split_precondition(ctx: &Ctx, span: &Span, name: &Fun, typs: &Typs, args: &Ex exps } +#[allow(dead_code)] struct DiagnosticsVoid {} impl air::messages::Diagnostics for DiagnosticsVoid { fn report_as(&self, _msg: &air::messages::ArcDynMessage, _level: air::messages::MessageLevel) {} diff --git a/source/vir/src/headers.rs b/source/vir/src/headers.rs index 3a09f9ff5..3ea25332c 100644 --- a/source/vir/src/headers.rs +++ b/source/vir/src/headers.rs @@ -227,10 +227,70 @@ pub fn read_header_block(block: &mut Vec) -> Result { } pub fn read_header(body: &mut Expr) -> Result { + #[derive(Clone, Copy)] + enum NestedHeaderBlock { + No, + Yes, + Unknown, + Conflict, + } + + impl NestedHeaderBlock { + fn join(&mut self, other: NestedHeaderBlock) { + match (*self, other) { + (NestedHeaderBlock::No, NestedHeaderBlock::No) => {} + (NestedHeaderBlock::Yes, NestedHeaderBlock::Yes) => {} + (_, NestedHeaderBlock::Unknown) => panic!("unexpected join with unknown"), + (NestedHeaderBlock::Unknown, _) => *self = other, + _ => *self = NestedHeaderBlock::Conflict, + } + } + } + match &body.x { ExprX::Block(stmts, expr) => { let mut expr = expr.clone(); - let mut block: Vec = (**stmts).clone(); + let mut block = Vec::new(); + for stmt in (**stmts).iter() { + let mut nested_header_block = NestedHeaderBlock::Unknown; + if let StmtX::Expr(e) = &stmt.x { + if let ExprX::Block(b, e) = &e.x { + for s in b.iter() { + if let StmtX::Expr(e) = &s.x { + if let ExprX::Header(_h) = &e.x { + block.push(s.clone()); + nested_header_block = NestedHeaderBlock::Yes; + } else { + nested_header_block.join(NestedHeaderBlock::No); + } + } else { + nested_header_block.join(NestedHeaderBlock::No); + } + } + if let Some(e) = &e { + if let ExprX::Header(_h) = &e.x { + nested_header_block = NestedHeaderBlock::Conflict; + } + } + } else { + nested_header_block.join(NestedHeaderBlock::No); + } + } else { + nested_header_block.join(NestedHeaderBlock::No); + } + match nested_header_block { + NestedHeaderBlock::No | NestedHeaderBlock::Unknown => { + block.push(stmt.clone()); + } + NestedHeaderBlock::Yes => {} + NestedHeaderBlock::Conflict => { + return Err(error( + &stmt.span, + "internal error: invalid nested header block", + )); + } + } + } let mut header = read_header_block(&mut block)?; if let Some(e) = &expr { if let ExprX::Header(h) = &e.x { diff --git a/source/vir/src/interpreter.rs b/source/vir/src/interpreter.rs index d0bf0441f..c2b598895 100644 --- a/source/vir/src/interpreter.rs +++ b/source/vir/src/interpreter.rs @@ -188,6 +188,7 @@ trait SyntacticEquality { fn definitely_eq(&self, other: &Self) -> bool { matches!(self.syntactic_eq(other), Some(true)) } + #[allow(dead_code)] fn definitely_ne(&self, other: &Self) -> bool { matches!(self.syntactic_eq(other), Some(false)) } diff --git a/source/vir/src/visitor.rs b/source/vir/src/visitor.rs index 657a33965..b6988e9bb 100644 --- a/source/vir/src/visitor.rs +++ b/source/vir/src/visitor.rs @@ -5,6 +5,7 @@ pub(crate) trait Returner { type Vec; type Opt; fn get(r: Self::Ret) -> A; + #[allow(dead_code)] fn get_vec(r: Self::Vec) -> Vec; fn get_vec_a(r: Self::Vec) -> Arc>; fn get_vec_or<'a, A>(r: &'a Self::Vec, or: &'a Vec) -> &'a Vec; diff --git a/source/vstd/atomic_ghost.rs b/source/vstd/atomic_ghost.rs index 6fab5d01b..21a427b8e 100644 --- a/source/vstd/atomic_ghost.rs +++ b/source/vstd/atomic_ghost.rs @@ -70,6 +70,8 @@ macro_rules! declare_atomic_type { let (patomic, Tracked(perm)) = $patomic_ty::new(u); let tracked pair = (perm, g); + assert(Pred::atomic_inv(k, u, g)); + assert(perm.view().patomic == patomic.id()); let tracked atomic_inv = AtomicInvariant::new( (k, patomic.id()), pair, 0); diff --git a/source/vstd/std_specs/core.rs b/source/vstd/std_specs/core.rs index df5f704c1..82ed86265 100644 --- a/source/vstd/std_specs/core.rs +++ b/source/vstd/std_specs/core.rs @@ -17,6 +17,11 @@ pub trait ExAllocator { type ExternalTraitSpecificationFor: core::alloc::Allocator; } +#[verifier::external_trait_specification] +pub trait ExFreeze { + type ExternalTraitSpecificationFor: core::marker::Freeze; +} + #[verifier::external_trait_specification] pub trait ExDebug { type ExternalTraitSpecificationFor: core::fmt::Debug; @@ -56,7 +61,8 @@ pub trait ExHash { pub trait ExPtrPointee { type ExternalTraitSpecificationFor: core::ptr::Pointee; - type Metadata: Copy + Send + Sync + Ord + core::hash::Hash + Unpin; + type Metadata: + Copy + Send + Sync + Ord + core::hash::Hash + Unpin + core::fmt::Debug + Sized + core::marker::Freeze; } #[verifier::external_trait_specification] diff --git a/source/vstd/vstd.rs b/source/vstd/vstd.rs index aece78000..d6f32be30 100644 --- a/source/vstd/vstd.rs +++ b/source/vstd/vstd.rs @@ -14,6 +14,7 @@ #![cfg_attr(verus_keep_ghost, feature(ptr_metadata))] #![cfg_attr(verus_keep_ghost, feature(strict_provenance))] #![cfg_attr(verus_keep_ghost, feature(strict_provenance_atomic_ptr))] +#![cfg_attr(verus_keep_ghost, feature(freeze))] #[cfg(feature = "alloc")] extern crate alloc;