Skip to content

Commit

Permalink
Upgrade Rust toolchain to nightly-2024-06-17 (model-checking#3271)
Browse files Browse the repository at this point in the history
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 model-checking#3260
  • Loading branch information
celinval authored Jun 17, 2024
1 parent 44f1878 commit fd013ff
Show file tree
Hide file tree
Showing 11 changed files with 39 additions and 28 deletions.
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ impl<'tcx> GotocCtx<'tcx> {
}
}
Operand::Constant(constant) => {
self.codegen_const(&constant.literal, self.codegen_span_stable(constant.span))
self.codegen_const(&constant.const_, self.codegen_span_stable(constant.span))
}
}
}
Expand Down
8 changes: 4 additions & 4 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ use rustc_smir::rustc_internal;
use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
use stable_mir::mir::{
visit::Location, Body, CastKind, Constant, MirVisitor, PointerCoercion, Rvalue, Terminator,
visit::Location, Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator,
TerminatorKind,
};
use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
Expand Down Expand Up @@ -375,9 +375,9 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
}

/// Collect constants that are represented as static variables.
fn visit_constant(&mut self, constant: &Constant, location: Location) {
debug!(?constant, ?location, literal=?constant.literal, "visit_constant");
let allocation = match constant.literal.kind() {
fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
debug!(?constant, ?location, literal=?constant.const_, "visit_constant");
let allocation = match constant.const_.kind() {
ConstantKind::Allocated(allocation) => allocation,
ConstantKind::Unevaluated(_) => {
unreachable!("Instance with polymorphic constant: `{constant:?}`")
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/stubbing/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable};
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::visit::{Location, MirVisitor};
use stable_mir::mir::Constant;
use stable_mir::mir::ConstOperand;
use stable_mir::ty::{FnDef, RigidTy, TyKind};
use stable_mir::{CrateDef, CrateItem};

Expand Down Expand Up @@ -185,8 +185,8 @@ impl<'tcx> StubConstChecker<'tcx> {

impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
/// Collect constants that are represented as static variables.
fn visit_constant(&mut self, constant: &Constant, location: Location) {
let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.literal));
fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.const_));
debug!(?constant, ?location, ?const_, "visit_constant");
match const_ {
Const::Val(..) | Const::Ty(..) => {}
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/transform/body.rs
Original file line number Diff line number Diff line change
Expand Up @@ -81,12 +81,12 @@ impl MutableBody {

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

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

/// Create a raw pointer of `*mut type` and return a new local where that value is stored.
Expand Down
6 changes: 3 additions & 3 deletions kani-compiler/src/kani_middle/transform/check_values.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape,
use stable_mir::mir::mono::{Instance, InstanceKind};
use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
use stable_mir::mir::{
AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, Constant, FieldIdx, Local, LocalDecl,
AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl,
MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue,
Statement, StatementKind, Terminator, TerminatorKind,
};
Expand Down Expand Up @@ -118,8 +118,8 @@ impl ValidValuePass {
reason: &str,
) {
let span = source.span(body.blocks());
let rvalue = Rvalue::Use(Operand::Constant(Constant {
literal: MirConst::from_bool(false),
let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
const_: MirConst::from_bool(false),
span,
user_ty: None,
}));
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/kani_middle/transform/contracts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use cbmc::{InternString, InternedString};
use rustc_middle::ty::TyCtxt;
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{Body, Constant, Operand, TerminatorKind};
use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind};
use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
use stable_mir::{CrateDef, DefId};
use std::collections::HashSet;
Expand Down Expand Up @@ -113,7 +113,7 @@ impl AnyModifiesPass {
let instance = Instance::resolve(self.kani_any.unwrap(), &instance_args).unwrap();
let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
let span = bb.terminator.span;
let new_func = Constant { span, user_ty: None, literal };
let new_func = ConstOperand { span, user_ty: None, const_: literal };
*func = Operand::Constant(new_func);
changed = true;
}
Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ use crate::kani_queries::QueryDb;
use rustc_middle::ty::TyCtxt;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{
BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
};
use stable_mir::target::MachineInfo;
use stable_mir::ty::{MirConst, RigidTy, TyKind};
Expand Down Expand Up @@ -79,10 +79,10 @@ impl IntrinsicGeneratorPass {
let span = new_body.locals()[ret_var].span;
let assign = StatementKind::Assign(
Place::from(ret_var),
Rvalue::Use(Operand::Constant(Constant {
Rvalue::Use(Operand::Constant(ConstOperand {
span,
user_ty: None,
literal: MirConst::from_bool(true),
const_: MirConst::from_bool(true),
})),
);
let stmt = Statement { kind: assign, span };
Expand Down Expand Up @@ -115,8 +115,8 @@ impl IntrinsicGeneratorPass {
}
Err(msg) => {
// We failed to retrieve all the valid ranges.
let rvalue = Rvalue::Use(Operand::Constant(Constant {
literal: MirConst::from_bool(false),
let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
const_: MirConst::from_bool(false),
span,
user_ty: None,
}));
Expand Down
8 changes: 4 additions & 4 deletions kani-compiler/src/kani_middle/transform/stubs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use rustc_middle::ty::TyCtxt;
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::visit::{Location, MirVisitor};
use stable_mir::mir::{Body, Constant, LocalDecl, Operand, Terminator, TerminatorKind};
use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
use stable_mir::CrateDef;
use std::collections::HashMap;
Expand Down Expand Up @@ -199,7 +199,7 @@ impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
let instance = Instance::resolve(*new_def, &args).unwrap();
let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
let span = term.span;
let new_func = Constant { span, user_ty: None, literal };
let new_func = ConstOperand { span, user_ty: None, const_: literal };
*func = Operand::Constant(new_func);
self.changed = true;
}
Expand All @@ -212,12 +212,12 @@ impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
let func_ty = operand.ty(&self.locals).unwrap();
if let TyKind::RigidTy(RigidTy::FnDef(orig_def, args)) = func_ty.kind() {
if let Some(new_def) = self.stubs.get(&orig_def) {
let Operand::Constant(Constant { span, .. }) = operand else {
let Operand::Constant(ConstOperand { span, .. }) = operand else {
unreachable!();
};
let instance = Instance::resolve_for_fn_ptr(*new_def, &args).unwrap();
let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
let new_func = Constant { span: *span, user_ty: None, literal };
let new_func = ConstOperand { span: *span, user_ty: None, const_: literal };
*operand = Operand::Constant(new_func);
self.changed = true;
}
Expand Down
4 changes: 4 additions & 0 deletions kani-driver/src/call_single_file.rs
Original file line number Diff line number Diff line change
Expand Up @@ -184,6 +184,10 @@ impl KaniSession {
}
}

if self.args.coverage {
flags.push("-Zmir-enable-passes=-SingleUseConsts".into());
}

// This argument will select the Kani flavour of the compiler. It will be removed before
// rustc driver is invoked.
flags.push("--kani-compiler".into());
Expand Down
4 changes: 2 additions & 2 deletions rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2024-06-11"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
channel = "nightly-2024-06-17"
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
11 changes: 9 additions & 2 deletions scripts/kani-regression.sh
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,8 @@ check_kissat_version.sh
# Formatting check
${SCRIPT_DIR}/kani-fmt.sh --check

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

# Unit tests
cargo test -p cprover_bindings
Expand Down Expand Up @@ -102,6 +102,13 @@ FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.tom
cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success
cargo clean --manifest-path "$FEATURES_MANIFEST_PATH"

# Build all packages in the workspace and ensure no warning is emitted.
# Please don't replace `cargo build-dev` above with this command.
# Setting RUSTFLAGS like this always resets cargo's build cache resulting in
# all tests to be re-run. I.e., cannot keep re-runing the regression from where
# we stopped.
RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings

echo
echo "All Kani regression tests completed successfully."
echo

0 comments on commit fd013ff

Please sign in to comment.