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

Harnesses verifying slice types for add, sub and offset #179

Open
wants to merge 28 commits into
base: main
Choose a base branch
from
Open

Harnesses verifying slice types for add, sub and offset #179

wants to merge 28 commits into from

Conversation

szlee118
Copy link

Towards #76

Changes

Contracts Added:

  • Added contracts for <*mut T>::add, <*mut T>::sub, and <*mut T>::offset operations for raw pointers to slices.

Proofs Implemented:

  • Added proofs for the above contracts, verifying safety for the following slice pointee types using arrays:
  • All integer types (i8, i16, i32, etc.).
  • Tuples (composite types) (e.g., (i8, i8), (i32, f64, bool)).
  • Unit type (()).

Macro Definitions:

  • Introduced macros to simplify and automate harness generation:
  • One macro for add and sub operations on slices.
  • Another macro for offset operations on slices.

Array-Based Implementation for Slice Verification:

  • Arrays are used as a proxy for slices (as slices do not have a known length at compile time) to enable proper bounds checking and assumptions during verification.

This should be merged after another PR for dependency issues.

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

xsxszab and others added 25 commits October 7, 2024 12:44
@xsxszab
added common codes for all proof of contracts
9a8993d
@xsxszab
implemented integer type proof for contract for fn add, sub and offset
55950bb
@stogaru
Merge branch 'main' into verify/ptr_mut
ce13e8f
@stogaru
Adds proofs for tuple types
3682858
@stogaru
Renames harnesses
a6d4d62
@MayureshJoshi25
Added unit type proofs for mut ptr
dec8c30
@stogaru
Merge pull request #8 from stogaru/verify/ptr_mut_unit_types
2be7639 
Added unit type proofs for mut ptr
@xsxszab
Merge branch 'verify/ptr_mut' into verify/ptr_mut_integer_types
75179dc
@xsxszab
Merge pull request #6 from stogaru/verify/ptr_mut_integer_types
34c670e 
implemented integer type proof for contract for fn add, sub and offset
@stogaru
Merge branch 'verify/ptr_mut' into verify/ptr_mut_composite
66c956e
@stogaru
Merge pull request #7 from stogaru/verify/ptr_mut_composite
d9b8c65 
Verify/ptr mut composite
@stogaru
Combined macros
0faac46
@stogaru
Fixes a typo
82345de
@stogaru
Removes an unnecessary attribute
656209b
@stogaru
Merge pull request #9 from stogaru/verify/ptr_mut_combined
46e839c 
Combines macros for different types.
@xsxszab
refactored function contracts for add, sub and offset using the same_…
96a8a2e 
…allocation api, modified their proof for harness accordingly
@xsxszab
merged macros for add, sub and offset
852e96f
@xsxszab
updated function contracts and proof for contracts for add(), sub() a…
04bd61e 
…nd offset()
@xsxszab
added support for unit type pointers
7557fc5
@xsxszab
updated function contracts, removed unnecessary kani::assmue
76b2311
@xsxszab
added comments to function contracts
cb6a177
@xsxszab
Merge pull request #12 from stogaru/verify/ptr_mut_refactor_harness
6385d4a 
Verify/ptr mut refactor harness
@xsxszab
added comments for magic numbers
a079a7a
@stogaru
Merge branch 'main' into verify/ptr_mut
214f84d
@szlee118
Add slice harness for mut
b77ae5a 
Use as_mut_ptr
@szlee118 szlee118 requested a review from a team as a code owner November 22, 2024 19:58
@szlee118 szlee118 changed the title Verify/ptr mut slice types Verify/ptr mut slice types(add, sub and offset) Nov 22, 2024
@szlee118 szlee118 changed the title Verify/ptr mut slice types(add, sub and offset) Harnesses verifying slice types for add, sub and offset Nov 22, 2024
@szlee118
Copy link
Author

@feliperodri FYI

@tautschnig
Copy link
Member

@szlee118 #113 has been merged, but now conflicts need to be resolved on this one.

@szlee118
Copy link
Author

@tautschnig @feliperodri conflict resolved.

feliperodri
feliperodri reviewed Nov 28, 2024
View reviewed changes
Copy link

@feliperodri feliperodri left a comment

Choose a reason for hiding this comment

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

It seems there are still some conflicts. Could you check if the conflicts were successfully solved?

library/core/src/ptr/mut_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs Outdated Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs Show resolved Hide resolved
feliperodri
feliperodri reviewed Nov 28, 2024
View reviewed changes
library/core/src/ptr/mut_ptr.rs Show resolved Hide resolved
library/core/src/ptr/mut_ptr.rs
Comment on lines +2371 to +2372
// Constant for array size used in all tests, for performance reason
const ARRAY_SIZE: usize = 5;
Copy link

Choose a reason for hiding this comment

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

Isn't 5 too low? How is the verification performance numbers?

Copy link
Author

Choose a reason for hiding this comment

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

Explained in another PR's comment that 5 is enough for this case.
This performance statement is outdated, and has been removed by newest commit.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@xsxszab xsxszab xsxszab left review comments

@feliperodri feliperodri feliperodri left review comments

At least 1 approving review is required to merge this pull request.

Assignees

@szlee118 szlee118

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@szlee118 @tautschnig @feliperodri @xsxszab @stogaru @MayureshJoshi25 @carolynzech