kani-0.16.0

Kani Rust verifier release bundle version 0.16.0.

What's Changed

• Allow panic with args to be called in a const context by @zhassan-aws in #1918
• Add support for SIMD vector comparison intrinsics by @adpaco-aws in #1853
• Restore support for bitwise SIMD intrinsics by @adpaco-aws in #1893
• Restore support for some SIMD arithmetic intrinsics by @adpaco-aws in #1931
• Restore simd_extract and simd_insert intrinsics by @adpaco-aws in #1942
• Fix crash for unsupported crate types by @celinval in #1912
• Upgrade rust toolchain to 2022-11-20 by @zhassan-aws in #1927

Full Changelog: kani-0.15.0...kani-0.16.0

kani-0.15.0

Kani Rust verifier release bundle version 0.15.0.

What's Changed

• Allow assert with custom message to be used in const contexts by @zhassan-aws in #1858
• Fix unsized coercion of a struct element by @celinval in #1880
• Treat lack of proof harnesses as success by @tedinski in #1886
• Encode string literals as a byte array by @zhassan-aws in #1903
• Use <target>/kani as the target directory and clean at every cargo kani run by @celinval in #1847
• Upgrade rust toolchain to nightly-2022-11-06 by @danielsn in #1859
• Upgrade to CBMC 5.70 by @zhassan-aws in #1888

Full Changelog: kani-0.14.1...kani-0.15.0

kani-0.14.1

What's Changed

This patch adds Apple Silicon (aarch64-apple-darwin) to the supported platforms for the Kani installer.

• Add M1 to the list of supported targets by @zhassan-aws in #1839

Full Changelog: kani-0.14.0...kani-0.14.1

kani-0.14.0

Kani Rust verifier release bundle version 0.14.0.

What's Changed

• Fix assess with the MIR linker by changing reachability modes by @tedinski in #1816
• RFC for Function and Method Stubbing by @aaronbembenek-aws in #1723
• Fix conflicting C function definitions by @celinval in #1812
• Bump dependencies by @tedinski in #1800
• Upgrade to CBMC 5.69.1 (with fixes) by @adpaco-aws in #1811
• Upgrade the rust toolchain to nightly-2022-10-24 by @rahulku in #1830

Full Changelog: kani-0.13.0...kani-0.14.0

kani-0.13.0

Kani Rust verifier release bundle version 0.13.0.

What's Changed

Major changes

The MIR linker has been turned on by default. It leads to significant improvements in run times and fixes the issue with missing std functions. The legacy version of the linker is accessible through the --legacy-linker option.

Other changes

• Report failure even when CBMC crashes, refactor CBMC parser/renderer by @tedinski in #1742
• Supress symtab2gb output by @celinval in #1753
• Introduce prototype cargo-kani assess feature to help find places to start writing proofs by @tedinski in #1756
• Fix Kani crash with const-generic [e; N] expression by @tedinski in #1770
• Fix issue with mutable static from upstream crate by @celinval in #1761
• Use CustomCoerce to get info about the unsized cast by @celinval in #1754
• Fix undefined symbol errors when rustup defaults to nightly rust by @tedinski in #1771
• Do not apply Ubuntu 18.04 workaround if user has installed newer versions of Python by @tedinski in #1783
• Fix bug where 'kani' would not delete a temporary file by @tedinski in #1790
• Fix target selection for MIR Linker by @celinval in #1789
• Enable MIR Linker by default and adjust tests by @celinval in #1785
• Disable debug_asserts inside std due to poor UX by @celinval in #1791
• Update Kani to Rust nightly-2022-10-11 by @tedinski in #1788

Full Changelog: kani-0.12.0...kani-0.13.0

kani-0.12.0

Kani Rust verifier release bundle version 0.12.0.

What's Changed

The MIR linker flow is almost complete, and we're in the process of turning it on by default. It leads to significant improvements in run times and fixes the issue with missing std functions. We appreciate if you can give it a try and provide your feedback. To enable it, run cargo kani/kani with --enable-unstable --mir-linker.

• Add option to enable layout randomization by @giltho in #1623
• More reliable property attributes extraction by @adpaco-aws in #1514
• Link std functions under --mir-linker by @celinval in #1717
• Introduce (experimental, unstable) parallel runner for proof harnesses by @tedinski in #1726
• Improve messages for unsupported constructs by @tedinski in #1725
• Fix cargo kani --debug and remove debug logs from --verbose by @celinval in #1730
• Improve Kani run time through running the symbol table to goto binary conversion step in parallel with codegen by @danielsn in #1686
• Bump CBMC version to 5.67.0 by @zhassan-aws in #1739
• Upgrade toolchain to nightly-2022-09-13 by @celinval in #1737

Full Changelog: kani-0.11.0...kani-0.12.0

kani-0.11.0

Kani Rust verifier release bundle version 0.11.0.

What's Changed

• Only generate tests if the failure is reproducible by @celinval in #1629
• Add initial implementation of the reachability algorithm by @celinval in #1683
• Bump CBMC version to 5.66.0 by @zhassan-aws in #1699

Full Changelog: kani-0.10.0...kani-0.11.0

kani-0.10.0

Kani Rust verifier release bundle version 0.10.0.

What's Changed

• Make panic and assert const functions by @zhassan-aws in #1590
• Eliminate unused variable warnings in panic and unreachable macros by @zhassan-aws in #1583
• Add concrete playback support for multiple failing harnesses by @sanjit-bhat in #1558
• Fix generator layout and sizes by @fzaiser in #1607
• Update rustc to nightly-2022-08-30 by @zhassan-aws in #1624
• Bump CBMC to 5.65.1 by @zhassan-aws in #1630

Full Changelog: kani-0.9.0...kani-0.10.0

kani-0.9.0

Kani Rust verifier release bundle version 0.9.0.

Breaking Changes

• Remove any_raw() and Invariant by @celinval in #1534
  • Note - Use Arbitrary instead of Invariant. See here for more info

What's Changed

• Concrete playback feature by @sanjit-bhat in #1409
• Fix error message for missing functions by @adpaco-aws in #1513
• Add --workspace to cargo kani. by @YoshikiTakashima in #1530
• Add --all-features to cargo kani. by @YoshikiTakashima in #1532
• Add -p flag to cargo kani. by @YoshikiTakashima in #1559
• Fix issue with niche optimizations on signed values by @danielsn in #1542
• Ensure Kani does not continue execution past a panic by @tedinski in #1428
• Mitigate issue with dangling pointers and memcmp by @fzaiser in #1526
• Use assert args in an unreachable block to prevent spurious warnings and to check for errors by @zhassan-aws in #1561
• Update rustc to nightly-2022-08-16 by @danielsn in #1535
• Bump CBMC to 5.64.0 by @zhassan-aws in #1560

Full Changelog: kani-0.8.0...kani-0.9.0

kani-0.8.0

Kani Rust verifier release bundle version 0.8.0.

Breaking Changes

• Users previously implementing the Kani Invariant trait should switch to using Arbitrary. The tutorial has been updated with the new recommended approach.

What's Changed

• Replace CBMC output parser by @adpaco-aws in #1433
• Replace struct impl of Invariant by Arbitrary by @celinval in #1401
• Deprecate any_raw and Invariant by @celinval in #1415
• Add basic support for async/.await by @fzaiser in #1414
• Add a kani::futures library containing block_on by @fzaiser in #1427
• Support ThreadLocalRef by @fzaiser in #1452
• Use #[kani::proof] for both sync and async functions by @fzaiser in #1471
• Cargo kani now uses the workspace's target directory by @YoshikiTakashima in #1421
• Disable --slice-formula when generating traces and add a flag by @jaisnan in #1479
• Fix kani's overridding of print macros by @zhassan-aws in #1446
• (Optimization) Use CBMC's arithmetic operators that return both the result and whether it overflowed by @zhassan-aws in #1426
• (Improve trace quality) Cleanup rvalue_repeat by @danielsn in #1458
• (Improve trace quality) Cleanup TagEncoding::Direct by @danielsn in #1457
• Bump CBMC Viewer to 3.6 by @tedinski in #1405
• Bump CBMC to 5.63.0 by @zhassan-aws in #1463

Full Changelog: kani-0.7.0...kani-0.8.0