Merge pull request rust-lang#18 from utaal/structural

Use the `builtin::Structural` trait to mark types that support structural equality

Author: utaal

verify/Cargo.toml

@@ -2,6 +2,7 @@
 members = [
   "air",
   "builtin",
+  "builtin_macros",
   "vir",
   "rust_verify",
   "rust_verify_test_macros",

verify/builtin/Cargo.toml

@@ -3,5 +3,4 @@ name = "builtin"
 version = "0.1.0"
 authors = ["Chris Hawblitzel <[email protected]>"]
 edition = "2018"
-
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

verify/builtin/src/lib.rs

@@ -1,3 +1,5 @@
+#![feature(rustc_attrs)]
+
 pub fn admit() {
     unimplemented!();
 }
@@ -141,3 +143,31 @@ impl std::cmp::Ord for nat {
         unimplemented!()
     }
 }
+
+// TODO(andreal) bake this into the compiler as a lang_item
+#[rustc_diagnostic_item = "builtin::Structural"]
+pub trait Structural {
+    #[doc(hidden)]
+    fn assert_receiver_is_structural(&self) -> () {}
+}
+
+#[doc(hidden)]
+pub struct AssertParamIsStructural<T: Structural + ?Sized> {
+    _field: std::marker::PhantomData<T>,
+}
+
+macro_rules! impl_structural {
+    ($($t:ty)*) => {
+        $(
+            impl Structural for $t { }
+        )*
+    }
+}
+
+impl_structural! {
+    int nat
+    usize u8 u16 u32 u64 u128
+    isize i8 i16 i32 i64 i128
+    // TODO: support f32 f64 ?
+    bool char
+}

verify/builtin_macros/Cargo.toml

@@ -0,0 +1,14 @@
+[package]
+name = "builtin_macros"
+version = "0.1.0"
+authors = ["Chris Hawblitzel <[email protected]>", "Andrea Lattuada <[email protected]>"]
+edition = "2018"
+
+[lib]
+proc-macro = true
+
+[dependencies]
+proc-macro2 = "1.0"
+quote = "1.0"
+synstructure = "0.12"
+syn = "1.0"

verify/builtin_macros/src/lib.rs

@@ -0,0 +1,28 @@
+use quote::quote;
+use synstructure::decl_derive;
+
+decl_derive!([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
+            }
+        }
+    })
+}

verify/rust_verify/example/structural.rs

@@ -0,0 +1,26 @@
+extern crate builtin;
+#[macro_use] extern crate builtin_macros;
+use builtin::*;
+mod pervasive;
+use pervasive::*;
+
+#[derive(Eq)]
+struct Thing { }
+
+impl std::cmp::PartialEq for Thing {
+    fn eq(&self, _: &Self) -> bool { todo!() }
+}
+
+#[derive(PartialEq, Eq, Structural)]
+struct Car<T> {
+    passengers: T,
+    four_doors: bool,
+}
+
+fn one() {
+    let c1 = Car { passengers: Thing { }, four_doors: true };
+    let c2 = Car { passengers: Thing { }, four_doors: true };
+    assert(c1 == c2);
+}
+
+fn main() { }

verify/rust_verify/src/main.rs

@@ -25,11 +25,13 @@ pub fn main() {
     // Run verifier callback to build VIR tree and run verifier
     let mut verifier = Verifier::new(our_args);
     let status = rustc_driver::RunCompiler::new(&rustc_args, &mut verifier).run();
-    println!(
-        "Verification results:: verified: {} errors: {}",
-        verifier.count_verified,
-        verifier.errors.len()
-    );
+    if !verifier.encountered_vir_error {
+        println!(
+            "Verification results:: verified: {} errors: {}",
+            verifier.count_verified,
+            verifier.errors.len()
+        );
+    }
     match status {
         Ok(_) => {}
         Err(_) => {

verify/rust_verify/src/rust_to_vir.rs

@@ -10,7 +10,7 @@ use crate::rust_to_vir_adts::{check_item_enum, check_item_struct};
 use crate::rust_to_vir_base::{hack_check_def_name, hack_get_def_name};
 use crate::rust_to_vir_func::{check_foreign_item_fn, check_item_fn};
 use crate::util::unsupported_err_span;
-use crate::{unsupported_err, unsupported_err_unless, unsupported_unless};
+use crate::{err_unless, unsupported_err, unsupported_err_unless, unsupported_unless};
 use rustc_ast::Attribute;
 use rustc_hir::{
     Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, Item, ItemId, ItemKind, ModuleItems,
@@ -62,11 +62,52 @@ fn check_item<'tcx>(
                             "core",
                             "marker::StructuralPartialEq"
                         )
-                        || hack_check_def_name(tcx, path.res.def_id(), "core", "cmp::PartialEq"),
+                        || hack_check_def_name(tcx, path.res.def_id(), "core", "cmp::PartialEq")
+                        || hack_check_def_name(tcx, path.res.def_id(), "builtin", "Structural"),
                     item.span,
                     "non_eq_trait_impl",
                     path
                 );
+                if hack_check_def_name(tcx, path.res.def_id(), "builtin", "Structural") {
+                    let ty = {
+                        // TODO extract to rust_to_vir_base, or use
+                        // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_typeck/fn.hir_ty_to_ty.html
+                        // ?
+                        let def_id = match impll.self_ty.kind {
+                            rustc_hir::TyKind::Path(QPath::Resolved(None, path)) => {
+                                path.res.def_id()
+                            }
+                            _ => panic!(
+                                "self type of impl is not resolved: {:?}",
+                                impll.self_ty.kind
+                            ),
+                        };
+                        tcx.type_of(def_id)
+                    };
+                    // TODO: this may be a bit of a hack: to query the TyCtxt for the StructuralEq impl it seems we need
+                    // a concrete type, so apply ! to all type parameters
+                    let ty_kind_applied_never =
+                        if let rustc_middle::ty::TyKind::Adt(def, substs) = ty.kind() {
+                            rustc_middle::ty::TyKind::Adt(
+                                def,
+                                tcx.mk_substs(substs.iter().map(|g| match g.unpack() {
+                                    rustc_middle::ty::subst::GenericArgKind::Type(_) => {
+                                        (*tcx).types.never.into()
+                                    }
+                                    _ => g,
+                                })),
+                            )
+                        } else {
+                            panic!("Structural impl for non-adt type");
+                        };
+                    let ty_applied_never = tcx.mk_ty(ty_kind_applied_never);
+                    err_unless!(
+                        ty_applied_never.is_structural_eq_shallow(tcx),
+                        item.span,
+                        format!("Structural impl for non-structural type {:?}", ty),
+                        ty
+                    );
+                }
             } else {
                 unsupported_err_unless!(
                     impll.of_trait.is_none(),
@@ -93,6 +134,15 @@ fn check_item<'tcx>(
                 }
             }
         }
+        ItemKind::Const(_ty, _body_id) => {
+            unsupported_err_unless!(
+                hack_get_def_name(tcx, _body_id.hir_id.owner.to_def_id())
+                    .starts_with("_DERIVE_builtin_Structural_FOR_"),
+                item.span,
+                "unsupported const",
+                item
+            );
+        }
         _ => {
             unsupported_err!(item.span, "unsupported item", item);
         }
@@ -118,7 +168,8 @@ fn check_module<'tcx>(
                 unsupported_unless!(
                     def_name == "assert_receiver_is_total_eq"
                         || def_name == "eq"
-                        || def_name == "ne",
+                        || def_name == "ne"
+                        || def_name == "assert_receiver_is_structural",
                     "impl definition in module",
                     id
                 );
@@ -207,7 +258,8 @@ pub fn crate_to_vir<'tcx>(tcx: TyCtxt<'tcx>, krate: &'tcx Crate<'tcx>) -> Result
         unsupported_unless!(
             impl_item_ident == "assert_receiver_is_total_eq"
                 || impl_item_ident == "eq"
-                || impl_item_ident == "ne",
+                || impl_item_ident == "ne"
+                || impl_item_ident == "assert_receiver_is_structural",
             "impl definition",
             impl_item
         );
@@ -217,7 +269,8 @@ pub fn crate_to_vir<'tcx>(tcx: TyCtxt<'tcx>, krate: &'tcx Crate<'tcx>) -> Result
             hack_check_def_name(tcx, *id, "core", "marker::StructuralEq")
                 || hack_check_def_name(tcx, *id, "core", "cmp::Eq")
                 || hack_check_def_name(tcx, *id, "core", "marker::StructuralPartialEq")
-                || hack_check_def_name(tcx, *id, "core", "cmp::PartialEq"),
+                || hack_check_def_name(tcx, *id, "core", "cmp::PartialEq")
+                || hack_check_def_name(tcx, *id, "builtin", "Structural"),
             "non_eq_trait_impl",
             id
         );

verify/rust_verify/src/rust_to_vir_base.rs

@@ -1,5 +1,5 @@
-use crate::util::{err_span_str, err_span_string, unsupported_err_span, warning_span};
-use crate::{unsupported, unsupported_err, unsupported_err_unless, unsupported_unless};
+use crate::util::{err_span_str, err_span_string, unsupported_err_span};
+use crate::{unsupported, unsupported_err, unsupported_err_unless};
 use rustc_ast::token::{Token, TokenKind};
 use rustc_ast::tokenstream::TokenTree;
 use rustc_ast::{AttrKind, Attribute, IntTy, MacArgs, UintTy};
@@ -12,7 +12,7 @@ use rustc_span::symbol::Ident;
 use rustc_span::Span;
 use std::rc::Rc;
 use vir::ast::{Idents, IntRange, Mode, Path, Typ, TypX, VirErr};
-use vir::ast_util::{path_to_string, types_equal};
+use vir::ast_util::types_equal;
 
 pub(crate) fn def_to_path<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Path {
     Rc::new(tcx.def_path(def_id).data.iter().map(|d| Rc::new(format!("{}", d))).collect::<Vec<_>>())
@@ -268,46 +268,28 @@ pub(crate) fn typ_of_node<'tcx>(ctxt: &Ctxt<'tcx>, id: &HirId) -> Typ {
 // Do equality operations on these operands translate into the SMT solver's == operation?
 pub(crate) fn is_smt_equality<'tcx>(
     ctxt: &Ctxt<'tcx>,
-    span: Span,
+    _span: Span,
     id1: &HirId,
     id2: &HirId,
 ) -> bool {
     let (t1, t2) = (typ_of_node(ctxt, id1), typ_of_node(ctxt, id2));
     match (&*t1, &*t2) {
         (TypX::Bool, TypX::Bool) => true,
         (TypX::Int(_), TypX::Int(_)) => true,
-        (TypX::Path(p), TypX::Path(_)) if types_equal(&t1, &t2) => {
-            // TODO: a type may provide a custom PartialEq implementation, or have interior
-            // mutability; this means that PartialEq::eq may not be the same as structural
-            // (member-wise) adt equality. We should check whether the PartialEq implementation
-            // is compatible with adt equality before allowing these. For now, warn that there
-            // may be unsoundness.
-            // As used here, StructuralEq is only sufficient for a shallow check.
-            // In the rust doc for `StructuralEq`:
-            // > Any type that derives Eq automatically implements this trait,
-            // > regardless of whether its type parameters implement Eq.
-            warning_span(
-                span,
-                format!(
-                    "the verifier will assume structural equality for {}, which may be un sound",
-                    path_to_string(p)
-                ),
-            );
-            let struct_eq_def_id = ctxt
+        (TypX::Path(_), TypX::Path(_)) if types_equal(&t1, &t2) => {
+            let structural_def_id = ctxt
                 .tcx
-                .lang_items()
-                .structural_teq_trait()
-                .expect("structural eq trait is not defined");
+                .get_diagnostic_item(rustc_span::Symbol::intern("builtin::Structural"))
+                .expect("structural trait is not defined");
             let ty = ctxt.types.node_type(*id1);
-            let substs_ref = ctxt.tcx.mk_substs_trait(ty, &[]);
-            let type_impls_struct_eq = ctxt.tcx.type_implements_trait((
-                struct_eq_def_id,
+            let substs_ref = ctxt.tcx.mk_substs([].iter());
+            let ty_impls_structural = ctxt.tcx.type_implements_trait((
+                structural_def_id,
                 ty,
                 substs_ref,
                 rustc_middle::ty::ParamEnv::empty(),
             ));
-            unsupported_unless!(type_impls_struct_eq, "eq_for_non_structural_eq");
-            true
+            ty_impls_structural
         }
         _ => false,
     }

verify/rust_verify/src/rust_to_vir_expr.rs

@@ -480,8 +480,9 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
             let vlhs = expr_to_vir(ctxt, lhs)?;
             let vrhs = expr_to_vir(ctxt, rhs)?;
             match op.node {
-                BinOpKind::Eq | BinOpKind::Ne => unsupported_unless!(
+                BinOpKind::Eq | BinOpKind::Ne => unsupported_err_unless!(
                     is_smt_equality(ctxt, expr.span, &lhs.hir_id, &rhs.hir_id),
+                    expr.span,
                     "==/!= for non smt equality types",
                     expr
                 ),

verify/rust_verify/src/util.rs

@@ -58,6 +58,22 @@ macro_rules! unsupported_err_unless {
     };
 }
 
+#[macro_export]
+macro_rules! err_unless {
+    ($assertion: expr, $span: expr, $msg: expr) => {
+        if (!$assertion) {
+            dbg!();
+            crate::util::err_span_string($span, $msg)?;
+        }
+    };
+    ($assertion: expr, $span: expr, $msg: expr, $info: expr) => {
+        if (!$assertion) {
+            dbg!($info);
+            crate::util::err_span_string($span, $msg)?;
+        }
+    };
+}
+
 #[macro_export]
 macro_rules! unsupported {
     ($msg: expr) => {{ panic!("The verifier does not yet support the following Rust feature: {}", $msg) }};