Skip to content

test: use kani built-in --harness-timeout option #5252

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Jun 19, 2025

Conversation

roypat
Copy link
Contributor

@roypat roypat commented Jun 6, 2025

Set a per-harness timeout of 40 minutes. This should make it easier to debug scenarios where proofs end up hanging indefinitely, as we now no longer hit the pytest timeout, but instead a timeout built into kani (which should tell us what exact harness timed out), e.g.:

Thread 95:
CBMC failed
VERIFICATION:- FAILED
CBMC timed out. You may want to rerun your proof with a larger timeout or use stubbing to reduce the size of the code the verifier reasons about.
Manual Harness Summary:
Verification failed for - devices::virtio::iovec::verification::verify_write_to_iovec
Complete - 34 successfully verified harnesses, 1 failures, 35 total.

License Acceptance

By submitting this pull request, I confirm that my contribution is made under
the terms of the Apache 2.0 license. For more information on following Developer
Certificate of Origin and signing off your commits, please check
CONTRIBUTING.md.

PR Checklist

  • I have read and understand CONTRIBUTING.md.
  • I have run tools/devtool checkstyle to verify that the PR passes the
    automated style checks.
  • I have described what is done in these changes, why they are needed, and
    how they are solving the problem in a clear and encompassing way.
  • I have updated any relevant documentation (both in code and in the docs)
    in the PR.
  • I have mentioned all user-facing changes in CHANGELOG.md.
  • If a specific issue led to this PR, this PR closes the issue.
  • When making API changes, I have followed the
    Runbook for Firecracker API changes.
  • I have tested all new and changed functionalities in unit tests and/or
    integration tests.
  • I have linked an issue to every new TODO.

  • This functionality cannot be added in rust-vmm.

Copy link

codecov bot commented Jun 6, 2025

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 82.90%. Comparing base (d5f3513) to head (c34953d).
Report is 2 commits behind head on main.

Additional details and impacted files
@@            Coverage Diff             @@
##             main    #5252      +/-   ##
==========================================
+ Coverage   82.84%   82.90%   +0.05%     
==========================================
  Files         250      250              
  Lines       26967    26967              
==========================================
+ Hits        22342    22356      +14     
+ Misses       4625     4611      -14     
Flag Coverage Δ
5.10-c5n.metal 83.33% <ø> (+<0.01%) ⬆️
5.10-m5n.metal 83.33% <ø> (ø)
5.10-m6a.metal 82.55% <ø> (ø)
5.10-m6g.metal 79.16% <ø> (ø)
5.10-m6i.metal 83.33% <ø> (+<0.01%) ⬆️
5.10-m7a.metal-48xl 82.54% <ø> (?)
5.10-m7g.metal 79.16% <ø> (ø)
5.10-m7i.metal-24xl 83.30% <ø> (?)
5.10-m7i.metal-48xl 83.29% <ø> (?)
5.10-m8g.metal-24xl 79.16% <ø> (?)
5.10-m8g.metal-48xl 79.16% <ø> (?)
6.1-c5n.metal 83.37% <ø> (ø)
6.1-m5n.metal 83.38% <ø> (+<0.01%) ⬆️
6.1-m6a.metal 82.59% <ø> (ø)
6.1-m6g.metal 79.16% <ø> (ø)
6.1-m6i.metal 83.38% <ø> (+<0.01%) ⬆️
6.1-m7a.metal-48xl 82.59% <ø> (?)
6.1-m7g.metal 79.16% <ø> (-0.01%) ⬇️
6.1-m7i.metal-24xl 83.38% <ø> (?)
6.1-m7i.metal-48xl 83.39% <ø> (?)
6.1-m8g.metal-24xl 79.16% <ø> (?)
6.1-m8g.metal-48xl 79.16% <ø> (?)

Flags with carried forward coverage won't be shown. Click here to find out more.

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@roypat roypat added the Status: Awaiting review Indicates that a pull request is ready to be reviewed label Jun 16, 2025
roypat added 2 commits June 16, 2025 14:45
Set a per-harness timeout of 30 minutes. This should hopefully make it
easier to debug scenarios where proofs end up hanging indefinitely, as
we now no longer hit the pytest timeout, but instead a timeout built
into kani (which should tell us what exact harness timed out).

Signed-off-by: Patrick Roy <[email protected]>
Just so that we run the test when we change only the test itself.

Signed-off-by: Patrick Roy <[email protected]>
@roypat roypat enabled auto-merge (rebase) June 18, 2025 13:34
@roypat roypat merged commit e7c320f into firecracker-microvm:main Jun 19, 2025
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Status: Awaiting review Indicates that a pull request is ready to be reviewed
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants