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.

Sign up for GitHub

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

Jump to bottom

Function Contracts: Modify Slices #3295

Merged
merged 39 commits into from
Jul 17, 2024
Merged

Function Contracts: Modify Slices #3295

merged 39 commits into from
Jul 17, 2024

Conversation

pi314mm
Copy link
Contributor

@pi314mm pi314mm commented Jun 26, 2024

Using the __CPROVER_object_upto function to pass modifies clauses to asserts clauses in goto for rust slices.

Resolves #2908

Todo: Testing and Documentatiaon

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

@pi314mm pi314mm added [C] Feature / Enhancement A new feature request or enhancement to an existing feature. Z-BenchCI Tag a PR to run benchmark CI labels Jun 26, 2024
@pi314mm pi314mm added this to the Function Contracts milestone Jun 26, 2024
@pi314mm pi314mm self-assigned this Jun 26, 2024
@pi314mm
Copy link
Contributor Author

pi314mm commented Jun 28, 2024 •
edited
Loading

We are currently relying on kani::any_modifies markers that are compiled away into kani::any. The purpose of them is to allow for the function contracts to type check even if the modifies data does not implement Arbitrary as long as stub_contract is not used.

Instead of the kani::any_modifies, we should be using kani::havoc that indicates that the parameter should be dereferenced and assigned to, which will allow us to handle both slim pointers and fat pointers, as the method to assign to them is different.

@pi314mm pi314mm marked this pull request as ready for review July 8, 2024 19:08
@pi314mm pi314mm requested a review from a team as a code owner July 8, 2024 19:08
celinval
celinval reviewed Jul 8, 2024
View reviewed changes
library/kani/src/lib.rs Outdated Show resolved Hide resolved
celinval
celinval requested changes Jul 9, 2024
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Thanks for doing this. I haven't reviewed the compiler changes yet.

library/kani/src/lib.rs Outdated Show resolved Hide resolved
library/kani/src/lib.rs Outdated Show resolved Hide resolved
library/kani/src/lib.rs Outdated Show resolved Hide resolved
library/kani/src/lib.rs Outdated Show resolved Hide resolved
celinval
celinval approved these changes Jul 16, 2024
View reviewed changes
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

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

Thanks!

kani-compiler/src/kani_middle/transform/contracts.rs Show resolved Hide resolved
@pi314mm pi314mm mentioned this pull request Jul 16, 2024
Open
@feliperodri feliperodri enabled auto-merge (squash) July 17, 2024 15:40
@feliperodri feliperodri merged commit 852fd8f into model-checking:main Jul 17, 2024
25 checks passed
@pi314mm pi314mm deleted the modifies_fat branch July 18, 2024 00:35
celinval added a commit to celinval/kani-dev that referenced this pull request Jul 25, 2024
@celinval
Add missing functionalities to kani_core
b52cb34 
  - Add Arbitrary for array
  - Add Arbitrary for tuples
  - Add missing changes from modifies slices (model-checking#3295)

Note that for adding `any_array` I had to cleanup the unnecessary usage
of constant parameters from `kani::any_raw`.
@celinval celinval mentioned this pull request Jul 25, 2024
Merged
celinval added a commit that referenced this pull request Jul 25, 2024
@celinval
Add missing functionalities to kani_core (#3384)
b18698f 
  - Add Arbitrary for array
  - Add Arbitrary for tuples
  - Add missing changes from modifies slices (#3295)

Note that for adding `any_array` I had to cleanup the unnecessary usage
of constant parameters from `kani::any_raw`.
@feliperodri feliperodri mentioned this pull request Aug 8, 2024
Merged
github-merge-queue bot 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 free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@feliperodri feliperodri feliperodri approved these changes

@celinval celinval celinval approved these changes

Assignees

@pi314mm pi314mm

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
Function Contracts
Development

Successfully merging this pull request may close these issues.

Support for slices in modifies clauses
3 participants
@pi314mm @feliperodri @celinval