#!/bin/sh
# DF-4522 static proof: the amdgpu_vm_fini cleanup loop is dead code on
# DragonFly because nothing in sys/ ever writes rb_root_cached.rb_leftmost.
#
# Each assertion exits non-zero with an explanation if it fails.
# Run from the repo root (or set SYSROOT).

d=$(cd "$(dirname "$0")" && pwd)
while [ "$d" != / ] && [ ! -e "$d/sys/sys/tree.h" ]; do d=$(dirname "$d"); done
[ -e "$d/sys/sys/tree.h" ] || { echo "cannot locate sys/ tree upward of $0"; exit 1; }
SYSROOT=${SYSROOT:-$d/sys}
fail() { echo "FAIL: $*"; exit 1; }

GREP=rg; command -v rg >/dev/null 2>&1 || GREP=grep
echo "[1] The only rb_leftmost references in all of sys/ are the two READ"
echo "    sites in amdgpu_vm_fini's loop (amdgpu_vm.c:3325-3326):"
refs=$($GREP -n 'rb_leftmost' "$SYSROOT" -g '*.[ch]' 2>/dev/null \
       | grep -v 'include/linux/rbtree.h')
echo "$refs"
[ "$(echo "$refs" | wc -l)" -eq 2 ] || fail "expected exactly 2 rb_leftmost refs, got: $refs"
echo "$refs" | grep -q ':3325:' || fail "no read at :3325"
echo "$refs" | grep -q 'while (vm->va.rb_leftmost)' || fail "fini loop read missing"

echo
echo "[2] No assignment writes ->rb_leftmost anywhere in sys/:"
$GREP -n 'rb_leftmost[[:space:]]*=' "$SYSROOT" -g '*.[ch]' 2>/dev/null \
    | grep -v '==' && fail "unexpected rb_leftmost writer found" || echo "    (none -- confirmed)"

echo
echo "[3] The shim: rb_insert_color_cached() IGNORES its leftmost argument and"
echo "    rb_erase_cached()/rb_first_cached() never touch the cache field"
echo "    (sys/dev/drm/include/linux/rbtree.h:100-106):"
sed -n '100,106p' "$SYSROOT/dev/drm/include/linux/rbtree.h"
# the only 'leftmost' in 100-106 is the ignored macro PARAMETER name in the
# #define line itself -- assert the expansion never uses it:
if sed -n '101,104p' "$SYSROOT/dev/drm/include/linux/rbtree.h" | grep -q 'leftmost'; then
    fail "expansion lines 101-104 mention leftmost"
fi

echo
echo "[4] sys/tree.h (the underlying DFly RB implementation) has no"
echo "    leftmost-cache concept at all:"
grep -n 'leftmost' "$SYSROOT/sys/tree.h" && fail "unexpected leftmost in tree.h" || echo "    (none -- confirmed)"

echo
echo "[5] vm->va is zero-initialized (struct rb_root_cached {rb_root; rb_leftmost;},"
echo "    rbtree.h:64-67) at amdgpu_vm_init (amdgpu_vm.c:3055):"
grep -n 'vm->va = LINUX_RB_ROOT_CACHED' "$SYSROOT/dev/drm/amd/amdgpu/amdgpu_vm.c"

echo
echo "CONCLUSION: vm->va.rb_leftmost is deterministically NULL for the VM's"
echo "entire lifetime => 'while (vm->va.rb_leftmost)' at amdgpu_vm.c:3325 runs"
echo "ZERO iterations => list_del+amdgpu_vm_it_remove+kfree at :3331-3333 never"
echo "execute => every mapping still in the tree at amdgpu_vm_fini leaks."
echo "PASS"