Skip to content

Commit 3105aa2

Browse files
tjhancetjhance
authored
change the encoding for consts and const fns (#1563)
1 parent c5dd91c commit 3105aa2

File tree

10 files changed

+376
-62
lines changed

10 files changed

+376
-62
lines changed

‎source/builtin_macros/src/syntax.rs‎

Lines changed: 229 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -28,14 +28,15 @@ use syn_verus::{
2828
FnArg, FnArgKind, FnMode, Global, Ident, ImplItem, ImplItemFn, Invariant, InvariantEnsures,
2929
InvariantExceptBreak, InvariantNameSet, InvariantNameSetList, InvariantNameSetSet, Item,
3030
ItemBroadcastGroup, ItemConst, ItemEnum, ItemFn, ItemImpl, ItemMod, ItemStatic, ItemStruct,
31-
ItemTrait, ItemUnion, Lit, Local, MatchesOpExpr, MatchesOpToken, ModeSpec, ModeSpecChecked,
32-
Pat, PatIdent, PatType, Path, Publish, Recommends, Requires, ReturnType, Returns, Signature,
33-
SignatureDecreases, SignatureInvariants, SignatureSpec, SignatureSpecAttr, SignatureUnwind,
34-
Stmt, Token, TraitItem, TraitItemFn, Type, TypeFnProof, TypeFnSpec, TypePath, UnOp, Visibility,
35-
braced, bracketed, parenthesized, parse_macro_input,
31+
ItemTrait, ItemUnion, Lit, Local, MatchesOpExpr, MatchesOpToken, Meta, MetaList, ModeSpec,
32+
ModeSpecChecked, Pat, PatIdent, PatType, Path, Publish, Recommends, Requires, ReturnType,
33+
Returns, Signature, SignatureDecreases, SignatureInvariants, SignatureSpec, SignatureSpecAttr,
34+
SignatureUnwind, Stmt, Token, TraitItem, TraitItemFn, Type, TypeFnProof, TypeFnSpec, TypePath,
35+
UnOp, Visibility, braced, bracketed, parenthesized, parse_macro_input,
3636
};
3737

3838
const VERUS_SPEC: &str = "VERUS_SPEC__";
39+
const VERUS_UNERASED_PROXY: &str = "VERUS_UNERASED_PROXY__";
3940

4041
fn take_expr(expr: &mut Expr) -> Expr {
4142
let dummy: Expr = Expr::Verbatim(TokenStream::new());
@@ -462,6 +463,10 @@ fn merge_default_ensures(
462463
}
463464

464465
impl Visitor {
466+
fn needs_unerased_proxies(&self) -> bool {
467+
self.erase_ghost.keep() && !self.rustdoc
468+
}
469+
465470
fn take_ghost<T: Default>(&self, dest: &mut T) -> T {
466471
take_ghost(self.erase_ghost, dest)
467472
}
@@ -822,6 +827,7 @@ impl Visitor {
822827
sig.mode,
823828
FnMode::Default | FnMode::Exec(_) | FnMode::Proof(_) | FnMode::ProofAxiom(_)
824829
) && !matches!(sig.publish, Publish::Default)
830+
&& !is_encoded_const(attrs)
825831
{
826832
let publish_span = sig.publish.span();
827833
stmts.push(stmt_with_semi!(
@@ -969,16 +975,12 @@ impl Visitor {
969975
con_expr: &mut Option<Box<Expr>>,
970976
con_eq_token: &mut Option<Token![=]>,
971977
con_semi_token: &mut Option<Token![;]>,
972-
con_ty: &Type,
978+
_con_ty: &Type,
973979
con_span: Span,
974980
) {
975981
if matches!(con_mode, FnMode::Spec(_) | FnMode::SpecChecked(_)) {
976-
if let Some(mut expr) = con_expr.take() {
982+
if let Some(expr) = con_expr.take() {
977983
let mut stmts = Vec::new();
978-
self.inside_ghost += 1;
979-
self.visit_expr_mut(&mut expr);
980-
self.inside_ghost -= 1;
981-
stmts.push(Stmt::Expr(Expr::Verbatim(quote_spanned!(con_span => #[allow(non_snake_case)]#[verus::internal(verus_macro)] #[verus::internal(const_body)] fn __VERUS_CONST_BODY__() -> #con_ty { #expr } )), None));
982984
stmts.push(Stmt::Expr(
983985
Expr::Verbatim(quote_spanned!(con_span => unsafe { core::mem::zeroed() })),
984986
None,
@@ -1399,6 +1401,8 @@ impl Visitor {
13991401
}
14001402

14011403
fn visit_items_prefilter(&mut self, items: &mut Vec<Item>) {
1404+
self.visit_items_make_unerased_proxies(items);
1405+
14021406
if self.erase_ghost.erase_all() {
14031407
// Erase ghost functions and constants
14041408
items.retain(|item| match item {
@@ -1836,6 +1840,160 @@ impl Visitor {
18361840
}
18371841
}
18381842

1843+
fn item_needs_unerased_proxy(&self, item: &Item) -> bool {
1844+
match item {
1845+
Item::Const(item_const) => !is_external(&item_const.attrs),
1846+
Item::Fn(item_fn) => item_fn.sig.constness.is_some() && !is_external(&item_fn.attrs),
1847+
_ => false,
1848+
}
1849+
}
1850+
1851+
fn item_translate_const_to_0_arg_fn(&self, item: Item) -> Item {
1852+
match item {
1853+
Item::Const(item_const) => {
1854+
let span = item_const.span();
1855+
let ItemConst {
1856+
mut attrs,
1857+
vis,
1858+
const_token,
1859+
ident,
1860+
generics,
1861+
colon_token,
1862+
ty,
1863+
eq_token: _,
1864+
expr,
1865+
semi_token: _,
1866+
publish,
1867+
mode,
1868+
ensures,
1869+
block,
1870+
} = item_const;
1871+
attrs.push(mk_verus_attr(span, quote! { encoded_const }));
1872+
1873+
let publish = match (publish, &mode, &vis) {
1874+
(publish, _, Visibility::Inherited) => publish,
1875+
(
1876+
Publish::Default,
1877+
FnMode::Spec(_) | FnMode::SpecChecked(_) | FnMode::Default,
1878+
_,
1879+
) => Publish::Open(syn_verus::Open { token: token::Open { span } }),
1880+
(publish, _, _) => publish,
1881+
};
1882+
1883+
Item::Fn(ItemFn {
1884+
attrs,
1885+
vis,
1886+
sig: Signature {
1887+
spec: SignatureSpec {
1888+
prover: None,
1889+
requires: None,
1890+
recommends: None,
1891+
ensures,
1892+
default_ensures: None,
1893+
returns: None,
1894+
decreases: None,
1895+
invariants: None,
1896+
unwind: None,
1897+
with: None,
1898+
},
1899+
publish,
1900+
constness: None,
1901+
asyncness: None,
1902+
unsafety: None,
1903+
abi: None,
1904+
broadcast: None,
1905+
mode: mode,
1906+
fn_token: token::Fn { span: const_token.span },
1907+
ident: ident.clone(),
1908+
generics,
1909+
paren_token: Paren { span: into_spans(colon_token.span) },
1910+
inputs: Punctuated::new(),
1911+
variadic: None,
1912+
output: ReturnType::Type(
1913+
token::RArrow { spans: [colon_token.span, colon_token.span] },
1914+
None,
1915+
None, /*
1916+
Some(Box::new((
1917+
Paren { span: into_spans(colon_token.span) },
1918+
Pat::Verbatim(quote!{ #ident }),
1919+
colon_token,
1920+
))), */
1921+
ty,
1922+
),
1923+
},
1924+
block: (match block {
1925+
Some(block) => block,
1926+
_ => {
1927+
let expr = expr.unwrap();
1928+
Box::new(Block {
1929+
brace_token: Brace { span: into_spans(expr.span()) },
1930+
stmts: vec![Stmt::Expr(*expr, None)],
1931+
})
1932+
}
1933+
}),
1934+
semi_token: None,
1935+
})
1936+
}
1937+
item => item,
1938+
}
1939+
}
1940+
1941+
fn item_make_proxy(&self, item: Item) -> Item {
1942+
let mut item = item;
1943+
item = self.item_translate_const_to_0_arg_fn(item);
1944+
match &mut item {
1945+
Item::Fn(item_fn) => {
1946+
item_fn.sig.ident = Ident::new(
1947+
&format!("{}{}", VERUS_UNERASED_PROXY, &item_fn.sig.ident),
1948+
item_fn.sig.span(),
1949+
);
1950+
item_fn.attrs.push(mk_verus_attr(item_fn.span(), quote! { unerased_proxy }));
1951+
}
1952+
_ => unreachable!(),
1953+
}
1954+
item
1955+
}
1956+
1957+
fn item_make_external_and_erased(&mut self, item: Item) -> Item {
1958+
let mut item = item;
1959+
1960+
self.erase_ghost = EraseGhost::Erase;
1961+
self.visit_item_mut(&mut item);
1962+
self.erase_ghost = EraseGhost::Keep;
1963+
1964+
let span = item.span();
1965+
let attributes = match &mut item {
1966+
Item::Fn(item_fn) => &mut item_fn.attrs,
1967+
Item::Const(item_const) => &mut item_const.attrs,
1968+
_ => unreachable!(),
1969+
};
1970+
attributes.push(mk_verifier_attr(span, quote! { external }));
1971+
attributes.push(mk_verus_attr(span, quote! { uses_unerased_proxy }));
1972+
1973+
item
1974+
}
1975+
1976+
fn visit_items_make_unerased_proxies(&mut self, items: &mut Vec<Item>) {
1977+
if !self.needs_unerased_proxies() {
1978+
return;
1979+
}
1980+
1981+
let mut new_items = vec![];
1982+
1983+
for item in std::mem::take(items).into_iter() {
1984+
if self.item_needs_unerased_proxy(&item) {
1985+
let proxy = self.item_make_proxy(item.clone());
1986+
let erased = self.item_make_external_and_erased(item);
1987+
new_items.push(proxy);
1988+
new_items.push(erased);
1989+
} else {
1990+
new_items.push(item);
1991+
}
1992+
}
1993+
1994+
*items = new_items;
1995+
}
1996+
18391997
fn visit_impl_items_prefilter(&mut self, items: &mut Vec<ImplItem>, for_trait: bool) {
18401998
if self.erase_ghost.erase_all() {
18411999
items.retain(|item| match item {
@@ -5048,6 +5206,36 @@ pub(crate) fn has_external_code(attrs: &Vec<Attribute>) -> bool {
50485206
})
50495207
}
50505208

5209+
pub(crate) fn is_encoded_const(attrs: &Vec<Attribute>) -> bool {
5210+
attrs.iter().any(|attr| match &attr.meta {
5211+
Meta::List(MetaList { path, delimiter: _, tokens }) => {
5212+
path.segments.len() == 2
5213+
&& path.segments[0].ident.to_string() == "verus"
5214+
&& path.segments[1].ident.to_string() == "internal"
5215+
&& tokens.to_string() == "encoded_const"
5216+
}
5217+
_ => false,
5218+
})
5219+
}
5220+
5221+
pub(crate) fn is_external(attrs: &Vec<Attribute>) -> bool {
5222+
attrs.iter().any(|attr| {
5223+
// verifier::external
5224+
attr.path().segments.len() == 2
5225+
&& attr.path().segments[0].ident.to_string() == "verifier"
5226+
&& attr.path().segments[1].ident.to_string() == "external"
5227+
// verifier(external)
5228+
|| attr.path().segments.len() == 1
5229+
&& attr.path().segments[0].ident.to_string() == "verifier"
5230+
&& match &attr.meta {
5231+
syn_verus::Meta::List(list) => {
5232+
matches!(list.tokens.to_string().as_str(), "external")
5233+
}
5234+
_ => false,
5235+
}
5236+
})
5237+
}
5238+
50515239
/// Constructs #[name(tokens)]
50525240
macro_rules! declare_mk_rust_attr {
50535241
($name:ident, $s:ident) => {
@@ -5083,7 +5271,7 @@ declare_mk_rust_attr!(mk_rust_attr_syn, syn);
50835271

50845272
/// Constructs #[verus::internal(tokens)]
50855273
macro_rules! declare_mk_verus_attr {
5086-
($name:ident, $s:ident) => {
5274+
($name:ident, $name2:ident, $s:ident) => {
50875275
pub(crate) fn $name(span: Span, tokens: TokenStream) -> $s::Attribute {
50885276
let mut path_segments = $s::punctuated::Punctuated::new();
50895277
path_segments.push($s::PathSegment {
@@ -5113,10 +5301,37 @@ macro_rules! declare_mk_verus_attr {
51135301
meta,
51145302
}
51155303
}
5304+
5305+
#[allow(dead_code)]
5306+
pub(crate) fn $name2(span: Span, tokens: TokenStream) -> $s::Attribute {
5307+
let mut path_segments = $s::punctuated::Punctuated::new();
5308+
path_segments.push($s::PathSegment {
5309+
ident: $s::Ident::new("verifier", span),
5310+
arguments: $s::PathArguments::None,
5311+
});
5312+
let path = $s::Path { leading_colon: None, segments: path_segments };
5313+
let meta = if tokens.is_empty() {
5314+
$s::Meta::Path(path)
5315+
} else {
5316+
$s::Meta::List($s::MetaList {
5317+
path,
5318+
delimiter: $s::MacroDelimiter::Paren($s::token::Paren {
5319+
span: into_spans(span),
5320+
}),
5321+
tokens: quote! { #tokens },
5322+
})
5323+
};
5324+
$s::Attribute {
5325+
pound_token: $s::token::Pound { spans: [span] },
5326+
style: $s::AttrStyle::Outer,
5327+
bracket_token: $s::token::Bracket { span: into_spans(span) },
5328+
meta,
5329+
}
5330+
}
51165331
};
51175332
}
5118-
declare_mk_verus_attr!(mk_verus_attr, syn_verus);
5119-
declare_mk_verus_attr!(mk_verus_attr_syn, syn);
5333+
declare_mk_verus_attr!(mk_verus_attr, mk_verifier_attr, syn_verus);
5334+
declare_mk_verus_attr!(mk_verus_attr_syn, mk_verifier_attr_syn, syn);
51205335

51215336
fn is_ptr_type(typ: &Type) -> bool {
51225337
match typ {

‎source/rust_verify/src/attributes.rs‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -336,6 +336,10 @@ pub(crate) enum Attr {
336336
ExecAllowNoDecreasesClause,
337337
// Assume that the function terminates
338338
AssumeTermination,
339+
// Proxy containing unerased code
340+
UnerasedProxy,
341+
UsesUnerasedProxy,
342+
EncodedConst,
339343
}
340344

341345
fn get_trigger_arg(span: Span, attr_tree: &AttrTree) -> Result<u64, VirErr> {
@@ -745,6 +749,15 @@ pub(crate) fn parse_attrs(
745749
AttrTree::Fun(_, arg, None) if arg == "open_visibility_qualifier" => {
746750
v.push(Attr::OpenVisibilityQualifier)
747751
}
752+
AttrTree::Fun(_, arg, None) if arg == "unerased_proxy" => {
753+
v.push(Attr::UnerasedProxy)
754+
}
755+
AttrTree::Fun(_, arg, None) if arg == "uses_unerased_proxy" => {
756+
v.push(Attr::UsesUnerasedProxy)
757+
}
758+
AttrTree::Fun(_, arg, None) if arg == "encoded_const" => {
759+
v.push(Attr::EncodedConst)
760+
}
748761
_ => {
749762
return err_span(span, "unrecognized internal attribute");
750763
}
@@ -931,6 +944,7 @@ pub(crate) struct ExternalAttrs {
931944
pub(crate) any_other_verus_specific_attribute: bool,
932945
pub(crate) internal_get_field_many_variants: bool,
933946
pub(crate) external_auto_derives: AutoDerivesAttr,
947+
pub(crate) uses_unerased_proxy: bool,
934948
}
935949

936950
#[derive(Debug)]
@@ -987,6 +1001,8 @@ pub(crate) struct VerifierAttrs {
9871001
pub(crate) open_visibility_qualifier: bool,
9881002
pub(crate) assume_termination: bool,
9891003
pub(crate) exec_allows_no_decreases_clause: bool,
1004+
pub(crate) unerased_proxy: bool,
1005+
pub(crate) encoded_const: bool,
9901006
}
9911007

9921008
// Check for the `get_field_many_variants` attribute
@@ -1043,6 +1059,7 @@ pub(crate) fn get_external_attrs(
10431059
any_other_verus_specific_attribute: false,
10441060
internal_get_field_many_variants: false,
10451061
external_auto_derives: AutoDerivesAttr::Regular,
1062+
uses_unerased_proxy: false,
10461063
};
10471064

10481065
for attr in parse_attrs(attrs, diagnostics)? {
@@ -1064,6 +1081,7 @@ pub(crate) fn get_external_attrs(
10641081
Attr::ExternalAutoDerives(Some(external_auto_derives)) => {
10651082
es.external_auto_derives = AutoDerivesAttr::SomeExternal(external_auto_derives)
10661083
}
1084+
Attr::UsesUnerasedProxy => es.uses_unerased_proxy = true,
10671085
Attr::UnsupportedRustcAttr(..) => {}
10681086
_ => {
10691087
es.any_other_verus_specific_attribute = true;
@@ -1145,6 +1163,8 @@ pub(crate) fn get_verifier_attrs_maybe_check(
11451163
open_visibility_qualifier: false,
11461164
assume_termination: false,
11471165
exec_allows_no_decreases_clause: false,
1166+
unerased_proxy: false,
1167+
encoded_const: false,
11481168
};
11491169
let mut unsupported_rustc_attr: Option<(String, Span)> = None;
11501170
for attr in parse_attrs(attrs, diagnostics)? {
@@ -1217,6 +1237,9 @@ pub(crate) fn get_verifier_attrs_maybe_check(
12171237
Attr::OpenVisibilityQualifier => vs.open_visibility_qualifier = true,
12181238
Attr::AssumeTermination => vs.assume_termination = true,
12191239
Attr::ExecAllowNoDecreasesClause => vs.exec_allows_no_decreases_clause = true,
1240+
Attr::UnerasedProxy => vs.unerased_proxy = true,
1241+
Attr::EncodedConst => vs.encoded_const = true,
1242+
Attr::UsesUnerasedProxy => {}
12201243
_ => {}
12211244
}
12221245
}

0 commit comments

Comments
 (0)