From 8071961895ea47d77e81fd1e0a9c4b56c70e0918 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Fri, 21 Jun 2024 17:40:17 +0200 Subject: [PATCH 1/7] port to rust 1.79.0 --- rust-toolchain.toml | 4 +- source/builtin/src/lib.rs | 48 +++--- source/builtin_macros/src/syntax.rs | 137 ++++++++++++------ source/lifetime_generate_works.txt | 1 + source/rust_verify/src/attributes.rs | 16 ++ .../src/hir_hide_reveal_rewrite.rs | 1 - source/rust_verify/src/lifetime_generate.rs | 62 ++++---- source/rust_verify/src/reveal_hide.rs | 7 +- source/rust_verify/src/rust_to_vir.rs | 10 +- source/rust_verify/src/rust_to_vir_base.rs | 38 +++-- source/rust_verify/src/rust_to_vir_expr.rs | 100 +++++++------ source/rust_verify/src/rust_to_vir_func.rs | 34 +++-- source/rust_verify/src/rust_to_vir_global.rs | 1 + source/rust_verify/src/rust_to_vir_trait.rs | 50 ++++++- source/rust_verify/src/util.rs | 2 + source/rust_verify/src/verifier.rs | 44 ++++-- source/rust_verify/src/verus_items.rs | 10 +- source/rust_verify_test/tests/common/mod.rs | 2 + source/rust_verify_test/tests/consts.rs | 14 +- source/rust_verify_test/tests/lifetime.rs | 2 +- source/rust_verify_test/tests/overflow.rs | 2 +- .../rust_verify_test_macros/src/rust_code.rs | 27 ++-- source/state_machines_macros/src/ast.rs | 1 + source/vir/src/ast_visitor.rs | 1 + source/vir/src/headers.rs | 62 +++++++- source/vir/src/interpreter.rs | 1 + source/vir/src/visitor.rs | 1 + source/vstd/Cargo.lock | 97 +++++++++++++ source/vstd/atomic_ghost.rs | 2 + source/vstd/cell.rs | 2 +- source/vstd/pcm_lib.rs | 2 +- source/vstd/std_specs/core.rs | 3 +- source/vstd/std_specs/range.rs | 1 - source/vstd/storage_protocol.rs | 2 +- source/vstd/vstd.rs | 1 + 35 files changed, 560 insertions(+), 228 deletions(-) create mode 100644 source/lifetime_generate_works.txt create mode 100644 source/vstd/Cargo.lock diff --git a/rust-toolchain.toml b/rust-toolchain.toml index ff2b9dc75e..55247438b7 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 550c176393..3347da20c7 100644 --- a/source/builtin/src/lib.rs +++ b/source/builtin/src/lib.rs @@ -145,9 +145,7 @@ pub fn opens_invariants_except(_a: A) { #[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"] @@ -348,14 +346,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 } } @@ -382,7 +381,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 @@ -391,7 +393,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) + } } } @@ -400,14 +405,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 } } @@ -430,8 +436,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 @@ -441,7 +447,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 @@ -451,7 +460,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) + } } } @@ -478,14 +490,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() } @@ -1427,9 +1441,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/syntax.rs b/source/builtin_macros/src/syntax.rs index 908fb45763..ed7148ed10 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -376,13 +376,15 @@ impl Visitor { let ensures = self.take_ghost(&mut sig.ensures); let decreases = self.take_ghost(&mut sig.decreases); let opens_invariants = self.take_ghost(&mut sig.invariants); + + 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])), ), @@ -395,13 +397,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)), ), @@ -425,7 +427,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]); @@ -458,14 +460,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])), ), @@ -483,7 +485,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( @@ -494,7 +496,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)), ), @@ -502,7 +504,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)), ), @@ -513,7 +515,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()), ), @@ -521,7 +523,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()), ), @@ -532,7 +534,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])), ), @@ -541,6 +543,13 @@ 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); + } + } self.inside_ghost -= 1; self.inside_bitvector = false; @@ -561,41 +570,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] }); } } @@ -606,7 +635,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 })); } @@ -640,10 +669,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 } } @@ -989,16 +1020,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! {} @@ -2921,7 +2960,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), @@ -2929,18 +2968,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), @@ -2948,11 +2989,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 0000000000..6ed22c96fd --- /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 fe7e2ad104..d11c7fbd39 100644 --- a/source/rust_verify/src/attributes.rs +++ b/source/rust_verify/src/attributes.rs @@ -295,6 +295,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 @@ -611,6 +615,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) } @@ -826,6 +836,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, @@ -930,6 +942,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, @@ -994,6 +1008,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 ea22c7a62a..d0f397ea57 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_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 2a6119a225..25d835b7ee 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, @@ -458,7 +458,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)) } @@ -626,7 +626,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)) } } @@ -635,7 +635,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))) } @@ -1050,7 +1050,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)); @@ -1067,8 +1067,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) @@ -1119,7 +1118,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))) } _ => { @@ -1154,6 +1153,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 { @@ -1205,7 +1207,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 { @@ -1474,7 +1476,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]) @@ -1538,12 +1540,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; @@ -1561,7 +1558,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); @@ -1612,10 +1609,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 { @@ -1625,13 +1622,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)))] } } @@ -1991,7 +1985,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"), @@ -2739,7 +2733,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(); @@ -2870,6 +2864,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( origin: OpaqueTyOrigin::AsyncFn(_), in_trait: _, lifetime_mapping: _, + precise_capturing_args: None, }) => { continue; } @@ -2888,6 +2883,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 8cb38e7b7a..50b85a2a49 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 c086f23954..4c7aabd728 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -77,6 +77,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"); } @@ -433,10 +436,7 @@ fn check_item<'tcx>( ); true } else if let Some( - RustItem::StructuralEq - | RustItem::StructuralPartialEq - | RustItem::PartialEq - | RustItem::Eq, + RustItem::StructuralPartialEq | RustItem::PartialEq | RustItem::Eq, ) = rust_item { // TODO SOUNDNESS additional checks of the implementation @@ -731,6 +731,7 @@ fn check_item<'tcx>( origin: OpaqueTyOrigin::AsyncFn(_), in_trait: _, lifetime_mapping: _, + precise_capturing_args: None, }) => { return Ok(()); } @@ -1134,6 +1135,7 @@ pub fn crate_to_vir<'tcx>(ctxt: &mut Context<'tcx>) -> Result<(Krate, ItemToModu } }, 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 d1b74b6a4c..04cc01d497 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::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, Generics, HirId, 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, 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) { @@ -503,7 +504,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() @@ -667,7 +668,7 @@ pub(crate) fn mid_ty_filter_for_external_impls<'tcx>( TyKind::Never => true, TyKind::Tuple(_) => true, TyKind::Slice(_) => true, - TyKind::RawPtr(_) => true, + TyKind::RawPtr(_, _) => true, TyKind::Array(..) => true, TyKind::Closure(..) => true, TyKind::FnDef(..) => true, @@ -701,6 +702,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, }; all_types_supported = all_types_supported && supported; } @@ -738,7 +742,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() @@ -833,7 +840,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]); @@ -1068,6 +1075,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) } @@ -1103,7 +1112,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")); } @@ -1327,7 +1340,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: diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index d4b22f98ae..453c19803c 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -10,6 +10,7 @@ use crate::rust_to_vir_base::{ is_smt_arith, is_smt_equality, local_to_var, 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, @@ -21,18 +22,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::{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; @@ -54,7 +55,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, @@ -207,7 +208,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, @@ -448,7 +449,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, @@ -604,6 +605,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(); @@ -708,7 +711,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: @@ -717,7 +720,7 @@ pub(crate) fn invariant_block_open<'a>( Pat { kind: PatKind::Binding( - BindingAnnotation(_, Mutability::Not), + BindingMode(_, Mutability::Not), guard_hir, _, None, @@ -728,7 +731,7 @@ pub(crate) fn invariant_block_open<'a>( inner_pat @ Pat { kind: PatKind::Binding( - BindingAnnotation(_, Mutability::Mut), + BindingMode(_, Mutability::Mut), inner_hir, _, None, @@ -775,7 +778,10 @@ pub(crate) fn invariant_block_open<'a>( }; Some((*guard_hir, *inner_hir, inner_pat, arg, atomicity)) } - _ => None, + _ => { + dbg!(&open_stmt); + None + } } } @@ -1126,10 +1132,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 { @@ -1495,7 +1498,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( @@ -1600,7 +1603,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); @@ -1692,12 +1695,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), @@ -1807,7 +1811,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))) @@ -1923,14 +1927,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(); @@ -1977,8 +1974,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 }; @@ -2119,7 +2115,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 @@ -2309,9 +2312,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), } } @@ -2394,11 +2399,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, @@ -2506,19 +2510,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)) + } } } @@ -2667,10 +2674,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)) { diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs index 91b629baf1..772dfb81de 100644 --- a/source/rust_verify/src/rust_to_vir_func.rs +++ b/source/rust_verify/src/rust_to_vir_func.rs @@ -82,8 +82,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 { @@ -675,13 +675,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)?; @@ -1545,7 +1539,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 26c40f3981..2a7e532aee 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_trait.rs b/source/rust_verify/src/rust_to_vir_trait.rs index a59adc90ff..3266698e51 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_func::{check_item_fn, CheckItemFnEither}; 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() { @@ -306,14 +306,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 036c584dea..a908fc719a 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 0743271305..a9eb076c14 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, 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, ) { @@ -2448,11 +2448,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(); @@ -2710,6 +2708,32 @@ 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; + + // providers.eval_static_initializer = |tcx, key| { + // eprintln!("static init start {:?}", &key); + // let r = (DEFAULT_QUERY_PROVIDERS.eval_static_initializer)(tcx, key); + // eprintln!("static init end {:?}", &key); + // r + // }; + // + // providers.eval_to_const_value_raw = |tcx, key| { + // eprintln!("eval start {:?}", &key); + // let r = (DEFAULT_QUERY_PROVIDERS.eval_to_const_value_raw)(tcx, key); + // eprintln!("eval end {:?}", &key); + // r + // }; + + // 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, + }) + }; }); } @@ -2720,7 +2744,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; } @@ -2785,7 +2809,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()); @@ -2854,7 +2878,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 a837594120..4267bc68c9 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!( "&{} {}", @@ -565,7 +565,6 @@ pub(crate) enum RustItem { FnOnce, FnMut, Drop, - StructuralEq, StructuralPartialEq, Eq, PartialEq, @@ -606,9 +605,6 @@ pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option 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() { @@ -39,7 +39,7 @@ test_verify_one_file! { #[test] test1_fails2 verus_code! { const C: u64 = S; const S: u64 = C; - } => Err(err) => assert_vir_error_msg(err, "recursive function must have a decreases clause") + } => Err(err) => assert_rust_error_msg(err, "cycle detected when simplifying constant for the type system") } test_verify_one_file! { @@ -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 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") } @@ -186,7 +186,7 @@ test_verify_one_file! { exec static E: u64 = 0; const s: u64 = E; - } => Err(e) => assert_vir_error_msg(e, "cannot read static with mode exec") + } => Err(e) => assert_rust_error_msg(e, "referencing statics in constants is unstable") } test_verify_one_file! { @@ -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(e) => assert_rust_error_msg(e, "cycle detected when evaluating initializer of static") } 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(e) => assert_rust_error_msg(e, "cycle detected when simplifying constant for the type system") } test_verify_one_file! { diff --git a/source/rust_verify_test/tests/lifetime.rs b/source/rust_verify_test/tests/lifetime.rs index aa0727fc3d..c04abc4267 100644 --- a/source/rust_verify_test/tests/lifetime.rs +++ b/source/rust_verify_test/tests/lifetime.rs @@ -754,5 +754,5 @@ 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") } diff --git a/source/rust_verify_test/tests/overflow.rs b/source/rust_verify_test/tests/overflow.rs index 32f55c5d23..c8fae6b12e 100644 --- a/source/rust_verify_test/tests/overflow.rs +++ b/source/rust_verify_test/tests/overflow.rs @@ -94,7 +94,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_literal_out_of_range verus_code! { const C: u8 = 256 - 1; - } => Err(err) => assert_vir_error_msg(err, "integer literal out of range") + } => Err(err) => assert_rust_error_msg(err, "evaluation of constant value failed") } test_verify_one_file! { diff --git a/source/rust_verify_test_macros/src/rust_code.rs b/source/rust_verify_test_macros/src/rust_code.rs index 14febb3192..6f5719ea55 100644 --- a/source/rust_verify_test_macros/src/rust_code.rs +++ b/source/rust_verify_test_macros/src/rust_code.rs @@ -9,18 +9,21 @@ pub(crate) fn rust_code_core(input: TokenStream) -> String { span = span.join(token.span()).unwrap(); } - let src = span.source_text().unwrap(); - let n = span.start().column() - 1; - let original_src = src; - let mut src = String::new(); - let mut lines = original_src.lines(); - src += lines.next().unwrap(); - src += "\n"; - for line in lines { - let (indent, line) = line.split_at(n.min(line.len())); - assert!(!indent.contains(|c| c != ' '), "Invalid indentation"); - src += line; + if let Some(src) = span.source_text() { + let n = span.start().column() - 1; + let original_src = src; + let mut src = String::new(); + let mut lines = original_src.lines(); + src += lines.next().unwrap(); src += "\n"; + for line in lines { + let (indent, line) = line.split_at(n.min(line.len())); + assert!(!indent.contains(|c| c != ' '), "Invalid indentation"); + src += line; + src += "\n"; + } + src + } else { + "panic!(\"source_text() returned None\")".to_string() } - src } diff --git a/source/state_machines_macros/src/ast.rs b/source/state_machines_macros/src/ast.rs index 16ff45b310..78aa6a8b65 100644 --- a/source/state_machines_macros/src/ast.rs +++ b/source/state_machines_macros/src/ast.rs @@ -217,6 +217,7 @@ pub struct Arm { pub pat: Pat, pub guard: Option<(token::If, Box)>, pub fat_arrow_token: token::FatArrow, + #[allow(dead_code)] pub comma: Option, } diff --git a/source/vir/src/ast_visitor.rs b/source/vir/src/ast_visitor.rs index bc947cfaa9..14f0219da8 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/headers.rs b/source/vir/src/headers.rs index 559046e934..a159724786 100644 --- a/source/vir/src/headers.rs +++ b/source/vir/src/headers.rs @@ -200,10 +200,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 f77ddf6518..b7a6d0bd5b 100644 --- a/source/vir/src/interpreter.rs +++ b/source/vir/src/interpreter.rs @@ -185,6 +185,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 657a33965c..b6988e9bb7 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/Cargo.lock b/source/vstd/Cargo.lock new file mode 100644 index 0000000000..12842c8de5 --- /dev/null +++ b/source/vstd/Cargo.lock @@ -0,0 +1,97 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "builtin" +version = "0.1.0" + +[[package]] +name = "builtin_macros" +version = "0.1.0" +dependencies = [ + "prettyplease_verus", + "proc-macro2", + "quote", + "syn", + "syn_verus", + "synstructure", +] + +[[package]] +name = "prettyplease_verus" +version = "0.1.15" +dependencies = [ + "proc-macro2", + "syn_verus", +] + +[[package]] +name = "proc-macro2" +version = "1.0.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.36" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "syn_verus" +version = "1.0.95" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "synstructure" +version = "0.12.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f" +dependencies = [ + "proc-macro2", + "quote", + "syn", + "unicode-xid", +] + +[[package]] +name = "unicode-ident" +version = "1.0.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" + +[[package]] +name = "unicode-xid" +version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f962df74c8c05a667b5ee8bcf162993134c104e96440b663c8daa176dc772d8c" + +[[package]] +name = "vstd" +version = "0.1.0" +dependencies = [ + "builtin", + "builtin_macros", +] diff --git a/source/vstd/atomic_ghost.rs b/source/vstd/atomic_ghost.rs index 24922b3ba4..2a7b45ac4c 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/cell.rs b/source/vstd/cell.rs index 1aa700f9ce..e37824d4db 100644 --- a/source/vstd/cell.rs +++ b/source/vstd/cell.rs @@ -19,6 +19,7 @@ verus! { broadcast use super::map::group_map_axioms, super::set::group_set_axioms; // TODO implement: borrow_mut; figure out Drop, see if we can avoid leaking? + /// `PCell` (which stands for "permissioned call") is the primitive Verus `Cell` type. /// /// Technically, it is a wrapper around @@ -55,7 +56,6 @@ broadcast use super::map::group_map_axioms, super::set::group_set_axioms; /// to extract data from the cell. /// /// ### Example (TODO) - #[verifier::external_body] #[verifier::accept_recursive_types(V)] pub struct PCell { diff --git a/source/vstd/pcm_lib.rs b/source/vstd/pcm_lib.rs index d8551d173b..f68f8fc3bf 100644 --- a/source/vstd/pcm_lib.rs +++ b/source/vstd/pcm_lib.rs @@ -8,8 +8,8 @@ use super::seq::*; verus! { broadcast use super::group_vstd_default; -/// Combines a list of values into one value using P::op(). +/// Combines a list of values into one value using P::op(). pub open spec fn combine_values(values: Seq

) -> P decreases values.len(), { diff --git a/source/vstd/std_specs/core.rs b/source/vstd/std_specs/core.rs index c10d1eb00c..92317cdc5a 100644 --- a/source/vstd/std_specs/core.rs +++ b/source/vstd/std_specs/core.rs @@ -56,7 +56,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/std_specs/range.rs b/source/vstd/std_specs/range.rs index d6164b816c..542673881d 100644 --- a/source/vstd/std_specs/range.rs +++ b/source/vstd/std_specs/range.rs @@ -68,7 +68,6 @@ impl< &&& self.cur.spec_is_lt(self.end) || self.cur == self.end // TODO (not important): use new "matches ==>" syntax here - &&& if let Some(init) = init { &&& init.start == init.cur &&& init.start == self.start diff --git a/source/vstd/storage_protocol.rs b/source/vstd/storage_protocol.rs index 415a4b78b3..20901f1727 100644 --- a/source/vstd/storage_protocol.rs +++ b/source/vstd/storage_protocol.rs @@ -4,6 +4,7 @@ use super::prelude::*; verus! { broadcast use super::set::group_set_axioms, super::map::group_map_axioms; + /// Interface for "storage protocol" ghost state. /// This is an extension-slash-variant on the more well-known concept /// of "PCM" ghost state, which we also have an interface for [here](crate::pcm::Resource). @@ -25,7 +26,6 @@ broadcast use super::set::group_set_axioms, super::map::group_map_axioms; /// For applications, I generally advise using the /// [`tokenized_state_machine!` system](https://verus-lang.github.io/verus/state_machines/), /// rather than using this interface directly. - #[verifier::external_body] #[verifier::accept_recursive_types(K)] #[verifier::accept_recursive_types(P)] diff --git a/source/vstd/vstd.rs b/source/vstd/vstd.rs index d3e335d78a..52bebc8ace 100644 --- a/source/vstd/vstd.rs +++ b/source/vstd/vstd.rs @@ -13,6 +13,7 @@ #![cfg_attr(verus_keep_ghost, feature(step_trait))] #![cfg_attr(verus_keep_ghost, feature(ptr_metadata))] #![cfg_attr(verus_keep_ghost, feature(strict_provenance))] +#![cfg_attr(verus_keep_ghost, feature(freeze))] #[cfg(feature = "alloc")] extern crate alloc; From af97df546f5db2b3b12cbab011d87ffd7ee8798b Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Mon, 28 Oct 2024 12:49:41 +0100 Subject: [PATCH 2/7] fmt --- source/rust_verify/src/rust_to_vir_base.rs | 5 ++++- source/rust_verify/src/rust_to_vir_impl.rs | 7 ++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs index 2af33825ea..25b3722917 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs @@ -1527,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_impl.rs b/source/rust_verify/src/rust_to_vir_impl.rs index d5a01fe62d..8dd136755a 100644 --- a/source/rust_verify/src/rust_to_vir_impl.rs +++ b/source/rust_verify/src/rust_to_vir_impl.rs @@ -288,11 +288,8 @@ pub(crate) fn translate_impl<'tcx>( ty ); true - } else if let Some( - 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 From 65b9deb638a76cb0841de5deb49b94b09080dbff Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Fri, 25 Oct 2024 15:22:33 -0700 Subject: [PATCH 3/7] fix vstd error in pointer missing Freeze --- source/vstd/std_specs/core.rs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/source/vstd/std_specs/core.rs b/source/vstd/std_specs/core.rs index a158acd0d6..82ed862654 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; From 1500f0c0b95bcd023613716b82b75f3cb7bf1a0b Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Mon, 28 Oct 2024 20:07:33 +0100 Subject: [PATCH 4/7] prevent const-eval from failing 32-bit usize tests --- source/rust_verify_test/tests/atomic_lib.rs | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/source/rust_verify_test/tests/atomic_lib.rs b/source/rust_verify_test/tests/atomic_lib.rs index 579197fcb4..d2f42892e5 100644 --- a/source/rust_verify_test/tests/atomic_lib.rs +++ b/source/rust_verify_test/tests/atomic_lib.rs @@ -990,27 +990,29 @@ test_verify_one_file! { // 32-bit -test_verify_one_file! { - #[test] test_atomic_usize_32_pass test_body( +// NOTE: we need --no-lifetime because running the compiler in erase mode, even +// if we stop after checking lifetimes, will now perform const evaluation, which +// fails for 32 bit pointers +test_verify_one_file_with_options! { + #[test] test_atomic_usize_32_pass ["--no-lifetime"] => 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) From c6fcf6d0d5d65103b4f5591bac66903af2473da9 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Mon, 28 Oct 2024 20:30:40 +0100 Subject: [PATCH 5/7] remove commented-out overrides --- source/rust_verify/src/verifier.rs | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index f054fbeccf..835dd72473 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -2771,20 +2771,6 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro { config.override_queries = Some(|_session, providers| { providers.hir_crate = hir_crate; - // providers.eval_static_initializer = |tcx, key| { - // eprintln!("static init start {:?}", &key); - // let r = (DEFAULT_QUERY_PROVIDERS.eval_static_initializer)(tcx, key); - // eprintln!("static init end {:?}", &key); - // r - // }; - // - // providers.eval_to_const_value_raw = |tcx, key| { - // eprintln!("eval start {:?}", &key); - // let r = (DEFAULT_QUERY_PROVIDERS.eval_to_const_value_raw)(tcx, key); - // eprintln!("eval end {:?}", &key); - // r - // }; - // 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. From dca492549e8ad188f1979ac8115d9e3c7360dd28 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Mon, 28 Oct 2024 20:38:39 +0100 Subject: [PATCH 6/7] remove vstd/Cargo.lock --- source/vstd/Cargo.lock | 97 ------------------------------------------ 1 file changed, 97 deletions(-) delete mode 100644 source/vstd/Cargo.lock diff --git a/source/vstd/Cargo.lock b/source/vstd/Cargo.lock deleted file mode 100644 index 12842c8de5..0000000000 --- a/source/vstd/Cargo.lock +++ /dev/null @@ -1,97 +0,0 @@ -# This file is automatically @generated by Cargo. -# It is not intended for manual editing. -version = 3 - -[[package]] -name = "builtin" -version = "0.1.0" - -[[package]] -name = "builtin_macros" -version = "0.1.0" -dependencies = [ - "prettyplease_verus", - "proc-macro2", - "quote", - "syn", - "syn_verus", - "synstructure", -] - -[[package]] -name = "prettyplease_verus" -version = "0.1.15" -dependencies = [ - "proc-macro2", - "syn_verus", -] - -[[package]] -name = "proc-macro2" -version = "1.0.86" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" -dependencies = [ - "unicode-ident", -] - -[[package]] -name = "quote" -version = "1.0.36" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" -dependencies = [ - "proc-macro2", -] - -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "syn_verus" -version = "1.0.95" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "synstructure" -version = "0.12.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f" -dependencies = [ - "proc-macro2", - "quote", - "syn", - "unicode-xid", -] - -[[package]] -name = "unicode-ident" -version = "1.0.12" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" - -[[package]] -name = "unicode-xid" -version = "0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f962df74c8c05a667b5ee8bcf162993134c104e96440b663c8daa176dc772d8c" - -[[package]] -name = "vstd" -version = "0.1.0" -dependencies = [ - "builtin", - "builtin_macros", -] From 3d639c0c169ff72f2326f69c82c13b22549ac678 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Wed, 30 Oct 2024 20:40:46 +0100 Subject: [PATCH 7/7] additional fix for const bodies that mix exec and proof code --- source/builtin_macros/src/syntax.rs | 1 - source/rust_verify/src/verifier.rs | 6 ++++++ source/rust_verify_test/tests/consts.rs | 19 +++++++++++++++---- source/rust_verify_test/tests/overflow.rs | 2 +- 4 files changed, 22 insertions(+), 6 deletions(-) diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index 4fc67447ca..2dab1230b1 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -608,7 +608,6 @@ impl Visitor { } } - // TODO(1.79.0) if let Some(SignatureUnwind { token, when }) = unwind { if let Some((when_token, mut when_expr)) = when { self.visit_expr_mut(&mut when_expr); diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index bed22bd51b..a5d64e16a3 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -2771,6 +2771,12 @@ impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro { 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. diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs index 1c117a44d1..ca53f7d3c6 100644 --- a/source/rust_verify_test/tests/consts.rs +++ b/source/rust_verify_test/tests/consts.rs @@ -39,7 +39,7 @@ test_verify_one_file! { #[test] test1_fails2 verus_code! { const C: u64 = S; const S: u64 = C; - } => Err(err) => assert_rust_error_msg(err, "cycle detected when simplifying constant for the type system") + } => Err(err) => assert_vir_error_msg(err, "recursive function must have a decreases clause") } test_verify_one_file! { @@ -186,7 +186,7 @@ test_verify_one_file! { exec static E: u64 = 0; const s: u64 = E; - } => Err(e) => assert_rust_error_msg(e, "referencing statics in constants is unstable") + } => Err(e) => assert_vir_error_msg(e, "cannot read static with mode exec") } test_verify_one_file! { @@ -226,7 +226,7 @@ test_verify_one_file! { proof { let x = E; } 0 } - } => Err(e) => assert_rust_error_msg(e, "cycle detected when evaluating initializer of static") + } => 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_rust_error_msg(e, "cycle detected when simplifying constant for the type system") + } => 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/overflow.rs b/source/rust_verify_test/tests/overflow.rs index 68b99dd797..ee1f1b2942 100644 --- a/source/rust_verify_test/tests/overflow.rs +++ b/source/rust_verify_test/tests/overflow.rs @@ -94,7 +94,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_literal_out_of_range verus_code! { const C: u8 = 256 - 1; - } => Err(err) => assert_rust_error_msg(err, "evaluation of constant value failed") + } => Err(err) => assert_vir_error_msg(err, "integer literal out of range") } test_verify_one_file! {