diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index a90f4c0b0b..67d3bd29c3 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -229,7 +229,6 @@ fn check_item<'tcx>( variant_data, generics, adt_def, - external_info, )?; } ItemKind::Enum(_ident, generics, enum_def) => { diff --git a/source/rust_verify/src/rust_to_vir_adts.rs b/source/rust_verify/src/rust_to_vir_adts.rs index 698f0be9a1..b40e25266c 100644 --- a/source/rust_verify/src/rust_to_vir_adts.rs +++ b/source/rust_verify/src/rust_to_vir_adts.rs @@ -3,7 +3,6 @@ use crate::context::Context; use crate::rust_to_vir_base::{ check_generics_bounds_with_polarity, mk_visibility, mk_visibility_from_vis, }; -use crate::rust_to_vir_impl::ExternalInfo; use crate::unsupported_err_unless; use crate::util::err_span; use air::ast_util::str_ident; @@ -127,7 +126,6 @@ pub(crate) fn check_item_struct<'tcx>( variant_data: &'tcx VariantData<'tcx>, generics: &'tcx Generics<'tcx>, adt_def: rustc_middle::ty::AdtDef<'tcx>, - external_info: &mut ExternalInfo, ) -> Result<(), VirErr> { assert!(adt_def.is_struct()); let vattrs = ctxt.get_verifier_attrs(attrs)?; @@ -144,7 +142,6 @@ pub(crate) fn check_item_struct<'tcx>( &vattrs, generics, adt_def, - external_info, ); } @@ -522,7 +519,6 @@ pub(crate) fn check_item_external<'tcx>( vattrs: &VerifierAttrs, generics: &'tcx Generics<'tcx>, proxy_adt_def: rustc_middle::ty::AdtDef<'tcx>, - external_info: &mut ExternalInfo, ) -> Result<(), VirErr> { // Like with functions, we disallow external_type_specification and external together // (This check is done in rust_to_vir) @@ -573,17 +569,6 @@ pub(crate) fn check_item_external<'tcx>( ); } - if crate::verus_items::get_rust_item(ctxt.tcx, external_adt_def.did()) - == Some(crate::verus_items::RustItem::AllocGlobal) - { - // Don't need to add this to the krate, since we handle this as as a VIR Primitive. - // We only get this far so we can add ourselves to the type_ids list. - // note: seems that Global is added to lang_items in future version of Rust, - // which makes it easier to get the ID so we can simplify this. - external_info.add_type_id(external_adt_def.did()); - return Ok(()); - } - // Check that the type args match. crate::rust_to_vir_base::check_item_external_generics( diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs index e444fb9f46..5705602427 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs @@ -996,13 +996,6 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>( } else { let rust_item = verus_items::get_rust_item(tcx, did); - if let Some(RustItem::AllocGlobal) = rust_item { - return Ok(( - Arc::new(TypX::Primitive(Primitive::Global, Arc::new(vec![]))), - false, - )); - } - let typ_args = mk_typ_args(&args)?; if Some(did) == tcx.lang_items().owned_box() && typ_args.len() == 2 { let (t0, ghost) = &typ_args[0]; diff --git a/source/rust_verify/src/rust_to_vir_impl.rs b/source/rust_verify/src/rust_to_vir_impl.rs index 42267b28f5..5b0f1afd2d 100644 --- a/source/rust_verify/src/rust_to_vir_impl.rs +++ b/source/rust_verify/src/rust_to_vir_impl.rs @@ -53,10 +53,6 @@ impl ExternalInfo { } } - pub(crate) fn add_type_id(&mut self, def_id: DefId) { - self.type_id_map.insert(def_id, true); - } - pub(crate) fn has_type_id<'tcx>(&mut self, ctxt: &Context<'tcx>, def_id: DefId) -> bool { match self.type_id_map.get(&def_id).copied() { None => { diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index f34ccfc485..cbc2919ad5 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -711,8 +711,6 @@ pub(crate) enum RustItem { CloneClone, CloneFrom, IntIntrinsic(RustIntIntrinsicItem), - AllocGlobal, - Allocator, TryTraitBranch, ResidualTraitFromResidual, IntoIterFn, @@ -825,12 +823,6 @@ pub(crate) fn get_rust_item_str(rust_path: Option<&str>) -> Option { return Some(RustItem::CloneFrom); } - if rust_path == Some("alloc::alloc::Global") { - return Some(RustItem::AllocGlobal); - } - if rust_path == Some("core::alloc::Allocator") { - return Some(RustItem::Allocator); - } if rust_path == Some("core::slice::index::private_slice_index::Sealed") { return Some(RustItem::SliceSealed); } diff --git a/source/rust_verify_test/tests/adts.rs b/source/rust_verify_test/tests/adts.rs index 7636cd47fe..ef2576ed3b 100644 --- a/source/rust_verify_test/tests/adts.rs +++ b/source/rust_verify_test/tests/adts.rs @@ -236,6 +236,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_well_founded1 verus_code! { + use vstd::std_specs::alloc::*; enum List { Cons(int, Box) } @@ -244,6 +245,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_well_founded2 verus_code! { + use vstd::std_specs::alloc::*; enum List { Cons1(int, Box), Cons2(int, Box), @@ -253,6 +255,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_well_founded3 verus_code! { + use vstd::std_specs::alloc::*; enum List1 { Cons(int, Box) } @@ -264,6 +267,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_well_founded4 verus_code! { + use vstd::std_specs::alloc::*; enum List { Cons(int, (Box, bool)) } @@ -272,6 +276,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_well_field_unbox verus_code! { + use vstd::std_specs::alloc::*; struct B { b: bool } fn foo(s1: Box, s2: &Box, s3: Box<&B>, s4: Box<(bool, bool)>) { let z1 = s1.b; diff --git a/source/rust_verify_test/tests/external_type_specification.rs b/source/rust_verify_test/tests/external_type_specification.rs index 5babbf5c6f..efc71c68ce 100644 --- a/source/rust_verify_test/tests/external_type_specification.rs +++ b/source/rust_verify_test/tests/external_type_specification.rs @@ -436,14 +436,21 @@ test_verify_one_file! { test_verify_one_file! { #[test] type_recursion_is_handled verus_code! { + use vstd::std_specs::alloc::*; + #[verifier(external)] + pub enum SomeStruct { + No, + Yes(T), + } + #[verifier(external_type_specification)] - #[verifier::reject_recursive_types(U)] - pub struct ExOption(core::option::Option); + #[verifier(reject_recursive_types(U))] + pub struct ExSomeStruct(SomeStruct); struct Test { - t: Box>, + t: Box>, } - } => Err(err) => assert_vir_error_msg(err, "crate::Test recursively uses type crate::Test in a non-positive position") + } => Err(err) => assert_vir_error_msg(err, "Type test_crate::Test recursively uses type test_crate::Test in a non-positive position") } test_verify_one_file! { diff --git a/source/rust_verify_test/tests/match.rs b/source/rust_verify_test/tests/match.rs index 95b9ebe122..0070976999 100644 --- a/source/rust_verify_test/tests/match.rs +++ b/source/rust_verify_test/tests/match.rs @@ -71,6 +71,7 @@ test_verify_one_file! { test_verify_one_file_with_options! { #[test] test2 ["exec_allows_no_decreases_clause"] => verus_code! { + use vstd::std_specs::alloc::*; enum List { Nil, Cons(A, Box>), @@ -120,6 +121,7 @@ test_verify_one_file_with_options! { test_verify_one_file_with_options! { #[test] test2_struct ["exec_allows_no_decreases_clause"] => verus_code! { + use vstd::std_specs::alloc::*; enum List { Nil, Cons { hd: A, tl: Box> }, @@ -169,6 +171,7 @@ test_verify_one_file_with_options! { test_verify_one_file_with_options! { #[test] test2_fails ["exec_allows_no_decreases_clause"] => verus_code! { + use vstd::std_specs::alloc::*; enum List { Nil, Cons(A, Box>), @@ -575,6 +578,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_or_patterns verus_code! { + use vstd::std_specs::alloc::*; #[is_variant] enum Foo { Bar(u64), diff --git a/source/rust_verify_test/tests/recursion.rs b/source/rust_verify_test/tests/recursion.rs index b4714dfc4e..abb124d107 100644 --- a/source/rust_verify_test/tests/recursion.rs +++ b/source/rust_verify_test/tests/recursion.rs @@ -1637,6 +1637,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] decrease_through_abstract_type verus_code! { + use vstd::std_specs::alloc::*; mod m1 { use verus_builtin::*; pub struct S(A, B); @@ -1708,6 +1709,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] height_intrinsic verus_code! { + use vstd::std_specs::alloc::*; #[is_variant] enum Tree { Node(Box, Box), @@ -1745,6 +1747,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] height_intrinsic_mode verus_code! { + use vstd::std_specs::alloc::*; #[is_variant] enum Tree { Node(Box, Box), @@ -1759,6 +1762,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] datatype_height_axiom_checks_the_variant verus_code! { + use vstd::std_specs::alloc::*; #[is_variant] enum List { Cons(Box), diff --git a/source/rust_verify_test/tests/recursive_types.rs b/source/rust_verify_test/tests/recursive_types.rs index a3ca8f64f1..049c0b26ff 100644 --- a/source/rust_verify_test/tests/recursive_types.rs +++ b/source/rust_verify_test/tests/recursive_types.rs @@ -5,6 +5,7 @@ use common::*; test_verify_one_file! { #[test] test1 verus_code! { + use vstd::std_specs::alloc::*; enum E1 { N(), E(Box), @@ -14,6 +15,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test2 verus_code! { + use vstd::std_specs::alloc::*; enum E1 { N(), E(Box), @@ -28,6 +30,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test3 verus_code! { + use vstd::std_specs::alloc::*; struct List { a: A, } @@ -46,6 +49,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test4 verus_code! { + use vstd::std_specs::alloc::*; struct List { a: A, } @@ -64,6 +68,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test1_ok verus_code! { + use vstd::std_specs::alloc::*; struct List { a: A, } @@ -78,6 +83,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test1_fails verus_code! { + use vstd::std_specs::alloc::*; #[verifier::reject_recursive_types(A)] struct List { a: A, @@ -93,6 +99,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test2_ok verus_code! { + use vstd::std_specs::alloc::*; struct List { a: A, } @@ -112,6 +119,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test2_fails verus_code! { + use vstd::std_specs::alloc::*; #[verifier::reject_recursive_types(A)] struct List { a: A, @@ -132,6 +140,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test3_ok verus_code! { + use vstd::std_specs::alloc::*; struct List { a: A, } @@ -151,6 +160,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test3_fails verus_code! { + use vstd::std_specs::alloc::*; #[verifier::reject_recursive_types(A)] struct List { a: A, @@ -271,6 +281,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] no_ground_variant2 verus_code! { + use vstd::std_specs::alloc::*; enum UngroundedList { // error: no ground variant; the only variant is Cons, which recursively uses UngroundedList Cons(A, Box>), @@ -280,6 +291,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] no_ground_variant_via_generics1 verus_code! { + use vstd::std_specs::alloc::*; // from https://github.com/verus-lang/verus/issues/538 struct I(A); struct R(Box>); @@ -303,6 +315,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] no_ground_variant_via_generics2 verus_code! { + use vstd::std_specs::alloc::*; // from https://github.com/verus-lang/verus/issues/538 #[verifier::accept_recursive_types(A)] struct I(A); diff --git a/source/rust_verify_test/tests/regression.rs b/source/rust_verify_test/tests/regression.rs index e20d73a8e8..9f2c8cd109 100644 --- a/source/rust_verify_test/tests/regression.rs +++ b/source/rust_verify_test/tests/regression.rs @@ -340,6 +340,7 @@ test_verify_one_file_with_options! { test_verify_one_file! { #[test] air_function_names_issue_376 verus_code! { + use vstd::std_specs::alloc::*; enum Nat { Zero, Succ(Box), diff --git a/source/rust_verify_test/tests/traits.rs b/source/rust_verify_test/tests/traits.rs index 7294a5595f..07f4b5e649 100644 --- a/source/rust_verify_test/tests/traits.rs +++ b/source/rust_verify_test/tests/traits.rs @@ -4144,6 +4144,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_recursion_through_sync_impl_is_checked verus_code! { + use vstd::std_specs::alloc::*; trait Tr { proof fn tr_g() { } @@ -4192,6 +4193,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_recursion_through_send_impl_is_checked verus_code! { + use vstd::std_specs::alloc::*; trait Tr { proof fn tr_g() { } diff --git a/source/rust_verify_test/tests/traits_dyn.rs b/source/rust_verify_test/tests/traits_dyn.rs index bcecb18513..759b3b0acd 100644 --- a/source/rust_verify_test/tests/traits_dyn.rs +++ b/source/rust_verify_test/tests/traits_dyn.rs @@ -337,6 +337,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] dyn_cycle3 verus_code! { + use vstd::std_specs::alloc::*; trait T { spec fn f(&self, d: &S) -> int; }