Implement validity checks (#3085)

This is still incomplete, but hopefully it can be merged as an unstable
feature. I'll publish an RFC shortly.

This instruments the function body with assertion checks to see if users
are generating invalid values. This covers:
  - Union access
  - Raw pointer dereference
  - Transmute value
  - Field assignment of struct with invalid values
  - Aggregate assignment

Things not covered today should trigger ICE or a delayed verification
failure due to unsupported feature.

## Design

This change has two main design changes which are inside the new
`kani_compiler::kani_middle::transform` module:
1- Instance body should now be retrieved from the `BodyTransformation`
structure. This structure will run transformation passes on instance
bodies (i.e.: monomorphic instances) and cache the result.
2- Create a new transformation pass that instruments the body of a
function for every potential invalid value generation.
3- Create a body builder which contains all elements of a function body
and mutable functions to modify them accordingly.


Related to #2998
Fixes #301 

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

kani-compiler/src/args.rs

@@ -71,4 +71,15 @@ pub struct Arguments {
     #[clap(long)]
     /// A legacy flag that is now ignored.
     goto_c: bool,
+    /// Enable specific checks.
+    #[clap(long)]
+    pub ub_check: Vec<ExtraChecks>,
+}
+
+#[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);
             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);
         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)