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

Contracts & Harnesses for wrapping_shr #123

Merged

Conversation

MWDZ
Copy link

@MWDZ MWDZ commented Oct 19, 2024

Towards #59

Changes
Added contracts for wrapping_shr (located in library/core/src/num/int_macros.rs and uint_macros.rs)
Added harnesses for wrapping_shr of each integer type
i8, i16, i32, i64, i128, isize, u8, u16, u32, u64, u128, usize --- 12 harnesses in total.
Revalidation
Per the discussion in #59, we have to build and run Kani from feature/verify-rust-std branch.
To revalidate the verification results, run the following command. <harness_to_run> can be either num::verify to run all harnesses or num::verify::<harness_name> (e.g. checked_wrapping_shl_i8) to run a specific harness.

kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates

All harnesses should pass the default checks (1251 checks where 1 unreachable).

SUMMARY:
 ** 0 of 161 failed (1 unreachable)

VERIFICATION:- SUCCESSFUL
Verification Time: 0.32086188s

Complete - 12 successfully verified harnesses, 0 failures, 12 total.

Example of the unreachable check:

Check 9: num::<impl i8>::wrapping_shr.assertion.1
	 - Status: UNREACHABLE
	 - Description: "attempt to subtract with overflow"
	 - Location: library/core/src/num/int_macros.rs:2199:42 in function num::<impl i8>::wrapping_shr

@MWDZ MWDZ requested a review from a team as a code owner October 19, 2024 05:57
@MWDZ MWDZ marked this pull request as draft October 19, 2024 05:58
@MWDZ MWDZ marked this pull request as ready for review October 19, 2024 06:01
Copy link

@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.

Awesome! Thanks

@celinval celinval enabled auto-merge (squash) October 22, 2024 00:52
@celinval celinval merged commit a636c05 into model-checking:main Oct 22, 2024
7 of 8 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants