Extended hacking to get snapshots labeled by line and column number.

Author: parno

verify/rust_verify/src/verifier.rs

@@ -192,7 +192,7 @@ impl Verifier {
         air_context.set_z3_param("air_recommended_options", "true");
         air_context.set_rlimit(self.args.rlimit * 1000000);
 
-        let ctx = vir::context::Ctx::new(&krate, self.args.debug)?;
+        let ctx = vir::context::Ctx::new(&krate, compiler.session().source_map(), self.args.debug)?;
 
         air_context.blank_line();
         air_context.comment("Prelude");

verify/vir/src/context.rs

@@ -1,22 +1,24 @@
 use crate::ast::{Function, Ident, Krate, Mode, Path, Variants, VirErr};
 use crate::def::FUEL_ID;
 use crate::scc::Graph;
+use rustc_span::source_map::SourceMap;
 use air::ast::{Command, CommandX, Commands, DeclX, MultiOp, Span};
 use air::ast_util::str_typ;
 use std::collections::HashMap;
 use std::rc::Rc;
 
-pub struct Ctx {
+pub struct Ctx<'a> {
     pub(crate) datatypes: HashMap<Path, Variants>,
     pub(crate) functions: Vec<Function>,
     pub(crate) func_map: HashMap<Ident, Function>,
     pub(crate) func_call_graph: Graph<Ident>,
+    pub(crate) source_map: &'a SourceMap,
     pub(crate) chosen_triggers: std::cell::RefCell<Vec<(Span, Vec<Vec<String>>)>>, // diagnostics
     pub(crate) debug: bool,
 }
 
-impl Ctx {
-    pub fn new(krate: &Krate, debug:bool) -> Result<Self, VirErr> {
+impl <'a> Ctx<'a> {
+    pub fn new(krate: &Krate, source_map: &'a SourceMap, debug:bool) -> Result<Self, VirErr> {
         let datatypes = krate
             .datatypes
             .iter()
@@ -33,7 +35,7 @@ impl Ctx {
         func_call_graph.compute_sccs();
         let chosen_triggers: std::cell::RefCell<Vec<(Span, Vec<Vec<String>>)>> =
             std::cell::RefCell::new(Vec::new());
-        Ok(Ctx { datatypes, functions, func_map, func_call_graph, chosen_triggers, debug })
+        Ok(Ctx { datatypes, functions, func_map, func_call_graph, source_map, chosen_triggers, debug })
     }
 
     pub fn prelude(&self) -> Commands {

verify/vir/src/lib.rs

@@ -1,5 +1,8 @@
+#![feature(rustc_private)]
 #![feature(or_patterns)]
 
+extern crate rustc_span;
+
 pub mod ast;
 mod ast_to_sst;
 pub mod ast_util;

verify/vir/src/recursion.rs

@@ -21,7 +21,7 @@ struct Ctxt<'a> {
     decreases_exp: Exp,
     decreases_typ: Typ,
     scc_rep: Ident,
-    ctx: &'a Ctx,
+    ctx: &'a Ctx<'a>,
 }
 
 fn check_decrease(ctxt: &Ctxt, exp: &Exp) -> Exp {

verify/vir/src/sst_to_air.rs

@@ -18,6 +18,7 @@ use air::ast_util::{
     bool_typ, ident_apply, ident_binder, ident_typ, ident_var, int_typ, mk_and, mk_eq, mk_exists,
     mk_implies, mk_ite, mk_not, mk_or, str_apply, str_ident, str_typ, str_var, string_var,
 };
+use rustc_span::Pos; //CharPos, FileName, MultiSpan, Span};
 use std::collections::{HashMap, HashSet};
 use std::rc::Rc;
 
@@ -356,8 +357,13 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Vec<Stmt> {
             };
             if ctx.debug {
                 // Add a snapshot before we modify the destination
-                //let (start, end) = source_map.is_valid_span(*stm.span).expect("internal error: invalid Span");
-                let name = format!("{}_{:?}", ident.clone(), stm.span.raw_span); // TODO: Use line number?
+                // TODO: Factor out the span reasoning, so we don't pull rustc into this part of
+                // the code base?
+                let span: &rustc_span::Span = (*stm.span.raw_span)
+                    .downcast_ref::<rustc_span::Span>()
+                    .expect("internal error: failed to cast to Span");
+                let (start, _end) = ctx.source_map.is_valid_span(*span).expect("internal error: invalid Span");
+                let name = format!("{}_{}_{}", ident.clone(), start.line, start.col.to_usize());
                 let snapshot = Rc::new(StmtX::Snapshot(Rc::new(name)));
                 stmts.push(snapshot);
             }