Add a kani::futures library containing block_on

library/kani/src/futures.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains functions to work with futures (and async/.await) in Kani.
+
+use std::{
+    future::Future,
+    pin::Pin,
+    task::{Context, RawWaker, RawWakerVTable, Waker},
+};
+
+/// A very simple executor: it polls the future in a busy loop until completion
+///
+/// This is intended as a drop-in replacement for `futures::block_on`, which Kani cannot handle.
+/// Whereas a clever executor like `block_on` in `futures` or `tokio` would interact with the OS scheduler
+/// to be woken up when a resource becomes available, this is not supported by Kani.
+/// As a consequence, this function completely ignores the waker infrastructure and just polls the given future in a busy loop.
+pub fn block_on<T>(mut fut: impl Future<Output = T>) -> T {
+    let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
+    let cx = &mut Context::from_waker(&waker);
+    // SAFETY: we shadow the original binding, so it cannot be accessed again for the rest of the scope.
+    // This is the same as what the pin_mut! macro in the futures crate does.
+    let mut fut = unsafe { Pin::new_unchecked(&mut fut) };
+    loop {
+        match fut.as_mut().poll(cx) {
+            std::task::Poll::Ready(res) => return res,
+            std::task::Poll::Pending => continue,
+        }
+    }
+}
+
+/// A dummy waker, which is needed to call [`Future::poll`]
+const NOOP_RAW_WAKER: RawWaker = {
+    #[inline]
+    unsafe fn clone_waker(_: *const ()) -> RawWaker {
+        NOOP_RAW_WAKER
+    }
+
+    #[inline]
+    unsafe fn noop(_: *const ()) {}
+
+    RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop))
+};

library/kani/src/lib.rs

@@ -4,11 +4,13 @@
 #![feature(min_specialization)] // Used for default implementation of Arbitrary.
 
 pub mod arbitrary;
+pub mod futures;
 pub mod invariant;
 pub mod slice;
 pub mod vec;
 
 pub use arbitrary::Arbitrary;
+pub use futures::block_on;
 pub use invariant::Invariant;
 
 /// Creates an assumption that will be valid after this statement run. Note that the assumption

tests/kani/AsyncAwait/main.rs

@@ -14,9 +14,21 @@ use std::{
 fn main() {}
 
 #[kani::proof]
-#[kani::unwind(10)]
+#[kani::unwind(2)]
 fn test_async_await() {
-    poll_loop(async {
+    // Test using the `block_on` implementation in Kani's library
+    kani::block_on(async {
+        let async_block_result = async { 42 }.await;
+        let async_fn_result = async_fn().await;
+        assert_eq!(async_block_result, async_fn_result);
+    })
+}
+
+#[kani::proof]
+#[kani::unwind(2)]
+fn test_async_await_manually() {
+    // Test using the manual `block_on` implementation
+    block_on(async {
         let async_block_result = async { 42 }.await;
         let async_fn_result = async_fn().await;
         assert_eq!(async_block_result, async_fn_result);
@@ -28,12 +40,12 @@ pub async fn async_fn() -> i32 {
 }
 
 /// A very simple executor that just polls the future in a loop
-pub fn poll_loop<F: Future>(mut fut: F) -> <F as Future>::Output {
+pub fn block_on<T>(mut fut: impl Future<Output = T>) -> T {
     let waker = unsafe { Waker::from_raw(NOOP_RAW_WAKER) };
     let cx = &mut Context::from_waker(&waker);
+    let mut fut = unsafe { Pin::new_unchecked(&mut fut) };
     loop {
-        let pinned = unsafe { Pin::new_unchecked(&mut fut) };
-        match pinned.poll(cx) {
+        match fut.as_mut().poll(cx) {
             std::task::Poll::Ready(res) => return res,
             std::task::Poll::Pending => continue,
         }
@@ -45,11 +57,6 @@ const NOOP_RAW_WAKER: RawWaker = {
     unsafe fn clone_waker(_: *const ()) -> RawWaker {
         NOOP_RAW_WAKER
     }
-    unsafe fn wake(_: *const ()) {}
-    unsafe fn wake_by_ref(_: *const ()) {}
-    unsafe fn drop_waker(_: *const ()) {}
-    RawWaker::new(
-        std::ptr::null(),
-        &RawWakerVTable::new(clone_waker, wake, wake_by_ref, drop_waker),
-    )
+    unsafe fn noop(_: *const ()) {}
+    RawWaker::new(std::ptr::null(), &RawWakerVTable::new(clone_waker, noop, noop, noop))
 };