Add async/await examples from tokio test suite

[fzaiser]

I went through the tokio's test suite and identified a couple of test cases that don't use a lot of I/O (or replace it with a mock) so that they seem like a reasonable target for Kani.

Description of changes:

No changes to how Kani works, this only adds tests that are ignored for now.

Testing:

• How is this change tested? No change of functionality, just adding tests

• Is this a refactor change? No.

Checklist

• [x] Each commit message has a non-empty body, explaining why the change was made
• [x] Methods or procedures are documented
• [x] Regression or unit tests are included, or existing tests cover the modified code
• [x] My PR is restricted to a single feature or bugfix

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

[zhassan-aws]

The tests have very few comments making it difficult to understand what they're doing. Can you add some comments, at least for the ones for which you have an idea what the purpose of the test is?

[fzaiser]

The tests compile under Kani now, but they take a very long time. I stopped the first harness (io_chain.rs) after two hours.

[adpaco-aws]

The tests compile under Kani now, but they take a very long time. I stopped the first harness (io_chain.rs) after two hours.

I saw you're using [kani::unwind(32)] for all harnesses. Have you tried using the minimum required for each harness?

[fzaiser]

I saw you're using [kani::unwind(32)] for all harnesses. Have you tried using the minimum required for each harness?

@adpaco-aws I will try this, but it's hard to know upfront what the necessary limit will be. Maybe I should try a smaller limit and successively increase it until it passes.

[fzaiser]

Progress report

Successful verification: 5 harnesses (basic_usage_fuse, basic_usage_once, empty_box_slice, empty_string, empty_vec)

Failed verification:

• 9 harnesses: too low unwinding bound (basic_usage_empty, empty_unit, issue_4435, merge_sync_streams, read_buf, read_exact, read, take, write_cursor)
• 4 harnesses: missing functions (empty, writ_buf_err, async_block, async_fn)

   Check 3880: _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE.1
    - Status: FAILURE
    - Description: "assertion"
    - Location: Unknown File in function _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE
   Check 4474: _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E.1
    - Status: FAILURE
    - Description: "assertion"
    - Location: Unknown File in function _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E
  

  missing epoll: 2 harnesses (async_block, async_fn)

  Check 5050: epoll_create1.1
   - Status: FAILURE
   - Description: "assertion"
   - Location: Unknown File in function epoll_create1
  

• 1 harness: unreachable code (empty)

  Check 1375: std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get.unreachable.1
   - Status: FAILURE
   - Description: "unreachable code"
   - Location: ~/.rustup/toolchains/nightly-2022-07-19-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:627:15 in function std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get
  

• rest: timed out or hit #1499

---

I will increase the unwinding bound for the ones with too low a bound.

[fzaiser]

Progress report after raising the unwind bound for some tests

Successful verification: 13 harnesses (basic_usage_fuse, basic_usage_once, empty_box_slice, empty_string, empty_vec, basic_usage_empty, empty_unit, issue_4435, read_exact, read, take, write_cursor, empty_result)

Failed verification:

• 4 harnesses: missing functions (empty, writ_buf_err, async_block, async_fn)

   Check 3880: _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE.1
    - Status: FAILURE
    - Description: "assertion"
    - Location: Unknown File in function _ZN3std3sys4unix4rand19hashmap_random_keys17hdd863e684c97ac1dE
   Check 4474: _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E.1
    - Status: FAILURE
    - Description: "assertion"
    - Location: Unknown File in function _ZN3std2io5error5Error4_new17ha2be3d29de30fdd1E
  

  missing epoll: 2 harnesses (async_block, async_fn)

  Check 5050: epoll_create1.1
   - Status: FAILURE
   - Description: "assertion"
   - Location: Unknown File in function epoll_create1
  

• ~1 harness: memcmp invalid pointer (empty_result) see #1489~ fixed
• 1 harness: unreachable code (empty)

  Check 1375: std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get.unreachable.1
   - Status: FAILURE
   - Description: "unreachable code"
   - Location: ~/.rustup/toolchains/nightly-2022-07-19-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:627:15 in function std::thread::local::lazy::LazyKeyInner::<std::cell::Cell<(u64, u64)>>::get
  

• rest: timed out or hit #1499

[fzaiser]

So the regresion tests pass now, but they take between 120 min (ubuntu-20.04) and 204 min (macos-11). It probably makes more sense to have those in a separate "slow" test suite.

As an alternative, we could add them as a compile-only test suite, which should be faster.

[danielsn]

I'd support adding a "slow" test suite, and running it nightly.

I'm not sure how many concurrent runners we get at the free tier. If its sufficient, we could also make it a "non-required" test so we would get information if it failed, but it wouldn't block work on PRs.

[fzaiser]

I've added a new slow test suite as suggested.

[fzaiser]

Another idea that @adpaco-aws mentioned is to run the slow tests after merging into main. But for now, I think the most important thing is to get the tests into main at all.

[fzaiser]

CI seems to have failed due to network issues, retrying

[fzaiser]

@danielsn I don't have rights to merge anymore. Can you merge it for me please?

[fzaiser]

Results of the slow test suite can be seen here: https://github.com/model-checking/kani/actions/workflows/slow-tests.yml