//! Miri tests for SkipList — detects UB that loom cannot:
//! Stacked Borrows violations, use-after-free, double-free, invalid pointers.
//!
//! Run:
//!   cargo +nightly miri test -p armdb --test miri_skiplist -- single_
//!   MIRIFLAGS="-Zmiri-preemption-rate=0.1" cargo +nightly miri test -p armdb --test miri_skiplist -- concurrent_

#![cfg(miri)]
#![allow(clippy::unwrap_used)]

use std::sync::Arc;
use std::thread;

use armdb::DiskLoc;
use armdb::skiplist::iter::Iter;
use armdb::skiplist::node::{ConstNode, SkipNode, VarNode};
use armdb::skiplist::{InsertResult, SkipList};

type TestNode = ConstNode<[u8; 4], 8>;
type TestList = SkipList<TestNode>;

fn disk() -> DiskLoc {
    DiskLoc::new(0, 0, 0)
}

fn alloc_node(key: [u8; 4], value: [u8; 8]) -> *mut TestNode {
    TestNode::alloc(key, value, disk(), 1)
}

fn alloc_node_h(key: [u8; 4], value: [u8; 8], height: u8) -> *mut TestNode {
    TestNode::alloc(key, value, disk(), height)
}

// ===== Category 1: Single-threaded (Stacked Borrows, pointer validity) =====

/// Full lifecycle: alloc → insert → get (&*ptr) → remove → retire → Drop.
/// Verifies the entire Box::into_raw / from_raw chain is sound.
#[test]
fn single_insert_get_remove() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let node = alloc_node([0, 0, 0, 1], [1u8; 8]);
    assert!(matches!(list.insert(node, &guard), InsertResult::Inserted));

    let found = list.get(&[0, 0, 0, 1], &guard).unwrap();
    assert_eq!(found.read_value(), [1u8; 8]);
    assert_eq!(list.len(), 1);

    let removed = list.remove(&[0, 0, 0, 1], &guard);
    assert!(removed.is_some());
    assert_eq!(list.len(), 0);

    // get after remove should return None
    assert!(list.get(&[0, 0, 0, 1], &guard).is_none());
}

/// ConstNode SeqLock: write_data then read_value.
/// Verifies SeqLock correctness for inline data update.
#[test]
fn single_overwrite_seqlock_const() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let node = alloc_node([0, 0, 0, 1], [1u8; 8]);
    list.insert(node, &guard);

    let found = list.get(&[0, 0, 0, 1], &guard).unwrap();
    assert_eq!(found.read_value(), [1u8; 8]);

    // SeqLock write (inline, no heap allocation)
    found.write_data(disk(), &[2u8; 8]);

    // Read after write — must see new data
    assert_eq!(found.read_value(), [2u8; 8]);
}

/// VarNode SeqLock: write_loc then read_loc (single-threaded provenance check).
#[test]
fn single_overwrite_seqlock_var() {
    type TVarNode = VarNode<[u8; 4]>;
    type TVarList = SkipList<TVarNode>;

    let d1 = DiskLoc::new(1, 100, 50);
    let list = TVarList::new(false);
    let guard = list.collector().enter();

    let node = TVarNode::alloc([0, 0, 0, 1], d1, 1);
    list.insert(node, &guard);

    let found = list.get(&[0, 0, 0, 1], &guard).unwrap();
    assert_eq!(found.read_loc(), d1);

    let d2 = DiskLoc::new(2, 200, 60);
    found.write_loc(d2);
    assert_eq!(found.read_loc(), d2);
}

/// Create list, insert 3 nodes, drop. Verifies Drop walks level 0
/// correctly — no double-free, no missed nodes.
#[test]
fn single_drop_populated() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    for i in 0u8..3 {
        let node = alloc_node([0, 0, 0, i], [i; 8]);
        list.insert(node, &guard);
    }
    assert_eq!(list.len(), 3);

    drop(guard);
    drop(list); // Drop walks level 0 and frees all nodes
}

/// Insert 3 nodes, iterate with Iter::all, verify all visited.
/// Checks iterator pointer validity through `&*self.current`.
#[test]
fn single_iter_full() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    for i in 0u8..3 {
        let node = alloc_node([0, 0, 0, i], [i; 8]);
        list.insert(node, &guard);
    }

    let iter = Iter::all(&list, &guard);
    let mut values: Vec<[u8; 8]> = iter.map(|n| n.read_value()).collect();
    values.sort();

    assert_eq!(values.len(), 3);
    assert_eq!(values[0], [0u8; 8]);
    assert_eq!(values[1], [1u8; 8]);
    assert_eq!(values[2], [2u8; 8]);
}

/// Insert same key twice — second returns Exists.
/// Verify rejected node is properly freed (no leak under Miri).
#[test]
fn single_insert_exists() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let n1 = alloc_node([0, 0, 0, 1], [1u8; 8]);
    assert!(matches!(list.insert(n1, &guard), InsertResult::Inserted));

    let n2 = alloc_node([0, 0, 0, 1], [2u8; 8]);
    match list.insert(n2, &guard) {
        InsertResult::Exists(existing) => {
            assert_eq!(existing.read_value(), [1u8; 8]);
            // Free rejected node — it was never inserted
            unsafe {
                TestNode::dealloc_node(n2);
            }
        }
        InsertResult::Inserted => panic!("expected Exists"),
    }

    assert_eq!(list.len(), 1);
}

/// S-1 regression: get must not overshoot past a marked higher-level node.
/// Setup: key 3 (height 1), key 6 (height 2). Mark node 6 without unlinking.
/// get(3) must return Some, not None.
#[test]
fn single_get_skips_marked_node() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let n3 = alloc_node_h([0, 0, 0, 3], [3u8; 8], 1);
    let n6 = alloc_node_h([0, 0, 0, 6], [6u8; 8], 2);
    list.insert(n3, &guard);
    list.insert(n6, &guard);

    let node6 = list.get(&[0, 0, 0, 6], &guard).unwrap();
    node6.mark();

    let found = list.get(&[0, 0, 0, 3], &guard);
    assert!(
        found.is_some(),
        "get(3) must not be blocked by marked node 6"
    );
    assert_eq!(found.unwrap().read_value(), [3u8; 8]);
}

/// S-1 regression: find_first_ge must not overshoot past a marked higher-level node.
#[test]
fn single_find_first_ge_skips_marked_node() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let n3 = alloc_node_h([0, 0, 0, 3], [3u8; 8], 1);
    let n6 = alloc_node_h([0, 0, 0, 6], [6u8; 8], 2);
    list.insert(n3, &guard);
    list.insert(n6, &guard);

    let node6 = list.get(&[0, 0, 0, 6], &guard).unwrap();
    node6.mark();

    let found = list.test_find_first_ge(&[0, 0, 0, 3], &guard);
    assert!(!found.is_null(), "find_first_ge(3) must find node 3");
    assert_eq!(unsafe { &*found }.key_bytes(), &[0, 0, 0, 3]);
}

/// S-1 regression: find_last_lt must not return a marked node or skip live predecessors.
/// Setup: key 5 (height 1), key 6 (height 2, marked). find_last_lt(7) must return node 5.
#[test]
fn single_find_last_lt_skips_marked_node() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let n5 = alloc_node_h([0, 0, 0, 5], [5u8; 8], 1);
    let n6 = alloc_node_h([0, 0, 0, 6], [6u8; 8], 2);
    list.insert(n5, &guard);
    list.insert(n6, &guard);

    let node6 = list.get(&[0, 0, 0, 6], &guard).unwrap();
    node6.mark();

    let found = list.test_find_last_lt(&[0, 0, 0, 7], &guard);
    assert!(!found.is_null(), "find_last_lt(7) must find node 5");
    let found_ref = unsafe { &*found };
    assert!(
        !found_ref.is_marked(),
        "find_last_lt must not return a marked node"
    );
    assert_eq!(found_ref.key_bytes(), &[0, 0, 0, 5]);
}

/// S-1 regression: find_last must not return a marked node.
/// Setup: key 3 (height 1), key 5 (height 1), key 8 (height 2, marked).
/// find_last() must return node 5, not marked node 8.
#[test]
fn single_find_last_skips_marked_node() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let n3 = alloc_node_h([0, 0, 0, 3], [3u8; 8], 1);
    let n5 = alloc_node_h([0, 0, 0, 5], [5u8; 8], 1);
    let n8 = alloc_node_h([0, 0, 0, 8], [8u8; 8], 2);
    list.insert(n3, &guard);
    list.insert(n5, &guard);
    list.insert(n8, &guard);

    let node8 = list.get(&[0, 0, 0, 8], &guard).unwrap();
    node8.mark();

    let found = list.test_find_last(&guard);
    assert!(!found.is_null(), "find_last must find a live node");
    let found_ref = unsafe { &*found };
    assert!(
        !found_ref.is_marked(),
        "find_last must not return a marked node"
    );
    assert_eq!(found_ref.key_bytes(), &[0, 0, 0, 5]);
}

/// S-1 regression: chain of consecutive marked nodes must be skipped entirely.
/// Setup: key 2 (height 1, live), key 4 (height 2, marked), key 6 (height 2, marked),
/// key 8 (height 1, live). find_last_lt(10) must return node 8, not a marked node.
#[test]
fn single_find_last_lt_skips_consecutive_marked_chain() {
    let list = TestList::new(false);
    let guard = list.collector().enter();

    let n2 = alloc_node_h([0, 0, 0, 2], [2u8; 8], 1);
    let n4 = alloc_node_h([0, 0, 0, 4], [4u8; 8], 2);
    let n6 = alloc_node_h([0, 0, 0, 6], [6u8; 8], 2);
    let n8 = alloc_node_h([0, 0, 0, 8], [8u8; 8], 1);
    list.insert(n2, &guard);
    list.insert(n4, &guard);
    list.insert(n6, &guard);
    list.insert(n8, &guard);

    list.get(&[0, 0, 0, 4], &guard).unwrap().mark();
    list.get(&[0, 0, 0, 6], &guard).unwrap().mark();

    let found = list.test_find_last_lt(&[0, 0, 0, 10], &guard);
    assert!(!found.is_null());
    let found_ref = unsafe { &*found };
    assert!(!found_ref.is_marked());
    assert_eq!(found_ref.key_bytes(), &[0, 0, 0, 8]);
}

// ===== Category 2: Multi-threaded (data races, use-after-free) =====

/// Reader vs writer: no data race on tower pointers.
#[test]
fn concurrent_get_insert() {
    let list = Arc::new(TestList::new(false));

    let l1 = list.clone();
    let t1 = thread::spawn(move || {
        let guard = l1.collector().enter();
        l1.get(&[0, 0, 0, 1], &guard).map(|n| n.read_value())
    });

    let l2 = list.clone();
    let t2 = thread::spawn(move || {
        let guard = l2.collector().enter();
        let node = alloc_node([0, 0, 0, 1], [1u8; 8]);
        l2.insert(node, &guard);
    });

    let read = t1.join().unwrap();
    t2.join().unwrap();

    if let Some(v) = read {
        assert_eq!(v, [1u8; 8]);
    }
}

/// Reader vs remover WITH REAL RETIRE.
/// Miri detects use-after-free if the seize guard doesn't protect the reader.
#[test]
fn concurrent_get_remove() {
    let list = Arc::new(TestList::new(false));

    // Pre-insert
    {
        let guard = list.collector().enter();
        let node = alloc_node([0, 0, 0, 1], [1u8; 8]);
        list.insert(node, &guard);
    }

    let l1 = list.clone();
    let t1 = thread::spawn(move || {
        let guard = l1.collector().enter();
        l1.get(&[0, 0, 0, 1], &guard).map(|n| n.read_value())
    });

    let l2 = list.clone();
    let t2 = thread::spawn(move || {
        let guard = l2.collector().enter();
        l2.remove(&[0, 0, 0, 1], &guard).is_some()
    });

    let read = t1.join().unwrap();
    let _removed = t2.join().unwrap();

    if let Some(v) = read {
        assert_eq!(v, [1u8; 8]);
    }
}

/// Iterator vs concurrent insert + remove.
/// Verifies no dangling pointer in iterator during modification.
#[test]
fn concurrent_iter_modify() {
    let list = Arc::new(TestList::new(false));

    // Pre-insert two nodes
    {
        let guard = list.collector().enter();
        let n1 = alloc_node([0, 0, 0, 1], [1u8; 8]);
        list.insert(n1, &guard);
        let n2 = alloc_node([0, 0, 0, 2], [2u8; 8]);
        list.insert(n2, &guard);
    }

    let l1 = list.clone();
    let t1 = thread::spawn(move || {
        let guard = l1.collector().enter();
        let iter = Iter::all(&l1, &guard);
        iter.map(|n| n.read_value()).collect::<Vec<_>>()
    });

    let l2 = list.clone();
    let t2 = thread::spawn(move || {
        let guard = l2.collector().enter();
        // Insert a new node
        let n3 = alloc_node([0, 0, 0, 3], [3u8; 8]);
        l2.insert(n3, &guard);
        // Remove an existing node
        let _ = l2.remove(&[0, 0, 0, 1], &guard);
    });

    let vals = t1.join().unwrap();
    t2.join().unwrap();

    // At least one node should be visible (node 2 is never removed)
    assert!(!vals.is_empty());
}

/// Optimistic presearch paths: concurrent insert of a new key + remove of a
/// neighbour. Exercises presearch/validate/fallback under Miri (provenance,
/// UAF) on the optimistic insert/remove code paths.
#[test]
fn concurrent_insert_remove_neighbors() {
    let list = Arc::new(TestList::new(false));
    {
        let guard = list.collector().enter();
        for k in [1u8, 3, 5, 7] {
            let node = alloc_node([0, 0, 0, k], [k; 8]);
            list.insert(node, &guard);
        }
    }

    let l1 = list.clone();
    let t1 = thread::spawn(move || {
        let guard = l1.collector().enter();
        let node = alloc_node([0, 0, 0, 4], [4u8; 8]);
        match l1.insert(node, &guard) {
            InsertResult::Inserted => {}
            InsertResult::Exists(_) => unsafe { TestNode::dealloc_node(node) },
        }
    });

    let l2 = list.clone();
    let t2 = thread::spawn(move || {
        let guard = l2.collector().enter();
        l2.remove(&[0, 0, 0, 3], &guard);
    });

    t1.join().unwrap();
    t2.join().unwrap();

    let guard = list.collector().enter();
    assert!(list.get(&[0, 0, 0, 4], &guard).is_some());
    assert!(list.get(&[0, 0, 0, 3], &guard).is_none());
    for k in [1u8, 5, 7] {
        assert!(list.get(&[0, 0, 0, k], &guard).is_some());
    }
}
