From 4c45266e67058f278d738ae72406856d56eb1630 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Tue, 25 Feb 2025 09:23:09 +0100 Subject: [PATCH] [wip] uninterp marker on uniterpreted spec fns --- dependencies/syn/src/gen/clone.rs | 9 ++++ dependencies/syn/src/gen/debug.rs | 13 +++++ dependencies/syn/src/gen/eq.rs | 11 ++++ dependencies/syn/src/gen/fold.rs | 14 +++++ dependencies/syn/src/gen/hash.rs | 13 ++++- dependencies/syn/src/gen/token.css | 7 +++ dependencies/syn/src/gen/visit.rs | 12 +++++ dependencies/syn/src/gen/visit_mut.rs | 12 +++++ dependencies/syn/src/lib.rs | 2 +- dependencies/syn/src/token.rs | 2 + dependencies/syn/src/verus.rs | 16 ++++++ dependencies/syn/syn.json | 17 ++++++ dependencies/syn/tests/debug/gen.rs | 18 +++++++ source/builtin_macros/src/rustdoc.rs | 1 + source/builtin_macros/src/syntax.rs | 4 +- source/rust_verify/src/attributes.rs | 26 ++++++--- source/rust_verify/src/rust_to_vir_func.rs | 25 ++++++--- source/rust_verify_test/tests/modules.rs | 63 +++++++++++++++++++--- source/vir/src/ast.rs | 10 +++- 19 files changed, 249 insertions(+), 26 deletions(-) diff --git a/dependencies/syn/src/gen/clone.rs b/dependencies/syn/src/gen/clone.rs index ec5dc82a50..675708e167 100644 --- a/dependencies/syn/src/gen/clone.rs +++ b/dependencies/syn/src/gen/clone.rs @@ -2237,6 +2237,7 @@ impl Clone for crate::Publish { crate::Publish::OpenRestricted(v0) => { crate::Publish::OpenRestricted(v0.clone()) } + crate::Publish::Uninterp(v0) => crate::Publish::Uninterp(v0.clone()), crate::Publish::Default => crate::Publish::Default, } } @@ -2770,6 +2771,14 @@ impl Clone for crate::UnOp { *self } } +#[cfg_attr(docsrs, doc(cfg(feature = "clone-impls")))] +impl Clone for crate::Uninterp { + fn clone(&self) -> Self { + crate::Uninterp { + token: self.token.clone(), + } + } +} #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "clone-impls")))] impl Clone for crate::UseGlob { diff --git a/dependencies/syn/src/gen/debug.rs b/dependencies/syn/src/gen/debug.rs index 06fe9e5aff..57d83fdb26 100644 --- a/dependencies/syn/src/gen/debug.rs +++ b/dependencies/syn/src/gen/debug.rs @@ -3186,6 +3186,11 @@ impl Debug for crate::Publish { formatter.field(v0); formatter.finish() } + crate::Publish::Uninterp(v0) => { + let mut formatter = formatter.debug_tuple("Uninterp"); + formatter.field(v0); + formatter.finish() + } crate::Publish::Default => formatter.write_str("Default"), } } @@ -3924,6 +3929,14 @@ impl Debug for crate::UnOp { } } } +#[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] +impl Debug for crate::Uninterp { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + let mut formatter = formatter.debug_struct("Uninterp"); + formatter.field("token", &self.token); + formatter.finish() + } +} #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] impl Debug for crate::UseGlob { diff --git a/dependencies/syn/src/gen/eq.rs b/dependencies/syn/src/gen/eq.rs index e5cb1da8f9..d62ff3aa09 100644 --- a/dependencies/syn/src/gen/eq.rs +++ b/dependencies/syn/src/gen/eq.rs @@ -2204,6 +2204,9 @@ impl PartialEq for crate::Publish { crate::Publish::OpenRestricted(self0), crate::Publish::OpenRestricted(other0), ) => self0 == other0, + (crate::Publish::Uninterp(self0), crate::Publish::Uninterp(other0)) => { + self0 == other0 + } (crate::Publish::Default, crate::Publish::Default) => true, _ => false, } @@ -2761,6 +2764,14 @@ impl PartialEq for crate::UnOp { } } } +#[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] +impl Eq for crate::Uninterp {} +#[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] +impl PartialEq for crate::Uninterp { + fn eq(&self, _other: &Self) -> bool { + true + } +} #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] impl Eq for crate::UseGlob {} diff --git a/dependencies/syn/src/gen/fold.rs b/dependencies/syn/src/gen/fold.rs index 7629ff4634..e3c1926dea 100644 --- a/dependencies/syn/src/gen/fold.rs +++ b/dependencies/syn/src/gen/fold.rs @@ -1165,6 +1165,9 @@ pub trait Fold { fn fold_un_op(&mut self, i: crate::UnOp) -> crate::UnOp { fold_un_op(self, i) } + fn fold_uninterp(&mut self, i: crate::Uninterp) -> crate::Uninterp { + fold_uninterp(self, i) + } #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "full")))] fn fold_use_glob(&mut self, i: crate::UseGlob) -> crate::UseGlob { @@ -4022,6 +4025,9 @@ where crate::Publish::OpenRestricted(_binding_0) => { crate::Publish::OpenRestricted(f.fold_open_restricted(_binding_0)) } + crate::Publish::Uninterp(_binding_0) => { + crate::Publish::Uninterp(f.fold_uninterp(_binding_0)) + } crate::Publish::Default => crate::Publish::Default, } } @@ -4695,6 +4701,14 @@ where crate::UnOp::Choose(_binding_0) => crate::UnOp::Choose(_binding_0), } } +pub fn fold_uninterp(f: &mut F, node: crate::Uninterp) -> crate::Uninterp +where + F: Fold + ?Sized, +{ + crate::Uninterp { + token: node.token, + } +} #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "full")))] pub fn fold_use_glob(f: &mut F, node: crate::UseGlob) -> crate::UseGlob diff --git a/dependencies/syn/src/gen/hash.rs b/dependencies/syn/src/gen/hash.rs index 14b5b5e7a4..dca7524232 100644 --- a/dependencies/syn/src/gen/hash.rs +++ b/dependencies/syn/src/gen/hash.rs @@ -2816,8 +2816,12 @@ impl Hash for crate::Publish { state.write_u8(2u8); v0.hash(state); } - crate::Publish::Default => { + crate::Publish::Uninterp(v0) => { state.write_u8(3u8); + v0.hash(state); + } + crate::Publish::Default => { + state.write_u8(4u8); } } } @@ -3499,6 +3503,13 @@ impl Hash for crate::UnOp { } } } +#[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] +impl Hash for crate::Uninterp { + fn hash(&self, _state: &mut H) + where + H: Hasher, + {} +} #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "extra-traits")))] impl Hash for crate::UseGlob { diff --git a/dependencies/syn/src/gen/token.css b/dependencies/syn/src/gen/token.css index 9d2823387a..416ee94de7 100644 --- a/dependencies/syn/src/gen/token.css +++ b/dependencies/syn/src/gen/token.css @@ -141,6 +141,7 @@ a.struct[title="struct syn::token::Try"], a.struct[title="struct syn::token::Type"], a.struct[title="struct syn::token::Typeof"], a.struct[title="struct syn::token::Underscore"], +a.struct[title="struct syn::token::Uninterp"], a.struct[title="struct syn::token::Union"], a.struct[title="struct syn::token::Unsafe"], a.struct[title="struct syn::token::Unsized"], @@ -299,6 +300,7 @@ a.struct[title="struct syn::token::Try"]::before, a.struct[title="struct syn::token::Type"]::before, a.struct[title="struct syn::token::Typeof"]::before, a.struct[title="struct syn::token::Underscore"]::before, +a.struct[title="struct syn::token::Uninterp"]::before, a.struct[title="struct syn::token::Union"]::before, a.struct[title="struct syn::token::Unsafe"]::before, a.struct[title="struct syn::token::Unsized"]::before, @@ -888,6 +890,10 @@ a.struct[title="struct syn::token::Underscore"]::before { font-size: calc(100% * 10 / 9); } +a.struct[title="struct syn::token::Uninterp"]::before { + content: "Token![uninterp]"; +} + a.struct[title="struct syn::token::Union"]::before { content: "Token![union]"; } @@ -1094,6 +1100,7 @@ a.struct[title="struct syn::token::Trait"]::after, a.struct[title="struct syn::token::Try"]::after, a.struct[title="struct syn::token::Type"]::after, a.struct[title="struct syn::token::Typeof"]::after, +a.struct[title="struct syn::token::Uninterp"]::after, a.struct[title="struct syn::token::Union"]::after, a.struct[title="struct syn::token::Unsafe"]::after, a.struct[title="struct syn::token::Unsized"]::after, diff --git a/dependencies/syn/src/gen/visit.rs b/dependencies/syn/src/gen/visit.rs index f650734945..a78af99be4 100644 --- a/dependencies/syn/src/gen/visit.rs +++ b/dependencies/syn/src/gen/visit.rs @@ -1050,6 +1050,9 @@ pub trait Visit<'ast> { fn visit_un_op(&mut self, i: &'ast crate::UnOp) { visit_un_op(self, i); } + fn visit_uninterp(&mut self, i: &'ast crate::Uninterp) { + visit_uninterp(self, i); + } #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "full")))] fn visit_use_glob(&mut self, i: &'ast crate::UseGlob) { @@ -4088,6 +4091,9 @@ where crate::Publish::OpenRestricted(_binding_0) => { v.visit_open_restricted(_binding_0); } + crate::Publish::Uninterp(_binding_0) => { + v.visit_uninterp(_binding_0); + } crate::Publish::Default => {} } } @@ -4791,6 +4797,12 @@ where } } } +pub fn visit_uninterp<'ast, V>(v: &mut V, node: &'ast crate::Uninterp) +where + V: Visit<'ast> + ?Sized, +{ + skip!(node.token); +} #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "full")))] pub fn visit_use_glob<'ast, V>(v: &mut V, node: &'ast crate::UseGlob) diff --git a/dependencies/syn/src/gen/visit_mut.rs b/dependencies/syn/src/gen/visit_mut.rs index 9db06f52c5..175bafeb37 100644 --- a/dependencies/syn/src/gen/visit_mut.rs +++ b/dependencies/syn/src/gen/visit_mut.rs @@ -1064,6 +1064,9 @@ pub trait VisitMut { fn visit_un_op_mut(&mut self, i: &mut crate::UnOp) { visit_un_op_mut(self, i); } + fn visit_uninterp_mut(&mut self, i: &mut crate::Uninterp) { + visit_uninterp_mut(self, i); + } #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "full")))] fn visit_use_glob_mut(&mut self, i: &mut crate::UseGlob) { @@ -3904,6 +3907,9 @@ where crate::Publish::OpenRestricted(_binding_0) => { v.visit_open_restricted_mut(_binding_0); } + crate::Publish::Uninterp(_binding_0) => { + v.visit_uninterp_mut(_binding_0); + } crate::Publish::Default => {} } } @@ -4582,6 +4588,12 @@ where } } } +pub fn visit_uninterp_mut(v: &mut V, node: &mut crate::Uninterp) +where + V: VisitMut + ?Sized, +{ + skip!(node.token); +} #[cfg(feature = "full")] #[cfg_attr(docsrs, doc(cfg(feature = "full")))] pub fn visit_use_glob_mut(v: &mut V, node: &mut crate::UseGlob) diff --git a/dependencies/syn/src/lib.rs b/dependencies/syn/src/lib.rs index b40004bfe6..cfc9fffb0e 100644 --- a/dependencies/syn/src/lib.rs +++ b/dependencies/syn/src/lib.rs @@ -559,7 +559,7 @@ pub use crate::verus::{ InvariantNameSetNone, ItemBroadcastGroup, MatchesOpExpr, MatchesOpToken, Mode, ModeExec, ModeGhost, ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted, Prover, Publish, Recommends, Requires, Returns, RevealHide, SignatureDecreases, SignatureInvariants, - SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification, TypeFnSpec, View, + SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification, TypeFnSpec, Uninterp, View, }; #[rustfmt::skip] // https://github.com/rust-lang/rustfmt/issues/6176 diff --git a/dependencies/syn/src/token.rs b/dependencies/syn/src/token.rs index 07d982f888..3cd35a2edc 100644 --- a/dependencies/syn/src/token.rs +++ b/dependencies/syn/src/token.rs @@ -748,6 +748,7 @@ define_keywords! { "exec" pub struct Exec "open" pub struct Open "closed" pub struct Closed + "uninterp" pub struct Uninterp "ghost" pub struct Ghost "tracked" pub struct Tracked "requires" pub struct Requires @@ -1031,6 +1032,7 @@ macro_rules! Token { [exec] => { $crate::token::Exec }; [open] => { $crate::token::Open }; [closed] => { $crate::token::Closed }; + [uninterp] => { $crate::token::Uninterp }; [ghost] => { $crate::token::Ghost }; [tracked] => { $crate::token::Tracked }; [requires] => { $crate::token::Requires }; diff --git a/dependencies/syn/src/verus.rs b/dependencies/syn/src/verus.rs index c31ec239c9..64ffabc560 100644 --- a/dependencies/syn/src/verus.rs +++ b/dependencies/syn/src/verus.rs @@ -7,6 +7,7 @@ ast_enum_of_structs! { Closed(Closed), Open(Open), OpenRestricted(OpenRestricted), + Uninterp(Uninterp), Default, } } @@ -32,6 +33,12 @@ ast_struct! { } } +ast_struct! { + pub struct Uninterp { + pub token: Token![uninterp], + } +} + ast_enum_of_structs! { pub enum Mode { Spec(ModeSpec), @@ -503,6 +510,9 @@ pub mod parsing { } else { Ok(Publish::Open(Open { token })) } + } else if input.peek(Token![uninterp]) { + let token = input.parse::()?; + Ok(Publish::Uninterp(Uninterp { token })) } else { Ok(Publish::Default) } @@ -1414,6 +1424,12 @@ mod printing { } } + impl ToTokens for Uninterp { + fn to_tokens(&self, tokens: &mut TokenStream) { + self.token.to_tokens(tokens); + } + } + #[cfg_attr(doc_cfg, doc(cfg(feature = "printing")))] impl ToTokens for ModeSpec { fn to_tokens(&self, tokens: &mut TokenStream) { diff --git a/dependencies/syn/syn.json b/dependencies/syn/syn.json index 8908806149..664b215706 100644 --- a/dependencies/syn/syn.json +++ b/dependencies/syn/syn.json @@ -5592,6 +5592,11 @@ "syn": "OpenRestricted" } ], + "Uninterp": [ + { + "syn": "Uninterp" + } + ], "Default": [] } }, @@ -6942,6 +6947,17 @@ }, "exhaustive": false }, + { + "ident": "Uninterp", + "features": { + "any": [] + }, + "fields": { + "token": { + "token": "Uninterp" + } + } + }, { "ident": "UseGlob", "features": { @@ -7394,6 +7410,7 @@ "Type": "type", "Typeof": "typeof", "Underscore": "_", + "Uninterp": "uninterp", "Union": "union", "Unsafe": "unsafe", "Unsized": "unsized", diff --git a/dependencies/syn/tests/debug/gen.rs b/dependencies/syn/tests/debug/gen.rs index 15b45ff179..8cd6b5149a 100644 --- a/dependencies/syn/tests/debug/gen.rs +++ b/dependencies/syn/tests/debug/gen.rs @@ -5110,6 +5110,13 @@ impl Debug for Lite { formatter.write_str(")")?; Ok(()) } + syn::Publish::Uninterp(_val) => { + formatter.write_str("Publish::Uninterp")?; + formatter.write_str("(")?; + Debug::fmt(Lite(_val), formatter)?; + formatter.write_str(")")?; + Ok(()) + } syn::Publish::Default => formatter.write_str("Publish::Default"), } } @@ -6403,6 +6410,12 @@ impl Debug for Lite { } } } +impl Debug for Lite { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + let mut formatter = formatter.debug_struct("Uninterp"); + formatter.finish() + } +} impl Debug for Lite { fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { let mut formatter = formatter.debug_struct("UseGlob"); @@ -7317,6 +7330,11 @@ impl Debug for Lite { formatter.write_str("Token![_]") } } +impl Debug for Lite { + fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { + formatter.write_str("Token![uninterp]") + } +} impl Debug for Lite { fn fmt(&self, formatter: &mut fmt::Formatter) -> fmt::Result { formatter.write_str("Token![union]") diff --git a/source/builtin_macros/src/rustdoc.rs b/source/builtin_macros/src/rustdoc.rs index c1729b5c1b..2f1264760a 100644 --- a/source/builtin_macros/src/rustdoc.rs +++ b/source/builtin_macros/src/rustdoc.rs @@ -185,6 +185,7 @@ fn fn_mode_to_string(mode: &FnMode, publish: &Publish) -> String { Publish::OpenRestricted(res) => { "open(".to_string() + &module_path_to_string(&res.path) + ") spec" } + Publish::Uninterp(_) => "uninterp".to_string(), Publish::Default => "spec".to_string(), }, FnMode::Proof(_) => "proof".to_string(), diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index dbf96012ef..1f82100def 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -579,7 +579,7 @@ impl Visitor { let publish_span = sig.publish.span(); stmts.push(stmt_with_semi!( publish_span => - compile_error!("only `spec` functions can be marked `open` or `closed`") + compile_error!("only `spec` functions can be marked `open`, `closed`, or `uninterp`") )); } @@ -601,6 +601,7 @@ impl Visitor { Publish::Default => vec![], Publish::Closed(o) => vec![mk_verus_attr(o.token.span, quote! { closed })], Publish::Open(o) => vec![mk_verus_attr(o.token.span, quote! { open })], + Publish::Uninterp(o) => vec![mk_verus_attr(o.token.span, quote! { uninterp })], Publish::OpenRestricted(_) => { unimplemented!("TODO: support open(...)") } @@ -743,6 +744,7 @@ impl Visitor { (_, _, Publish::Default) => vec![mk_verus_attr(span, quote! { open })], (_, _, Publish::Closed(o)) => vec![mk_verus_attr(o.token.span, quote! { closed })], (_, _, Publish::Open(o)) => vec![mk_verus_attr(o.token.span, quote! { open })], + (_, _, Publish::Uninterp(o)) => vec![mk_verus_attr(o.token.span, quote! { uninterp })], (_, _, Publish::OpenRestricted(_)) => { unimplemented!("TODO: support open(...)") } diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs index a79cbb4b61..40c490d0a2 100644 --- a/source/rust_verify/src/attributes.rs +++ b/source/rust_verify/src/attributes.rs @@ -199,6 +199,13 @@ pub(crate) enum GhostBlockAttr { Wrapper, } +#[derive(Debug, PartialEq)] +pub(crate) enum AttrPublish { + Open, + Closed, + Uninterp, +} + #[derive(Debug, PartialEq)] pub(crate) enum Attr { // specify mode (spec, proof, exec) @@ -218,7 +225,7 @@ pub(crate) enum Attr { // hide body (from all modules) until revealed Opaque, // publish body? - Publish(bool), + Publish(AttrPublish), // publish body with zero fuel OpaqueOutsideModule, // inline spec function in SMT query @@ -384,10 +391,6 @@ pub(crate) fn parse_attrs( AttrTree::Fun(_, arg, None) if arg == "external" => v.push(Attr::External), AttrTree::Fun(_, arg, None) if arg == "verify" => v.push(Attr::Verify), AttrTree::Fun(_, arg, None) if arg == "opaque" => v.push(Attr::Opaque), - AttrTree::Fun(_, arg, None) if arg == "publish" => { - report_deprecated("publish", "use `open spec fn` and `closed spec fn` instead"); - v.push(Attr::Publish(true)) - } AttrTree::Fun(_, arg, None) if arg == "opaque_outside_module" => { v.push(Attr::OpaqueOutsideModule) } @@ -622,8 +625,15 @@ pub(crate) fn parse_attrs( AttrTree::Fun(_, arg, None) if arg == "external_body" => { v.push(Attr::ExternalBody) } - AttrTree::Fun(_, arg, None) if arg == "open" => v.push(Attr::Publish(true)), - AttrTree::Fun(_, arg, None) if arg == "closed" => v.push(Attr::Publish(false)), + AttrTree::Fun(_, arg, None) if arg == "open" => { + v.push(Attr::Publish(AttrPublish::Open)) + } + AttrTree::Fun(_, arg, None) if arg == "closed" => { + v.push(Attr::Publish(AttrPublish::Closed)) + } + AttrTree::Fun(_, arg, None) if arg == "uninterp" => { + v.push(Attr::Publish(AttrPublish::Uninterp)) + } AttrTree::Fun(_, arg, Some(box [AttrTree::Fun(_, name, None)])) if arg == "returns" && name == "spec" => { @@ -851,7 +861,7 @@ pub(crate) struct VerifierAttrs { pub(crate) verus_macro: bool, pub(crate) external_body: bool, pub(crate) opaque: bool, - pub(crate) publish: Option, + pub(crate) publish: Option, pub(crate) opaque_outside_module: bool, pub(crate) inline: bool, pub(crate) ext_equal: bool, diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs index 4311e54ce2..d1489fcf2b 100644 --- a/source/rust_verify/src/rust_to_vir_func.rs +++ b/source/rust_verify/src/rust_to_vir_func.rs @@ -1,4 +1,4 @@ -use crate::attributes::{get_mode, get_ret_mode, get_var_mode, VerifierAttrs}; +use crate::attributes::{get_mode, get_ret_mode, get_var_mode, AttrPublish, VerifierAttrs}; use crate::context::{BodyCtxt, Context}; use crate::rust_to_vir_base::mk_visibility; use crate::rust_to_vir_base::{ @@ -964,7 +964,8 @@ pub(crate) fn check_item_fn<'tcx>( } else { vir_body }; - let open_closed_present = vattrs.publish.is_some(); + let open_closed_present = + vattrs.publish == Some(AttrPublish::Open) || vattrs.publish == Some(AttrPublish::Closed); match kind { FunctionKind::TraitMethodImpl { .. } | FunctionKind::TraitMethodDecl { .. } if body.is_some() => @@ -1924,7 +1925,7 @@ pub(crate) fn check_foreign_item_fn<'tcx>( fn get_body_visibility_and_fuel( span: Span, func_visibility: &Visibility, - publish: Option, + publish: Option, opaque: bool, opaque_outside_module: bool, mode: Mode, @@ -1934,10 +1935,10 @@ fn get_body_visibility_and_fuel( let private_vis = Visibility { restricted_to: Some(my_module.clone()) }; if mode != Mode::Spec { - if publish == Some(true) { + if publish == Some(AttrPublish::Open) { return err_span(span, "function is marked `open` but it is not a `spec` function"); } - if publish == Some(false) { + if publish == Some(AttrPublish::Closed) { return err_span(span, "function is marked `closed` but it is not a `spec` function"); } if opaque || opaque_outside_module { @@ -1954,19 +1955,27 @@ fn get_body_visibility_and_fuel( // These don't matter without a body Ok((private_vis, Opaqueness::Opaque)) } else { + // mode == Mode::Spec && has_body + if publish == Some(AttrPublish::Uninterp) { + return err_span(span, "function is marked `uninterp` but it has a body"); + } + if opaque && opaque_outside_module { return err_span(span, "function is marked both 'opaque' and 'opaque_outside_module'"); } - if publish == Some(true) && func_visibility == &private_vis { + if publish == Some(AttrPublish::Open) && func_visibility == &private_vis { return err_span( span, "function is marked `open` but not marked `pub`; for the body of a function to be visible, the function symbol must also be visible", ); } - let body_visibility = - if publish == Some(true) { func_visibility.clone() } else { private_vis.clone() }; + let body_visibility = if publish == Some(AttrPublish::Open) { + func_visibility.clone() + } else { + private_vis.clone() + }; let opaqueness = if opaque { Opaqueness::Opaque diff --git a/source/rust_verify_test/tests/modules.rs b/source/rust_verify_test/tests/modules.rs index 269bfcec4c..fbcb8f0be2 100644 --- a/source/rust_verify_test/tests/modules.rs +++ b/source/rust_verify_test/tests/modules.rs @@ -163,18 +163,16 @@ test_verify_one_file! { test_verify_one_file! { #[test] publish_proof_fail verus_code! { - #[verifier(publish)] - pub proof fn bar() { + pub open proof fn bar() { } - } => Err(err) => assert_vir_error_msg(err, "function is marked `open` but it is not a `spec` function") + } => Err(err) => assert_vir_error_msg(err, "only `spec` functions can be marked `open`, `closed`, or `uninterp`") } test_verify_one_file! { #[test] publish_exec_fail verus_code! { - #[verifier(publish)] - pub fn bar() { + pub open fn bar() { } - } => Err(err) => assert_vir_error_msg(err, "function is marked `open` but it is not a `spec` function") + } => Err(err) => assert_vir_error_msg(err, "only `spec` functions can be marked `open`, `closed`, or `uninterp`") } test_verify_one_file! { @@ -209,3 +207,56 @@ test_verify_one_file! { } } => Err(err) => assert_vir_error_msg(err, "in pub open spec function, cannot refer to private const") } + +test_verify_one_file! { + #[test] uninterp_exec_fail verus_code! { + pub uninterp fn bar() { + } + } => Err(err) => assert_vir_error_msg(err, "only `spec` functions can be marked `open`, `closed`, or `uninterp`") +} + +test_verify_one_file! { + #[test] uninterp_spec_body_free_fail verus_code! { + pub uninterp spec fn bar() -> bool { + true + } + } => Err(err) => assert_vir_error_msg(err, "function is marked `uninterp` but it has a body") +} + +test_verify_one_file! { + #[test] uninterp_spec_body_assoc_fail verus_code! { + struct G { + v: bool, + } + + impl G { + pub uninterp spec fn bar(&self) -> bool { + self.v + } + } + } => Err(err) => assert_vir_error_msg(err, "function is marked `uninterp` but it has a body") +} + +test_verify_one_file! { + #[test] uninterp_spec_body_trait_fail verus_code! { + trait T { + uninterp spec fn bar(&self) -> bool { + true + } + } + } => Err(err) => assert_vir_error_msg(err, "function is marked `uninterp` but it has a body") +} + +test_verify_one_file! { + #[test] uninterp_spec_body_trait_impl_fail verus_code! { + trait T { + uninterp spec fn bar(&self) -> bool; + } + + impl T for bool { + spec fn bar(&self) -> bool { + *self + } + } + } => Err(err) => { todo!() } +} diff --git a/source/vir/src/ast.rs b/source/vir/src/ast.rs index 4e3c6115d3..30749d127b 100644 --- a/source/vir/src/ast.rs +++ b/source/vir/src/ast.rs @@ -104,6 +104,14 @@ pub struct Visibility { pub restricted_to: Option, } +#[derive(Clone, Debug, Serialize, Deserialize, ToDebugSNode, PartialEq, Eq)] +pub enum BodyVisibility { + Uninterpreted, + /// None for pub + /// Some(path) means visible to path and path's descendents + Visibility(Visibility), +} + /// Describes whether a variable, function, etc. is compiled or just used for verification #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq, Hash)] pub enum Mode { @@ -1075,7 +1083,7 @@ pub struct FunctionX { /// Access control (public/private) pub visibility: Visibility, /// Controlled by 'open'. (Only applicable to spec functions.) - pub body_visibility: Visibility, + pub body_visibility: BodyVisibility, /// Controlled by 'opaque/opaque_outside_module'. (Only applicable to spec functions.) pub opaqueness: Opaqueness, /// Owning module