From 6c24d7d0327c8fcae5690eed7e5c274cf8f2115b Mon Sep 17 00:00:00 2001 From: Simon Hrabec Date: Wed, 5 Apr 2023 19:08:21 +0900 Subject: [PATCH] make position manager return positions with unique line/column --- prusti-viper/src/encoder/encoder.rs | 6 +-- .../src/encoder/errors/error_manager.rs | 17 ++------ .../src/encoder/errors/position_manager.rs | 42 ++++--------------- 3 files changed, 14 insertions(+), 51 deletions(-) diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index 08e5966d17f..28f239dfe06 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -67,7 +67,7 @@ use super::high::to_typed::types::HighToTypedTypeEncoderState; pub struct Encoder<'v, 'tcx: 'v> { env: &'v Environment<'tcx>, - error_manager: RefCell>, + error_manager: RefCell, /// A map containing all functions: identifier → function definition. functions: RefCell>>, builtin_domains: RefCell>, @@ -151,7 +151,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { Encoder { env, - error_manager: RefCell::new(ErrorManager::new(env.query.codemap())), + error_manager: RefCell::new(ErrorManager::default()), functions: RefCell::new(FxHashMap::default()), builtin_domains: RefCell::new(FxHashMap::default()), builtin_domains_in_progress: RefCell::new(FxHashSet::default()), @@ -228,7 +228,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { self.env } - pub fn error_manager(&self) -> RefMut> { + pub fn error_manager(&self) -> RefMut { self.error_manager.borrow_mut() } diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 53d5e0e6c3d..272569f54a2 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -8,7 +8,6 @@ use std::fmt::Debug; use vir_crate::polymorphic::Position; use rustc_hash::FxHashMap; -use prusti_rustc_interface::span::source_map::SourceMap; use prusti_rustc_interface::errors::MultiSpan; use viper::VerificationError; use prusti_interface::PrustiError; @@ -191,22 +190,14 @@ pub enum ErrorCtxt { } /// The error manager -#[derive(Clone)] -pub struct ErrorManager<'tcx> { - position_manager: PositionManager<'tcx>, +#[derive(Clone, Default)] +pub struct ErrorManager { + position_manager: PositionManager, error_contexts: FxHashMap, inner_positions: FxHashMap, } -impl<'tcx> ErrorManager<'tcx> { - pub fn new(codemap: &'tcx SourceMap) -> Self { - ErrorManager { - position_manager: PositionManager::new(codemap), - error_contexts: FxHashMap::default(), - inner_positions: FxHashMap::default(), - } - } - +impl ErrorManager { pub fn position_manager(&self) -> &PositionManager { &self.position_manager } diff --git a/prusti-viper/src/encoder/errors/position_manager.rs b/prusti-viper/src/encoder/errors/position_manager.rs index b1575ec0e0f..2e58b677cb9 100644 --- a/prusti-viper/src/encoder/errors/position_manager.rs +++ b/prusti-viper/src/encoder/errors/position_manager.rs @@ -8,17 +8,14 @@ use std::fmt::Debug; use vir_crate::polymorphic::Position; use rustc_hash::FxHashMap; -use prusti_rustc_interface::span::source_map::SourceMap; use prusti_rustc_interface::errors::MultiSpan; -use log::debug; use prusti_interface::data::ProcedureDefId; /// Mapping from VIR positions to the source code that generated them. /// One VIR position can be involved in multiple errors. If an error needs to refer to a special /// span, that should be done by adding the span to `ErrorCtxt`, not by registering a new span. #[derive(Clone)] -pub struct PositionManager<'tcx> { - codemap: &'tcx SourceMap, +pub struct PositionManager { next_pos_id: u64, /// The def_id of the procedure that generated the given VIR position. pub(crate) def_id: FxHashMap, @@ -26,51 +23,26 @@ pub struct PositionManager<'tcx> { pub(crate) source_span: FxHashMap, } -impl<'tcx> PositionManager<'tcx> -{ - pub fn new(codemap: &'tcx SourceMap) -> Self { +impl Default for PositionManager { + fn default() -> Self { PositionManager { - codemap, next_pos_id: 1, def_id: FxHashMap::default(), source_span: FxHashMap::default(), } } +} +impl PositionManager +{ #[tracing::instrument(level = "trace", skip(self), ret)] pub fn register_span + Debug>(&mut self, def_id: ProcedureDefId, span: T) -> Position { let span = span.into(); let pos_id = self.next_pos_id; self.next_pos_id += 1; - - let pos = if let Some(primary_span) = span.primary_span() { - let lines_info_res = self - .codemap - .span_to_lines(primary_span.source_callsite()); - match lines_info_res { - Ok(lines_info) => { - if let Some(first_line_info) = lines_info.lines.get(0) { - let line = first_line_info.line_index as i32 + 1; - let column = first_line_info.start_col.0 as i32 + 1; - Position::new(line, column, pos_id) - } else { - debug!("Primary span of position id {} has no lines", pos_id); - Position::new(0, 0, pos_id) - } - } - Err(e) => { - debug!("Error converting primary span of position id {} to lines: {:?}", pos_id, e); - Position::new(0, 0, pos_id) - } - } - } else { - debug!("Position id {} has no primary span", pos_id); - Position::new(0, 0, pos_id) - }; - self.def_id.insert(pos_id, def_id); self.source_span.insert(pos_id, span); - pos + Position::new(pos_id as i32, 0, pos_id) } pub fn duplicate(&mut self, pos: Position) -> Position {