#!/bin/sh
# DF-4605 — verbatim control-flow proof (runs ON THE GUEST).
#
# Proves, from the LIVE kernel source at /usr/src (not a hand copy), that:
#   1. the event guard in amdgpu_atif_handler (amdgpu_acpi.c:374-385) has an
#      EMPTY body — its only statements are inside `#if 0`, so the preprocessor
#      removes them and the `if` becomes a no-op;
#   2. control therefore falls through to `atif->functions.sbios_requests`
#      (amdgpu_acpi.c:387), which reads offset 0x12 of a NULL pointer when
#      adev->atif == NULL (the normal state on ATIF-less systems, e.g. all
#      discrete desktop AMD GPUs — see README.md reachability analysis);
#   3. the proposed fix (restore the early `return;`) removes the fault.
#
# The kernel itself cannot run this path on this guest (no AMD GPU, amdgpu.ko
# not built) — this harness compiles the EXACT extracted lines with the exact
# struct layout instead, so the control-flow claim is mechanically verified.
set -u
SRC=/usr/src/sys/dev/drm/amd/amdgpu/amdgpu_acpi.c
[ -f "$SRC" ] || { echo "FATAL: kernel source not present: $SRC"; exit 1; }

WORK=$(mktemp -d /tmp/df4605.XXXXXX)
cd "$WORK"

# --- extract the exact lines under test from the live kernel source -------
sed -n '374,385p' "$SRC" > guard.inc        # the guard (if (...) { #if 0 ... #endif })
sed -n '387p'    "$SRC" > deref.inc         # `if (atif->functions.sbios_requests) {`

echo "===== extracted guard.inc (amdgpu_acpi.c:374-385) ====="
cat -n guard.inc
echo "===== extracted deref.inc (amdgpu_acpi.c:387) ====="
cat -n deref.inc

# fixed variant: same guard with the #if 0..#endif block (frag lines 6-11)
# replaced by a real early return; the closing brace (frag line 12) is kept
sed '6,11c\
        return;' guard.inc > guard_fixed.inc
echo "===== guard_fixed.inc (proposed fix applied) ====="
cat -n guard_fixed.inc

# --- harness with exact struct layout from amdgpu_acpi.c:38-75 -------------
cat > guard_test.c <<'EOF'
/*
 * DF-4605 control-flow harness. The two #include fragments below are
 * sed-extracted verbatim from the guest's live kernel source:
 *   guard.inc  = amdgpu_acpi.c lines 374-385 (the gutted guard)
 *   deref.inc  = amdgpu_acpi.c line 387      (the first deref)
 * Struct definitions replicate sys/dev/drm/amd/amdgpu/amdgpu_acpi.c:38-75
 * byte-for-byte in size/offset (ACPI_HANDLE = pointer, bool = 1 byte),
 * so `functions.sbios_requests` sits at offset 18 (0x12), exactly as in
 * the kernel build.
 */
#include <stdio.h>
#include <signal.h>
#include <stdint.h>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>

typedef unsigned int UINT32;

struct amdgpu_atif_notification_cfg { char enabled; int command_code; };
struct amdgpu_atif_notifications {
	char display_switch, expansion_mode_change, thermal_state,
	     forced_power_state, system_power_state, display_conf_change,
	     px_gfx_switch, brightness_change, dgpu_display_event; /* 9 x 1B */
};
struct amdgpu_atif_functions {
	char system_params, sbios_requests, select_active_disp, lid_state,
	     get_tv_standard, set_tv_standard, get_panel_expansion_mode,
	     set_panel_expansion_mode, temperature_change,
	     graphics_device_types;                               /* 10 x 1B */
};
struct amdgpu_atif {
	void *handle;                          /* ACPI_HANDLE        @0   */
	struct amdgpu_atif_notifications notifications;   /* @8..16     */
	struct amdgpu_atif_functions functions;           /* @17..26    */
	struct amdgpu_atif_notification_cfg notification_cfg;
};

static int fixed_mode = 0;
/*
 * Opaque barrier: prevents the optimizer from proving atif==NULL and
 * deleting the deref as dead code (UB elision). In the kernel, atif comes
 * from adev->atif at notify-dispatch time and is never foldable.
 */
static struct amdgpu_atif * volatile atif_arg = NULL;

__attribute__((noinline))
static void handler_under_test(struct amdgpu_atif *atif, UINT32 type)
{
	if (fixed_mode) {
#include "guard_fixed.inc"
	} else {
#include "guard.inc"
	}
#include "deref.inc"
	/* kernel body (amdgpu_acpi.c:388-431) calls amdgpu_atif_get_sbios_requests()
	 * — a real side effect. The sink replicates that so the compiler cannot
	 * drop the (dead-looking) empty-guard + load. */
	printf("KERNEL-EQUIV: sbios_requests path entered "
	       "(kernel evaluates ATIF GET_SYSTEM_BIOS_REQUESTS here)\n");
	}
}

static void segv(int sig, siginfo_t *si, void *uc)
{
	(void)sig; (void)uc;
	printf("RESULT: SIGSEGV at address %p  "
	       "(=&atif->functions.sbios_requests with atif==NULL, expected 0x12)\n",
	       si->si_addr);
	if (fixed_mode)
		printf("FIXED-MODE FAULT: unexpected — fix did NOT work\n");
	else
		printf("VERDICT: guard body compiled to NOTHING; control fell "
		       "through the if() into the NULL deref\n");
	exit(fixed_mode ? 1 : 42);
}

int main(int argc, char **argv)
{
	struct sigaction sa;
	fixed_mode = (argc > 1);

	memset(&sa, 0, sizeof(sa));
	sa.sa_sigaction = segv;
	sa.sa_flags = SA_SIGINFO;
	sigaction(SIGSEGV, &sa, NULL);

	printf("sizeof(struct amdgpu_atif)=%zu  "
	       "offsetof(functions.sbios_requests)=%zu\n",
	       sizeof(struct amdgpu_atif),
	       (size_t)&((struct amdgpu_atif *)0)->functions.sbios_requests);

	/* exactly the kernel state on ATIF-less systems: adev->atif == NULL.
	 * The NULL is produced at RUNTIME (getenv) so the optimizer cannot
	 * constant-fold it and delete the deref as UB-dead-code (which gcc 8
	 * demonstrably does otherwise — see VERDICT.md; in the kernel atif is
	 * adev->atif, an opaque heap field, equally unfoldable). */
	{
		const char *e = getenv("DF4605_ATIF");
		struct amdgpu_atif *atif =
			(struct amdgpu_atif *)(uintptr_t)(e ? strtol(e, NULL, 0) : 0);
		handler_under_test(atif, 0x81);
	}
	printf("RESULT: no fault — guard returned early (finding REFUTED in this mode)\n");
	return 0;
}
EOF

echo "===== build (kernel-style -O2) ====="
cc -O2 -Wall -o guard_test guard_test.c || exit 1

echo "===== run BASELINE (gutted guard, verbatim kernel lines) ====="
./guard_test; rc=$?
echo "baseline exit=$rc"

echo "===== run FIXED (guard with restored return) ====="
./guard_test fixed; rc2=$?
echo "fixed exit=$rc2"

if [ "$rc" = "42" ] && [ "$rc2" = "0" ]; then
	echo "PROOF-OK: baseline faults at NULL+0x12; fixed variant returns cleanly"
else
	echo "PROOF-UNEXPECTED: baseline=$rc fixed=$rc2"
fi
echo "workdir: $WORK"