Add #[is_variant] to enable adt.is_Variant() functions that are direc…

…tly encoded to SMT (is-Variant)

source/builtin_macros/src/is_variant.rs

@@ -0,0 +1,36 @@
+use quote::quote;
+
+pub fn attribute_is_variant(
+    _attr: proc_macro2::TokenStream,
+    s: synstructure::Structure,
+) -> proc_macro2::TokenStream {
+    let ast = &s.ast();
+    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::<proc_macro2::TokenStream>();
+
+    let generics = &ast.generics;
+    quote! {
+        #ast
+
+        #[automatically_derived]
+        impl#generics #struct_name#generics {
+            #is_impls
+        }
+    }
+}

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::<proc_macro2::TokenStream>();
-    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);

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::<proc_macro2::TokenStream>();
+    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
+            }
+        }
+    })
+}

source/rust_verify/example/adts.rs

@@ -11,30 +11,42 @@ struct Car<P> {
 
 #[derive(Structural, PartialEq, Eq)]
 enum Vehicle {
-    Car(Car<int>),
+    Car(Car<u64>),
     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<T> {
+    Car(Car<T>),
+    Train(bool),
+}
+
+fn test_is_variant_1(v: Vehicle2<u64>) {
+    match v {
+        Vehicle2::Car(_) => assert(v.is_Car()),
+        Vehicle2::Train(_) => assert(v.is_Train()),
+    };
+}
 
 fn main() {
 }

source/rust_verify/src/def.rs

@@ -0,0 +1 @@
+pub const IS_VARIANT_PREFIX: &str = "is_";

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))))
         }

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;

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,13 +187,44 @@ fn check_item<'tcx>(
                                     mk_visibility(&Some(module_path.clone()), &impl_item.vis);
                                 match &impl_item.kind {
                                     ImplItemKind::Fn(sig, 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 {
+                                            // TODO: refactor when #31 is merged
+                                            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",
+                                                );
+                                            }
+                                            return Ok(());
+                                        }
                                         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()),
+                                            fn_attrs,
                                             sig,
                                             trait_path.clone(),
                                             Some(&impll.generics),

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<DefId> {
+    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<u64, VirErr> {
@@ -328,6 +331,9 @@ pub(crate) fn parse_attrs(attrs: &[Attribute]) -> Result<Vec<Attr>, 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<VerifierAttrs, VirErr> {
@@ -441,6 +448,7 @@ pub(crate) fn get_verifier_attrs(attrs: &[Attribute]) -> Result<VerifierAttrs, V
         bit_vector: false,
         unforgeable: false,
         atomic: false,
+        is_variant: false,
     };
     for attr in parse_attrs(attrs)? {
         match attr {
@@ -453,6 +461,7 @@ pub(crate) fn get_verifier_attrs(attrs: &[Attribute]) -> Result<VerifierAttrs, V
             Attr::BitVector => vs.bit_vector = true,
             Attr::Unforgeable => vs.unforgeable = true,
             Attr::Atomic => vs.atomic = true,
+            Attr::IsVariant => vs.is_variant = true,
             _ => {}
         }
     }