Add warning for unsupported constructs (rust-lang#1095)

Author: celinval

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -5,7 +5,7 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use bitflags::_core::any::Any;
-use cbmc::goto_program::symtab_transformer;
+use cbmc::goto_program::{symtab_transformer, Location};
 use cbmc::InternedString;
 use kani_metadata::KaniMetadata;
 use kani_queries::{QueryDb, UserInput};
@@ -121,6 +121,9 @@ impl CodegenBackend for GotocCodegenBackend {
             }
         }
 
+        // Print compilation report.
+        print_report(&c, tcx);
+
         // perform post-processing symbol table passes
         let passes = self.queries.get_symbol_table_passes();
         let symtab = symtab_transformer::do_passes(c.symbol_table, &passes);
@@ -258,3 +261,24 @@ where
         serde_json::to_writer(writer, &source).unwrap();
     }
 }
+
+/// Prints a report at the end of the compilation.
+fn print_report<'tcx>(ctx: &GotocCtx, tcx: TyCtxt<'tcx>) {
+    // Print all unsupported constructs.
+    if !ctx.unsupported_constructs.is_empty() {
+        // Sort alphabetically.
+        let unsupported: BTreeMap<String, &Vec<Location>> = ctx
+            .unsupported_constructs
+            .iter()
+            .map(|(key, val)| (key.map(|s| String::from(s)), val))
+            .collect();
+        let mut msg = String::from("Found the following unsupported constructs:\n");
+        unsupported.iter().for_each(|(construct, locations)| {
+            msg += &format!("    - {} ({})\n", construct, locations.len())
+        });
+        msg += "\nVerification will fail if one or more of these constructs is reachable.";
+        msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \
+        details.";
+        tcx.sess.warn(&msg);
+    }
+}

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -61,6 +61,8 @@ pub struct GotocCtx<'tcx> {
     pub proof_harnesses: Vec<HarnessMetadata>,
     /// a global counter for generating unique IDs for checks
     pub global_checks_count: u64,
+    /// A map of unsupported constructs that were found while codegen
+    pub unsupported_constructs: FxHashMap<InternedString, Vec<Location>>,
 }
 
 /// Constructor
@@ -83,6 +85,7 @@ impl<'tcx> GotocCtx<'tcx> {
             type_map: FxHashMap::default(),
             proof_harnesses: vec![],
             global_checks_count: 0,
+            unsupported_constructs: FxHashMap::default(),
         }
     }
 }

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -3,11 +3,11 @@
 use super::super::codegen::TypeExt;
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::btree_string_map;
 use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, SymbolTable, Type};
+use cbmc::{btree_string_map, InternedString};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::Ty;
-use tracing::warn;
+use tracing::debug;
 
 // Should move into rvalue
 //make this a member function
@@ -46,18 +46,20 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This means that if the unimplemented feature is dynamically used by the code being verified, we will see an assertion failure.
     /// If it is not used, we the assertion will pass.
     /// This allows us to continue to make progress parsing rust code, while remaining sound (thanks to the `assert(false)`)
-    ///
-    /// TODO: https://github.com/model-checking/kani/issues/8 assume the required validity constraints for the nondet return
-    /// TODO: https://github.com/model-checking/kani/issues/9 Have a parameter that decides whether to `assume(0)` to block further traces or not
     pub fn codegen_unimplemented(
         &mut self,
         operation_name: &str,
         t: Type,
         loc: Location,
         url: &str,
     ) -> Expr {
-        // TODO: This should print a more user friendly warning format.
-        warn!("codegen_unimplemented: {} at {}", operation_name, loc.short_string());
+        // Save this occurrence so we can emit a warning in the compilation report.
+        debug!("codegen_unimplemented: {} at {}", operation_name, loc.short_string());
+        let key: InternedString = operation_name.into();
+        if !self.unsupported_constructs.contains_key(&key) {
+            self.unsupported_constructs.insert(key, Vec::new());
+        }
+        self.unsupported_constructs.get_mut(&key).unwrap().push(loc.clone());
 
         let body = vec![
             // Assert false to alert the user that there is a path that uses an unimplemented feature.

tests/kani/Options/check_tests.rs

@@ -20,7 +20,7 @@ mod test {
     #[test]
     #[kani::proof]
     fn test_harness() {
-        let input: i32 = kani::nondet();
+        let input: i32 = kani::any();
         kani::assume(input > 1);
         fn_under_verification(input);
     }

tests/ui/unsupported-features/thread/expected

@@ -1 +1,7 @@
+warning: Found the following unsupported constructs:\
+Rvalue::ThreadLocalRef\
+\
+Verification will fail if one or more of these constructs is reachable.\
+See https://model-checking.github.io/kani/rust-feature-support.html for more details.
+
 Failed Checks: Rvalue::ThreadLocalRef is not currently supported by Kani.