Add RAPx tool description and CI workflow

.github/workflows/rapx.yml

@@ -0,0 +1,66 @@
+name: RAPx
+
+on:
+  workflow_dispatch:
+  push:
+    branches: [main,rapx-verify-std]
+  pull_request:
+    branches: [main,rapx-verify-std]
+
+env:
+  RAPx_VERSION: "2f8cefc8a4bbd7c347e02e97c61de1d8224776ba"
+  SAFETY_TOOL_VERSION: "6b77419da66865bb5a36b6c9baec71b3e833d3c9"
+
+jobs:
+  check-with-rapx:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      - name: Clone and setup safety_tool
+        run: |
+          git clone https://github.com/Artisan-Lab/tag-std.git
+          cd tag-std
+          git checkout $SAFETY_TOOL_VERSION
+          cargo install cargo-expand
+          cd safety-tool
+          TOOL_DIR=$(pwd)
+          echo "TOOL_DIR=$TOOL_DIR" >> $GITHUB_ENV
+          rm -f rust-toolchain.toml
+          ./gen_rust_toolchain_toml.rs std
+
+      - name: Install safety_tool
+        run: |
+          export VERIFY_RUST_STD=1
+          export LD_LIBRARY_PATH=$(rustc --print sysroot)/lib
+          cd tag-std/safety-tool
+          cargo install --path . --locked -Fstd
+          safety-tool --version
+          safety-tool-rfl build-dev
+          safety-tool-rfl --display-extra-rustc-args
+
+      - name: Clone and install RAPx
+        run: |
+          rm -rf RAPx
+          git clone https://github.com/Artisan-Lab/RAPx.git
+          cd RAPx
+          git checkout $RAPx_VERSION
+          ./install.sh
+
+      - name: Set up RAPx environment
+        run: |
+            RUSTUP_TOOLCHAIN=$(rustup show active-toolchain | cut -d ' ' -f 1)
+            echo "RUSTUP_TOOLCHAIN=$RUSTUP_TOOLCHAIN" >> $GITHUB_ENV
+            CURRENT_DIR=$(pwd)
+            RUST_SRC_PATH="$CURRENT_DIR/library"
+            echo "__CARGO_TESTS_ONLY_SRC_ROOT=$RUST_SRC_PATH" >> $GITHUB_ENV
+
+      - name: Run RAPx verification
+        run: |
+          cargo new dummy_crate
+          cd dummy_crate
+          export LD_LIBRARY_PATH=$(rustc --print sysroot)/lib
+          export RUSTFLAGS="--cfg=rapx -L $TOOL_DIR/target/safety-tool/lib --extern=safety_macro -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)"
+          cargo +$RUSTUP_TOOLCHAIN rapx -verify-std -- -Zbuild-std=panic_abort,core,std --target x86_64-unknown-linux-gnu

doc/src/SUMMARY.md

@@ -11,6 +11,7 @@
   - [GOTO Transcoder](./tools/goto-transcoder.md)
   - [VeriFast](./tools/verifast.md)
   - [Flux](./tools/flux.md)
+  - [RAPx](./tools/rapx.md)
 
 ---
 

doc/src/tools/rapx.md

@@ -0,0 +1,62 @@
+# RAPx
+RAPx is a static analysis platform for Rust programs. It can serve as a companion to the Rust compiler in detecting semantic bugs related to unsafe code.
+
+Using abstract interpretation, RAPx checks for undefined behavior (UB) by pre-tagging unsafe APIs. When a caller calls such a pre-tagged API, RAPx examines all program paths to verify whether the program state meets the tag's conditions—ensuring the caller remains sound under any input and does not trigger UB. Currently, RAPx can detect various types of UB, such as misaligned or dangling pointers, out-of-bounds memory access, and uninitialized memory usage.
+
+## Safety Property Verification
+This section will briefly describe several key steps of UB validation by RAPx.
+
+RAPx has a specialized verification module for unsafe Rust code that systematically prevents undefined behavior (UB) through two core steps:
+
++ Audit Unit Generation: Segment code into verifiable units by analyzing unsafe code propagation patterns.
+
++ Safety Property Verification: Use contract-based abstract interpretation to validate safety properties.
+
+For comprehensive methodology details and practical examples, see the [module of verification in RAPx-Book](https://artisan-lab.github.io/RAPx-Book/6.4-unsafe.html).
+
+## Installation
+See the [quick start section](https://github.com/Artisan-Lab/RAPx?tab=readme-ov-file#quick-start) to learn how to install RAPx. The version of rustc used by RAPx is continuously updated and tries to match the `verify-rust-std` project's version whenever possible.
+
+## Usage
+### Usage in verifying third-party crate
+After ensuring that RAPx with the correct rustc version has been installed, you can verify the soundness of your code by doing the following steps:
++ Navigate to the root directory of the crate you wish to analyze:
+```
+cd /to-be-verified-crate/
+```
++ Set the required environment variables. Since RAPx by default checks all unsafe calls in the standard library, __CARGO_TESTS_ONLY_SRC_ROOT must point to a pre-annotated version of std. A fully annotated std repository for RAPx linking will be released in the future.
+```
+export RUSTUP_TOOLCHAIN=$RUSTUP_TOOLCHAIN_OF_RAPX
+export __CARGO_TESTS_ONLY_SRC_ROOT=/path-to-pre-annotated-std-lib/library
+```
++ Run the verification using the -verify subcommand. RAPx requires linking to the annotated standard library, so the -Zbuild-std argument is necessary:
+```
+# In Linux
+cargo +$RUSTUP_TOOLCHAIN rapx -verify -- -Zbuild-std=panic_abort,core,alloc,std --target x86_64-unknown-linux-gnu
+# In Mac(Arm)
+cargo +$RUSTUP_TOOLCHAIN rapx -verify -- -Zbuild-std=panic_abort,core,alloc,std --target aarch64-apple-darwin
+```
+Upon completion, RAPx will output the analysis results regarding the contract compliance of APIs containing unsafe code:
+```
+|RAP|INFO|: --------In safe function "alloc::vec::into_raw_parts_with_alloc"---------
+|RAP|INFO|:   Use unsafe api "core::ptr::read".
+|RAP|INFO|:       Argument 1's passed Sps: {"ValidPtr", "Typed", "Align"}
+```
+
+### Usage in verifying the the Rust Standard Library
+Apart from the need to set up a `dummy_crate` as the entry point for the verification command, the process is the same as validating third-party libraries. However, RAPx offers a customized command, `-verify-std`, specifically for standard library verification. When using this command, RAPx scans all APIs in the standard library and verifies those annotated with `proof` targets. For example:
+```rust
+#[cfg_attr(rapx, safety {proof})]
+pub fn pop(&mut self) -> Option<T> {
+    ...
+}
+```
+This annotation will be conditionally expanded and verified during RAPx's compilation process.
+
+## Caveats
+RAPx provides sound detection of undefined behavior - if any path in the program contains UB, it will be reported. But this guarantee comes with inherent over-approximation of program paths, which may yield false positives where reported UB paths are infeasible in concrete execution.
+
+Besides, RAPx is still under heavy development and can currently validate some SPs mentioned in [tag-std](https://github.com/Artisan-Lab/tag-std/blob/main/primitive-sp.md#21-summary-of-primitive-sps). Continued development and integration are needed to support the verification of the remaining ones. 
+
+Finally, RAPx ensures the absence of undefined behavior (UB) on all paths by (i) checking the callee’s preconditions or (ii) tracking subsequent [hazard conditions](https://github.com/Artisan-Lab/tag-std/blob/main/primitive-sp.md#1-overall-idea). RAPx can not provide any proof for the logic correctness of function.
+

library/alloc/Cargo.toml

@@ -34,4 +34,5 @@ check-cfg = [
     'cfg(no_global_oom_handling)',
     'cfg(no_rc)',
     'cfg(no_sync)',
+    'cfg(rapx)'
 ]

library/alloc/src/lib.rs

@@ -234,6 +234,11 @@ pub mod sync;
 pub mod task;
 pub mod vec;
 
+#[cfg(rapx)]
+mod rapx_macro {
+    pub use safety_macro::safety;
+}
+
 #[doc(hidden)]
 #[unstable(feature = "liballoc_internals", issue = "none", reason = "implementation detail")]
 pub mod __export {

library/alloc/src/vec/mod.rs

@@ -92,6 +92,8 @@ use crate::alloc::{Allocator, Global};
 use crate::borrow::{Cow, ToOwned};
 use crate::boxed::Box;
 use crate::collections::TryReserveError;
+#[cfg(rapx)]
+use crate::rapx_macro::safety;
 use crate::raw_vec::RawVec;
 
 mod extract_if;
@@ -1256,6 +1258,7 @@ impl<T, A: Allocator> Vec<T, A> {
     #[must_use = "losing the pointer will leak memory"]
     #[unstable(feature = "allocator_api", issue = "32838")]
     // #[unstable(feature = "vec_into_raw_parts", reason = "new API", issue = "65816")]
+    #[cfg_attr(rapx, safety {proof})]
     pub fn into_raw_parts_with_alloc(self) -> (*mut T, usize, usize, A) {
         let mut me = ManuallyDrop::new(self);
         let len = me.len();

library/core/Cargo.toml

@@ -42,7 +42,8 @@ check-cfg = [
     'cfg(target_has_reliable_f128)',
     'cfg(target_has_reliable_f128_math)',
     'cfg(kani)',
-    'cfg(flux)'
+    'cfg(flux)',
+    'cfg(rapx)'
 ]
 
 [package.metadata.flux]

library/core/src/lib.rs

@@ -434,3 +434,8 @@ include!("primitive_docs.rs");
 
 #[cfg(flux)]
 mod flux_info;
+
+#[cfg(rapx)]
+mod rapx_macro {
+    pub use safety_macro::safety;
+}

library/core/src/ptr/mod.rs

@@ -408,6 +408,8 @@ use crate::kani;
 use crate::marker::{FnPtr, PointeeSized};
 use crate::mem::{self, MaybeUninit, SizedTypeProperties};
 use crate::num::NonZero;
+#[cfg(rapx)]
+use crate::rapx_macro::safety;
 use crate::{fmt, hash, intrinsics, ub_checks};
 
 mod alignment;
@@ -1664,6 +1666,9 @@ pub const unsafe fn replace<T>(dst: *mut T, src: T) -> T {
 #[rustc_const_stable(feature = "const_ptr_read", since = "1.71.0")]
 #[track_caller]
 #[rustc_diagnostic_item = "ptr_read"]
+#[cfg_attr(rapx, safety {ValidPtr(src, T, 1)})]
+#[cfg_attr(rapx, safety {Typed(src, T)})]
+#[cfg_attr(rapx, safety {Align(src, T)})]
 pub const unsafe fn read<T>(src: *const T) -> T {
     // It would be semantically correct to implement this via `copy_nonoverlapping`
     // and `MaybeUninit`, as was done before PR #109035. Calling `assume_init`

library/core/src/ptr/mut_ptr.rs

@@ -7,6 +7,8 @@ use crate::intrinsics::const_eval_select;
 use crate::kani;
 use crate::marker::PointeeSized;
 use crate::mem::{self, SizedTypeProperties};
+#[cfg(rapx)]
+use crate::rapx_macro::safety;
 use crate::slice::{self, SliceIndex};
 
 impl<T: PointeeSized> *mut T {
@@ -1041,6 +1043,8 @@ impl<T: PointeeSized> *mut T {
     // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
     // verifying that the result remains within the same allocation as `self`.
     #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self as *const T, *result as *const T))]
+    #[cfg_attr(rapx, safety {InBound(self, T, count)})]
+    #[cfg_attr(rapx, safety {ValidNum(count * size_of(T) <= isize::MAX)})]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,