Fix description updates for missing function properties (#1513)

* Update conditions to check for missing undef functions

* Update UI tests

* Remove const string not used anymore

* Import `rustc-demangle` and use it

* Update tests to account for function names

* Short-form for dependencies declaration

* Include demangled name in tests

* Don't use mangled part of demangled name in tests

* Use alternative format for demangled names

* Add backquotes around function names

* Update comment

* Remove backquotes for location

* Update missing function tests

Author: adpaco-aws

Cargo.lock

@@ -344,6 +344,7 @@ dependencies = [
  "once_cell",
  "pathdiff",
  "regex",
+ "rustc-demangle",
  "serde",
  "serde_json",
  "structopt",

kani-driver/Cargo.toml

@@ -24,6 +24,7 @@ clap = "2.34"
 glob = "0.3"
 toml = "0.5"
 regex = "1.6"
+rustc-demangle = "0.1.21"
 pathdiff = "0.2.1"
 
 # A good set of suggested dependencies can be found in rustup:

kani-driver/src/cbmc_output_parser.rs

@@ -25,6 +25,7 @@ use console::style;
 use once_cell::sync::Lazy;
 use pathdiff::diff_paths;
 use regex::Regex;
+use rustc_demangle::demangle;
 use serde::Deserialize;
 use std::{
     collections::HashMap,
@@ -176,7 +177,6 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
 
 const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani";
 const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop";
-const ASSERTION_FALSE: &str = "assertion false";
 const DEFAULT_ASSERTION: &str = "assertion";
 const REACH_CHECK_DESC: &str = "[KANI_REACHABILITY_CHECK]";
 
@@ -277,7 +277,8 @@ impl std::fmt::Display for SourceLocation {
             write!(&mut fmt_str, "Unknown file")?;
         }
         if let Some(function) = self.function.clone() {
-            write!(&mut fmt_str, " in function {function}")?;
+            let demangled_function = demangle(&function);
+            write!(&mut fmt_str, " in function {:#}", demangled_function)?;
         }
 
         write! {f, "{}", fmt_str}
@@ -811,16 +812,17 @@ fn has_check_failure(properties: &Vec<Property>, description: &str) -> bool {
 
 /// Replaces the description of all properties from functions with a missing
 /// definition.
-/// TODO: This hasn't been working as expected, see
-/// <https://github.com/model-checking/kani/issues/1424>
 fn modify_undefined_function_checks(mut properties: Vec<Property>) -> (Vec<Property>, bool) {
     let mut has_unknown_location_checks = false;
     for mut prop in &mut properties {
-        if prop.description.contains(ASSERTION_FALSE)
-            && extract_property_class(prop).unwrap() == DEFAULT_ASSERTION
+        if let Some(function) = &prop.source_location.function
+            && prop.description == DEFAULT_ASSERTION
             && prop.source_location.file.is_none()
         {
-            prop.description = "Function with missing definition is unreachable".to_string();
+            // Missing functions come with mangled names.
+            // `demangle` produces the demangled version if it's a mangled name.
+            let modified_description = format!("Function `{:#}` with missing definition is unreachable", demangle(function));
+            prop.description = modified_description;
             if prop.status == CheckStatus::Failure {
                 has_unknown_location_checks = true;
             }

tests/ui/missing-function/extern_c/expected

@@ -1,4 +1,5 @@
-Status: UNREACHABLE\
+Status: UNDETERMINED\
 Description: "assertion failed: x == 5"
-
+Status: FAILURE\
+Description: "Function `missing_function` with missing definition is unreachable"
 VERIFICATION:- FAILED

tests/ui/missing-function/extern_c/extern_c.rs

@@ -7,8 +7,6 @@
 // TODO: Verify that this prints a compiler warning:
 //  - https://github.com/model-checking/kani/issues/576
 
-// TODO: Missing functions produce non-informative property descriptions
-// https://github.com/model-checking/kani/issues/1271
 extern "C" {
     fn missing_function() -> u32;
 }

tests/ui/missing-function/replaced-description/expected

@@ -1,2 +1,3 @@
 Status: FAILURE\
-Description: "assertion"
+Description: "Function `<alloc::string::String as core::clone::Clone>::clone` with missing definition is unreachable"
+Status: UNDETERMINED

tests/ui/missing-function/replaced-description/main.rs

@@ -1,10 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// This test is to check if the description for undefined functions has been updated to "Function with missing definition is unreachable"
+// Checks if the description for undefined functions has been updated to
+// "Function with missing definition is unreachable"
 
-// TODO: Missing functions produce non-informative property descriptions
-// https://github.com/model-checking/kani/issues/1271
 #[kani::proof]
 fn main() {
     let x = String::from("foo");

tests/ui/missing-function/rust-by-example-description/expected

@@ -1,2 +1,3 @@
 Status: FAILURE\
-Description: "assertion"
+Description: "Function `core::num::<impl core::str::traits::FromStr for i32>::from_str` with missing definition is unreachable"
+Status: UNDETERMINED

tests/ui/missing-function/rust-by-example-description/main.rs

@@ -4,8 +4,6 @@
 // kani-flags: --enable-unstable --cbmc-args --unwind 4 --object-bits 9
 // This test is to check if the description for undefined functions has been updated to "Function with missing definition is unreachable"
 
-// TODO: Missing functions produce non-informative property descriptions
-// https://github.com/model-checking/kani/issues/1271
 #![allow(unused)]
 #[kani::proof]
 pub fn main() {