Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions docs/src/rustc-hacks.md
Original file line number Diff line number Diff line change
Expand Up @@ -68,11 +68,11 @@ Here is an example:
# ** At the bottom of the dependencies section: **
# Adjust the path here to point to a local copy of the rust compiler.
# E.g.: ~/.rustup/toolchains/<toolchain>/lib/rustlib/rustc-src/rust/compiler
rustc_smir = { path = "<path_to_rustc>/rustc_smir", optional = true }
stable_mir = { path = "<path_to_rustc>/stable_mir", optional = true }
rustc_public_bridge = { path = "<path_to_rustc>/rustc_public_bridge", optional = true }
rustc_public = { path = "<path_to_rustc>/rustc_public", optional = true }

[features]
clion = ['rustc_smir', 'stable_mir']
clion = ['rustc_public_bridge', 'rustc_public']
```

**Don't forget to rollback the changes before you create your PR.**
Expand Down
6 changes: 3 additions & 3 deletions docs/src/stable-mir.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ despite them not being stable yet.

### StableMIR APIs

For now, the StableMIR APIs are exposed as a crate in the compiler named `stable_mir`.
For now, the StableMIR APIs are exposed as a crate in the compiler named `rustc_public`.
This crate includes the definition of structures and methods to be stabilized,
which are expected to become the stable APIs in the compiler.
To reduce the migration burden, these APIs are somewhat close to the original compiler interfaces.
Expand Down Expand Up @@ -59,15 +59,15 @@ there are two helpful methods to convert StableMIR constructs to internal rustc
- `rustc_internal::internal()`: Convert a Stable item into an internal one.
- `rustc_internal::stable()`: Convert an internal item into a Stable one.

Both of these methods are inside `rustc_smir` crate in the `rustc_internal`
Both of these methods are inside `rustc_public_bridge` crate in the `rustc_internal`
module inside the compiler.
Note that there is no plan to stabilize any of these methods,
and there's also no guarantee on its support and coverage.

The conversion is not implemented for all items, and some conversions may be incomplete.
Please proceed with caution when using these methods.

Besides that, do not invoke any other `rustc_smir` methods, except for `run`.
Besides that, do not invoke any other `rustc_public_bridge` methods, except for `run`.
This crate's methods are not meant to be invoked externally.
Note that, the method `run` will also eventually be replaced by a Stable driver.

Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,12 +33,12 @@ use rustc_metadata::EncodedMetadata;
use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
use rustc_middle::ty::TyCtxt;
use rustc_middle::util::Providers;
use rustc_public::mir::mono::{Instance, MonoItem};
use rustc_public::rustc_internal;
use rustc_public::{CrateDef, DefId};
use rustc_session::Session;
use rustc_session::config::{CrateType, OutputFilenames, OutputType};
use rustc_session::output::out_filename;
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::rustc_internal;
use stable_mir::{CrateDef, DefId};
use std::any::Any;
use std::fs::File;
use std::path::Path;
Expand Down Expand Up @@ -253,8 +253,8 @@ impl CodegenBackend for LlbcCodegenBackend {
ReachabilityType::PubFns => {
let unit = CodegenUnit::default();
let transformer = BodyTransformation::new(&queries, tcx, &unit);
let main_instance =
stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap());
let main_instance = rustc_public::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(tcx, instance.def.def_id());
Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id)
Expand Down
12 changes: 6 additions & 6 deletions kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -56,19 +56,19 @@ use charon_lib::{error_assert, error_or_panic};
use core::panic;
use rustc_data_structures::fx::FxHashMap;
use rustc_middle::ty::{TyCtxt, TypingEnv};
use stable_mir::mir::mono::{Instance, InstanceDef};
use stable_mir::mir::{
use rustc_public::mir::mono::{Instance, InstanceDef};
use rustc_public::mir::{
AggregateKind, BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Local, Mutability,
Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator,
TerminatorKind, UnOp, VarDebugInfoContents,
};
use stable_mir::rustc_internal;
use stable_mir::ty::{
use rustc_public::rustc_internal;
use rustc_public::ty::{
AdtDef, AdtKind, Allocation, ConstantKind, FnDef, GenericArgKind, GenericArgs,
GenericParamDefKind, IntTy, MirConst, Region, RegionKind, RigidTy, Span, TraitDecl, TraitDef,
Ty, TyConst, TyConstKind, TyKind, UintTy,
};
use stable_mir::{CrateDef, CrateDefType, DefId};
use rustc_public::{CrateDef, CrateDefType, DefId};
use std::collections::HashMap;
use std::iter::zip;
use std::path::PathBuf;
Expand Down Expand Up @@ -157,7 +157,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {

//This function extract the traitrefs and their span from a def_id
//Those information will be added into generic args of the type or the func with the def_id
//Note that Generic args of Charon contains trait_refs while those of stable_mir do not
//Note that Generic args of Charon contains trait_refs while those of rustc_public do not
fn get_traitrefs_and_span_from_defid(
&mut self,
defid: DefId,
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ use super::source_region::SourceRegion;
use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::InternedString;
use cbmc::goto_program::{Expr, Location, Stmt, Type};
use stable_mir::mir::{Place, ProjectionElem};
use stable_mir::ty::{Span as SpanStable, Ty};
use rustc_public::mir::{Place, ProjectionElem};
use rustc_public::ty::{Span as SpanStable, Ty};
use strum_macros::{AsRefStr, EnumString};
use tracing::debug;

Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

use crate::codegen_cprover_gotoc::GotocCtx;
use stable_mir::mir::{BasicBlock, BasicBlockIdx, Body};
use rustc_public::mir::{BasicBlock, BasicBlockIdx, Body};
use std::collections::HashSet;
use tracing::debug;

Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@ use cbmc::goto_program::FunctionContract;
use cbmc::goto_program::{Expr, Lambda, Location, Type};
use kani_metadata::AssignsContract;
use rustc_hir::def_id::DefId as InternalDefId;
use stable_mir::CrateDef;
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::mir::{Local, VarDebugInfoContents};
use stable_mir::rustc_internal;
use stable_mir::ty::{FnDef, RigidTy, TyKind};
use rustc_public::CrateDef;
use rustc_public::mir::mono::{Instance, MonoItem};
use rustc_public::mir::{Local, VarDebugInfoContents};
use rustc_public::rustc_internal;
use rustc_public::ty::{FnDef, RigidTy, TyKind};

impl GotocCtx<'_> {
/// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -15,11 +15,11 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
use cbmc::{InternString, InternedString};
use lazy_static::lazy_static;
use stable_mir::CrateDef;
use stable_mir::abi::{CallConvention, PassMode};
use stable_mir::mir::Place;
use stable_mir::mir::mono::Instance;
use stable_mir::ty::{RigidTy, TyKind};
use rustc_public::CrateDef;
use rustc_public::abi::{CallConvention, PassMode};
use rustc_public::mir::Place;
use rustc_public::mir::mono::Instance;
use rustc_public::ty::{RigidTy, TyKind};
use tracing::{debug, trace};

lazy_static! {
Expand Down
20 changes: 10 additions & 10 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,10 @@ use crate::codegen_cprover_gotoc::codegen::block::reverse_postorder;
use cbmc::InternString;
use cbmc::InternedString;
use cbmc::goto_program::{Expr, Stmt, Symbol};
use stable_mir::CrateDef;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{Body, Local};
use stable_mir::ty::{RigidTy, TyKind};
use rustc_public::CrateDef;
use rustc_public::mir::mono::Instance;
use rustc_public::mir::{Body, Local};
use rustc_public::ty::{RigidTy, TyKind};
use std::collections::BTreeMap;
use tracing::{debug, debug_span};

Expand Down Expand Up @@ -235,17 +235,17 @@ impl GotocCtx<'_> {
}
}

pub mod rustc_smir {
pub mod rustc_public_bridge {
use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region};
use crate::stable_mir::CrateDef;
use crate::rustc_public::CrateDef;
use rustc_middle::mir::coverage::BasicCoverageBlock;
use rustc_middle::mir::coverage::MappingKind::Code;
use rustc_middle::ty::TyCtxt;
use stable_mir::mir::mono::Instance;
use stable_mir::rustc_internal;
use stable_mir::{Filename, Opaque};
use rustc_public::mir::mono::Instance;
use rustc_public::rustc_internal;
use rustc_public::{Filename, Opaque};

type CoverageOpaque = stable_mir::Opaque;
type CoverageOpaque = rustc_public::Opaque;

/// Retrieves the `SourceRegion` associated with the data in a
/// `CoverageOpaque` object.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type};
use rustc_middle::ty::TypingEnv;
use rustc_middle::ty::layout::ValidityRequirement;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{BasicBlockIdx, Operand, Place};
use stable_mir::rustc_internal;
use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
use rustc_public::mir::mono::Instance;
use rustc_public::mir::{BasicBlockIdx, Operand, Place};
use rustc_public::rustc_internal;
use rustc_public::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
use tracing::debug;

pub struct SizeAlign {
Expand Down
14 changes: 7 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,16 +6,16 @@ use crate::kani_middle::is_anon_static;
use crate::unwrap_or_return_codegen_unimplemented;
use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type};
use rustc_middle::ty::Const as ConstInternal;
use rustc_span::Span as SpanInternal;
use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
use stable_mir::mir::mono::{Instance, StaticDef};
use stable_mir::mir::{Mutability, Operand};
use stable_mir::rustc_internal;
use stable_mir::ty::{
use rustc_public::mir::alloc::{AllocId, GlobalAlloc};
use rustc_public::mir::mono::{Instance, StaticDef};
use rustc_public::mir::{Mutability, Operand};
use rustc_public::rustc_internal;
use rustc_public::ty::{
Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty,
TyConst, TyConstKind, TyKind, UintTy,
};
use stable_mir::{CrateDef, CrateItem};
use rustc_public::{CrateDef, CrateItem};
use rustc_span::Span as SpanInternal;
use tracing::{debug, trace};

#[derive(Clone, Debug)]
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,9 @@ use crate::unwrap_or_return_codegen_unimplemented;
use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, Type};
use rustc_abi::{TagEncoding, Variants};
use rustc_middle::ty::layout::LayoutOf;
use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
use stable_mir::rustc_internal;
use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
use rustc_public::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
use rustc_public::rustc_internal;
use rustc_public::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx};
use tracing::{debug, trace, warn};

/// A projection in Kani can either be to a type (the normal case),
Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,13 +20,13 @@ use cbmc::{InternString, InternedString, btree_string_map};
use num::bigint::BigInt;
use rustc_abi::{FieldsShape, TagEncoding, Variants};
use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry};
use stable_mir::abi::{Primitive, Scalar, ValueAbi};
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{
use rustc_public::abi::{Primitive, Scalar, ValueAbi};
use rustc_public::mir::mono::Instance;
use rustc_public::mir::{
AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
};
use stable_mir::rustc_internal;
use stable_mir::ty::{
use rustc_public::rustc_internal;
use rustc_public::ty::{
Binder, ClosureKind, ExistentialPredicate, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy,
VariantIdx,
};
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,9 @@ use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::Location;
use lazy_static::lazy_static;
use rustc_hir::Attribute;
use rustc_public::rustc_internal;
use rustc_public::ty::Span as SpanStable;
use rustc_span::Span;
use stable_mir::rustc_internal;
use stable_mir::ty::Span as SpanStable;
use std::collections::HashMap;

lazy_static! {
Expand Down
14 changes: 7 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
use super::typ::FN_RETURN_VOID_VAR_NAME;
use super::typ::TypeExt;
use super::{PropertyClass, bb_label};
use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque;
use crate::codegen_cprover_gotoc::codegen::function::rustc_public_bridge::region_from_coverage_opaque;
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
use crate::unwrap_or_return_codegen_unimplemented_stmt;
use cbmc::goto_program::ExprValue;
Expand All @@ -12,15 +12,15 @@ use rustc_abi::Size;
use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{List, TypingEnv};
use stable_mir::CrateDef;
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
use stable_mir::mir::mono::{Instance, InstanceKind};
use stable_mir::mir::{
use rustc_public::CrateDef;
use rustc_public::abi::{ArgAbi, FnAbi, PassMode};
use rustc_public::mir::mono::{Instance, InstanceKind};
use rustc_public::mir::{
AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
};
use stable_mir::rustc_internal;
use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
use rustc_public::rustc_internal;
use rustc_public::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx};
use tracing::{debug, debug_span, trace};

impl GotocCtx<'_> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@

use crate::codegen_cprover_gotoc::GotocCtx;
use crate::kani_middle::is_interior_mut;
use stable_mir::CrateDef;
use stable_mir::mir::mono::{Instance, StaticDef};
use rustc_public::CrateDef;
use rustc_public::mir::mono::{Instance, StaticDef};
use tracing::debug;

impl GotocCtx<'_> {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,10 @@ use crate::codegen_cprover_gotoc::GotocCtx;
use crate::kani_middle::abi::LayoutOf;
use cbmc::goto_program::Type;
use rustc_middle::ty::layout::{LayoutOf as _, TyAndLayout};
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{Local, Operand, Place, Rvalue};
use stable_mir::rustc_internal;
use stable_mir::ty::{FnSig, RigidTy, Ty, TyKind};
use rustc_public::mir::mono::Instance;
use rustc_public::mir::{Local, Operand, Place, Rvalue};
use rustc_public::rustc_internal;
use rustc_public::ty::{FnSig, RigidTy, Ty, TyKind};

impl<'tcx> GotocCtx<'tcx> {
pub fn place_ty_stable(&self, place: &Place) -> Ty {
Expand Down
14 changes: 7 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,15 +20,15 @@ use rustc_middle::ty::{
};
use rustc_middle::ty::{ExistentialTraitRef, GenericArgsRef};
use rustc_middle::ty::{List, TypeFoldable};
use rustc_span::def_id::DefId;
use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
use stable_mir::mir::Body;
use stable_mir::mir::mono::Instance as InstanceStable;
use stable_mir::rustc_internal;
use stable_mir::ty::{
use rustc_public::abi::{ArgAbi, FnAbi, PassMode};
use rustc_public::mir::Body;
use rustc_public::mir::mono::Instance as InstanceStable;
use rustc_public::rustc_internal;
use rustc_public::ty::{
Binder, DynKind, ExistentialPredicate, ExistentialProjection, Region, RegionKind, RigidTy,
Ty as StableTy,
};
use rustc_span::def_id::DefId;
use tracing::{debug, trace, warn};

/// Map the unit type to an empty struct
Expand Down Expand Up @@ -304,7 +304,7 @@ impl<'tcx> GotocCtx<'tcx> {
let rigid =
RigidTy::Dynamic(predictates, Region { kind: RegionKind::ReErased }, DynKind::Dyn);

stable_mir::ty::Ty::from_rigid_kind(rigid)
rustc_public::ty::Ty::from_rigid_kind(rigid)
}

/// Generates the type for a single field for a dynamic vtable.
Expand Down
Loading
Loading