diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 4c45b475a3a7..555fc43b8999 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -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)) } } } diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 4ebff6868bf5..279dcf8cc107 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -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}; @@ -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:?}`") diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index f21a02b7681e..f145a4d105e2 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -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}; @@ -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(..) => {} diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index e058c5aedc98..2bf424a1332d 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -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. diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index c7c9548bd609..4ecb16fab023 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -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, }; @@ -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, })); diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 10fa6775a0d9..f5760bd4d829 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -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; @@ -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; } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 053b210babb0..53bbd52086ac 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -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}; @@ -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 }; @@ -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, })); diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 53db34dc902f..4f249afdd45a 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -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; @@ -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; } @@ -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; } diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 29128a02dc2a..7992543cdaa1 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -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()); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index d1baa70550de..eeabc79dd980 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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"] diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index d3bb0f7efb45..b1de293d533c 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -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 @@ -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