kani-0.55.0

Kani Rust verifier release bundle version 0.55.0.

Major/Breaking Changes

• Coverage reporting in Kani is now source-based instead of line-based.
  Consequently, the unstable -Zline-coverage flag has been replaced with a -Zsource-coverage one.
  Check the Source-Coverage RFC for more details.
• Several improvements were made to the memory initialization checks. The current state is summarized in #3300. We welcome your feedback!

What's Changed

• Update CBMC build instructions for Amazon Linux 2 by @tautschnig in #3431
• Implement memory initialization state copy functionality by @artemagvanian in #3350
• Make points-to analysis handle all intrinsics explicitly by @artemagvanian in #3452
• Avoid corner-cases by grouping instrumentation into basic blocks and using backward iteration by @artemagvanian in #3438
• Fix ICE due to mishandling of Aggregate rvalue for raw pointers to str by @celinval in #3448
• Basic support for memory initialization checks for unions by @artemagvanian in #3444
• Adopt Rust's source-based code coverage instrumentation by @adpaco-aws in #3119
• Extra tests and bug fixes to the delayed UB instrumentation by @artemagvanian in #3419
• Partially integrate uninit memory checks into verify_std by @artemagvanian in #3470
• Rust toolchain upgraded to nightly-2024-09-03 by @jaisnan @carolynzech

Full Changelog: kani-0.54.0...kani-0.55.0

kani-0.54.0

Major Changes

• We added support for slices in the #[kani::modifies(...)] clauses when using function contracts.
• We introduce an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros.
• We enabled support for concrete playback for harness that contains stubs or function contracts.
• We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.

Breaking Changes

• The -Z ptr-to-ref-cast-checks option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.

What's Changed

• Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in #3332
• Fix visibility of some Kani intrinsics by @artemagvanian in #3323
• Function Contracts: Modify Slices by @pi314mm in #3295
• Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in #3344
• Add support for global transformations by @artemagvanian in #3348
• Enable an #[safety_constraint(...)] attribute helper for the Arbitrary and Invariant macros by @adpaco-aws in #3283
• Fix contract handling of promoted constants and constant static by @celinval in #3305
• Bump CBMC Viewer to 3.9 by @tautschnig in #3373
• Update to CBMC version 6.1.1 by @tautschnig in #2995
• Define a struct-level #[safety_constraint(...)] attribute by @adpaco-aws in #3270
• Enable concrete playback for contract and stubs by @celinval in #3389
• Add code scanner tool by @celinval in #3120
• Enable contracts in associated functions by @celinval in #3363
• Enable log2*, log10* intrinsics by @tautschnig in #3001
• Enable powif* intrinsics by @tautschnig in #2999
• Enable fma* intrinsics by @tautschnig in #3002
• Enable sqrt* intrinsics by @tautschnig in #3000
• Remove assigns clause for ZST pointers by @carolynzech in #3417
• Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in #3374
• Unify kani library and kani core logic by @jaisnan in #3333
• Stabilize pointer-to-reference cast validity checks by @artemagvanian in #3426
• Rust toolchain upgraded to nightly-2024-08-07 by @jaisnan @qinheping @tautschnig @feliperodri

New Contributors

• @carolynzech made their first contribution in #3387

Full Changelog: kani-0.53.0...kani-0.54.0

kani-0.53.0

Major Changes

• The --visualize option is being deprecated and will be removed in a future release. Consider using the --concrete-playback option instead.
• The -Z ptr-to-ref-cast-checks option is being introduced to check pointer validity when casting raw pointers to references. The feature is currently behind an unstable flag but is expected to be stabilized in a future release once remaining performance issues have been resolved.
• The -Z uninit-checks option is being introduced to check memory initialization. The feature is currently behind an unstable flag and also requires the -Z ghost-state option.

Breaking Changes

• Remove support for the unstable argument --function by @celinval in #3278
• Remove deprecated --enable-stubbing by @celinval in #3309

What's Changed

• Change ensures into closures by @pi314mm in #3207
• (Re)introduce Invariant trait by @adpaco-aws in #3190
• Remove empty box creation from contracts impl by @celinval in #3233
• Add a new verify-std subcommand to Kani by @celinval in #3231
• Inject pointer validity check when casting raw pointers to references by @artemagvanian in #3221
• Do not turn trivially diverging loops into assume(false) by @tautschnig in #3223
• Fix "unused mut" warnings created by generated code. by @jsalzbergedu in #3247
• Refactor stubbing so Kani compiler only invoke rustc once per crate by @celinval in #3245
• Use cfg=kani_host for host crates by @tautschnig in #3244
• Add intrinsics and Arbitrary support for no_core by @jaisnan in #3230
• Contracts: Avoid attribute duplication and const function generation for constant function by @celinval in #3255
• Fix contract of constant fn with effect feature by @celinval in #3259
• Fix typed_swap for ZSTs by @tautschnig in #3256
• Add a #[derive(Invariant)] macro by @adpaco-aws in #3250
• Contracts: History Expressions via "old" monad by @pi314mm in #3232
• Function Contracts: remove instances of _renamed by @pi314mm in #3274
• Deprecate --visualize in favor of concrete playback by @celinval in #3281
• Fix operand in fat pointer comparison by @pi314mm in #3297
• Function Contracts: Closure Type Inference by @pi314mm in #3307
• Add support for f16 and f128 for toolchain upgrade to 6/28 by @jaisnan in #3306
• Towards Proving Memory Initialization by @artemagvanian in #3264
• Rust toolchain upgraded to nightly-2024-07-01 by @tautschnig @celinval @jaisnan @adpaco-aws

Full Changelog: kani-0.52.0...kani-0.53.0

kani-0.52.0

What's Changed

• New section about linter configuraton checking in the doc by @remi-delmas-3000 in #3198
• Fix {,e}println!() by @GrigorenkoPV in #3209
• Contracts for a few core functions by @celinval in #3107
• Add simple API for shadow memory by @zhassan-aws in #3200
• Upgrade Rust toolchain to 2024-05-28 by @zhassan-aws @remi-delmas-3000 @qinheping

Full Changelog: kani-0.51.0...kani-0.52.0

kani-0.51.0

Kani Rust verifier release bundle version 0.51.0.

What's Changed

• Do not assume that ZST-typed symbols refer to unique objects by @tautschnig in #3134
• Remove kani::Arbitrary from the modifies contract instrumentation by @feliperodri in #3169
• Emit source locations whenever possible to ease debugging and coverage reporting by @tautschnig in #3173
• Rust toolchain upgraded to nightly-2024-04-21 by @celinval

Full Changelog: kani-0.50.0...kani-0.51.0

kani-0.50.0

Major Changes

• Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (#3138).

What's Changed

• Implement valid value check for write_bytes by @celinval in #3108
• Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval

Full Changelog: kani-0.49.0...kani-0.50.0

kani-0.49.0

What's Changed

• Disable removal of storage markers by @zhassan-aws in #3083
• Ensure storage markers are kept in std code by @zhassan-aws in #3080
• Implement validity checks by @celinval in #3085
• Allow modifies clause for verification only by @feliperodri in #3098
• Add optional scatterplot to benchcomp output by @tautschnig in #3077
• Expand ${var} in benchcomp variant env by @karkhaz in #3090
• Add benchcomp filter command by @karkhaz in #3105
• Upgrade Rust toolchain to 2024-03-29 by @zhassan-aws @celinval @adpaco-aws @feliperodri

Full Changelog: kani-0.48.0...kani-0.49.0

kani-0.48.0

Major Changes

• We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in #3063

What's Changed

• Fix codegen_atomic_binop for atomic_ptr by @qinheping in #3047
• Retrieve info for recursion tracker reliably by @feliperodri in #3045
• Add --use-local-toolchain to Kani setup by @jaisnan in #3056
• Replace internal reverse_postorder by a stable one by @celinval in #3064
• Add option to override --crate-name from kani by @adpaco-aws in #3054
• Add method to assert a pointer is valid by @celinval in #3062
• Rust toolchain upgraded to 2024-03-11 by @adpaco-ws @celinval @zyadh

Full Changelog: kani-0.47.0...kani-0.48.0

kani-0.47.0

What's Changed

• Upgrade toolchain to 2024-02-14 by @zhassan-aws in #3036

Full Changelog: kani-0.46.0...kani-0.47.0

kani-0.46.0

What's Changed

• modifies Clauses for Function Contracts by @JustusAdam in #2800
• Fix ICEs due to mismatched arguments by @celinval in #2994. Resolves the following issues:
  • #2260
  • #2312
• Enable powf*, exp*, log* intrinsics by @tautschnig in #2996
• Upgrade Rust toolchain to nightly-2024-01-25 by @celinval @feliperodri @qinheping

Full Changelog: kani-0.45.0...kani-0.46.0