safe-abstraction: Correct the misconception

[bitboom]

This PR

• corrects the misconception
• replaces the closure-based methods with and with_mut with direct access methods as_ref and as_mut.

Previous Assumptions (misconception)

The use of closures was initially based on the belief that they helped maintain the context for unsafe code, which was presumed difficult to analyze effectively.

Findings from MIR Analysis

Recent evaluations using MIR-level analysis tools have shown that this tool, MIRI, is capable of effectively analyzing hidden unsafe code, regardless of the use of hidden unsafe code.

Evaluation

fn hidden_unsafe() {
    let handle1 = thread::spawn(move || {
        for _ in 0..1_000_000 {
            let x1 = get_mut_counter();
            *x1 += 1;
        }
    });

    let handle2 = thread::spawn(move || {
        for _ in 0..1_000_000 {
            let x1 = get_mut_counter();
            *x1 += 1;
        }
    });

    handle1.join().unwrap();
    handle2.join().unwrap();

    println!("Final value: {}", get_mut_counter());
}

fn get_mut_counter<'a>() -> &'a mut i32 {
    unsafe {
        let x1 = &COUNTER as *const i32 as usize;
        &mut *(x1 as *mut i32)
    }
}

fn main() {
    unsafe { explicit_unsafe(); }
    hidden_unsafe();
}

MIRI results

error: Undefined Behavior: Data race detected between (1) Write on thread `<unnamed>` and (2) Read on thread `<unnamed>` at alloc1. (2) just happened here
  --> src/main.rs:18:13
   |
18 |             *x1 += 1;
   |             ^^^^^^^^ Data race detected between (1) Write on thread `<unnamed>` and (2) Read on thread `<unnamed>` at alloc1. (2) just happened here
   |
help: and (1) occurred earlier here
  --> src/main.rs:10:13
   |
10 |             *x1 += 1;
   |             ^^^^^^^^
   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
   = note: BACKTRACE (of the first span):
   = note: inside closure at src/main.rs:18:13: 18:21

Decision Rationale

• Given that SafetyAssumed is marked safe by developers and relies on manual analysis to minimize unsafe code usage, it has been determined that maintaining additional closures does not provide substantial benefits.

• The API has been simplified to allow direct access through as_ref and as_mut, reducing the complexity and improving the transparency of safety assumptions.

[jinbpark]

does it mean that all the codes, in our repo, that use SafeAbstraction can be investigated through MIRI? right?

[bitboom]

that use

Yes, right!