/*
 * DF-0855 — dirfs_findfd KKASSERT panic / NULL deref on unlinked dirfs nodes
 *
 * Deterministic proof harness (dirfs is vkernel64-only, NOT compiled into the
 * running X86_64_GENERIC host kernel — see VERDICT.md). Transcribes:
 *
 *   - dirfs_findfd()            sys/vfs/dirfs/dirfs_subr.c:450-497
 *   - the unlinked-node setup   sys/vfs/dirfs/dirfs_vnops.c:914-916
 *                               (dirfs_nremove: dnp->dn_parent = NULL)
 *
 * The bug:
 *   dirfs_subr.c:479   dnp1 = dnp1->dn_parent;
 *   dirfs_subr.c:480   KKASSERT(dnp1 != NULL);          <-- PANIC if unlinked
 *
 * The sibling dirfs_node_absolute_path_plus (dirfs_subr.c:422-424) does the
 * SAME parent walk but uses `if (dnp1 == NULL) break;` — proving the author
 * KNEW the NULL case is reachable; dirfs_findfd was simply not given the same
 * guard.
 *
 * We simulate KKASSERT (with INVARIANTS on, which VKERNEL64 ships by default)
 * as panic()-equivalent: a printed panic message + abort().
 */

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <stdint.h>
#include <signal.h>

/* ---- minimal dirfs_node transcription (only fields used by dirfs_findfd) -- */
#define DIRFS_NOFD    (-1)
#define DIRFS_ROOT    0x0001
#define MAXPATHLEN    1024

struct dirfs_node {
    int                  dn_state;
    int                  dn_fd;
    int                  dn_namelen;
    char                *dn_name;
    struct dirfs_node   *dn_parent;
};
typedef struct dirfs_node *dirfs_node_t;

#define dirfs_node_isroot(n)  ((n)->dn_state & DIRFS_ROOT)

/* ---- KKASSERT = panic() when INVARIANTS is on (the VKERNEL64 default) ----- */
static int g_panic_fired = 0;
static const char *g_panic_msg = NULL;

#define KKASSERT(exp)                                                     \
    do {                                                                  \
        if (__builtin_expect(!(exp), 0)) {                                \
            g_panic_fired = 1;                                            \
            g_panic_msg = "assertion \"" #exp "\" failed "                \
                          "in dirfs_findfd at dirfs_subr.c:480";         \
            return NULL;  /* simulate panic: unwinding abort of the walk */\
        }                                                                 \
    } while (0)

/* ---- FAITHFUL transcription of dirfs_findfd (dirfs_subr.c:450-497) ------- */
/* BUGGY version (as shipped): KKASSERT(dnp1 != NULL) at :480               */
static dirfs_node_t
dirfs_findfd_BUGGY(struct dirfs_node *cur, char **pathto, char **pathfreep)
{
    struct dirfs_node *dnp1;
    int count;
    char *buf;

    *pathfreep = NULL;
    *pathto = NULL;

    if (cur == NULL)
        return NULL;

    buf = calloc(MAXPATHLEN + 1, 1);
    count = 0;

    dnp1 = cur;
    /* dirfs_subr.c:470 */
    while (dnp1 == cur || dnp1->dn_fd == DIRFS_NOFD) {
        count += dnp1->dn_namelen;                          /* :471 */
        if (count <= MAXPATHLEN) {
            bcopy(dnp1->dn_name, &buf[MAXPATHLEN - count], /* :473 */
                  dnp1->dn_namelen);
        }
        ++count;                                           /* :476 */
        if (count <= MAXPATHLEN)
            buf[MAXPATHLEN - count] = '/';                 /* :478 */
        dnp1 = dnp1->dn_parent;                            /* :479 */
        KKASSERT(dnp1 != NULL);                            /* :480 -- PANIC */
    }

    if (dnp1 && count <= MAXPATHLEN) {                     /* :483 */
        *pathfreep = buf;
        *pathto = &buf[MAXPATHLEN - count + 1];
    } else {
        free(buf);
        *pathfreep = NULL;
        *pathto = NULL;
        dnp1 = NULL;
    }
    return dnp1;
}

#undef KKASSERT

/* ---- FIXED version: mirror dirfs_node_absolute_path_plus (:422-424) ------ */
static dirfs_node_t
dirfs_findfd_FIXED(struct dirfs_node *cur, char **pathto, char **pathfreep)
{
    struct dirfs_node *dnp1;
    int count;
    char *buf;

    *pathfreep = NULL;
    *pathto = NULL;

    if (cur == NULL)
        return NULL;

    buf = calloc(MAXPATHLEN + 1, 1);
    count = 0;

    dnp1 = cur;
    while (dnp1 == cur || dnp1->dn_fd == DIRFS_NOFD) {
        count += dnp1->dn_namelen;
        if (count <= MAXPATHLEN) {
            bcopy(dnp1->dn_name, &buf[MAXPATHLEN - count], dnp1->dn_namelen);
        }
        ++count;
        if (count <= MAXPATHLEN)
            buf[MAXPATHLEN - count] = '/';
        dnp1 = dnp1->dn_parent;
        /* FIX: mirror dirfs_node_absolute_path_plus (dirfs_subr.c:423-424) */
        if (dnp1 == NULL)
            break;
    }

    if (dnp1 && count <= MAXPATHLEN) {
        *pathfreep = buf;
        *pathto = &buf[MAXPATHLEN - count + 1];
    } else {
        free(buf);
        *pathfreep = NULL;
        *pathto = NULL;
        dnp1 = NULL;
    }
    return dnp1;
}

/* ---- build the unlinked-node scenario ---- */
/* dirfs_nremove (dirfs_vnops.c:906-922):
 *   pathnp = dirfs_findfd(dmp, dnp, ...);    // BEFORE unlink — parent valid
 *   unlinkat(pathnp->dn_fd, tmp, 0);
 *   if (success) {
 *       ... dnp->dn_parent = NULL;           // :916 — UNLINKED
 *   }
 * The vnode stays alive (open fd). The next VOP_GETATTR (fstat) on it calls
 * dirfs_getattr -> dirfs_findfd on the now-unlinked node -> KKASSERT panic.
 */
static struct dirfs_node *
make_node(const char *name, int fd, struct dirfs_node *parent)
{
    struct dirfs_node *n = calloc(1, sizeof(*n));
    n->dn_name = strdup(name);
    n->dn_namelen = strlen(name);
    n->dn_fd = fd;
    n->dn_parent = parent;
    return n;
}

int
main(void)
{
    int bugs = 0, fixes_ok = 0;

    /* Build a 2-level tree: /rootdir/file.txt
     * rootdir has a valid fd; file.txt has DIRFS_NOFD (passive, resolved by
     * walking up to the parent's fd — exactly the dirfs_findfd use case).   */
    struct dirfs_node *root = make_node("rootdir", 3, NULL);
    root->dn_state |= DIRFS_ROOT;
    struct dirfs_node *file = make_node("file.txt", DIRFS_NOFD, root);

    printf("=== DF-0855 dirfs_findfd KKASSERT panic / NULL deref ===\n\n");
    printf("setup: root=%p (fd=%d, isroot), file=%p (fd=DIRFS_NOFD, parent=root)\n",
           (void*)root, root->dn_fd, (void*)file);
    printf("       file->dn_parent = %p (valid)\n\n", (void*)file->dn_parent);

    /* ---- 1. happy path (parent intact) — both versions succeed ---- */
    {
        char *tmp = NULL, *pf = NULL;
        g_panic_fired = 0; g_panic_msg = NULL;
        dirfs_node_t r = dirfs_findfd_BUGGY(file, &tmp, &pf);
        printf("[happy path, parent intact]\n");
        printf("  BUGGY: pathnp=%p panic=%d path=\"%s\"   (expect panic=0, path set)\n",
               (void*)r, g_panic_fired, tmp ? tmp : "(null)");
        if (pf) free(pf);
        if (r == root && !g_panic_fired) ; else bugs++;
    }
    {
        char *tmp = NULL, *pf = NULL;
        dirfs_node_t r = dirfs_findfd_FIXED(file, &tmp, &pf);
        printf("  FIXED: pathnp=%p panic=%d path=\"%s\"   (expect panic=0, path set)\n\n",
               (void*)r, g_panic_fired, tmp ? tmp : "(null)");
        if (pf) free(pf);
        if (r == root) fixes_ok++;   /* happy path: FIXED succeeds too */
    }

    /* ---- 2. THE BUG: unlink the file -> dn_parent = NULL ---- */
    /* dirfs_vnops.c:916  dnp->dn_parent = NULL; */
    file->dn_parent = NULL;
    printf("[AFTER dirfs_nremove: file->dn_parent = NULL (unlinked, vnode alive)]\n");
    printf("       file->dn_parent = %p\n\n", (void*)file->dn_parent);

    /* BUGGY: dirfs_findfd on the unlinked node -> KKASSERT panic at :480 */
    {
        char *tmp = NULL, *pf = NULL;
        g_panic_fired = 0; g_panic_msg = NULL;
        dirfs_node_t r = dirfs_findfd_BUGGY(file, &tmp, &pf);
        printf("[fstat(fd) -> VOP_GETATTR -> dirfs_getattr -> dirfs_findfd]\n");
        printf("  BUGGY: pathnp=%p panic=%d\n", (void*)r, g_panic_fired);
        if (g_panic_fired) {
            printf("         ** PANIC: %s\n", g_panic_msg);
            printf("         ** => kernel panic (KKASSERT w/ INVARIANTS) or NULL deref (without)\n");
            bugs++;
        } else {
            printf("         (no panic — unexpected)\n");
        }
        if (pf) free(pf);
    }

    /* FIXED: dirfs_findfd returns NULL gracefully, caller returns ESTALE */
    {
        char *tmp = NULL, *pf = NULL;
        dirfs_node_t r = dirfs_findfd_FIXED(file, &tmp, &pf);
        printf("  FIXED: pathnp=%p tmp=%s pf=%p  (expect NULL — caller returns ESTALE)\n",
               (void*)r, tmp ? "(set)" : "NULL", (void*)pf);
        if (r == NULL && tmp == NULL && pf == NULL) {
            printf("         => no panic, no leak; caller (dirfs_getattr) returns ESTALE\n");
            fixes_ok++;
        } else {
            printf("         (unexpected non-NULL return)\n");
        }
    }

    printf("\n=== SUMMARY ===\n");
    printf("DF_0855_BUG_PANIC_ON_UNLINKED_NODE   = %s\n", bugs >= 1 ? "YES (KKASSERT fires)" : "no");
    printf("DF_0855_FIX_RETURNS_NULL_NO_PANIC    = %s\n", fixes_ok == 2 ? "YES" : "no");

    /* the harness exits 0 only if the bug fired AND the fix closed it */
    return (bugs >= 1 && fixes_ok == 2) ? 0 : 1;
}