diff --git a/docs/dev-guide/src/config/flags.md b/docs/dev-guide/src/config/flags.md index b3ef1913dc9..b8abb82c915 100644 --- a/docs/dev-guide/src/config/flags.md +++ b/docs/dev-guide/src/config/flags.md @@ -15,6 +15,7 @@ | [`CHECK_TIMEOUT`](#check_timeout) | `Option` | `None` | A | | [`COUNTEREXAMPLE`](#counterexample) | `bool` | `false` | A | | [`DELETE_BASIC_BLOCKS`](#delete_basic_blocks) | `Vec` | `vec![]` | A | +| [`DETECT_UNREACHABLE_CODE`](#detect_unreachable_code) | `bool` | `false` | A | | [`DISABLE_NAME_MANGLING`](#disable_name_mangling) | `bool` | `false` | A | | [`DUMP_BORROWCK_INFO`](#dump_borrowck_info) | `bool` | `false` | A | | [`DUMP_DEBUG_INFO`](#dump_debug_info) | `bool` | `false` | A | @@ -146,6 +147,10 @@ When enabled, Prusti will try to find and print a counterexample for any failed The given basic blocks will be replaced with `assume false`. +## `DETECT_UNREACHABLE_CODE` + +When enabled, Viper will issue warning for code that cannot be reached. + ## `DISABLE_NAME_MANGLING` When enabled, Viper name mangling will be disabled. diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 65a6bc9e624..aef6985a9dc 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -129,6 +129,7 @@ lazy_static::lazy_static! { settings.set_default("use_new_encoder", true).unwrap(); settings.set_default::>("number_of_parallel_verifiers", None).unwrap(); settings.set_default::>("min_prusti_version", None).unwrap(); + settings.set_default("detect_unreachable_code", false).unwrap(); settings.set_default("print_desugared_specs", false).unwrap(); settings.set_default("print_typeckd_specs", false).unwrap(); @@ -958,6 +959,10 @@ pub fn delete_basic_blocks() -> Vec { read_setting("delete_basic_blocks") } +pub fn detect_unreachable_code() -> bool { + read_setting("detect_unreachable_code") +} + /// When enabled, features not supported by Prusti will be reported as warnings /// rather than errors. pub fn skip_unsupported_features() -> bool { 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..7cbc06a1f66 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; @@ -188,25 +187,19 @@ pub enum ErrorCtxt { /// The state that fold-unfold algorithm deduced as unreachable, is actually /// reachable. UnreachableFoldingState, + /// Raised when DETECT_UNREACHABLE_CODE is enabled and an code is determined as unreachable. + UnreachableCode, } /// 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 } @@ -705,6 +698,10 @@ impl<'tcx> ErrorManager<'tcx> { ) } + ("refute.failed:refutation.true", ErrorCtxt::UnreachableCode) => { + PrustiError::warning("Detected unreachable code", error_span) + } + (full_err_id, ErrorCtxt::Unexpected) => { PrustiError::internal( format!( 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 { diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 6d823998555..68a146ddf84 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1257,6 +1257,47 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { ); } + if config::detect_unreachable_code() { + let bb_data = &self.mir.basic_blocks[bbi]; + let statements: &Vec> = &bb_data.statements; + + let panic_free = match &bb_data.terminator().kind { + TerminatorKind::Unreachable => false, + TerminatorKind::Assert { .. } => false, + TerminatorKind::Call { + func: + mir::Operand::Constant(box mir::Constant { + literal, + .. + }), + .. + } => { + if let ty::TyKind::FnDef(called_def_id, _call_substs) = literal.ty().kind() { + let full_func_proc_name: &str = + &self.encoder.env().name.get_absolute_item_name(*called_def_id); + + !matches!(full_func_proc_name, "std::rt::begin_panic" | "core::panicking::panic" | "core::panicking::panic_fmt") + } else { + true + } + } + _ => true, + }; + + if !statements.is_empty() && panic_free { + let location = mir::Location { + block: bbi, + statement_index: 0, + }; + let span = self.mir_encoder.get_span_of_location(location); + let expr_position = self.mir_encoder.register_span(span); + let stmt_position = self.register_error(span, ErrorCtxt::UnreachableCode); + let refute_expr = vir::ast::Expr::Const(vir_crate::polymorphic::ConstExpr{value: vir_crate::polymorphic::Const::Bool(false), position: expr_position}); + let refute_stmt = vir::Stmt::Refute(vir::Refute {expr: refute_expr, position: stmt_position}); + self.cfg_method.add_stmt(curr_block, refute_stmt); + } + } + self.encode_execution_flag(bbi, curr_block)?; let opt_successor = self.encode_block_statements(bbi, curr_block)?; let mir_successor: MirSuccessor = if let Some(successor) = opt_successor { diff --git a/prusti/src/verifier.rs b/prusti/src/verifier.rs index 74775f0d628..0e19ff5f344 100644 --- a/prusti/src/verifier.rs +++ b/prusti/src/verifier.rs @@ -77,7 +77,8 @@ pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) { env.diagnostic.has_errors() || config::internal_errors_as_warnings() || (config::skip_unsupported_features() - && config::allow_unreachable_unsupported_code()) + && config::allow_unreachable_unsupported_code() + || config::detect_unreachable_code()) ); } };