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

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

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