Skip to content

Unify kani library and kani core logic - #3333

Merged
jaisnan merged 21 commits into
model-checking:mainfrom
jaisnan:clean-kani-core
Aug 6, 2024
Merged

Unify kani library and kani core logic#3333
jaisnan merged 21 commits into
model-checking:mainfrom
jaisnan:clean-kani-core

Conversation

@jaisnan

@jaisnanjaisnan commented Jul 9, 2024•
edited
Loading

Copy link
Copy Markdown
Contributor
  1. Unifies Kani library and kani_core for Arbitrary, mem and intrinsics along with the internal module.
  2. Adjusts some regression expected files to reflect the new underlying source of Arbitrary

Related to ##3257

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

@jaisnan
jaisnan requested a review from a team as a code ownerJuly 9, 2024 16:31
@github-actionsgithub-actionsBot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jul 9, 2024
@jaisnanjaisnan changed the title Cleanup duplicate Kani coreUnify kani library and kani coreJul 9, 2024
@jaisnanjaisnan changed the title Unify kani library and kani coreUnify kani library and kani core logicJul 9, 2024
@celinval
celinval requested a review from adpacoJuly 9, 2024 18:58
adpaco
adpaco reviewed Jul 10, 2024
View reviewed changes

@adpacoadpaco left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In order for this cleanup to work, we need to remove the unstable feature being inserted into every kani_sysroot related compilation. This does not change anything for the end user, as long as they add

#[unstable(feature="kani", issue="none")]

when they invoke kani in core.

Do you mean that if a user wants to analyze core or std with Kani, they need to manually add this attribute to the Kani functions and compile from source?

Comment threadlibrary/kani/src/lib.rs Outdated
Comment threadlibrary/kani/src/vec.rs
Comment threadlibrary/kani_core/src/lib.rs
Comment threadlibrary/kani_macros/src/sysroot/contracts/shared.rs Outdated
Comment threadtests/expected/function-contract/modifies/check_invalid_modifies.expected Outdated
@jaisnan

jaisnan commented Jul 10, 2024

Copy link
Copy Markdown
ContributorAuthor

In order for this cleanup to work, we need to remove the unstable feature being inserted into every kani_sysroot related compilation. This does not change anything for the end user, as long as they add

#[unstable(feature="kani", issue="none")]

when they invoke kani in core.

Do you mean that if a user wants to analyze core or std with Kani, they need to manually add this attribute to the Kani functions and compile from source?

No, what I meant was that they need to add this to their invocation below cfg(kani) like we do here.

@jaisnan
jaisnan requested a review from adpacoJuly 12, 2024 15:42
celinval
celinval reviewed Jul 16, 2024
View reviewed changes
Comment threadlibrary/kani_core/src/lib.rs
@jaisnanjaisnan mentioned this pull request Jul 24, 2024
Merged
@jaisnan
jaisnan added this pull request to the merge queueAug 6, 2024
@jaisnan
jaisnan removed this pull request from the merge queue due to a manual request Aug 6, 2024
@jaisnan
jaisnan added this pull request to the merge queueAug 6, 2024
@feliperodrifeliperodri added the [I] Refactoring / Clean Up Refactoring or cleaning up of existing code label Aug 6, 2024
Merged via the queue into model-checking:main with commit 2a0e9bdAug 6, 2024
@jaisnan
jaisnan deleted the clean-kani-core branch August 6, 2024 16:57
@feliperodrifeliperodri mentioned this pull request Aug 8, 2024
Merged
github-merge-queueBot pushed a commit that referenced this pull request Aug 9, 2024
@feliperodri
Bump Kani version to 0.54.0 (#3430)
7a6f1a4
## 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
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@celinvalcelinvalcelinval left review comments
@feliperodrifeliperodrifeliperodri approved these changes
@adpacoadpacoAwaiting requested review from adpaco

Assignees

@jaisnanjaisnan

Labels

[I] Refactoring / Clean UpRefactoring or cleaning up of existing codeZ-EndToEndBenchCITag a PR to run benchmark CI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@jaisnan@feliperodri@celinval@adpaco