A false positive in double lock detector

[soyo114]

Description

The false positive occurs because the detector fails to account for the semantics of drop. Below is a minimized reproduction case.

Lockbud should not report DoubleLock warning as the code example does not generate a deadlock during execution. The first lock was dropped before the execution of line 19. I use the command cargo lockbud -k all to run LockBud.

struct Foo {
    rw: spin::RwLock<i32>,
}
impl Foo {
    fn new() -> Self {
        Self {
            rw: spin::RwLock::new(1),
        }
    }
    fn spin_rwlock_write_1(&self) {
        let mut write_guard = self.rw.write(); // report first lock
        match *write_guard {
            1 => {
                drop(write_guard);
                self.spin_rwlock_write_2();
            }
            _ => {}
        };
        self.spin_rwlock_write_cleanup();
    }
    fn spin_rwlock_write_cleanup(&self) {
        *self.rw.write() += 0;  // report second lock
    }
    fn spin_rwlock_write_2(&self) {
        *self.rw.write() += 1;
    }
}
fn main() {
    let foo1 = Foo::new();
    foo1.spin_rwlock_write_1();
    foo1.spin_rwlock_write_2();
}

Analysis results

Lockbud reported DoubleLock warning :

"first_lock_type": "SpinWrite(i32)",
"first_lock_span": "src/main.rs:11:13: 11:28 (#0)",
"second_lock_type": "SpinWrite(i32)",
"second_lock_span": "src/main.rs:22:10: 22:25 (#0)",