Merge pull request rust-lang#27 from Chris-Hawblitzel/fn-path

Use full Paths, instead of just the name, to identify functions in vir

verify/rust_verify/src/context.rs

@@ -8,7 +8,7 @@ use vir::ast::Mode;
 pub struct ErasureInfo {
     pub(crate) resolved_calls: Vec<(SpanData, ResolvedCall)>,
     pub(crate) condition_modes: Vec<(SpanData, Mode)>,
-    pub(crate) external_functions: Vec<air::ast::Ident>,
+    pub(crate) external_functions: Vec<vir::ast::Path>,
 }
 
 type ErasureInfoRef = std::rc::Rc<std::cell::RefCell<ErasureInfo>>;

verify/rust_verify/src/erase.rs

@@ -39,7 +39,7 @@
 use crate::rust_to_vir_base::get_verifier_attrs;
 use crate::util::{from_raw_span, vec_map};
 use crate::{unsupported, unsupported_unless};
-use air::ast::Ident;
+
 use rustc_ast::ast::{
     Block, Crate, Expr, ExprKind, FnDecl, FnKind, FnSig, Item, ItemKind, Local, ModKind, Param,
     Stmt, StmtKind,
@@ -48,7 +48,8 @@ use rustc_ast::ptr::P;
 use rustc_interface::interface::Compiler;
 use rustc_span::{Span, SpanData};
 use std::collections::HashMap;
-use std::sync::Arc;
+use vir::ast::Path;
+
 use vir::ast::{Function, Krate, Mode};
 use vir::modes::ErasureModes;
 
@@ -60,7 +61,7 @@ pub enum ResolvedCall {
     /// The call is to an operator like == or + that should be compiled.
     CompilableOperator,
     /// The call is to a function, and we record the resolved name of the function here.
-    Call(Ident),
+    Call(Path),
 }
 
 #[derive(Clone)]
@@ -73,16 +74,18 @@ pub struct ErasureHints {
     pub erasure_modes: ErasureModes,
     /// List of #[verifier(external)] functions.  (These don't appear in vir_crate,
     /// so we need to record them separately here.)
-    pub external_functions: Vec<Ident>,
+    pub external_functions: Vec<Path>,
 }
 
 #[derive(Clone)]
 pub struct Ctxt {
     /// Copy of the entire VIR crate that was created in the first run's HIR -> VIR transformation
     vir_crate: Krate,
-    /// Map each function name to its VIR Function, or to None if it is a #[verifier(external)]
+    /// Map each function path to its VIR Function, or to None if it is a #[verifier(external)]
     /// function
-    functions: HashMap<Ident, Option<Function>>,
+    functions: HashMap<Path, Option<Function>>,
+    /// Map each function span to its VIR Function, excluding #[verifier(external)] functions
+    functions_by_span: HashMap<Span, Function>,
     /// Details of each call in the first run's HIR
     calls: HashMap<Span, ResolvedCall>,
     /// Mode of each if/else or match condition, used to decide how to erase if/else and match
@@ -181,8 +184,8 @@ fn erase_expr_opt(ctxt: &Ctxt, is_exec: bool, expr: &Expr) -> Option<Expr> {
                     f_expr.clone(),
                     vec_map(args, |e| P(erase_expr(ctxt, is_exec, e))),
                 ),
-                ResolvedCall::Call(f_name) => {
-                    let f = &ctxt.functions[f_name];
+                ResolvedCall::Call(f_path) => {
+                    let f = &ctxt.functions[f_path];
                     if let Some(f) = f {
                         match f.x.mode {
                             Mode::Spec | Mode::Proof => return None,
@@ -271,13 +274,13 @@ fn erase_block(ctxt: &Ctxt, is_exec: bool, block: &Block) -> Block {
     Block { stmts, id, rules, span, tokens: block.tokens.clone() }
 }
 
-fn erase_fn(ctxt: &Ctxt, f_name: &String, f: &FnKind) -> Option<FnKind> {
-    let f_vir = &ctxt.functions[&Arc::new(f_name.clone())].as_ref().expect("erase_fn");
+fn erase_fn(ctxt: &Ctxt, f: &FnKind) -> Option<FnKind> {
+    let FnKind(defaultness, sig, generics, body_opt) = f;
+    let f_vir = &ctxt.functions_by_span[&sig.span];
     match f_vir.x.mode {
         Mode::Spec | Mode::Proof => return None,
         Mode::Exec => {}
     }
-    let FnKind(defaultness, sig, generics, body_opt) = f;
     let FnSig { header: _, decl, span: _ } = sig;
     let FnDecl { inputs, output } = &**decl;
     let mut new_inputs: Vec<Param> = Vec::new();
@@ -315,7 +318,7 @@ fn erase_item(ctxt: &Ctxt, item: &Item) -> Vec<P<Item>> {
             if vattrs.external {
                 return vec![P(item.clone())];
             }
-            match erase_fn(ctxt, &item.ident.name.to_string(), kind) {
+            match erase_fn(ctxt, kind) {
                 None => return vec![],
                 Some(kind) => ItemKind::Fn(Box::new(kind)),
             }
@@ -364,9 +367,11 @@ pub struct CompilerCallbacks {
 
 fn mk_ctxt(erasure_hints: &ErasureHints) -> Ctxt {
     let mut functions = HashMap::new();
+    let mut functions_by_span = HashMap::new();
     let mut calls: HashMap<Span, ResolvedCall> = HashMap::new();
     for f in &erasure_hints.vir_crate.functions {
-        functions.insert(f.x.name.clone(), Some(f.clone()));
+        functions.insert(f.x.path.clone(), Some(f.clone()));
+        functions_by_span.insert(from_raw_span(&f.span.raw_span), f.clone());
     }
     for name in &erasure_hints.external_functions {
         functions.insert(name.clone(), None);
@@ -385,6 +390,7 @@ fn mk_ctxt(erasure_hints: &ErasureHints) -> Ctxt {
     Ctxt {
         vir_crate: erasure_hints.vir_crate.clone(),
         functions,
+        functions_by_span,
         calls,
         condition_modes,
         var_modes,

verify/rust_verify/src/rust_to_vir.rs

@@ -14,8 +14,8 @@ use crate::util::unsupported_err_span;
 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,
-    QPath, TraitRef, TyKind,
+    Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, Item,
+    ItemId, ItemKind, ModuleItems, QPath, TraitRef, TyKind,
 };
 use rustc_middle::ty::TyCtxt;
 use std::collections::HashMap;
@@ -35,7 +35,8 @@ fn check_item<'tcx>(
             check_item_fn(
                 ctxt,
                 vir,
-                item.ident,
+                None,
+                item.def_id.to_def_id(),
                 visibility,
                 ctxt.tcx.hir().attrs(item.hir_id()),
                 sig,
@@ -189,7 +190,7 @@ fn check_item<'tcx>(
 }
 
 fn check_module<'tcx>(
-    tcx: TyCtxt<'tcx>,
+    _tcx: TyCtxt<'tcx>,
     module_path: &Path,
     module_items: &'tcx ModuleItems,
     item_to_module: &mut HashMap<ItemId, Path>,
@@ -200,18 +201,8 @@ fn check_module<'tcx>(
                 item_to_module.insert(*item_id, module_path.clone());
             }
             unsupported_unless!(trait_items.len() == 0, "trait definitions", trait_items);
-            // TODO: deduplicate with crate_to_vir
-            for id in impl_items {
-                let def_name = hack_get_def_name(tcx, id.def_id.to_def_id());
-                // TODO: check whether these implement the correct trait
-                unsupported_unless!(
-                    def_name == "assert_receiver_is_total_eq"
-                        || def_name == "eq"
-                        || def_name == "ne"
-                        || def_name == "assert_receiver_is_structural",
-                    "impl definition in module",
-                    id
-                );
+            for _id in impl_items {
+                // TODO?
             }
             for _id in foreign_items {
                 // TODO
@@ -232,7 +223,7 @@ fn check_foreign_item<'tcx>(
             check_foreign_item_fn(
                 ctxt,
                 vir,
-                item.ident,
+                item.def_id.to_def_id(),
                 item.span,
                 mk_visibility(&None, &item.vis),
                 ctxt.tcx.hir().attrs(item.hir_id()),

verify/rust_verify/src/rust_to_vir_expr.rs

@@ -9,7 +9,7 @@ use crate::util::{
     vec_map_result,
 };
 use crate::{unsupported, unsupported_err, unsupported_err_unless, unsupported_unless};
-use air::ast::{Binder, BinderX, Ident, Quant};
+use air::ast::{Binder, BinderX, Quant};
 use rustc_ast::{Attribute, BorrowKind, LitKind, Mutability};
 use rustc_hir::def::{DefKind, Res};
 use rustc_hir::{
@@ -181,17 +181,15 @@ fn record_fun(
     } else if is_compilable_operator {
         ResolvedCall::CompilableOperator
     } else {
-        ResolvedCall::Call(Arc::new(hack_get_def_name(ctxt.tcx, id)))
+        ResolvedCall::Call(def_id_to_vir_path(ctxt.tcx, id))
     };
     erasure_info.resolved_calls.push((span.data(), resolved_call));
 }
 
-fn get_fn_name<'tcx>(tcx: TyCtxt<'tcx>, expr: &Expr<'tcx>) -> Result<Ident, VirErr> {
+fn get_fn_path<'tcx>(tcx: TyCtxt<'tcx>, expr: &Expr<'tcx>) -> Result<vir::ast::Path, VirErr> {
     match &expr.kind {
         ExprKind::Path(QPath::Resolved(None, path)) => match path.res {
-            Res::Def(DefKind::Fn, id) => {
-                Ok(Arc::new(hack_get_def_name(tcx, id))) // TODO: proper handling of paths
-            }
+            Res::Def(DefKind::Fn, id) => Ok(def_id_to_vir_path(tcx, id)),
             res => unsupported_err!(expr.span, format!("Path {:?}", res)),
         },
         _ => unsupported_err!(expr.span, format!("{:?}", expr)),
@@ -273,7 +271,7 @@ fn fn_call_to_vir<'tcx>(
 
     if is_hide || is_reveal {
         unsupported_err_unless!(len == 1, expr.span, "expected hide/reveal", &args);
-        let x = get_fn_name(tcx, &args[0])?;
+        let x = get_fn_path(tcx, &args[0])?;
         if is_hide {
             let header = Arc::new(HeaderExprX::Hide(x));
             return Ok(mk_expr(ExprX::Header(header)));
@@ -283,7 +281,7 @@ fn fn_call_to_vir<'tcx>(
     }
     if is_reveal_fuel {
         unsupported_err_unless!(len == 2, expr.span, "expected reveal_fuel", &args);
-        let x = get_fn_name(tcx, &args[0])?;
+        let x = get_fn_path(tcx, &args[0])?;
         match &expr_to_vir(bctx, &args[1])?.x {
             ExprX::Const(Constant::Nat(s)) => {
                 let n = s.parse::<u32>().expect(&format!("internal error: parse {}", s));
@@ -396,11 +394,10 @@ fn fn_call_to_vir<'tcx>(
             },
         };
         // make call
-        let name = hack_get_def_name(tcx, f); // TODO: proper handling of paths
         let mut call = spanned_typed_new(
             expr.span,
             &possibly_boxed_ret_typ,
-            ExprX::Call(Arc::new(name), Arc::new(typ_args), Arc::new(vir_args)),
+            ExprX::Call(def_id_to_vir_path(tcx, f), Arc::new(typ_args), Arc::new(vir_args)),
         );
         // unbox result if necessary
         if let Some(ret_typ) = ret_typ {

verify/rust_verify/src/rust_to_vir_func.rs

@@ -1,7 +1,7 @@
 use crate::context::Context;
 use crate::rust_to_vir_base::{
-    check_generics, get_fuel, get_mode, get_var_mode, get_verifier_attrs, ident_to_var, ty_to_vir,
-    BodyCtxt,
+    check_generics, def_id_to_vir_path, get_fuel, get_mode, get_var_mode, get_verifier_attrs,
+    ident_to_var, ty_to_vir, BodyCtxt,
 };
 use crate::rust_to_vir_expr::{expr_to_vir, pat_to_var};
 use crate::util::{err_span_str, err_span_string, spanned_new, unsupported_err_span};
@@ -50,14 +50,15 @@ fn check_fn_decl<'tcx>(
 pub(crate) fn check_item_fn<'tcx>(
     ctxt: &Context<'tcx>,
     vir: &mut KrateX,
-    id: Ident,
+    _self_path: Option<&'tcx rustc_hir::Path<'tcx>>,
+    id: rustc_span::def_id::DefId,
     visibility: vir::ast::Visibility,
     attrs: &[Attribute],
     sig: &'tcx FnSig<'tcx>,
     generics: &'tcx Generics,
     body_id: &BodyId,
 ) -> Result<(), VirErr> {
-    let name = Arc::new(ident_to_var(&id));
+    let path = def_id_to_vir_path(ctxt.tcx, id);
     let mode = get_mode(Mode::Exec, attrs);
     let ret_typ_mode = match sig {
         FnSig {
@@ -74,7 +75,7 @@ pub(crate) fn check_item_fn<'tcx>(
     let vattrs = get_verifier_attrs(attrs)?;
     if vattrs.external {
         let mut erasure_info = ctxt.erasure_info.borrow_mut();
-        erasure_info.external_functions.push(name);
+        erasure_info.external_functions.push(path);
         return Ok(());
     }
     let body = &ctxt.krate.bodies[body_id];
@@ -129,7 +130,7 @@ pub(crate) fn check_item_fn<'tcx>(
         _ => panic!("internal error: ret_typ"),
     };
     let func = FunctionX {
-        name,
+        path,
         visibility,
         mode,
         fuel,
@@ -152,7 +153,7 @@ pub(crate) fn check_item_fn<'tcx>(
 pub(crate) fn check_foreign_item_fn<'tcx>(
     ctxt: &Context<'tcx>,
     vir: &mut KrateX,
-    id: Ident,
+    id: rustc_span::def_id::DefId,
     span: Span,
     visibility: vir::ast::Visibility,
     attrs: &[Attribute],
@@ -172,10 +173,10 @@ pub(crate) fn check_foreign_item_fn<'tcx>(
         let vir_param = spanned_new(param.span, ParamX { name, typ, mode });
         vir_params.push(vir_param);
     }
-    let name = Arc::new(ident_to_var(&id));
+    let path = def_id_to_vir_path(ctxt.tcx, id);
     let params = Arc::new(vir_params);
     let func = FunctionX {
-        name,
+        path,
         visibility,
         fuel,
         mode,

verify/rust_verify/src/verifier.rs

@@ -12,6 +12,7 @@ use rustc_span::{CharPos, FileName, MultiSpan, Span};
 use std::fs::File;
 use std::io::Write;
 use vir::ast::{Krate, Path, VirErr, VirErrX, Visibility};
+use vir::ast_util::path_to_string;
 use vir::def::SnapPos;
 use vir::model::Model as VModel;
 
@@ -247,7 +248,7 @@ impl Verifier {
             Self::run_commands(
                 air_context,
                 &commands,
-                &("Function-Decl ".to_string() + &function.x.name),
+                &("Function-Decl ".to_string() + &path_to_string(&function.x.path)),
             );
         }
 
@@ -264,7 +265,7 @@ impl Verifier {
             Self::run_commands(
                 air_context,
                 &decl_commands,
-                &("Function-Axioms ".to_string() + &function.x.name),
+                &("Function-Axioms ".to_string() + &path_to_string(&function.x.path)),
             );
 
             // Check termination
@@ -276,7 +277,7 @@ impl Verifier {
                 air_context,
                 &check_commands,
                 &vec![],
-                &("Function-Termination ".to_string() + &function.x.name),
+                &("Function-Termination ".to_string() + &path_to_string(&function.x.path)),
             );
         }
 
@@ -291,7 +292,7 @@ impl Verifier {
                 air_context,
                 &commands,
                 &snap_map,
-                &("Function-Def ".to_string() + &function.x.name),
+                &("Function-Def ".to_string() + &path_to_string(&function.x.path)),
             );
         }
 
@@ -399,7 +400,7 @@ impl Verifier {
                 writeln!(&mut file).expect("cannot write to vir file");
             }
             for func in vir_crate.functions.iter() {
-                writeln!(&mut file, "fn {} @ {:?}", func.x.name, func.span)
+                writeln!(&mut file, "fn {} @ {:?}", path_to_string(&func.x.path), func.span)
                     .expect("cannot write to vir file");
                 for param in func.x.params.iter() {
                     writeln!(