Add a timeout option #3649
Merged
Add a timeout option #3649
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
The changes seems to have slowed down Kani (regressions have been running for over an hour). Turning the PR into a draft till I investigate. |
|
Addressed the performance issue in 0502cc2. |
tautschnig
approved these changes
Oct 26, 2024
celinval
approved these changes
Oct 29, 2024
Merged
via the queue into
model-checking:main
with commit Oct 29, 2024
323fc27
26 of 27 checks passed
tautschnig
added a commit
to tautschnig/kani
that referenced
this pull request
Dec 13, 2024
Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml
-exec sed -i 's/version = "0.56.0"/version = "0.57.0"/' {} \;`) and ran
`cargo build-dev` to have `Cargo.lock` files updated.
GitHub generated release notes:
## What's Changed
* Remove the overflow checks for wrapping_offset by @zhassan-aws in model-checking#3589
* `kani-cov`: A coverage tool for Kani by @adpaco-aws in model-checking#3121
* Automatic toolchain upgrade to nightly-2024-10-04 by @github-actions in model-checking#3570
* Automatic toolchain upgrade to nightly-2024-10-05 by @github-actions in model-checking#3591
* Automatic toolchain upgrade to nightly-2024-10-06 by @github-actions in model-checking#3592
* Exclude Charon from workspace by @zhassan-aws in model-checking#3580
* Support fully-qualified --package arguments by @celinval in model-checking#3593
* Automatic toolchain upgrade to nightly-2024-10-07 by @github-actions in model-checking#3595
* Automatic toolchain upgrade to nightly-2024-10-08 by @github-actions in model-checking#3597
* Automatic cargo update to 2024-10-14 by @github-actions in model-checking#3598
* Bump tests/perf/s2n-quic from `17171ec` to `7752afb` by @dependabot in model-checking#3601
* Automatic toolchain upgrade to nightly-2024-10-09 by @github-actions in model-checking#3600
* Automatic toolchain upgrade to nightly-2024-10-10 by @github-actions in model-checking#3602
* Automatic toolchain upgrade to nightly-2024-10-11 by @github-actions in model-checking#3603
* Loop Contracts Annotation for While-Loop by @qinheping in model-checking#3151
* Automatic toolchain upgrade to nightly-2024-10-12 by @github-actions in model-checking#3604
* Update toolchain to 2024-10-15 by @zhassan-aws in model-checking#3605
* Automatic toolchain upgrade to nightly-2024-10-16 by @github-actions in model-checking#3607
* Implement proper function pointer handling for validity checks by @celinval in model-checking#3606
* Update toolchain to 2024-10-17 by @zhassan-aws in model-checking#3610
* Add fn that checks pointers point to same allocation by @celinval in model-checking#3583
* Automatic toolchain upgrade to nightly-2024-10-18 by @github-actions in model-checking#3613
* [aeneas] Preserve variable names by @zhassan-aws in model-checking#3560
* [Breaking change] Make `kani::check` private by @celinval in model-checking#3614
* Emit an error when proof_for_contract function is not found by @zhassan-aws in model-checking#3609
* Automatic toolchain upgrade to nightly-2024-10-19 by @github-actions in model-checking#3617
* Automatic toolchain upgrade to nightly-2024-10-20 by @github-actions in model-checking#3619
* Update test small_slice_eq by @qinheping in model-checking#3618
* Automatic toolchain upgrade to nightly-2024-10-21 by @github-actions in model-checking#3621
* Automatic cargo update to 2024-10-21 by @github-actions in model-checking#3622
* Bump tests/perf/s2n-quic from `7752afb` to `cd0314b` by @dependabot in model-checking#3625
* Update coverage flag in docs by @zhassan-aws in model-checking#3626
* Automatic toolchain upgrade to nightly-2024-10-22 by @github-actions in model-checking#3628
* Automatic toolchain upgrade to nightly-2024-10-23 by @github-actions in model-checking#3635
* Remove dead Option layer from run_piped by @zhassan-aws in model-checking#3634
* Add `free(0)` to codegen of loop contracts by @qinheping in model-checking#3637
* [Lean] Rename user-facing options from Aeneas to Lean by @zhassan-aws in model-checking#3630
* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in model-checking#3636
* Automatic toolchain upgrade to nightly-2024-10-24 by @github-actions in model-checking#3639
* Add regular & fixme tests for function contracts by @celinval in model-checking#3371
* Call `goto-instrument` with `DFCC` only once by @qinheping in model-checking#3642
* Build and include `kani-cov` in the bundle by @adpaco-aws in model-checking#3641
* Fix loop contracts transformation when loops in branching by @qinheping in model-checking#3640
* Update toolchain to 10/25 by @carolynzech in model-checking#3648
* Automatic toolchain upgrade to nightly-2024-10-26 by @github-actions in model-checking#3651
* Automatic toolchain upgrade to nightly-2024-10-27 by @github-actions in model-checking#3652
* Bump tests/perf/s2n-quic from `cd0314b` to `ed9db08` by @dependabot in model-checking#3655
* Automatic cargo update to 2024-10-28 by @github-actions in model-checking#3654
* Automatic toolchain upgrade to nightly-2024-10-28 by @github-actions in model-checking#3653
* Reduce the number of object bits for refcell test by @zhassan-aws in model-checking#3656
* Move any_slice_from_array to kani_core by @qinheping in model-checking#3646
* Upgrade toolchain to 2024-10-29 by @zhassan-aws in model-checking#3658
* Add a timeout option by @zhassan-aws in model-checking#3649
* Upgrade toolchain to 2024-10-30 by @tautschnig in model-checking#3661
* Upgrade Rust toolchain to 2024-10-31 by @zhassan-aws in model-checking#3668
* Upgrade toolchain to 2024-11-01 by @tautschnig in model-checking#3671
* Automatic toolchain upgrade to nightly-2024-11-02 by @github-actions in model-checking#3673
* Implement `Arbitrary` for `Range*` by @c410-f3r in model-checking#3666
* Automatic toolchain upgrade to nightly-2024-11-03 by @github-actions in model-checking#3674
* codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in model-checking#3675
* Automatic cargo update to 2024-11-04 by @github-actions in model-checking#3677
* Bump tests/perf/s2n-quic from `192de7d` to `65d55a4` by @dependabot in model-checking#3678
* Update dependencies following Audit workflow failure. by @remi-delmas-3000 in model-checking#3680
* Harness output individual files by @Alexander-Aghili in model-checking#3360
* Update Charon submodule to 2024-11-04 by @zhassan-aws in model-checking#3686
* Add support for float_to_int_unchecked by @zhassan-aws in model-checking#3660
* Change `same_allocation` to accept wide pointers by @celinval in model-checking#3684
* Automatic upgrade of CBMC from 6.3.1 to 6.4.0 by @github-actions in model-checking#3689
* Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in model-checking#3692
* Update cbmc-viewer to 3.10 by @remi-delmas-3000 in model-checking#3683
* Apply loop contracts only if there exists some usage by @qinheping in model-checking#3694
* Remove symtab json support by @celinval in model-checking#3695
* Remove CBMC viewer and visualize option by @zhassan-aws in model-checking#3699
* Ignore derivative in Cargo deny by @qinheping in model-checking#3708
* Upgrade Rust toolchain to 2024-11-08 by @zhassan-aws in model-checking#3703
* Automatic cargo update to 2024-11-11 by @github-actions in model-checking#3704
* Update verify-std-check workflow to enable loop contracts by @qinheping in model-checking#3705
* Automatic toolchain upgrade to nightly-2024-11-09 by @github-actions in model-checking#3709
* Bump tests/perf/s2n-quic from `65d55a4` to `cb41b35` by @dependabot in model-checking#3706
* Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in model-checking#3701
* Upgrade toolchain to nightly-2024-11-11 by @qinheping in model-checking#3710
* Automatic toolchain upgrade to nightly-2024-11-12 by @github-actions in model-checking#3713
* Update charon submodule by @zhassan-aws in model-checking#3716
* Revert "Ignore derivative in Cargo deny" by @qinheping in model-checking#3712
* Upgrade toolchain to nightly-2024-11-13 by @qinheping in model-checking#3715
* Automatic toolchain upgrade to nightly-2024-11-14 by @github-actions in model-checking#3719
* Automatic toolchain upgrade to nightly-2024-11-15 by @github-actions in model-checking#3720
* Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in model-checking#3644
* Improve Kani handling of function markers by @celinval in model-checking#3718
* Automatic toolchain upgrade to nightly-2024-11-16 by @github-actions in model-checking#3722
* Automatic toolchain upgrade to nightly-2024-11-17 by @github-actions in model-checking#3724
* Automatic cargo update to 2024-11-18 by @github-actions in model-checking#3723
* Bump tests/perf/s2n-quic from `cb41b35` to `4c3ba69` by @dependabot in model-checking#3725
* Automatic toolchain upgrade to nightly-2024-11-18 by @github-actions in model-checking#3727
* Enable contracts for const generic functions by @qinheping in model-checking#3726
* List Subcommand Improvements by @carolynzech in model-checking#3729
* Automatic toolchain upgrade to nightly-2024-11-19 by @github-actions in model-checking#3730
* add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in model-checking#3721
* Fix issues with how we compute DST size by @celinval in model-checking#3687
* Bump tests/perf/s2n-quic from `4c3ba69` to `c84ba19` by @dependabot in model-checking#3736
* Fix size and alignment computation for intrinsics by @celinval in model-checking#3734
* Automatic cargo update to 2024-11-25 by @github-actions in model-checking#3735
* Cleanup a few internal compiler deps by @celinval in model-checking#3739
* Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in model-checking#3742
* Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in model-checking#3744
* Update toolchain to nightly-2024-11-26 by @celinval in model-checking#3740
* Automatic upgrade of CBMC from 6.4.0 to 6.4.1 by @github-actions in model-checking#3748
* Automatic cargo update to 2024-12-02 by @github-actions in model-checking#3749
* Update download-artifact, upload-artifact and checkout to v4 by @thanhnguyen-aws in model-checking#3745
* Bump tests/perf/s2n-quic from `c84ba19` to `96d2e22` by @dependabot in model-checking#3750
* Upgrade toolchain to 2024-11-27 by @tautschnig in model-checking#3751
* Upgrade toolchain to 2024-11-28 by @tautschnig in model-checking#3753
* Setup/CI: cleanup Ubuntu 18.04 and cbmc-viewer left-overs and enable 24.04 by @tautschnig in model-checking#3758
* Automatic cargo update to 2024-12-09 by @github-actions in model-checking#3766
* Bump tests/perf/s2n-quic from `96d2e22` to `e4a2365` by @dependabot in model-checking#3767
* Upgrade toolchain to 2024-12-09 by @carolynzech in model-checking#3768
* Add out of bounds check for `offset` intrinsics by @celinval in model-checking#3755
* Upgrade toolchain to 2024-12-12 by @carolynzech in model-checking#3774
* Automatic toolchain upgrade to nightly-2024-12-13 by @github-actions in model-checking#3775
## New Contributors
* @c410-f3r made their first contribution in model-checking#3666
* @workingjubilee made their first contribution in model-checking#3675
* @Alexander-Aghili made their first contribution in model-checking#3360
* @AlgebraicWolf made their first contribution in model-checking#3692
* @thanhnguyen-aws made their first contribution in model-checking#3721
**Full Changelog**: model-checking/kani@kani-0.56.0...kani-0.57.0
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a new option,
--cbmc-timeoutwhich can be used for setting a timeout for the CBMC run.The timeout applies on a per-harness basis in the Kani run.
The implementation uses tokio to perform non-blocking reads from the CBMC process's
stdoutso that the timeout can be checked asynchronously.Call-outs:
There are other names I considered for the option:
--harness-timeout: This makes it clearer that the timeout applies to each individual harness (and not to the overall Kani run). It doesn't indicate that the timeout only applies to the CBMC portion of the flow though.--engine-timeout: This makes it a bit more general across multiple engine/backends. The notion of an engine is not really part of the Kani jargon currently though, so might not be clear to users.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.