Clean up dead code and resolved TODO

Author: utaal

verify/rust_verify/src/rust_to_vir.rs

@@ -69,10 +69,6 @@ fn check_item<'tcx>(
                     path
                 );
                 if hack_check_def_name(tcx, path.res.def_id(), "builtin", "Structural") {
-                    let struct_eq_def_id = tcx
-                        .lang_items()
-                        .structural_teq_trait()
-                        .expect("structural eq trait is not defined");
                     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
@@ -88,7 +84,6 @@ fn check_item<'tcx>(
                         };
                         tcx.type_of(def_id)
                     };
-                    let substs_ref = tcx.mk_substs([].iter());
                     // 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 =
@@ -106,12 +101,6 @@ fn check_item<'tcx>(
                             panic!("Structural impl for non-adt type");
                         };
                     let ty_applied_never = tcx.mk_ty(ty_kind_applied_never);
-                    let ty_implements_struct_eq = tcx.type_implements_trait((
-                        struct_eq_def_id,
-                        ty_applied_never,
-                        substs_ref,
-                        rustc_middle::ty::ParamEnv::empty(),
-                    ));
                     err_unless!(
                         ty_applied_never.is_structural_eq_shallow(tcx),
                         item.span,
@@ -155,23 +144,6 @@ fn check_item<'tcx>(
             );
         }
         _ => {
-            // 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)
-            //     ),
-            // );
-
             unsupported_err!(item.span, "unsupported item", item);
         }
     }

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,15 +268,15 @@ 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) => {
+        (TypX::Path(_), TypX::Path(_)) if types_equal(&t1, &t2) => {
             let structural_def_id = ctxt
                 .tcx
                 .get_diagnostic_item(rustc_span::Symbol::intern("builtin::Structural"))