Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update toolchain to nightly 2023-08-04 #2661

Merged
2 changes: 1 addition & 1 deletion cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1410,7 +1410,7 @@ impl Expr {
ArithmeticOverflowResult { result, overflowed }
}

/// Uses CBMC's [binop]-with-overflow operation that performs a single arithmetic
/// Uses CBMC's \[binop\]-with-overflow operation that performs a single arithmetic
/// operation
/// `struct (T, bool) overflow(binop, self, e)` where `T` is the type of `self`
/// Pseudocode:
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -110,16 +110,15 @@ impl<'tcx> GotocCtx<'tcx> {
.args
.iter()
.enumerate()
.filter_map(|(idx, arg)| {
(!arg.is_ignore()).then(|| {
let arg_name = format!("{fn_name}::param_{idx}");
let base_name = format!("param_{idx}");
let arg_type = self.codegen_ty(arg.layout.ty);
let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
.with_is_parameter(true);
self.symbol_table.insert(sym);
arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
})
.filter(|&(_, arg)| (!arg.is_ignore()))
.map(|(idx, arg)| {
let arg_name = format!("{fn_name}::param_{idx}");
let base_name = format!("param_{idx}");
let arg_type = self.codegen_ty(arg.layout.ty);
let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
.with_is_parameter(true);
self.symbol_table.insert(sym);
arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
})
.collect();
let ret_type = self.codegen_ty(fn_abi.ret.layout.ty);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ impl<'tcx> GotocCtx<'tcx> {

let tupe = sig.inputs().last().unwrap();
let args = match tupe.kind() {
ty::Tuple(substs) => *substs,
ty::Tuple(args) => *args,
_ => unreachable!("a function's spread argument must be a tuple"),
};
let starting_idx = sig.inputs().len();
Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -245,7 +245,7 @@ impl<'tcx> GotocCtx<'tcx> {

macro_rules! codegen_size_align {
($which: ident) => {{
let tp_ty = instance.substs.type_at(0);
let tp_ty = instance.args.type_at(0);
let arg = fargs.remove(0);
let size_align = self.size_and_align_of_dst(tp_ty, arg);
self.codegen_expr_to_place(p, size_align.$which)
Expand Down Expand Up @@ -422,7 +422,7 @@ impl<'tcx> GotocCtx<'tcx> {
"cttz" => codegen_count_intrinsic!(cttz, true),
"cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
"discriminant_value" => {
let ty = instance.substs.type_at(0);
let ty = instance.args.type_at(0);
let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
self.codegen_expr_to_place(p, e)
}
Expand Down Expand Up @@ -764,7 +764,7 @@ impl<'tcx> GotocCtx<'tcx> {
intrinsic: &str,
span: Option<Span>,
) -> Stmt {
let ty = instance.substs.type_at(0);
let ty = instance.args.type_at(0);
let layout = self.layout_of(ty);
// Note: We follow the pattern seen in `codegen_panic_intrinsic` from `rustc_codegen_ssa`
// https://github.com/rust-lang/rust/blob/master/compiler/rustc_codegen_ssa/src/mir/block.rs
Expand Down Expand Up @@ -1034,7 +1034,7 @@ impl<'tcx> GotocCtx<'tcx> {
let offset = fargs.remove(0);

// Check that computing `offset` in bytes would not overflow
let ty = self.monomorphize(instance.substs.type_at(0));
let ty = self.monomorphize(instance.args.type_at(0));
let (offset_bytes, bytes_overflow_check) =
self.count_in_bytes(offset.clone(), ty, Type::ssize_t(), intrinsic, loc);

Expand Down Expand Up @@ -1184,7 +1184,7 @@ impl<'tcx> GotocCtx<'tcx> {
p: &Place<'tcx>,
loc: Location,
) -> Stmt {
let ty = self.monomorphize(instance.substs.type_at(0));
let ty = self.monomorphize(instance.args.type_at(0));
let dst = fargs.remove(0).cast_to(Type::void_pointer());
let val = fargs.remove(0).cast_to(Type::void_pointer());
let layout = self.layout_of(ty);
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -139,7 +139,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
ConstValue::ZeroSized => match lit_ty.kind() {
// Rust "function items" (not closures, not function pointers, see `codegen_fndef`)
ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span),
ty::FnDef(d, args) => self.codegen_fndef(*d, args, span),
_ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table),
},
}
Expand Down Expand Up @@ -693,11 +693,11 @@ impl<'tcx> GotocCtx<'tcx> {
pub fn codegen_fndef(
&mut self,
d: DefId,
substs: ty::subst::SubstsRef<'tcx>,
args: ty::GenericArgsRef<'tcx>,
span: Option<&Span>,
) -> Expr {
let instance =
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap();
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, args).unwrap().unwrap();
self.codegen_fn_item(instance, span)
}

Expand Down
12 changes: 6 additions & 6 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -368,7 +368,7 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option<Expr> {
match ty.kind() {
// A local that is itself a FnDef, like Fn::call_once
ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)),
ty::FnDef(defid, args) => Some(self.codegen_fndef(*defid, args, None)),
// A local can be pointer to a FnDef, like Fn::call and Fn::call_mut
ty::RawPtr(inner) => self
.codegen_local_fndef(inner.ty)
Expand Down Expand Up @@ -513,14 +513,14 @@ impl<'tcx> GotocCtx<'tcx> {
// https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
match before.mir_typ().kind() {
ty::Array(ty, len) => {
let len = len.kind().try_to_target_usize(self.tcx).unwrap();
let len = len.try_to_target_usize(self.tcx).unwrap();
let subarray_len = if from_end {
// `to` counts from the end of the array
len - to - from
} else {
to - from
};
let typ = self.tcx.mk_array(*ty, subarray_len);
let typ = Ty::new_array(self.tcx, *ty, subarray_len);
let goto_typ = self.codegen_ty(typ);
// unimplemented
Err(UnimplementedData::new(
Expand All @@ -542,9 +542,9 @@ impl<'tcx> GotocCtx<'tcx> {
} else {
Expr::int_constant(to - from, Type::size_t())
};
let typ = self.tcx.mk_slice(*elemt);
let typ = Ty::new_slice(self.tcx, *elemt);
let typ_and_mut = TypeAndMut { ty: typ, mutbl: Mutability::Mut };
let ptr_typ = self.tcx.mk_ptr(typ_and_mut);
let ptr_typ = Ty::new_ptr(self.tcx, typ_and_mut);
let goto_type = self.codegen_ty(ptr_typ);

let index = Expr::int_constant(from, Type::ssize_t());
Expand Down Expand Up @@ -704,7 +704,7 @@ impl<'tcx> GotocCtx<'tcx> {
match before.mir_typ().kind() {
//TODO, ask on zulip if we can ever have from_end here?
ty::Array(elemt, length) => {
let length = length.kind().try_to_target_usize(self.tcx).unwrap();
let length = length.try_to_target_usize(self.tcx).unwrap();
assert!(length >= min_length);
let idx = if from_end { length - offset } else { offset };
let idxe = Expr::int_constant(idx, Type::ssize_t());
Expand Down
40 changes: 18 additions & 22 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use num::bigint::BigInt;
use rustc_abi::FieldIdx;
use rustc_index::IndexVec;
use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
use rustc_middle::ty::adjustment::PointerCast;
use rustc_middle::ty::adjustment::PointerCoercion;
use rustc_middle::ty::layout::LayoutOf;
use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants};
Expand Down Expand Up @@ -706,7 +706,7 @@ impl<'tcx> GotocCtx<'tcx> {
"https://github.com/model-checking/kani/issues/1784",
)
}
Rvalue::Cast(CastKind::Pointer(k), e, t) => {
Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => {
let t = self.monomorphize(*t);
self.codegen_pointer_cast(k, e, t, loc)
}
Expand Down Expand Up @@ -738,7 +738,7 @@ impl<'tcx> GotocCtx<'tcx> {
// See https://github.com/rust-lang/compiler-team/issues/460 for more details.
let operand = self.codegen_operand(operand);
let t = self.monomorphize(*content_ty);
let box_ty = self.tcx.mk_box(t);
let box_ty = Ty::new_box(self.tcx, t);
let box_ty = self.codegen_ty(box_ty);
let cbmc_t = self.codegen_ty(t);
let box_contents = operand.cast_to(cbmc_t.to_pointer());
Expand Down Expand Up @@ -991,22 +991,22 @@ impl<'tcx> GotocCtx<'tcx> {
}

/// "Pointer casts" are particular kinds of pointer-to-pointer casts.
/// See the [`PointerCast`] type for specifics.
/// See the [`PointerCoercion`] type for specifics.
/// Note that this does not include all casts involving pointers,
/// many of which are instead handled by [`Self::codegen_misc_cast`] instead.
fn codegen_pointer_cast(
&mut self,
k: &PointerCast,
k: &PointerCoercion,
operand: &Operand<'tcx>,
t: Ty<'tcx>,
loc: Location,
) -> Expr {
debug!(cast=?k, op=?operand, ?loc, "codegen_pointer_cast");
match k {
PointerCast::ReifyFnPointer => match self.operand_ty(operand).kind() {
ty::FnDef(def_id, substs) => {
PointerCoercion::ReifyFnPointer => match self.operand_ty(operand).kind() {
ty::FnDef(def_id, args) => {
let instance =
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs)
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
.unwrap()
.unwrap();
// We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs.
Expand All @@ -1015,24 +1015,20 @@ impl<'tcx> GotocCtx<'tcx> {
}
_ => unreachable!(),
},
PointerCast::UnsafeFnPointer => self.codegen_operand(operand),
PointerCast::ClosureFnPointer(_) => {
if let ty::Closure(def_id, substs) = self.operand_ty(operand).kind() {
let instance = Instance::resolve_closure(
self.tcx,
*def_id,
substs,
ty::ClosureKind::FnOnce,
)
.expect("failed to normalize and resolve closure during codegen")
.polymorphize(self.tcx);
PointerCoercion::UnsafeFnPointer => self.codegen_operand(operand),
PointerCoercion::ClosureFnPointer(_) => {
if let ty::Closure(def_id, args) = self.operand_ty(operand).kind() {
let instance =
Instance::resolve_closure(self.tcx, *def_id, args, ty::ClosureKind::FnOnce)
.expect("failed to normalize and resolve closure during codegen")
.polymorphize(self.tcx);
self.codegen_func_expr(instance, None).address_of()
} else {
unreachable!("{:?} cannot be cast to a fn ptr", operand)
}
}
PointerCast::MutToConstPointer => self.codegen_operand(operand),
PointerCast::ArrayToPointer => {
PointerCoercion::MutToConstPointer => self.codegen_operand(operand),
PointerCoercion::ArrayToPointer => {
// TODO: I am not sure whether it is correct or not.
//
// some reasoning is as follows.
Expand All @@ -1054,7 +1050,7 @@ impl<'tcx> GotocCtx<'tcx> {
_ => unreachable!(),
}
}
PointerCast::Unsize => {
PointerCoercion::Unsize => {
let src_goto_expr = self.codegen_operand(operand);
let src_mir_type = self.operand_ty(operand);
let dst_mir_type = t;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::Symbol;
use rustc_hir::def_id::DefId;
use rustc_middle::mir::mono::MonoItem;
use rustc_middle::ty::{subst::InternalSubsts, Instance};
use rustc_middle::ty::{GenericArgs, Instance};
use tracing::debug;

impl<'tcx> GotocCtx<'tcx> {
Expand All @@ -28,10 +28,10 @@ impl<'tcx> GotocCtx<'tcx> {
// Unique mangled monomorphized name.
let symbol_name = item.symbol_name(self.tcx).to_string();
// Pretty name which may include function name.
let pretty_name = Instance::new(def_id, InternalSubsts::empty()).to_string();
let pretty_name = Instance::new(def_id, GenericArgs::empty()).to_string();
debug!(?symbol_name, ?pretty_name, "declare_static {}", item);

let typ = self.codegen_ty(self.tcx.type_of(def_id).subst_identity());
let typ = self.codegen_ty(self.tcx.type_of(def_id).instantiate_identity());
let span = self.tcx.def_span(def_id);
let location = self.codegen_span(&span);
let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)
Expand Down
Loading
Loading