From 217ef98cb7c05961deffb307a0406f65f345a2a1 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 13 Sep 2022 17:18:02 -0700 Subject: [PATCH 1/9] Add initial implementation of the reachability algorithm TODO: - Cleanup the code. - Add more tests. --- .../codegen_cprover_gotoc/codegen/function.rs | 23 + .../compiler_interface.rs | 214 ++++--- .../src/codegen_cprover_gotoc/mod.rs | 1 + .../src/codegen_cprover_gotoc/reachability.rs | 586 ++++++++++++++++++ kani-compiler/src/main.rs | 6 +- .../mir-linker/Cargo.toml | 3 +- tests/cargo-kani/mir-linker/expected | 3 + tests/cargo-kani/mir-linker/src/lib.rs | 29 + tests/cargo-ui/mir-linker/expected | 1 - tests/cargo-ui/mir-linker/src/lib.rs | 13 - tests/ui/mir-linker/expected | 3 +- tests/ui/mir-linker/generic-harness/expected | 1 + .../mir-linker/generic-harness/incorrect.rs | 16 + tests/ui/unwind-without-proof/main.rs | 1 + tools/compiletest/src/common.rs | 5 + tools/compiletest/src/main.rs | 2 + tools/compiletest/src/runtest.rs | 12 + 17 files changed, 816 insertions(+), 103 deletions(-) create mode 100644 kani-compiler/src/codegen_cprover_gotoc/reachability.rs rename tests/{cargo-ui => cargo-kani}/mir-linker/Cargo.toml (74%) create mode 100644 tests/cargo-kani/mir-linker/expected create mode 100644 tests/cargo-kani/mir-linker/src/lib.rs delete mode 100644 tests/cargo-ui/mir-linker/expected delete mode 100644 tests/cargo-ui/mir-linker/src/lib.rs create mode 100644 tests/ui/mir-linker/generic-harness/expected create mode 100644 tests/ui/mir-linker/generic-harness/incorrect.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 3c59ec3d9b93..023a9fb02847 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -9,6 +9,8 @@ use cbmc::InternString; use kani_metadata::HarnessMetadata; use rustc_ast::ast; use rustc_ast::{Attribute, LitKind}; +use rustc_hir::def::DefKind; +use rustc_hir::def_id::DefId; use rustc_middle::mir::{HasLocalDecls, Local}; use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::{self, Instance}; @@ -262,6 +264,27 @@ impl<'tcx> GotocCtx<'tcx> { self.reset_current_fn(); } + pub fn is_proof_harness(&self, def_id: DefId) -> bool { + let all_attributes = self.tcx.get_attrs_unchecked(def_id); + let (proof_attributes, _) = partition_kanitool_attributes(all_attributes); + if !proof_attributes.is_empty() { + let span = proof_attributes.first().unwrap().span; + if self.tcx.def_kind(def_id) != DefKind::Fn { + self.tcx + .sess + .span_err(span, "The kani::proof attribute can only be applied to functions."); + } else if self.tcx.generics_of(def_id).requires_monomorphization(self.tcx) { + self.tcx + .sess + .span_err(span, "The proof attribute cannot be applied to generic functions."); + } + self.tcx.sess.abort_if_errors(); + true + } else { + false + } + } + /// This updates the goto context with any information that should be accumulated from a function's /// attributes. /// diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 2b5cd8f0f05f..e3c28e942267 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -3,10 +3,11 @@ //! This file contains the code necessary to interface with the compiler backend +use crate::codegen_cprover_gotoc::reachability::collect_reachable_items; use crate::codegen_cprover_gotoc::GotocCtx; use bitflags::_core::any::Any; use cbmc::goto_program::{symtab_transformer, Location}; -use cbmc::InternedString; +use cbmc::{InternedString, MachineModel}; use kani_metadata::KaniMetadata; use kani_queries::{QueryDb, ReachabilityType, UserInput}; use rustc_codegen_ssa::traits::CodegenBackend; @@ -17,7 +18,7 @@ use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::mir::mono::{CodegenUnit, MonoItem}; use rustc_middle::ty::query::Providers; -use rustc_middle::ty::{self, TyCtxt}; +use rustc_middle::ty::{self, Instance, TyCtxt}; use rustc_session::config::{OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::Session; @@ -60,95 +61,95 @@ impl CodegenBackend for GotocCodegenBackend { super::utils::init(); check_target(tcx.sess); - check_options(tcx.sess, need_metadata_module, self.queries.clone()); - - let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1; - let mut c = GotocCtx::new(tcx, self.queries.clone()); + check_options(tcx.sess, need_metadata_module); + + // 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.clone()); + let items = codegen_items(tcx, &gcx); + if items.is_empty() { + // There's nothing to do. + return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); + } // we first declare all functions - for cgu in codegen_units { - let items = cgu.items_in_deterministic_order(tcx); - for (item, _) in items { - match item { - MonoItem::Fn(instance) => { - c.call_with_panic_debug_info( - |ctx| ctx.declare_function(instance), - format!("declare_function: {}", c.readable_instance_name(instance)), - instance.def_id(), + for item in &items { + match *item { + MonoItem::Fn(instance) => { + gcx.call_with_panic_debug_info( + |ctx| ctx.declare_function(instance), + format!("declare_function: {}", gcx.readable_instance_name(instance)), + instance.def_id(), + ); + } + MonoItem::Static(def_id) => { + gcx.call_with_panic_debug_info( + |ctx| ctx.declare_static(def_id, *item), + format!("declare_static: {:?}", def_id), + def_id, + ); + } + MonoItem::GlobalAsm(_) => { + if !self.queries.get_ignore_global_asm() { + let error_msg = format!( + "Crate {} contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**).", + gcx.short_crate_name() ); - } - MonoItem::Static(def_id) => { - c.call_with_panic_debug_info( - |ctx| ctx.declare_static(def_id, item), - format!("declare_static: {:?}", def_id), - def_id, + tcx.sess.err(&error_msg); + } else { + warn!( + "Ignoring global ASM in crate {}. Verification results may be impacted.", + gcx.short_crate_name() ); } - MonoItem::GlobalAsm(_) => { - if !self.queries.get_ignore_global_asm() { - let error_msg = format!( - "Crate {} contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**).", - c.short_crate_name() - ); - tcx.sess.err(&error_msg); - } else { - warn!( - "Ignoring global ASM in crate {}. Verification results may be impacted.", - c.short_crate_name() - ); - } - } } } } // then we move on to codegen - for cgu in codegen_units { - let items = cgu.items_in_deterministic_order(tcx); - for (item, _) in items { - match item { - MonoItem::Fn(instance) => { - c.call_with_panic_debug_info( - |ctx| ctx.codegen_function(instance), - format!( - "codegen_function: {}\n{}", - c.readable_instance_name(instance), - c.symbol_name(instance) - ), - instance.def_id(), - ); - } - MonoItem::Static(def_id) => { - c.call_with_panic_debug_info( - |ctx| ctx.codegen_static(def_id, item), - format!("codegen_static: {:?}", def_id), - def_id, - ); - } - MonoItem::GlobalAsm(_) => {} // We have already warned above + for item in items { + match item { + MonoItem::Fn(instance) => { + gcx.call_with_panic_debug_info( + |ctx| ctx.codegen_function(instance), + format!( + "codegen_function: {}\n{}", + gcx.readable_instance_name(instance), + gcx.symbol_name(instance) + ), + instance.def_id(), + ); } + MonoItem::Static(def_id) => { + gcx.call_with_panic_debug_info( + |ctx| ctx.codegen_static(def_id, item), + format!("codegen_static: {:?}", def_id), + def_id, + ); + } + MonoItem::GlobalAsm(_) => {} // We have already warned above } } // Print compilation report. - print_report(&c, tcx); + print_report(&gcx, 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); + let symtab = symtab_transformer::do_passes(gcx.symbol_table, &passes); // Map MIR types to GotoC types let type_map: BTreeMap = - BTreeMap::from_iter(c.type_map.into_iter().map(|(k, v)| (k, v.to_string().into()))); + BTreeMap::from_iter(gcx.type_map.into_iter().map(|(k, v)| (k, v.to_string().into()))); // Get the vtable function pointer restrictions if requested - let vtable_restrictions = if c.vtable_ctx.emit_vtable_restrictions { - Some(c.vtable_ctx.get_virtual_function_restrictions()) + let vtable_restrictions = if gcx.vtable_ctx.emit_vtable_restrictions { + Some(gcx.vtable_ctx.get_virtual_function_restrictions()) } else { None }; - let metadata = KaniMetadata { proof_harnesses: c.proof_harnesses }; + let metadata = KaniMetadata { proof_harnesses: gcx.proof_harnesses.clone() }; // No output should be generated if user selected no_codegen. if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { @@ -163,18 +164,7 @@ impl CodegenBackend for GotocCodegenBackend { write_file(&base_filename, "restrictions.json", &restrictions, pretty); } } - - let work_products = FxHashMap::::default(); - Box::new(( - CodegenResults { - modules: vec![], - allocator_module: None, - metadata_module: None, - metadata: rustc_metadata, - crate_info: CrateInfo::new(tcx, symtab.machine_model().architecture.clone()), - }, - work_products, - )) + codegen_results(tcx, rustc_metadata, symtab.machine_model()) } fn join_codegen( @@ -246,7 +236,7 @@ fn check_target(session: &Session) { session.abort_if_errors(); } -fn check_options(session: &Session, need_metadata_module: bool, queries: Rc) { +fn check_options(session: &Session, need_metadata_module: bool) { // The requirements for `min_global_align` and `endian` are needed to build // a valid CBMC machine model in function `machine_model_from_session` from // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -281,14 +271,6 @@ fn check_options(session: &Session, need_metadata_module: bool, queries: Rc(ctx: &GotocCtx, tcx: TyCtxt<'tcx>) { tcx.sess.warn(&msg); } } + +fn codegen_results( + tcx: TyCtxt, + rustc_metadata: EncodedMetadata, + machine: &MachineModel, +) -> Box { + let work_products = FxHashMap::::default(); + Box::new(( + CodegenResults { + modules: vec![], + allocator_module: None, + metadata_module: None, + metadata: rustc_metadata, + crate_info: CrateInfo::new(tcx, machine.architecture.clone()), + }, + work_products, + )) +} + +/// Collect all harnesses in the current crate. +fn collect_harnesses<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec> { + // Filter proof harnesses. + tcx.hir_crate_items(()) + .items() + .filter_map(|hir_id| { + let def_id = hir_id.def_id.to_def_id(); + gcx.is_proof_harness(def_id).then(|| MonoItem::Fn(Instance::mono(tcx, def_id))) + }) + .collect() +} + +/// Retrieve all items that need to be processed. +fn codegen_items<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec> { + let reach = gcx.queries.get_reachability_analysis(); + debug!(?reach, "starting_points"); + match reach { + ReachabilityType::Legacy => { + // Use rustc monomorphizer to retrieve items to codegen. + let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1; + codegen_units + .iter() + .flat_map(|cgu| cgu.items_in_deterministic_order(tcx)) + .map(|(item, _)| item) + .collect() + } + ReachabilityType::Harnesses => { + // Cross-crate collecting of all items that are reachable from the crate harnesses. + let harnesses = collect_harnesses(tcx, gcx); + collect_reachable_items(tcx, &harnesses).into_iter().collect() + } + ReachabilityType::None => Vec::new(), + ReachabilityType::PubFns => { + // TODO: https://github.com/model-checking/kani/issues/1674 + let err_msg = format!( + "Using {} reachability mode is still unsupported.", + ReachabilityType::PubFns.as_ref() + ); + tcx.sess.err(&err_msg); + Vec::new() + } + } +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/mod.rs index 46bcc8aa33ce..9c8080c03f6e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/mod.rs @@ -5,6 +5,7 @@ mod codegen; mod compiler_interface; mod context; mod overrides; +mod reachability; mod utils; pub use compiler_interface::GotocCodegenBackend; diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs new file mode 100644 index 000000000000..bb60769ea811 --- /dev/null +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -0,0 +1,586 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module implements a cross-crate collector that allow us to find all items that +//! should be included in order to verify one or more proof harness. +//! +//! This module works as following: +//! - Traverse all reachable items starting at the given starting points. +//! - For every function, traverse its body and collect the following: +//! - Constants / Static objects. +//! - Functions that are called or have their address taken. +//! - VTable methods for types that are coerced as unsized types. +//! - For every static, collect initializer and drop functions. +//! +//! We have kept this module agnostic of any Kani code in case we can contribute this back to rustc. +use rustc_data_structures::fx::FxHashSet; +use rustc_middle::mir::interpret::{AllocId, ConstValue, ErrorHandled, GlobalAlloc, Scalar}; +use rustc_middle::mir::mono::MonoItem; +use rustc_middle::mir::visit::Visitor as MirVisitor; +use rustc_middle::mir::{ + Body, CastKind, Constant, ConstantKind, Location, Rvalue, Terminator, TerminatorKind, +}; +use rustc_middle::span_bug; +use rustc_middle::ty::adjustment::PointerCast; +use rustc_middle::ty::layout::{ + HasParamEnv, HasTyCtxt, LayoutError, LayoutOf, LayoutOfHelpers, TyAndLayout, +}; +use rustc_middle::ty::{ + Closure, ClosureKind, Const, ConstKind, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, TyKind, + TypeAndMut, TypeFoldable, VtblEntry, +}; +use rustc_span::def_id::DefId; +use rustc_span::source_map::Span; +use rustc_target::abi::{HasDataLayout, TargetDataLayout, VariantIdx}; +use tracing::{debug, debug_span, trace, warn}; + +struct MonoItemsCollector<'tcx> { + /// The compiler context. + tcx: TyCtxt<'tcx>, + /// Set of collected items used to avoid entering recursion loops. + collected: FxHashSet>, + /// Keep items collected sorted by visiting order which should be more stable. + collected_sorted: Vec>, + /// Items enqueued for visiting. + queue: Vec>, +} + +impl<'tcx> MonoItemsCollector<'tcx> { + /// Collects all reachable items starting from the given root. + pub fn collect(&mut self, root: MonoItem<'tcx>) { + debug!(?root, "collect"); + self.queue.push(root); + self.reachable_items(); + } + + /// Traverses the call graph starting from the given root. For every function, we visit all + /// instruction looking for the items that should be included in the compilation. + fn reachable_items(&mut self) { + while !self.queue.is_empty() { + let to_visit = self.queue.pop().unwrap(); + if !self.collected.contains(&to_visit) { + self.collected.insert(to_visit); + self.collected_sorted.push(to_visit); + match to_visit { + MonoItem::Fn(instance) => { + self.visit_fn(instance); + } + MonoItem::Static(def_id) => { + self.visit_static(def_id); + } + MonoItem::GlobalAsm(_) => { + self.visit_asm(to_visit); + } + } + } + } + } + + /// Visit a function and collect all mono-items reachable from its instructions. + fn visit_fn(&mut self, instance: Instance<'tcx>) { + let _guard = debug_span!("visit_fn", function=?instance).entered(); + let body = self.tcx.instance_mir(instance.def); + let mut collector = + MonoItemsFnCollector { tcx: self.tcx, collected: FxHashSet::default(), instance, body }; + collector.visit_body(body); + self.queue.extend(collector.collected.iter().filter(|item| !self.collected.contains(item))); + } + + /// Visit a static object and collect drop / initialization functions. + fn visit_static(&mut self, def_id: DefId) { + let _guard = debug_span!("visit_static", ?def_id).entered(); + let instance = Instance::mono(self.tcx, def_id); + + // Collect drop function. + let static_ty = instance.ty(self.tcx, ParamEnv::reveal_all()); + let instance = Instance::resolve_drop_in_place(self.tcx, static_ty); + self.queue.push(MonoItem::Fn(instance.polymorphize(self.tcx))); + + // Collect initialization. + if let Ok(alloc) = self.tcx.eval_static_initializer(def_id) { + for &id in alloc.inner().relocations().values() { + self.queue.extend(global_alloc(self.tcx, id).iter()); + } + } + } + + /// Visit global assembly and emit either a warning or an error. + fn visit_asm(&mut self, item: MonoItem<'tcx>) { + debug!(?item, "visit_asm"); + self.collected.insert(item); + } +} + +struct MonoItemsFnCollector<'a, 'tcx> { + tcx: TyCtxt<'tcx>, + collected: FxHashSet>, + instance: Instance<'tcx>, + body: &'a Body<'tcx>, +} + +impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { + fn monomorphize(&self, value: T) -> T + where + T: TypeFoldable<'tcx>, + { + trace!(instance=?self.instance, ?value, "monomorphize"); + self.instance.subst_mir_and_normalize_erasing_regions( + self.tcx, + ParamEnv::reveal_all(), + value, + ) + } + + /// Collect the implementation of all trait methods and its supertrait methods for the given + /// concrete type. + fn collect_vtable_methods(&mut self, concrete_ty: Ty<'tcx>, trait_ty: Ty<'tcx>) { + trace!(?concrete_ty, ?trait_ty, "collect_vtable_methods"); + assert!(!concrete_ty.is_trait(), "Already a trait: {:?}", concrete_ty); + assert!(trait_ty.is_trait(), "Expected a trait: {:?}", trait_ty); + if let TyKind::Dynamic(trait_list, ..) = trait_ty.kind() { + // A trait object type can have multiple trait bounds but up to one non-auto-trait + // bound. This non-auto-trait, named principal, is the only one that can have methods. + if let Some(principal) = trait_list.principal() { + let poly_trait_ref = principal.with_self_ty(self.tcx, concrete_ty); + + // Walk all methods of the trait, including those of its supertraits + let entries = self.tcx.vtable_entries(poly_trait_ref); + let methods = entries.iter().filter_map(|entry| match entry { + VtblEntry::MetadataDropInPlace + | VtblEntry::MetadataSize + | VtblEntry::MetadataAlign + | VtblEntry::Vacant => None, + VtblEntry::TraitVPtr(_) => { + // all super trait items already covered, so skip them. + None + } + VtblEntry::Method(instance) if should_codegen_locally(self.tcx, instance) => { + Some(MonoItem::Fn(instance.polymorphize(self.tcx))) + } + VtblEntry::Method(..) => None, + }); + trace!(methods=?methods.clone().collect::>(), "collect_vtable_methods"); + self.collected.extend(methods); + } + } + + // Add the destructor for the concrete type. + let instance = Instance::resolve_drop_in_place(self.tcx, concrete_ty); + self.collect_instance(instance, false); + } + + /// Collect an instance depending on how it is used (invoked directly or via fn_ptr). + fn collect_instance(&mut self, instance: Instance<'tcx>, is_direct_call: bool) { + let should_collect = match instance.def { + InstanceDef::Virtual(..) | InstanceDef::Intrinsic(_) => { + // Instance definition has no body. + assert!(is_direct_call, "Expected direct call {:?}", instance); + false + } + InstanceDef::DropGlue(_, None) => { + // Only need the glue if we are not calling it directly. + !is_direct_call + } + InstanceDef::DropGlue(_, Some(_)) + | InstanceDef::VTableShim(..) + | InstanceDef::ReifyShim(..) + | InstanceDef::ClosureOnceShim { .. } + | InstanceDef::Item(..) + | InstanceDef::FnPtrShim(..) + | InstanceDef::CloneShim(..) => true, + }; + if should_collect && should_codegen_locally(self.tcx, &instance) { + trace!(?instance, "collect_instance"); + self.collected.insert(MonoItem::Fn(instance.polymorphize(self.tcx))); + } + } + + /// Collect constant values represented by static variables. + fn collect_const_value(&mut self, value: ConstValue<'tcx>) { + debug!(?value, "collect_const_value"); + match value { + ConstValue::Scalar(Scalar::Ptr(ptr, _size)) => { + self.collected.extend(global_alloc(self.tcx, ptr.provenance).iter()); + } + ConstValue::Slice { data: alloc, start: _, end: _ } + | ConstValue::ByRef { alloc, .. } => { + for &id in alloc.inner().relocations().values() { + self.collected.extend(global_alloc(self.tcx, id).iter()) + } + } + _ => {} + } + } +} + +/// Visit the function body looking for MonoItems that should be included in the analysis. +/// This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`. +impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { + /// Collect the following: + /// - Trait implementations when casting from concrete to dyn Trait. + /// - Functions / Closures that have their address taken. + /// - Thread Local. + fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, location: Location) { + trace!(rvalue=?*rvalue, "visit_rvalue"); + + match *rvalue { + Rvalue::Cast(CastKind::Pointer(PointerCast::Unsize), ref operand, target) => { + // Check if the conversion include casting a concrete type to a trait type. + // If so, collect items from the impl `Trait for Concrete {}`. + let target_ty = self.monomorphize(target); + let source_ty = self.monomorphize(operand.ty(self.body, self.tcx)); + if let Some((concrete_ty, trait_ty)) = + find_trait_conversion(self.tcx, source_ty, target_ty) + { + self.collect_vtable_methods(concrete_ty, trait_ty); + } + } + Rvalue::Cast(CastKind::Pointer(PointerCast::ReifyFnPointer), ref operand, _) => { + let fn_ty = operand.ty(self.body, self.tcx); + let fn_ty = self.monomorphize(fn_ty); + if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() { + let instance = Instance::resolve_for_fn_ptr( + self.tcx, + ParamEnv::reveal_all(), + def_id, + substs, + ) + .unwrap(); + self.collect_instance(instance, false); + } else { + unreachable!("Expected FnDef type, but got: {:?}", fn_ty); + } + } + Rvalue::Cast(CastKind::Pointer(PointerCast::ClosureFnPointer(_)), ref operand, _) => { + let source_ty = operand.ty(self.body, self.tcx); + let source_ty = self.monomorphize(source_ty); + match *source_ty.kind() { + Closure(def_id, substs) => { + let instance = Instance::resolve_closure( + self.tcx, + def_id, + substs, + ClosureKind::FnOnce, + ) + .expect("failed to normalize and resolve closure during codegen"); + self.collect_instance(instance, false); + } + _ => unreachable!("Unexpected type: {:?}", source_ty), + } + } + Rvalue::ThreadLocalRef(def_id) => { + assert!(self.tcx.is_thread_local_static(def_id)); + trace!(?def_id, "visit_rvalue thread_local"); + let instance = Instance::mono(self.tcx, def_id); + if should_codegen_locally(self.tcx, &instance) { + trace!("collecting thread-local static {:?}", def_id); + self.collected.insert(MonoItem::Static(def_id)); + } + } + _ => { /* not interesting */ } + } + + self.super_rvalue(rvalue, location); + } + + /// Collect constants that are represented as static variables. + fn visit_constant(&mut self, constant: &Constant<'tcx>, location: Location) { + let literal = self.monomorphize(constant.literal); + debug!(?constant, ?location, ?literal, "visit_constant"); + let val = match literal { + ConstantKind::Val(const_val, _) => const_val, + ConstantKind::Ty(ct) => match ct.kind() { + ConstKind::Value(v) => self.tcx.valtree_to_const_val((ct.ty(), v)), + ConstKind::Unevaluated(un_eval) => { + // Thread local fall into this category. + match self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None) { + // The `monomorphize` call should have evaluated that constant already. + Ok(const_val) => const_val, + Err(ErrorHandled::TooGeneric) => span_bug!( + self.body.source_info(location).span, + "Unexpected polymorphic constant: {:?}", + literal + ), + Err(error) => { + warn!(?error, "Error already reported"); + return; + } + } + } + // Nothing to do + ConstKind::Param(..) | ConstKind::Infer(..) | ConstKind::Error(..) => return, + + // Shouldn't happen + ConstKind::Placeholder(..) | ConstKind::Bound(..) => { + unreachable!("Unexpected constant type {:?} ({:?})", ct, ct.kind()) + } + }, + }; + self.collect_const_value(val); + } + + fn visit_const(&mut self, constant: Const<'tcx>, location: Location) { + trace!(?constant, ?location, "visit_const"); + self.super_const(constant); + } + + /// Collect function calls. + fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) { + trace!(?terminator, ?location, "visit_terminator"); + + let tcx = self.tcx; + match terminator.kind { + TerminatorKind::Call { ref func, .. } => { + let callee_ty = func.ty(self.body, tcx); + let fn_ty = self.monomorphize(callee_ty); + if let TyKind::FnDef(def_id, substs) = *fn_ty.kind() { + let instance = + Instance::resolve(self.tcx, ParamEnv::reveal_all(), def_id, substs) + .unwrap() + .unwrap(); + self.collect_instance(instance, true); + } else { + assert!( + matches!(fn_ty.kind(), TyKind::FnPtr(..)), + "Unexpected type: {:?}", + fn_ty + ); + } + } + TerminatorKind::Drop { ref place, .. } + | TerminatorKind::DropAndReplace { ref place, .. } => { + let place_ty = place.ty(self.body, self.tcx).ty; + let place_mono_ty = self.monomorphize(place_ty); + let instance = Instance::resolve_drop_in_place(self.tcx, place_mono_ty); + self.collect_instance(instance, true); + } + TerminatorKind::InlineAsm { .. } => { + // We don't support inline assembly. Skip for now. + } + TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { + // We generate code for this without invoking any lang item. + } + TerminatorKind::Goto { .. } + | TerminatorKind::SwitchInt { .. } + | TerminatorKind::Resume + | TerminatorKind::Return + | TerminatorKind::Unreachable => {} + TerminatorKind::GeneratorDrop + | TerminatorKind::Yield { .. } + | TerminatorKind::FalseEdge { .. } + | TerminatorKind::FalseUnwind { .. } => { + unreachable!("Unexpected at this MIR level") + } + } + + self.super_terminator(terminator, location); + } +} + +/// Visit every instruction in a function and collect the following: +/// 1. Every function / method / closures that may be directly invoked. +/// 2. Every function / method / closures that may have their address taken. +/// 3. Every method that compose the impl of a trait for a given type when there's a conversion +/// from the type to the trait. +/// - I.e.: If we visit the following code: +/// ``` +/// let var = MyType::new(); +/// let ptr : &dyn MyTrait = &var; +/// ``` +/// We collect the entire implementation of `MyTrait` for `MyType`. +/// 4. Every Static variable that is referenced in the function. +/// 5. Drop glue? Static Initialization? +/// +impl<'tcx> MirVisitor<'tcx> for MonoItemsCollector<'tcx> {} + +/// This is the reachability starting point. We start from every static item and proof harnesses. +pub fn collect_reachable_items<'tcx>( + tcx: TyCtxt<'tcx>, + starting_points: &[MonoItem<'tcx>], +) -> FxHashSet> { + // For each harness, collect items using the same collector. + let mut collector = MonoItemsCollector { + tcx, + collected: FxHashSet::default(), + queue: vec![], + collected_sorted: vec![], + }; + for item in starting_points { + collector.collect(*item); + } + collector.collected +} + +/// Return whether we should include the item into codegen. +/// We don't include foreign items only. +fn should_codegen_locally<'tcx>(tcx: TyCtxt<'tcx>, instance: &Instance<'tcx>) -> bool { + if let Some(def_id) = instance.def.def_id_if_not_guaranteed_local_codegen() { + if tcx.is_foreign_item(def_id) { + // We cannot codegen foreign items. + false + } else { + // TODO: This should either be an assert or a warning. + // Need to compile std with --always-encode-mir first though. + // https://github.com/model-checking/kani/issues/1605 + // assert!(tcx.is_mir_available(def_id), "no MIR available for {:?}", def_id); + //(!tcx.is_mir_available(def_id)).then(|| warn!(?def_id, "Missing MIR")); + tcx.is_mir_available(def_id) + } + } else { + // This will include things like VTableShim and other stuff. See the method + // def_id_if_not_guaranteed_local_codegen for the full list. + true + } +} + +/// Extract the pair (concrete, trait) for a unsized cast. +/// This function will return None if this is not a unsizing coercion from concrete to trait. +/// +/// For example, if `&u8` is being converted to `&dyn Debug`, this method would return: +/// `Some(u8, dyn Debug)`. +/// +/// This method also handles nested cases and `std` smart pointers. E.g.: +/// +/// Conversion between `Rc>` into `Rc>` should return: +/// `Some(T, dyn Debug)` +/// +/// The first step of this method is to extract the pointee types. Then we need to traverse the +/// pointee types to find the actual trait and the type implementing it. +/// +/// TODO: Do we need to handle &Wrapper to &dyn T2 or is that taken care of with super +/// trait handling? What about CoerceUnsized trait? +fn find_trait_conversion<'tcx>( + tcx: TyCtxt<'tcx>, + src_ty: Ty<'tcx>, + dst_ty: Ty<'tcx>, +) -> Option<(Ty<'tcx>, Ty<'tcx>)> { + let vtable_metadata = |mir_type: Ty<'tcx>| { + let (metadata, _) = mir_type.ptr_metadata_ty(tcx, |ty| ty); + metadata != tcx.types.unit && metadata != tcx.types.usize + }; + + trace!(?dst_ty, ?src_ty, "find_trait_conversion"); + let dst_ty_inner = find_pointer(tcx, dst_ty); + let src_ty_inner = find_pointer(tcx, src_ty); + + trace!(?dst_ty_inner, ?src_ty_inner, "find_trait_conversion"); + (vtable_metadata(dst_ty_inner) && !vtable_metadata(src_ty_inner)).then(|| { + let param_env = ParamEnv::reveal_all(); + tcx.struct_lockstep_tails_erasing_lifetimes(src_ty_inner, dst_ty_inner, param_env) + }) +} + +/// This function extracts the pointee type of a regular pointer and std smart pointers. +/// +/// TODO: Refactor this to use `CustomCoerceUnsized` logic which includes custom smart pointers. +/// +/// E.g.: For `Rc` where the Rc definition is: +/// ``` +/// pub struct Rc { +/// ptr: NonNull>, +/// phantom: PhantomData>, +/// } +/// +/// pub struct NonNull { +/// pointer: *const T, +/// } +/// ``` +/// +/// This function will return `pointer: *const T`. +fn find_pointer<'tcx>(tcx: TyCtxt<'tcx>, typ: Ty<'tcx>) -> Ty<'tcx> { + struct ReceiverIter<'tcx> { + pub curr: Ty<'tcx>, + pub tcx: TyCtxt<'tcx>, + } + + impl<'tcx> LayoutOfHelpers<'tcx> for ReceiverIter<'tcx> { + type LayoutOfResult = TyAndLayout<'tcx>; + + #[inline] + fn handle_layout_err(&self, err: LayoutError, span: Span, ty: Ty<'tcx>) -> ! { + span_bug!(span, "failed to get layout for `{}`: {}", ty, err) + } + } + + impl<'tcx> HasParamEnv<'tcx> for ReceiverIter<'tcx> { + fn param_env(&self) -> ParamEnv<'tcx> { + ParamEnv::reveal_all() + } + } + + impl<'tcx> HasTyCtxt<'tcx> for ReceiverIter<'tcx> { + fn tcx(&self) -> TyCtxt<'tcx> { + self.tcx + } + } + + impl<'tcx> HasDataLayout for ReceiverIter<'tcx> { + fn data_layout(&self) -> &TargetDataLayout { + self.tcx.data_layout() + } + } + + impl<'tcx> Iterator for ReceiverIter<'tcx> { + type Item = (String, Ty<'tcx>); + + fn next(&mut self) -> Option { + if let TyKind::Adt(adt_def, adt_substs) = self.curr.kind() { + assert_eq!( + adt_def.variants().len(), + 1, + "Expected a single-variant ADT. Found {:?}", + self.curr + ); + let tcx = self.tcx; + let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; + let mut non_zsts = fields + .iter() + .filter(|field| !self.layout_of(field.ty(tcx, adt_substs)).is_zst()) + .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(tcx, adt_substs))); + let (name, next) = non_zsts.next().expect("Expected one non-zst field."); + assert!(non_zsts.next().is_none(), "Expected only one non-zst field."); + self.curr = next; + Some((name, self.curr)) + } else { + None + } + } + } + if let Some(TypeAndMut { ty, .. }) = typ.builtin_deref(true) { + ty + } else { + ReceiverIter { tcx, curr: typ }.last().unwrap().1 + } +} + +/// Scans the allocation type and collect static objects. +fn global_alloc<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec { + let mut items = vec![]; + match tcx.global_alloc(alloc_id) { + GlobalAlloc::Static(def_id) => { + assert!(!tcx.is_thread_local_static(def_id)); + let instance = Instance::mono(tcx, def_id); + should_codegen_locally(tcx, &instance).then(|| { + trace!(?def_id, "global_alloc"); + items.push(MonoItem::Static(def_id)) + }); + } + GlobalAlloc::Function(instance) => { + should_codegen_locally(tcx, &instance).then(|| { + trace!(?alloc_id, ?instance, "global_alloc"); + items.push(MonoItem::Fn(instance.polymorphize(tcx))) + }); + } + GlobalAlloc::Memory(alloc) => { + trace!(?alloc_id, "global_alloc memory"); + items + .extend(alloc.inner().relocations().values().flat_map(|id| global_alloc(tcx, *id))); + } + GlobalAlloc::VTable(ty, trait_ref) => { + trace!(?alloc_id, "global_alloc vtable"); + let vtable_id = tcx.vtable_allocation((ty, trait_ref)); + items.append(&mut global_alloc(tcx, vtable_id)); + } + }; + items +} diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index ce16179d0c17..3e0cf14ef3e6 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -62,6 +62,8 @@ fn rustc_gotoc_flags(lib_path: &str) -> Vec { "trim-diagnostic-paths=no", "-Z", "human_readable_cgu_names", + "-Z", + "always-encode-mir", "--cfg=kani", "-Z", "crate-attr=feature(register_tool)", @@ -128,11 +130,11 @@ impl Callbacks for KaniCallbacks {} /// Generate the arguments to pass to rustc_driver. fn generate_rustc_args(args: &ArgMatches) -> Vec { - let mut gotoc_args = + let gotoc_args = rustc_gotoc_flags(args.value_of(parser::KANI_LIB).unwrap_or(std::env!("KANI_LIB_PATH"))); let mut rustc_args = vec![String::from("rustc")]; if args.is_present(parser::GOTO_C) { - rustc_args.append(&mut gotoc_args); + rustc_args.extend_from_slice(&gotoc_args); } if args.is_present(parser::RUSTC_VERSION) { diff --git a/tests/cargo-ui/mir-linker/Cargo.toml b/tests/cargo-kani/mir-linker/Cargo.toml similarity index 74% rename from tests/cargo-ui/mir-linker/Cargo.toml rename to tests/cargo-kani/mir-linker/Cargo.toml index deab2d6dd69e..39d5016a407b 100644 --- a/tests/cargo-ui/mir-linker/Cargo.toml +++ b/tests/cargo-kani/mir-linker/Cargo.toml @@ -4,9 +4,10 @@ name = "mir-linker" version = "0.1.0" edition = "2021" +description = "Ensures that the mir-linker works accross crates" [dependencies] -rand = "0.8.4" +semver = "1.0" [package.metadata.kani] flags = { mir-linker=true, enable-unstable=true } diff --git a/tests/cargo-kani/mir-linker/expected b/tests/cargo-kani/mir-linker/expected new file mode 100644 index 000000000000..2a5a5ac367ba --- /dev/null +++ b/tests/cargo-kani/mir-linker/expected @@ -0,0 +1,3 @@ +Status: SUCCESS\ +Next is greater\ +in function check_version diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs new file mode 100644 index 000000000000..e4d8aadfed31 --- /dev/null +++ b/tests/cargo-kani/mir-linker/src/lib.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Dummy test to check --mir-linker runs on a cargo project. +use semver::{BuildMetadata, Prerelease, Version}; + +#[kani::proof] +fn check_version() { + let next_major: u64 = kani::any(); + let next_minor: u64 = kani::any(); + kani::assume(next_major.wrapping_add(next_minor) > 0); + + // Check whether this requirement matches version 1.2.3-alpha.1 (no) + let v0 = Version { + major: 0, + minor: 0, + patch: 0, + pre: Prerelease::EMPTY, + build: BuildMetadata::EMPTY, + }; + let next = Version { + major: next_major, + minor: next_minor, + patch: 0, + pre: Prerelease::EMPTY, + build: BuildMetadata::EMPTY, + }; + assert!(next > v0, "Next is greater"); +} diff --git a/tests/cargo-ui/mir-linker/expected b/tests/cargo-ui/mir-linker/expected deleted file mode 100644 index 3267e7dc1181..000000000000 --- a/tests/cargo-ui/mir-linker/expected +++ /dev/null @@ -1 +0,0 @@ -error: Using none reachability mode is still unsupported. diff --git a/tests/cargo-ui/mir-linker/src/lib.rs b/tests/cargo-ui/mir-linker/src/lib.rs deleted file mode 100644 index 98302f2bb76a..000000000000 --- a/tests/cargo-ui/mir-linker/src/lib.rs +++ /dev/null @@ -1,13 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Dummy test to check --mir-linker runs on a cargo project. -pub fn add(left: usize, right: usize) -> usize { - left + right -} - -#[kani::proof] -fn check_add() { - let result = add(2, 2); - assert_eq!(result, 4); -} diff --git a/tests/ui/mir-linker/expected b/tests/ui/mir-linker/expected index 2bc00d12220d..ac9ef183fb2c 100644 --- a/tests/ui/mir-linker/expected +++ b/tests/ui/mir-linker/expected @@ -1 +1,2 @@ -error: Using harnesses reachability mode is still unsupported. +Failed Checks: Function `alloc::string::String::from_utf8_lossy` with missing definition is unreachable + diff --git a/tests/ui/mir-linker/generic-harness/expected b/tests/ui/mir-linker/generic-harness/expected new file mode 100644 index 000000000000..5621a9a68433 --- /dev/null +++ b/tests/ui/mir-linker/generic-harness/expected @@ -0,0 +1 @@ +error: The proof attribute cannot be applied to generic functions. diff --git a/tests/ui/mir-linker/generic-harness/incorrect.rs b/tests/ui/mir-linker/generic-harness/incorrect.rs new file mode 100644 index 000000000000..e68eba6ec834 --- /dev/null +++ b/tests/ui/mir-linker/generic-harness/incorrect.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: --enable-unstable --mir-linker +// +//! Checks that we correctly fail if the harness is a generic function. + +#[kani::proof] +fn harness() { + let _ = T::default(); +} + +#[kani::proof] +fn other_harness() { + harness::(); +} diff --git a/tests/ui/unwind-without-proof/main.rs b/tests/ui/unwind-without-proof/main.rs index c97ec201c07b..1029d9235703 100644 --- a/tests/ui/unwind-without-proof/main.rs +++ b/tests/ui/unwind-without-proof/main.rs @@ -9,6 +9,7 @@ #[kani::proof] fn main() { assert!(1 == 2); + harness(); } #[kani::unwind(7)] diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index 67771fa9da58..f039d8925e21 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -137,6 +137,11 @@ pub struct Config { /// Whether to rerun tests even if the inputs are unchanged. pub force_rerun: bool, + + /// Allow us to run the regression with the mir linker enabled by default. For that, set + /// `RUSTFLAGS=--cfg=mir_linker` while compiling `compiletest`. + /// Remove this as part of https://github.com/model-checking/kani/issues/1677 + pub mir_linker: bool, } #[derive(Debug, Clone)] diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index a87440021250..741f3d97fc05 100644 --- a/tools/compiletest/src/main.rs +++ b/tools/compiletest/src/main.rs @@ -221,6 +221,7 @@ pub fn parse_config(args: Vec) -> Config { edition: matches.opt_str("edition"), force_rerun: matches.opt_present("force-rerun"), + mir_linker: cfg!(mir_linker), } } @@ -239,6 +240,7 @@ pub fn log_config(config: &Config) { logv(c, format!("host: {}", config.host)); logv(c, format!("verbose: {}", config.verbose)); logv(c, format!("quiet: {}", config.quiet)); + logv(c, format!("mir_linker: {}", config.mir_linker)); logv(c, "\n".to_string()); } diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 85eb1fb973d9..d3eb069dc8df 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -296,6 +296,12 @@ impl<'test> TestCx<'test> { if "expected" != self.testpaths.file.file_name().unwrap() { cargo.args(["--harness", function_name]); } + + if self.config.mir_linker { + // Allow us to run the regression with the mir linker enabled by default. + cargo.arg("--enable-unstable").arg("--mir-linker"); + } + let proc_res = self.compose_and_run(cargo); let expected = fs::read_to_string(self.testpaths.file.clone()).unwrap(); self.verify_output(&proc_res, &expected); @@ -315,6 +321,12 @@ impl<'test> TestCx<'test> { if !self.props.compile_flags.is_empty() { kani.env("RUSTFLAGS", self.props.compile_flags.join(" ")); } + + if self.config.mir_linker { + // Allow us to run the regression with the mir linker enabled by default. + kani.arg("--enable-unstable").arg("--mir-linker"); + } + // Pass the test path along with Kani and CBMC flags parsed from comments at the top of the test file. kani.arg(&self.testpaths.file).args(&self.props.kani_flags); From 2759e3ba9c239442ac812e7ebbde9ce45a5906df Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 15 Sep 2022 12:33:38 -0700 Subject: [PATCH 2/9] Address PR comments --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 5 +++-- kani-compiler/src/codegen_cprover_gotoc/reachability.rs | 3 ++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index e3c28e942267..af1c623b1685 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -66,7 +66,7 @@ impl CodegenBackend for GotocCodegenBackend { // 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.clone()); - let items = codegen_items(tcx, &gcx); + let items = collect_codegen_items(tcx, &gcx); if items.is_empty() { // There's nothing to do. return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); @@ -310,6 +310,7 @@ fn print_report<'tcx>(ctx: &GotocCtx, tcx: TyCtxt<'tcx>) { } } +/// Return a struct that contains information about the codegen results as expected by `rustc`. fn codegen_results( tcx: TyCtxt, rustc_metadata: EncodedMetadata, @@ -341,7 +342,7 @@ fn collect_harnesses<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec> { +fn collect_codegen_items<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec> { let reach = gcx.queries.get_reachability_analysis(); debug!(?reach, "starting_points"); match reach { diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs index bb60769ea811..bb00eabca2fc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -355,7 +355,8 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { self.collect_instance(instance, true); } TerminatorKind::InlineAsm { .. } => { - // We don't support inline assembly. Skip for now. + // We don't support inline assembly. This shall be replaced by an unsupported + // construct during codegen. } TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { // We generate code for this without invoking any lang item. From a409aa0b1ca2e7aa55806574805dad0960492827 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 16 Sep 2022 12:07:29 -0700 Subject: [PATCH 3/9] Sort items by string for now to keep stable order --- .../src/codegen_cprover_gotoc/reachability.rs | 20 +++++++++---------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs index bb00eabca2fc..65a7b72f699b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -39,8 +39,6 @@ struct MonoItemsCollector<'tcx> { tcx: TyCtxt<'tcx>, /// Set of collected items used to avoid entering recursion loops. collected: FxHashSet>, - /// Keep items collected sorted by visiting order which should be more stable. - collected_sorted: Vec>, /// Items enqueued for visiting. queue: Vec>, } @@ -60,7 +58,6 @@ impl<'tcx> MonoItemsCollector<'tcx> { let to_visit = self.queue.pop().unwrap(); if !self.collected.contains(&to_visit) { self.collected.insert(to_visit); - self.collected_sorted.push(to_visit); match to_visit { MonoItem::Fn(instance) => { self.visit_fn(instance); @@ -398,18 +395,19 @@ impl<'tcx> MirVisitor<'tcx> for MonoItemsCollector<'tcx> {} pub fn collect_reachable_items<'tcx>( tcx: TyCtxt<'tcx>, starting_points: &[MonoItem<'tcx>], -) -> FxHashSet> { +) -> Vec> { // For each harness, collect items using the same collector. - let mut collector = MonoItemsCollector { - tcx, - collected: FxHashSet::default(), - queue: vec![], - collected_sorted: vec![], - }; + let mut collector = MonoItemsCollector { tcx, collected: FxHashSet::default(), queue: vec![] }; for item in starting_points { collector.collect(*item); } - collector.collected + + // Sort the result so code generation follows deterministic order. + // This helps us to debug the code, but it also provides the user a good experience since the + // order of the errors and warnings is stable. + let mut sorted_items: Vec<_> = collector.collected.into_iter().collect(); + sorted_items.sort_by_cached_key(|item| item.to_string()); + sorted_items } /// Return whether we should include the item into codegen. From 25e0943c1917910e927c8dfbb1d4f9341b8eae27 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 16 Sep 2022 16:12:47 -0700 Subject: [PATCH 4/9] Address most comments to compiler_interface file --- .../codegen_cprover_gotoc/codegen/function.rs | 40 ++++++--- .../compiler_interface.rs | 83 ++++++++++--------- .../src/codegen_cprover_gotoc/reachability.rs | 16 ++++ 3 files changed, 89 insertions(+), 50 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 023a9fb02847..e42f4f42a6c9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -285,14 +285,26 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// This updates the goto context with any information that should be accumulated from a function's - /// attributes. - /// - /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here) - fn handle_kanitool_attributes(&mut self) { - let all_attributes = self.tcx.get_attrs_unchecked(self.current_fn().instance().def_id()); + // Check that all attributes assigned to an item is valid. + pub fn check_attributes(&self, def_id: DefId) { + let all_attributes = self.tcx.get_attrs_unchecked(def_id); let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes); - if proof_attributes.is_empty() && !other_attributes.is_empty() { + if !proof_attributes.is_empty() { + let span = proof_attributes.first().unwrap().span; + if self.tcx.def_kind(def_id) != DefKind::Fn { + self.tcx + .sess + .span_err(span, "The kani::proof attribute can only be applied to functions."); + } else if self.tcx.generics_of(def_id).requires_monomorphization(self.tcx) { + self.tcx + .sess + .span_err(span, "The proof attribute cannot be applied to generic functions."); + } else if proof_attributes.len() > 1 { + self.tcx + .sess + .span_warn(proof_attributes[0].span, "Only one '#[kani::proof]' allowed"); + } + } else if !other_attributes.is_empty() { self.tcx.sess.span_err( other_attributes[0].1.span, format!( @@ -301,12 +313,16 @@ impl<'tcx> GotocCtx<'tcx> { ) .as_str(), ); - return; - } - if proof_attributes.len() > 1 { - // No return because this only requires a warning - self.tcx.sess.span_warn(proof_attributes[0].span, "Only one '#[kani::proof]' allowed"); } + } + + /// This updates the goto context with any information that should be accumulated from a function's + /// attributes. + /// + /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here) + fn handle_kanitool_attributes(&mut self) { + let all_attributes = self.tcx.get_attrs_unchecked(self.current_fn().instance().def_id()); + let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes); if !proof_attributes.is_empty() { self.create_proof_harness(other_attributes); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index af1c623b1685..2a18d4681e7c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -3,7 +3,7 @@ //! This file contains the code necessary to interface with the compiler backend -use crate::codegen_cprover_gotoc::reachability::collect_reachable_items; +use crate::codegen_cprover_gotoc::reachability::{collect_reachable_items, filter_crate_items}; use crate::codegen_cprover_gotoc::GotocCtx; use bitflags::_core::any::Any; use cbmc::goto_program::{symtab_transformer, Location}; @@ -14,11 +14,12 @@ use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; use rustc_data_structures::fx::FxHashMap; use rustc_errors::ErrorGuaranteed; +use rustc_hir::def::DefKind; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::mir::mono::{CodegenUnit, MonoItem}; use rustc_middle::ty::query::Providers; -use rustc_middle::ty::{self, Instance, TyCtxt}; +use rustc_middle::ty::{self, TyCtxt}; use rustc_session::config::{OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::Session; @@ -52,21 +53,22 @@ impl CodegenBackend for GotocCodegenBackend { fn provide_extern(&self, _providers: &mut ty::query::ExternProviders) {} - fn codegen_crate<'tcx>( + fn codegen_crate( &self, - tcx: TyCtxt<'tcx>, + tcx: TyCtxt, rustc_metadata: EncodedMetadata, need_metadata_module: bool, ) -> Box { super::utils::init(); - check_target(tcx.sess); - check_options(tcx.sess, need_metadata_module); - // 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.clone()); - let items = collect_codegen_items(tcx, &gcx); + check_target(tcx.sess); + check_options(tcx.sess, need_metadata_module); + check_crate_items(&gcx); + + let items = collect_codegen_items(&gcx); if items.is_empty() { // There's nothing to do. return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); @@ -89,20 +91,7 @@ impl CodegenBackend for GotocCodegenBackend { def_id, ); } - MonoItem::GlobalAsm(_) => { - if !self.queries.get_ignore_global_asm() { - let error_msg = format!( - "Crate {} contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**).", - gcx.short_crate_name() - ); - tcx.sess.err(&error_msg); - } else { - warn!( - "Ignoring global ASM in crate {}. Verification results may be impacted.", - gcx.short_crate_name() - ); - } - } + MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it. } } @@ -149,7 +138,7 @@ impl CodegenBackend for GotocCodegenBackend { None }; - let metadata = KaniMetadata { proof_harnesses: gcx.proof_harnesses.clone() }; + let metadata = KaniMetadata { proof_harnesses: gcx.proof_harnesses }; // No output should be generated if user selected no_codegen. if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { @@ -274,6 +263,34 @@ fn check_options(session: &Session, need_metadata_module: bool) { session.abort_if_errors(); } +/// 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 +/// error was found. +fn check_crate_items(gcx: &GotocCtx) { + let tcx = gcx.tcx; + for item in tcx.hir_crate_items(()).items() { + let def_id = item.def_id.to_def_id(); + gcx.check_attributes(def_id); + if tcx.def_kind(def_id) == DefKind::GlobalAsm { + if !gcx.queries.get_ignore_global_asm() { + let error_msg = format!( + "Crate {} contains global ASM, which is not supported by Kani. Rerun with \ + `--enable-unstable --ignore-global-asm` to suppress this error \ + (**Verification results may be impacted**).", + gcx.short_crate_name() + ); + tcx.sess.err(&error_msg); + } else { + warn!( + "Ignoring global ASM in crate {}. Verification results may be impacted.", + gcx.short_crate_name() + ); + } + } + } + tcx.sess.abort_if_errors(); +} + fn write_file(base_filename: &Path, extension: &str, source: &T, pretty: bool) where T: serde::Serialize, @@ -329,20 +346,9 @@ fn codegen_results( )) } -/// Collect all harnesses in the current crate. -fn collect_harnesses<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec> { - // Filter proof harnesses. - tcx.hir_crate_items(()) - .items() - .filter_map(|hir_id| { - let def_id = hir_id.def_id.to_def_id(); - gcx.is_proof_harness(def_id).then(|| MonoItem::Fn(Instance::mono(tcx, def_id))) - }) - .collect() -} - /// Retrieve all items that need to be processed. -fn collect_codegen_items<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec> { +fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec> { + let tcx = gcx.tcx; let reach = gcx.queries.get_reachability_analysis(); debug!(?reach, "starting_points"); match reach { @@ -357,7 +363,7 @@ fn collect_codegen_items<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec { // Cross-crate collecting of all items that are reachable from the crate harnesses. - let harnesses = collect_harnesses(tcx, gcx); + let harnesses = filter_crate_items(tcx, |_, def_id| gcx.is_proof_harness(def_id)); collect_reachable_items(tcx, &harnesses).into_iter().collect() } ReachabilityType::None => Vec::new(), @@ -368,7 +374,8 @@ fn collect_codegen_items<'tcx>(tcx: TyCtxt<'tcx>, gcx: &GotocCtx) -> Vec MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { /// impl<'tcx> MirVisitor<'tcx> for MonoItemsCollector<'tcx> {} +/// Collect all items in the crate that matches the given predicate. +pub fn filter_crate_items(tcx: TyCtxt, predicate: F) -> Vec +where + F: FnMut(TyCtxt, DefId) -> bool, +{ + // Filter proof harnesses. + let mut filter = predicate; + tcx.hir_crate_items(()) + .items() + .filter_map(|hir_id| { + let def_id = hir_id.def_id.to_def_id(); + filter(tcx, def_id).then(|| MonoItem::Fn(Instance::mono(tcx, def_id))) + }) + .collect() +} + /// This is the reachability starting point. We start from every static item and proof harnesses. pub fn collect_reachable_items<'tcx>( tcx: TyCtxt<'tcx>, From c10c20d98de3fa390a465fedeb4c839f28804166 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 16 Sep 2022 16:45:23 -0700 Subject: [PATCH 5/9] Better hash function to sort mono items --- .../src/codegen_cprover_gotoc/reachability.rs | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs index 2722646db854..dcfd7abdfc25 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -13,7 +13,9 @@ //! - For every static, collect initializer and drop functions. //! //! We have kept this module agnostic of any Kani code in case we can contribute this back to rustc. +use rustc_data_structures::fingerprint::Fingerprint; use rustc_data_structures::fx::FxHashSet; +use rustc_data_structures::stable_hasher::{HashStable, StableHasher}; use rustc_middle::mir::interpret::{AllocId, ConstValue, ErrorHandled, GlobalAlloc, Scalar}; use rustc_middle::mir::mono::MonoItem; use rustc_middle::mir::visit::Visitor as MirVisitor; @@ -407,6 +409,16 @@ where .collect() } +/// Convert a `MonoItem` into a stable `Fingerprint` which can be used as a stable hash across +/// compilation sessions. This allow us to provide a stable deterministic order to codegen. +fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint { + tcx.with_stable_hashing_context(|mut hcx| { + let mut hasher = StableHasher::new(); + item.hash_stable(&mut hcx, &mut hasher); + hasher.finish() + }) +} + /// This is the reachability starting point. We start from every static item and proof harnesses. pub fn collect_reachable_items<'tcx>( tcx: TyCtxt<'tcx>, @@ -422,7 +434,8 @@ pub fn collect_reachable_items<'tcx>( // This helps us to debug the code, but it also provides the user a good experience since the // order of the errors and warnings is stable. let mut sorted_items: Vec<_> = collector.collected.into_iter().collect(); - sorted_items.sort_by_cached_key(|item| item.to_string()); + sorted_items.sort_by_cached_key(|item| to_fingerprint(tcx, item)); + sorted_items.iter().for_each(|item| println!("{:?}", item)); sorted_items } From 8fd9e3d9dc08c1f3a1282c9aa5e306c5a466daeb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sat, 17 Sep 2022 20:40:52 -0700 Subject: [PATCH 6/9] Address PR comments related to reachability mod --- .../src/codegen_cprover_gotoc/reachability.rs | 216 +++++++++--------- tests/cargo-kani/mir-linker/src/lib.rs | 2 +- 2 files changed, 110 insertions(+), 108 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs index dcfd7abdfc25..0f895c1181cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -56,8 +56,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// Traverses the call graph starting from the given root. For every function, we visit all /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { - while !self.queue.is_empty() { - let to_visit = self.queue.pop().unwrap(); + while let Some(to_visit) = self.queue.pop() { if !self.collected.contains(&to_visit) { self.collected.insert(to_visit); match to_visit { @@ -96,14 +95,13 @@ impl<'tcx> MonoItemsCollector<'tcx> { self.queue.push(MonoItem::Fn(instance.polymorphize(self.tcx))); // Collect initialization. - if let Ok(alloc) = self.tcx.eval_static_initializer(def_id) { - for &id in alloc.inner().relocations().values() { - self.queue.extend(global_alloc(self.tcx, id).iter()); - } + let alloc = self.tcx.eval_static_initializer(def_id).unwrap(); + for &id in alloc.inner().relocations().values() { + self.queue.extend(collect_alloc_items(self.tcx, id).iter()); } } - /// Visit global assembly and emit either a warning or an error. + /// Visit global assembly and collect its item. fn visit_asm(&mut self, item: MonoItem<'tcx>) { debug!(?item, "visit_asm"); self.collected.insert(item); @@ -134,20 +132,21 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { /// concrete type. fn collect_vtable_methods(&mut self, concrete_ty: Ty<'tcx>, trait_ty: Ty<'tcx>) { trace!(?concrete_ty, ?trait_ty, "collect_vtable_methods"); - assert!(!concrete_ty.is_trait(), "Already a trait: {:?}", concrete_ty); + assert!(!concrete_ty.is_trait(), "Expected a concrete type, but found: {:?}", concrete_ty); assert!(trait_ty.is_trait(), "Expected a trait: {:?}", trait_ty); if let TyKind::Dynamic(trait_list, ..) = trait_ty.kind() { // A trait object type can have multiple trait bounds but up to one non-auto-trait // bound. This non-auto-trait, named principal, is the only one that can have methods. + // https://doc.rust-lang.org/reference/special-types-and-traits.html#auto-traits if let Some(principal) = trait_list.principal() { let poly_trait_ref = principal.with_self_ty(self.tcx, concrete_ty); // Walk all methods of the trait, including those of its supertraits let entries = self.tcx.vtable_entries(poly_trait_ref); let methods = entries.iter().filter_map(|entry| match entry { - VtblEntry::MetadataDropInPlace + VtblEntry::MetadataAlign + | VtblEntry::MetadataDropInPlace | VtblEntry::MetadataSize - | VtblEntry::MetadataAlign | VtblEntry::Vacant => None, VtblEntry::TraitVPtr(_) => { // all super trait items already covered, so skip them. @@ -180,13 +179,13 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { // Only need the glue if we are not calling it directly. !is_direct_call } - InstanceDef::DropGlue(_, Some(_)) - | InstanceDef::VTableShim(..) - | InstanceDef::ReifyShim(..) + InstanceDef::CloneShim(..) | InstanceDef::ClosureOnceShim { .. } - | InstanceDef::Item(..) + | InstanceDef::DropGlue(_, Some(_)) | InstanceDef::FnPtrShim(..) - | InstanceDef::CloneShim(..) => true, + | InstanceDef::Item(..) + | InstanceDef::ReifyShim(..) + | InstanceDef::VTableShim(..) => true, }; if should_collect && should_codegen_locally(self.tcx, &instance) { trace!(?instance, "collect_instance"); @@ -199,12 +198,12 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { debug!(?value, "collect_const_value"); match value { ConstValue::Scalar(Scalar::Ptr(ptr, _size)) => { - self.collected.extend(global_alloc(self.tcx, ptr.provenance).iter()); + self.collected.extend(collect_alloc_items(self.tcx, ptr.provenance).iter()); } ConstValue::Slice { data: alloc, start: _, end: _ } | ConstValue::ByRef { alloc, .. } => { for &id in alloc.inner().relocations().values() { - self.collected.extend(global_alloc(self.tcx, id).iter()) + self.collected.extend(collect_alloc_items(self.tcx, id).iter()) } } _ => {} @@ -212,7 +211,20 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { } } -/// Visit the function body looking for MonoItems that should be included in the analysis. +/// Visit every instruction in a function and collect the following: +/// 1. Every function / method / closures that may be directly invoked. +/// 2. Every function / method / closures that may have their address taken. +/// 3. Every method that compose the impl of a trait for a given type when there's a conversion +/// from the type to the trait. +/// - I.e.: If we visit the following code: +/// ``` +/// let var = MyType::new(); +/// let ptr : &dyn MyTrait = &var; +/// ``` +/// We collect the entire implementation of `MyTrait` for `MyType`. +/// 4. Every Static variable that is referenced in the function or constant used in the function. +/// 5. Drop glue. +/// 6. Static Initialization /// This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`. impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { /// Collect the following: @@ -229,7 +241,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { let target_ty = self.monomorphize(target); let source_ty = self.monomorphize(operand.ty(self.body, self.tcx)); if let Some((concrete_ty, trait_ty)) = - find_trait_conversion(self.tcx, source_ty, target_ty) + extract_trait_casting(self.tcx, source_ty, target_ty) { self.collect_vtable_methods(concrete_ty, trait_ty); } @@ -377,22 +389,6 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { } } -/// Visit every instruction in a function and collect the following: -/// 1. Every function / method / closures that may be directly invoked. -/// 2. Every function / method / closures that may have their address taken. -/// 3. Every method that compose the impl of a trait for a given type when there's a conversion -/// from the type to the trait. -/// - I.e.: If we visit the following code: -/// ``` -/// let var = MyType::new(); -/// let ptr : &dyn MyTrait = &var; -/// ``` -/// We collect the entire implementation of `MyTrait` for `MyType`. -/// 4. Every Static variable that is referenced in the function. -/// 5. Drop glue? Static Initialization? -/// -impl<'tcx> MirVisitor<'tcx> for MonoItemsCollector<'tcx> {} - /// Collect all items in the crate that matches the given predicate. pub fn filter_crate_items(tcx: TyCtxt, predicate: F) -> Vec where @@ -419,12 +415,13 @@ fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint { }) } -/// This is the reachability starting point. We start from every static item and proof harnesses. +/// Collect all reachable items starting from the given starting points. pub fn collect_reachable_items<'tcx>( tcx: TyCtxt<'tcx>, starting_points: &[MonoItem<'tcx>], ) -> Vec> { // For each harness, collect items using the same collector. + // I.e.: This will return any item that is reachable from one or more of the starting points. let mut collector = MonoItemsCollector { tcx, collected: FxHashSet::default(), queue: vec![] }; for item in starting_points { collector.collect(*item); @@ -440,7 +437,7 @@ pub fn collect_reachable_items<'tcx>( } /// Return whether we should include the item into codegen. -/// We don't include foreign items only. +/// We don't include foreign items and items that don't have MIR. fn should_codegen_locally<'tcx>(tcx: TyCtxt<'tcx>, instance: &Instance<'tcx>) -> bool { if let Some(def_id) = instance.def.def_id_if_not_guaranteed_local_codegen() { if tcx.is_foreign_item(def_id) { @@ -469,30 +466,31 @@ fn should_codegen_locally<'tcx>(tcx: TyCtxt<'tcx>, instance: &Instance<'tcx>) -> /// /// This method also handles nested cases and `std` smart pointers. E.g.: /// -/// Conversion between `Rc>` into `Rc>` should return: -/// `Some(T, dyn Debug)` +/// Conversion between `Rc>` into `Rc>` should return: +/// `Some(String, dyn Debug)` /// /// The first step of this method is to extract the pointee types. Then we need to traverse the /// pointee types to find the actual trait and the type implementing it. /// /// TODO: Do we need to handle &Wrapper to &dyn T2 or is that taken care of with super /// trait handling? What about CoerceUnsized trait? -fn find_trait_conversion<'tcx>( +/// https://github.com/model-checking/kani/issues/1692 +fn extract_trait_casting<'tcx>( tcx: TyCtxt<'tcx>, src_ty: Ty<'tcx>, dst_ty: Ty<'tcx>, ) -> Option<(Ty<'tcx>, Ty<'tcx>)> { - let vtable_metadata = |mir_type: Ty<'tcx>| { + let has_vtable_metadata = |mir_type: Ty<'tcx>| { let (metadata, _) = mir_type.ptr_metadata_ty(tcx, |ty| ty); metadata != tcx.types.unit && metadata != tcx.types.usize }; trace!(?dst_ty, ?src_ty, "find_trait_conversion"); - let dst_ty_inner = find_pointer(tcx, dst_ty); - let src_ty_inner = find_pointer(tcx, src_ty); + let dst_ty_inner = extract_pointer(tcx, dst_ty); + let src_ty_inner = extract_pointer(tcx, src_ty); trace!(?dst_ty_inner, ?src_ty_inner, "find_trait_conversion"); - (vtable_metadata(dst_ty_inner) && !vtable_metadata(src_ty_inner)).then(|| { + (has_vtable_metadata(dst_ty_inner) && !has_vtable_metadata(src_ty_inner)).then(|| { let param_env = ParamEnv::reveal_all(); tcx.struct_lockstep_tails_erasing_lifetimes(src_ty_inner, dst_ty_inner, param_env) }) @@ -501,6 +499,7 @@ fn find_trait_conversion<'tcx>( /// This function extracts the pointee type of a regular pointer and std smart pointers. /// /// TODO: Refactor this to use `CustomCoerceUnsized` logic which includes custom smart pointers. +/// https://github.com/model-checking/kani/issues/1694 /// /// E.g.: For `Rc` where the Rc definition is: /// ``` @@ -515,65 +514,7 @@ fn find_trait_conversion<'tcx>( /// ``` /// /// This function will return `pointer: *const T`. -fn find_pointer<'tcx>(tcx: TyCtxt<'tcx>, typ: Ty<'tcx>) -> Ty<'tcx> { - struct ReceiverIter<'tcx> { - pub curr: Ty<'tcx>, - pub tcx: TyCtxt<'tcx>, - } - - impl<'tcx> LayoutOfHelpers<'tcx> for ReceiverIter<'tcx> { - type LayoutOfResult = TyAndLayout<'tcx>; - - #[inline] - fn handle_layout_err(&self, err: LayoutError, span: Span, ty: Ty<'tcx>) -> ! { - span_bug!(span, "failed to get layout for `{}`: {}", ty, err) - } - } - - impl<'tcx> HasParamEnv<'tcx> for ReceiverIter<'tcx> { - fn param_env(&self) -> ParamEnv<'tcx> { - ParamEnv::reveal_all() - } - } - - impl<'tcx> HasTyCtxt<'tcx> for ReceiverIter<'tcx> { - fn tcx(&self) -> TyCtxt<'tcx> { - self.tcx - } - } - - impl<'tcx> HasDataLayout for ReceiverIter<'tcx> { - fn data_layout(&self) -> &TargetDataLayout { - self.tcx.data_layout() - } - } - - impl<'tcx> Iterator for ReceiverIter<'tcx> { - type Item = (String, Ty<'tcx>); - - fn next(&mut self) -> Option { - if let TyKind::Adt(adt_def, adt_substs) = self.curr.kind() { - assert_eq!( - adt_def.variants().len(), - 1, - "Expected a single-variant ADT. Found {:?}", - self.curr - ); - let tcx = self.tcx; - let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; - let mut non_zsts = fields - .iter() - .filter(|field| !self.layout_of(field.ty(tcx, adt_substs)).is_zst()) - .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(tcx, adt_substs))); - let (name, next) = non_zsts.next().expect("Expected one non-zst field."); - assert!(non_zsts.next().is_none(), "Expected only one non-zst field."); - self.curr = next; - Some((name, self.curr)) - } else { - None - } - } - } +fn extract_pointer<'tcx>(tcx: TyCtxt<'tcx>, typ: Ty<'tcx>) -> Ty<'tcx> { if let Some(TypeAndMut { ty, .. }) = typ.builtin_deref(true) { ty } else { @@ -582,7 +523,7 @@ fn find_pointer<'tcx>(tcx: TyCtxt<'tcx>, typ: Ty<'tcx>) -> Ty<'tcx> { } /// Scans the allocation type and collect static objects. -fn global_alloc<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec { +fn collect_alloc_items<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec { let mut items = vec![]; match tcx.global_alloc(alloc_id) { GlobalAlloc::Static(def_id) => { @@ -601,14 +542,75 @@ fn global_alloc<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec { } GlobalAlloc::Memory(alloc) => { trace!(?alloc_id, "global_alloc memory"); - items - .extend(alloc.inner().relocations().values().flat_map(|id| global_alloc(tcx, *id))); + items.extend( + alloc.inner().relocations().values().flat_map(|id| collect_alloc_items(tcx, *id)), + ); } GlobalAlloc::VTable(ty, trait_ref) => { trace!(?alloc_id, "global_alloc vtable"); let vtable_id = tcx.vtable_allocation((ty, trait_ref)); - items.append(&mut global_alloc(tcx, vtable_id)); + items.append(&mut collect_alloc_items(tcx, vtable_id)); } }; items } + +/// Struct used to visit the data path of a received type all the way down to the data pointer. +struct ReceiverIter<'tcx> { + pub curr: Ty<'tcx>, + pub tcx: TyCtxt<'tcx>, +} + +impl<'tcx> LayoutOfHelpers<'tcx> for ReceiverIter<'tcx> { + type LayoutOfResult = TyAndLayout<'tcx>; + + #[inline] + fn handle_layout_err(&self, err: LayoutError, span: Span, ty: Ty<'tcx>) -> ! { + span_bug!(span, "failed to get layout for `{}`: {}", ty, err) + } +} + +impl<'tcx> HasParamEnv<'tcx> for ReceiverIter<'tcx> { + fn param_env(&self) -> ParamEnv<'tcx> { + ParamEnv::reveal_all() + } +} + +impl<'tcx> HasTyCtxt<'tcx> for ReceiverIter<'tcx> { + fn tcx(&self) -> TyCtxt<'tcx> { + self.tcx + } +} + +impl<'tcx> HasDataLayout for ReceiverIter<'tcx> { + fn data_layout(&self) -> &TargetDataLayout { + self.tcx.data_layout() + } +} + +impl<'tcx> Iterator for ReceiverIter<'tcx> { + type Item = (String, Ty<'tcx>); + + fn next(&mut self) -> Option { + if let TyKind::Adt(adt_def, adt_substs) = self.curr.kind() { + assert_eq!( + adt_def.variants().len(), + 1, + "Expected a single-variant ADT. Found {:?}", + self.curr + ); + let tcx = self.tcx; + let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; + let mut non_zsts = fields + .iter() + .filter(|field| !self.layout_of(field.ty(tcx, adt_substs)).is_zst()) + .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(tcx, adt_substs))); + let (name, next) = non_zsts.next().expect("Expected one non-zst field."); + assert!(non_zsts.next().is_none(), "Expected only one non-zst field."); + self.curr = next; + Some((name, self.curr)) + } else { + None + } + } +} diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs index e4d8aadfed31..a1514d454828 100644 --- a/tests/cargo-kani/mir-linker/src/lib.rs +++ b/tests/cargo-kani/mir-linker/src/lib.rs @@ -8,7 +8,7 @@ use semver::{BuildMetadata, Prerelease, Version}; fn check_version() { let next_major: u64 = kani::any(); let next_minor: u64 = kani::any(); - kani::assume(next_major.wrapping_add(next_minor) > 0); + kani::assume(next_major != 0 || next_minor != 0); // Check whether this requirement matches version 1.2.3-alpha.1 (no) let v0 = Version { From da2a9727ec6da40e99e1734e9de48040ed56bc94 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 19 Sep 2022 10:13:18 -0700 Subject: [PATCH 7/9] We use `sess.abort_if_errors()` for global ASM errors Thus, we no longer print "Failed to compile crate" --- .../asm/global_error/doesnt_call_crate_with_global_asm.expected | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected index 4a5476f7207f..89d23a65d258 100644 --- a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected +++ b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected @@ -1,4 +1,3 @@ error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**). -Error: "Failed to compile crate." error: could not compile `crate_with_global_asm` due to previous error Error: cargo exited with status exit status: 101 From da951ce45bd11bc181b6f9ac11c61956668e876f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 20 Sep 2022 09:50:57 -0700 Subject: [PATCH 8/9] Fix doc and remove println :) --- kani-compiler/src/codegen_cprover_gotoc/reachability.rs | 5 ++--- tools/compiletest/src/common.rs | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs index 0f895c1181cd..7da8b5d603a1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs @@ -432,7 +432,6 @@ pub fn collect_reachable_items<'tcx>( // order of the errors and warnings is stable. let mut sorted_items: Vec<_> = collector.collected.into_iter().collect(); sorted_items.sort_by_cached_key(|item| to_fingerprint(tcx, item)); - sorted_items.iter().for_each(|item| println!("{:?}", item)); sorted_items } @@ -474,7 +473,7 @@ fn should_codegen_locally<'tcx>(tcx: TyCtxt<'tcx>, instance: &Instance<'tcx>) -> /// /// TODO: Do we need to handle &Wrapper to &dyn T2 or is that taken care of with super /// trait handling? What about CoerceUnsized trait? -/// https://github.com/model-checking/kani/issues/1692 +/// fn extract_trait_casting<'tcx>( tcx: TyCtxt<'tcx>, src_ty: Ty<'tcx>, @@ -499,7 +498,7 @@ fn extract_trait_casting<'tcx>( /// This function extracts the pointee type of a regular pointer and std smart pointers. /// /// TODO: Refactor this to use `CustomCoerceUnsized` logic which includes custom smart pointers. -/// https://github.com/model-checking/kani/issues/1694 +/// /// /// E.g.: For `Rc` where the Rc definition is: /// ``` diff --git a/tools/compiletest/src/common.rs b/tools/compiletest/src/common.rs index f039d8925e21..03a1fb6efca9 100644 --- a/tools/compiletest/src/common.rs +++ b/tools/compiletest/src/common.rs @@ -140,7 +140,7 @@ pub struct Config { /// Allow us to run the regression with the mir linker enabled by default. For that, set /// `RUSTFLAGS=--cfg=mir_linker` while compiling `compiletest`. - /// Remove this as part of https://github.com/model-checking/kani/issues/1677 + /// Remove this as part of pub mir_linker: bool, } From 1cfafe63d895cd358493b3872751962005bdb961 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 20 Sep 2022 11:55:22 -0700 Subject: [PATCH 9/9] Improve comments --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 2a18d4681e7c..940cb773d4a6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -74,7 +74,7 @@ impl CodegenBackend for GotocCodegenBackend { return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); } - // we first declare all functions + // we first declare all items for item in &items { match *item { MonoItem::Fn(instance) => { @@ -346,7 +346,16 @@ fn codegen_results( )) } -/// Retrieve all items that need to be processed. +/// Retrieve all items that need to be processed according to the selected reachability mode: +/// +/// - Harnesses: Cross-crate collection of all reachable items starting from local harnesses. +/// - None: Skip collection and codegen all together. This is used to compile dependencies. +/// - Legacy: Use regular compiler collection that will collect local items, and a few cross +/// crate items (such as generic functions and functions candidate to be inlined). +/// +/// To be implemented: +/// - PubFns: Cross-crate reachability analysis that use the local public fns as starting point. + fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec> { let tcx = gcx.tcx; let reach = gcx.queries.get_reachability_analysis();