Skip to content
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

Unify kani library and kani core logic #3333

Merged
merged 21 commits into from
Aug 6, 2024

Conversation

jaisnan
Copy link
Contributor

@jaisnan jaisnan commented Jul 9, 2024

  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 owner July 9, 2024 16:31
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Jul 9, 2024
@jaisnan jaisnan changed the title Cleanup duplicate Kani core Unify kani library and kani core Jul 9, 2024
@jaisnan jaisnan changed the title Unify kani library and kani core Unify kani library and kani core logic Jul 9, 2024
@celinval celinval requested a review from adpaco-aws July 9, 2024 18:58
Copy link
Contributor

@adpaco-aws adpaco-aws left a comment

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?

library/kani/src/lib.rs Outdated Show resolved Hide resolved
library/kani/src/vec.rs Outdated Show resolved Hide resolved
library/kani_core/src/lib.rs Outdated Show resolved Hide resolved
library/kani_macros/src/sysroot/contracts/shared.rs Outdated Show resolved Hide resolved
@jaisnan
Copy link
Contributor Author

jaisnan commented Jul 10, 2024

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 adpaco-aws July 12, 2024 15:42
@jaisnan jaisnan added this pull request to the merge queue Aug 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 queue Aug 6, 2024
@feliperodri feliperodri 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 2a0e9bd Aug 6, 2024
27 checks passed
@jaisnan jaisnan deleted the clean-kani-core branch August 6, 2024 16:57
github-merge-queue bot pushed a commit that referenced this pull request Aug 9, 2024
## 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 free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[I] Refactoring / Clean Up Refactoring or cleaning up of existing code Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants