From c2dc48939ce2863dbb223cd68e671f7d8d3415f9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 26 Feb 2024 08:34:07 -0800 Subject: [PATCH] Upgrade rust toolchain to 2024-02-17 (#3040) Upgrade toolchain to 2024-02-17. Relevant PR: - https://github.com/rust-lang/rust/pull/120500 - https://github.com/rust-lang/rust/pull/100603 Fixes https://github.com/model-checking/kani/issues/87 Fixes https://github.com/model-checking/kani/issues/3034 Fixes https://github.com/model-checking/kani/issues/3037 --- .../codegen/intrinsic.rs | 25 +--- .../codegen_cprover_gotoc/codegen/operand.rs | 11 ++ .../codegen/statement.rs | 110 ++++++++++-------- .../codegen/ty_stable.rs | 5 + .../src/codegen_cprover_gotoc/codegen/typ.rs | 39 +------ kani-compiler/src/kani_middle/intrinsics.rs | 4 +- kani-compiler/src/main.rs | 1 + rust-toolchain.toml | 2 +- tests/kani/Closure/zst_unwrap.rs | 16 +++ tests/kani/SizeAndAlignOfDst/main_assert.rs | 58 +++++++++ .../SizeAndAlignOfDst/main_assert_fixme.rs | 85 ++++++++------ tests/kani/Tuple/tuple_trait.rs | 19 +++ 12 files changed, 227 insertions(+), 148 deletions(-) create mode 100644 tests/kani/Closure/zst_unwrap.rs create mode 100644 tests/kani/SizeAndAlignOfDst/main_assert.rs create mode 100644 tests/kani/Tuple/tuple_trait.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 6c711e3d20e4..e497cfc6b47c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -12,7 +12,7 @@ use cbmc::goto_program::{ use rustc_middle::ty::layout::ValidityRequirement; use rustc_middle::ty::ParamEnv; use rustc_smir::rustc_internal; -use stable_mir::mir::mono::{Instance, InstanceKind}; +use stable_mir::mir::mono::Instance; use stable_mir::mir::{BasicBlockIdx, Operand, Place}; use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy}; use tracing::debug; @@ -45,17 +45,15 @@ impl<'tcx> GotocCtx<'tcx> { /// there is no terminator. pub fn codegen_funcall_of_intrinsic( &mut self, - func: &Operand, + instance: Instance, args: &[Operand], destination: &Place, target: Option, span: Span, ) -> Stmt { - let instance = self.get_intrinsic_instance(func).unwrap(); - if let Some(target) = target { let loc = self.codegen_span_stable(span); - let fargs = self.codegen_funcall_args(args, false); + let fargs = args.iter().map(|arg| self.codegen_operand_stable(arg)).collect::>(); Stmt::block( vec![ self.codegen_intrinsic(instance, fargs, destination, span), @@ -68,23 +66,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Returns `Some(instance)` if the function is an intrinsic; `None` otherwise - fn get_intrinsic_instance(&self, func: &Operand) -> Option { - let funct = self.operand_ty_stable(func); - match funct.kind() { - TyKind::RigidTy(RigidTy::FnDef(def, args)) => { - let instance = Instance::resolve(def, &args).unwrap(); - if matches!(instance.kind, InstanceKind::Intrinsic) { Some(instance) } else { None } - } - _ => None, - } - } - - /// Returns true if the `func` is a call to a compiler intrinsic; false otherwise. - pub fn is_intrinsic(&self, func: &Operand) -> bool { - self.get_intrinsic_instance(func).is_some() - } - /// Handles codegen for non returning intrinsics /// Non returning intrinsics are not associated with a destination pub fn codegen_never_return_intrinsic(&mut self, instance: Instance, span: Span) -> Stmt { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 517609bb0b4c..6c75c6a5ad5a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -557,6 +557,17 @@ impl<'tcx> GotocCtx<'tcx> { alloc_vals } + /// Returns `Some(instance)` if the function is an intrinsic; `None` otherwise + pub fn get_instance(&self, func: &Operand) -> Option { + let funct = self.operand_ty_stable(func); + match funct.kind() { + TyKind::RigidTy(RigidTy::FnDef(def, args)) => { + Some(Instance::resolve(def, &args).unwrap()) + } + _ => None, + } + } + /// Generate a goto expression for a MIR "function item" reference. /// /// A "function item" is a ZST that corresponds to a specific single function. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 05eb1bc41dc7..05b153f9583f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -7,14 +7,16 @@ use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; use rustc_middle::ty::layout::LayoutOf; +use rustc_middle::ty::{List, ParamEnv}; use rustc_smir::rustc_internal; use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; +use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::{ AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL, }; -use stable_mir::ty::{RigidTy, Span, Ty, TyKind, VariantIdx}; +use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx}; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -432,31 +434,21 @@ impl<'tcx> GotocCtx<'tcx> { /// as subsequent parameters. /// /// See [GotocCtx::ty_needs_untupled_args] for more details. - fn codegen_untupled_args( - &mut self, - instance: Instance, - fargs: &mut Vec, - last_mir_arg: Option<&Operand>, - ) { - debug!("codegen_untuple_closure_args instance: {:?}, fargs {:?}", instance.name(), fargs); - if !fargs.is_empty() { - let tuple_ty = self.operand_ty_stable(last_mir_arg.unwrap()); - if self.is_zst_stable(tuple_ty) { - // Don't pass anything if all tuple elements are ZST. - // ZST arguments are ignored. - return; - } - let tupe = fargs.remove(fargs.len() - 1); - if let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() { - for (idx, arg_ty) in tupled_args.iter().enumerate() { - if !self.is_zst_stable(*arg_ty) { - // Access the tupled parameters through the `member` operation - let idx_expr = tupe.clone().member(&idx.to_string(), &self.symbol_table); - fargs.push(idx_expr); - } - } - } - } + fn codegen_untupled_args(&mut self, op: &Operand, args_abi: &[ArgAbi]) -> Vec { + let tuple_ty = self.operand_ty_stable(op); + let tuple_expr = self.codegen_operand_stable(op); + let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() else { unreachable!() }; + tupled_args + .iter() + .enumerate() + .filter_map(|(idx, _)| { + let arg_abi = &args_abi[idx]; + (arg_abi.mode != PassMode::Ignore).then(|| { + // Access the tupled parameters through the `member` operation + tuple_expr.clone().member(idx.to_string(), &self.symbol_table) + }) + }) + .collect() } /// Because function calls terminate basic blocks, to "end" a function call, we @@ -472,25 +464,24 @@ impl<'tcx> GotocCtx<'tcx> { /// Generate Goto-C for each argument to a function call. /// /// N.B. public only because instrinsics use this directly, too. - /// When `skip_zst` is set to `true`, the return value will not include any argument that is ZST. - /// This is used because we ignore ZST arguments, except for intrinsics. - pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand], skip_zst: bool) -> Vec { - let fargs = args + pub(crate) fn codegen_funcall_args(&mut self, fn_abi: &FnAbi, args: &[Operand]) -> Vec { + let fargs: Vec = args .iter() - .filter_map(|op| { - let op_ty = self.operand_ty_stable(op); - if op_ty.kind().is_bool() { + .enumerate() + .filter_map(|(i, op)| { + // Functions that require caller info will have an extra parameter. + let arg_abi = &fn_abi.args.get(i); + let ty = self.operand_ty_stable(op); + if ty.kind().is_bool() { Some(self.codegen_operand_stable(op).cast_to(Type::c_bool())) - } else if !self.is_zst_stable(op_ty) || !skip_zst { + } else if arg_abi.map_or(true, |abi| abi.mode != PassMode::Ignore) { Some(self.codegen_operand_stable(op)) } else { - // We ignore ZST types. - debug!(arg=?op, "codegen_funcall_args ignore"); None } }) .collect(); - debug!(?fargs, "codegen_funcall_args"); + debug!(?fargs, args_abi=?fn_abi.args, "codegen_funcall_args"); fargs } @@ -515,9 +506,12 @@ impl<'tcx> GotocCtx<'tcx> { span: Span, ) -> Stmt { debug!(?func, ?args, ?destination, ?span, "codegen_funcall"); - if self.is_intrinsic(&func) { + let instance_opt = self.get_instance(func); + if let Some(instance) = instance_opt + && matches!(instance.kind, InstanceKind::Intrinsic) + { return self.codegen_funcall_of_intrinsic( - &func, + instance, &args, &destination, target.map(|bb| bb), @@ -526,16 +520,23 @@ impl<'tcx> GotocCtx<'tcx> { } let loc = self.codegen_span_stable(span); - let funct = self.operand_ty_stable(func); - let mut fargs = self.codegen_funcall_args(&args, true); - match funct.kind() { - TyKind::RigidTy(RigidTy::FnDef(def, subst)) => { - let instance = Instance::resolve(def, &subst).unwrap(); - - // TODO(celina): Move this check to be inside codegen_funcall_args. - if self.ty_needs_untupled_args(rustc_internal::internal(self.tcx, funct)) { - self.codegen_untupled_args(instance, &mut fargs, args.last()); - } + let fn_ty = self.operand_ty_stable(func); + match fn_ty.kind() { + fn_def @ TyKind::RigidTy(RigidTy::FnDef(..)) => { + let instance = instance_opt.unwrap(); + let fn_abi = instance.fn_abi().unwrap(); + let mut fargs = if args.is_empty() + || fn_def.fn_sig().unwrap().value.abi != Abi::RustCall + { + self.codegen_funcall_args(&fn_abi, &args) + } else { + let (untupled, first_args) = args.split_last().unwrap(); + let mut fargs = self.codegen_funcall_args(&fn_abi, &first_args); + fargs.append( + &mut self.codegen_untupled_args(untupled, &fn_abi.args[first_args.len()..]), + ); + fargs + }; if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) { return hk.handle(self, instance, fargs, destination, *target, span); @@ -573,7 +574,16 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::block(stmts, loc) } // Function call through a pointer - TyKind::RigidTy(RigidTy::FnPtr(_)) => { + TyKind::RigidTy(RigidTy::FnPtr(fn_sig)) => { + let fn_sig_internal = rustc_internal::internal(self.tcx, fn_sig); + let fn_ptr_abi = rustc_internal::stable( + self.tcx + .fn_abi_of_fn_ptr( + ParamEnv::reveal_all().and((fn_sig_internal, &List::empty())), + ) + .unwrap(), + ); + let fargs = self.codegen_funcall_args(&fn_ptr_abi, &args); let func_expr = self.codegen_operand_stable(func).dereference(); // Actually generate the function call and return. Stmt::block( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs index 0130beffe84b..7ba2ff9c53c8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs @@ -115,6 +115,11 @@ impl<'tcx> GotocCtx<'tcx> { pub fn pretty_ty(&self, ty: Ty) -> String { rustc_internal::internal(self.tcx, ty).to_string() } + + pub fn requires_caller_location(&self, instance: Instance) -> bool { + let instance_internal = rustc_internal::internal(self.tcx, instance); + instance_internal.def.requires_caller_location(self.tcx) + } } /// If given type is a Ref / Raw ref, return the pointee type. pub fn pointee_type(mir_type: Ty) -> Option { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index b0e3c115d597..57af958abf41 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -21,7 +21,6 @@ use rustc_target::abi::{ Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding, TyAndLayout, VariantIdx, Variants, }; -use rustc_target::spec::abi::Abi; use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::mono::Instance as InstanceStable; use stable_mir::mir::Body; @@ -731,39 +730,6 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_struct_fields(flds, &layout.layout.0, Size::ZERO) } - /// A closure / some shims in Rust MIR takes two arguments: - /// - /// 0. a struct representing the environment - /// 1. a tuple containing the parameters - /// - /// However, during codegen/lowering from MIR, the 2nd tuple of parameters - /// is flattened into subsequent parameters. - /// - /// Checking whether the type's kind is a closure is insufficient, because - /// a virtual method call through a vtable can have the trait's non-closure - /// type. For example: - /// - /// ``` - /// let p: &dyn Fn(i32) = &|x| assert!(x == 1); - /// p(1); - /// ``` - /// - /// Here, the call `p(1)` desugars to an MIR trait call `Fn::call(&p, (1,))`, - /// where the second argument is a tuple. The instance type kind for - /// `Fn::call` is not a closure, because dynamically, the pointer may be to - /// a function definition instead. We still need to untuple in this case, - /// so we follow the example elsewhere in Rust to use the ABI call type. - /// - /// See `make_call_args` in `rustc_mir_transform/src/inline.rs` - pub fn ty_needs_untupled_args(&self, ty: Ty<'tcx>) -> bool { - // Note that [Abi::RustCall] is not [Abi::Rust]. - // Documentation is sparse, but it does seem to correspond to the need for untupling. - match ty.kind() { - ty::FnDef(..) | ty::FnPtr(..) => ty.fn_sig(self.tcx).abi() == Abi::RustCall, - _ => unreachable!("Can't treat type as a function: {:?}", ty), - } - } - /// A closure is a struct of all its environments. That is, a closure is /// just a tuple with a unique type identifier, so that Fn related traits /// can find its impl. @@ -1647,13 +1613,12 @@ impl<'tcx> GotocCtx<'tcx> { /// 1. In some cases, an argument can be ignored (e.g.: ZST arguments in regular Rust calls). /// 2. We currently don't support `track_caller`, so we ignore the extra argument that is added to support that. /// Tracked here: - fn codegen_args<'a>( + pub fn codegen_args<'a>( &self, instance: InstanceStable, fn_abi: &'a FnAbi, ) -> impl Iterator { - let instance_internal = rustc_internal::internal(self.tcx, instance); - let requires_caller_location = instance_internal.def.requires_caller_location(self.tcx); + let requires_caller_location = self.requires_caller_location(instance); let num_args = fn_abi.args.len(); fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| { arg_abi.mode != PassMode::Ignore && !(requires_caller_location && idx + 1 == num_args) diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index 8a7fc16d8e9f..404cb0f277c3 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -101,8 +101,8 @@ fn resolve_rust_intrinsic<'tcx>( func_ty: Ty<'tcx>, ) -> Option<(Symbol, GenericArgsRef<'tcx>)> { if let ty::FnDef(def_id, args) = *func_ty.kind() { - if tcx.is_intrinsic(def_id) { - return Some((tcx.item_name(def_id), args)); + if let Some(symbol) = tcx.intrinsic(def_id) { + return Some((symbol, args)); } } None diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 4316d188c02d..fef0fba66489 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -13,6 +13,7 @@ #![feature(lazy_cell)] #![feature(more_qualified_paths)] #![feature(iter_intersperse)] +#![feature(let_chains)] extern crate rustc_abi; extern crate rustc_ast; extern crate rustc_ast_pretty; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 42bd4779102f..42f6af899b43 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-02-14" +channel = "nightly-2024-02-17" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Closure/zst_unwrap.rs b/tests/kani/Closure/zst_unwrap.rs new file mode 100644 index 000000000000..4c755e08abc7 --- /dev/null +++ b/tests/kani/Closure/zst_unwrap.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Test that Kani can properly handle closure to fn ptr when an argument type is Never (`!`). +//! See for more details. +#![feature(never_type)] + +pub struct Foo { + _x: i32, + _never: !, +} + +#[kani::proof] +fn check_unwrap_never() { + let res = Result::::Ok(3); + let _x = res.unwrap_or_else(|_f| 5); +} diff --git a/tests/kani/SizeAndAlignOfDst/main_assert.rs b/tests/kani/SizeAndAlignOfDst/main_assert.rs new file mode 100644 index 000000000000..09f7b1b0c774 --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/main_assert.rs @@ -0,0 +1,58 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This is a regression test for size_and_align_of_dst computing the +//! size and alignment of a dynamically-sized type like +//! Arc>. +//! + +/// This test fails on macos but not in other platforms. +/// Thus only enable it for platforms where this shall succeed. +#[cfg(not(target_os = "macos"))] +mod not_macos { + use std::sync::Arc; + use std::sync::Mutex; + + pub trait Subscriber { + fn process(&self); + fn increment(&mut self); + fn get(&self) -> u32; + } + + struct DummySubscriber { + val: u32, + } + + impl DummySubscriber { + fn new() -> Self { + DummySubscriber { val: 0 } + } + } + + impl Subscriber for DummySubscriber { + fn process(&self) {} + fn increment(&mut self) { + self.val = self.val + 1; + } + fn get(&self) -> u32 { + self.val + } + } + + #[kani::proof] + #[kani::unwind(2)] + fn simplified() { + let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); + let data = s.lock().unwrap(); + assert!(data.get() == 0); + } + + #[kani::proof] + #[kani::unwind(1)] + fn original() { + let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); + let mut data = s.lock().unwrap(); + data.increment(); + assert!(data.get() == 1); + } +} diff --git a/tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs b/tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs index 9173eca7db3c..25075bc910d9 100644 --- a/tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs +++ b/tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs @@ -8,51 +8,64 @@ //! Arc>. //! We added a simplified version of the original harness from: //! -//! This currently fails due to -//! +//! This currently fails on MacOS instances due to unsupported foreign function: +//! `pthread_mutexattr_init`. -use std::sync::Arc; -use std::sync::Mutex; +#[cfg(target_os = "macos")] +mod macos { + use std::sync::Arc; + use std::sync::Mutex; -pub trait Subscriber { - fn process(&self); - fn increment(&mut self); - fn get(&self) -> u32; -} + pub trait Subscriber { + fn process(&self); + fn increment(&mut self); + fn get(&self) -> u32; + } -struct DummySubscriber { - val: u32, -} + struct DummySubscriber { + val: u32, + } -impl DummySubscriber { - fn new() -> Self { - DummySubscriber { val: 0 } + impl DummySubscriber { + fn new() -> Self { + DummySubscriber { val: 0 } + } } -} -impl Subscriber for DummySubscriber { - fn process(&self) {} - fn increment(&mut self) { - self.val = self.val + 1; + impl Subscriber for DummySubscriber { + fn process(&self) {} + fn increment(&mut self) { + self.val = self.val + 1; + } + fn get(&self) -> u32 { + self.val + } } - fn get(&self) -> u32 { - self.val + + #[kani::proof] + #[kani::unwind(2)] + fn simplified() { + let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); + let data = s.lock().unwrap(); + assert!(data.get() == 0); } -} -#[kani::proof] -#[kani::unwind(2)] -fn simplified() { - let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); - let data = s.lock().unwrap(); - assert!(data.get() == 0); + #[kani::proof] + #[kani::unwind(1)] + fn original() { + let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); + let mut data = s.lock().unwrap(); + data.increment(); + assert!(data.get() == 1); + } } -#[kani::proof] -#[kani::unwind(1)] -fn original() { - let s: Arc> = Arc::new(Mutex::new(DummySubscriber::new())); - let mut data = s.lock().unwrap(); - data.increment(); - assert!(data.get() == 1); +#[cfg(not(target_os = "macos"))] +mod not_macos { + /// Since this is a fixme test, it must also fail in other platforms. + /// Remove this once we fix the issue above. + #[kani::proof] + fn fail() { + assert!(false); + } } diff --git a/tests/kani/Tuple/tuple_trait.rs b/tests/kani/Tuple/tuple_trait.rs new file mode 100644 index 000000000000..d775b393b0b8 --- /dev/null +++ b/tests/kani/Tuple/tuple_trait.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Tests support for functions declared with "rust-call" ABI and an empty set of arguments. +#![feature(unboxed_closures, tuple_trait)] + +extern "rust-call" fn foo(_: T) -> usize { + static mut COUNTER: usize = 0; + unsafe { + COUNTER += 1; + COUNTER + } +} + +#[kani::proof] +fn main() { + assert_eq!(foo(()), 1); + assert_eq!(foo(()), 2); +}