/*
 * DF-2214 verbatim-code rig - HEAD
 * Target: sys/dev/drm/radeon/rv770_dma.c:42-94 rv770_copy_dma()
 * Claim under test: size_in_dw = (num_gpu_pages << RADEON_GPU_PAGE_SHIFT) / 4
 *                   computed in 32-bit unsigned arithmetic wraps for
 *                   num_gpu_pages >= 2^20 (4 GiB-class TTM moves), so the DMA
 *                   engine is told to copy only a fraction (or nothing) while
 *                   radeon_fence_emit() still signals success.
 *
 * This head provides the minimal FABRICATED boundary state the verbatim
 * production function walks: the real types it names, real constants
 * (RADEON_GPU_PAGE_SHIFT, DMA_PACKET/DMA_PACKET_COPY from rv770d.h, real DMA
 * ring geometry from rv770.c:1968), and shim implementations of the radeon
 * helpers that replicate the observable semantics of the production bodies
 * (each cited). All ring writes land in a kmalloc'd ring buffer bracketed by
 * canary zones so the "no host kernel memory is corrupted" negative claim is
 * tested empirically, not just asserted.
 *
 * The production function body itself is concatenated UNMODIFIED (byte range
 * lines 42..94 of the tree file) by build.sh - see the sha256 checks there.
 */
#include <sys/param.h>		/* howmany */
#include <sys/types.h>
#include <sys/systm.h>		/* kprintf */
#include <sys/kernel.h>		/* SI_SUB_* */
#include <sys/module.h>
#include <sys/malloc.h>
#include <sys/lock.h>
#include <sys/errno.h>
/* no <string.h>: sys/systm.h provides the fortified memset macro; a
 * prototype would collide with it in kernel context */

/* ------------------------------------------------------------------ */
/* Types the verbatim body names (fabricated minimal, member paths     */
/* exactly as dereferenced by the production code)                     */
/* ------------------------------------------------------------------ */
typedef uint8_t  u8;
typedef uint16_t u16;
typedef uint32_t u32;
typedef uint64_t u64;
/* bool comes from sys/stdint.h (typedef _Bool bool) in this environment */
#ifndef __bool_true_false_are_defined
#define false 0
#define true 1
#define __bool_true_false_are_defined 1
#endif

struct reservation_object { int rig_dummy; };

struct radeon_device;

struct radeon_fence {
	struct radeon_device	*rdev;
	int			ring;
	u64			seq;		/* radeon_fence.c:117-127 shape */
};

/* real struct radeon_sync holds 2 semaphore ptrs + a fence (radeon.h:619-622);
 * the verbatim body only passes &sync around - shape is irrelevant, calls are */
struct radeon_sync { void *s[2]; struct radeon_fence *f; };

struct radeon_ring {
	int		idx;			/* radeon.h ring block        */
	u32		*ring;			/* CPU mapping of ring buffer */
	unsigned	ring_size;		/* bytes (radeon_ring.c:106)  */
	u32		wptr;			/* radeon.h:2708-2717 state   */
	u32		wptr_old;
	u32		ptr_mask;		/* radeon_ring.c:410          */
	u32		align_mask;		/* radeon_ring.c:114          */
	int		count_dw;		/* radeon.h:2710/2715         */
	int		ring_free_dw;
	int		ready;			/* radeon_ttm.c move gate     */
};

struct radeon_asic {
	struct { int dma_ring_index; } copy;	/* radeon.h asic->copy        */
};

#define RADEON_NUM_RINGS 8			/* radeon.h:161 */

struct radeon_device {
	const struct radeon_asic *asic;
	struct radeon_ring	ring[RADEON_NUM_RINGS];
	u64			sync_seq[RADEON_NUM_RINGS]; /* radeon.h:369 */
	struct lock		ring_lock;		/* radeon_ring.c:143 */
};

/* ------------------------------------------------------------------ */
/* Real constants/macros (verbatim from the cited tree lines)          */
/* ------------------------------------------------------------------ */
#define RADEON_GPU_PAGE_SHIFT	12		/* radeon.h:645 */
#define R600_RING_TYPE_DMA_INDEX 3		/* radeon.h:149 */

/* rv770d.h:663-666 verbatim */
#define DMA_PACKET(cmd, t, s, n)	((((cmd) & 0xF) << 28) |	\
					 (((t) & 0x1) << 23) |		\
					 (((s) & 0x1) << 22) |		\
					 (((n) & 0xFFFF) << 0))
/* rv770d.h:669 */
#define	DMA_PACKET_COPY					  0x3

/* sys/dev/drm/include/linux/kernel.h:59 */
#define DIV_ROUND_UP(x, y)	howmany(x, y)

/* linux compat semantics used by the body */
#define upper_32_bits(n) ((u32)(((n) >> 16) >> 16))
#define MAX_ERRNO 4096L
#define ERR_PTR(e)	((void *)(intptr_t)(e))
#define IS_ERR_VALUE(x) ((unsigned long)(x) >= (unsigned long)-MAX_ERRNO)
#define IS_ERR(p)	IS_ERR_VALUE((intptr_t)(p))

/* ------------------------------------------------------------------ */
/* Rig observation state                                               */
/* ------------------------------------------------------------------ */
struct rig_stats {
	unsigned long	writes;			/* total radeon_ring_write calls */
	unsigned	copy_packets;		/* DMA_PACKET_COPY headers seen  */
	u64		sum_chunk_dw;		/* sum of packet n fields        */
	u32		max_chunk, min_chunk;
	u32		first_pkt;		/* first packet header dword     */
	u32		first5[5], last5[5];	/* raw ring dwords               */
	int		fence_emits;
	u64		fence_seq;
	int		fence_ring;
	int		lock_rc;
	unsigned	attempted_ndw;		/* ndw passed to radeon_ring_lock */
	unsigned	committed;
	unsigned	undone;
	int		underruns;		/* count_dw<=0 at write time     */
	int		sync_create, sync_resv, sync_rings, sync_free;
	int		drm_errors;
};
static struct rig_stats g_stats;

#define DRM_ERROR(fmt, ...) do { g_stats.drm_errors++;			\
	kprintf("DF2214   [DRM_ERROR] " fmt, ##__VA_ARGS__); } while (0)

/* ------------------------------------------------------------------ */
/* Shim: radeon_sync_* (production radeon_sync.c:42,89,137,212)        */
/* ------------------------------------------------------------------ */
static void radeon_sync_create(struct radeon_sync *sync)	/* :42 */
{
	memset(sync, 0, sizeof(*sync));
	g_stats.sync_create++;
}

static int radeon_sync_resv(struct radeon_device *rdev,	/* :89 */
			    struct radeon_sync *sync,
			    struct reservation_object *resv, bool shared)
{
	g_stats.sync_resv++;
	return 0;
}

static int radeon_sync_rings(struct radeon_device *rdev,	/* :137 */
			     struct radeon_sync *sync, int ring)
{
	g_stats.sync_rings++;
	return 0;
}

static void radeon_sync_free(struct radeon_device *rdev,	/* :212 */
			     struct radeon_sync *sync,
			     struct radeon_fence *fence)
{
	g_stats.sync_free++;
}

/* ------------------------------------------------------------------ */
/* Shim: ring allocation/lock - observable semantics of                */
/* radeon_ring.c:107-127 (radeon_ring_alloc) and 140-152 (lock)        */
/* ------------------------------------------------------------------ */
static int rig_ring_alloc(struct radeon_device *rdev,
			   struct radeon_ring *ring, unsigned ndw)
{
	/* radeon_ring.c:108-110 */
	if (ndw > (ring->ring_size / 4))
		return -ENOMEM;
	/* radeon_ring.c:113-114 */
	ndw = (ndw + ring->align_mask) & ~ring->align_mask;
	ring->count_dw = ndw;
	ring->wptr_old = ring->wptr;
	return 0;
}

static int radeon_ring_lock(struct radeon_device *rdev,
			    struct radeon_ring *ring, unsigned ndw)
{
	int r;

	g_stats.attempted_ndw = ndw;		/* rig observation only */
	lockmgr(&rdev->ring_lock, LK_EXCLUSIVE);
	r = rig_ring_alloc(rdev, ring, ndw);
	if (r) {
		lockmgr(&rdev->ring_lock, LK_RELEASE);
		g_stats.lock_rc = r;
		return r;
	}
	g_stats.lock_rc = 0;
	return 0;
}

/* radeon_ring.c:195-213: unlock_commit pads+releases; padding writes 0 in
 * this boundary state (align_mask==0); observed effect = commit count */
static void radeon_ring_unlock_commit(struct radeon_device *rdev,
				      struct radeon_ring *ring, bool b)
{
	g_stats.committed++;
	lockmgr(&rdev->ring_lock, LK_RELEASE);
}

/* radeon_ring.c:221-226: undo resets wptr to the allocation-time value */
static void radeon_ring_unlock_undo(struct radeon_device *rdev,
				    struct radeon_ring *ring)
{
	ring->wptr = ring->wptr_old;
	g_stats.undone++;
	lockmgr(&rdev->ring_lock, LK_RELEASE);
}

/* ------------------------------------------------------------------ */
/* Shim: radeon_ring_write - PRODUCTION BODY VERBATIM radeon.h:2710-   */
/* 2716, plus trailing rig instrumentation (clearly separated). The    */
/* production bytes write ring->ring[wptr++&mask] and count down       */
/* count_dw / ring_free_dw; every write stays inside the ring buffer   */
/* allocation by the ptr_mask invariant.                               */
/* ------------------------------------------------------------------ */
static void radeon_ring_write(struct radeon_ring *ring, uint32_t v)
{
	if (ring->count_dw <= 0)
		DRM_ERROR("radeon: writing more dwords to the ring than expected!\n");

	ring->ring[ring->wptr++] = v;
	ring->wptr &= ring->ptr_mask;
	ring->count_dw--;
	ring->ring_free_dw--;
	/* ---- rig instrumentation below, NOT production bytes ---- */
	{
		u32 n5 = (u32)((g_stats.writes + 1) % 5);
		g_stats.writes++;
		if (g_stats.writes <= 5)
			g_stats.first5[g_stats.writes - 1] = v;
		g_stats.last5[n5] = v;
		if (n5 == 1) {		/* packet header position in the 5-dword cadence */
			u32 cmd = (v >> 28) & 0xF;
			u32 n = v & 0xFFFF;
			if (cmd == DMA_PACKET_COPY) {
				if (g_stats.copy_packets == 0) {
					g_stats.first_pkt = v;
					g_stats.min_chunk = 0xFFFFFFFFu;
				}
				g_stats.copy_packets++;
				g_stats.sum_chunk_dw += n;
				if (n > g_stats.max_chunk)
					g_stats.max_chunk = n;
				if (n < g_stats.min_chunk)
					g_stats.min_chunk = n;
			}
		}
	}
}

/* ------------------------------------------------------------------ */
/* Shim: radeon_fence_emit - production radeon_fence.c:128-141         */
/* (kmalloc + ++sync_seq[ring]); fence packets consume the +8 slack    */
/* reserved by the caller, which the rig records as 0 writes.          */
/* ------------------------------------------------------------------ */
static int radeon_fence_emit(struct radeon_device *rdev,
			     struct radeon_fence **fence, int ring)
{
	struct radeon_fence *f;

	f = kmalloc(sizeof(*f), M_TEMP, M_WAITOK | M_ZERO);
	f->rdev = rdev;
	f->ring = ring;
	f->seq = ++rdev->sync_seq[ring];
	*fence = f;
	g_stats.fence_emits++;
	g_stats.fence_seq = f->seq;
	g_stats.fence_ring = ring;
	return 0;
}