Merge branch 'main' into dhvani_mem

Author: QinyuanWu

.github/ISSUE_TEMPLATE/tool_application.md

@@ -0,0 +1,10 @@
+---
+name: Tool Application
+about: Submit a new tool application
+title: "[Tool Application] "
+labels: Tool Application
+---
+
+<!--
+Please see https://model-checking.github.io/verify-rust-std/tool_template.html for the application template.
+-->

doc/src/SUMMARY.md

@@ -19,7 +19,7 @@
   - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
   - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md)
   - [6: Safety of `NonNull`](./challenges/0006-nonnull.md)
-  - [7: Safety of Methods for Atomic Types and `ReentrantLock`](./challenges/0007-atomic-types.md)
+  - [7: Safety of Methods for Atomic Types & Atomic Intrinsics](./challenges/0007-atomic-types.md)
   - [8: Contracts for SmallSort](./challenges/0008-smallsort.md)
   - [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md)
   - [10: Memory safety of String](./challenges/0010-string.md)

doc/src/general-rules.md

@@ -69,20 +69,17 @@ Follow the following steps to create a new proposal:
 
 ## Tool Applications
 
-Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools):
-
-* Any new tool that participants want to enable will require an application using the [tool application template](./tool_template.md).
-* The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS
-* A new tool application should clearly specify the differences to existing techniques and provide sufficient background
-  of why this is needed.
-* The tool application should also include mechanisms to audit its implementation and correctness.
-* Once the tool is approved, the participant needs to create a PR that creates a new action that runs the
-  std library verification using the new tool, as well as an entry to the “Approved Tools” section of this book.
-* Once the PR is merged, the tool is considered integrated.
-* The repository will be updated periodically, which can impact the tool capacity to analyze the new version of the repository.
-  I.e., the action may no longer pass after an update.
-  This will not impact the approval status of the tool, however,
-  new solutions that want to employ the tool may need to ensure the action is passing first.
+Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools).
+To use a new tool, participants must first submit an application for it.
+
+* To submit a tool application, open a new issue in this repository using the "Tool Application" issue template.
+* The committee will review the application. Once a committee member approves the application, the participant needs to create a PR with:
+  * A new workflow that runs the tool against the standard library.
+  * A new entry to the “Approved Tools” section of this book.
+* Once this PR is merged, the tool is considered integrated, and the tool application issue will be closed.
+
+The repository will be updated periodically, which can impact a tool's capacity to analyze the new version of the repository (i.e., the workflow may no longer pass after an update).
+If it is determined that the tool requires changes and such changes cannot be provided in a timely fashion the tool's approval may be revoked.
 
 ## Committee Applications
 

doc/src/tool_template.md

@@ -15,6 +15,9 @@ _Please enter a description for your tool and any information you deem relevant.
 * [ ] Is the tool under development? 
 * [ ] Will you or your team be able to provide support for the tool?
 
+## Comparison to Other Approved Tools
+_Describe how this tool compares to the other approved tools. For example, are there certain properties that this tool can prove that the other tools cannot? The comparison does not need to be exhaustive; the purpose of this section is for the committee to understand the salient differences, and how this tool would fit into the larger effort._
+
 ## Licenses
 _Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s)._
 
@@ -24,8 +27,12 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
 2. \[Second Step\]
 3. \[and so on...\]
 
-## Artifacts
-_If there are noteworthy examples of using the tool to perform verification, please include them in this section.Links, papers, etc._
+## Artifacts & Audit Mechanisms
+_If there are noteworthy examples of using the tool to perform verification, please include them in this section. Links, papers, etc._
+_Also include mechanisms for the committee to audit the implementation and correctness of this tool (e.g., regression tests)._
+
+## Versioning
+_Please describe how you version the tool._
 
-## CI & Versioning
-_Please describe how you version the tool and how it will be supported in CI pipelines._
+## CI
+_If your tool is approved, you will be responsible merging a workflow into this repository that runs your tool against the standard library. For an example, see the Kani workflow (.github/workflows/kani.yml). Describe, at a high level, how your workflow will operate. (E.g., how will you package the tool to run in CI, how will you identify which proofs to run?)._

library/core/src/ffi/c_str.rs

@@ -456,6 +456,10 @@ impl CStr {
     #[stable(feature = "cstr_from_bytes", since = "1.10.0")]
     #[rustc_const_stable(feature = "const_cstr_unchecked", since = "1.59.0")]
     #[rustc_allow_const_fn_unstable(const_eval_select)]
+    // Preconditions: Null-terminated and no intermediate null bytes
+    #[requires(!bytes.is_empty() && bytes[bytes.len() - 1] == 0 && !bytes[..bytes.len()-1].contains(&0))]
+    // Postcondition: The resulting CStr satisfies the same conditions as preconditions
+    #[ensures(|result| result.is_safe())]
     pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr {
         const_eval_select!(
             @capture { bytes: &[u8] } -> &CStr:
@@ -779,6 +783,8 @@ impl AsRef<CStr> for CStr {
 #[unstable(feature = "cstr_internals", issue = "none")]
 #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0"))]
 #[rustc_allow_const_fn_unstable(const_eval_select)]
+#[requires(is_null_terminated(ptr))]
+#[ensures(|&result| result < isize::MAX as usize && unsafe { *ptr.add(result) } == 0)]
 const unsafe fn strlen(ptr: *const c_char) -> usize {
     const_eval_select!(
         @capture { s: *const c_char = ptr } -> usize:
@@ -910,6 +916,25 @@ mod verify {
         }
     }
 
+    //  pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr
+    #[kani::proof_for_contract(CStr::from_bytes_with_nul_unchecked)]
+    #[kani::unwind(33)]
+    fn check_from_bytes_with_nul_unchecked() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+
+        // Kani assumes that the input slice is null-terminated and contains
+        // no intermediate null bytes
+        let c_str = unsafe { CStr::from_bytes_with_nul_unchecked(slice) };
+        // Kani ensures that the output CStr holds the CStr safety invariant
+
+        // Correctness check
+        let bytes = c_str.to_bytes();
+        let len = bytes.len();
+        assert_eq!(bytes, &slice[..len]);
+    }
+      
     // pub fn bytes(&self) -> Bytes<'_>
     #[kani::proof]
     #[kani::unwind(32)]
@@ -972,6 +997,7 @@ mod verify {
         assert!(c_str.is_safe());
     }
 
+    // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError>
     #[kani::proof]
     #[kani::unwind(17)] 
     fn check_from_bytes_with_nul() {
@@ -1042,6 +1068,18 @@ mod verify {
         assert!(c_str.is_safe());
     }
 
+    // const unsafe fn strlen(ptr: *const c_char) -> usize
+    #[kani::proof_for_contract(super::strlen)]
+    #[kani::unwind(33)]
+    fn check_strlen_contract() {
+        const MAX_SIZE: usize = 32;
+        let mut string: [u8; MAX_SIZE] = kani::any();
+        let ptr = string.as_ptr() as *const c_char;
+
+        unsafe { super::strlen(ptr); }
+    }
+
+    // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr
     #[kani::proof_for_contract(CStr::from_ptr)]
     #[kani::unwind(33)]
     fn check_from_ptr_contract() {
@@ -1052,6 +1090,7 @@ mod verify {
         unsafe { CStr::from_ptr(ptr); }
     }
 
+    // pub const fn is_empty(&self) -> bool
     #[kani::proof]
     #[kani::unwind(33)]
     fn check_is_empty() {
@@ -1064,5 +1103,5 @@ mod verify {
         let expected_is_empty = bytes.len() == 0;
         assert_eq!(expected_is_empty, c_str.is_empty());
         assert!(c_str.is_safe());
-  }
+    }
 }