Skip to content

Commit fd013ff

Browse files
authored
Upgrade Rust toolchain to nightly-2024-06-17 (#3271)
Related changes: - rust-lang/rust#125910: Introduces a new constant propagation pass which broke Kani coverage tests. For now, disable this pass if coverage is enabled. - rust-lang/rust#126410: Rename ConstOperands Resolves #3260
1 parent 44f1878 commit fd013ff

File tree

11 files changed

+39
-28
lines changed

11 files changed

+39
-28
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ impl<'tcx> GotocCtx<'tcx> {
5353
}
5454
}
5555
Operand::Constant(constant) => {
56-
self.codegen_const(&constant.literal, self.codegen_span_stable(constant.span))
56+
self.codegen_const(&constant.const_, self.codegen_span_stable(constant.span))
5757
}
5858
}
5959
}

kani-compiler/src/kani_middle/reachability.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ use rustc_smir::rustc_internal;
2626
use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
2727
use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
2828
use stable_mir::mir::{
29-
visit::Location, Body, CastKind, Constant, MirVisitor, PointerCoercion, Rvalue, Terminator,
29+
visit::Location, Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator,
3030
TerminatorKind,
3131
};
3232
use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
@@ -375,9 +375,9 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
375375
}
376376

377377
/// Collect constants that are represented as static variables.
378-
fn visit_constant(&mut self, constant: &Constant, location: Location) {
379-
debug!(?constant, ?location, literal=?constant.literal, "visit_constant");
380-
let allocation = match constant.literal.kind() {
378+
fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
379+
debug!(?constant, ?location, literal=?constant.const_, "visit_constant");
380+
let allocation = match constant.const_.kind() {
381381
ConstantKind::Allocated(allocation) => allocation,
382382
ConstantKind::Unevaluated(_) => {
383383
unreachable!("Instance with polymorphic constant: `{constant:?}`")

kani-compiler/src/kani_middle/stubbing/mod.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable};
1616
use rustc_smir::rustc_internal;
1717
use stable_mir::mir::mono::Instance;
1818
use stable_mir::mir::visit::{Location, MirVisitor};
19-
use stable_mir::mir::Constant;
19+
use stable_mir::mir::ConstOperand;
2020
use stable_mir::ty::{FnDef, RigidTy, TyKind};
2121
use stable_mir::{CrateDef, CrateItem};
2222

@@ -185,8 +185,8 @@ impl<'tcx> StubConstChecker<'tcx> {
185185

186186
impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
187187
/// Collect constants that are represented as static variables.
188-
fn visit_constant(&mut self, constant: &Constant, location: Location) {
189-
let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.literal));
188+
fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
189+
let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.const_));
190190
debug!(?constant, ?location, ?const_, "visit_constant");
191191
match const_ {
192192
Const::Val(..) | Const::Ty(..) => {}

kani-compiler/src/kani_middle/transform/body.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -81,12 +81,12 @@ impl MutableBody {
8181

8282
pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand {
8383
let literal = MirConst::from_str(msg);
84-
Operand::Constant(Constant { span, user_ty: None, literal })
84+
Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
8585
}
8686

8787
pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
8888
let literal = MirConst::try_from_uint(val, uint_ty).unwrap();
89-
Operand::Constant(Constant { span, user_ty: None, literal })
89+
Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
9090
}
9191

9292
/// Create a raw pointer of `*mut type` and return a new local where that value is stored.

kani-compiler/src/kani_middle/transform/check_values.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape,
2424
use stable_mir::mir::mono::{Instance, InstanceKind};
2525
use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
2626
use stable_mir::mir::{
27-
AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, Constant, FieldIdx, Local, LocalDecl,
27+
AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl,
2828
MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue,
2929
Statement, StatementKind, Terminator, TerminatorKind,
3030
};
@@ -118,8 +118,8 @@ impl ValidValuePass {
118118
reason: &str,
119119
) {
120120
let span = source.span(body.blocks());
121-
let rvalue = Rvalue::Use(Operand::Constant(Constant {
122-
literal: MirConst::from_bool(false),
121+
let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
122+
const_: MirConst::from_bool(false),
123123
span,
124124
user_ty: None,
125125
}));

kani-compiler/src/kani_middle/transform/contracts.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use cbmc::{InternString, InternedString};
1010
use rustc_middle::ty::TyCtxt;
1111
use rustc_smir::rustc_internal;
1212
use stable_mir::mir::mono::Instance;
13-
use stable_mir::mir::{Body, Constant, Operand, TerminatorKind};
13+
use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind};
1414
use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
1515
use stable_mir::{CrateDef, DefId};
1616
use std::collections::HashSet;
@@ -113,7 +113,7 @@ impl AnyModifiesPass {
113113
let instance = Instance::resolve(self.kani_any.unwrap(), &instance_args).unwrap();
114114
let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
115115
let span = bb.terminator.span;
116-
let new_func = Constant { span, user_ty: None, literal };
116+
let new_func = ConstOperand { span, user_ty: None, const_: literal };
117117
*func = Operand::Constant(new_func);
118118
changed = true;
119119
}

kani-compiler/src/kani_middle/transform/kani_intrinsics.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ use crate::kani_queries::QueryDb;
1515
use rustc_middle::ty::TyCtxt;
1616
use stable_mir::mir::mono::Instance;
1717
use stable_mir::mir::{
18-
BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
18+
BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
1919
};
2020
use stable_mir::target::MachineInfo;
2121
use stable_mir::ty::{MirConst, RigidTy, TyKind};
@@ -79,10 +79,10 @@ impl IntrinsicGeneratorPass {
7979
let span = new_body.locals()[ret_var].span;
8080
let assign = StatementKind::Assign(
8181
Place::from(ret_var),
82-
Rvalue::Use(Operand::Constant(Constant {
82+
Rvalue::Use(Operand::Constant(ConstOperand {
8383
span,
8484
user_ty: None,
85-
literal: MirConst::from_bool(true),
85+
const_: MirConst::from_bool(true),
8686
})),
8787
);
8888
let stmt = Statement { kind: assign, span };
@@ -115,8 +115,8 @@ impl IntrinsicGeneratorPass {
115115
}
116116
Err(msg) => {
117117
// We failed to retrieve all the valid ranges.
118-
let rvalue = Rvalue::Use(Operand::Constant(Constant {
119-
literal: MirConst::from_bool(false),
118+
let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
119+
const_: MirConst::from_bool(false),
120120
span,
121121
user_ty: None,
122122
}));

kani-compiler/src/kani_middle/transform/stubs.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ use rustc_middle::ty::TyCtxt;
1111
use rustc_smir::rustc_internal;
1212
use stable_mir::mir::mono::Instance;
1313
use stable_mir::mir::visit::{Location, MirVisitor};
14-
use stable_mir::mir::{Body, Constant, LocalDecl, Operand, Terminator, TerminatorKind};
14+
use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
1515
use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
1616
use stable_mir::CrateDef;
1717
use std::collections::HashMap;
@@ -199,7 +199,7 @@ impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
199199
let instance = Instance::resolve(*new_def, &args).unwrap();
200200
let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
201201
let span = term.span;
202-
let new_func = Constant { span, user_ty: None, literal };
202+
let new_func = ConstOperand { span, user_ty: None, const_: literal };
203203
*func = Operand::Constant(new_func);
204204
self.changed = true;
205205
}
@@ -212,12 +212,12 @@ impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
212212
let func_ty = operand.ty(&self.locals).unwrap();
213213
if let TyKind::RigidTy(RigidTy::FnDef(orig_def, args)) = func_ty.kind() {
214214
if let Some(new_def) = self.stubs.get(&orig_def) {
215-
let Operand::Constant(Constant { span, .. }) = operand else {
215+
let Operand::Constant(ConstOperand { span, .. }) = operand else {
216216
unreachable!();
217217
};
218218
let instance = Instance::resolve_for_fn_ptr(*new_def, &args).unwrap();
219219
let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
220-
let new_func = Constant { span: *span, user_ty: None, literal };
220+
let new_func = ConstOperand { span: *span, user_ty: None, const_: literal };
221221
*operand = Operand::Constant(new_func);
222222
self.changed = true;
223223
}

kani-driver/src/call_single_file.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -184,6 +184,10 @@ impl KaniSession {
184184
}
185185
}
186186

187+
if self.args.coverage {
188+
flags.push("-Zmir-enable-passes=-SingleUseConsts".into());
189+
}
190+
187191
// This argument will select the Kani flavour of the compiler. It will be removed before
188192
// rustc driver is invoked.
189193
flags.push("--kani-compiler".into());

rust-toolchain.toml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2024-06-11"
6-
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
5+
channel = "nightly-2024-06-17"
6+
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

scripts/kani-regression.sh

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,8 @@ check_kissat_version.sh
3333
# Formatting check
3434
${SCRIPT_DIR}/kani-fmt.sh --check
3535

36-
# Build all packages in the workspace and ensure no warning is emitted.
37-
RUSTFLAGS="-D warnings" cargo build-dev
36+
# Build kani
37+
cargo build-dev
3838

3939
# Unit tests
4040
cargo test -p cprover_bindings
@@ -102,6 +102,13 @@ FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.tom
102102
cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success
103103
cargo clean --manifest-path "$FEATURES_MANIFEST_PATH"
104104

105+
# Build all packages in the workspace and ensure no warning is emitted.
106+
# Please don't replace `cargo build-dev` above with this command.
107+
# Setting RUSTFLAGS like this always resets cargo's build cache resulting in
108+
# all tests to be re-run. I.e., cannot keep re-runing the regression from where
109+
# we stopped.
110+
RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings
111+
105112
echo
106113
echo "All Kani regression tests completed successfully."
107114
echo

0 commit comments

Comments
 (0)