From f0d134773db896a1eadd57221ebf7ff629a6b648 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 20 Jan 2022 14:08:21 +0100 Subject: [PATCH 1/6] Add #[is_variant] to enable adt.is_Variant() functions that are directly encoded to SMT (is-Variant) --- source/builtin_macros/src/is_variant.rs | 40 ++++++++++++++ source/builtin_macros/src/lib.rs | 31 ++--------- source/builtin_macros/src/structural.rs | 25 +++++++++ source/rust_verify/example/adts.rs | 44 +++++++++------ source/rust_verify/src/def.rs | 1 + source/rust_verify/src/erase.rs | 3 ++ source/rust_verify/src/lib.rs | 1 + source/rust_verify/src/rust_to_vir.rs | 63 ++++++++++++++++------ source/rust_verify/src/rust_to_vir_base.rs | 57 +++++++++++--------- source/rust_verify/src/rust_to_vir_expr.rs | 55 ++++++++++++++++--- source/rust_verify/tests/adts.rs | 40 ++++++++++++++ 11 files changed, 273 insertions(+), 87 deletions(-) create mode 100644 source/builtin_macros/src/is_variant.rs create mode 100644 source/builtin_macros/src/structural.rs create mode 100644 source/rust_verify/src/def.rs diff --git a/source/builtin_macros/src/is_variant.rs b/source/builtin_macros/src/is_variant.rs new file mode 100644 index 0000000000..e2cb7c3500 --- /dev/null +++ b/source/builtin_macros/src/is_variant.rs @@ -0,0 +1,40 @@ +use quote::quote; + +pub fn attribute_is_variant( + _attr: proc_macro2::TokenStream, + s: synstructure::Structure, +) -> proc_macro2::TokenStream { + let ast = &s.ast(); + match ast.data { + syn::Data::Enum(_) => {} + _ => panic!("#[is_variant] is only allowed on enums"), + } + let struct_name = &s.ast().ident; + let is_impls = s + .variants() + .iter() + .map(|v| { + let variant_ident = v.ast().ident.to_string(); + + let fun_ident = + syn::Ident::new(&format!("is_{}", &variant_ident), v.ast().ident.span()); + quote! { + #[doc(hidden)] + #[spec] + #[verifier(is_variant)] + #[allow(non_snake_case)] + fn #fun_ident(&self) -> bool { unimplemented!() } + } + }) + .collect::(); + + let generics = &ast.generics; + quote! { + #ast + + #[automatically_derived] + impl#generics #struct_name#generics { + #is_impls + } + } +} diff --git a/source/builtin_macros/src/lib.rs b/source/builtin_macros/src/lib.rs index c2e8becd7b..190244388e 100644 --- a/source/builtin_macros/src/lib.rs +++ b/source/builtin_macros/src/lib.rs @@ -1,28 +1,7 @@ -use quote::quote; -use synstructure::decl_derive; +use synstructure::{decl_attribute, decl_derive}; +mod is_variant; +mod structural; -decl_derive!([Structural] => derive_structural); +decl_derive!([Structural] => structural::derive_structural); -fn derive_structural(s: synstructure::Structure) -> proc_macro2::TokenStream { - let assert_receiver_is_structural_body = s - .variants() - .iter() - .flat_map(|v| v.ast().fields) - .map(|f| { - let ty = &f.ty; - quote! { - let _: ::builtin::AssertParamIsStructural<#ty>; - } - }) - .collect::(); - s.gen_impl(quote! { - #[automatically_derived] - gen impl ::builtin::Structural for @Self { - #[inline] - #[doc(hidden)] - fn assert_receiver_is_structural(&self) -> () { - #assert_receiver_is_structural_body - } - } - }) -} +decl_attribute!([is_variant] => is_variant::attribute_is_variant); diff --git a/source/builtin_macros/src/structural.rs b/source/builtin_macros/src/structural.rs new file mode 100644 index 0000000000..9fbff7677b --- /dev/null +++ b/source/builtin_macros/src/structural.rs @@ -0,0 +1,25 @@ +use quote::quote; + +pub fn derive_structural(s: synstructure::Structure) -> proc_macro2::TokenStream { + let assert_receiver_is_structural_body = s + .variants() + .iter() + .flat_map(|v| v.ast().fields) + .map(|f| { + let ty = &f.ty; + quote! { + let _: ::builtin::AssertParamIsStructural<#ty>; + } + }) + .collect::(); + s.gen_impl(quote! { + #[automatically_derived] + gen impl ::builtin::Structural for @Self { + #[inline] + #[doc(hidden)] + fn assert_receiver_is_structural(&self) -> () { + #assert_receiver_is_structural_body + } + } + }) +} diff --git a/source/rust_verify/example/adts.rs b/source/rust_verify/example/adts.rs index e071faabb0..fa23ac0621 100644 --- a/source/rust_verify/example/adts.rs +++ b/source/rust_verify/example/adts.rs @@ -11,30 +11,42 @@ struct Car

{ #[derive(Structural, PartialEq, Eq)] enum Vehicle { - Car(Car), + Car(Car), Train(bool), } -fn test_struct_1(p: int) { +fn test_struct_1(p: u64) { let c1 = Car { four_doors: true, passengers: p }; assert(c1.passengers == p); assert((Car { passengers: p, four_doors: true }).passengers == p); } -// fn test_structural_eq(passengers: int) { -// let c1 = Car { passengers, four_doors: true }; -// let c2 = Car { passengers, four_doors: false }; -// let c3 = Car { passengers, four_doors: true }; -// -// assert(c1 == c3); -// assert(c1 != c2); -// -// let t = Vehicle::Train(true); -// let ca = Vehicle::Car(c1); -// -// assert(t != ca); -// // assert(t == ca); // FAILS -// } +fn test_structural_eq(passengers: u64) { + let c1 = Car { passengers, four_doors: true }; + let c2 = Car { passengers, four_doors: false }; + let c3 = Car { passengers, four_doors: true }; + + assert(c1 == c3); + assert(c1 != c2); + + let t = Vehicle::Train(true); + let ca = Vehicle::Car(c1); + + assert(t != ca); +} + +#[is_variant] #[derive(Structural, PartialEq, Eq)] +enum Vehicle2 { + Car(Car), + Train(bool), +} + +fn test_is_variant_1(v: Vehicle2) { + match v { + Vehicle2::Car(_) => assert(v.is_Car()), + Vehicle2::Train(_) => assert(v.is_Train()), + }; +} fn main() { } diff --git a/source/rust_verify/src/def.rs b/source/rust_verify/src/def.rs new file mode 100644 index 0000000000..559217ac72 --- /dev/null +++ b/source/rust_verify/src/def.rs @@ -0,0 +1 @@ +pub const IS_VARIANT_PREFIX: &str = "is_"; diff --git a/source/rust_verify/src/erase.rs b/source/rust_verify/src/erase.rs index 6fef22d15c..117b850859 100644 --- a/source/rust_verify/src/erase.rs +++ b/source/rust_verify/src/erase.rs @@ -994,6 +994,9 @@ fn erase_assoc_item(ctxt: &Ctxt, mctxt: &mut MCtxt, item: &AssocItem) -> Option< if vattrs.external { return Some(item.clone()); } + if vattrs.is_variant { + return None; + } let erased = erase_fn(ctxt, mctxt, f, vattrs.external_body); erased.map(|f| update_item(item, AssocItemKind::Fn(Box::new(f)))) } diff --git a/source/rust_verify/src/lib.rs b/source/rust_verify/src/lib.rs index f08ea4c519..901d42bff0 100644 --- a/source/rust_verify/src/lib.rs +++ b/source/rust_verify/src/lib.rs @@ -21,6 +21,7 @@ extern crate rustc_typeck; pub mod config; pub mod context; pub mod debugger; +pub mod def; pub mod driver; pub mod erase; pub mod file_loader; diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index 1238d95464..2cb1543251 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -8,9 +8,12 @@ For soundness's sake, be as defensive as possible: use crate::context::Context; use crate::rust_to_vir_adts::{check_item_enum, check_item_struct}; -use crate::rust_to_vir_base::{def_id_to_vir_path, get_mode, hack_get_def_name, mk_visibility}; +use crate::rust_to_vir_base::{ + def_id_to_vir_path, fn_item_hir_id_to_self_def_id, get_mode, get_verifier_attrs, + hack_get_def_name, mk_visibility, +}; use crate::rust_to_vir_func::{check_foreign_item_fn, check_item_fn}; -use crate::util::unsupported_err_span; +use crate::util::{err_span_str, unsupported_err_span}; use crate::{err_unless, unsupported_err, unsupported_err_unless, unsupported_unless}; use rustc_ast::Attribute; use rustc_hir::{ @@ -184,19 +187,49 @@ fn check_item<'tcx>( mk_visibility(&Some(module_path.clone()), &impl_item.vis); match &impl_item.kind { ImplItemKind::Fn(sig, body_id) => { - check_item_fn( - ctxt, - vir, - Some((self_path.clone(), adt_mode)), - impl_item.def_id.to_def_id(), - impl_item_visibility, - ctxt.tcx.hir().attrs(impl_item.hir_id()), - sig, - trait_path.clone(), - Some(&impll.generics), - &impl_item.generics, - body_id, - )?; + let fn_attrs = ctxt.tcx.hir().attrs(impl_item.hir_id()); + let fn_vattrs = get_verifier_attrs(fn_attrs)?; + if fn_vattrs.is_variant { + let valid = fn_item_hir_id_to_self_def_id( + ctxt.tcx, + impl_item.hir_id(), + ) + .map(|self_def_id| ctxt.tcx.adt_def(self_def_id)) + .and_then(|adt| { + impl_item + .ident + .as_str() + .strip_prefix(crate::def::IS_VARIANT_PREFIX) + .and_then(|variant_name| { + adt.variants.iter().find(|v| { + v.ident.as_str() == variant_name + }) + }) + }) + .is_some(); + if !valid + || get_mode(Mode::Exec, fn_attrs) != Mode::Spec + { + return err_span_str( + sig.span, + "invalid is_variant function, do not use #[verifier(is_variant)] directly, use the #[is_variant] macro instead", + ); + } + } else { + check_item_fn( + ctxt, + vir, + Some((self_path.clone(), adt_mode)), + impl_item.def_id.to_def_id(), + impl_item_visibility, + fn_attrs, + sig, + trait_path.clone(), + Some(&impll.generics), + &impl_item.generics, + body_id, + )?; + } } _ => unsupported_err!( item.span, diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs index 1dabfcff1b..5331ea31e4 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs @@ -47,6 +47,28 @@ pub(crate) fn typ_path_and_ident_to_vir_path<'tcx>(path: &Path, ident: vir::ast: return Arc::new(path); } +pub(crate) fn fn_item_hir_id_to_self_def_id<'tcx>( + tcx: TyCtxt<'tcx>, + hir_id: HirId, +) -> Option { + let parent_id = tcx.hir().get_parent_node(hir_id); + let parent_node = tcx.hir().get(parent_id); + match parent_node { + rustc_hir::Node::Item(rustc_hir::Item { + kind: rustc_hir::ItemKind::Impl(impll), .. + }) => match &impll.self_ty.kind { + rustc_hir::TyKind::Path(QPath::Resolved( + None, + rustc_hir::Path { res: rustc_hir::def::Res::Def(_, self_def_id), .. }, + )) => Some(*self_def_id), + _ => { + panic!("impl type is not given by a path"); + } + }, + _ => None, + } +} + pub(crate) fn def_id_to_vir_path<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Path { // The path that rustc gives a DefId might be given in terms of an 'impl' path // However, it makes for a better path name to use the path to the *type*. @@ -55,30 +77,9 @@ pub(crate) fn def_id_to_vir_path<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Path if let Some(local_id) = def_id.as_local() { let hir = tcx.hir().local_def_id_to_hir_id(local_id); if is_function_def_impl_item_node(tcx.hir().get(hir)) { - let parent_id = tcx.hir().get_parent_node(hir); - let parent_node = tcx.hir().get(parent_id); - match parent_node { - rustc_hir::Node::Item(rustc_hir::Item { - kind: rustc_hir::ItemKind::Impl(impll), - .. - }) => { - let ty_path = match &impll.self_ty.kind { - rustc_hir::TyKind::Path(QPath::Resolved( - None, - rustc_hir::Path { - res: rustc_hir::def::Res::Def(_, self_def_id), .. - }, - )) => def_path_to_vir_path(tcx, tcx.def_path(*self_def_id)), - _ => { - panic!("impl type is not given by a path"); - } - }; - return typ_path_and_ident_to_vir_path( - &ty_path, - def_to_path_ident(tcx, def_id), - ); - } - _ => {} + if let Some(self_def_id) = fn_item_hir_id_to_self_def_id(tcx, hir) { + let ty_path = def_path_to_vir_path(tcx, tcx.def_path(self_def_id)); + return typ_path_and_ident_to_vir_path(&ty_path, def_to_path_ident(tcx, def_id)); } } } @@ -267,6 +268,8 @@ pub(crate) enum Attr { Atomic, // specifies an invariant block InvariantBlock, + // an enum variant is_Variant + IsVariant, } fn get_trigger_arg(span: Span, attr_tree: &AttrTree) -> Result { @@ -328,6 +331,9 @@ pub(crate) fn parse_attrs(attrs: &[Attribute]) -> Result, VirErr> { Some(box [AttrTree::Fun(_, arg, None)]) if arg == "invariant_block" => { v.push(Attr::InvariantBlock) } + Some(box [AttrTree::Fun(_, arg, None)]) if arg == "is_variant" => { + v.push(Attr::IsVariant) + } Some(box [AttrTree::Fun(_, arg, Some(box [AttrTree::Fun(_, msg, None)]))]) if arg == "custom_req_err" => { @@ -428,6 +434,7 @@ pub(crate) struct VerifierAttrs { pub(crate) bit_vector: bool, pub(crate) unforgeable: bool, pub(crate) atomic: bool, + pub(crate) is_variant: bool, } pub(crate) fn get_verifier_attrs(attrs: &[Attribute]) -> Result { @@ -441,6 +448,7 @@ pub(crate) fn get_verifier_attrs(attrs: &[Attribute]) -> Result Result vs.bit_vector = true, Attr::Unforgeable => vs.unforgeable = true, Attr::Atomic => vs.atomic = true, + Attr::IsVariant => vs.is_variant = true, _ => {} } } diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index 057fa4c42c..3ab0a81b18 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -1,9 +1,10 @@ use crate::context::BodyCtxt; use crate::erase::ResolvedCall; use crate::rust_to_vir_base::{ - def_id_to_vir_path, def_to_path_ident, get_range, get_trigger, get_var_mode, hack_get_def_name, - ident_to_var, is_smt_arith, is_smt_equality, mid_ty_to_vir, mk_range, parse_attrs, ty_to_vir, - typ_of_node, typ_of_node_expect_mut_ref, typ_path_and_ident_to_vir_path, Attr, + def_id_to_vir_path, def_to_path_ident, get_range, get_trigger, get_var_mode, + get_verifier_attrs, hack_get_def_name, ident_to_var, is_smt_arith, is_smt_equality, + mid_ty_to_vir, mk_range, parse_attrs, ty_to_vir, typ_of_node, typ_of_node_expect_mut_ref, + typ_path_and_ident_to_vir_path, Attr, }; use crate::util::{ err_span_str, err_span_string, slice_vec_map_result, spanned_new, spanned_typed_new, @@ -269,6 +270,34 @@ fn fn_call_to_vir<'tcx>( def_id_to_vir_path(tcx, f) }; + let is_variant = { + match tcx.hir().get_if_local(f) { + Some(rustc_hir::Node::ImplItem( + impl_item + @ + rustc_hir::ImplItem { + kind: rustc_hir::ImplItemKind::Fn(..), + ident: fn_ident, + .. + }, + )) => { + let fn_attrs = bctx.ctxt.tcx.hir().attrs(impl_item.hir_id()); + let fn_vattrs = get_verifier_attrs(fn_attrs)?; + if fn_vattrs.is_variant { + let variant_name = fn_ident + .as_str() + .strip_prefix(crate::def::IS_VARIANT_PREFIX) + .expect("invalid is_variant function") + .to_string(); + Some(variant_name) + } else { + None + } + } + _ => None, + } + }; + let f_name = path_as_rust_name(&def_id_to_vir_path(tcx, f)); let is_admit = f_name == "builtin::admit"; let is_requires = f_name == "builtin::requires"; @@ -349,7 +378,7 @@ fn fn_call_to_vir<'tcx>( expr.span, "call of trait impl" ); - let name = Arc::new(FunX { path: path, trait_path: None }); + let name = Arc::new(FunX { path: path.clone(), trait_path: None }); record_fun( &bctx.ctxt, @@ -361,7 +390,8 @@ fn fn_call_to_vir<'tcx>( || is_assert_by || is_choose || is_assert_bit_vector - || is_old, + || is_old + || is_variant.is_some(), is_implies, ); @@ -488,7 +518,7 @@ fn fn_call_to_vir<'tcx>( } _ => expr_to_vir(bctx, arg, ExprModifier::Regular), })?; - if let Some(autoview_typ) = autoview_typ { + let self_path = if let Some(autoview_typ) = autoview_typ { // replace f(arg0, arg1, ..., argn) with f(arg0.view(), arg1, ..., argn) let typ_args = if let TypX::Datatype(_, args) = &**autoview_typ { args.clone() @@ -507,6 +537,19 @@ fn fn_call_to_vir<'tcx>( let target = CallTarget::Static(fun, typ_args); let viewx = ExprX::Call(target, Arc::new(vec![vir_args[0].clone()])); vir_args[0] = spanned_typed_new(expr.span, autoview_typ, viewx); + self_path + } else { + let mut self_path = path.clone(); + let self_path_mut = Arc::make_mut(&mut self_path); + Arc::make_mut(&mut self_path_mut.segments).pop(); + self_path + }; + + if let Some(variant_name) = is_variant { + return Ok(mk_expr(ExprX::UnaryOpr( + UnaryOpr::IsVariant { datatype: self_path, variant: str_ident(&variant_name) }, + vir_args.into_iter().next().expect("missing arg for is_variant"), + ))); } let is_smt_binary = if is_equal { diff --git a/source/rust_verify/tests/adts.rs b/source/rust_verify/tests/adts.rs index 232d6e7945..b769c57b5e 100644 --- a/source/rust_verify/tests/adts.rs +++ b/source/rust_verify/tests/adts.rs @@ -229,3 +229,43 @@ test_verify_one_file! { } } => Err(e) => assert_vir_error(e) } + +test_verify_one_file! { + #[test] test_is_variant_pass code! { + #[is_variant] + pub enum Maybe { + Some(T), + None, + } + + pub fn test1(m: Maybe) { + match m { + Maybe::Some(_) => assert(m.is_Some()), + Maybe::None => assert(m.is_None()), + }; + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] test_is_variant_illegal code! { + pub enum Maybe { + Some(T), + None, + } + + impl Maybe { + #[doc(hidden)] #[spec] #[verifier(is_variant)] #[allow(non_snake_case)] + fn is_Thing(&self) -> bool { ::core::panicking::panic("not implemented") } + } + } => Err(e) => assert_vir_error(e) +} + +test_verify_one_file! { + #[test] test_is_variant_not_enum code! { + #[is_variant] + pub struct Maybe { + t: T, + } + } => Err(_) +} From 4a975ba8d124adf9ae9dba4fd1f41a08e30d14c6 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 20 Jan 2022 20:38:33 +0100 Subject: [PATCH 2/6] Add a #[spec] .get_Variant() function to #[is_variant] enums with tuple constructors --- source/builtin_macros/src/is_variant.rs | 30 +++++++++++++++++++++---- source/rust_verify/example/adts.rs | 10 +++++++++ source/rust_verify/tests/adts.rs | 25 +++++++++++++++++++++ 3 files changed, 61 insertions(+), 4 deletions(-) diff --git a/source/builtin_macros/src/is_variant.rs b/source/builtin_macros/src/is_variant.rs index e2cb7c3500..80990f203e 100644 --- a/source/builtin_macros/src/is_variant.rs +++ b/source/builtin_macros/src/is_variant.rs @@ -14,16 +14,38 @@ pub fn attribute_is_variant( .variants() .iter() .map(|v| { - let variant_ident = v.ast().ident.to_string(); - + let variant_ident = v.ast().ident; + let variant_ident_str = variant_ident.to_string(); let fun_ident = - syn::Ident::new(&format!("is_{}", &variant_ident), v.ast().ident.span()); + syn::Ident::new(&format!("is_{}", &variant_ident_str), v.ast().ident.span()); + let get_ident = + syn::Ident::new(&format!("get_{}", &variant_ident_str), v.ast().ident.span()); + let get_fn = match v.ast().fields { + &syn::Fields::Named(_) | &syn::Fields::Unit => { quote! { } } + &syn::Fields::Unnamed(syn::FieldsUnnamed { unnamed: ref fields, .. }) => { + let field_tys = fields.iter().map(|f| &f.ty).collect::>(); + let field_idents = fields.iter().zip(0..).map(|(_, i)| syn::Ident::new(&format!("e{}", i), v.ast().ident.span())).collect::>(); + quote! { + #[allow(non_snake_case)] + #[spec] + pub fn #get_ident(self) -> (#(#field_tys),*,) { + match self { + #struct_name::#variant_ident(#(#field_idents),*) => (#(#field_idents),*,), + _ => arbitrary(), + } + } + } + }, + }; + quote! { #[doc(hidden)] #[spec] #[verifier(is_variant)] #[allow(non_snake_case)] - fn #fun_ident(&self) -> bool { unimplemented!() } + pub fn #fun_ident(&self) -> bool { unimplemented!() } + + #get_fn } }) .collect::(); diff --git a/source/rust_verify/example/adts.rs b/source/rust_verify/example/adts.rs index fa23ac0621..ae1a36ba64 100644 --- a/source/rust_verify/example/adts.rs +++ b/source/rust_verify/example/adts.rs @@ -48,5 +48,15 @@ fn test_is_variant_1(v: Vehicle2) { }; } +fn test_is_variant_2(v: Vehicle2) { + requires(v.is_Train() && v.get_Train().0); +} + +#[is_variant] +pub enum Maybe { + Some(T), + None, +} + fn main() { } diff --git a/source/rust_verify/tests/adts.rs b/source/rust_verify/tests/adts.rs index b769c57b5e..8f64fc9e92 100644 --- a/source/rust_verify/tests/adts.rs +++ b/source/rust_verify/tests/adts.rs @@ -269,3 +269,28 @@ test_verify_one_file! { } } => Err(_) } + +test_verify_one_file! { + #[test] test_is_variant_get code! { + #[is_variant] + pub enum Maybe { + Some(T), + None, + } + + pub fn test1(m: Maybe) { + requires(m.is_Some() && m.get_Some().0 > 10); + } + } => Ok(()) +} + +test_verify_one_file! { + #[test] test_is_variant_no_get code! { + #[is_variant] + pub enum Maybe { + // #[is_variant] won't generate a get_Some for this, but should not panic + Some { t: T }, + None, + } + } => Ok(()) +} From e88cef15a1b7cef56bcb4742c0566e288cecf91c Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 20 Jan 2022 21:04:32 +0100 Subject: [PATCH 3/6] Additional #[is_variant] tests --- source/rust_verify/tests/adts.rs | 45 ++++++++++++++++++++++---------- 1 file changed, 31 insertions(+), 14 deletions(-) diff --git a/source/rust_verify/tests/adts.rs b/source/rust_verify/tests/adts.rs index 8f64fc9e92..cba4197f0a 100644 --- a/source/rust_verify/tests/adts.rs +++ b/source/rust_verify/tests/adts.rs @@ -230,14 +230,16 @@ test_verify_one_file! { } => Err(e) => assert_vir_error(e) } -test_verify_one_file! { - #[test] test_is_variant_pass code! { - #[is_variant] - pub enum Maybe { - Some(T), - None, - } +const IS_VARIANT_MAYBE: &str = code_str! { + #[is_variant] + pub enum Maybe { + Some(T), + None, + } +}; +test_verify_one_file! { + #[test] test_is_variant_pass IS_VARIANT_MAYBE.to_string() + code_str! { pub fn test1(m: Maybe) { match m { Maybe::Some(_) => assert(m.is_Some()), @@ -271,19 +273,34 @@ test_verify_one_file! { } test_verify_one_file! { - #[test] test_is_variant_get code! { - #[is_variant] - pub enum Maybe { - Some(T), - None, - } - + #[test] test_is_variant_get_1 IS_VARIANT_MAYBE.to_string() + code_str! { pub fn test1(m: Maybe) { requires(m.is_Some() && m.get_Some().0 > 10); } } => Ok(()) } +test_verify_one_file! { + #[test] test_is_variant_get_2 IS_VARIANT_MAYBE.to_string() + code_str! { + pub fn test1(m: Maybe) -> bool { + ensures(|res: bool| + (m.is_Some() >>= res == (m.get_Some().0 == 3)) && + (m.is_None() >>= !res) + ); + match m { + Maybe::Some(v) => v == 3, + Maybe::None => false, + } + } + + pub fn test2() { + let m = Maybe::Some(3); + let res = test1(m); + assert(res); + } + } => Ok(()) +} + test_verify_one_file! { #[test] test_is_variant_no_get code! { #[is_variant] From 35cf52b3d42b55a5e16046618a416d0aa1cb1aea Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Fri, 21 Jan 2022 10:53:01 +0100 Subject: [PATCH 4/6] Change #[is-variant] accessor functions from get_Variant().x to .get_Variant_x() and encode them directly This is sound because a requires like ``` fn foo(m: Maybe) { requires(m.get_Some_0() == 3); // no facts about whether m.is_Some() or m.is_None() } ``` encoded as ``` (declare-fun req%foo. (Maybe) Bool) (axiom (forall ((m@ Maybe.)) (! (= (req%foo. m@) (and (axiom_location ("failed precondition") (= (Maybe./Some/_0 m@) 3)) )) :pattern ... ))) ``` is not a useful spec, but is not dangerous, as it is not possible to construct an `m == None` for which the precondition is true. --- source/builtin_macros/src/is_variant.rs | 41 +++++++------ source/docs/air/enum_field.air | 68 ++++++++++++++++++++++ source/rust_verify/Cargo.toml | 1 + source/rust_verify/example/adts.rs | 2 +- source/rust_verify/src/def.rs | 28 +++++++++ source/rust_verify/src/rust_to_vir.rs | 27 ++++++--- source/rust_verify/src/rust_to_vir_expr.rs | 35 ++++++----- source/rust_verify/tests/adts.rs | 21 ++++++- 8 files changed, 180 insertions(+), 43 deletions(-) create mode 100644 source/docs/air/enum_field.air diff --git a/source/builtin_macros/src/is_variant.rs b/source/builtin_macros/src/is_variant.rs index 80990f203e..06e1bbb24b 100644 --- a/source/builtin_macros/src/is_variant.rs +++ b/source/builtin_macros/src/is_variant.rs @@ -18,34 +18,39 @@ pub fn attribute_is_variant( let variant_ident_str = variant_ident.to_string(); let fun_ident = syn::Ident::new(&format!("is_{}", &variant_ident_str), v.ast().ident.span()); - let get_ident = - syn::Ident::new(&format!("get_{}", &variant_ident_str), v.ast().ident.span()); - let get_fn = match v.ast().fields { - &syn::Fields::Named(_) | &syn::Fields::Unit => { quote! { } } - &syn::Fields::Unnamed(syn::FieldsUnnamed { unnamed: ref fields, .. }) => { - let field_tys = fields.iter().map(|f| &f.ty).collect::>(); - let field_idents = fields.iter().zip(0..).map(|(_, i)| syn::Ident::new(&format!("e{}", i), v.ast().ident.span())).collect::>(); - quote! { - #[allow(non_snake_case)] - #[spec] - pub fn #get_ident(self) -> (#(#field_tys),*,) { - match self { - #struct_name::#variant_ident(#(#field_idents),*) => (#(#field_idents),*,), - _ => arbitrary(), + let get_fns = match v.ast().fields { + &syn::Fields::Named(_) | &syn::Fields::Unit => { + quote! {} + } + &syn::Fields::Unnamed(syn::FieldsUnnamed { unnamed: ref fields, .. }) => fields + .iter() + .zip(0..) + .map(|(f, i)| { + let field_ty = &f.ty; + let get_ident = syn::Ident::new( + &format!("get_{}_{}", variant_ident_str, i), + v.ast().ident.span(), + ); + + quote! { + #[spec] + #[allow(non_snake_case)] + #[verifier(is_variant)] + pub fn #get_ident(self) -> #field_ty { + unimplemented!() } } - } - }, + }) + .collect::(), }; quote! { - #[doc(hidden)] #[spec] #[verifier(is_variant)] #[allow(non_snake_case)] pub fn #fun_ident(&self) -> bool { unimplemented!() } - #get_fn + #get_fns } }) .collect::(); diff --git a/source/docs/air/enum_field.air b/source/docs/air/enum_field.air new file mode 100644 index 0000000000..39cb0b6254 --- /dev/null +++ b/source/docs/air/enum_field.air @@ -0,0 +1,68 @@ +(declare-datatypes () ( + (Maybe. + (Maybe./Some + (Maybe./Some/_0 Int) + ) + (Maybe./None) + ) +)) + +(check-valid + (declare-const m@ Maybe.) + (block + (assume + (= m@ (Maybe./None)) + ) + (assert ("000") (= (Maybe./Some/_0 m@) 3)) ; FAILS + ) +) + +(check-valid + (declare-const m@ Maybe.) + (block + (assume + (and + (is-Maybe./Some m@) + (= (Maybe./Some/_0 m@) 3) + ) + ) + (assert ("001") (= m@ (Maybe./Some 3))) + ) +) + +(check-valid + (declare-const m@ Maybe.) + (block + (assume + (and + (is-Maybe./None m@) + (= (Maybe./Some/_0 m@) 3) + ) + ) + (assert ("002a") + (= (Maybe./Some/_0 m@) 3) + ) + (assert ("002b") + (is-Maybe./None m@) + ) + ) +) + + (declare-fun req%foo. (Maybe.) Bool) + (axiom (forall ((m@ Maybe.)) (! + (= (req%foo. m@) (and + (axiom_location ("failed precondition") (= (Maybe./Some/_0 m@) 3)) + )) + ))) + +(check-valid + (declare-const m@ Maybe.) + (block + (assume + (is-Maybe./None m@) + ) + (assert ("003") ; FAILS + (req%foo. m@) + ) + ) +) diff --git a/source/rust_verify/Cargo.toml b/source/rust_verify/Cargo.toml index 0b8dce1cfb..d1dca06111 100644 --- a/source/rust_verify/Cargo.toml +++ b/source/rust_verify/Cargo.toml @@ -11,6 +11,7 @@ air = { path = "../air" } vir = { path = "../vir" } sise = "0.6.0" getopts = { git = "https://github.com/utaal/getopts.git", branch = "parse-partial" } +regex = "1" [target.'cfg(windows)'.dependencies] win32job = "1" diff --git a/source/rust_verify/example/adts.rs b/source/rust_verify/example/adts.rs index ae1a36ba64..3dd77482fa 100644 --- a/source/rust_verify/example/adts.rs +++ b/source/rust_verify/example/adts.rs @@ -49,7 +49,7 @@ fn test_is_variant_1(v: Vehicle2) { } fn test_is_variant_2(v: Vehicle2) { - requires(v.is_Train() && v.get_Train().0); + requires(v.is_Train() && v.get_Train_0()); } #[is_variant] diff --git a/source/rust_verify/src/def.rs b/source/rust_verify/src/def.rs index 559217ac72..c8c21c2c8e 100644 --- a/source/rust_verify/src/def.rs +++ b/source/rust_verify/src/def.rs @@ -1 +1,29 @@ +use regex::Regex; + pub const IS_VARIANT_PREFIX: &str = "is_"; +pub const GET_VARIANT_PREFIX: &str = "get_"; + +/// Returns `Some((name, field))` if the ident matches the expected name for #[is_variant] functions +/// `name` is the variant name +/// `field` is `Some(num)` if this was a `.get_Variant_num()` function +/// `field` is `None` if this was a `.is_Variant` function +pub(crate) fn is_get_variant_fn_name( + ident: &rustc_span::symbol::Ident, +) -> Option<(String, Option)> { + let fn_name = ident.as_str(); + fn_name.strip_prefix(crate::def::IS_VARIANT_PREFIX).map(|n| (n.to_string(), None)).or_else( + || { + let re = + Regex::new(&("^".to_string() + crate::def::GET_VARIANT_PREFIX + r"(.*)_(\d+)$")) + .unwrap(); + re.captures(&fn_name).and_then(|c| { + c.get(2) + .unwrap() + .as_str() + .parse::() + .ok() + .map(|f| (c.get(1).unwrap().as_str().to_string(), Some(f))) + }) + }, + ) +} diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index 2cb1543251..41b911fd5e 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -7,6 +7,7 @@ For soundness's sake, be as defensive as possible: */ use crate::context::Context; +use crate::def::is_get_variant_fn_name; use crate::rust_to_vir_adts::{check_item_enum, check_item_struct}; use crate::rust_to_vir_base::{ def_id_to_vir_path, fn_item_hir_id_to_self_def_id, get_mode, get_verifier_attrs, @@ -196,15 +197,23 @@ fn check_item<'tcx>( ) .map(|self_def_id| ctxt.tcx.adt_def(self_def_id)) .and_then(|adt| { - impl_item - .ident - .as_str() - .strip_prefix(crate::def::IS_VARIANT_PREFIX) - .and_then(|variant_name| { - adt.variants.iter().find(|v| { - v.ident.as_str() == variant_name - }) - }) + is_get_variant_fn_name(&impl_item.ident).and_then( + |(variant_name, variant_field)| { + adt.variants + .iter() + .find(|v| { + v.ident.as_str() == variant_name + }) + .and_then(|variant| { + if let Some(field) = variant_field { + (field < variant.fields.len()) + .then(|| ()) + } else { + Some(()) + } + }) + }, + ) }) .is_some(); if !valid diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index 3ab0a81b18..a8f9bc6b97 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -1,4 +1,5 @@ use crate::context::BodyCtxt; +use crate::def::is_get_variant_fn_name; use crate::erase::ResolvedCall; use crate::rust_to_vir_base::{ def_id_to_vir_path, def_to_path_ident, get_range, get_trigger, get_var_mode, @@ -270,7 +271,7 @@ fn fn_call_to_vir<'tcx>( def_id_to_vir_path(tcx, f) }; - let is_variant = { + let is_get_variant = { match tcx.hir().get_if_local(f) { Some(rustc_hir::Node::ImplItem( impl_item @@ -284,12 +285,7 @@ fn fn_call_to_vir<'tcx>( let fn_attrs = bctx.ctxt.tcx.hir().attrs(impl_item.hir_id()); let fn_vattrs = get_verifier_attrs(fn_attrs)?; if fn_vattrs.is_variant { - let variant_name = fn_ident - .as_str() - .strip_prefix(crate::def::IS_VARIANT_PREFIX) - .expect("invalid is_variant function") - .to_string(); - Some(variant_name) + Some(is_get_variant_fn_name(fn_ident).expect("invalid is_variant function")) } else { None } @@ -391,7 +387,7 @@ fn fn_call_to_vir<'tcx>( || is_choose || is_assert_bit_vector || is_old - || is_variant.is_some(), + || is_get_variant.is_some(), is_implies, ); @@ -545,11 +541,24 @@ fn fn_call_to_vir<'tcx>( self_path }; - if let Some(variant_name) = is_variant { - return Ok(mk_expr(ExprX::UnaryOpr( - UnaryOpr::IsVariant { datatype: self_path, variant: str_ident(&variant_name) }, - vir_args.into_iter().next().expect("missing arg for is_variant"), - ))); + match is_get_variant { + Some((variant_name, None)) => { + return Ok(mk_expr(ExprX::UnaryOpr( + UnaryOpr::IsVariant { datatype: self_path, variant: str_ident(&variant_name) }, + vir_args.into_iter().next().expect("missing arg for is_variant"), + ))); + } + Some((variant_name, Some(variant_field))) => { + return Ok(mk_expr(ExprX::UnaryOpr( + UnaryOpr::Field { + datatype: self_path, + variant: str_ident(&variant_name), + field: positional_field_ident(variant_field), + }, + vir_args.into_iter().next().expect("missing arg for is_variant"), + ))); + } + None => {} } let is_smt_binary = if is_equal { diff --git a/source/rust_verify/tests/adts.rs b/source/rust_verify/tests/adts.rs index cba4197f0a..dac033bc24 100644 --- a/source/rust_verify/tests/adts.rs +++ b/source/rust_verify/tests/adts.rs @@ -275,7 +275,7 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_is_variant_get_1 IS_VARIANT_MAYBE.to_string() + code_str! { pub fn test1(m: Maybe) { - requires(m.is_Some() && m.get_Some().0 > 10); + requires(m.is_Some() && m.get_Some_0() > 10); } } => Ok(()) } @@ -284,7 +284,7 @@ test_verify_one_file! { #[test] test_is_variant_get_2 IS_VARIANT_MAYBE.to_string() + code_str! { pub fn test1(m: Maybe) -> bool { ensures(|res: bool| - (m.is_Some() >>= res == (m.get_Some().0 == 3)) && + (m.is_Some() >>= res == (m.get_Some_0() == 3)) && (m.is_None() >>= !res) ); match m { @@ -298,6 +298,15 @@ test_verify_one_file! { let res = test1(m); assert(res); } + + pub fn test3(v: Maybe) { + requires(v.is_Some() && v.get_Some_0() == 5); + if let Maybe::Some(a) = v { + assert(a == 5); + } else { + unreached::<()>(); + } + } } => Ok(()) } @@ -311,3 +320,11 @@ test_verify_one_file! { } } => Ok(()) } + +test_verify_one_file! { + #[test] test_is_variant_no_field IS_VARIANT_MAYBE.to_string() + code_str! { + fn test1(v: Maybe) { + assert(v.get_Some_1() == 3); + } + } => Err(_) // type-checking error +} From d2e8869aa85bde74dfbce9c55cb86fec7b90f589 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Fri, 21 Jan 2022 10:57:16 +0100 Subject: [PATCH 5/6] Add test, and fix assumption in the mode checker --- source/rust_verify/tests/adts.rs | 19 +++++++++++++++++++ source/vir/src/modes.rs | 4 ++-- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/source/rust_verify/tests/adts.rs b/source/rust_verify/tests/adts.rs index dac033bc24..5f1364d749 100644 --- a/source/rust_verify/tests/adts.rs +++ b/source/rust_verify/tests/adts.rs @@ -310,6 +310,25 @@ test_verify_one_file! { } => Ok(()) } +test_verify_one_file! { + #[test] test_is_variant_get_fail IS_VARIANT_MAYBE.to_string() + code_str! { + pub fn test1(m: Maybe) -> u64 { + requires(m.get_Some_0() == 4); + if let Maybe::Some(v) = m { + v + } else { + unreached() // FAILS + } + } + + pub fn test2() { + let m = Maybe::None; + assume(m.get_Some_0() == 4); + test1(m); + } + } => Err(e) => assert_one_fails(e) +} + test_verify_one_file! { #[test] test_is_variant_no_get code! { #[is_variant] diff --git a/source/vir/src/modes.rs b/source/vir/src/modes.rs index b448050325..8307d6ca9a 100644 --- a/source/vir/src/modes.rs +++ b/source/vir/src/modes.rs @@ -285,10 +285,10 @@ fn check_expr(typing: &mut Typing, outer_mode: Mode, expr: &Expr) -> Result panic!("internal error: HasType in modes.rs"), ExprX::UnaryOpr(UnaryOpr::IsVariant { .. }, e1) => check_expr(typing, outer_mode, e1), ExprX::UnaryOpr(UnaryOpr::TupleField { .. }, e1) => check_expr(typing, outer_mode, e1), - ExprX::UnaryOpr(UnaryOpr::Field { datatype, variant: _, field }, e1) => { + ExprX::UnaryOpr(UnaryOpr::Field { datatype, variant, field }, e1) => { let e1_mode = check_expr(typing, outer_mode, e1)?; let datatype = &typing.datatypes[datatype]; - let field = get_field(&datatype.x.get_only_variant().a, field); + let field = get_field(&datatype.x.get_variant(variant).a, field); Ok(mode_join(e1_mode, field.a.1)) } ExprX::Binary(op, e1, e2) => { From 73cab81f983bcfa1b37cfc03b4e0236d136a0830 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Tue, 25 Jan 2022 23:30:55 +0100 Subject: [PATCH 6/6] Add #[spec] .get_Variant_field() accessor functions to #[is_variant] enums with variants with named fields --- source/builtin_macros/src/is_variant.rs | 27 ++++++++++++++++--- source/rust_verify/src/def.rs | 27 ++++++++++++------- source/rust_verify/src/rust_to_vir.rs | 23 +++++++++++++---- source/rust_verify/src/rust_to_vir_expr.rs | 11 +++++--- source/rust_verify/tests/adts.rs | 30 ++++++++++++++++++---- 5 files changed, 93 insertions(+), 25 deletions(-) diff --git a/source/builtin_macros/src/is_variant.rs b/source/builtin_macros/src/is_variant.rs index 06e1bbb24b..20c04e739e 100644 --- a/source/builtin_macros/src/is_variant.rs +++ b/source/builtin_macros/src/is_variant.rs @@ -19,9 +19,29 @@ pub fn attribute_is_variant( let fun_ident = syn::Ident::new(&format!("is_{}", &variant_ident_str), v.ast().ident.span()); let get_fns = match v.ast().fields { - &syn::Fields::Named(_) | &syn::Fields::Unit => { - quote! {} - } + &syn::Fields::Named(syn::FieldsNamed { named: ref fields, .. }) => fields + .iter() + .map(|f| { + let field_ty = &f.ty; + let get_ident = syn::Ident::new( + &format!( + "get_{}_{}", + variant_ident_str, + f.ident.as_ref().expect("missing field ident").to_string() + ), + v.ast().ident.span(), + ); + + quote! { + #[spec] + #[allow(non_snake_case)] + #[verifier(is_variant)] + pub fn #get_ident(self) -> #field_ty { + unimplemented!() + } + } + }) + .collect::(), &syn::Fields::Unnamed(syn::FieldsUnnamed { unnamed: ref fields, .. }) => fields .iter() .zip(0..) @@ -42,6 +62,7 @@ pub fn attribute_is_variant( } }) .collect::(), + &syn::Fields::Unit => quote! {}, }; quote! { diff --git a/source/rust_verify/src/def.rs b/source/rust_verify/src/def.rs index c8c21c2c8e..4ba0a5aa86 100644 --- a/source/rust_verify/src/def.rs +++ b/source/rust_verify/src/def.rs @@ -3,26 +3,35 @@ use regex::Regex; pub const IS_VARIANT_PREFIX: &str = "is_"; pub const GET_VARIANT_PREFIX: &str = "get_"; +pub(crate) enum FieldName { + Named(String), + Unnamed(usize), +} + /// Returns `Some((name, field))` if the ident matches the expected name for #[is_variant] functions /// `name` is the variant name /// `field` is `Some(num)` if this was a `.get_Variant_num()` function /// `field` is `None` if this was a `.is_Variant` function pub(crate) fn is_get_variant_fn_name( ident: &rustc_span::symbol::Ident, -) -> Option<(String, Option)> { +) -> Option<(String, Option)> { let fn_name = ident.as_str(); fn_name.strip_prefix(crate::def::IS_VARIANT_PREFIX).map(|n| (n.to_string(), None)).or_else( || { let re = - Regex::new(&("^".to_string() + crate::def::GET_VARIANT_PREFIX + r"(.*)_(\d+)$")) + Regex::new(&("^".to_string() + crate::def::GET_VARIANT_PREFIX + r"(.+)_(.+)$")) .unwrap(); - re.captures(&fn_name).and_then(|c| { - c.get(2) - .unwrap() - .as_str() - .parse::() - .ok() - .map(|f| (c.get(1).unwrap().as_str().to_string(), Some(f))) + re.captures(&fn_name).map(|c| { + let f_name = c.get(2).unwrap().as_str().to_string(); + let v_name = c.get(1).unwrap().as_str().to_string(); + + ( + v_name, + Some(match f_name.parse::().ok() { + Some(i) => FieldName::Unnamed(i), + None => FieldName::Named(f_name), + }), + ) }) }, ) diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index 41b911fd5e..5ec436cd89 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -205,11 +205,24 @@ fn check_item<'tcx>( v.ident.as_str() == variant_name }) .and_then(|variant| { - if let Some(field) = variant_field { - (field < variant.fields.len()) - .then(|| ()) - } else { - Some(()) + use crate::def::FieldName; + match variant_field { + Some(FieldName::Named( + f_name, + )) => variant + .fields + .iter() + .find(|f| { + f.ident.as_str() + == f_name + }) + .map(|_| ()), + Some(FieldName::Unnamed( + f_num, + )) => (f_num + < variant.fields.len()) + .then(|| ()), + None => Some(()), } }) }, diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index a8f9bc6b97..6da000f1e4 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -549,11 +549,16 @@ fn fn_call_to_vir<'tcx>( ))); } Some((variant_name, Some(variant_field))) => { + use crate::def::FieldName; + let variant_name_ident = str_ident(&variant_name); return Ok(mk_expr(ExprX::UnaryOpr( UnaryOpr::Field { - datatype: self_path, - variant: str_ident(&variant_name), - field: positional_field_ident(variant_field), + datatype: self_path.clone(), + variant: variant_name_ident.clone(), + field: match variant_field { + FieldName::Unnamed(i) => positional_field_ident(i), + FieldName::Named(f) => str_ident(&f), + }, }, vir_args.into_iter().next().expect("missing arg for is_variant"), ))); diff --git a/source/rust_verify/tests/adts.rs b/source/rust_verify/tests/adts.rs index 5f1364d749..6d90ba73f7 100644 --- a/source/rust_verify/tests/adts.rs +++ b/source/rust_verify/tests/adts.rs @@ -330,12 +330,32 @@ test_verify_one_file! { } test_verify_one_file! { - #[test] test_is_variant_no_get code! { + #[test] test_is_variant_get_named_field code! { #[is_variant] - pub enum Maybe { - // #[is_variant] won't generate a get_Some for this, but should not panic - Some { t: T }, - None, + pub enum Res { + Ok { t: T }, + Err { v: u64 }, + } + + fn test1(m: Res) { + requires(m.is_Err() && m.get_Err_v() == 42); + match m { + Res::Ok { .. } => assert(false), + Res::Err { v } => assert(v == 42), + }; + } + + fn test2(m: &Res) -> bool { + ensures(|res: bool| equal(res, m.is_Ok() && m.get_Ok_t())); + match m { + Res::Ok { t } if *t => true, + _ => false, + } + } + + fn caller() { + let r = test2(&Res::Ok { t: false }); + assert(!r); } } => Ok(()) }