Verify CStr CloneToUninit and Index<RangeFrom> safety (Challenge 13)#543
Open
jrey8343 wants to merge 3 commits intomodel-checking:mainfrom
Open
Verify CStr CloneToUninit and Index<RangeFrom> safety (Challenge 13)#543jrey8343 wants to merge 3 commits intomodel-checking:mainfrom
jrey8343 wants to merge 3 commits intomodel-checking:mainfrom
Conversation
Add the final 2 verification harnesses to complete Challenge 13: - check_clone_to_uninit: Verifies the unsafe CloneToUninit impl for CStr correctly copies all bytes (including NUL terminator) and produces a valid CStr at the destination. Includes safety contract on clone_to_uninit requiring non-null dest pointer. - check_index_from: Verifies ops::Index<RangeFrom<usize>> for CStr produces a valid CStr that maintains the safety invariant and matches the expected tail of the original bytes. Both harnesses are bounded (MAX_SIZE=16/32) with appropriate unwind limits and verify the CStr is_safe() invariant holds.
The harness was timing out (10 min CBMC limit) due to expensive symbolic pointer arithmetic in clone_to_uninit combined with a symbolic-length verification loop. Fix: reduce MAX_SIZE from 16 to 8 bytes (sufficient to cover empty, single-char, and multi-char C strings) and remove the byte-by-byte verification loop (the CStr reconstruction check still validates the safety invariant).
jrey8343
force-pushed
the
challenge-13-cstr
branch
from
b3f7293 to
f0e5049
Compare
Author
|
CI is passing — ready for review. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
check_clone_to_uninit: Verifies the unsafeCloneToUninitimpl forCStrcorrectly copies all bytes including NUL terminator, with safety contract requiring non-null destcheck_index_from: Verifiesops::Index<RangeFrom<usize>>forCStrmaintains theis_safe()invariant on the resulting sub-CStrChanges
library/core/src/clone.rs: Added#[requires(!dest.is_null())]safety contract onCloneToUninit::clone_to_uninitforCStr, plususe crate::kanianduse safety::requiresimportslibrary/core/src/ffi/c_str.rs: Addedcheck_clone_to_uninitandcheck_index_fromharnesses in the existingmod verifyblockVerification
Both harnesses pass with Kani 0.65.0:
check_clone_to_uninit(MAX_SIZE=16, unwind=17): ~159scheck_index_from(MAX_SIZE=32, unwind=33): ~189sResolves
Challenge 13: Safety of
CStr(#150)Test plan
check_clone_to_uninitpasses Kani verificationcheck_index_frompasses Kani verification