Merge branch 'main' into attr-invariant

.github/workflows/release.yml

@@ -108,7 +108,7 @@ jobs:
             build-essential bash-completion curl lsb-release sudo g++ gcc flex \
             bison make patch git python3.7 python3.7-dev python3.7-distutils
           update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1
-          curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py
+          curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py
           python3 get-pip.py --force-reinstall
           rm get-pip.py
 
@@ -410,7 +410,7 @@ jobs:
           OWNER: '${{ github.repository_owner }}'
 
       - name: Build and push
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           file: scripts/ci/Dockerfile.bundle-release-20-04

Cargo.lock

@@ -140,19 +140,19 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "clap"
-version = "4.5.6"
+version = "4.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a9689a29b593160de5bc4aacab7b5d54fb52231de70122626c178e6a368994c7"
+checksum = "5db83dced34638ad474f39f250d7fea9598bdd239eaced1bdf45d597da0f433f"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.6"
+version = "4.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2e5387378c84f6faa26890ebf9f0a92989f8873d4d380467bcd0d8d8620424df"
+checksum = "f7e204572485eb3fbf28f871612191521df159bc3e15a9f5064c66dba3a8c05f"
 dependencies = [
  "anstream",
  "anstyle",
@@ -551,9 +551,9 @@ dependencies = [
 
 [[package]]
 name = "memchr"
-version = "2.7.2"
+version = "2.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6c8640c5d730cb13ebd907d8d04b52f55ac9a2eec55b440c8892f40d56c76c1d"
+checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
 
 [[package]]
 name = "memuse"
@@ -801,9 +801,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.1"
+version = "0.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "469052894dcb553421e483e4209ee581a45100d31b4018de03e5a7ad86374a7e"
+checksum = "c82cf8cff14456045f55ec4241383baeff27af886adb72ffb2162f99911de0fd"
 dependencies = [
  "bitflags",
 ]

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))
             }
         }
     }

kani-compiler/src/kani_middle/mod.rs

@@ -105,7 +105,10 @@ pub fn dump_mir_items(
         match item {
             // Exclude FnShims and others that cannot be dumped.
             MonoItem::Fn(instance) => Some(*instance),
-            MonoItem::Static(def) => Some((*def).into()),
+            MonoItem::Static(def) => {
+                let instance: Instance = (*def).into();
+                instance.has_body().then_some(instance)
+            }
             MonoItem::GlobalAsm(_) => None,
         }
     }

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:?}`")

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(..) => {}

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.

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,
         }));

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;
             }

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,
                 }));

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;
             }

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());

library/kani/src/contracts.rs

@@ -225,4 +225,27 @@
 //! Rust pointer type (`&T`, `&mut T`, `*const T` or `*mut T`). In addition `T`
 //! must implement [`Arbitrary`](super::Arbitrary). This is used to assign
 //! `kani::any()` to the location when the function is used in a `stub_verified`.
+//!
+//! ## History Expressions
+//!
+//! Additionally, an ensures clause is allowed to refer to the state of the function arguments before function execution and perform simple computations on them
+//! via an `old` monad. Any instance of `old(computation)` will evaluate the
+//! computation before the function is called. It is required that this computation
+//! is effect free and closed with respect to the function arguments.
+//!
+//! For example, the following code passes kani tests:
+//!
+//! ```
+//! #[kani::modifies(a)]
+//! #[kani::ensures(|result| old(*a).wrapping_add(1) == *a)]
+//! #[kani::ensures(|result : &u32| old(*a).wrapping_add(1) == *result)]
+//! fn add1(a : &mut u32) -> u32 {
+//!     *a=a.wrapping_add(1);
+//!     *a
+//! }
+//! ```
+//!
+//! Here, the value stored in `a` is precomputed and remembered after the function
+//! is called, even though the contents of `a` changed during the function execution.
+//!
 pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified};

library/kani_macros/Cargo.toml

@@ -15,7 +15,7 @@ proc-macro = true
 proc-macro2 = "1.0"
 proc-macro-error = "1.0.4"
 quote = "1.0.20"
-syn = { version = "2.0.18", features = ["full", "visit-mut", "visit"] }
+syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-traits"] }
 
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.

library/kani_macros/src/sysroot/contracts/check.rs

@@ -9,7 +9,7 @@ use syn::{Expr, FnArg, ItemFn, Token};
 
 use super::{
     helpers::*,
-    shared::{make_unsafe_argument_copies, try_as_result_assign_mut},
+    shared::{build_ensures, try_as_result_assign_mut},
     ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
 };
 
@@ -33,14 +33,13 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#inner)*
                 )
             }
-            ContractConditionsData::Ensures { argument_names, attr } => {
-                let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names);
+            ContractConditionsData::Ensures { attr } => {
+                let (remembers, ensures_clause) = build_ensures(attr);
 
                 // The code that enforces the postconditions and cleans up the shallow
                 // argument copies (with `mem::forget`).
                 let exec_postconditions = quote!(
-                    kani::assert(#attr, stringify!(#attr_copy));
-                    #copy_clean
+                    kani::assert(#ensures_clause, stringify!(#attr_copy));
                 );
 
                 assert!(matches!(
@@ -51,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> {
 
                 let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
                 quote!(
-                    #arg_copies
+                    #remembers
                     #(#inner)*
                     #exec_postconditions
                     #result

library/kani_macros/src/sysroot/contracts/helpers.rs

@@ -268,3 +268,21 @@ pub fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 {
     let long_hash = hasher.finish();
     long_hash % SIX_HEX_DIGITS_MASK
 }
+
+macro_rules! assert_spanned_err {
+    ($condition:expr, $span_source:expr, $msg:expr, $($args:expr),+) => {
+        if !$condition {
+            $span_source.span().unwrap().error(format!($msg, $($args),*)).emit();
+            assert!(false);
+        }
+    };
+    ($condition:expr, $span_source:expr, $msg:expr $(,)?) => {
+        if !$condition {
+            $span_source.span().unwrap().error($msg).emit();
+            assert!(false);
+        }
+    };
+    ($condition:expr, $span_source:expr) => {
+        assert_spanned_err!($condition, $span_source, concat!("Failed assertion ", stringify!($condition)))
+    };
+}