Redefine AIR span to hold file-related info. Still need to update the

many callsites.

Author: parno

verify/air/src/ast.rs

@@ -7,6 +7,11 @@ pub struct Span {
     pub description: Option<String>,
     pub raw_span: RawSpan,
     pub as_string: String, // if we can't print (description, raw_span), print as_string instead
+    pub filename: String,
+    pub start_row: u32,
+    pub start_col: u32,
+    pub end_row: u32,
+    pub end_col: u32,
 }
 pub type SpanOption = Rc<Option<Span>>;
 

verify/air/src/print_parse.rs

@@ -512,7 +512,8 @@ pub(crate) fn node_to_expr(node: &Node) -> Result<Expr, String> {
                 {
                     let raw_span = Rc::new(());
                     let as_string = label[1..label.len() - 1].to_string();
-                    let span = Rc::new(Some(Span { description: None, raw_span, as_string }));
+                    // TODO: Update AIR syntax to support file info
+                    let span = Rc::new(Some(Span { description: None, raw_span, as_string, filename:"".to_string(), start_row:0, start_col: 0, end_row: 0, end_col: 0 }));
                     let expr = node_to_expr(e)?;
                     return Ok(Rc::new(ExprX::LabeledAssertion(span, expr)));
                 }
@@ -714,7 +715,8 @@ pub(crate) fn node_to_stmt(node: &Node) -> Result<Stmt, String> {
             {
                 let raw_span = Rc::new(());
                 let as_string = label[1..label.len() - 1].to_string();
-                let span = Span { description: None, raw_span, as_string };
+                // TODO: Update AIR syntax to support file info
+                let span = Span { description: None, raw_span, as_string, filename:"".to_string(), start_row:0, start_col: 0, end_row: 0, end_col: 0 };
                 let expr = node_to_expr(&e)?;
                 Ok(Rc::new(StmtX::Assert(Rc::new(Some(span)), expr)))
             }

verify/rust_verify/src/util.rs

@@ -1,12 +1,25 @@
-use rustc_span::Span;
+use rustc_span::{FileName, Span};
+use rustc_span::source_map::SourceMap;
 use std::rc::Rc;
+use crate::unsupported;
 use vir::ast::{VirErr, VirErrX};
 use vir::def::Spanned;
 
-pub(crate) fn spanned_new<X>(span: Span, x: X) -> Rc<Spanned<X>> {
+static mut SOURCE_MAP: Option<SourceMap> = None;
+
+pub(crate) fn spanned_new<X>(map: &SourceMap, span: Span, x: X) -> Rc<Spanned<X>> {
     let raw_span = Rc::new(span);
     let as_string = format!("{:?}", span);
-    Spanned::new(air::ast::Span { description: None, raw_span, as_string }, x)
+    let filename: String = match map.span_to_filename(span) {
+        FileName::Real(rfn) => rfn
+            .local_path()
+            .to_str()
+            .expect("internal error: path is not a valid string")
+            .to_string(),
+        _ => unsupported!("non real filenames in verifier errors", span),
+    };
+    let (start, end) = map.is_valid_span(span).expect("internal error: invalid Span");
+    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)
 }
 
 pub(crate) fn err_span_str<A>(span: Span, msg: &str) -> Result<A, VirErr> {