/*
 * DF-0710 code-level reproduction harness.
 *
 * The vulnerable path sys/netbt/sco_socket.c:221-222 (sco_input) is
 * unreachable on this guest: it requires a Bluetooth controller driving
 * hci_sco_recv() (sys/netbt/hci_link.c:828) which is only compiled when
 * `options BLUETOOTH` is set AND requires a real BT radio. The guest has
 * neither (no `options BLUETOOTH` in X86_64_GENERIC, netbt.ko not loaded,
 * no BT USB/PCI device). This harness therefore replicates the EXACT kernel
 * control-flow primitives to prove the infinite-loop defect deterministically,
 * and proves the `if`-based fix (matching l2cap/rfcomm) eliminates it.
 *
 * Faithful replicas of the in-kernel primitives:
 *   - sbspace()  : sys/netbt/bluetooth.h:150-152
 *        #define sbspace(sb) ((long) imin((int)((sb)->ssb_hiwat - (sb)->ssb_cc),
 *                                         (int)((sb)->ssb_mbmax - (sb)->ssb_mbcnt)))
 *   - sbdroprecord(): sys/kern/uipc_sockbuf.c:517-535  (NO-OP when sb_mb == NULL,
 *        guarded by `if (m)` at line 524)
 *   - sco_recvspace = 4096   : sys/netbt/sco_socket.c:81
 *
 * We model the sockbuf as a small queue of records; ssb_cc tracks total data
 * bytes queued, ssb_mbcnt tracks mbuf accounting bytes. sbdroprecord pops and
 * frees the head record (or does nothing if empty) -- identical semantics.
 *
 * Build: cc -O2 -o sco_input_logic sco_input_logic.c
 * Run:   ./sco_input_logic
 */
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

#define SCO_RECVSPACE 4096
#define SCO_MBMAX     4096          /* soreserve typically sets mbmax >= hiwat */
#define LOOP_CAP      100000        /* iteration cap to detect the infinite loop */

/* minimal imin */
static inline int imin_(int a, int b) { return a < b ? a : b; }

/* ---- replica of sys/netbt/bluetooth.h:150-152 ---- */
#define sbspace(ssb) \
    ((long) imin_((int)((ssb)->ssb_hiwat - (ssb)->ssb_cc), \
                  (int)((ssb)->ssb_mbmax - (ssb)->ssb_mbcnt)))

struct record { int len; struct record *next; };
struct signalsockbuf {
    int ssb_hiwat;
    int ssb_mbmax;
    int ssb_cc;            /* data bytes queued */
    int ssb_mbcnt;         /* mbuf accounting bytes queued */
    struct record *head;   /* sb_mb (record list) */
    struct record *tail;
};

/* replica of sbdroprecord() -- sys/kern/uipc_sockbuf.c:517-535 */
static void sbdroprecord(struct signalsockbuf *sb)
{
    struct record *m = sb->head;
    if (m) {                       /* line 524: guard -- NO-OP when empty */
        sb->head = m->next;
        if (sb->head == NULL) sb->tail = NULL;
        sb->ssb_cc    -= m->len;
        sb->ssb_mbcnt -= m->len;   /* sbfree decrements accounting */
        free(m);
    }
}

static void sb_append(struct signalsockbuf *sb, int len)
{
    struct record *r = malloc(sizeof(*r));
    r->len = len; r->next = NULL;
    if (sb->tail) sb->tail->next = r; else sb->head = r;
    sb->tail = r;
    sb->ssb_cc += len;
    sb->ssb_mbcnt += len;
}

static void ssb_init(struct signalsockbuf *sb)
{
    memset(sb, 0, sizeof(*sb));
    sb->ssb_hiwat = SCO_RECVSPACE;
    sb->ssb_mbmax = SCO_MBMAX;
}

/* ---- BUGGY sco_input: sys/netbt/sco_socket.c:221-222 (while) ----
 * Returns the iteration count; if it hits LOOP_CAP the loop would run forever.
 */
static long sco_input_buggy(struct signalsockbuf *sb, int m_len, int *appended)
{
    long iters = 0;
    *appended = 0;
    /* while (m->m_pkthdr.len > sbspace(&so->so_rcv)) sbdroprecord(&so->so_rcv.sb); */
    while (m_len > sbspace(sb)) {
        sbdroprecord(sb);
        if (++iters >= LOOP_CAP) return iters;   /* detect infinite loop */
    }
    sb_append(sb, m_len);
    *appended = 1;
    return iters;
}

/* ---- FIXED sco_input: while -> if { drop; return } (matches l2cap/rfcomm) ----
 * sys/netbt/l2cap_socket.c:231, sys/netbt/rfcomm_socket.c:241
 */
static long sco_input_fixed(struct signalsockbuf *sb, int m_len, int *appended)
{
    long iters = 0;
    *appended = 0;
    if (m_len > sbspace(sb)) {
        /* m_freem(m); return; -- drop the packet that can never fit */
        return 1;
    }
    sb_append(sb, m_len);
    *appended = 1;
    return iters;
}

struct testcase {
    const char *name;
    int prefill_records[8];   /* records already queued before the packet */
    int prefill_count;
    int incoming_len;
};

static const struct testcase cases[] = {
    /* 1. empty buffer, oversized single packet (the malicious-dongle scenario) */
    { "empty buf + oversize pkt (8192 > 4096)", {0}, 0, 8192 },
    /* 2. slightly-over: 4097 bytes, empty buffer -> can NEVER fit */
    { "empty buf + pkt 4097 (> hiwat 4096 by 1)", {0}, 0, 4097 },
    /* 3. partially full buffer, oversized packet: buggy drains then spins */
    { "half-full buf (2048) + oversize pkt 8192", {2048}, 1, 8192 },
    /* 4. multiple queued records, oversized packet: buggy drains all then spins */
    { "3 records (1024 each) + oversize pkt 8192", {1024,1024,1024}, 3, 8192 },
    /* 5. benign: small packet that fits -> no loop on either path */
    { "empty buf + small pkt 100 (control)", {0}, 0, 100 },
    /* 6. packet exactly fills remaining space (boundary) */
    { "empty buf + pkt 4096 (== hiwat, fits)", {0}, 0, 4096 },
};

int main(void)
{
    int ncases = sizeof(cases)/sizeof(cases[0]);
    int buggy_infinite = 0, fixed_ok = 0;

    printf("=== DF-0710 sco_input while-vs-if logic harness ===\n");
    printf("sco_recvspace(hiwat)=%d  mbmax=%d  LOOP_CAP=%d\n\n",
           SCO_RECVSPACE, SCO_MBMAX, LOOP_CAP);

    for (int i = 0; i < ncases; i++) {
        const struct testcase *t = &cases[i];
        int appended;
        long iters;

        /* --- BUGGY (while) --- */
        struct signalsockbuf sb_b; ssb_init(&sb_b);
        for (int j = 0; j < t->prefill_count; j++)
            if (t->prefill_records[j] > 0) sb_append(&sb_b, t->prefill_records[j]);
        long space_before_b = sbspace(&sb_b);
        iters = sco_input_buggy(&sb_b, t->incoming_len, &appended);
        int buggy_loop = (iters >= LOOP_CAP);

        /* --- FIXED (if) --- */
        struct signalsockbuf sb_f; ssb_init(&sb_f);
        for (int j = 0; j < t->prefill_count; j++)
            if (t->prefill_records[j] > 0) sb_append(&sb_f, t->prefill_records[j]);
        long space_before_f = sbspace(&sb_f);
        int appended_f;
        long iters_f = sco_input_fixed(&sb_f, t->incoming_len, &appended_f);

        printf("[case %d] %s\n", i+1, t->name);
        printf("    sbspace before = %ld\n", space_before_b);
        printf("    BUGGY(while): iters=%ld %s (appended=%d)\n",
               iters, buggy_loop ? "*** WOULD LOOP FOREVER ***" : "(terminated)", appended);
        printf("    FIXED (if)  : iters=%ld %s (appended=%d)\n",
               iters_f, appended_f ? "(appended)" : "(dropped packet)", appended_f);

        if (buggy_loop) buggy_infinite++;
        if (!appended_f || (appended_f && space_before_f >= t->incoming_len))
            fixed_ok++;   /* fixed never loops; appends only when truly fits */
    }

    printf("\n=== SUMMARY ===\n");
    printf("cases where BUGGY(while) infinite-loops: %d / %d\n", buggy_infinite, ncases);
    printf("FIXED (if) terminates in <=1 iter on ALL cases: %s\n",
          fixed_ok == ncases ? "YES" : "NO");
    printf("BUG CONFIRMED: while-loop spins when an incoming SCO packet exceeds\n");
    printf("sco_recvspace and the buffer cannot free enough room (incl. empty buf)\n");

    /* exit code: 0 = bug demonstrated (buggy loops on >=1 oversize case) */
    return (buggy_infinite > 0) ? 0 : 1;
}