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

Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_unchecked #193

Merged
merged 39 commits into from
Dec 12, 2024
Merged

Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_unchecked #193

merged 39 commits into from
Dec 12, 2024

Conversation

rajathkotyal
Copy link

@rajathkotyal rajathkotyal commented Nov 28, 2024 •
edited
Loading

Towards #150

Annotates and verifies the safety contracts for the following unsafe functions:

from_bytes_with_nul_uncheked core::ffi::c_str
strlen core::ffi::c_str

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

@rajathkotyal rajathkotyal requested a review from a team as a code owner November 28, 2024 06:14
@rajathkotyal rajathkotyal changed the title C0013-Cstr verify safety contracts of unsafe functions Cstr verify safety contracts of unsafe functions from_ptr, strlen, from_bytes_with_nul_uncheked - Stubbing Nov 28, 2024
@rajathkotyal rajathkotyal marked this pull request as draft November 28, 2024 09:54
@rajathkotyal rajathkotyal changed the title Cstr verify safety contracts of unsafe functions from_ptr, strlen, from_bytes_with_nul_uncheked - Stubbing Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_uncheked Dec 3, 2024
@rajathkotyal rajathkotyal marked this pull request as ready for review December 3, 2024 02:30
tautschnig
tautschnig approved these changes Dec 3, 2024
View reviewed changes
library/core/src/ffi/c_str.rs Outdated Show resolved Hide resolved
@Yenyun035
Copy link

Yenyun035 commented Dec 10, 2024 •
edited
Loading

That means we need to enable C-FFI support like #204

@celinval Got it. Thank you for mentioning that. This means #204 needs to be merged first.

Edit: I tried adding -Z c-ffi --output-format=old --no-assertion-reach-checks flags to run_kani.sh, it still failed with the same error.

@carolynzech
Copy link

@Yenyun035 can you fix the failing Rust tests and then we'll take a look if there's still issues?

@Yenyun035
Copy link

@carolynzech Sure. I annotated is_null_terminated helper function with #[cfg(kani)] now. I think it should fix the failed rust tests. If not, I'll try to figure out another solution.

github-merge-queue bot pushed a commit that referenced this pull request Dec 11, 2024
@rajathkotyal @Yenyun035
CStr : Proof for from_ptr with contract (#204)
9058f0b 
Towards #150

Similar PR Ref : #193 

Annotates and verifies the safety contracts for the unsafe function :
`from_ptr` - `core::ffi::c_str`

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

---------

Co-authored-by: Yenyun035 <57857379+Yenyun035@users.noreply.github.com>
Co-authored-by: Yenyun035 <yew005eng@gmail.com>
@tautschnig
Copy link
Member

@rajathkotyal Can I please ask you to resolve conflicts that arose with #204 now merged?

@Yenyun035
Copy link

@tautschnig Fixed. Thank you.

@tautschnig tautschnig enabled auto-merge December 11, 2024 21:10
@tautschnig tautschnig disabled auto-merge December 11, 2024 21:11
carolynzech
carolynzech approved these changes Dec 11, 2024
View reviewed changes
Copy link

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

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

Nice!

@carolynzech carolynzech changed the title Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_uncheked Cstr verify safety contracts of unsafe functions strlen, from_bytes_with_nul_unchecked Dec 11, 2024
@rajathkotyal
Copy link
Author

Thanks @Yenyun035 !

@carolynzech carolynzech added this pull request to the merge queue Dec 12, 2024
Merged via the queue into model-checking:main with commit eb21f69 Dec 12, 2024
8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Yenyun035 Yenyun035 Yenyun035 left review comments

@celinval celinval celinval left review comments

@carolynzech carolynzech carolynzech approved these changes

@tautschnig tautschnig tautschnig approved these changes

Assignees

@carolynzech carolynzech

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@rajathkotyal @Yenyun035 @celinval @carolynzech @tautschnig