Implement validity checks

kani-compiler/src/args.rs

@@ -71,4 +71,18 @@ pub struct Arguments {
     #[clap(long)]
     /// A legacy flag that is now ignored.
     goto_c: bool,
+    /// Enable specific checks.
+    #[clap(long, conflicts_with = "check_all")]
+    pub ub_check: Vec<ExtraChecks>,
+    /// Enable all extra checks.
+    #[clap(long)]
+    pub check_all: bool,
+}
+
+#[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]
+#[strum(serialize_all = "snake_case")]
+pub enum ExtraChecks {
+    /// Check that produced values are valid except for uninitialized values.
+    /// See https://github.com/model-checking/kani/issues/920.
+    Validity,
 }

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -60,7 +60,7 @@ impl<'tcx> GotocCtx<'tcx> {
             debug!("Double codegen of {:?}", old_sym);
         } else {
             assert!(old_sym.is_function());
-            let body = instance.body().unwrap();
+            let body = self.transformer.body(self.tcx, instance).unwrap();
             self.set_current_fn(instance, &body);
             self.print_instance(instance, &body);
             self.codegen_function_prelude(&body);
@@ -201,7 +201,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     pub fn declare_function(&mut self, instance: Instance) {
         debug!("declaring {}; {:?}", instance.name(), instance);
-        let body = instance.body().unwrap();
+        let body = self.transformer.body(self.tcx, instance).unwrap();
         self.set_current_fn(instance, &body);
         debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
         self.ensure(&self.symbol_name_stable(instance), |ctx, fname| {

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -12,6 +12,7 @@ use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{
     collect_reachable_items, filter_const_crate_items, filter_crate_items,
 };
+use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_middle::{check_reachable_items, dump_mir_items};
 use crate::kani_queries::QueryDb;
 use cbmc::goto_program::Location;
@@ -86,16 +87,18 @@ impl GotocCodegenBackend {
         symtab_goto: &Path,
         machine_model: &MachineModel,
         check_contract: Option<InternalDefId>,
+        mut transformer: BodyTransformation,
     ) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
         let items = with_timer(
-            || collect_reachable_items(tcx, starting_items),
+            || collect_reachable_items(tcx, &mut transformer, starting_items),
             "codegen reachability analysis",
         );
         dump_mir_items(tcx, &items, &symtab_goto.with_extension("kani.mir"));
 
         // Follow rustc naming convention (cx is abbrev for context).
         // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions
-        let mut gcx = GotocCtx::new(tcx, (*self.queries.lock().unwrap()).clone(), machine_model);
+        let mut gcx =
+            GotocCtx::new(tcx, (*self.queries.lock().unwrap()).clone(), machine_model, transformer);
         check_reachable_items(gcx.tcx, &gcx.queries, &items);
 
         let contract_info = with_timer(
@@ -227,6 +230,7 @@ impl CodegenBackend for GotocCodegenBackend {
             // - None: Don't generate code. This is used to compile dependencies.
             let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
             let reachability = queries.args().reachability_analysis;
+            let mut transformer = BodyTransformation::new(&queries, tcx);
             let mut results = GotoCodegenResults::new(tcx, reachability);
             match reachability {
                 ReachabilityType::Harnesses => {
@@ -248,8 +252,9 @@ impl CodegenBackend for GotocCodegenBackend {
                             model_path,
                             &results.machine_model,
                             contract_metadata,
+                            transformer,
                         );
-                        results.extend(gcx, items, None);
+                        transformer = results.extend(gcx, items, None);
                         if let Some(assigns_contract) = contract_info {
                             self.queries.lock().unwrap().register_assigns_contract(
                                 canonical_mangled_name(harness).intern(),
@@ -263,7 +268,7 @@ impl CodegenBackend for GotocCodegenBackend {
                     // test closure that we want to execute
                     // TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match.
                     let mut descriptions = vec![];
-                    let harnesses = filter_const_crate_items(tcx, |_, item| {
+                    let harnesses = filter_const_crate_items(tcx, &mut transformer, |_, item| {
                         if is_test_harness_description(tcx, item.def) {
                             descriptions.push(item.def);
                             true
@@ -282,6 +287,7 @@ impl CodegenBackend for GotocCodegenBackend {
                         &model_path,
                         &results.machine_model,
                         Default::default(),
+                        transformer,
                     );
                     results.extend(gcx, items, None);
 
@@ -319,9 +325,10 @@ impl CodegenBackend for GotocCodegenBackend {
                         &model_path,
                         &results.machine_model,
                         Default::default(),
+                        transformer,
                     );
                     assert!(contract_info.is_none());
-                    results.extend(gcx, items, None);
+                    let _ = results.extend(gcx, items, None);
                 }
             }
 
@@ -613,12 +620,18 @@ impl GotoCodegenResults {
         }
     }
 
-    fn extend(&mut self, gcx: GotocCtx, items: Vec<MonoItem>, metadata: Option<HarnessMetadata>) {
+    fn extend(
+        &mut self,
+        gcx: GotocCtx,
+        items: Vec<MonoItem>,
+        metadata: Option<HarnessMetadata>,
+    ) -> BodyTransformation {
         let mut items = items;
         self.harnesses.extend(metadata);
         self.concurrent_constructs.extend(gcx.concurrent_constructs);
         self.unsupported_constructs.extend(gcx.unsupported_constructs);
         self.items.append(&mut items);
+        gcx.transformer
     }
 
     /// Prints a report at the end of the compilation.

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

@@ -18,6 +18,7 @@ use super::vtable_ctx::VtableCtx;
 use crate::codegen_cprover_gotoc::overrides::{fn_hooks, GotocHooks};
 use crate::codegen_cprover_gotoc::utils::full_crate_name;
 use crate::codegen_cprover_gotoc::UnsupportedConstructs;
+use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_queries::QueryDb;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
@@ -70,6 +71,8 @@ pub struct GotocCtx<'tcx> {
     /// We collect them and print one warning at the end if not empty instead of printing one
     /// warning at each occurrence.
     pub concurrent_constructs: UnsupportedConstructs,
+    /// The body transformation agent.
+    pub transformer: BodyTransformation,
 }
 
 /// Constructor
@@ -78,6 +81,7 @@ impl<'tcx> GotocCtx<'tcx> {
         tcx: TyCtxt<'tcx>,
         queries: QueryDb,
         machine_model: &MachineModel,
+        transformer: BodyTransformation,
     ) -> GotocCtx<'tcx> {
         let fhks = fn_hooks();
         let symbol_table = SymbolTable::new(machine_model.clone());
@@ -99,6 +103,7 @@ impl<'tcx> GotocCtx<'tcx> {
             global_checks_count: 0,
             unsupported_constructs: FxHashMap::default(),
             concurrent_constructs: FxHashMap::default(),
+            transformer,
         }
     }
 }

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -10,6 +10,7 @@
 
 use crate::codegen_cprover_gotoc::codegen::{bb_label, PropertyClass};
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::kani_middle::attributes::matches_diagnostic as matches_function;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::ty::TyCtxt;
@@ -35,17 +36,6 @@ pub trait GotocHook {
     ) -> Stmt;
 }
 
-fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool {
-    let attr_sym = rustc_span::symbol::Symbol::intern(attr_name);
-    if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) {
-        if rustc_internal::internal(tcx, instance.def.def_id()) == *attr_id {
-            debug!("matched: {:?} {:?}", attr_id, attr_sym);
-            return true;
-        }
-    }
-    false
-}
-
 /// A hook for Kani's `cover` function (declared in `library/kani/src/lib.rs`).
 /// The function takes two arguments: a condition expression (bool) and a
 /// message (&'static str).
@@ -57,7 +47,7 @@ fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool {
 struct Cover;
 impl GotocHook for Cover {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance, "KaniCover")
+        matches_function(tcx, instance.def, "KaniCover")
     }
 
     fn handle(
@@ -92,7 +82,7 @@ impl GotocHook for Cover {
 struct Assume;
 impl GotocHook for Assume {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance, "KaniAssume")
+        matches_function(tcx, instance.def, "KaniAssume")
     }
 
     fn handle(
@@ -116,7 +106,7 @@ impl GotocHook for Assume {
 struct Assert;
 impl GotocHook for Assert {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance, "KaniAssert")
+        matches_function(tcx, instance.def, "KaniAssert")
     }
 
     fn handle(
@@ -157,7 +147,7 @@ struct Nondet;
 
 impl GotocHook for Nondet {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance, "KaniAnyRaw")
+        matches_function(tcx, instance.def, "KaniAnyRaw")
     }
 
     fn handle(
@@ -201,7 +191,7 @@ impl GotocHook for Panic {
             || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str)
             || Some(def_id) == tcx.lang_items().panic_fmt()
             || Some(def_id) == tcx.lang_items().begin_panic_fn()
-            || matches_function(tcx, instance, "KaniPanic")
+            || matches_function(tcx, instance.def, "KaniPanic")
     }
 
     fn handle(
@@ -221,7 +211,7 @@ impl GotocHook for Panic {
 struct IsReadOk;
 impl GotocHook for IsReadOk {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance, "KaniIsReadOk")
+        matches_function(tcx, instance.def, "KaniIsReadOk")
     }
 
     fn handle(
@@ -365,7 +355,7 @@ struct UntrackedDeref;
 
 impl GotocHook for UntrackedDeref {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance, "KaniUntrackedDeref")
+        matches_function(tcx, instance.def, "KaniUntrackedDeref")
     }
 
     fn handle(

kani-compiler/src/kani_middle/attributes.rs

@@ -1037,3 +1037,14 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option<KaniAttributeKind> {
         _ => None,
     }
 }
+
+pub fn matches_diagnostic<T: CrateDef>(tcx: TyCtxt, def: T, attr_name: &str) -> bool {
+    let attr_sym = rustc_span::symbol::Symbol::intern(attr_name);
+    if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) {
+        if rustc_internal::internal(tcx, def.def_id()) == *attr_id {
+            debug!("matched: {:?} {:?}", attr_id, attr_sym);
+            return true;
+        }
+    }
+    false
+}

kani-compiler/src/kani_middle/mod.rs

@@ -23,7 +23,7 @@ use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem};
 use stable_mir::mir::pretty::pretty_ty;
-use stable_mir::ty::{BoundVariableKind, RigidTy, Span as SpanStable, Ty, TyKind};
+use stable_mir::ty::{BoundVariableKind, FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
 use stable_mir::visitor::{Visitable, Visitor as TypeVisitor};
 use stable_mir::{CrateDef, DefId};
 use std::fs::File;
@@ -41,6 +41,7 @@ pub mod provide;
 pub mod reachability;
 pub mod resolve;
 pub mod stubbing;
+pub mod transform;
 
 /// Check that all crate items are supported and there's no misconfiguration.
 /// This method will exhaustively print any error / warning and it will abort at the end if any
@@ -316,3 +317,18 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> {
         }
     }
 }
+
+/// Find an instance of a function from the given crate that has been annotated with `diagnostic`
+/// item.
+fn find_fn_def(tcx: TyCtxt, diagnostic: &str) -> Option<FnDef> {
+    let attr_id = tcx
+        .all_diagnostic_items(())
+        .name_to_id
+        .get(&rustc_span::symbol::Symbol::intern(diagnostic))?;
+    let TyKind::RigidTy(RigidTy::FnDef(def, _)) =
+        rustc_internal::stable(tcx.type_of(attr_id)).value.kind()
+    else {
+        return None;
+    };
+    Some(def)
+}

kani-compiler/src/kani_middle/provide.rs

@@ -8,6 +8,7 @@ use crate::args::{Arguments, ReachabilityType};
 use crate::kani_middle::intrinsics::ModelIntrinsics;
 use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use crate::kani_middle::stubbing;
+use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_queries::QueryDb;
 use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_middle::util::Providers;
@@ -79,8 +80,9 @@ fn collect_and_partition_mono_items(
     rustc_smir::rustc_internal::run(tcx, || {
         let local_reachable =
             filter_crate_items(tcx, |_, _| true).into_iter().map(MonoItem::Fn).collect::<Vec<_>>();
+
         // We do not actually need the value returned here.
-        collect_reachable_items(tcx, &local_reachable);
+        collect_reachable_items(tcx, &mut BodyTransformation::dummy(), &local_reachable);
     })
     .unwrap();
     (rustc_interface::DEFAULT_QUERY_PROVIDERS.collect_and_partition_mono_items)(tcx, key)