Add #[is_variant] to enable adt.is_Variant() and adt.get_Variant()

source/builtin_macros/src/is_variant.rs

@@ -0,0 +1,88 @@
+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;
+            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_fns = match v.ast().fields {
+                &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::<proc_macro2::TokenStream>(),
+                &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::<proc_macro2::TokenStream>(),
+                &syn::Fields::Unit => quote! {},
+            };
+
+            quote! {
+                #[spec]
+                #[verifier(is_variant)]
+                #[allow(non_snake_case)]
+                pub fn #fun_ident(&self) -> bool { unimplemented!() }
+
+                #get_fns
+            }
+        })
+        .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/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@)
+  )
+ )
+)

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"

source/rust_verify/example/adts.rs

@@ -11,30 +11,52 @@ 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 test_is_variant_2(v: Vehicle2<u64>) {
+    requires(v.is_Train() && v.get_Train_0());
+}
+
+#[is_variant]
+pub enum Maybe<T> {
+    Some(T),
+    None,
+}
 
 fn main() {
 }

source/rust_verify/src/def.rs

@@ -0,0 +1,38 @@
+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<FieldName>)> {
+    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"(.+)_(.+)$"))
+                    .unwrap();
+            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::<usize>().ok() {
+                        Some(i) => FieldName::Unnamed(i),
+                        None => FieldName::Named(f_name),
+                    }),
+                )
+            })
+        },
+    )
+}

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;