Skip to content

Commit 24b825a

Browse files
parnoparno
committed
Plumbed a new Context object throughout rust_verify. Consolidates
TyCtxt and Krate, and holds a new SourceMap entry used for error reporting via Span.
1 parent 7bc353e commit 24b825a

File tree

9 files changed

+255
-233
lines changed

9 files changed

+255
-233
lines changed

‎verify/rust_verify/src/context.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
use rustc_middle::ty::TyCtxt;
2+
use rustc_hir::Crate;
3+
use rustc_span::source_map::SourceMap;
4+
5+
pub(crate) struct Context<'tcx> {
6+
pub(crate) tcx: TyCtxt<'tcx>,
7+
pub(crate) krate: &'tcx Crate<'tcx>,
8+
pub(crate) source_map: &'tcx SourceMap,
9+
}

‎verify/rust_verify/src/lib.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ extern crate rustc_span;
1414
extern crate rustc_typeck;
1515

1616
pub mod config;
17+
pub mod context;
1718
pub mod rust_to_vir;
1819
pub mod rust_to_vir_adts;
1920
pub mod rust_to_vir_base;

‎verify/rust_verify/src/rust_to_vir.rs

Lines changed: 41 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ For soundness's sake, be as defensive as possible:
66
- explicitly match all fields of the Rust AST so we catch any features added in the future
77
*/
88

9+
use crate::context::Context;
910
use crate::rust_to_vir_adts::{check_item_enum, check_item_struct};
1011
use crate::rust_to_vir_base::{hack_check_def_name, hack_get_def_name};
1112
use crate::rust_to_vir_func::{check_foreign_item_fn, check_item_fn};
@@ -22,20 +23,18 @@ use std::rc::Rc;
2223
use vir::ast::{Krate, KrateX, VirErr};
2324

2425
fn check_item<'tcx>(
25-
tcx: TyCtxt<'tcx>,
26-
krate: &'tcx Crate<'tcx>,
26+
ctxt: &'tcx Context<'tcx>,
2727
vir: &mut KrateX,
2828
id: &ItemId,
2929
item: &'tcx Item<'tcx>,
3030
) -> Result<(), VirErr> {
3131
match &item.kind {
3232
ItemKind::Fn(sig, generics, body_id) => {
3333
check_item_fn(
34-
tcx,
35-
krate,
34+
ctxt,
3635
vir,
3736
item.ident,
38-
tcx.hir().attrs(item.hir_id()),
37+
ctxt.tcx.hir().attrs(item.hir_id()),
3938
sig,
4039
generics,
4140
body_id,
@@ -49,30 +48,31 @@ fn check_item<'tcx>(
4948
// TODO use rustc_middle info here? if sufficient, it may allow for a single code path
5049
// for definitions of the local crate and imported crates
5150
// let adt_def = tcx.adt_def(item.def_id);
52-
check_item_struct(tcx, krate, vir, item.span, id, variant_data, generics)?;
51+
check_item_struct(ctxt, vir, item.span, id, variant_data, generics)?;
5352
}
5453
ItemKind::Enum(enum_def, generics) => {
5554
// TODO use rustc_middle? see `Struct` case
56-
check_item_enum(tcx, krate, vir, item.span, id, enum_def, generics)?;
55+
check_item_enum(ctxt, vir, item.span, id, enum_def, generics)?;
5756
}
5857
ItemKind::Impl(impll) => {
5958
if let Some(TraitRef { path, hir_ref_id: _ }) = impll.of_trait {
6059
unsupported_err_unless!(
61-
hack_check_def_name(tcx, path.res.def_id(), "core", "marker::StructuralEq")
62-
|| hack_check_def_name(tcx, path.res.def_id(), "core", "cmp::Eq")
60+
ctxt,
61+
hack_check_def_name(ctxt.tcx, path.res.def_id(), "core", "marker::StructuralEq")
62+
|| hack_check_def_name(ctxt.tcx, path.res.def_id(), "core", "cmp::Eq")
6363
|| hack_check_def_name(
64-
tcx,
64+
ctxt.tcx,
6565
path.res.def_id(),
6666
"core",
6767
"marker::StructuralPartialEq"
6868
)
69-
|| hack_check_def_name(tcx, path.res.def_id(), "core", "cmp::PartialEq")
70-
|| hack_check_def_name(tcx, path.res.def_id(), "builtin", "Structural"),
69+
|| hack_check_def_name(ctxt.tcx, path.res.def_id(), "core", "cmp::PartialEq")
70+
|| hack_check_def_name(ctxt.tcx, path.res.def_id(), "builtin", "Structural"),
7171
item.span,
7272
"non_eq_trait_impl",
7373
path
7474
);
75-
if hack_check_def_name(tcx, path.res.def_id(), "builtin", "Structural") {
75+
if hack_check_def_name(ctxt.tcx, path.res.def_id(), "builtin", "Structural") {
7676
let ty = {
7777
// TODO extract to rust_to_vir_base, or use
7878
// https://doc.rust-lang.org/nightly/nightly-rustc/rustc_typeck/fn.hir_ty_to_ty.html
@@ -86,40 +86,43 @@ fn check_item<'tcx>(
8686
impll.self_ty.kind
8787
),
8888
};
89-
tcx.type_of(def_id)
89+
ctxt.tcx.type_of(def_id)
9090
};
9191
// TODO: this may be a bit of a hack: to query the TyCtxt for the StructuralEq impl it seems we need
9292
// a concrete type, so apply ! to all type parameters
9393
let ty_kind_applied_never =
9494
if let rustc_middle::ty::TyKind::Adt(def, substs) = ty.kind() {
9595
rustc_middle::ty::TyKind::Adt(
9696
def,
97-
tcx.mk_substs(substs.iter().map(|g| match g.unpack() {
97+
ctxt.tcx.mk_substs(substs.iter().map(|g| match g.unpack() {
9898
rustc_middle::ty::subst::GenericArgKind::Type(_) => {
99-
(*tcx).types.never.into()
99+
(*ctxt.tcx).types.never.into()
100100
}
101101
_ => g,
102102
})),
103103
)
104104
} else {
105105
panic!("Structural impl for non-adt type");
106106
};
107-
let ty_applied_never = tcx.mk_ty(ty_kind_applied_never);
107+
let ty_applied_never = ctxt.tcx.mk_ty(ty_kind_applied_never);
108108
err_unless!(
109-
ty_applied_never.is_structural_eq_shallow(tcx),
109+
ctxt,
110+
ty_applied_never.is_structural_eq_shallow(ctxt.tcx),
110111
item.span,
111112
format!("Structural impl for non-structural type {:?}", ty),
112113
ty
113114
);
114115
}
115116
} else {
116117
unsupported_err_unless!(
118+
ctxt,
117119
impll.of_trait.is_none(),
118120
item.span,
119121
"unsupported impl of trait",
120122
item
121123
);
122124
unsupported_err_unless!(
125+
ctxt,
123126
impll.generics.params.len() == 0,
124127
item.span,
125128
"unsupported impl of non-trait with generics",
@@ -129,26 +132,27 @@ fn check_item<'tcx>(
129132
TyKind::Path(QPath::Resolved(_, _path)) => {
130133
for impl_item in impll.items {
131134
// TODO once we have references
132-
unsupported_err!(item.span, "unsupported method in impl", impl_item);
135+
unsupported_err!(ctxt, item.span, "unsupported method in impl", impl_item);
133136
}
134137
}
135138
_ => {
136-
unsupported_err!(item.span, "unsupported impl of non-path type", item);
139+
unsupported_err!(ctxt, item.span, "unsupported impl of non-path type", item);
137140
}
138141
}
139142
}
140143
}
141144
ItemKind::Const(_ty, _body_id) => {
142145
unsupported_err_unless!(
143-
hack_get_def_name(tcx, _body_id.hir_id.owner.to_def_id())
146+
ctxt,
147+
hack_get_def_name(ctxt.tcx, _body_id.hir_id.owner.to_def_id())
144148
.starts_with("_DERIVE_builtin_Structural_FOR_"),
145149
item.span,
146150
"unsupported const",
147151
item
148152
);
149153
}
150154
_ => {
151-
unsupported_err!(item.span, "unsupported item", item);
155+
unsupported_err!(ctxt, item.span, "unsupported item", item);
152156
}
153157
}
154158
Ok(())
@@ -187,26 +191,26 @@ fn check_module<'tcx>(
187191
}
188192

189193
fn check_foreign_item<'tcx>(
190-
tcx: TyCtxt<'tcx>,
194+
ctxt: &Context<'tcx>,
191195
vir: &mut KrateX,
192196
_id: &ForeignItemId,
193197
item: &'tcx ForeignItem<'tcx>,
194198
) -> Result<(), VirErr> {
195199
match &item.kind {
196200
ForeignItemKind::Fn(decl, idents, generics) => {
197201
check_foreign_item_fn(
198-
tcx,
202+
ctxt,
199203
vir,
200204
item.ident,
201205
item.span,
202-
tcx.hir().attrs(item.hir_id()),
206+
ctxt.tcx.hir().attrs(item.hir_id()),
203207
decl,
204208
idents,
205209
generics,
206210
)?;
207211
}
208212
_ => {
209-
unsupported_err!(item.span, "unsupported item", item);
213+
unsupported_err!(ctxt, item.span, "unsupported item", item);
210214
}
211215
}
212216
Ok(())
@@ -221,7 +225,7 @@ fn check_attr<'tcx>(
221225
Ok(())
222226
}
223227

224-
pub fn crate_to_vir<'tcx>(tcx: TyCtxt<'tcx>, krate: &'tcx Crate<'tcx>) -> Result<Krate, VirErr> {
228+
pub fn crate_to_vir<'tcx>(ctxt: &Context<'tcx>) -> Result<Krate, VirErr> {
225229
let Crate {
226230
item: _,
227231
exported_macros,
@@ -237,7 +241,7 @@ pub fn crate_to_vir<'tcx>(tcx: TyCtxt<'tcx>, krate: &'tcx Crate<'tcx>) -> Result
237241
proc_macros,
238242
trait_map,
239243
attrs,
240-
} = krate;
244+
} = ctxt.krate;
241245
let mut vir: KrateX = Default::default();
242246
unsupported_unless!(
243247
exported_macros.len() == 0,
@@ -250,10 +254,10 @@ pub fn crate_to_vir<'tcx>(tcx: TyCtxt<'tcx>, krate: &'tcx Crate<'tcx>) -> Result
250254
non_exported_macro_attrs
251255
);
252256
for (id, item) in foreign_items {
253-
check_foreign_item(tcx, &mut vir, id, item)?;
257+
check_foreign_item(ctxt, &mut vir, id, item)?;
254258
}
255259
for (id, item) in items {
256-
check_item(tcx, krate, &mut vir, id, item)?;
260+
check_item(ctxt, &mut vir, id, item)?;
257261
}
258262
unsupported_unless!(trait_items.len() == 0, "trait definitions", trait_items);
259263
for (_id, impl_item) in impl_items {
@@ -270,22 +274,22 @@ pub fn crate_to_vir<'tcx>(tcx: TyCtxt<'tcx>, krate: &'tcx Crate<'tcx>) -> Result
270274
}
271275
for (id, _trait_impl) in trait_impls {
272276
unsupported_unless!(
273-
hack_check_def_name(tcx, *id, "core", "marker::StructuralEq")
274-
|| hack_check_def_name(tcx, *id, "core", "cmp::Eq")
275-
|| hack_check_def_name(tcx, *id, "core", "marker::StructuralPartialEq")
276-
|| hack_check_def_name(tcx, *id, "core", "cmp::PartialEq")
277-
|| hack_check_def_name(tcx, *id, "builtin", "Structural"),
277+
hack_check_def_name(ctxt.tcx, *id, "core", "marker::StructuralEq")
278+
|| hack_check_def_name(ctxt.tcx, *id, "core", "cmp::Eq")
279+
|| hack_check_def_name(ctxt.tcx, *id, "core", "marker::StructuralPartialEq")
280+
|| hack_check_def_name(ctxt.tcx, *id, "core", "cmp::PartialEq")
281+
|| hack_check_def_name(ctxt.tcx, *id, "builtin", "Structural"),
278282
"non_eq_trait_impl",
279283
id
280284
);
281285
}
282286
for (id, module) in modules {
283-
check_module(tcx, id, module)?;
287+
check_module(ctxt.tcx, id, module)?;
284288
}
285289
unsupported_unless!(proc_macros.len() == 0, "procedural macros", proc_macros);
286290
unsupported_unless!(trait_map.iter().all(|(_, v)| v.len() == 0), "traits", trait_map);
287291
for (id, attr) in attrs {
288-
check_attr(tcx, id, attr)?;
292+
check_attr(ctxt.tcx, id, attr)?;
289293
}
290294
Ok(Rc::new(vir))
291295
}

‎verify/rust_verify/src/rust_to_vir_adts.rs

Lines changed: 19 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,18 @@
1+
use crate::context::Context;
12
use crate::rust_to_vir_base::{
23
check_generics, def_id_to_vir_path, get_mode, hack_get_def_name, ty_to_vir,
34
};
45
use crate::unsupported_unless;
56
use crate::util::spanned_new;
6-
use rustc_hir::{Crate, EnumDef, Generics, ItemId, VariantData};
7-
use rustc_middle::ty::TyCtxt;
7+
use rustc_hir::{EnumDef, Generics, ItemId, VariantData};
88
use rustc_span::Span;
99
use std::rc::Rc;
1010
use vir::ast::{DatatypeX, Ident, KrateX, Mode, Variant, VirErr};
1111
use vir::ast_util::{ident_binder, str_ident};
1212
use vir::def::{variant_field_ident, variant_ident, variant_positional_field_ident};
1313

1414
fn check_variant_data<'tcx>(
15-
tcx: TyCtxt<'tcx>,
16-
_krate: &'tcx Crate<'tcx>,
15+
ctxt: &Context<'tcx>,
1716
name: &Ident,
1817
variant_data: &'tcx VariantData<'tcx>,
1918
) -> Variant {
@@ -31,8 +30,8 @@ fn check_variant_data<'tcx>(
3130
ident_binder(
3231
&variant_field_ident(name, &field.ident.as_str()),
3332
&(
34-
ty_to_vir(tcx, field.ty),
35-
get_mode(Mode::Exec, tcx.hir().attrs(field.hir_id)),
33+
ty_to_vir(ctxt.tcx, field.ty),
34+
get_mode(Mode::Exec, ctxt.tcx.hir().attrs(field.hir_id)),
3635
),
3736
)
3837
})
@@ -47,8 +46,8 @@ fn check_variant_data<'tcx>(
4746
ident_binder(
4847
&variant_positional_field_ident(name, i),
4948
&(
50-
ty_to_vir(tcx, field.ty),
51-
get_mode(Mode::Exec, tcx.hir().attrs(field.hir_id)),
49+
ty_to_vir(ctxt.tcx, field.ty),
50+
get_mode(Mode::Exec, ctxt.tcx.hir().attrs(field.hir_id)),
5251
),
5352
)
5453
})
@@ -60,35 +59,33 @@ fn check_variant_data<'tcx>(
6059
}
6160

6261
pub fn check_item_struct<'tcx>(
63-
tcx: TyCtxt<'tcx>,
64-
krate: &'tcx Crate<'tcx>,
62+
ctxt: &Context<'tcx>,
6563
vir: &mut KrateX,
6664
span: Span,
6765
id: &ItemId,
6866
variant_data: &'tcx VariantData<'tcx>,
6967
generics: &'tcx Generics<'tcx>,
7068
) -> Result<(), VirErr> {
71-
check_generics(generics)?;
72-
let name = hack_get_def_name(tcx, id.def_id.to_def_id());
73-
let path = def_id_to_vir_path(tcx, id.def_id.to_def_id());
69+
check_generics(ctxt, generics)?;
70+
let name = hack_get_def_name(ctxt.tcx, id.def_id.to_def_id());
71+
let path = def_id_to_vir_path(ctxt.tcx, id.def_id.to_def_id());
7472
let variant_name = variant_ident(&name, &name);
75-
let variants = Rc::new(vec![check_variant_data(tcx, krate, &variant_name, variant_data)]);
76-
vir.datatypes.push(spanned_new(span, DatatypeX { path, variants }));
73+
let variants = Rc::new(vec![check_variant_data(ctxt, &variant_name, variant_data)]);
74+
vir.datatypes.push(spanned_new(ctxt, span, DatatypeX { path, variants }));
7775
Ok(())
7876
}
7977

8078
pub fn check_item_enum<'tcx>(
81-
tcx: TyCtxt<'tcx>,
82-
krate: &'tcx Crate<'tcx>,
79+
ctxt: &Context<'tcx>,
8380
vir: &mut KrateX,
8481
span: Span,
8582
id: &ItemId,
8683
enum_def: &'tcx EnumDef<'tcx>,
8784
generics: &'tcx Generics<'tcx>,
8885
) -> Result<(), VirErr> {
89-
check_generics(generics)?;
90-
let name = Rc::new(hack_get_def_name(tcx, id.def_id.to_def_id()));
91-
let path = def_id_to_vir_path(tcx, id.def_id.to_def_id());
86+
check_generics(ctxt, generics)?;
87+
let name = Rc::new(hack_get_def_name(ctxt.tcx, id.def_id.to_def_id()));
88+
let path = def_id_to_vir_path(ctxt.tcx, id.def_id.to_def_id());
9289
let variants = Rc::new(
9390
enum_def
9491
.variants
@@ -99,10 +96,10 @@ pub fn check_item_enum<'tcx>(
9996
format!("{}{}{}", name, vir::def::VARIANT_SEPARATOR, rust_variant_name)
10097
.as_str(),
10198
);
102-
check_variant_data(tcx, krate, &variant_name, &variant.data)
99+
check_variant_data(ctxt, &variant_name, &variant.data)
103100
})
104101
.collect::<Vec<_>>(),
105102
);
106-
vir.datatypes.push(spanned_new(span, DatatypeX { path, variants }));
103+
vir.datatypes.push(spanned_new(ctxt, span, DatatypeX { path, variants }));
107104
Ok(())
108105
}

0 commit comments

Comments
 (0)