Skip to content

Commit

Permalink
Migrate foreign function, compiler-interface and kani-middle modules …
Browse files Browse the repository at this point in the history 
…to use StableMIR (#2959)

We still need internal APIs to handle things like:

- **FnAbi:** Support is pending this PR to be merged:
rust-lang/rust#119094
- **Filter non-function items:** Also pending a fix on the rust side:
rust-lang/rust#119135
- **Checking for reachable functions:** This is not needed in theory,
but std lib build fails since it unncovers an existing issue in Kani
with a function that was not previously included. I'll create an issue
for that. It's unrelated to this change though.
- **Function attribute handling**
- **Span error**

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
  • Loading branch information
@celinval @adpaco-aws
celinval and adpaco-aws authored Dec 20, 2023
1 parent c28dc5a commit ee0ff7e
Show file tree
Hide file tree
Showing 14 changed files with 221 additions and 238 deletions.
43 changes: 19 additions & 24 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,10 @@ use crate::kani_middle;
use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
use cbmc::{InternString, InternedString};
use lazy_static::lazy_static;
use rustc_middle::ty::Instance;
use rustc_smir::rustc_internal;
use rustc_target::abi::call::Conv;
use stable_mir::mir::mono::Instance as InstanceStable;
use stable_mir::mir::mono::Instance;
use stable_mir::CrateDef;
use tracing::{debug, trace};

lazy_static! {
Expand Down Expand Up @@ -46,15 +46,16 @@ impl<'tcx> GotocCtx<'tcx> {
///
/// For other foreign items, we declare a shim and add to the list of foreign shims to be
/// handled later.
pub fn codegen_foreign_fn(&mut self, instance: InstanceStable) -> &Symbol {
pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
debug!(?instance, "codegen_foreign_function");
let instance = rustc_internal::internal(instance);
let fn_name = self.symbol_name(instance).intern();
let instance_internal = rustc_internal::internal(instance);
let fn_name = self.symbol_name_stable(instance).intern();
if self.symbol_table.contains(fn_name) {
// Symbol has been added (either a built-in CBMC function or a Rust allocation function).
self.symbol_table.lookup(fn_name).unwrap()
} else if RUST_ALLOC_FNS.contains(&fn_name)
|| (self.is_cffi_enabled() && kani_middle::fn_abi(self.tcx, instance).conv == Conv::C)
|| (self.is_cffi_enabled()
&& kani_middle::fn_abi(self.tcx, instance_internal).conv == Conv::C)
{
// Add a Rust alloc lib function as is declared by core.
// When C-FFI feature is enabled, we just trust the rust declaration.
Expand All @@ -63,14 +64,8 @@ impl<'tcx> GotocCtx<'tcx> {
// https://github.com/model-checking/kani/issues/2426
self.ensure(fn_name, |gcx, _| {
let typ = gcx.codegen_ffi_type(instance);
Symbol::function(
fn_name,
typ,
None,
gcx.readable_instance_name(instance),
Location::none(),
)
.with_is_extern(true)
Symbol::function(fn_name, typ, None, instance.name(), Location::none())
.with_is_extern(true)
})
} else {
let shim_name = format!("{fn_name}_ffi_shim");
Expand All @@ -82,7 +77,7 @@ impl<'tcx> GotocCtx<'tcx> {
&shim_name,
typ,
Some(gcx.codegen_ffi_shim(shim_name.as_str().into(), instance)),
gcx.readable_instance_name(instance),
instance.name(),
Location::none(),
)
})
Expand All @@ -96,19 +91,19 @@ impl<'tcx> GotocCtx<'tcx> {
}

/// Generate code for a foreign function shim.
fn codegen_ffi_shim(&mut self, shim_name: InternedString, instance: Instance<'tcx>) -> Stmt {
fn codegen_ffi_shim(&mut self, shim_name: InternedString, instance: Instance) -> Stmt {
debug!(?shim_name, ?instance, sym=?self.symbol_table.lookup(shim_name), "generate_foreign_shim");

let loc = self.codegen_span(&self.tcx.def_span(instance.def_id()));
let loc = self.codegen_span_stable(instance.def.span());
let unsupported_check = self.codegen_ffi_unsupported(instance, loc);
Stmt::block(vec![unsupported_check], loc)
}

/// Generate type for the given foreign instance.
fn codegen_ffi_type(&mut self, instance: Instance<'tcx>) -> Type {
let fn_name = self.symbol_name(instance);
let fn_abi = kani_middle::fn_abi(self.tcx, instance);
let loc = self.codegen_span(&self.tcx.def_span(instance.def_id()));
fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
let fn_name = self.symbol_name_stable(instance);
let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance));
let loc = self.codegen_span_stable(instance.def.span());
let params = fn_abi
.args
.iter()
Expand Down Expand Up @@ -137,15 +132,15 @@ impl<'tcx> GotocCtx<'tcx> {
///
/// This will behave like `codegen_unimplemented_stmt` but print a message that includes
/// the name of the function not supported and the calling convention.
fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt {
let fn_name = &self.symbol_name(instance);
fn codegen_ffi_unsupported(&mut self, instance: Instance, loc: Location) -> Stmt {
let fn_name = &self.symbol_name_stable(instance);
debug!(?fn_name, ?loc, "codegen_ffi_unsupported");

// Save this occurrence so we can emit a warning in the compilation report.
let entry = self.unsupported_constructs.entry("foreign function".into()).or_default();
entry.push(loc);

let call_conv = kani_middle::fn_abi(self.tcx, instance).conv;
let call_conv = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)).conv;
let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`");
let url = if call_conv == Conv::C {
"https://github.com/model-checking/kani/issues/2423"
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1331,7 +1331,7 @@ impl<'tcx> GotocCtx<'tcx> {
TyKind::RigidTy(RigidTy::Slice(_)) | TyKind::RigidTy(RigidTy::Str) => {
let unit_t = match ty.kind() {
TyKind::RigidTy(RigidTy::Slice(et)) => et,
TyKind::RigidTy(RigidTy::Str) => rustc_internal::stable(self.tcx.types.u8),
TyKind::RigidTy(RigidTy::Str) => Ty::unsigned_ty(UintTy::U8),
_ => unreachable!(),
};
let unit = self.layout_of_stable(unit_t);
Expand Down
80 changes: 36 additions & 44 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use crate::kani_middle::{check_reachable_items, dump_mir_items};
use crate::kani_queries::QueryDb;
use cbmc::goto_program::Location;
use cbmc::irep::goto_binary_serde::write_goto_binary_file;
use cbmc::RoundingMode;
use cbmc::{InternString, RoundingMode};
use cbmc::{InternedString, MachineModel};
use kani_metadata::artifact::convert_type;
use kani_metadata::CompilerArtifactStub;
Expand All @@ -32,12 +32,10 @@ use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
use rustc_data_structures::temp_dir::MaybeTempDir;
use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
use rustc_hir::def_id::LOCAL_CRATE;
use rustc_hir::definitions::DefPathHash;
use rustc_metadata::creader::MetadataLoaderDyn;
use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
use rustc_metadata::EncodedMetadata;
use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
use rustc_middle::mir::mono::MonoItem;
use rustc_middle::ty::TyCtxt;
use rustc_middle::util::Providers;
use rustc_session::config::{CrateType, OutputFilenames, OutputType};
Expand All @@ -46,7 +44,7 @@ use rustc_session::Session;
use rustc_smir::rustc_internal;
use rustc_target::abi::Endian;
use rustc_target::spec::PanicStrategy;
use stable_mir::mir::mono::MonoItem as MonoItemStable;
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::CrateDef;
use std::any::Any;
use std::collections::BTreeMap;
Expand Down Expand Up @@ -82,10 +80,10 @@ impl GotocCodegenBackend {
fn codegen_items<'tcx>(
&self,
tcx: TyCtxt<'tcx>,
starting_items: &[MonoItem<'tcx>],
starting_items: &[MonoItem],
symtab_goto: &Path,
machine_model: &MachineModel,
) -> (GotocCtx<'tcx>, Vec<MonoItem<'tcx>>) {
) -> (GotocCtx<'tcx>, Vec<MonoItem>) {
let items = with_timer(
|| collect_reachable_items(tcx, starting_items),
"codegen reachability analysis",
Expand All @@ -103,17 +101,13 @@ impl GotocCodegenBackend {
for item in &items {
match *item {
MonoItem::Fn(instance) => {
let instance = rustc_internal::stable(instance);
gcx.call_with_panic_debug_info(
|ctx| ctx.declare_function(instance),
format!("declare_function: {}", instance.name()),
instance.def,
);
}
MonoItem::Static(_) => {
let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
unreachable!()
};
MonoItem::Static(def) => {
gcx.call_with_panic_debug_info(
|ctx| ctx.declare_static(def),
format!("declare_static: {}", def.name()),
Expand All @@ -128,7 +122,6 @@ impl GotocCodegenBackend {
for item in &items {
match *item {
MonoItem::Fn(instance) => {
let instance = rustc_internal::stable(instance);
gcx.call_with_panic_debug_info(
|ctx| ctx.codegen_function(instance),
format!(
Expand All @@ -139,10 +132,7 @@ impl GotocCodegenBackend {
instance.def,
);
}
MonoItem::Static(_) => {
let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
unreachable!()
};
MonoItem::Static(def) => {
gcx.call_with_panic_debug_info(
|ctx| ctx.codegen_static(def),
format!("codegen_static: {}", def.name()),
Expand Down Expand Up @@ -237,28 +227,31 @@ impl CodegenBackend for GotocCodegenBackend {
ReachabilityType::Harnesses => {
// Cross-crate collecting of all items that are reachable from the crate harnesses.
let harnesses = queries.target_harnesses();
let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
let mut items: HashSet<_> = HashSet::with_capacity(harnesses.len());
items.extend(harnesses);
let harnesses = filter_crate_items(tcx, |_, def_id| {
items.contains(&tcx.def_path_hash(def_id))
let harnesses = filter_crate_items(tcx, |_, instance| {
items.contains(&instance.mangled_name().intern())
});
for harness in harnesses {
let model_path = queries
.harness_model_path(&tcx.def_path_hash(harness.def_id()))
.unwrap();
let (gcx, items) =
self.codegen_items(tcx, &[harness], model_path, &results.machine_model);
results.extend(gcx, items, None);
let model_path =
queries.harness_model_path(&harness.mangled_name()).unwrap();
let (gcx, mono_items) = self.codegen_items(
tcx,
&[MonoItem::Fn(harness)],
model_path,
&results.machine_model,
);
results.extend(gcx, mono_items, None);
}
}
ReachabilityType::Tests => {
// We're iterating over crate items here, so what we have to codegen is the "test description" containing the
// 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, |_, def_id| {
if is_test_harness_description(tcx, def_id) {
descriptions.push(def_id);
let harnesses = filter_const_crate_items(tcx, |_, item| {
if is_test_harness_description(tcx, item.def) {
descriptions.push(item.def);
true
} else {
false
Expand Down Expand Up @@ -289,11 +282,15 @@ impl CodegenBackend for GotocCodegenBackend {
}
ReachabilityType::None => {}
ReachabilityType::PubFns => {
let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
let local_reachable = filter_crate_items(tcx, |_, def_id| {
(tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
|| entry_fn == Some(def_id)
});
let main_instance =
stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap());
let local_reachable = filter_crate_items(tcx, |_, instance| {
let def_id = rustc_internal::internal(instance.def.def_id());
Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id)
})
.into_iter()
.map(MonoItem::Fn)
.collect::<Vec<_>>();
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
let (gcx, items) = self.codegen_items(
tcx,
Expand Down Expand Up @@ -527,17 +524,17 @@ where
}
}

struct GotoCodegenResults<'tcx> {
struct GotoCodegenResults {
reachability: ReachabilityType,
harnesses: Vec<HarnessMetadata>,
unsupported_constructs: UnsupportedConstructs,
concurrent_constructs: UnsupportedConstructs,
items: Vec<MonoItem<'tcx>>,
items: Vec<MonoItem>,
crate_name: InternedString,
machine_model: MachineModel,
}

impl<'tcx> GotoCodegenResults<'tcx> {
impl GotoCodegenResults {
pub fn new(tcx: TyCtxt, reachability: ReachabilityType) -> Self {
GotoCodegenResults {
reachability,
Expand Down Expand Up @@ -585,12 +582,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {
}
}

fn extend(
&mut self,
gcx: GotocCtx,
items: Vec<MonoItem<'tcx>>,
metadata: Option<HarnessMetadata>,
) {
fn extend(&mut self, gcx: GotocCtx, items: Vec<MonoItem>, metadata: Option<HarnessMetadata>) {
let mut items = items;
self.harnesses.extend(metadata);
self.concurrent_constructs.extend(gcx.concurrent_constructs);
Expand All @@ -599,7 +591,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {
}

/// Prints a report at the end of the compilation.
fn print_report(&self, tcx: TyCtxt<'tcx>) {
fn print_report(&self, tcx: TyCtxt) {
// Print all unsupported constructs.
if !self.unsupported_constructs.is_empty() {
// Sort alphabetically.
Expand Down Expand Up @@ -631,7 +623,7 @@ impl<'tcx> GotoCodegenResults<'tcx> {

// Print some compilation stats.
if tracing::enabled!(tracing::Level::INFO) {
analysis::print_stats(tcx, &self.items);
analysis::print_stats(&self.items);
}
}
}
Expand Down
31 changes: 3 additions & 28 deletions kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,9 @@ use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::InternedString;
use rustc_hir::def_id::LOCAL_CRATE;
use rustc_middle::mir::mono::CodegenUnitNameBuilder;
use rustc_middle::ty::print::with_no_trimmed_paths;
use rustc_middle::ty::{Instance, TyCtxt};
use stable_mir::mir::mono::Instance as InstanceStable;
use rustc_middle::ty::TyCtxt;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::Local;
use tracing::debug;

impl<'tcx> GotocCtx<'tcx> {
/// The full crate name including versioning info
Expand Down Expand Up @@ -52,34 +50,11 @@ impl<'tcx> GotocCtx<'tcx> {
format!("{var_name}_init")
}

/// A human readable name in Rust for reference, should not be used as a key.
pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String {
with_no_trimmed_paths!(self.tcx.def_path_str_with_args(instance.def_id(), instance.args))
}

/// The actual function name used in the symbol table
pub fn symbol_name(&self, instance: Instance<'tcx>) -> String {
let llvm_mangled = self.tcx.symbol_name(instance).name.to_string();
debug!(
"finding function name for instance: {}, debug: {:?}, name: {}, symbol: {}",
instance,
instance,
self.readable_instance_name(instance),
llvm_mangled,
);

let pretty = self.readable_instance_name(instance);

// Make main function a special case in order to support `--function main`
// TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
if pretty == "main" { pretty } else { llvm_mangled }
}

/// Return the mangled name to be used in the symbol table.
///
/// We special case main function in order to support `--function main`.
// TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
pub fn symbol_name_stable(&self, instance: InstanceStable) -> String {
pub fn symbol_name_stable(&self, instance: Instance) -> String {
let pretty = instance.name();
if pretty == "main" { pretty } else { instance.mangled_name() }
}
Expand Down
Loading

0 comments on commit ee0ff7e

Please sign in to comment.