Skip to content

Commit 1b54753

Browse files
parnoparno
committed
After extensive wrestling with lifetime parameters, the new context
finally goes through.
1 parent 24b825a commit 1b54753

File tree

10 files changed

+58
-61
lines changed

10 files changed

+58
-61
lines changed

‎verify/air/src/ast.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@ pub struct Span {
88
pub raw_span: RawSpan,
99
pub as_string: String, // if we can't print (description, raw_span), print as_string instead
1010
pub filename: String,
11-
pub start_row: u32,
12-
pub start_col: u32,
13-
pub end_row: u32,
14-
pub end_col: u32,
11+
pub start_row: usize,
12+
pub start_col: usize,
13+
pub end_row: usize,
14+
pub end_col: usize,
1515
}
1616
pub type SpanOption = Rc<Option<Span>>;
1717

‎verify/rust_verify/src/context.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ use rustc_middle::ty::TyCtxt;
22
use rustc_hir::Crate;
33
use rustc_span::source_map::SourceMap;
44

5-
pub(crate) struct Context<'tcx> {
5+
pub struct Context<'tcx,'sm> {
66
pub(crate) tcx: TyCtxt<'tcx>,
77
pub(crate) krate: &'tcx Crate<'tcx>,
8-
pub(crate) source_map: &'tcx SourceMap,
8+
pub(crate) source_map: &'sm SourceMap,
99
}

‎verify/rust_verify/src/rust_to_vir.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@ use rustc_span::def_id::LocalDefId;
2222
use std::rc::Rc;
2323
use vir::ast::{Krate, KrateX, VirErr};
2424

25-
fn check_item<'tcx>(
26-
ctxt: &'tcx Context<'tcx>,
25+
fn check_item<'tcx,'sm>(
26+
ctxt: &Context<'tcx,'sm>,
2727
vir: &mut KrateX,
2828
id: &ItemId,
2929
item: &'tcx Item<'tcx>,
@@ -190,8 +190,8 @@ fn check_module<'tcx>(
190190
Ok(())
191191
}
192192

193-
fn check_foreign_item<'tcx>(
194-
ctxt: &Context<'tcx>,
193+
fn check_foreign_item<'tcx,'sm>(
194+
ctxt: &Context<'tcx,'sm>,
195195
vir: &mut KrateX,
196196
_id: &ForeignItemId,
197197
item: &'tcx ForeignItem<'tcx>,
@@ -225,7 +225,7 @@ fn check_attr<'tcx>(
225225
Ok(())
226226
}
227227

228-
pub fn crate_to_vir<'tcx>(ctxt: &Context<'tcx>) -> Result<Krate, VirErr> {
228+
pub fn crate_to_vir<'tcx,'sm>(ctxt: &Context<'tcx,'sm>) -> Result<Krate, VirErr> {
229229
let Crate {
230230
item: _,
231231
exported_macros,

‎verify/rust_verify/src/rust_to_vir_adts.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ 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

14-
fn check_variant_data<'tcx>(
15-
ctxt: &Context<'tcx>,
14+
fn check_variant_data<'tcx,'sm>(
15+
ctxt: &Context<'tcx,'sm>,
1616
name: &Ident,
1717
variant_data: &'tcx VariantData<'tcx>,
1818
) -> Variant {
@@ -58,8 +58,8 @@ fn check_variant_data<'tcx>(
5858
)
5959
}
6060

61-
pub fn check_item_struct<'tcx>(
62-
ctxt: &Context<'tcx>,
61+
pub fn check_item_struct<'tcx,'sm>(
62+
ctxt: &Context<'tcx,'sm>,
6363
vir: &mut KrateX,
6464
span: Span,
6565
id: &ItemId,
@@ -75,8 +75,8 @@ pub fn check_item_struct<'tcx>(
7575
Ok(())
7676
}
7777

78-
pub fn check_item_enum<'tcx>(
79-
ctxt: &Context<'tcx>,
78+
pub fn check_item_enum<'tcx,'sm>(
79+
ctxt: &Context<'tcx,'sm>,
8080
vir: &mut KrateX,
8181
span: Span,
8282
id: &ItemId,

‎verify/rust_verify/src/rust_to_vir_base.rs

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -259,19 +259,19 @@ pub(crate) fn ty_to_vir<'tcx>(tcx: TyCtxt<'tcx>, ty: &Ty) -> Typ {
259259
Rc::new(typ_x)
260260
}
261261

262-
pub(crate) struct BodyCtxt<'tcx> {
263-
pub(crate) ctxt: &'tcx Context<'tcx>,
262+
pub(crate) struct BodyCtxt<'tcx, 'sm> {
263+
pub(crate) ctxt: &'sm Context<'tcx,'sm>,
264264
pub(crate) types: &'tcx TypeckResults<'tcx>,
265265
pub(crate) mode: Mode,
266266
}
267267

268-
pub(crate) fn typ_of_node<'tcx>(ctxt: &BodyCtxt<'tcx>, id: &HirId) -> Typ {
268+
pub(crate) fn typ_of_node<'tcx,'sm>(ctxt: &BodyCtxt<'tcx,'sm>, id: &HirId) -> Typ {
269269
mid_ty_to_vir(ctxt.ctxt.tcx, ctxt.types.node_type(*id))
270270
}
271271

272272
// Do equality operations on these operands translate into the SMT solver's == operation?
273-
pub(crate) fn is_smt_equality<'tcx>(
274-
ctxt: &BodyCtxt<'tcx>,
273+
pub(crate) fn is_smt_equality<'tcx,'sm>(
274+
ctxt: &BodyCtxt<'tcx,'sm>,
275275
_span: Span,
276276
id1: &HirId,
277277
id2: &HirId,
@@ -302,15 +302,15 @@ pub(crate) fn is_smt_equality<'tcx>(
302302

303303
// Do arithmetic operations on these operands translate into the SMT solver's <=, +, =>, etc.?
304304
// (possibly with clipping/wrapping for finite-size integers?)
305-
pub(crate) fn is_smt_arith<'tcx>(ctxt: &BodyCtxt<'tcx>, id1: &HirId, id2: &HirId) -> bool {
305+
pub(crate) fn is_smt_arith<'tcx,'sm>(ctxt: &BodyCtxt<'tcx,'sm>, id1: &HirId, id2: &HirId) -> bool {
306306
match (&*typ_of_node(ctxt, id1), &*typ_of_node(ctxt, id2)) {
307307
(TypX::Bool, TypX::Bool) => true,
308308
(TypX::Int(_), TypX::Int(_)) => true,
309309
_ => false,
310310
}
311311
}
312312

313-
pub(crate) fn check_generics<'tcx>(ctxt: &Context<'tcx>, generics: &'tcx Generics<'tcx>) -> Result<Idents, VirErr> {
313+
pub(crate) fn check_generics<'tcx,'sm>(ctxt: &Context<'tcx,'sm>, generics: &'tcx Generics<'tcx>) -> Result<Idents, VirErr> {
314314
let Generics { params, where_clause, span: _ } = generics;
315315
let mut typ_params: Vec<vir::ast::Ident> = Vec::new();
316316
for param in params.iter() {

‎verify/rust_verify/src/rust_to_vir_expr.rs

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -73,15 +73,15 @@ fn extract_array<'tcx>(expr: &'tcx Expr<'tcx>) -> Vec<&'tcx Expr<'tcx>> {
7373
}
7474
}
7575

76-
fn get_ensures_arg<'tcx>(ctxt: &BodyCtxt<'tcx>, expr: &Expr<'tcx>) -> Result<vir::ast::Expr, VirErr> {
76+
fn get_ensures_arg<'tcx,'sm>(ctxt: &BodyCtxt<'tcx,'sm>, expr: &Expr<'tcx>) -> Result<vir::ast::Expr, VirErr> {
7777
if matches!(ctxt.types.node_type(expr.hir_id).kind(), TyKind::Bool) {
7878
expr_to_vir(ctxt, expr)
7979
} else {
8080
err_span_str(ctxt.ctxt, expr.span, "ensures needs a bool expression")
8181
}
8282
}
8383

84-
fn extract_ensures<'tcx>(ctxt: &BodyCtxt<'tcx>, expr: &'tcx Expr<'tcx>) -> Result<HeaderExpr, VirErr> {
84+
fn extract_ensures<'tcx,'sm>(ctxt: &BodyCtxt<'tcx,'sm>, expr: &'tcx Expr<'tcx>) -> Result<HeaderExpr, VirErr> {
8585
let tcx = ctxt.ctxt.tcx;
8686
match &expr.kind {
8787
ExprKind::Closure(_, fn_decl, body_id, _, _) => {
@@ -104,8 +104,8 @@ fn extract_ensures<'tcx>(ctxt: &BodyCtxt<'tcx>, expr: &'tcx Expr<'tcx>) -> Resul
104104
}
105105
}
106106

107-
fn extract_quant<'tcx>(
108-
ctxt: &BodyCtxt<'tcx>,
107+
fn extract_quant<'tcx,'sm>(
108+
ctxt: &BodyCtxt<'tcx,'sm>,
109109
span: Span,
110110
quant: Quant,
111111
expr: &'tcx Expr<'tcx>,
@@ -144,8 +144,8 @@ fn mk_ty_clip<'tcx>(ty: rustc_middle::ty::Ty<'tcx>, expr: &vir::ast::Expr) -> vi
144144
mk_clip(&mk_range(ty), expr)
145145
}
146146

147-
pub(crate) fn expr_to_vir<'tcx>(
148-
ctxt: &BodyCtxt<'tcx>,
147+
pub(crate) fn expr_to_vir<'tcx,'sm>(
148+
ctxt: &BodyCtxt<'tcx,'sm>,
149149
expr: &Expr<'tcx>,
150150
) -> Result<vir::ast::Expr, VirErr> {
151151
let mut vir_expr = expr_to_vir_inner(ctxt, expr)?;
@@ -155,8 +155,8 @@ pub(crate) fn expr_to_vir<'tcx>(
155155
Ok(vir_expr)
156156
}
157157

158-
fn fn_call_to_vir<'tcx>(
159-
ctxt: &BodyCtxt<'tcx>,
158+
fn fn_call_to_vir<'tcx,'sm>(
159+
ctxt: &BodyCtxt<'tcx,'sm>,
160160
expr: &Expr<'tcx>,
161161
fun: &'tcx Expr<'tcx>,
162162
args_slice: &'tcx [Expr<'tcx>],
@@ -358,8 +358,8 @@ fn fn_call_to_vir<'tcx>(
358358
}
359359
}
360360

361-
pub(crate) fn expr_tuple_datatype_ctor_to_vir<'tcx>(
362-
ctxt: &BodyCtxt<'tcx>,
361+
pub(crate) fn expr_tuple_datatype_ctor_to_vir<'tcx,'sm>(
362+
ctxt: &BodyCtxt<'tcx,'sm>,
363363
expr: &Expr<'tcx>,
364364
res: &Res,
365365
args_slice: &[Expr<'tcx>],
@@ -415,8 +415,8 @@ pub(crate) fn expr_tuple_datatype_ctor_to_vir<'tcx>(
415415
Ok(spanned_new(ctxt.ctxt, expr.span, ExprX::Ctor(vir_path, variant_name, vir_fields)))
416416
}
417417

418-
pub(crate) fn expr_to_vir_inner<'tcx>(
419-
ctxt: &BodyCtxt<'tcx>,
418+
pub(crate) fn expr_to_vir_inner<'tcx,'sm>(
419+
ctxt: &BodyCtxt<'tcx,'sm>,
420420
expr: &Expr<'tcx>,
421421
) -> Result<vir::ast::Expr, VirErr> {
422422
let tcx = ctxt.ctxt.tcx;
@@ -724,8 +724,8 @@ pub(crate) fn expr_to_vir_inner<'tcx>(
724724
}
725725
}
726726

727-
pub(crate) fn let_stmt_to_vir<'tcx>(
728-
ctxt: &BodyCtxt<'tcx>,
727+
pub(crate) fn let_stmt_to_vir<'tcx,'sm>(
728+
ctxt: &BodyCtxt<'tcx,'sm>,
729729
pattern: &rustc_hir::Pat<'tcx>,
730730
initializer: &Option<&Expr<'tcx>>,
731731
attrs: &[Attribute],
@@ -766,8 +766,8 @@ pub(crate) fn let_stmt_to_vir<'tcx>(
766766
}
767767
}
768768

769-
pub(crate) fn stmt_to_vir<'tcx>(
770-
ctxt: &BodyCtxt<'tcx>,
769+
pub(crate) fn stmt_to_vir<'tcx,'sm>(
770+
ctxt: &BodyCtxt<'tcx,'sm>,
771771
stmt: &Stmt<'tcx>,
772772
) -> Result<Vec<vir::ast::Stmt>, VirErr> {
773773
match &stmt.kind {

‎verify/rust_verify/src/rust_to_vir_func.rs

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -14,16 +14,16 @@ use std::rc::Rc;
1414
use vir::ast::{FunctionX, KrateX, Mode, ParamX, Typ, VirErr};
1515
use vir::def::RETURN_VALUE;
1616

17-
pub(crate) fn body_to_vir<'tcx>(
18-
ctxt: &'tcx Context<'tcx>,
17+
pub(crate) fn body_to_vir<'tcx,'sm>(
18+
ctxt: &Context<'tcx,'sm>,
1919
id: &BodyId,
2020
body: &Body<'tcx>,
2121
mode: Mode,
2222
) -> Result<vir::ast::Expr, VirErr> {
2323
let def = rustc_middle::ty::WithOptConstParam::unknown(id.hir_id.owner);
2424
let types = ctxt.tcx.typeck_opt_const_arg(def);
25-
let ctxt = BodyCtxt { ctxt, types, mode };
26-
expr_to_vir(&ctxt, &body.value)
25+
let bctx = BodyCtxt { ctxt, types, mode };
26+
expr_to_vir(&bctx, &body.value)
2727
}
2828

2929
fn check_fn_decl<'tcx>(
@@ -46,8 +46,8 @@ fn check_fn_decl<'tcx>(
4646
}
4747
}
4848

49-
pub(crate) fn check_item_fn<'tcx>(
50-
ctxt: &'tcx Context<'tcx>,
49+
pub(crate) fn check_item_fn<'tcx,'sm>(
50+
ctxt: &Context<'tcx,'sm>,
5151
vir: &mut KrateX,
5252
id: Ident,
5353
attrs: &[Attribute],
@@ -139,8 +139,8 @@ pub(crate) fn check_item_fn<'tcx>(
139139
Ok(())
140140
}
141141

142-
pub(crate) fn check_foreign_item_fn<'tcx>(
143-
ctxt: &Context<'tcx>,
142+
pub(crate) fn check_foreign_item_fn<'tcx,'sm>(
143+
ctxt: &Context<'tcx,'sm>,
144144
vir: &mut KrateX,
145145
id: Ident,
146146
span: Span,

‎verify/rust_verify/src/util.rs

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
use rustc_span::{FileName, Span};
2-
use rustc_span::source_map::SourceMap;
1+
use rustc_span::{FileName, Span, Pos};
32
use std::rc::Rc;
43
use crate::unsupported;
54
use vir::ast::{VirErr, VirErrX};
@@ -9,16 +8,16 @@ use crate::context::Context;
98
pub(crate) fn spanned_new<X>(ctxt: &Context, span: Span, x: X) -> Rc<Spanned<X>> {
109
let raw_span = Rc::new(span);
1110
let as_string = format!("{:?}", span);
12-
let filename: String = match map.span_to_filename(span) {
11+
let filename: String = match ctxt.source_map.span_to_filename(span) {
1312
FileName::Real(rfn) => rfn
1413
.local_path()
1514
.to_str()
1615
.expect("internal error: path is not a valid string")
1716
.to_string(),
1817
_ => unsupported!("non real filenames in verifier errors", span),
1918
};
20-
let (start, end) = map.is_valid_span(span).expect("internal error: invalid Span");
21-
Spanned::new(air::ast::Span { description: None, raw_span, as_string, filename, start_row:start.line, start_col:start.col.to_u32(), end_row:end.line, end_col:end.col.to_u32() }, x)
19+
let (start, end) = ctxt.source_map.is_valid_span(span).expect("internal error: invalid Span");
20+
Spanned::new(air::ast::Span { description: None, raw_span, as_string, filename, start_row:start.line, start_col:start.col.to_usize(), end_row:end.line, end_col:end.col.to_usize() }, x)
2221
}
2322

2423
pub(crate) fn err_span_str<A>(ctxt: &Context, span: Span, msg: &str) -> Result<A, VirErr> {

‎verify/rust_verify/src/verifier.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -273,7 +273,7 @@ impl Verifier {
273273
Ok(())
274274
}
275275

276-
fn run<'tcx>(&mut self, compiler: &'tcx Compiler, tcx: TyCtxt<'tcx>) -> Result<bool, VirErr> {
276+
fn run<'tcx>(&mut self, compiler: &Compiler, tcx: TyCtxt<'tcx>) -> Result<bool, VirErr> {
277277
let _ = tcx.formal_verifier_callback.replace(Some(Box::new(crate::typecheck::Typecheck {
278278
int_ty_id: None,
279279
nat_ty_id: None,
@@ -340,9 +340,9 @@ impl rustc_driver::Callbacks for Verifier {
340340
}
341341
}
342342

343-
fn after_expansion<'tcx>(
344-
&mut self,
345-
compiler: &Compiler,
343+
fn after_expansion<'a,'tcx>(
344+
&'a mut self,
345+
compiler: &'a Compiler,
346346
queries: &'tcx rustc_interface::Queries<'tcx>,
347347
) -> rustc_driver::Compilation {
348348
let _result = queries.global_ctxt().expect("global_ctxt").peek_mut().enter(|tcx| {

‎verify/vir/src/sst_to_air.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -321,7 +321,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
321321
}
322322
if ctx.debug {
323323
// Add a snapshot after we modify the destination
324-
let name = format!("{}_{:?}", var.clone(), stm.span.raw_span); // TODO: Use line number?
324+
let name = format!("{}_{}_{}", var.clone(), stm.span.start_row, stm.span.start_col);
325325
let snapshot = Rc::new(StmtX::Snapshot(Rc::new(name)));
326326
stmts.push(snapshot);
327327
}
@@ -356,10 +356,8 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
356356
};
357357
stmts.push(Rc::new(StmtX::Assign(suffix_local_id(&ident), exp_to_expr(ctx, rhs))));
358358
if ctx.debug {
359-
//let name = format!("{}_{}_{}", ident.clone(), start.line, start.col.to_usize());
360359
// Add a snapshot after we modify the destination
361-
//let (start, end) = source_map.is_valid_span(*stm.span).expect("internal error: invalid Span");
362-
let name = format!("{}_{:?}", ident.clone(), stm.span.raw_span); // TODO: Use line number?
360+
let name = format!("{}_{}_{}", ident.clone(), stm.span.start_row, stm.span.start_col);
363361
let snapshot = Rc::new(StmtX::Snapshot(Rc::new(name)));
364362
stmts.push(snapshot);
365363
}

0 commit comments

Comments
 (0)