Skip to content

Commit 0656301

Browse files
utaalutaal
authored
Merge pull request rust-lang#27 from Chris-Hawblitzel/fn-path
Use full Paths, instead of just the name, to identify functions in vir
2 parents a6df76d + d350c4a commit 0656301

21 files changed

+171
-152
lines changed

‎verify/rust_verify/src/context.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ use vir::ast::Mode;
88
pub struct ErasureInfo {
99
pub(crate) resolved_calls: Vec<(SpanData, ResolvedCall)>,
1010
pub(crate) condition_modes: Vec<(SpanData, Mode)>,
11-
pub(crate) external_functions: Vec<air::ast::Ident>,
11+
pub(crate) external_functions: Vec<vir::ast::Path>,
1212
}
1313

1414
type ErasureInfoRef = std::rc::Rc<std::cell::RefCell<ErasureInfo>>;

‎verify/rust_verify/src/erase.rs

Lines changed: 19 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@
3939
use crate::rust_to_vir_base::get_verifier_attrs;
4040
use crate::util::{from_raw_span, vec_map};
4141
use crate::{unsupported, unsupported_unless};
42-
use air::ast::Ident;
42+
4343
use rustc_ast::ast::{
4444
Block, Crate, Expr, ExprKind, FnDecl, FnKind, FnSig, Item, ItemKind, Local, ModKind, Param,
4545
Stmt, StmtKind,
@@ -48,7 +48,8 @@ use rustc_ast::ptr::P;
4848
use rustc_interface::interface::Compiler;
4949
use rustc_span::{Span, SpanData};
5050
use std::collections::HashMap;
51-
use std::sync::Arc;
51+
use vir::ast::Path;
52+
5253
use vir::ast::{Function, Krate, Mode};
5354
use vir::modes::ErasureModes;
5455

@@ -60,7 +61,7 @@ pub enum ResolvedCall {
6061
/// The call is to an operator like == or + that should be compiled.
6162
CompilableOperator,
6263
/// The call is to a function, and we record the resolved name of the function here.
63-
Call(Ident),
64+
Call(Path),
6465
}
6566

6667
#[derive(Clone)]
@@ -73,16 +74,18 @@ pub struct ErasureHints {
7374
pub erasure_modes: ErasureModes,
7475
/// List of #[verifier(external)] functions. (These don't appear in vir_crate,
7576
/// so we need to record them separately here.)
76-
pub external_functions: Vec<Ident>,
77+
pub external_functions: Vec<Path>,
7778
}
7879

7980
#[derive(Clone)]
8081
pub struct Ctxt {
8182
/// Copy of the entire VIR crate that was created in the first run's HIR -> VIR transformation
8283
vir_crate: Krate,
83-
/// Map each function name to its VIR Function, or to None if it is a #[verifier(external)]
84+
/// Map each function path to its VIR Function, or to None if it is a #[verifier(external)]
8485
/// function
85-
functions: HashMap<Ident, Option<Function>>,
86+
functions: HashMap<Path, Option<Function>>,
87+
/// Map each function span to its VIR Function, excluding #[verifier(external)] functions
88+
functions_by_span: HashMap<Span, Function>,
8689
/// Details of each call in the first run's HIR
8790
calls: HashMap<Span, ResolvedCall>,
8891
/// 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> {
181184
f_expr.clone(),
182185
vec_map(args, |e| P(erase_expr(ctxt, is_exec, e))),
183186
),
184-
ResolvedCall::Call(f_name) => {
185-
let f = &ctxt.functions[f_name];
187+
ResolvedCall::Call(f_path) => {
188+
let f = &ctxt.functions[f_path];
186189
if let Some(f) = f {
187190
match f.x.mode {
188191
Mode::Spec | Mode::Proof => return None,
@@ -271,13 +274,13 @@ fn erase_block(ctxt: &Ctxt, is_exec: bool, block: &Block) -> Block {
271274
Block { stmts, id, rules, span, tokens: block.tokens.clone() }
272275
}
273276

274-
fn erase_fn(ctxt: &Ctxt, f_name: &String, f: &FnKind) -> Option<FnKind> {
275-
let f_vir = &ctxt.functions[&Arc::new(f_name.clone())].as_ref().expect("erase_fn");
277+
fn erase_fn(ctxt: &Ctxt, f: &FnKind) -> Option<FnKind> {
278+
let FnKind(defaultness, sig, generics, body_opt) = f;
279+
let f_vir = &ctxt.functions_by_span[&sig.span];
276280
match f_vir.x.mode {
277281
Mode::Spec | Mode::Proof => return None,
278282
Mode::Exec => {}
279283
}
280-
let FnKind(defaultness, sig, generics, body_opt) = f;
281284
let FnSig { header: _, decl, span: _ } = sig;
282285
let FnDecl { inputs, output } = &**decl;
283286
let mut new_inputs: Vec<Param> = Vec::new();
@@ -315,7 +318,7 @@ fn erase_item(ctxt: &Ctxt, item: &Item) -> Vec<P<Item>> {
315318
if vattrs.external {
316319
return vec![P(item.clone())];
317320
}
318-
match erase_fn(ctxt, &item.ident.name.to_string(), kind) {
321+
match erase_fn(ctxt, kind) {
319322
None => return vec![],
320323
Some(kind) => ItemKind::Fn(Box::new(kind)),
321324
}
@@ -364,9 +367,11 @@ pub struct CompilerCallbacks {
364367

365368
fn mk_ctxt(erasure_hints: &ErasureHints) -> Ctxt {
366369
let mut functions = HashMap::new();
370+
let mut functions_by_span = HashMap::new();
367371
let mut calls: HashMap<Span, ResolvedCall> = HashMap::new();
368372
for f in &erasure_hints.vir_crate.functions {
369-
functions.insert(f.x.name.clone(), Some(f.clone()));
373+
functions.insert(f.x.path.clone(), Some(f.clone()));
374+
functions_by_span.insert(from_raw_span(&f.span.raw_span), f.clone());
370375
}
371376
for name in &erasure_hints.external_functions {
372377
functions.insert(name.clone(), None);
@@ -385,6 +390,7 @@ fn mk_ctxt(erasure_hints: &ErasureHints) -> Ctxt {
385390
Ctxt {
386391
vir_crate: erasure_hints.vir_crate.clone(),
387392
functions,
393+
functions_by_span,
388394
calls,
389395
condition_modes,
390396
var_modes,

‎verify/rust_verify/src/rust_to_vir.rs

Lines changed: 8 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@ use crate::util::unsupported_err_span;
1414
use crate::{err_unless, unsupported_err, unsupported_err_unless, unsupported_unless};
1515
use rustc_ast::Attribute;
1616
use rustc_hir::{
17-
Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, Item, ItemId, ItemKind, ModuleItems,
18-
QPath, TraitRef, TyKind,
17+
Crate, ForeignItem, ForeignItemId, ForeignItemKind, HirId, Item,
18+
ItemId, ItemKind, ModuleItems, QPath, TraitRef, TyKind,
1919
};
2020
use rustc_middle::ty::TyCtxt;
2121
use std::collections::HashMap;
@@ -35,7 +35,8 @@ fn check_item<'tcx>(
3535
check_item_fn(
3636
ctxt,
3737
vir,
38-
item.ident,
38+
None,
39+
item.def_id.to_def_id(),
3940
visibility,
4041
ctxt.tcx.hir().attrs(item.hir_id()),
4142
sig,
@@ -189,7 +190,7 @@ fn check_item<'tcx>(
189190
}
190191

191192
fn check_module<'tcx>(
192-
tcx: TyCtxt<'tcx>,
193+
_tcx: TyCtxt<'tcx>,
193194
module_path: &Path,
194195
module_items: &'tcx ModuleItems,
195196
item_to_module: &mut HashMap<ItemId, Path>,
@@ -200,18 +201,8 @@ fn check_module<'tcx>(
200201
item_to_module.insert(*item_id, module_path.clone());
201202
}
202203
unsupported_unless!(trait_items.len() == 0, "trait definitions", trait_items);
203-
// TODO: deduplicate with crate_to_vir
204-
for id in impl_items {
205-
let def_name = hack_get_def_name(tcx, id.def_id.to_def_id());
206-
// TODO: check whether these implement the correct trait
207-
unsupported_unless!(
208-
def_name == "assert_receiver_is_total_eq"
209-
|| def_name == "eq"
210-
|| def_name == "ne"
211-
|| def_name == "assert_receiver_is_structural",
212-
"impl definition in module",
213-
id
214-
);
204+
for _id in impl_items {
205+
// TODO?
215206
}
216207
for _id in foreign_items {
217208
// TODO
@@ -232,7 +223,7 @@ fn check_foreign_item<'tcx>(
232223
check_foreign_item_fn(
233224
ctxt,
234225
vir,
235-
item.ident,
226+
item.def_id.to_def_id(),
236227
item.span,
237228
mk_visibility(&None, &item.vis),
238229
ctxt.tcx.hir().attrs(item.hir_id()),

‎verify/rust_verify/src/rust_to_vir_expr.rs

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ use crate::util::{
99
vec_map_result,
1010
};
1111
use crate::{unsupported, unsupported_err, unsupported_err_unless, unsupported_unless};
12-
use air::ast::{Binder, BinderX, Ident, Quant};
12+
use air::ast::{Binder, BinderX, Quant};
1313
use rustc_ast::{Attribute, BorrowKind, LitKind, Mutability};
1414
use rustc_hir::def::{DefKind, Res};
1515
use rustc_hir::{
@@ -181,17 +181,15 @@ fn record_fun(
181181
} else if is_compilable_operator {
182182
ResolvedCall::CompilableOperator
183183
} else {
184-
ResolvedCall::Call(Arc::new(hack_get_def_name(ctxt.tcx, id)))
184+
ResolvedCall::Call(def_id_to_vir_path(ctxt.tcx, id))
185185
};
186186
erasure_info.resolved_calls.push((span.data(), resolved_call));
187187
}
188188

189-
fn get_fn_name<'tcx>(tcx: TyCtxt<'tcx>, expr: &Expr<'tcx>) -> Result<Ident, VirErr> {
189+
fn get_fn_path<'tcx>(tcx: TyCtxt<'tcx>, expr: &Expr<'tcx>) -> Result<vir::ast::Path, VirErr> {
190190
match &expr.kind {
191191
ExprKind::Path(QPath::Resolved(None, path)) => match path.res {
192-
Res::Def(DefKind::Fn, id) => {
193-
Ok(Arc::new(hack_get_def_name(tcx, id))) // TODO: proper handling of paths
194-
}
192+
Res::Def(DefKind::Fn, id) => Ok(def_id_to_vir_path(tcx, id)),
195193
res => unsupported_err!(expr.span, format!("Path {:?}", res)),
196194
},
197195
_ => unsupported_err!(expr.span, format!("{:?}", expr)),
@@ -273,7 +271,7 @@ fn fn_call_to_vir<'tcx>(
273271

274272
if is_hide || is_reveal {
275273
unsupported_err_unless!(len == 1, expr.span, "expected hide/reveal", &args);
276-
let x = get_fn_name(tcx, &args[0])?;
274+
let x = get_fn_path(tcx, &args[0])?;
277275
if is_hide {
278276
let header = Arc::new(HeaderExprX::Hide(x));
279277
return Ok(mk_expr(ExprX::Header(header)));
@@ -283,7 +281,7 @@ fn fn_call_to_vir<'tcx>(
283281
}
284282
if is_reveal_fuel {
285283
unsupported_err_unless!(len == 2, expr.span, "expected reveal_fuel", &args);
286-
let x = get_fn_name(tcx, &args[0])?;
284+
let x = get_fn_path(tcx, &args[0])?;
287285
match &expr_to_vir(bctx, &args[1])?.x {
288286
ExprX::Const(Constant::Nat(s)) => {
289287
let n = s.parse::<u32>().expect(&format!("internal error: parse {}", s));
@@ -396,11 +394,10 @@ fn fn_call_to_vir<'tcx>(
396394
},
397395
};
398396
// make call
399-
let name = hack_get_def_name(tcx, f); // TODO: proper handling of paths
400397
let mut call = spanned_typed_new(
401398
expr.span,
402399
&possibly_boxed_ret_typ,
403-
ExprX::Call(Arc::new(name), Arc::new(typ_args), Arc::new(vir_args)),
400+
ExprX::Call(def_id_to_vir_path(tcx, f), Arc::new(typ_args), Arc::new(vir_args)),
404401
);
405402
// unbox result if necessary
406403
if let Some(ret_typ) = ret_typ {

‎verify/rust_verify/src/rust_to_vir_func.rs

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use crate::context::Context;
22
use crate::rust_to_vir_base::{
3-
check_generics, get_fuel, get_mode, get_var_mode, get_verifier_attrs, ident_to_var, ty_to_vir,
4-
BodyCtxt,
3+
check_generics, def_id_to_vir_path, get_fuel, get_mode, get_var_mode, get_verifier_attrs,
4+
ident_to_var, ty_to_vir, BodyCtxt,
55
};
66
use crate::rust_to_vir_expr::{expr_to_vir, pat_to_var};
77
use crate::util::{err_span_str, err_span_string, spanned_new, unsupported_err_span};
@@ -50,14 +50,15 @@ fn check_fn_decl<'tcx>(
5050
pub(crate) fn check_item_fn<'tcx>(
5151
ctxt: &Context<'tcx>,
5252
vir: &mut KrateX,
53-
id: Ident,
53+
_self_path: Option<&'tcx rustc_hir::Path<'tcx>>,
54+
id: rustc_span::def_id::DefId,
5455
visibility: vir::ast::Visibility,
5556
attrs: &[Attribute],
5657
sig: &'tcx FnSig<'tcx>,
5758
generics: &'tcx Generics,
5859
body_id: &BodyId,
5960
) -> Result<(), VirErr> {
60-
let name = Arc::new(ident_to_var(&id));
61+
let path = def_id_to_vir_path(ctxt.tcx, id);
6162
let mode = get_mode(Mode::Exec, attrs);
6263
let ret_typ_mode = match sig {
6364
FnSig {
@@ -74,7 +75,7 @@ pub(crate) fn check_item_fn<'tcx>(
7475
let vattrs = get_verifier_attrs(attrs)?;
7576
if vattrs.external {
7677
let mut erasure_info = ctxt.erasure_info.borrow_mut();
77-
erasure_info.external_functions.push(name);
78+
erasure_info.external_functions.push(path);
7879
return Ok(());
7980
}
8081
let body = &ctxt.krate.bodies[body_id];
@@ -129,7 +130,7 @@ pub(crate) fn check_item_fn<'tcx>(
129130
_ => panic!("internal error: ret_typ"),
130131
};
131132
let func = FunctionX {
132-
name,
133+
path,
133134
visibility,
134135
mode,
135136
fuel,
@@ -152,7 +153,7 @@ pub(crate) fn check_item_fn<'tcx>(
152153
pub(crate) fn check_foreign_item_fn<'tcx>(
153154
ctxt: &Context<'tcx>,
154155
vir: &mut KrateX,
155-
id: Ident,
156+
id: rustc_span::def_id::DefId,
156157
span: Span,
157158
visibility: vir::ast::Visibility,
158159
attrs: &[Attribute],
@@ -172,10 +173,10 @@ pub(crate) fn check_foreign_item_fn<'tcx>(
172173
let vir_param = spanned_new(param.span, ParamX { name, typ, mode });
173174
vir_params.push(vir_param);
174175
}
175-
let name = Arc::new(ident_to_var(&id));
176+
let path = def_id_to_vir_path(ctxt.tcx, id);
176177
let params = Arc::new(vir_params);
177178
let func = FunctionX {
178-
name,
179+
path,
179180
visibility,
180181
fuel,
181182
mode,

‎verify/rust_verify/src/verifier.rs

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ use rustc_span::{CharPos, FileName, MultiSpan, Span};
1212
use std::fs::File;
1313
use std::io::Write;
1414
use vir::ast::{Krate, Path, VirErr, VirErrX, Visibility};
15+
use vir::ast_util::path_to_string;
1516
use vir::def::SnapPos;
1617
use vir::model::Model as VModel;
1718

@@ -247,7 +248,7 @@ impl Verifier {
247248
Self::run_commands(
248249
air_context,
249250
&commands,
250-
&("Function-Decl ".to_string() + &function.x.name),
251+
&("Function-Decl ".to_string() + &path_to_string(&function.x.path)),
251252
);
252253
}
253254

@@ -264,7 +265,7 @@ impl Verifier {
264265
Self::run_commands(
265266
air_context,
266267
&decl_commands,
267-
&("Function-Axioms ".to_string() + &function.x.name),
268+
&("Function-Axioms ".to_string() + &path_to_string(&function.x.path)),
268269
);
269270

270271
// Check termination
@@ -276,7 +277,7 @@ impl Verifier {
276277
air_context,
277278
&check_commands,
278279
&vec![],
279-
&("Function-Termination ".to_string() + &function.x.name),
280+
&("Function-Termination ".to_string() + &path_to_string(&function.x.path)),
280281
);
281282
}
282283

@@ -291,7 +292,7 @@ impl Verifier {
291292
air_context,
292293
&commands,
293294
&snap_map,
294-
&("Function-Def ".to_string() + &function.x.name),
295+
&("Function-Def ".to_string() + &path_to_string(&function.x.path)),
295296
);
296297
}
297298

@@ -399,7 +400,7 @@ impl Verifier {
399400
writeln!(&mut file).expect("cannot write to vir file");
400401
}
401402
for func in vir_crate.functions.iter() {
402-
writeln!(&mut file, "fn {} @ {:?}", func.x.name, func.span)
403+
writeln!(&mut file, "fn {} @ {:?}", path_to_string(&func.x.path), func.span)
403404
.expect("cannot write to vir file");
404405
for param in func.x.params.iter() {
405406
writeln!(

0 commit comments

Comments
 (0)