diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 282b26a98f..e727428fff 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -106,4 +106,5 @@ jobs: vargo clean vargo build $env:VERUS_Z3_PATH = "$(Get-Location)/z3"; vargo test -p rust_verify_test --test basic + $env:VERUS_Z3_PATH = "$(Get-Location)/z3"; vargo test -p rust_verify_test --test layout shell: powershell diff --git a/dependencies/syn/src/gen/clone.rs b/dependencies/syn/src/gen/clone.rs index 478b8b448b..b0748b0812 100644 --- a/dependencies/syn/src/gen/clone.rs +++ b/dependencies/syn/src/gen/clone.rs @@ -1125,6 +1125,36 @@ impl Clone for Global { Global { attrs: self.attrs.clone(), global_token: self.global_token.clone(), + inner: self.inner.clone(), + semi: self.semi.clone(), + } + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "clone-impls")))] +impl Clone for GlobalInner { + fn clone(&self) -> Self { + match self { + GlobalInner::SizeOf(v0) => GlobalInner::SizeOf(v0.clone()), + GlobalInner::Layout(v0) => GlobalInner::Layout(v0.clone()), + } + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "clone-impls")))] +impl Clone for GlobalLayout { + fn clone(&self) -> Self { + GlobalLayout { + layout_token: self.layout_token.clone(), + type_: self.type_.clone(), + is_token: self.is_token.clone(), + size: self.size.clone(), + align: self.align.clone(), + } + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "clone-impls")))] +impl Clone for GlobalSizeOf { + fn clone(&self) -> Self { + GlobalSizeOf { size_of_token: self.size_of_token.clone(), type_: self.type_.clone(), eq_token: self.eq_token.clone(), diff --git a/dependencies/syn/src/gen/debug.rs b/dependencies/syn/src/gen/debug.rs index f8065e701a..ba00a49544 100644 --- a/dependencies/syn/src/gen/debug.rs +++ b/dependencies/syn/src/gen/debug.rs @@ -1626,6 +1626,44 @@ impl Debug for Global { let mut formatter = formatter.debug_struct("Global"); formatter.field("attrs", &self.attrs); formatter.field("global_token", &self.global_token); + formatter.field("inner", &self.inner); + formatter.field("semi", &self.semi); + formatter.finish() + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Debug for GlobalInner { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + match self { + GlobalInner::SizeOf(v0) => { + let mut formatter = formatter.debug_tuple("SizeOf"); + formatter.field(v0); + formatter.finish() + } + GlobalInner::Layout(v0) => { + let mut formatter = formatter.debug_tuple("Layout"); + formatter.field(v0); + formatter.finish() + } + } + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Debug for GlobalLayout { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + let mut formatter = formatter.debug_struct("GlobalLayout"); + formatter.field("layout_token", &self.layout_token); + formatter.field("type_", &self.type_); + formatter.field("is_token", &self.is_token); + formatter.field("size", &self.size); + formatter.field("align", &self.align); + formatter.finish() + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Debug for GlobalSizeOf { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + let mut formatter = formatter.debug_struct("GlobalSizeOf"); formatter.field("size_of_token", &self.size_of_token); formatter.field("type_", &self.type_); formatter.field("eq_token", &self.eq_token); diff --git a/dependencies/syn/src/gen/eq.rs b/dependencies/syn/src/gen/eq.rs index 8764b7fd7c..da295c06b4 100644 --- a/dependencies/syn/src/gen/eq.rs +++ b/dependencies/syn/src/gen/eq.rs @@ -1104,8 +1104,35 @@ impl Eq for Global {} #[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] impl PartialEq for Global { fn eq(&self, other: &Self) -> bool { - self.attrs == other.attrs && self.type_ == other.type_ - && self.expr_lit == other.expr_lit + self.attrs == other.attrs && self.inner == other.inner + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Eq for GlobalInner {} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl PartialEq for GlobalInner { + fn eq(&self, other: &Self) -> bool { + match (self, other) { + (GlobalInner::SizeOf(self0), GlobalInner::SizeOf(other0)) => self0 == other0, + (GlobalInner::Layout(self0), GlobalInner::Layout(other0)) => self0 == other0, + _ => false, + } + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Eq for GlobalLayout {} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl PartialEq for GlobalLayout { + fn eq(&self, other: &Self) -> bool { + self.type_ == other.type_ && self.size == other.size && self.align == other.align + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Eq for GlobalSizeOf {} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl PartialEq for GlobalSizeOf { + fn eq(&self, other: &Self) -> bool { + self.type_ == other.type_ && self.expr_lit == other.expr_lit } } #[cfg(feature = "full")] diff --git a/dependencies/syn/src/gen/fold.rs b/dependencies/syn/src/gen/fold.rs index 71909816e4..a4f4a6711f 100644 --- a/dependencies/syn/src/gen/fold.rs +++ b/dependencies/syn/src/gen/fold.rs @@ -374,6 +374,15 @@ pub trait Fold { fn fold_global(&mut self, i: Global) -> Global { fold_global(self, i) } + fn fold_global_inner(&mut self, i: GlobalInner) -> GlobalInner { + fold_global_inner(self, i) + } + fn fold_global_layout(&mut self, i: GlobalLayout) -> GlobalLayout { + fold_global_layout(self, i) + } + fn fold_global_size_of(&mut self, i: GlobalSizeOf) -> GlobalSizeOf { + fold_global_size_of(self, i) + } fn fold_ident(&mut self, i: Ident) -> Ident { fold_ident(self, i) } @@ -2189,6 +2198,50 @@ where Global { attrs: FoldHelper::lift(node.attrs, |it| f.fold_attribute(it)), global_token: Token![global](tokens_helper(f, &node.global_token.span)), + inner: f.fold_global_inner(node.inner), + semi: Token![;](tokens_helper(f, &node.semi.spans)), + } +} +pub fn fold_global_inner(f: &mut F, node: GlobalInner) -> GlobalInner +where + F: Fold + ?Sized, +{ + match node { + GlobalInner::SizeOf(_binding_0) => { + GlobalInner::SizeOf(f.fold_global_size_of(_binding_0)) + } + GlobalInner::Layout(_binding_0) => { + GlobalInner::Layout(f.fold_global_layout(_binding_0)) + } + } +} +pub fn fold_global_layout(f: &mut F, node: GlobalLayout) -> GlobalLayout +where + F: Fold + ?Sized, +{ + GlobalLayout { + layout_token: Token![layout](tokens_helper(f, &node.layout_token.span)), + type_: f.fold_type(node.type_), + is_token: Token![is](tokens_helper(f, &node.is_token.span)), + size: ( + f.fold_ident((node.size).0), + Token![==](tokens_helper(f, &(node.size).1.spans)), + f.fold_expr_lit((node.size).2), + ), + align: (node.align) + .map(|it| ( + Token![,](tokens_helper(f, &(it).0.spans)), + f.fold_ident((it).1), + Token![==](tokens_helper(f, &(it).2.spans)), + f.fold_expr_lit((it).3), + )), + } +} +pub fn fold_global_size_of(f: &mut F, node: GlobalSizeOf) -> GlobalSizeOf +where + F: Fold + ?Sized, +{ + GlobalSizeOf { size_of_token: Token![size_of](tokens_helper(f, &node.size_of_token.span)), type_: f.fold_type(node.type_), eq_token: Token![==](tokens_helper(f, &node.eq_token.spans)), diff --git a/dependencies/syn/src/gen/hash.rs b/dependencies/syn/src/gen/hash.rs index 72fbd79862..79a4835c69 100644 --- a/dependencies/syn/src/gen/hash.rs +++ b/dependencies/syn/src/gen/hash.rs @@ -1514,6 +1514,44 @@ impl Hash for Global { H: Hasher, { self.attrs.hash(state); + self.inner.hash(state); + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Hash for GlobalInner { + fn hash(&self, state: &mut H) + where + H: Hasher, + { + match self { + GlobalInner::SizeOf(v0) => { + state.write_u8(0u8); + v0.hash(state); + } + GlobalInner::Layout(v0) => { + state.write_u8(1u8); + v0.hash(state); + } + } + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Hash for GlobalLayout { + fn hash(&self, state: &mut H) + where + H: Hasher, + { + self.type_.hash(state); + self.size.hash(state); + self.align.hash(state); + } +} +#[cfg_attr(doc_cfg, doc(cfg(feature = "extra-traits")))] +impl Hash for GlobalSizeOf { + fn hash(&self, state: &mut H) + where + H: Hasher, + { self.type_.hash(state); self.expr_lit.hash(state); } diff --git a/dependencies/syn/src/gen/visit.rs b/dependencies/syn/src/gen/visit.rs index 5a4e46ab90..a2d5e51a65 100644 --- a/dependencies/syn/src/gen/visit.rs +++ b/dependencies/syn/src/gen/visit.rs @@ -373,6 +373,15 @@ pub trait Visit<'ast> { fn visit_global(&mut self, i: &'ast Global) { visit_global(self, i); } + fn visit_global_inner(&mut self, i: &'ast GlobalInner) { + visit_global_inner(self, i); + } + fn visit_global_layout(&mut self, i: &'ast GlobalLayout) { + visit_global_layout(self, i); + } + fn visit_global_size_of(&mut self, i: &'ast GlobalSizeOf) { + visit_global_size_of(self, i); + } fn visit_ident(&mut self, i: &'ast Ident) { visit_ident(self, i); } @@ -2421,6 +2430,43 @@ where v.visit_attribute(it); } tokens_helper(v, &node.global_token.span); + v.visit_global_inner(&node.inner); + tokens_helper(v, &node.semi.spans); +} +pub fn visit_global_inner<'ast, V>(v: &mut V, node: &'ast GlobalInner) +where + V: Visit<'ast> + ?Sized, +{ + match node { + GlobalInner::SizeOf(_binding_0) => { + v.visit_global_size_of(_binding_0); + } + GlobalInner::Layout(_binding_0) => { + v.visit_global_layout(_binding_0); + } + } +} +pub fn visit_global_layout<'ast, V>(v: &mut V, node: &'ast GlobalLayout) +where + V: Visit<'ast> + ?Sized, +{ + tokens_helper(v, &node.layout_token.span); + v.visit_type(&node.type_); + tokens_helper(v, &node.is_token.span); + v.visit_ident(&(node.size).0); + tokens_helper(v, &(node.size).1.spans); + v.visit_expr_lit(&(node.size).2); + if let Some(it) = &node.align { + tokens_helper(v, &(it).0.spans); + v.visit_ident(&(it).1); + tokens_helper(v, &(it).2.spans); + v.visit_expr_lit(&(it).3); + } +} +pub fn visit_global_size_of<'ast, V>(v: &mut V, node: &'ast GlobalSizeOf) +where + V: Visit<'ast> + ?Sized, +{ tokens_helper(v, &node.size_of_token.span); v.visit_type(&node.type_); tokens_helper(v, &node.eq_token.spans); diff --git a/dependencies/syn/src/gen/visit_mut.rs b/dependencies/syn/src/gen/visit_mut.rs index 260c9d94ee..849084e725 100644 --- a/dependencies/syn/src/gen/visit_mut.rs +++ b/dependencies/syn/src/gen/visit_mut.rs @@ -374,6 +374,15 @@ pub trait VisitMut { fn visit_global_mut(&mut self, i: &mut Global) { visit_global_mut(self, i); } + fn visit_global_inner_mut(&mut self, i: &mut GlobalInner) { + visit_global_inner_mut(self, i); + } + fn visit_global_layout_mut(&mut self, i: &mut GlobalLayout) { + visit_global_layout_mut(self, i); + } + fn visit_global_size_of_mut(&mut self, i: &mut GlobalSizeOf) { + visit_global_size_of_mut(self, i); + } fn visit_ident_mut(&mut self, i: &mut Ident) { visit_ident_mut(self, i); } @@ -2419,6 +2428,43 @@ where v.visit_attribute_mut(it); } tokens_helper(v, &mut node.global_token.span); + v.visit_global_inner_mut(&mut node.inner); + tokens_helper(v, &mut node.semi.spans); +} +pub fn visit_global_inner_mut(v: &mut V, node: &mut GlobalInner) +where + V: VisitMut + ?Sized, +{ + match node { + GlobalInner::SizeOf(_binding_0) => { + v.visit_global_size_of_mut(_binding_0); + } + GlobalInner::Layout(_binding_0) => { + v.visit_global_layout_mut(_binding_0); + } + } +} +pub fn visit_global_layout_mut(v: &mut V, node: &mut GlobalLayout) +where + V: VisitMut + ?Sized, +{ + tokens_helper(v, &mut node.layout_token.span); + v.visit_type_mut(&mut node.type_); + tokens_helper(v, &mut node.is_token.span); + v.visit_ident_mut(&mut (node.size).0); + tokens_helper(v, &mut (node.size).1.spans); + v.visit_expr_lit_mut(&mut (node.size).2); + if let Some(it) = &mut node.align { + tokens_helper(v, &mut (it).0.spans); + v.visit_ident_mut(&mut (it).1); + tokens_helper(v, &mut (it).2.spans); + v.visit_expr_lit_mut(&mut (it).3); + } +} +pub fn visit_global_size_of_mut(v: &mut V, node: &mut GlobalSizeOf) +where + V: VisitMut + ?Sized, +{ tokens_helper(v, &mut node.size_of_token.span); v.visit_type_mut(&mut node.type_); tokens_helper(v, &mut node.eq_token.spans); diff --git a/dependencies/syn/src/item.rs b/dependencies/syn/src/item.rs index af962ac0a8..94e82a6283 100644 --- a/dependencies/syn/src/item.rs +++ b/dependencies/syn/src/item.rs @@ -72,7 +72,7 @@ ast_enum_of_structs! { /// Tokens forming an item not interpreted by Syn. Verbatim(TokenStream), - + // Verus Global(Global), diff --git a/dependencies/syn/src/lib.rs b/dependencies/syn/src/lib.rs index 7234cc4e44..f1ee2aac01 100644 --- a/dependencies/syn/src/lib.rs +++ b/dependencies/syn/src/lib.rs @@ -458,10 +458,10 @@ mod whitespace; mod verus; pub use crate::verus::{ Assert, AssertForall, Assume, BigAnd, BigOr, Closed, DataMode, Decreases, Ensures, ExprHas, - ExprIs, FnMode, Invariant, InvariantEnsures, InvariantNameSet, InvariantNameSetAny, - InvariantNameSetNone, Mode, ModeExec, ModeGhost, ModeProof, ModeSpec, ModeSpecChecked, - ModeTracked, Open, OpenRestricted, Publish, Recommends, Requires, RevealHide, - SignatureDecreases, SignatureInvariants, Specification, TypeFnSpec, View, Global, + ExprIs, FnMode, Global, GlobalInner, GlobalLayout, GlobalSizeOf, Invariant, InvariantEnsures, + InvariantNameSet, InvariantNameSetAny, InvariantNameSetNone, Mode, ModeExec, ModeGhost, + ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted, Publish, Recommends, + Requires, RevealHide, SignatureDecreases, SignatureInvariants, Specification, TypeFnSpec, View, }; mod gen { diff --git a/dependencies/syn/src/token.rs b/dependencies/syn/src/token.rs index 86e514d945..b4e247883c 100644 --- a/dependencies/syn/src/token.rs +++ b/dependencies/syn/src/token.rs @@ -737,6 +737,7 @@ define_keywords! { "has" pub struct Has /// `has` "global" pub struct Global /// `global` "size_of" pub struct SizeOf /// `size_of` + "layout" pub struct Layout /// `layout` } define_punctuation! { @@ -953,6 +954,7 @@ macro_rules! export_token_macro { [has] => { $crate::token::Has }; [global] => { $crate::token::Global }; [size_of] => { $crate::token::SizeOf }; + [layout] => { $crate::token::Layout }; [FnSpec] => { $crate::token::FnSpec }; [&&&] => { $crate::token::BigAnd }; [|||] => { $crate::token::BigOr }; diff --git a/dependencies/syn/src/verus.rs b/dependencies/syn/src/verus.rs index b3d751fc19..4a091a9cd1 100644 --- a/dependencies/syn/src/verus.rs +++ b/dependencies/syn/src/verus.rs @@ -283,9 +283,7 @@ ast_struct! { } ast_struct! { - pub struct Global { - pub attrs: Vec, - pub global_token: Token![global], + pub struct GlobalSizeOf { pub size_of_token: Token![size_of], pub type_: Type, pub eq_token: Token![==], @@ -293,6 +291,32 @@ ast_struct! { } } +ast_struct! { + pub struct GlobalLayout { + pub layout_token: Token![layout], + pub type_: Type, + pub is_token: Token![is], + pub size: (Ident, Token![==], ExprLit), + pub align: Option<(Token![,], Ident, Token![==], ExprLit)>, + } +} + +ast_enum_of_structs! { + pub enum GlobalInner { + SizeOf(GlobalSizeOf), + Layout(GlobalLayout), + } +} + +ast_struct! { + pub struct Global { + pub attrs: Vec, + pub global_token: Token![global], + pub inner: GlobalInner, + pub semi: Token![;], + } +} + #[cfg(feature = "parsing")] pub mod parsing { use super::*; @@ -852,15 +876,27 @@ pub mod parsing { fn parse(input: ParseStream) -> Result { let attrs = Vec::new(); let global_token: Token![global] = input.parse()?; + let inner: GlobalInner = input.parse()?; + let semi: Token![;] = input.parse()?; + + Ok(Global { + attrs, + global_token, + inner, + semi, + }) + } + } + + #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))] + impl Parse for GlobalSizeOf { + fn parse(input: ParseStream) -> Result { let size_of_token: Token![size_of] = input.parse()?; let type_: Type = input.parse()?; let eq_token: Token![==] = input.parse()?; let expr_lit: ExprLit = input.parse()?; - let _: Token![;] = input.parse()?; - - Ok(Global { - attrs, - global_token, + + Ok(GlobalSizeOf { size_of_token, type_, eq_token, @@ -868,6 +904,54 @@ pub mod parsing { }) } } + + #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))] + impl Parse for GlobalLayout { + fn parse(input: ParseStream) -> Result { + let layout_token: Token![layout] = input.parse()?; + let type_: Type = input.parse()?; + let is_token: Token![is] = input.parse()?; + let size_ident: Ident = input.parse()?; + if size_ident.to_string() != "size" { + return Err(input.error("expected `size`")); + } + let size_eq_token: Token![==] = input.parse()?; + let size_expr_lit: ExprLit = input.parse()?; + let size = (size_ident, size_eq_token, size_expr_lit); + let align = if input.peek(Token![,]) { + let comma: Token![,] = input.parse()?; + let align_ident: Ident = input.parse()?; + if align_ident.to_string() != "align" { + return Err(input.error("expected `align`")); + } + let align_eq_token: Token![==] = input.parse()?; + let align_expr_lit: ExprLit = input.parse()?; + Some((comma, align_ident, align_eq_token, align_expr_lit)) + } else { + None + }; + Ok(GlobalLayout { + layout_token, + type_, + is_token, + size, + align, + }) + } + } + + #[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))] + impl Parse for GlobalInner { + fn parse(input: ParseStream) -> Result { + if input.peek(Token![size_of]) { + Ok(GlobalInner::SizeOf(input.parse()?)) + } else if input.peek(Token![layout]) { + Ok(GlobalInner::Layout(input.parse()?)) + } else { + Err(input.error("expected `size_of` or `layout`")) + } + } + } } #[cfg(feature = "printing")] @@ -1171,16 +1255,41 @@ mod printing { } #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))] - impl ToTokens for Global { + impl ToTokens for GlobalSizeOf { fn to_tokens(&self, tokens: &mut TokenStream) { - outer_attrs_to_tokens(&self.attrs, tokens); - self.global_token.to_tokens(tokens); self.size_of_token.to_tokens(tokens); self.type_.to_tokens(tokens); self.eq_token.to_tokens(tokens); self.expr_lit.to_tokens(tokens); } } + + #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))] + impl ToTokens for GlobalLayout { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.layout_token.to_tokens(tokens); + self.type_.to_tokens(tokens); + self.is_token.to_tokens(tokens); + self.size.0.to_tokens(tokens); + self.size.1.to_tokens(tokens); + self.size.2.to_tokens(tokens); + if let Some(align) = &self.align { + align.0.to_tokens(tokens); + align.1.to_tokens(tokens); + align.2.to_tokens(tokens); + } + } + } + + #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))] + impl ToTokens for Global { + fn to_tokens(&self, tokens: &mut TokenStream) { + outer_attrs_to_tokens(&self.attrs, tokens); + self.global_token.to_tokens(tokens); + self.inner.to_tokens(tokens); + self.semi.to_tokens(tokens); + } + } } pub(crate) fn disallow_prefix_binop(input: crate::parse::ParseStream) -> crate::parse::Result<()> { diff --git a/dependencies/syn/syn.json b/dependencies/syn/syn.json index 372bfe256e..e17417bfd3 100644 --- a/dependencies/syn/syn.json +++ b/dependencies/syn/syn.json @@ -2853,6 +2853,86 @@ "global_token": { "token": "Global" }, + "inner": { + "syn": "GlobalInner" + }, + "semi": { + "token": "Semi" + } + } + }, + { + "ident": "GlobalInner", + "features": { + "any": [] + }, + "variants": { + "SizeOf": [ + { + "syn": "GlobalSizeOf" + } + ], + "Layout": [ + { + "syn": "GlobalLayout" + } + ] + } + }, + { + "ident": "GlobalLayout", + "features": { + "any": [] + }, + "fields": { + "layout_token": { + "token": "Layout" + }, + "type_": { + "syn": "Type" + }, + "is_token": { + "token": "Is" + }, + "size": { + "tuple": [ + { + "proc_macro2": "Ident" + }, + { + "token": "EqEq" + }, + { + "syn": "ExprLit" + } + ] + }, + "align": { + "option": { + "tuple": [ + { + "token": "Comma" + }, + { + "proc_macro2": "Ident" + }, + { + "token": "EqEq" + }, + { + "syn": "ExprLit" + } + ] + } + } + } + }, + { + "ident": "GlobalSizeOf", + "features": { + "any": [] + }, + "fields": { "size_of_token": { "token": "SizeOf" }, @@ -6701,6 +6781,7 @@ "InvariantEnsures": "invariant_ensures", "Is": "is", "LArrow": "<-", + "Layout": "layout", "Le": "<=", "Let": "let", "Loop": "loop", diff --git a/dependencies/syn/tests/debug/gen.rs b/dependencies/syn/tests/debug/gen.rs index dd2dd44bd9..fcfcdd36e5 100644 --- a/dependencies/syn/tests/debug/gen.rs +++ b/dependencies/syn/tests/debug/gen.rs @@ -3044,6 +3044,62 @@ impl Debug for Lite { if !_val.attrs.is_empty() { formatter.field("attrs", Lite(&_val.attrs)); } + formatter.field("inner", Lite(&_val.inner)); + formatter.finish() + } +} +impl Debug for Lite { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + let _val = &self.value; + match _val { + syn::GlobalInner::SizeOf(_val) => { + formatter.write_str("SizeOf")?; + formatter.write_str("(")?; + Debug::fmt(Lite(_val), formatter)?; + formatter.write_str(")")?; + Ok(()) + } + syn::GlobalInner::Layout(_val) => { + formatter.write_str("Layout")?; + formatter.write_str("(")?; + Debug::fmt(Lite(_val), formatter)?; + formatter.write_str(")")?; + Ok(()) + } + } + } +} +impl Debug for Lite { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + let _val = &self.value; + let mut formatter = formatter.debug_struct("GlobalLayout"); + formatter.field("type_", Lite(&_val.type_)); + formatter.field("size", &(Lite(&&_val.size.0), Lite(&&_val.size.2))); + if let Some(val) = &_val.align { + #[derive(RefCast)] + #[repr(transparent)] + struct Print( + (syn::token::Comma, proc_macro2::Ident, syn::token::EqEq, syn::ExprLit), + ); + impl Debug for Print { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("Some")?; + let _val = &self.0; + formatter.write_str("(")?; + Debug::fmt(&(Lite(&_val.1), Lite(&_val.3)), formatter)?; + formatter.write_str(")")?; + Ok(()) + } + } + formatter.field("align", Print::ref_cast(val)); + } + formatter.finish() + } +} +impl Debug for Lite { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + let _val = &self.value; + let mut formatter = formatter.debug_struct("GlobalSizeOf"); formatter.field("type_", Lite(&_val.type_)); formatter.field("expr_lit", Lite(&_val.expr_lit)); formatter.finish() diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index 0efd8544b9..eb08e38ef6 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -3,8 +3,8 @@ use crate::EraseGhost; use proc_macro2::Span; use proc_macro2::TokenStream; use proc_macro2::TokenTree; +use quote::format_ident; use quote::{quote, quote_spanned}; -use std::iter::FromIterator; use syn_verus::parse::{Parse, ParseStream}; use syn_verus::punctuated::Punctuated; use syn_verus::spanned::Spanned; @@ -887,33 +887,78 @@ impl Visitor { } for item in items.iter_mut() { if let Item::Global(global) = &item { - let Global { - attrs: _, - global_token: _, - size_of_token: _, - type_, - eq_token: _, - expr_lit, - } = global; + use quote::ToTokens; + let Global { attrs: _, global_token: _, inner, semi: _ } = global; + let (type_, size_lit, align_lit) = match inner { + syn_verus::GlobalInner::SizeOf(size_of) => { + (&size_of.type_, &size_of.expr_lit, None) + } + syn_verus::GlobalInner::Layout(layout) => { + (&layout.type_, &layout.size.2, layout.align.as_ref().map(|a| &a.3)) + } + }; let span = item.span(); - let static_assert = quote_spanned! { span => - if ::core::mem::size_of::<#type_>() != #expr_lit { + let static_assert_size = quote! { + if ::core::mem::size_of::<#type_>() != #size_lit { panic!("does not have the expected size"); } }; + 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"); + } + } + } else { + quote! {} + }; if self.erase_ghost.erase() { *item = Item::Verbatim( quote_spanned! { span => #[verus::internal(size_of)] const _: () = { - #static_assert + #static_assert_size + #static_assert_align }; }, ); } else { - *item = Item::Verbatim( - quote_spanned! { span => #[verus::internal(size_of)] const _: () = { - ::builtin::global_size_of::<#type_>(#expr_lit); - #static_assert - }; }, - ); + let type_name_escaped = format!("{}", type_.into_token_stream()) + .replace(" ", "") + .replace("<", "_LL_") + .replace(">", "_RR_"); + if !type_name_escaped.chars().all(|c| c.is_alphanumeric() || c == '_') { + let err = + "this type name is not supported (it must only include A-Za-z0-9<>)"; + *item = Item::Verbatim( + quote_spanned!(span => const _: () = { compile_error!(#err) };), + ); + } else { + let lemma_ident = format_ident!("VERUS_layout_of_{}", type_name_escaped); + + let ensures_align = if let Some(align_lit) = align_lit { + quote! { ::vstd::layout::align_of::<#type_>() == #align_lit, } + } else { + quote! {} + }; + + *item = Item::Verbatim(quote_spanned! { span => + #[verus::internal(size_of)] const _: () = { + ::builtin::global_size_of::<#type_>(#size_lit); + + #static_assert_size + #static_assert_align + }; + + ::builtin_macros::verus! { + #[verifier::external_body] + #[verifier::broadcast_forall] + #[allow(non_snake_case)] + proof fn #lemma_ident() + ensures + ::vstd::layout::size_of::<#type_>() == #size_lit, + #ensures_align + {} + } + }); + } } } } @@ -2856,6 +2901,7 @@ fn rejoin_tokens(stream: proc_macro::TokenStream) -> proc_macro::TokenStream { _ => {} } } + use std::iter::FromIterator; proc_macro::TokenStream::from_iter(tokens.into_iter()) } diff --git a/source/pervasive/layout.rs b/source/pervasive/layout.rs new file mode 100644 index 0000000000..de6a58309e --- /dev/null +++ b/source/pervasive/layout.rs @@ -0,0 +1,109 @@ +#![allow(unused_imports)] + +use builtin::*; +use builtin_macros::*; +use crate::prelude::*; + +verus!{ + +// TODO add some means for Verus to calculate the size & alignment of types + +// TODO use a definition from a math library, once we have one. +pub open spec fn is_power_2(n: int) -> bool + decreases n +{ + if n <= 0 { + false + } else if n == 1 { + true + } else { + n % 2 == 0 && is_power_2(n / 2) + } +} + +/// Matches the conditions here: https://doc.rust-lang.org/stable/std/alloc/struct.Layout.html +pub open spec fn valid_layout(size: usize, align: usize) -> bool { + is_power_2(align as int) + && size <= isize::MAX as int - (isize::MAX as int % align as int) +} + +// Keep in mind that the `V: Sized` trait bound is COMPLETELY ignored in the +// VIR encoding. It is not possible to write an axiom like +// "If `V: Sized`, then `size_of::<&V>() == size_of::()`. +// If you tried, it wouldn't work the way you expect. +// The ONLY thing that checks Sized marker bounds is rustc, but it is possible +// to get around rustc's checks with broadcast_forall. +// Therefore, in spec-land, we must use the `is_sized` predicate instead. +// +// Note: for exec functions, and for proof functions that take tracked arguments, +// we CAN rely on rustc's checking. So in those cases it's okay for us to assume +// a `V: Sized` type is sized. + +pub spec fn is_sized() -> bool; +pub spec fn size_of() -> nat; +pub spec fn align_of() -> nat; + +// Naturally, the size of any executable type is going to fit into a `usize`. +// What I'm not sure of is whether it will be possible to "reason about" arbitrarily +// big types _in ghost code_ without tripping one of rustc's checks. +// +// I think it could go like this: +// - Have some polymorphic code that constructs a giant tuple and proves false +// - Make sure the code doesn't get monomorphized by rustc +// - To export the 'false' fact from the polymorphic code without monomorphizing, +// use broadcast_forall. +// +// Therefore, we are NOT creating an axiom that `size_of` fits in usize. +// However, we still give the guarantee that if you call `core::mem::size_of` +// at runtime, then the resulting usize is correct. + +#[verifier(inline)] +pub open spec fn size_of_as_usize() -> usize + recommends size_of::() as usize as int == size_of::() +{ + size_of::() as usize +} + +#[verifier(inline)] +pub open spec fn align_of_as_usize() -> usize + recommends align_of::() as usize as int == align_of::() +{ + align_of::() as usize +} + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(size_of_as_usize)] +pub fn ex_size_of() -> (u: usize) + ensures + is_sized::(), + u as nat == size_of::(), + +{ + core::mem::size_of::() +} + +#[verifier::external_fn_specification] +#[verifier::when_used_as_spec(align_of_as_usize)] +pub fn ex_align_of() -> (u: usize) + ensures + is_sized::(), + u as nat == align_of::() +{ + core::mem::align_of::() +} + +// This is marked as exec, again, in order to force `V` to be a real exec type. +// Of course, it's still a no-op. + +#[verifier(external_body)] +#[inline(always)] +pub exec fn layout_for_type_is_valid() + ensures + valid_layout(size_of::() as usize, align_of::() as usize), + is_sized::(), + size_of::() as usize as nat == size_of::(), + align_of::() as usize as nat == align_of::(), +{ +} + +} diff --git a/source/pervasive/ptr.rs b/source/pervasive/ptr.rs index dedc3e4e97..52a47f169c 100644 --- a/source/pervasive/ptr.rs +++ b/source/pervasive/ptr.rs @@ -1,5 +1,6 @@ #![allow(unused_imports)] +use alloc::alloc::Layout; use core::{marker, mem, mem::MaybeUninit}; use builtin::*; @@ -8,9 +9,14 @@ use crate::*; use crate::pervasive::*; use crate::modes::*; use crate::prelude::*; +use crate::layout::*; + +#[cfg(verus_keep_ghost)] +use crate::set_lib::set_int_range; verus!{ + /// `PPtr` (which stands for "permissioned pointer") /// is a wrapper around a raw pointer to `V` on the heap. /// @@ -115,13 +121,24 @@ verus!{ // // However, int->ptr conversions ought to be allowed in the VERUS POINTER MODEL, // so I'm going with (2) here. +// +// TODO reconsider: Is this plan actually good? Exposing all pointers has the potential +// to ruin optimizations. If the plan is bad, and we want to avoid the cost of +// "expose-everywhere", we may need to actually track provenance as part +// of the specification of PPtr. +// +// Perhaps what we could do is specify a low-level pointer library with +// strict provenance rules + exposed pointers, +// and then verify user libraries on top of that? // TODO implement: borrow_mut; figure out Drop, see if we can avoid leaking? +// TODO just replace this with `*mut V` +#[repr(C)] #[verifier(external_body)] #[verifier::accept_recursive_types(V)] pub struct PPtr { - uptr: *mut MaybeUninit, + pub uptr: *mut V, } // PPtr is always safe to Send/Sync. It's the PointsTo object where Send/Sync matters. @@ -133,7 +150,7 @@ unsafe impl Sync for PPtr {} #[verifier(external)] unsafe impl Send for PPtr {} -// TODO split up the "deallocation" permission and the "access" permission? +// TODO some of functionality could have V: ?Sized /// A `tracked` ghost object that gives the user permission to dereference a pointer /// for reading or writing, or to free the memory at that pointer. @@ -164,6 +181,44 @@ pub ghost struct PointsToData { pub value: Option, } +// TODO add similiar height axioms for other ghost objects + +#[verifier(broadcast_forall)] +#[verifier(external_body)] +pub proof fn points_to_height_axiom(points_to: PointsTo) + ensures #[trigger] is_smaller_than(points_to@, points_to) +{ + unimplemented!() +} + +/// Points to uninitialized memory. + +#[verifier(external_body)] +pub tracked struct PointsToRaw { + no_copy: NoCopy, +} + +#[verifier(external_body)] +pub tracked struct Dealloc<#[verifier(strictly_positive)] V> { + phantom: marker::PhantomData, + no_copy: NoCopy, +} + +pub ghost struct DeallocData { + pub pptr: int, +} + +#[verifier(external_body)] +pub tracked struct DeallocRaw { + no_copy: NoCopy, +} + +pub ghost struct DeallocRawData { + pub pptr: int, + pub size: nat, + pub align: nat, +} + impl PointsTo { pub spec fn view(self) -> PointsToData; @@ -187,8 +242,215 @@ impl PointsTo { } } -impl PPtr { +impl PointsTo { + #[verifier(external_body)] + pub proof fn into_raw(tracked self) -> (tracked points_to_raw: PointsToRaw) + requires + self@.value.is_None(), + ensures + points_to_raw.is_range(self@.pptr, size_of::() as int), + is_sized::(), + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn borrow_raw(tracked &self) -> (tracked points_to_raw: &PointsToRaw) + requires + self@.value.is_None(), + ensures + points_to_raw.is_range(self@.pptr, size_of::() as int), + is_sized::(), + { + unimplemented!(); + } +} + +impl PointsToRaw { + pub spec fn view(self) -> Map; + + pub open spec fn contains_range(self, start: int, len: int) -> bool { + set_int_range(start, start + len).subset_of(self@.dom()) + } + + pub open spec fn is_range(self, start: int, len: int) -> bool { + set_int_range(start, start + len) =~= self@.dom() + } + + pub open spec fn spec_index(self, i: int) -> u8 { + self@[i] + } + + #[verifier(external_body)] + pub proof fn is_nonnull(tracked &self) + ensures !self@.dom().contains(0) + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn is_in_bounds(tracked &self) + ensures forall |i: int| self@.dom().contains(i) ==> 0 < i <= usize::MAX, + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn empty() -> (tracked points_to_raw: Self) + ensures points_to_raw@ == Map::::empty(), + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn into_typed(tracked self, start: int) -> (tracked points_to: PointsTo) + requires + is_sized::(), + start % align_of::() as int == 0, + self.is_range(start, size_of::() as int), + ensures + points_to@.pptr === start, + points_to@.value === None, + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn borrow_typed(tracked &self, start: int) -> (tracked points_to: &PointsTo) + requires + is_sized::(), + start % align_of::() as int == 0, + self.contains_range(start, size_of::() as int), + ensures + points_to@.pptr === start, + points_to@.value === None, + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn join(tracked self, tracked other: Self) -> (tracked joined: Self) + ensures + self@.dom().disjoint(other@.dom()), + joined@ == self@.union_prefer_right(other@), + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn borrow_join<'a>(tracked &'a self, tracked other: &'a Self) -> (tracked joined: &'a Self) + ensures + (forall |i| #![trigger self@.dom().contains(i), other@.dom().contains(i)] + self@.dom().contains(i) && other@.dom().contains(i) ==> self@[i] == other@[i]), + joined@ == self@.union_prefer_right(other@), + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn split(tracked self, range: Set) -> (tracked res: (Self, Self)) + requires + range.subset_of(self@.dom()), + ensures + res.0@ == self@.restrict(range), + res.1@ == self@.remove_keys(range), + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn borrow_subset(tracked &self, range: Set) -> (tracked res: &Self) + requires + range.subset_of(self@.dom()), + ensures + res@ == self@.restrict(range), + { + unimplemented!(); + } +} + +impl Dealloc { + pub spec fn view(self) -> DeallocData; +} + +impl Dealloc { + #[verifier(external_body)] + pub proof fn is_nonnull(tracked &self) + ensures self@.pptr != 0, + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn into_raw(tracked self) -> (tracked dealloc_raw: DeallocRaw) + ensures + dealloc_raw@.pptr === self@.pptr, + dealloc_raw@.size === size_of::(), + dealloc_raw@.align === align_of::(), + is_sized::(), + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn borrow_raw(tracked &self) -> (tracked dealloc_raw: &DeallocRaw) + ensures + dealloc_raw@.pptr === self@.pptr, + dealloc_raw@.size === size_of::(), + dealloc_raw@.align === align_of::(), + is_sized::(), + { + unimplemented!(); + } +} + +impl DeallocRaw { + pub spec fn view(self) -> DeallocRawData; + + #[verifier(external_body)] + pub proof fn is_nonnull(tracked &self) + ensures self@.pptr != 0, + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn into_typed(tracked self) -> (tracked dealloc: Dealloc) + requires + is_sized::(), + self@.size === size_of::(), + self@.align === align_of::(), + ensures + dealloc@.pptr === self@.pptr, + { + unimplemented!(); + } + + #[verifier(external_body)] + pub proof fn borrow_typed(tracked &self) -> (tracked dealloc: &Dealloc) + requires + is_sized::(), + self@.size === size_of::(), + self@.align === align_of::(), + ensures + dealloc@.pptr === self@.pptr, + { + unimplemented!(); + } +} + +impl Clone for PPtr { + #[verifier(external_body)] + fn clone(&self) -> (s: Self) + ensures s == *self, + { + PPtr { uptr: self.uptr } + } +} +impl Copy for PPtr { } + +impl PPtr { /// Cast a pointer to an integer. #[inline(always)] @@ -221,7 +483,7 @@ impl PPtr { pub fn from_usize(u: usize) -> (p: Self) ensures p.id() == u as int, { - let uptr = u as *mut MaybeUninit; + let uptr = u as *mut V; PPtr { uptr } } @@ -229,30 +491,42 @@ impl PPtr { #[inline(always)] #[verifier(external_body)] - pub fn empty() -> (pt: (PPtr, Tracked>)) - ensures pt.1@@ === (PointsToData{ pptr: pt.0.id(), value: Option::None }), + pub fn empty() -> (pt: (PPtr, Tracked>, Tracked>)) + ensures + pt.1@@ === (PointsToData{ pptr: pt.0.id(), value: None }), + pt.2@@ === (DeallocData{ pptr: pt.0.id() }), opens_invariants none { - let p = PPtr { - uptr: alloc::boxed::Box::leak(alloc::boxed::Box::new(MaybeUninit::uninit())).as_mut_ptr(), - }; - - // See explanation about exposing pointers, above - let _exposed_addr = p.uptr as usize; - - (p, Tracked::assume_new(|| unreachable!())) + let layout = Layout::new::(); + let size = layout.size(); + let align = layout.align(); + let (p, _, _) = PPtr::::alloc(size, align); + (p, Tracked::assume_new(|| unreachable!()), Tracked::assume_new(|| unreachable!())) } - /// Clones the pointer. - /// TODO implement the `Clone` and `Copy` traits - #[inline(always)] #[verifier(external_body)] - pub fn clone(&self) -> (pt: PPtr) - ensures pt.id() === self.id(), + pub fn alloc(size: usize, align: usize) -> (pt: (PPtr, Tracked, Tracked)) + requires + valid_layout(size, align), + ensures + pt.1@.is_range(pt.0.id(), size as int), + pt.2@@ === (DeallocRawData{ pptr: pt.0.id(), size: size as nat, align: align as nat }), + pt.0.id() % align as int == 0, opens_invariants none { - PPtr { uptr: self.uptr } + // Add padding (this is to prevent the user from being able to "combine" allocations) + // Constructing the layout object might fail if the allocation becomes too big. + // The 'add' can't overflow, since we already know (size, align) is a valid layout. + let layout = Layout::from_size_align(size + align, align).unwrap(); + let p = PPtr { + uptr: unsafe { ::alloc::alloc::alloc(layout) as *mut V }, + }; + + // See explanation about exposing pointers, above + let _exposed_addr = p.uptr as usize; + + (p, Tracked::assume_new(|| unreachable!()), Tracked::assume_new(|| unreachable!())) } /// Moves `v` into the location pointed to by the pointer `self`. @@ -266,14 +540,18 @@ impl PPtr { pub fn put(&self, Tracked(perm): Tracked<&mut PointsTo>, v: V) requires self.id() === old(perm)@.pptr, - old(perm)@.value === Option::None, + old(perm)@.value === None, ensures perm@.pptr === old(perm)@.pptr, - perm@.value === Option::Some(v), + perm@.value === Some(v), opens_invariants none { + // See explanation about exposing pointers, above + let ptr = self.uptr as usize as *mut V; + unsafe { - *(self.uptr) = MaybeUninit::new(v); + // We use `write` here because it does not attempt to "drop" the memory at `*ptr`. + core::ptr::write(ptr, v); } } @@ -293,14 +571,15 @@ impl PPtr { old(perm)@.value.is_Some(), ensures perm@.pptr === old(perm)@.pptr, - perm@.value === Option::None, + perm@.value === None, v === old(perm)@.value.get_Some_0(), opens_invariants none { + // See explanation about exposing pointers, above + let ptr = self.uptr as usize as *mut V; + unsafe { - let mut m = MaybeUninit::uninit(); - mem::swap(&mut m, &mut *self.uptr); - m.assume_init() + core::ptr::read(ptr) } } @@ -315,14 +594,17 @@ impl PPtr { old(perm)@.value.is_Some(), ensures perm@.pptr === old(perm)@.pptr, - perm@.value === Option::Some(in_v), + perm@.value === Some(in_v), out_v === old(perm)@.value.get_Some_0(), opens_invariants none { + // See explanation about exposing pointers, above + let ptr = self.uptr as usize as *mut V; + unsafe { - let mut m = MaybeUninit::new(in_v); - mem::swap(&mut m, &mut *self.uptr); - m.assume_init() + let mut m = in_v; + mem::swap(&mut m, &mut *ptr); + m } } @@ -340,8 +622,11 @@ impl PPtr { ensures *v === perm@.value.get_Some_0(), opens_invariants none { + // See explanation about exposing pointers, above + let ptr = self.uptr as usize as *mut V; + unsafe { - (*self.uptr).assume_init_ref() + &*ptr } } @@ -353,14 +638,44 @@ impl PPtr { #[inline(always)] #[verifier(external_body)] - pub fn dispose(&self, Tracked(perm): Tracked>) + pub fn dispose(&self, Tracked(perm): Tracked>, Tracked(dealloc): Tracked>) requires self.id() === perm@.pptr, - perm@.value === Option::None, + perm@.value === None, + perm@.pptr == dealloc@.pptr, opens_invariants none { unsafe { - alloc::alloc::dealloc(self.uptr as *mut u8, alloc::alloc::Layout::for_value(&*self.uptr)); + let layout = alloc::alloc::Layout::for_value(&*self.uptr); + let size = layout.size(); + let align = layout.align(); + // Add the padding to match what we did in 'alloc' + let layout = Layout::from_size_align_unchecked(size + align, align); + ::alloc::alloc::dealloc(self.uptr as *mut u8, layout); + } + } + + #[inline(always)] + #[verifier(external_body)] + pub fn dealloc(&self, + size: usize, + align: usize, + Tracked(perm): Tracked, + Tracked(dealloc): Tracked + ) + requires + perm.is_range(self.id(), size as int), + dealloc@.pptr === self.id(), + dealloc@.size === size as nat, + dealloc@.align === align as nat, + opens_invariants none + { + unsafe { + // Since we have the Dealloc object, we know this is a valid layout + // and that it's safe to call 'deallocate' + // Remember to add the padding, like in `alloc` + let layout = Layout::from_size_align_unchecked(size + align, align); + ::alloc::alloc::dealloc(self.uptr as *mut u8, layout); } } @@ -374,9 +689,10 @@ impl PPtr { /// access to the memory by freeing it. #[inline(always)] - pub fn into_inner(self, Tracked(perm): Tracked>) -> (v: V) + pub fn into_inner(self, Tracked(perm): Tracked>, Tracked(dealloc): Tracked>) -> (v: V) requires self.id() === perm@.pptr, + perm@.pptr == dealloc@.pptr, perm@.value.is_Some(), ensures v === perm@.value.get_Some_0(), @@ -384,7 +700,7 @@ impl PPtr { { let tracked mut perm = perm; let v = self.take(Tracked(&mut perm)); - self.dispose(Tracked(perm)); + self.dispose(Tracked(perm), Tracked(dealloc)); v } @@ -392,13 +708,46 @@ impl PPtr { /// with the given value `v`. #[inline(always)] - pub fn new(v: V) -> (pt: (PPtr, Tracked>)) + pub fn new(v: V) -> (pt: (PPtr, Tracked>, Tracked>)) ensures - (pt.1@@ === PointsToData{ pptr: pt.0.id(), value: Option::Some(v) }), + (pt.1@@ === PointsToData{ pptr: pt.0.id(), value: Some(v) }), + (pt.2@@ === DeallocData{ pptr: pt.0.id() }), { - let (p, Tracked(mut t)) = Self::empty(); + let (p, Tracked(mut t), Tracked(d)) = Self::empty(); p.put(Tracked(&mut t), v); - (p, Tracked(t)) + (p, Tracked(t), Tracked(d)) + } +} + +// Manipulating the contents in a PointsToRaw + +impl PPtr { + #[cfg_attr(not(verus_keep_ghost), allow(unused_variables))] + #[verifier::external_body] + fn copy_nonoverlapping(&self, dst: PPtr, count: usize, perm_src: &PointsToRaw, perm_dst: &mut PointsToRaw) + requires perm_src.contains_range(self.id(), count as int), + old(perm_dst).contains_range(dst.id(), count as int), + ensures + perm_dst@ == old(perm_dst)@.union_prefer_right( + perm_src@.restrict(set_int_range(self.id(), self.id() + count))) + { + unsafe { + core::ptr::copy_nonoverlapping(self.uptr, dst.uptr, count) + } + } + + #[cfg_attr(not(verus_keep_ghost), allow(unused_variables))] + #[verifier::external_body] + fn write_bytes(&self, val: u8, count: usize, perm: &mut PointsToRaw) + requires old(perm).contains_range(self.id(), count as int), + ensures + perm@ == old(perm)@.union_prefer_right( + Map::new(|addr| set_int_range(self.id(), self.id() + count).contains(addr), + |addr| val)) + { + unsafe { + core::ptr::write_bytes::(self.uptr, val, count); + } } } diff --git a/source/pervasive/vstd.rs b/source/pervasive/vstd.rs index 2fe34d208b..6d775067f9 100644 --- a/source/pervasive/vstd.rs +++ b/source/pervasive/vstd.rs @@ -11,6 +11,7 @@ #![allow(rustdoc::invalid_rust_codeblocks)] #![cfg_attr(verus_keep_ghost, feature(core_intrinsics))] +#![cfg_attr(verus_keep_ghost, feature(allocator_api))] #[cfg(feature = "alloc")] extern crate alloc; @@ -34,6 +35,7 @@ pub mod atomic; pub mod atomic_ghost; pub mod math; pub mod modes; +pub mod layout; pub mod multiset; pub mod function; pub mod state_machine_internal; diff --git a/source/rust_verify/example/doubly_linked_xor.rs b/source/rust_verify/example/doubly_linked_xor.rs index a8e7e61077..4f392a6b28 100644 --- a/source/rust_verify/example/doubly_linked_xor.rs +++ b/source/rust_verify/example/doubly_linked_xor.rs @@ -30,9 +30,11 @@ struct Node { // Contains head pointer, tail pointer // and in ghost code, tracks all the pointers and all the permissions to access the nodes +type MemPerms = (PointsTo>, Dealloc>); + struct DListXor { ptrs: Ghost>>>, - perms: Tracked>>>, + perms: Tracked>>, head: u64, tail: u64, @@ -67,11 +69,12 @@ impl DListXor { recommends i < self.ptrs@.len() { &&& self.perms@.dom().contains(i) - &&& self.perms@[i].view().pptr == self.ptrs@[i as int].id() + &&& self.perms@[i].0.view().pptr == self.ptrs@[i as int].id() + &&& self.perms@[i].1.view().pptr == self.ptrs@[i as int].id() &&& 0 < self.ptrs@[i as int].id() &&& self.ptrs@[i as int].id() < 0x10000000000000000 - &&& self.perms@[i].view().value.is_Some() - &&& self.perms@[i].view().value.get_Some_0().xored == ( + &&& self.perms@[i].0.view().value.is_Some() + &&& self.perms@[i].0.view().value.get_Some_0().xored == ( self.prev_of(i) ^ self.next_of(i) ) } @@ -102,7 +105,7 @@ impl DListXor { { Seq::::new(self.ptrs@.len(), |i: int| { - self.perms@[i as nat]@.value.get_Some_0().v + self.perms@[i as nat].0@.value.get_Some_0().v }) } @@ -127,15 +130,14 @@ impl DListXor { self.wf(), self@ == old(self)@.push(v), { - let (ptr, perm) = PPtr::new( + let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new( Node:: { xored: 0, v } ); proof { self.ptrs@ = self.ptrs@.push(ptr); - let tracked perm = perm.get(); (&perm).is_nonnull(); - (self.perms.borrow_mut()) - .tracked_insert((self.ptrs@.len() - 1) as nat, perm); + self.perms.borrow_mut() + .tracked_insert((self.ptrs@.len() - 1) as nat, (perm, dealloc)); } self.tail = ptr.to_usize() as u64; @@ -169,17 +171,17 @@ impl DListXor { let tail_ptr_u64 = self.tail; proof { lemma_usize_u64(tail_ptr_u64); } let tail_ptr = PPtr::>::from_usize(tail_ptr_u64 as usize); - let tracked mut tail_perm: PointsTo> = - (self.perms.borrow_mut()).tracked_remove((self.ptrs@.len() - 1) as nat); + let tracked (mut tail_perm, de): MemPerms = + self.perms.borrow_mut().tracked_remove((self.ptrs@.len() - 1) as nat); let mut tail_node = tail_ptr.take(Tracked(&mut tail_perm)); let second_to_last_ptr = tail_node.xored; - let (ptr, perm) = PPtr::new( + let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new( Node:: { xored: tail_ptr_u64, v } ); proof { - (perm.borrow()).is_nonnull(); + perm.is_nonnull(); } let new_ptr_u64 = ptr.to_usize() as u64; @@ -187,10 +189,10 @@ impl DListXor { tail_node.xored = second_to_last_ptr ^ new_ptr_u64; tail_ptr.put(Tracked(&mut tail_perm), tail_node); proof { - (self.perms.borrow_mut()) - .tracked_insert((self.ptrs@.len() - 1) as nat, tail_perm); - (self.perms.borrow_mut()) - .tracked_insert(self.ptrs@.len(), (perm).get()); + self.perms.borrow_mut() + .tracked_insert((self.ptrs@.len() - 1) as nat, (tail_perm, de)); + self.perms.borrow_mut() + .tracked_insert(self.ptrs@.len(), (perm, dealloc)); self.ptrs@ = self.ptrs@.push(ptr); } self.tail = new_ptr_u64; @@ -240,10 +242,9 @@ impl DListXor { let last_u64 = self.tail; proof { lemma_usize_u64(last_u64); } let last_ptr = PPtr::>::from_usize(last_u64 as usize); - let last_perm: Tracked>> = Tracked( - (self.perms.borrow_mut()).tracked_remove((self.ptrs@.len() - 1) as nat) - ); - let last_node = last_ptr.into_inner(last_perm); + let tracked last_perm: MemPerms = + self.perms.borrow_mut().tracked_remove((self.ptrs@.len() - 1) as nat); + let last_node = last_ptr.into_inner(Tracked(last_perm.0), Tracked(last_perm.1)); let penult_u64 = last_node.xored; let v = last_node.v; @@ -279,8 +280,8 @@ impl DListXor { lemma_usize_u64(penult_u64); } let penult_ptr = PPtr::>::from_usize(penult_u64 as usize); - let tracked mut penult_perm = - (self.perms.borrow_mut()).tracked_remove((self.ptrs@.len() - 2) as nat); + let tracked (mut penult_perm, de) = + self.perms.borrow_mut().tracked_remove((self.ptrs@.len() - 2) as nat); let mut penult_node = penult_ptr.take(Tracked(&mut penult_perm)); let t: Ghost = Ghost(self.prev_of((self.ptrs@.len() - 2) as nat)); assert((t@ ^ last_u64) ^ last_u64 == t@ ^ 0) by(bit_vector); @@ -291,8 +292,8 @@ impl DListXor { penult_ptr.put(Tracked(&mut penult_perm), penult_node); proof { - (self.perms.borrow_mut()) - .tracked_insert((self.ptrs@.len() - 2) as nat, penult_perm); + self.perms.borrow_mut() + .tracked_insert((self.ptrs@.len() - 2) as nat, (penult_perm, de)); } } @@ -349,10 +350,9 @@ impl DListXor { let first_u64 = self.head; proof { lemma_usize_u64(first_u64); } let first_ptr = PPtr::>::from_usize(first_u64 as usize); - let first_perm: Tracked>> = Tracked( - (self.perms.borrow_mut()).tracked_remove(0) - ); - let first_node = first_ptr.into_inner(first_perm); + let tracked first_perm: MemPerms = + self.perms.borrow_mut().tracked_remove(0); + let first_node = first_ptr.into_inner(Tracked(first_perm.0), Tracked(first_perm.1)); let second_u64 = first_node.xored; let v = first_node.v; @@ -388,7 +388,7 @@ impl DListXor { lemma_usize_u64(second_u64); } let second_ptr = PPtr::>::from_usize(second_u64 as usize); - let tracked mut second_perm = (self.perms.borrow_mut()).tracked_remove(1); + let tracked (mut second_perm, de) = (self.perms.borrow_mut()).tracked_remove(1); let mut second_node = second_ptr.take(Tracked(&mut second_perm)); let t: Ghost = Ghost(self.next_of(1)); assert((first_u64 ^ t@) ^ first_u64 == 0 ^ t@) by(bit_vector); @@ -399,8 +399,8 @@ impl DListXor { second_ptr.put(Tracked(&mut second_perm), second_node); proof { - (self.perms.borrow_mut()) - .tracked_insert(1, second_perm); + self.perms.borrow_mut() + .tracked_insert(1, (second_perm, de)); assert forall |j: nat| 1 <= j < old(self)@.len() implies self.perms@.dom().contains(j) @@ -469,17 +469,17 @@ impl DListXor { let head_ptr_u64 = self.head; proof { lemma_usize_u64(head_ptr_u64); } let head_ptr = PPtr::>::from_usize(head_ptr_u64 as usize); - let tracked mut head_perm: PointsTo> = + let tracked (mut head_perm, de): MemPerms = (self.perms.borrow_mut()).tracked_remove(0); let mut head_node = head_ptr.take(Tracked(&mut head_perm)); let second_ptr = head_node.xored; - let (ptr, perm) = PPtr::new( + let (ptr, Tracked(perm), Tracked(dealloc)) = PPtr::new( Node:: { xored: head_ptr_u64, v } ); proof { - (perm.borrow()).is_nonnull(); + perm.is_nonnull(); } let new_ptr_u64 = ptr.to_usize() as u64; @@ -487,22 +487,22 @@ impl DListXor { head_node.xored = new_ptr_u64 ^ second_ptr; head_ptr.put(Tracked(&mut head_perm), head_node); proof { - (self.perms.borrow_mut()) - .tracked_insert(0, head_perm); + self.perms.borrow_mut() + .tracked_insert(0, (head_perm, de)); assert forall |j: nat| 0 <= j < old(self)@.len() implies self.perms@.dom().contains(j) by { assert(old(self).wf_perm(j)); } - (self.perms.borrow_mut()).tracked_map_keys_in_place( + self.perms.borrow_mut().tracked_map_keys_in_place( Map::::new( |j: nat| 1 <= j <= old(self)@.len(), |j: nat| (j - 1) as nat, ) ); - (self.perms.borrow_mut()) - .tracked_insert(0, (perm).get()); + self.perms.borrow_mut() + .tracked_insert(0, (perm, dealloc)); self.ptrs@ = seq![ptr].add(self.ptrs@); } self.head = new_ptr_u64; @@ -522,9 +522,9 @@ impl DListXor { // self.prev_of(i) ^ self.next_of(i) //)); - assert(self.perms@.index(1)@.value.get_Some_0().xored == new_ptr_u64 ^ second_ptr); - assert(self.perms@.index(0)@.value.get_Some_0().xored == head_ptr_u64); - assert(self.perms@.index(1)@.pptr == head_ptr_u64 as int); + assert(self.perms@.index(1).0@.value.get_Some_0().xored == new_ptr_u64 ^ second_ptr); + assert(self.perms@.index(0).0@.value.get_Some_0().xored == head_ptr_u64); + assert(self.perms@.index(1).0@.pptr == head_ptr_u64 as int); assert(self.wf_perm(1)); assert(self.wf_perm(0)); diff --git a/source/rust_verify/example/rfmig_script.rs b/source/rust_verify/example/rfmig_script.rs index 7e8e6dd6d6..381422f972 100644 --- a/source/rust_verify/example/rfmig_script.rs +++ b/source/rust_verify/example/rfmig_script.rs @@ -210,7 +210,7 @@ fn start_thread(counter: PPtr, Tracked(perm): Tracked>) requires counter.id() == perm@.pptr, perm@.value === None, { - send_pointer(counter.clone()); + send_pointer(counter); let tracked mut perm: PointsTo = perm; diff --git a/source/rust_verify/example/state_machines/tutorial/rc.rs b/source/rust_verify/example/state_machines/tutorial/rc.rs index 1d0e0063b0..6d473baa8b 100644 --- a/source/rust_verify/example/state_machines/tutorial/rc.rs +++ b/source/rust_verify/example/state_machines/tutorial/rc.rs @@ -198,13 +198,15 @@ struct InnerRc { pub s: S, } +type MemPerms = (ptr::PointsTo>, ptr::Dealloc>); + tracked struct GhostStuff { pub tracked rc_perm: cell::PointsTo, - pub tracked rc_token: RefCounter::counter>>, + pub tracked rc_token: RefCounter::counter>, } impl GhostStuff { - pub open spec fn wf(self, inst: RefCounter::Instance>>, cell: PCell) -> bool { + pub open spec fn wf(self, inst: RefCounter::Instance>, cell: PCell) -> bool { &&& self.rc_perm@.pcell == cell.id() &&& self.rc_token@.instance == inst &&& self.rc_perm@.value.is_Some() @@ -220,9 +222,9 @@ impl InnerRc { struct_with_invariants!{ struct MyRc { - pub inst: Tracked< RefCounter::Instance>> >, + pub inst: Tracked< RefCounter::Instance> >, pub inv: Tracked< Duplicable, _>> >, - pub reader: Tracked< RefCounter::reader>> >, + pub reader: Tracked< RefCounter::reader> >, pub ptr: PPtr>, @@ -231,12 +233,14 @@ struct_with_invariants!{ spec fn wf(self) -> bool { predicate { - &&& self.reader@@.key@.pptr == self.ptr.id() + &&& self.reader@@.key.0@.pptr == self.ptr.id() + &&& self.reader@@.key.1@.pptr == self.ptr.id() + &&& self.reader@@.instance == self.inst@ &&& self.reader@@.count == 1 - &&& self.reader@@.key@.value.is_Some() + &&& self.reader@@.key.0@.value.is_Some() &&& self.inv@.wf() - &&& self.reader@@.key@.value.get_Some_0().rc_cell == self.rc_cell + &&& self.reader@@.key.0@.value.get_Some_0().rc_cell == self.rc_cell } invariant on inv with (inst, rc_cell) @@ -250,7 +254,7 @@ struct_with_invariants!{ impl MyRc { spec fn view(self) -> S { - self.reader@@.key@.value.get_Some_0().s + self.reader@@.key.0@.value.get_Some_0().s } fn new(s: S) -> (rc: Self) @@ -258,34 +262,20 @@ impl MyRc { rc.wf(), rc@ == s, { - let (rc_cell, Tracked(rc_perm)) = PCell::new(1); let inner_rc = InnerRc:: { rc_cell, s }; - let (ptr, Tracked(ptr_perm)) = PPtr::new(inner_rc); + let (ptr, Tracked(ptr_perm), Tracked(dealloc_perm)) = PPtr::new(inner_rc); - let tracked inst; - let tracked reader; - let tracked inv; - let tracked g; - proof { - let tracked (Tracked(inst0), Tracked(mut rc_token), _) = RefCounter::Instance::initialize_empty(Option::None); - inst = inst0; + let tracked (Tracked(inst), Tracked(mut rc_token), _) = RefCounter::Instance::initialize_empty(Option::None); + let tracked reader = inst.do_deposit((ptr_perm, dealloc_perm), &mut rc_token, (ptr_perm, dealloc_perm)); + let tracked g = GhostStuff:: { rc_perm, rc_token }; - let tracked reader0 = inst.do_deposit(ptr_perm, &mut rc_token, ptr_perm); - g = GhostStuff:: { rc_perm, rc_token }; - reader = reader0; - } let tr_inst = Tracked(inst); let gh_cell = Ghost(rc_cell); - proof { - let tracked inv0 = LocalInvariant::new( - (tr_inst, gh_cell), g, 0); - let tracked inv0 = Duplicable::new(inv0); - - inv = inv0; - } + let tracked inv = LocalInvariant::new((tr_inst, gh_cell), g, 0); + let tracked inv = Duplicable::new(inv); MyRc { inst: tr_inst, inv: Tracked(inv), reader: Tracked(reader), @@ -301,7 +291,7 @@ impl MyRc { let tracked inst = self.inst.borrow(); let tracked reader = self.reader.borrow(); let tracked perm = inst.reader_guard(reader@.key, &reader); - &self.ptr.borrow(Tracked(perm)).s + &self.ptr.borrow(Tracked(&perm.0)).s } fn clone(&self) -> (s: Self) @@ -312,7 +302,7 @@ impl MyRc { let tracked reader = self.reader.borrow(); let tracked perm = inst.reader_guard(reader@.key, &reader); - let inner_rc_ref = self.ptr.borrow(Tracked(perm)); + let inner_rc_ref = self.ptr.borrow(Tracked(&perm.0)); let tracked new_reader; open_local_invariant!(self.inv.borrow().borrow() => g => { @@ -339,7 +329,7 @@ impl MyRc { inst: Tracked(self.inst.borrow().clone()), inv: Tracked(self.inv.borrow().clone()), reader: Tracked(new_reader), - ptr: self.ptr.clone(), + ptr: self.ptr, rc_cell: Ghost(self.rc_cell@), } } @@ -353,7 +343,7 @@ impl MyRc { reader@.key, &reader); - let inner_rc_ref = &ptr.borrow(Tracked(perm)); + let inner_rc_ref = &ptr.borrow(Tracked(&perm.0)); open_local_invariant!(inv.borrow() => g => { let tracked GhostStuff { rc_perm: mut rc_perm, rc_token: mut rc_token } = g; @@ -370,7 +360,7 @@ impl MyRc { reader); } } else { - let tracked mut inner_rc_perm = inst.dec_to_zero( + let tracked (mut inner_rc_perm, inner_rc_dealloc) = inst.dec_to_zero( reader.view().key, &mut rc_token, reader); @@ -383,7 +373,7 @@ impl MyRc { let count = count - 1; inner_rc.rc_cell.put(Tracked(&mut rc_perm), count); - ptr.dispose(Tracked(inner_rc_perm)); + ptr.dispose(Tracked(inner_rc_perm), Tracked(inner_rc_dealloc)); } proof { g = GhostStuff { rc_perm, rc_token }; } diff --git a/source/rust_verify/example/verified_vec.rs b/source/rust_verify/example/verified_vec.rs new file mode 100644 index 0000000000..bcb4a95568 --- /dev/null +++ b/source/rust_verify/example/verified_vec.rs @@ -0,0 +1,187 @@ +// rust_verify/tests/example.rs +#![allow(unused_imports)] + +use builtin::*; +use builtin_macros::*; +use vstd::*; +use vstd::modes::*; +use vstd::ptr::*; +use vstd::prelude::*; +use vstd::layout::*; + +verus!{ + +struct Vector { + pub ptr: PPtr, + pub len: usize, + pub capacity: usize, + + pub elems: Tracked>>, + pub rest: Tracked, + pub dealloc: Tracked, +} + +impl Vector { + pub closed spec fn well_formed(&self) -> bool { + &&& self.len <= self.capacity + &&& (forall |i: nat| 0 <= i < self.len ==> + self.elems@.dom().contains(i)) + &&& (forall |i: nat| 0 <= i < self.len ==> + (#[trigger] self.elems@.index(i))@.pptr + == self.ptr.id() + i as int * size_of::()) + &&& (forall |i: nat| 0 <= i < self.len ==> + (#[trigger] self.elems@.index(i))@.value.is_Some()) + &&& self.rest@.is_range( + self.ptr.id() + self.len * size_of::(), + (self.capacity - self.len) * size_of::()) + &&& self.dealloc@@.pptr == self.ptr.id() + &&& self.dealloc@@.size == self.capacity * size_of::() + &&& self.dealloc@@.align == align_of::() + &&& is_sized::() + } + + pub closed spec fn view(&self) -> Seq { + Seq::new( + self.len as nat, + |i: int| self.elems@.index(i as nat)@.value.get_Some_0(), + ) + } + + pub fn empty() -> (vec: Self) + requires is_sized::(), + ensures vec.well_formed(), + { + layout_for_type_is_valid::(); + let (p, Tracked(points_to), Tracked(dealloc)) = + PPtr::::alloc(0, std::mem::align_of::()); + + Vector { + ptr: p, + len: 0, + capacity: 0, + elems: Tracked(Map::tracked_empty()), + rest: Tracked(points_to), + dealloc: Tracked(dealloc), + } + } + + pub fn index(&self, i: usize) -> (elem: &V) + requires + self.well_formed(), + 0 <= i < self@.len(), + ensures + *elem === self@.index(i as int), + { + let ptr_usize = self.ptr.to_usize(); + + assume( + (i as int * size_of::()) as usize as int + == (i as int * size_of::())); + assume( + (ptr_usize as int + i as int * size_of::()) as usize as int + == (ptr_usize as int + i as int * size_of::())); + + let elem_ptr_usize = ptr_usize + i * std::mem::size_of::(); + let elem_ptr = PPtr::::from_usize(elem_ptr_usize); + + let tracked perm = self.elems.borrow().tracked_borrow(i as nat); + + elem_ptr.borrow(Tracked(perm)) + } + + pub fn resize(&mut self, new_capacity: usize) + requires + old(self).well_formed(), + old(self).len <= new_capacity, + ensures + self.well_formed(), + old(self)@ === self@, + self.capacity === new_capacity, + { + // TODO implement + assume(false); + } + + pub fn push(&mut self, v: V) + requires + old(self).well_formed(), + ensures + self@ === old(self)@.push(v) + { + if self.len == self.capacity { + assume((self.capacity as int * 2) as usize as int + == (self.capacity as int * 2)); + let new_cap = if self.capacity == 0 { 2 } else { self.capacity * 2 }; + self.resize(new_cap); + + assert((if self.capacity == 0 { 2 } else { self.capacity * 2 }) > self.capacity) by (nonlinear_arith); + assert(new_cap > old(self).capacity); + assert(self@.len() == old(self)@.len()); + assert(self.len == old(self).len); + assert(self.len < self.capacity); + } + assert(self.len < self.capacity); + + let tracked mut points_to; + proof { + let tracked mut rest = PointsToRaw::empty(); + tracked_swap(&mut rest, self.rest.borrow_mut()); + + assert(size_of::() as int <= + (self.capacity - self.len) * size_of::()) + by { + assert((self.capacity - self.len) >= 1 + ==> + size_of::() as int <= (self.capacity - self.len) * size_of::()) + by(nonlinear_arith); + } + + assert(rest.is_range( + self.ptr.id() + self.len * size_of::(), + (self.capacity - self.len) * size_of::())); + assert(rest@.dom() == crate::set_lib::set_int_range( + self.ptr.id() + self.len * size_of::(), + self.ptr.id() + self.len * size_of::() + (self.capacity - self.len) * size_of::())); + let item_range = crate::set_lib::set_int_range( + self.ptr.id() + self.len * size_of::(), + self.ptr.id() + self.len * size_of::() + size_of::() as int); + + assert(item_range.subset_of(rest@.dom())); + + let tracked (points_to_raw, mut rest) = rest.split(item_range); + assume((self.ptr.id() + self.len * size_of::()) % align_of::() as int == 0); + points_to = points_to_raw.into_typed::(self.ptr.id() + self.len * size_of::()); + + tracked_swap(&mut rest, self.rest.borrow_mut()); + } + + let i = self.len; + let ptr_usize = self.ptr.to_usize(); + + assume( + (i as int * size_of::()) as usize as int + == (i as int * size_of::())); + assume( + (ptr_usize as int + i as int * size_of::()) as usize as int + == (ptr_usize as int + i as int * size_of::())); + + let elem_ptr_usize = ptr_usize + i * std::mem::size_of::(); + let elem_ptr = PPtr::::from_usize(elem_ptr_usize); + + elem_ptr.put(Tracked(&mut points_to), v); + + proof { + self.elems.borrow_mut().tracked_insert(self.len as nat, points_to); + } + + self.len = self.len + 1; + + proof { + assert_seqs_equal!(self@, old(self)@.push(v)); + } + } +} + +fn main() { } + +} diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 42febe56a6..8ad5cb3dc0 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -112,7 +112,6 @@ pub fn enable_default_features_and_verus_attr( "unboxed_closures", "register_tool", "tuple_trait", - "allocator_api", "custom_inner_attributes", ] { rustc_args.push("-Z".to_string()); diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index 8849b2ad5f..7e3410011a 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -14,6 +14,7 @@ use crate::rust_to_vir_base::{ typ_path_and_ident_to_vir_path, }; use crate::rust_to_vir_func::{check_foreign_item_fn, check_item_fn, CheckItemFnEither}; +use crate::rust_to_vir_global::TypIgnoreImplPaths; use crate::util::{err_span, unsupported_err_span}; use crate::verus_items::{self, BuiltinTraitItem, MarkerItem, RustItem, VerusItem}; use crate::{err_unless, unsupported_err, unsupported_err_unless}; @@ -744,11 +745,17 @@ pub fn crate_to_vir<'tcx>(ctxt: &mut Context<'tcx>) -> Result { } } } + + let mut typs_sizes_set: HashMap = HashMap::new(); for (_, owner_opt) in ctxt.krate.owners.iter_enumerated() { if let MaybeOwner::Owner(owner) = owner_opt { match owner.node() { OwnerNode::Item(item) => { - crate::rust_to_vir_global::process_const_early(ctxt, item)?; + crate::rust_to_vir_global::process_const_early( + ctxt, + &mut typs_sizes_set, + item, + )?; } _ => (), } diff --git a/source/rust_verify/src/rust_to_vir_global.rs b/source/rust_verify/src/rust_to_vir_global.rs index 6ce7849ecc..0dcbdcc7f5 100644 --- a/source/rust_verify/src/rust_to_vir_global.rs +++ b/source/rust_verify/src/rust_to_vir_global.rs @@ -1,15 +1,27 @@ use std::sync::Arc; use rustc_hir::{Item, ItemKind}; -use vir::ast::{IntRange, VirErr}; +use vir::ast::{IntRange, Typ, TypX, VirErr}; use crate::{ attributes::get_verifier_attrs, context::Context, unsupported_err_unless, verus_items::VerusItem, }; +#[derive(Debug, Hash)] +pub(crate) struct TypIgnoreImplPaths(pub Typ); + +impl PartialEq for TypIgnoreImplPaths { + fn eq(&self, other: &Self) -> bool { + vir::ast_util::types_equal(&self.0, &other.0) + } +} + +impl Eq for TypIgnoreImplPaths {} + pub(crate) fn process_const_early<'tcx>( ctxt: &mut Context<'tcx>, + typs_sizes_set: &mut std::collections::HashMap, item: &Item<'tcx>, ) -> Result<(), VirErr> { let attrs = ctxt.tcx.hir().attrs(item.hir_id()); @@ -33,7 +45,7 @@ pub(crate) fn process_const_early<'tcx>( let rustc_hir::ExprKind::Block(block, _) = body.value.kind else { return err; }; - if block.stmts.len() != 1 { + if block.stmts.len() < 1 { return err; } let rustc_hir::StmtKind::Semi(expr) = block.stmts[0].kind else { @@ -73,28 +85,45 @@ pub(crate) fn process_const_early<'tcx>( return err; }; - match &*ty { - vir::ast::TypX::Int(IntRange::USize) => { - let arch_word_bits = &mut Arc::make_mut(ctxt).arch_word_bits; - if arch_word_bits.is_some() { + vir::layout::layout_of_typ_supported(&ty, &crate::spans::err_air_span(item.span))?; + + match typs_sizes_set.entry(TypIgnoreImplPaths(ty.clone())) { + std::collections::hash_map::Entry::Occupied(_occ) => { + return crate::util::err_span( + item.span, + format!( + "the size of `{}` can only be set once per crate", + vir::ast_util::typ_to_diagnostic_str(&ty) + ), + ); + } + std::collections::hash_map::Entry::Vacant(vac) => { + vac.insert(size); + } + } + + if let TypX::Int(IntRange::USize | IntRange::ISize) = &*ty { + let arch_word_bits = &mut Arc::make_mut(ctxt).arch_word_bits; + if let Some(arch_word_bits) = arch_word_bits { + let vir::ast::ArchWordBits::Exactly(size_bits_set) = arch_word_bits else { + panic!("unexpected ArchWordBits"); + }; + if (size * 8) as u32 != *size_bits_set { return crate::util::err_span( item.span, - "the size of usize can only be set once per crate", + format!("usize or isize have already been set to {} bits", *size_bits_set), ); } - *arch_word_bits = Some(match size { - 4 | 8 => vir::ast::ArchWordBits::Exactly((size as u32) * 8), - _ => { - return crate::util::err_span( - item.span, - "usize can be either 32 or 64 bits", - ); - } - }); - } - _ => { - return crate::util::err_span(item.span, "only usize is currently supported here"); } + *arch_word_bits = Some(match size { + 4 | 8 => vir::ast::ArchWordBits::Exactly((size * 8) as u32), + _ => { + return crate::util::err_span( + item.span, + "usize and isize can be either 32 or 64 bits", + ); + } + }); } } Ok(()) diff --git a/source/rust_verify_test/tests/bitvector.rs b/source/rust_verify_test/tests/bitvector.rs index b513ff7031..f43a9279c1 100644 --- a/source/rust_verify_test/tests/bitvector.rs +++ b/source/rust_verify_test/tests/bitvector.rs @@ -294,8 +294,8 @@ test_verify_one_file! { } => Err(err) => assert_fails(err, 4) } -test_verify_one_file! { - #[test] bit_vector_usize_as_32bit verus_code! { +test_verify_one_file_with_options! { + #[test] bit_vector_usize_as_32bit ["vstd"] => verus_code! { global size_of usize == 4; proof fn test1(x: usize) { @@ -329,8 +329,8 @@ test_verify_one_file! { } => Err(err) => assert_fails(err, 4) } -test_verify_one_file! { - #[test] bit_vector_usize_as_64bit verus_code! { +test_verify_one_file_with_options! { + #[test] bit_vector_usize_as_64bit ["vstd"] => verus_code! { global size_of usize == 8; proof fn test1(x: usize) { diff --git a/source/rust_verify_test/tests/cell_lib.rs b/source/rust_verify_test/tests/cell_lib.rs index 432794ac4e..9db34027b0 100644 --- a/source/rust_verify_test/tests/cell_lib.rs +++ b/source/rust_verify_test/tests/cell_lib.rs @@ -54,7 +54,7 @@ test_verify_one_file! { } const PTR_TEST: &str = code_str! { - let (ptr, Tracked(mut token)) = PPtr::::empty(); + let (ptr, Tracked(mut token), Tracked(dealloc)) = PPtr::::empty(); assert(equal(token.view().pptr, ptr.id())); assert(equal(token.view().value, Option::None)); @@ -75,7 +75,7 @@ const PTR_TEST: &str = code_str! { assert(equal(token.view().value, Option::None)); assert(equal(x, 7)); - ptr.dispose(Tracked(token)); + ptr.dispose(Tracked(token), Tracked(dealloc)); }; test_verify_one_file! { @@ -172,8 +172,8 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_mismatch_put IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); - let (ptr2, Tracked(mut token2)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); + let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::::empty(); ptr1.put(Tracked(&mut token2), 5); // FAILS } } => Err(err) => assert_one_fails(err) @@ -182,8 +182,8 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_mismatch_take IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); - let (ptr2, Tracked(mut token2)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::::empty(); + let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::::empty(); ptr1.put(Tracked(&mut token1), 5); ptr2.put(Tracked(&mut token2), 5); let x = ptr1.take(Tracked(&mut token2)); // FAILS @@ -194,8 +194,8 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_mismatch_replace IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); - let (ptr2, Tracked(mut token2)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); + let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::::empty(); ptr1.put(Tracked(&mut token1), 5); ptr2.put(Tracked(&mut token2), 5); let x = ptr1.replace(Tracked(&mut token2), 7); // FAILS @@ -206,8 +206,8 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_mismatch_borrow IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); - let (ptr2, Tracked(mut token2)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); + let (ptr2, Tracked(mut token2), Tracked(dealloc)) = PPtr::::empty(); ptr1.put(Tracked(&mut token1), 5); ptr2.put(Tracked(&mut token2), 5); let x = ptr1.borrow(Tracked(&token2)); // FAILS @@ -218,9 +218,19 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_mismatch_dispose IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); - let (ptr2, Tracked(mut token2)) = PPtr::::empty(); - ptr1.dispose(Tracked(token2)); // FAILS + let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::::empty(); + let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::::empty(); + ptr1.dispose(Tracked(token2), Tracked(dealloc1)); // FAILS + } + } => Err(err) => assert_one_fails(err) +} + +test_verify_one_file! { + #[test] ptr_mismatch_dispose2 IMPORTS.to_string() + verus_code_str! { + pub fn f() { + let (ptr1, Tracked(mut token1), Tracked(dealloc1)) = PPtr::::empty(); + let (ptr2, Tracked(mut token2), Tracked(dealloc2)) = PPtr::::empty(); + ptr1.dispose(Tracked(token1), Tracked(dealloc2)); // FAILS } } => Err(err) => assert_one_fails(err) } @@ -228,7 +238,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_some_put IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); ptr1.put(Tracked(&mut token1), 7); ptr1.put(Tracked(&mut token1), 5); // FAILS } @@ -238,7 +248,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_none_take IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); let x = ptr1.take(Tracked(&mut token1)); // FAILS } } => Err(err) => assert_one_fails(err) @@ -247,7 +257,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_none_replace IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); let x = ptr1.replace(Tracked(&mut token1), 7); // FAILS } } => Err(err) => assert_one_fails(err) @@ -256,7 +266,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_none_borrow IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); let x = ptr1.borrow(Tracked(&token1)); // FAILS } } => Err(err) => assert_one_fails(err) @@ -265,9 +275,9 @@ test_verify_one_file! { test_verify_one_file! { #[test] ptr_some_dispose IMPORTS.to_string() + verus_code_str! { pub fn f() { - let (ptr1, Tracked(mut token1)) = PPtr::::empty(); + let (ptr1, Tracked(mut token1), Tracked(dealloc)) = PPtr::::empty(); ptr1.put(Tracked(&mut token1), 5); - ptr1.dispose(Tracked(token1)); // FAILS + ptr1.dispose(Tracked(token1), Tracked(dealloc)); // FAILS } } => Err(err) => assert_one_fails(err) } diff --git a/source/rust_verify_test/tests/arch_word_bits.rs b/source/rust_verify_test/tests/layout.rs similarity index 58% rename from source/rust_verify_test/tests/arch_word_bits.rs rename to source/rust_verify_test/tests/layout.rs index 122a13b472..a36073b2a5 100644 --- a/source/rust_verify_test/tests/arch_word_bits.rs +++ b/source/rust_verify_test/tests/layout.rs @@ -120,8 +120,8 @@ test_verify_one_file! { } => Err(err) => assert_fails(err, 5) } -test_verify_one_file! { - #[test] test_set_to_32 verus_code! { +test_verify_one_file_with_options! { + #[test] test_set_to_32 ["vstd"] => verus_code! { global size_of usize == 4; fn test1() { // ARCH-WORD-BITS-32 @@ -145,8 +145,8 @@ test_verify_one_file! { } => Err(err) => assert_fails(err, 1) } -test_verify_one_file! { - #[test] test_set_to_64 verus_code! { +test_verify_one_file_with_options! { + #[test] test_set_to_64 ["vstd"] => verus_code! { global size_of usize == 8; fn test1() { // ARCH-WORD-BITS-64 @@ -170,25 +170,48 @@ test_verify_one_file! { } => Err(err) => assert_fails(err, 1) } -test_verify_one_file! { - #[test] test_set_to_both_fail_1 verus_code! { +test_verify_one_file_with_options! { + #[test] test_set_to_both_fail_1 ["vstd"] => verus_code! { global size_of usize == 8; global size_of usize == 4; - } => Err(err) => assert_vir_error_msg(err, "the size of usize can only be set once per crate") + } => Err(err) => assert_rust_error_msg(err, "the name `VERUS_layout_of_usize` is defined multiple times") } -test_verify_one_file! { - #[test] test_set_to_both_fail_2 verus_code! { +test_verify_one_file_with_options! { + #[test] test_set_to_both_fail_2 ["vstd"] => verus_code! { global size_of usize == 8; mod m3 { global size_of usize == 4; } - } => Err(err) => assert_vir_error_msg(err, "the size of usize can only be set once per crate") + } => Err(err) => assert_vir_error_msg(err, "the size of `usize` can only be set once per crate") +} + +test_verify_one_file_with_options! { + #[test] test_set_both_usize_isize_pass ["vstd"] => verus_code! { + global size_of usize == 8; + global size_of isize == 8; + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] test_set_both_usize_isize_fail_1 ["vstd"] => verus_code! { + global size_of usize == 4; + global size_of isize == 8; + } => Err(err) => assert_vir_error_msg(err, "usize or isize have already been set to 32 bits") +} + +test_verify_one_file_with_options! { + #[test] test_set_both_usize_isize_fail_2 ["vstd"] => verus_code! { + global size_of usize == 8; + mod m3 { + global size_of isize == 4; + } + } => Err(err) => assert_vir_error_msg(err, "usize or isize have already been set to 64 bits") } #[cfg(target_pointer_width = "64")] test_verify_one_file_with_options! { - #[test] test_set_to_32_on_64_bit_compile ["--compile"] => verus_code! { + #[test] test_set_to_32_on_64_bit_compile ["vstd", "--compile"] => verus_code! { global size_of usize == 4; } => Err(err) => { assert_rust_error_msg(err.clone(), "evaluation of constant value failed"); @@ -198,14 +221,14 @@ test_verify_one_file_with_options! { #[cfg(target_pointer_width = "64")] test_verify_one_file_with_options! { - #[test] test_set_to_64_on_64_bit_compile ["--compile"] => verus_code! { + #[test] test_set_to_64_on_64_bit_compile ["vstd", "--compile"] => verus_code! { global size_of usize == 8; } => Ok(()) } #[cfg(target_pointer_width = "32")] test_verify_one_file_with_options! { - #[test] test_set_to_64_on_32_bit_compile ["--compile"] => verus_code! { + #[test] test_set_to_64_on_32_bit_compile ["vstd", "--compile"] => verus_code! { global size_of usize == 8; } => Err(err) => { assert_rust_error_msg(err.clone(), "evaluation of constant value failed"); @@ -215,7 +238,7 @@ test_verify_one_file_with_options! { #[cfg(target_pointer_width = "32")] test_verify_one_file_with_options! { - #[test] test_set_to_32_on_32_bit_compile ["--compile"] => verus_code! { + #[test] test_set_to_32_on_32_bit_compile ["vstd", "--compile"] => verus_code! { global size_of usize == 4; } => Ok(()) } @@ -253,3 +276,144 @@ test_verify_one_file! { } } => Err(err) => assert_vir_error_msg(err, "expression has mode spec, expected mode exec") } + +test_verify_one_file_with_options! { + #[test] test_size_of_1 ["vstd"] => verus_code! { + global size_of usize == 8; + global size_of isize == 8; + + fn test() { + assert(core::mem::size_of::() == 8); + assert(core::mem::size_of::() != 4); + assert(core::mem::size_of::() == 8); + assert(core::mem::size_of::() != 4); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] test_size_of_2 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: u64 } + + global size_of S == 8; + + fn test() { + assert(core::mem::size_of::() == 8); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] test_size_of_3 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: V } + + global size_of S == 8; + + fn test() { + assert(core::mem::size_of::>() == 8); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] test_size_of_4 ["vstd", "--compile"] => verus_code! { + trait T { + type X; + } + + struct U {} + + impl T for U { + type X = u64; + } + + #[repr(C)] + struct S { v: V::X } + + global size_of S == 8; + + fn test() { + assert(core::mem::size_of::>() == 8); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] test_layout_1 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: u64 } + + global layout S is size == 8, align == 8; + + fn test() { + assert(core::mem::size_of::() == 8); + assert(core::mem::align_of::() == 8); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] test_layout_2 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: u64 } + + global layout S is size == 8; + + fn test() { + assert(core::mem::size_of::() == 8); + assert(core::mem::align_of::() == 8); // FAILS + } + } => Err(err) => assert_one_fails(err) +} + +test_verify_one_file_with_options! { + #[test] test_layout_3 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: u64, z: u32 } + + global layout S is size == 16, align == 8; + + fn test() { + assert(core::mem::size_of::() == 16); + assert(core::mem::size_of::() != 8); + assert(core::mem::align_of::() == 8); + assert(core::mem::align_of::() != 16); + } + } => Ok(()) +} + +test_verify_one_file_with_options! { + #[test] test_layout_4 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: u64, z: u32 } + + global layout S is size == 16, align == 16; + } => Err(err) => { + assert_rust_error_msg(err.clone(), "evaluation of constant value failed"); + assert!(err.errors[0].rendered.contains("does not have the expected alignment")); + } +} + +test_verify_one_file_with_options! { + #[test] test_layout_5 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: u64, z: u32 } + + global layout S is size == 8, align == 8; + } => Err(err) => { + assert_rust_error_msg(err.clone(), "evaluation of constant value failed"); + assert!(err.errors[0].rendered.contains("does not have the expected size")); + } +} + +test_verify_one_file_with_options! { + #[test] test_layout_6 ["vstd", "--compile"] => verus_code! { + #[repr(C)] + struct S { v: V, z: V } + + global layout S is size == 16, align == 8; + global layout S is size == 8, align == 4; + } => Ok(()) +} diff --git a/source/rust_verify_test/tests/lifetime.rs b/source/rust_verify_test/tests/lifetime.rs index dfcb367df2..63a2b05662 100644 --- a/source/rust_verify_test/tests/lifetime.rs +++ b/source/rust_verify_test/tests/lifetime.rs @@ -561,7 +561,7 @@ test_verify_one_file! { #[test] tracked_new_issue870 verus_code! { use vstd::ptr::*; fn test() { - let (pptr, Tracked(perm)) = PPtr::::empty(); + let (pptr, Tracked(perm), Tracked(dealloc)) = PPtr::::empty(); pptr.put(Tracked(&mut perm), 5); let x: &u64 = pptr.borrow(Tracked(&perm)); // should tie x's lifetime to the perm borrow assert(x == 5); @@ -575,11 +575,11 @@ test_verify_one_file! { #[test] tracked_new2_issue870 verus_code! { use vstd::ptr::*; fn test() { - let (pptr, Tracked(perm)) = PPtr::::empty(); + let (pptr, Tracked(perm), Tracked(dealloc)) = PPtr::::empty(); pptr.put(Tracked(&mut perm), 5); let x: &u64 = pptr.borrow(Tracked(&perm)); // should tie x's lifetime to the perm borrow assert(x == 5); - pptr.dispose(Tracked(perm)); + pptr.dispose(Tracked(perm), Tracked(dealloc)); let z: u64 = *x; // but x is still available here } } => Err(err) => assert_vir_error_msg(err, "cannot move out of `perm` because it is borrowed") diff --git a/source/rust_verify_test/tests/overflow.rs b/source/rust_verify_test/tests/overflow.rs index f3893f9b2f..bba92906c2 100644 --- a/source/rust_verify_test/tests/overflow.rs +++ b/source/rust_verify_test/tests/overflow.rs @@ -238,8 +238,8 @@ test_verify_one_file! { } => Err(e) => assert_vir_error_msg(e, "possible bit shift underflow/overflow") } -test_verify_one_file! { - #[test] bit_shift_overflow_arch32 verus_code! { +test_verify_one_file_with_options! { + #[test] bit_shift_overflow_arch32 ["vstd"] => verus_code! { global size_of usize == 4; fn test_usize_overflow() { @@ -258,8 +258,8 @@ test_verify_one_file! { } => Err(e) => assert_fails(e, 1) } -test_verify_one_file! { - #[test] bit_shift_overflow_arch64 verus_code! { +test_verify_one_file_with_options! { + #[test] bit_shift_overflow_arch64 ["vstd"] => verus_code! { global size_of usize == 8; fn test_usize_overflow() { diff --git a/source/rust_verify_test/tests/size_of.rs b/source/rust_verify_test/tests/size_of.rs new file mode 100644 index 0000000000..ee367abfaf --- /dev/null +++ b/source/rust_verify_test/tests/size_of.rs @@ -0,0 +1,85 @@ +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; + +// See https://doc.rust-lang.org/std/mem/fn.size_of.html +// for stable guarantees about the size of Rust types + +test_verify_one_file! { + #[test] sizeof_test verus_code! { + use vstd::layout::*; + use std::sync::Arc; + use std::rc::Rc; + + // this size of a pointer/reference should be the same as usize ONLY + // for sized types V + + fn test_unsized_wrong() { + assert(size_of::<&V>() == size_of::()); // FAILS + } + + fn test_unsized_wrong2() { + assert(size_of::<&[u8]>() == size_of::()); // FAILS + } + + // (&mut not supported right now) + //fn test_unsized_wrong3() { + // assert(size_of::<&mut V>() == size_of::()); // FAILS + //} + + //fn test_unsized_wrong4() { + // assert(size_of::<&mut [u8]>() == size_of::()); // FAILS + //} + + fn test_unsized_wrong5() { + assert(size_of::>() == size_of::()); // FAILS + } + + fn test_unsized_wrong6() { + assert(size_of::>() == size_of::()); // FAILS + } + + // I don't think Rust guarantees this, so this should fail. + + fn test_tuple_wrong() { + assert(size_of::<(A, B)>() == size_of::() + size_of::()); // FAILS + } + + // &A and A need to be distinguished + + fn test_ref_distinguished() { + assert(size_of::() == size_of::<&A>()); // FAILS + } + + //fn test_mut_ref_distinguished() { + // assert(size_of::() == size_of::<&mut A>()); // FAILS + //} + + fn test_box_distinguished() { + assert(size_of::() == size_of::>()); // FAILS + } + + fn test_rc_distinguished() { + assert(size_of::() == size_of::>()); // FAILS + } + + fn test_arc_distinguished() { + assert(size_of::() == size_of::>()); // FAILS + } + + // See the explanation in pervasive/layout.rs for why we don't make this assumption. + + fn test_not_assumed_bounded() { + assert(size_of::() as usize as int == size_of::()); // FAILS + } + + fn test_not_assumed_bounded_align() { + assert(align_of::() as usize as int == align_of::()); // FAILS + } + + fn test_not_assumed_nonzero() { + assert(size_of::() != 0); // FAILS + } + } => Err(err) => assert_fails(err, 12) +} diff --git a/source/tools/docs.sh b/source/tools/docs.sh index 2a079e6ec9..2eb298d8ee 100755 --- a/source/tools/docs.sh +++ b/source/tools/docs.sh @@ -36,7 +36,6 @@ RUSTC_BOOTSTRAP=1 eval ""VERUSDOC=1 VERUS_Z3_PATH="$(pwd)/z3" rustdoc \ -Zcrate-attr=feature\\\(register_tool\\\) \ -Zcrate-attr=feature\\\(rustc_attrs\\\) \ -Zcrate-attr=feature\\\(unboxed_closures\\\) \ - -Zcrate-attr=feature\\\(allocator_api\\\) \ -Zcrate-attr=register_tool\\\(verus\\\) \ -Zcrate-attr=register_tool\\\(verifier\\\) \ pervasive/vstd.rs"" diff --git a/source/vir/src/layout.rs b/source/vir/src/layout.rs new file mode 100644 index 0000000000..80821fc2d5 --- /dev/null +++ b/source/vir/src/layout.rs @@ -0,0 +1,42 @@ +use crate::{ + ast::{Typ, TypDecoration, VirErr}, + ast_visitor::map_typ_visitor, + messages::{error, Span}, +}; + +pub fn layout_of_typ_supported(typ: &Typ, span: &Span) -> Result<(), VirErr> { + let _ = map_typ_visitor(typ, &|typ| match &**typ { + crate::ast::TypX::Bool + | crate::ast::TypX::Int(_) + | crate::ast::TypX::Tuple(_) + | crate::ast::TypX::Datatype(_, _, _) + | crate::ast::TypX::Decorate( + TypDecoration::Ref + | TypDecoration::Rc + | TypDecoration::Arc + | TypDecoration::Box + | TypDecoration::Tracked + | TypDecoration::Ghost + | TypDecoration::Never, + _, + ) + | crate::ast::TypX::Boxed(_) + | crate::ast::TypX::ConstInt(_) + | crate::ast::TypX::Char + | crate::ast::TypX::Primitive(_, _) => Ok(typ.clone()), + + crate::ast::TypX::Lambda(_, _) + | crate::ast::TypX::AnonymousClosure(_, _, _) + | crate::ast::TypX::Decorate(_, _) + | crate::ast::TypX::TypParam(_) + | crate::ast::TypX::Projection { .. } + | crate::ast::TypX::StrSlice => { + return Err(error(span, "this type is not supported in global size_of / align_of")); + } + + crate::ast::TypX::Air(_) | crate::ast::TypX::TypeId => { + unreachable!() + } + })?; + Ok(()) +} diff --git a/source/vir/src/lib.rs b/source/vir/src/lib.rs index 910400073d..9029b10890 100644 --- a/source/vir/src/lib.rs +++ b/source/vir/src/lib.rs @@ -44,6 +44,7 @@ pub mod func_to_air; pub mod headers; pub mod interpreter; mod inv_masks; +pub mod layout; pub mod messages; pub mod modes; pub mod poly;