Merge branch 'main' into attr-invariant

.github/workflows/verify-std-check.yml

@@ -39,6 +39,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           path: kani
+          fetch-depth: 0
 
       - name: Setup Kani Dependencies
         uses: ./kani/.github/actions/setup
@@ -79,8 +80,10 @@ jobs:
             -Z mem-predicates -Z ptr-to-ref-cast-checks
 
       - name: Compare PR results
-        if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output
+        if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome
         run: |
           echo "New failure introduced by this change"
+          echo "HEAD: ${{ steps.check-head.outcome }}"
+          echo "BASE: ${{ steps.check-base.outcome }}"
           exit 1
 

kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs

@@ -25,7 +25,7 @@ pub fn init() {
 
 /// Custom panic hook to add more information when panic occurs during goto-c codegen.
 #[allow(clippy::type_complexity)]
-static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
+static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + Sync + Send + 'static>> =
     LazyLock::new(|| {
         let hook = panic::take_hook();
         panic::set_hook(Box::new(|info| {

kani-compiler/src/session.rs

@@ -29,7 +29,7 @@ const BUG_REPORT_URL: &str =
 
 // Custom panic hook when running under user friendly message format.
 #[allow(clippy::type_complexity)]
-static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
+static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + Sync + Send + 'static>> =
     LazyLock::new(|| {
         let hook = panic::take_hook();
         panic::set_hook(Box::new(|info| {
@@ -46,7 +46,7 @@ static PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 's
 
 // Custom panic hook when executing under json error format `--error-format=json`.
 #[allow(clippy::type_complexity)]
-static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send + 'static>> =
+static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicHookInfo<'_>) + Sync + Send + 'static>> =
     LazyLock::new(|| {
         let hook = panic::take_hook();
         panic::set_hook(Box::new(|info| {

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-07-21"
+channel = "nightly-2024-07-30"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/function-contract/interior-mutability/api/cell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/api/cell.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// Mutating Cell via `as_ptr` in contracts
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+#[kani::ensures(|_| im.x.get() < 101)]
+///im is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&im)
+}

tests/expected/function-contract/interior-mutability/api/cell_stub.expected

@@ -0,0 +1,9 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get()) == im.x.get()"\
+
+assertion\
+- Status: SUCCESS\
+- Description: "|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/api/cell_stub.rs

@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple.
+/// This shows that we can generate `kani::any()` for Cell.
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::ensures(|_| old(im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(im.x.as_ptr())]
+fn double(im: &InteriorMutability) {
+    im.x.set(im.x.get() + im.x.get())
+}
+
+#[kani::proof_for_contract(double)]
+fn double_harness() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    double(&im);
+}
+
+#[kani::ensures(|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get())]
+#[kani::requires(im.x.get() < 50)]
+#[kani::modifies(im.x.as_ptr())]
+fn quadruple(im: &InteriorMutability) {
+    double(im);
+    double(im)
+}
+
+#[kani::proof_for_contract(quadruple)]
+#[kani::stub_verified(double)]
+fn quadruple_harness() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    quadruple(&im);
+}

tests/expected/function-contract/interior-mutability/api/unsafecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/api/unsafecell.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+use std::cell::UnsafeCell;
+
+/// This struct contains UnsafeCell which can be mutated
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.get()} < 100)]
+#[kani::modifies(im.x.get())]
+#[kani::ensures(|_| unsafe{*im.x.get()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&im)
+}

tests/expected/function-contract/interior-mutability/whole-struct/cell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get() < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/whole-struct/cell.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct
+use std::cell::Cell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: Cell<u32>,
+}
+
+#[kani::requires(im.x.get() < 100)]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| im.x.get() < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.set(im.x.get() + 1)
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) };
+    modify(&im)
+}

tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| im.x.get().is_some()"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an OnceCell used as interior mutability in an immutable struct
+use std::cell::OnceCell;
+
+/// This struct contains OnceCell which can be mutated
+struct InteriorMutability {
+    x: OnceCell<u32>,
+}
+
+#[kani::requires(im.x.get().is_none())]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| im.x.get().is_some())]
+fn modify(im: &InteriorMutability) {
+    im.x.set(5).expect("")
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: OnceCell::new() };
+    modify(&im)
+}

tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct
+use std::cell::RefCell;
+
+/// This struct contains Cell which can be mutated
+struct InteriorMutability {
+    x: RefCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.as_ptr()} < 100)]
+#[kani::modifies(&im.x)]
+#[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    im.x.replace_with(|&mut old| old + 1);
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: RefCell::new(kani::any()) };
+    modify(&im)
+}

tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected

@@ -0,0 +1,6 @@
+assertion\
+- Status: SUCCESS\
+- Description: "|_| unsafe{ *im.x.get() } < 101"\
+in function modify
+
+VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+/// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct
+use std::cell::UnsafeCell;
+
+/// This struct contains UnsafeCell which can be mutated
+struct InteriorMutability {
+    x: UnsafeCell<u32>,
+}
+
+#[kani::requires(unsafe{*im.x.get()} < 100)]
+#[kani::modifies(im.x.get())]
+#[kani::ensures(|_| unsafe{*im.x.get()} < 101)]
+/// `im` is an immutable reference with interior mutability
+fn modify(im: &InteriorMutability) {
+    unsafe { *im.x.get() += 1 }
+}
+
+#[kani::proof_for_contract(modify)]
+fn harness_for_modify() {
+    let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) };
+    modify(&im)
+}