Skip to content

Commit 63f513f

Browse files
remi-delmas-3000Remi Delmasadpaco-aws
authored
Update toolchain to nightly 2023-08-04 (rust-lang#2661)
Co-authored-by: Remi Delmas <delmasrd@amazon.com> Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
1 parent 9a9e815 commit 63f513f

File tree

22 files changed

+154
-145
lines changed

22 files changed

+154
-145
lines changed

‎cprover_bindings/src/goto_program/expr.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1410,7 +1410,7 @@ impl Expr {
14101410
ArithmeticOverflowResult { result, overflowed }
14111411
}
14121412

1413-
/// Uses CBMC's [binop]-with-overflow operation that performs a single arithmetic
1413+
/// Uses CBMC's \[binop\]-with-overflow operation that performs a single arithmetic
14141414
/// operation
14151415
/// `struct (T, bool) overflow(binop, self, e)` where `T` is the type of `self`
14161416
/// Pseudocode:

‎kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -110,16 +110,15 @@ impl<'tcx> GotocCtx<'tcx> {
110110
.args
111111
.iter()
112112
.enumerate()
113-
.filter_map(|(idx, arg)| {
114-
(!arg.is_ignore()).then(|| {
115-
let arg_name = format!("{fn_name}::param_{idx}");
116-
let base_name = format!("param_{idx}");
117-
let arg_type = self.codegen_ty(arg.layout.ty);
118-
let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
119-
.with_is_parameter(true);
120-
self.symbol_table.insert(sym);
121-
arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
122-
})
113+
.filter(|&(_, arg)| (!arg.is_ignore()))
114+
.map(|(idx, arg)| {
115+
let arg_name = format!("{fn_name}::param_{idx}");
116+
let base_name = format!("param_{idx}");
117+
let arg_type = self.codegen_ty(arg.layout.ty);
118+
let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
119+
.with_is_parameter(true);
120+
self.symbol_table.insert(sym);
121+
arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
123122
})
124123
.collect();
125124
let ret_type = self.codegen_ty(fn_abi.ret.layout.ty);

‎kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,7 @@ impl<'tcx> GotocCtx<'tcx> {
187187

188188
let tupe = sig.inputs().last().unwrap();
189189
let args = match tupe.kind() {
190-
ty::Tuple(substs) => *substs,
190+
ty::Tuple(args) => *args,
191191
_ => unreachable!("a function's spread argument must be a tuple"),
192192
};
193193
let starting_idx = sig.inputs().len();

‎kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -245,7 +245,7 @@ impl<'tcx> GotocCtx<'tcx> {
245245

246246
macro_rules! codegen_size_align {
247247
($which: ident) => {{
248-
let tp_ty = instance.substs.type_at(0);
248+
let tp_ty = instance.args.type_at(0);
249249
let arg = fargs.remove(0);
250250
let size_align = self.size_and_align_of_dst(tp_ty, arg);
251251
self.codegen_expr_to_place(p, size_align.$which)
@@ -422,7 +422,7 @@ impl<'tcx> GotocCtx<'tcx> {
422422
"cttz" => codegen_count_intrinsic!(cttz, true),
423423
"cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
424424
"discriminant_value" => {
425-
let ty = instance.substs.type_at(0);
425+
let ty = instance.args.type_at(0);
426426
let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
427427
self.codegen_expr_to_place(p, e)
428428
}
@@ -764,7 +764,7 @@ impl<'tcx> GotocCtx<'tcx> {
764764
intrinsic: &str,
765765
span: Option<Span>,
766766
) -> Stmt {
767-
let ty = instance.substs.type_at(0);
767+
let ty = instance.args.type_at(0);
768768
let layout = self.layout_of(ty);
769769
// Note: We follow the pattern seen in `codegen_panic_intrinsic` from `rustc_codegen_ssa`
770770
// https://github.com/rust-lang/rust/blob/master/compiler/rustc_codegen_ssa/src/mir/block.rs
@@ -1034,7 +1034,7 @@ impl<'tcx> GotocCtx<'tcx> {
10341034
let offset = fargs.remove(0);
10351035

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

@@ -1184,7 +1184,7 @@ impl<'tcx> GotocCtx<'tcx> {
11841184
p: &Place<'tcx>,
11851185
loc: Location,
11861186
) -> Stmt {
1187-
let ty = self.monomorphize(instance.substs.type_at(0));
1187+
let ty = self.monomorphize(instance.args.type_at(0));
11881188
let dst = fargs.remove(0).cast_to(Type::void_pointer());
11891189
let val = fargs.remove(0).cast_to(Type::void_pointer());
11901190
let layout = self.layout_of(ty);

‎kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,7 @@ impl<'tcx> GotocCtx<'tcx> {
139139
}
140140
ConstValue::ZeroSized => match lit_ty.kind() {
141141
// Rust "function items" (not closures, not function pointers, see `codegen_fndef`)
142-
ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span),
142+
ty::FnDef(d, args) => self.codegen_fndef(*d, args, span),
143143
_ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table),
144144
},
145145
}
@@ -693,11 +693,11 @@ impl<'tcx> GotocCtx<'tcx> {
693693
pub fn codegen_fndef(
694694
&mut self,
695695
d: DefId,
696-
substs: ty::subst::SubstsRef<'tcx>,
696+
args: ty::GenericArgsRef<'tcx>,
697697
span: Option<&Span>,
698698
) -> Expr {
699699
let instance =
700-
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap();
700+
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, args).unwrap().unwrap();
701701
self.codegen_fn_item(instance, span)
702702
}
703703

‎kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -368,7 +368,7 @@ impl<'tcx> GotocCtx<'tcx> {
368368
fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option<Expr> {
369369
match ty.kind() {
370370
// A local that is itself a FnDef, like Fn::call_once
371-
ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)),
371+
ty::FnDef(defid, args) => Some(self.codegen_fndef(*defid, args, None)),
372372
// A local can be pointer to a FnDef, like Fn::call and Fn::call_mut
373373
ty::RawPtr(inner) => self
374374
.codegen_local_fndef(inner.ty)
@@ -513,14 +513,14 @@ impl<'tcx> GotocCtx<'tcx> {
513513
// https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
514514
match before.mir_typ().kind() {
515515
ty::Array(ty, len) => {
516-
let len = len.kind().try_to_target_usize(self.tcx).unwrap();
516+
let len = len.try_to_target_usize(self.tcx).unwrap();
517517
let subarray_len = if from_end {
518518
// `to` counts from the end of the array
519519
len - to - from
520520
} else {
521521
to - from
522522
};
523-
let typ = self.tcx.mk_array(*ty, subarray_len);
523+
let typ = Ty::new_array(self.tcx, *ty, subarray_len);
524524
let goto_typ = self.codegen_ty(typ);
525525
// unimplemented
526526
Err(UnimplementedData::new(
@@ -542,9 +542,9 @@ impl<'tcx> GotocCtx<'tcx> {
542542
} else {
543543
Expr::int_constant(to - from, Type::size_t())
544544
};
545-
let typ = self.tcx.mk_slice(*elemt);
545+
let typ = Ty::new_slice(self.tcx, *elemt);
546546
let typ_and_mut = TypeAndMut { ty: typ, mutbl: Mutability::Mut };
547-
let ptr_typ = self.tcx.mk_ptr(typ_and_mut);
547+
let ptr_typ = Ty::new_ptr(self.tcx, typ_and_mut);
548548
let goto_type = self.codegen_ty(ptr_typ);
549549

550550
let index = Expr::int_constant(from, Type::ssize_t());
@@ -704,7 +704,7 @@ impl<'tcx> GotocCtx<'tcx> {
704704
match before.mir_typ().kind() {
705705
//TODO, ask on zulip if we can ever have from_end here?
706706
ty::Array(elemt, length) => {
707-
let length = length.kind().try_to_target_usize(self.tcx).unwrap();
707+
let length = length.try_to_target_usize(self.tcx).unwrap();
708708
assert!(length >= min_length);
709709
let idx = if from_end { length - offset } else { offset };
710710
let idxe = Expr::int_constant(idx, Type::ssize_t());

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 18 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ use num::bigint::BigInt;
2020
use rustc_abi::FieldIdx;
2121
use rustc_index::IndexVec;
2222
use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
23-
use rustc_middle::ty::adjustment::PointerCast;
23+
use rustc_middle::ty::adjustment::PointerCoercion;
2424
use rustc_middle::ty::layout::LayoutOf;
2525
use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
2626
use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants};
@@ -706,7 +706,7 @@ impl<'tcx> GotocCtx<'tcx> {
706706
"https://github.com/model-checking/kani/issues/1784",
707707
)
708708
}
709-
Rvalue::Cast(CastKind::Pointer(k), e, t) => {
709+
Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => {
710710
let t = self.monomorphize(*t);
711711
self.codegen_pointer_cast(k, e, t, loc)
712712
}
@@ -738,7 +738,7 @@ impl<'tcx> GotocCtx<'tcx> {
738738
// See https://github.com/rust-lang/compiler-team/issues/460 for more details.
739739
let operand = self.codegen_operand(operand);
740740
let t = self.monomorphize(*content_ty);
741-
let box_ty = self.tcx.mk_box(t);
741+
let box_ty = Ty::new_box(self.tcx, t);
742742
let box_ty = self.codegen_ty(box_ty);
743743
let cbmc_t = self.codegen_ty(t);
744744
let box_contents = operand.cast_to(cbmc_t.to_pointer());
@@ -991,22 +991,22 @@ impl<'tcx> GotocCtx<'tcx> {
991991
}
992992

993993
/// "Pointer casts" are particular kinds of pointer-to-pointer casts.
994-
/// See the [`PointerCast`] type for specifics.
994+
/// See the [`PointerCoercion`] type for specifics.
995995
/// Note that this does not include all casts involving pointers,
996996
/// many of which are instead handled by [`Self::codegen_misc_cast`] instead.
997997
fn codegen_pointer_cast(
998998
&mut self,
999-
k: &PointerCast,
999+
k: &PointerCoercion,
10001000
operand: &Operand<'tcx>,
10011001
t: Ty<'tcx>,
10021002
loc: Location,
10031003
) -> Expr {
10041004
debug!(cast=?k, op=?operand, ?loc, "codegen_pointer_cast");
10051005
match k {
1006-
PointerCast::ReifyFnPointer => match self.operand_ty(operand).kind() {
1007-
ty::FnDef(def_id, substs) => {
1006+
PointerCoercion::ReifyFnPointer => match self.operand_ty(operand).kind() {
1007+
ty::FnDef(def_id, args) => {
10081008
let instance =
1009-
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs)
1009+
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
10101010
.unwrap()
10111011
.unwrap();
10121012
// We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs.
@@ -1015,24 +1015,20 @@ impl<'tcx> GotocCtx<'tcx> {
10151015
}
10161016
_ => unreachable!(),
10171017
},
1018-
PointerCast::UnsafeFnPointer => self.codegen_operand(operand),
1019-
PointerCast::ClosureFnPointer(_) => {
1020-
if let ty::Closure(def_id, substs) = self.operand_ty(operand).kind() {
1021-
let instance = Instance::resolve_closure(
1022-
self.tcx,
1023-
*def_id,
1024-
substs,
1025-
ty::ClosureKind::FnOnce,
1026-
)
1027-
.expect("failed to normalize and resolve closure during codegen")
1028-
.polymorphize(self.tcx);
1018+
PointerCoercion::UnsafeFnPointer => self.codegen_operand(operand),
1019+
PointerCoercion::ClosureFnPointer(_) => {
1020+
if let ty::Closure(def_id, args) = self.operand_ty(operand).kind() {
1021+
let instance =
1022+
Instance::resolve_closure(self.tcx, *def_id, args, ty::ClosureKind::FnOnce)
1023+
.expect("failed to normalize and resolve closure during codegen")
1024+
.polymorphize(self.tcx);
10291025
self.codegen_func_expr(instance, None).address_of()
10301026
} else {
10311027
unreachable!("{:?} cannot be cast to a fn ptr", operand)
10321028
}
10331029
}
1034-
PointerCast::MutToConstPointer => self.codegen_operand(operand),
1035-
PointerCast::ArrayToPointer => {
1030+
PointerCoercion::MutToConstPointer => self.codegen_operand(operand),
1031+
PointerCoercion::ArrayToPointer => {
10361032
// TODO: I am not sure whether it is correct or not.
10371033
//
10381034
// some reasoning is as follows.
@@ -1054,7 +1050,7 @@ impl<'tcx> GotocCtx<'tcx> {
10541050
_ => unreachable!(),
10551051
}
10561052
}
1057-
PointerCast::Unsize => {
1053+
PointerCoercion::Unsize => {
10581054
let src_goto_expr = self.codegen_operand(operand);
10591055
let src_mir_type = self.operand_ty(operand);
10601056
let dst_mir_type = t;

‎kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
77
use cbmc::goto_program::Symbol;
88
use rustc_hir::def_id::DefId;
99
use rustc_middle::mir::mono::MonoItem;
10-
use rustc_middle::ty::{subst::InternalSubsts, Instance};
10+
use rustc_middle::ty::{GenericArgs, Instance};
1111
use tracing::debug;
1212

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

34-
let typ = self.codegen_ty(self.tcx.type_of(def_id).subst_identity());
34+
let typ = self.codegen_ty(self.tcx.type_of(def_id).instantiate_identity());
3535
let span = self.tcx.def_span(def_id);
3636
let location = self.codegen_span(&span);
3737
let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)

0 commit comments

Comments
 (0)