Unreachable code detection

docs/dev-guide/src/config/flags.md

@@ -15,6 +15,7 @@
 | [`CHECK_TIMEOUT`](#check_timeout) | `Option<u32>` | `None` | A |
 | [`COUNTEREXAMPLE`](#counterexample) | `bool` | `false` | A |
 | [`DELETE_BASIC_BLOCKS`](#delete_basic_blocks) | `Vec<String>` | `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.

prusti-utils/src/config.rs

@@ -129,6 +129,7 @@ lazy_static::lazy_static! {
         settings.set_default("use_new_encoder", true).unwrap();
         settings.set_default::<Option<u8>>("number_of_parallel_verifiers", None).unwrap();
         settings.set_default::<Option<String>>("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<String> {
     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 {

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<ErrorManager<'tcx>>,
+    error_manager: RefCell<ErrorManager>,
     /// A map containing all functions: identifier → function definition.
     functions: RefCell<FxHashMap<vir::FunctionIdentifier, Rc<vir::Function>>>,
     builtin_domains: RefCell<FxHashMap<BuiltinDomainKind, vir::Domain>>,
@@ -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<ErrorManager<'tcx>> {
+    pub fn error_manager(&self) -> RefMut<ErrorManager> {
         self.error_manager.borrow_mut()
     }
 

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<u64, ErrorCtxt>,
     inner_positions: FxHashMap<u64, Position>,
 }
 
-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!(

prusti-viper/src/encoder/errors/position_manager.rs

@@ -8,69 +8,41 @@ 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<u64, ProcedureDefId>,
     /// The span of the source code that generated the given VIR position.
     pub(crate) source_span: FxHashMap<u64, MultiSpan>,
 }
 
-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<T: Into<MultiSpan> + 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 {

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<mir::Statement<'tcx>> = &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 {

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())
                 );
             }
         };