Skip to content

Commit

Permalink
Update toolchain to nightly 2023-08-04 (#2661)
Browse files Browse the repository at this point in the history
Co-authored-by: Remi Delmas <delmasrd@amazon.com>
Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
  • Loading branch information
3 people authored Aug 8, 2023
1 parent 9a9e815 commit 63f513f
Show file tree
Hide file tree
Showing 22 changed files with 154 additions and 145 deletions.
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
6 changes: 3 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
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

0 comments on commit 63f513f

Please sign in to comment.