Selectively enable and fix (slow) Tokio tests

tests/slow/tokio-proofs/expected

@@ -1 +1 @@
-Complete - 13 successfully verified harnesses, 0 failures, 13 total.
+Complete - 27 successfully verified harnesses, 0 failures, 27 total.

tests/slow/tokio-proofs/src/tokio/io_chain.rs

@@ -12,9 +12,8 @@
 use tokio::io::AsyncReadExt;
 use tokio_test::assert_ok;
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn chain() {
     let mut buf = Vec::new();
     let rd1: &[u8] = b"hello ";

tests/slow/tokio-proofs/src/tokio/io_copy.rs

@@ -17,7 +17,7 @@ use tokio_test::assert_ok;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn copy() {
@@ -47,7 +47,7 @@ async fn copy() {
     assert_eq!(wr, b"hello world");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn proxy() {

tests/slow/tokio-proofs/src/tokio/io_lines.rs

@@ -12,7 +12,7 @@
 use tokio::io::AsyncBufReadExt;
 use tokio_test::assert_ok;
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires memchr
 #[kani::proof]
 #[kani::unwind(2)]
 async fn lines_inherent() {

tests/slow/tokio-proofs/src/tokio/io_mem_stream.rs

@@ -11,7 +11,7 @@
 
 use tokio::io::{AsyncReadExt, AsyncWriteExt, duplex};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn ping_pong() {
@@ -29,7 +29,7 @@ async fn ping_pong() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn across_tasks() {
@@ -54,7 +54,7 @@ async fn across_tasks() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn disconnect() {
@@ -79,7 +79,7 @@ async fn disconnect() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn disconnect_reader() {
@@ -101,7 +101,7 @@ async fn disconnect_reader() {
 }
 
 // Kani does not support this one yet because it uses spawn
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn max_write_size() {
@@ -124,7 +124,7 @@ async fn max_write_size() {
 }
 
 // Kani does not support this one yet because it uses select
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn duplex_is_cooperative() {

tests/slow/tokio-proofs/src/tokio/io_read.rs

@@ -71,11 +71,9 @@ impl AsyncRead for BadAsyncRead {
     }
 }
 
-#[cfg(disabled)] // because Kani does not support should_panic
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
-#[should_panic]
+#[kani::should_panic]
 async fn read_buf_bad_async_read() {
     let mut buf = Vec::with_capacity(10);
     BadAsyncRead::new().read_buf(&mut buf).await.unwrap();

tests/slow/tokio-proofs/src/tokio/io_read_buf.rs

@@ -16,7 +16,6 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(12)]
 async fn read_buf() {

tests/slow/tokio-proofs/src/tokio/io_read_line.rs

@@ -15,7 +15,7 @@ use tokio_test::{assert_ok, io::Builder};
 
 use std::io::Cursor;
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line() {
@@ -39,7 +39,7 @@ async fn read_line() {
     assert_eq!(buf, "");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_not_all_ready() {
@@ -68,7 +68,7 @@ async fn read_line_not_all_ready() {
     assert_eq!(line.as_str(), "2");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_invalid_utf8() {
@@ -83,7 +83,7 @@ async fn read_line_invalid_utf8() {
     assert_eq!(line.as_str(), "Foo");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_fail() {
@@ -101,7 +101,7 @@ async fn read_line_fail() {
     assert_eq!(line.as_str(), "FooHello Wor");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_line_fail_and_utf8_fail() {

tests/slow/tokio-proofs/src/tokio/io_read_to_end.rs

@@ -14,9 +14,8 @@ use std::task::{Context, Poll};
 use tokio::io::{AsyncRead, AsyncReadExt, ReadBuf};
 use tokio_test::assert_ok;
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn read_to_end() {
     let mut buf = vec![];
     let mut rd: &[u8] = b"hello world";
@@ -75,9 +74,8 @@ impl AsyncRead for UninitTest {
     }
 }
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(65)]
 async fn read_to_end_uninit() {
     let mut buf = Vec::with_capacity(64);
     let mut test = UninitTest { num_init: 0, state: State::Initializing };

tests/slow/tokio-proofs/src/tokio/io_read_to_string.rs

@@ -14,9 +14,9 @@ use tokio::io::AsyncReadExt;
 use tokio_test::assert_ok;
 use tokio_test::io::Builder;
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC takes more than 15 minutes
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn read_to_string() {
     let mut buf = String::new();
     let mut rd: &[u8] = b"hello world";
@@ -26,7 +26,7 @@ async fn read_to_string() {
     assert_eq!(buf[..], "hello world"[..]);
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn to_string_does_not_truncate_on_utf8_error() {
@@ -43,7 +43,7 @@ async fn to_string_does_not_truncate_on_utf8_error() {
     assert_eq!(s, "abc");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn to_string_does_not_truncate_on_io_error() {
@@ -62,7 +62,7 @@ async fn to_string_does_not_truncate_on_io_error() {
     assert_eq!(s, "abc");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn to_string_appends() {

tests/slow/tokio-proofs/src/tokio/io_read_until.rs

@@ -13,7 +13,7 @@ use std::io::ErrorKind;
 use tokio::io::{AsyncBufReadExt, BufReader, Error};
 use tokio_test::{assert_ok, io::Builder};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires memchr
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_until() {
@@ -33,7 +33,7 @@ async fn read_until() {
     assert_eq!(buf, []);
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_until_not_all_ready() {
@@ -62,7 +62,7 @@ async fn read_until_not_all_ready() {
     assert_eq!(chunk, b"2");
 }
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // CBMC consumes more than 10 GB
 #[kani::proof]
 #[kani::unwind(2)]
 async fn read_until_fail() {

tests/slow/tokio-proofs/src/tokio/io_take.rs

@@ -68,11 +68,9 @@ impl AsyncRead for BadReader {
     }
 }
 
-#[cfg(disabled)] //  because Kani does not support should_panic
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
-#[should_panic]
+#[kani::should_panic]
 async fn bad_reader_fails() {
     let mut buf = Vec::with_capacity(10);
 

tests/slow/tokio-proofs/src/tokio/io_util_empty.rs

@@ -11,10 +11,9 @@
 #![cfg(feature = "full")]
 use tokio::io::{AsyncBufReadExt, AsyncReadExt};
 
-#[cfg(disabled)] // because Kani does not support select yet
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
 async fn empty_read_is_cooperative() {
     tokio::select! {
         biased;
@@ -29,10 +28,9 @@ async fn empty_read_is_cooperative() {
     }
 }
 
-#[cfg(disabled)] // because Kani does not support select yet
+#[cfg(disabled)] // requires pthread_key_create
 #[kani::proof]
 #[kani::unwind(2)]
-#[tokio::test]
 async fn empty_buf_reads_are_cooperative() {
     tokio::select! {
         biased;

tests/slow/tokio-proofs/src/tokio/io_write.rs

@@ -17,9 +17,8 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write2() {
     struct Wr {
         buf: BytesMut,

tests/slow/tokio-proofs/src/tokio/io_write_all.rs

@@ -18,9 +18,8 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write_all() {
     struct Wr {
         buf: BytesMut,

tests/slow/tokio-proofs/src/tokio/io_write_all_buf.rs

@@ -18,7 +18,7 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
+#[cfg(disabled)] // requires write
 #[kani::proof]
 #[kani::unwind(2)]
 async fn write_all_buf() {
@@ -62,9 +62,8 @@ async fn write_all_buf() {
     assert!(!buf.has_remaining());
 }
 
-#[cfg(disabled)] // because of missing functions
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write_buf_err() {
     /// Error out after writing the first 4 bytes
     struct Wr {

tests/slow/tokio-proofs/src/tokio/io_write_buf.rs

@@ -18,9 +18,8 @@ use std::io::{self, Cursor};
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
-#[kani::unwind(2)]
+#[kani::unwind(12)]
 async fn write_all1() {
     struct Wr {
         buf: BytesMut,

tests/slow/tokio-proofs/src/tokio/io_write_int.rs

@@ -15,7 +15,6 @@ use std::io;
 use std::pin::Pin;
 use std::task::{Context, Poll};
 
-#[cfg(disabled)] // because it timed out after 2h
 #[kani::proof]
 #[kani::unwind(2)]
 async fn write_int_should_err_if_write_count_0() {