Skip to content

Contract & Harnesses for byte_sub, offset, map_addr and with_addr #107

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

Merged
merged 52 commits into from
Dec 11, 2024
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
52 commits
Select commit Hold shift + click to select a range
0bb80ab
byte_sub and offset
Dhvani-Kapadia Oct 5, 2024
0a2913f
contract and harness for byte_sub and offset
Dhvani-Kapadia Oct 7, 2024
77e8865
editing the mod.rs file(#91)
Dhvani-Kapadia Oct 7, 2024
bcfca87
Delete library/target/.rustc_info.json
Dhvani-Kapadia Oct 11, 2024
a1fc1ae
Update non_null.rs
Dhvani-Kapadia Oct 11, 2024
29f740c
Update mod.rs
Dhvani-Kapadia Oct 11, 2024
c03befa
Delete library/core/src/ptr/target/kani_verify_std/Cargo.toml
Dhvani-Kapadia Oct 11, 2024
bf29680
Delete library/core/src/ptr/target directory
Dhvani-Kapadia Oct 11, 2024
99d4f9e
Delete library/target/kani_verify_std directory
Dhvani-Kapadia Oct 11, 2024
bea518b
Contract and harness for map_addr and with_addr
Dhvani-Kapadia Oct 13, 2024
6d18084
removed kani::requires and self is non null
Dhvani-Kapadia Oct 16, 2024
73eb7cc
resolving conflict
Dhvani-Kapadia Nov 14, 2024
1df5f54
Delete verify-error.log
Dhvani-Kapadia Nov 14, 2024
5972e04
Revised contracts
Dhvani-Kapadia Nov 15, 2024
51c2336
Merge branch 'dhvani_develop' of https://github.com/danielhumanmod/ve…
Dhvani-Kapadia Nov 15, 2024
f5538fd
removing comments
Dhvani-Kapadia Nov 15, 2024
bcb17b1
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 15, 2024
7e5584b
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 15, 2024
bc40a6b
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 16, 2024
a27cf5e
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 18, 2024
7b7ec2f
local changes
Dhvani-Kapadia Nov 19, 2024
78d7894
conflicts merged
Dhvani-Kapadia Nov 19, 2024
3c7e711
removing comments from harness
Dhvani-Kapadia Nov 19, 2024
a61ce84
resolved conflicts with main
Dhvani-Kapadia Nov 19, 2024
dcd0890
resolving merge from main conflicts
Dhvani-Kapadia Nov 19, 2024
4818616
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 22, 2024
2253393
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 22, 2024
5e2ac1a
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 22, 2024
105c2ac
Update library/core/src/ptr/non_null.rs
Dhvani-Kapadia Nov 22, 2024
0cb1044
merged with main
Dhvani-Kapadia Nov 25, 2024
6d0e284
ran rustfmt on the file
Dhvani-Kapadia Nov 25, 2024
59c349c
update
Dhvani-Kapadia Nov 25, 2024
37784bb
Reverted to commit 0cb1044
Dhvani-Kapadia Nov 26, 2024
e9ccbd3
Updated submodule reference for library/stdarch
Dhvani-Kapadia Nov 26, 2024
4f5a3a1
reverting to 37784bb
Dhvani-Kapadia Nov 26, 2024
ceb2c52
modified stdarch
Dhvani-Kapadia Nov 26, 2024
2df925e
merged from main
Dhvani-Kapadia Nov 26, 2024
fe0eb58
Revert change to stdarch
zhassan-aws Nov 27, 2024
9196acb
Merge branch 'main' into dhvani_develop
Dhvani-Kapadia Nov 27, 2024
fda97db
Update non_null.rs
Dhvani-Kapadia Nov 27, 2024
6898d9f
Update non_null.rs
Dhvani-Kapadia Nov 27, 2024
172f150
Update non_null.rs
Dhvani-Kapadia Nov 27, 2024
d743938
Update non_null.rs
Dhvani-Kapadia Nov 27, 2024
3f9f593
Update non_null.rs
Dhvani-Kapadia Nov 27, 2024
5e23b52
Merge branch 'main' into dhvani_develop
Dhvani-Kapadia Dec 4, 2024
1246d25
same_allocation offset
Dhvani-Kapadia Dec 4, 2024
8b34f00
Merge branch 'dhvani_develop' of https://github.com/danielhumanmod/ve…
Dhvani-Kapadia Dec 4, 2024
4ce3119
using ub_checks
Dhvani-Kapadia Dec 6, 2024
bcf4586
Merge branch 'main' into dhvani_develop
tautschnig Dec 10, 2024
6268a5f
Merge branch 'main' into dhvani_develop
tautschnig Dec 10, 2024
659b104
Merge branch 'main' into dhvani_develop
carolynzech Dec 11, 2024
d771b0c
Merge branch 'main' into dhvani_develop
tautschnig Dec 11, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion library/core/src/num/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1585,7 +1585,6 @@ from_str_radix_size_impl! { i16 isize, u16 usize }
from_str_radix_size_impl! { i32 isize, u32 usize }
#[cfg(target_pointer_width = "64")]
from_str_radix_size_impl! { i64 isize, u64 usize }

#[cfg(kani)]
#[unstable(feature = "kani", issue = "none")]
mod verify {
Expand Down
53 changes: 53 additions & 0 deletions library/core/src/ptr/non_null.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
use crate::cmp::Ordering;
use crate::marker::Unsize;
//use crate::num::NonZeroUsize;
use crate::mem::{MaybeUninit, SizedTypeProperties};
use crate::num::NonZero;
use crate::ops::{CoerceUnsized, DispatchFromDyn};
Expand Down Expand Up @@ -476,6 +477,12 @@ impl<T: ?Sized> NonNull<T> {
#[must_use = "returns a new pointer rather than modifying its argument"]
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
// Requires that the input pointer is not null
#[kani::requires(!self.as_ptr().is_null())]
// Requires that multiplying count by the size of T doesn't overflow isize
#[kani::requires(count.checked_mul(core::mem::size_of::<T>() as isize).is_some())]
//Two conditions for postconditions: 1.Resulting pointer is not null 2.Safe operation of pointer arithmetic
#[kani::ensures(|result: &NonNull<T>| !result.as_ptr().is_null() && (result.as_ptr() as isize) == (self.as_ptr() as isize).wrapping_add(count.wrapping_mul(core::mem::size_of::<T>() as isize)))]
pub const unsafe fn offset(self, count: isize) -> Self
where
T: Sized,
Expand Down Expand Up @@ -663,6 +670,12 @@ impl<T: ?Sized> NonNull<T> {
#[rustc_allow_const_fn_unstable(set_ptr_value)]
#[stable(feature = "non_null_convenience", since = "1.80.0")]
#[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
//Requires that the input pointer is not null
#[kani::requires(!self.as_ptr().is_null())]
// Requires that count doesnt exceed Max
#[kani::requires(count <= isize::MAX as usize)]
//Ensures that result is not null
#[kani::ensures(|result: &NonNull<T>| !result.as_ptr().is_null())]
pub const unsafe fn byte_sub(self, count: usize) -> Self {
// SAFETY: the caller must uphold the safety contract for `sub` and `byte_sub` has the same
// safety contract.
Expand Down Expand Up @@ -1803,4 +1816,44 @@ mod verify {
let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() };
let _ = NonNull::new(maybe_null_ptr);
}
#[kani::proof_for_contract(NonNull::byte_sub)]
pub fn non_null_check_byte_sub() {
// Initializing array of size 10000
const ARR_SIZE: usize = 100000;
let arr: [i32; ARR_SIZE] = kani::any();
//Randomizing start pointer within array
let offset = kani::any_where(|x| *x <= ARR_SIZE);
// Create a NonNull pointer to the end of the array
let raw_ptr: *mut i32 = unsafe { arr.as_ptr().add(offset) as *mut i32 };
let ptr = unsafe { NonNull::new(raw_ptr).unwrap() };
// Choose an arbitrary count to subtract
let count: usize = kani::any();
// Ensure that the subtraction doesnt go out of bounds of array
kani::assume(count < ARR_SIZE - offset);
unsafe {
// Perform the byte_sub operation
let result = ptr.byte_sub(count);
}}

#[kani::proof_for_contract(NonNull::offset)]
pub fn non_null_check_offset(){
//Initializing array of size 10000
const ARR_SIZE: usize = 10000;
let arr: [i32; ARR_SIZE] = kani::any();
// Randomizing start pointer within array
let start_offset = kani::any_where(|x| *x < ARR_SIZE);
// Creating a NonNull pointer to a random position within the array
let ptr = unsafe { NonNull::new(arr.as_ptr().add(start_offset) as *mut i32).unwrap() };
// Choose an arbitrary count to offset
let count: isize = kani::any();
// Constraining the count to ensure it doesn't go out of bounds
kani::assume(
(count >= 0 && (count as usize) < ARR_SIZE - start_offset) ||
(count < 0 && count.unsigned_abs() <= start_offset)
);
unsafe {
// Perform the offset operation
let result = ptr.offset(count);
}
}
}
6 changes: 6 additions & 0 deletions library/core/src/ptr/target/kani_verify_std/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
[package]
name = "kani_verify_std"
version = "0.1.0"
edition = "2021"

[dependencies]
14 changes: 14 additions & 0 deletions library/core/src/ptr/target/kani_verify_std/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
pub fn add(left: u64, right: u64) -> u64 {
left + right
}

#[cfg(test)]
mod tests {
use super::*;

#[test]
fn it_works() {
let result = add(2, 2);
assert_eq!(result, 4);
}
}
1 change: 1 addition & 0 deletions library/target/.rustc_info.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc_fingerprint":16687169700156757383,"outputs":{"10106512464066337823":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.dylib\nlib___.dylib\nlib___.a\nlib___.dylib\n/Users/dhvanikapadia/.rustup/toolchains/nightly-2024-09-03-x86_64-apple-darwin\noff\npacked\nunpacked\n___\ndebug_assertions\nfmt_debug=\"full\"\nkani_host\noverflow_checks\npanic=\"unwind\"\nproc_macro\nrelocation_model=\"pic\"\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"\"\ntarget_family=\"unix\"\ntarget_feature=\"cmpxchg16b\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"lahfsahf\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_feature=\"sse3\"\ntarget_feature=\"sse4.1\"\ntarget_feature=\"ssse3\"\ntarget_has_atomic\ntarget_has_atomic=\"128\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_has_atomic_equal_alignment=\"128\"\ntarget_has_atomic_equal_alignment=\"16\"\ntarget_has_atomic_equal_alignment=\"32\"\ntarget_has_atomic_equal_alignment=\"64\"\ntarget_has_atomic_equal_alignment=\"8\"\ntarget_has_atomic_equal_alignment=\"ptr\"\ntarget_has_atomic_load_store\ntarget_has_atomic_load_store=\"128\"\ntarget_has_atomic_load_store=\"16\"\ntarget_has_atomic_load_store=\"32\"\ntarget_has_atomic_load_store=\"64\"\ntarget_has_atomic_load_store=\"8\"\ntarget_has_atomic_load_store=\"ptr\"\ntarget_os=\"macos\"\ntarget_pointer_width=\"64\"\ntarget_thread_local\ntarget_vendor=\"apple\"\nub_checks\nunix\n","stderr":""},"3303698679050187852":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.dylib\nlib___.dylib\nlib___.a\nlib___.dylib\n/Users/dhvanikapadia/.rustup/toolchains/nightly-2024-09-03-x86_64-apple-darwin\noff\npacked\nunpacked\n___\ndebug_assertions\nfmt_debug=\"full\"\nkani\noverflow_checks\npanic=\"abort\"\nproc_macro\nrelocation_model=\"pic\"\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"\"\ntarget_family=\"unix\"\ntarget_has_atomic\ntarget_has_atomic=\"128\"\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_has_atomic_equal_alignment=\"128\"\ntarget_has_atomic_equal_alignment=\"16\"\ntarget_has_atomic_equal_alignment=\"32\"\ntarget_has_atomic_equal_alignment=\"64\"\ntarget_has_atomic_equal_alignment=\"8\"\ntarget_has_atomic_equal_alignment=\"ptr\"\ntarget_has_atomic_load_store\ntarget_has_atomic_load_store=\"128\"\ntarget_has_atomic_load_store=\"16\"\ntarget_has_atomic_load_store=\"32\"\ntarget_has_atomic_load_store=\"64\"\ntarget_has_atomic_load_store=\"8\"\ntarget_has_atomic_load_store=\"ptr\"\ntarget_os=\"macos\"\ntarget_pointer_width=\"64\"\ntarget_thread_local\ntarget_vendor=\"apple\"\nub_checks\nunix\n","stderr":""},"4614504638168534921":{"success":true,"status":"","code":0,"stdout":"rustc 1.83.0-nightly (bd53aa3bf 2024-09-02)\nbinary: rustc\ncommit-hash: bd53aa3bf7a24a70d763182303bd75e5fc51a9af\ncommit-date: 2024-09-02\nhost: x86_64-apple-darwin\nrelease: 1.83.0-nightly\nLLVM version: 19.1.0\n","stderr":""}},"successes":{}}
6 changes: 6 additions & 0 deletions library/target/kani_verify_std/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
[package]
name = "kani_verify_std"
version = "0.1.0"
edition = "2021"

[dependencies]
14 changes: 14 additions & 0 deletions library/target/kani_verify_std/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
pub fn add(left: u64, right: u64) -> u64 {
left + right
}

#[cfg(test)]
mod tests {
use super::*;

#[test]
fn it_works() {
let result = add(2, 2);
assert_eq!(result, 4);
}
}
Loading