Selectively enable and fix (slow) Tokio tests (#4203)

1. Some of the tests that were disabled wouldn't even compile. Fixed,
even when they may still be disabled.
2. Adjusted unwinding bounds and `should_fail` attributes to avoid
spurious test failures.
3. Updated comments to clarify why tests are (still) disabled.
4. Enabled all tests that completed under 15 minutes and with less than
10 GB of memory footprint (14 additional tests).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: tautschnig

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