use ui;
use core:sync;
use core:lang;

/**
 * Exception thrown to exit.
 */
class ExitError extends Exception {
	void message(StrBuf to) : override {
		to << "Time to terminate!";
	}
}

/**
 * Custom data type to use when referring to a thread ID.
 *
 * When referring to a thread by ID, it is important to use this type so that the system can
 * properly collapse the thread ID:s when checking the program for errors (when doing this, we
 * aggressively collapse states that are considered to be the same). So, whenever the runtime system
 * finds a thread id by accessing a ProgThread class and displays it to the user, it is important to
 * wrap it inside an instance of this class. For values that are returned from functions that create
 * threads, that intentionally expose thread ids to the system, this is not necessary. As the thread
 * id is visible to the user, the system is not able to merge executions.
 *
 * Note: The value 0 means "no thread", and a special value (noinit) means that the ID has not yet
 * been initialized (useful to distinguish between "no initialization" and "no thread currently" in
 * locks for example).
 *
 * Note: The size of this class must be exactly one Nat, otherwise other implementations may break
 * (we access this from asm/RawPtr:s).
 */
value ThreadId {
	// The actual thread id.
	Nat v;

	// Create an 'empty' thread id.
	init() {
		init { v = 0; }
	}

	// Create.
	init(Nat v) {
		init { v = v; }
	}

	// Create uninitialized id.
	ThreadId noInit() : static {
		ThreadId((-1).nat);
	}

	// Empty?
	Bool empty() { this.noInit() | (v == 0); }
	Bool any() { !empty(); }

	// Not initialized?
	Bool noInit() { v == (-1).nat; }

	// Hash and equals if we want to use ThreadId throughout the system.
	Nat hash() { v.hash; }
	Bool ==(Nat o) { v == o; }

	// To string.
	void toS(StrBuf to) {
		if (v == (-1).nat)
			to << "<not initialized>";
		else if (empty)
			to << "<no thread>";
		else
			to << "thread " << v;
	}
}

/**
 * Custom data type to use when referring to a positive value that should also have a representation
 * for "not initialized".
 *
 * Much like ThreadId, this type needs to be exactly a Nat in size, as it is manipulated from
 * ASM/RawPtr:s. The "no value" is represented as -1. The difference from ThreadId is that this
 * class does not handle thread ID:s as a special case, it only provides a special representation
 * for "no value".
 */
value MaybePositive {
	// The actual value.
	Nat v;

	// Create an 'empty' value.
	init() {
		init { v = (-1).nat; }
	}

	// Create with a value.
	init(Nat v) {
		init { v = v; }
	}

	// Empty?
	Bool empty() { v == (-1).nat; }

	// Hash and equals.
	Nat hash() { v.hash; }
	Bool ==(Nat o) { v == o; }
}


/**
 * Represents a running thread inside the program.
 */
class ProgThread on Render {
	// Semaphore used to pause the monitored thread.
	private Sema sema;

	// Duration for automatic stepping. If zero, we will wait for user input instead.
	private Duration autoStep;

	// Step to the next barrier instead of the next statement.
	private Bool barrierStep;

	// Speed when stepping through a barrier step. If zero, no animation is done.
	private Duration barrierSpeed;

	// Current call depth. There may be additional entries in 'frames', as we might have exited a
	// function but not yet received any new information. In this case, we will still show the old
	// state since it might contain references to values that are still known by the code, but not
	// otherwise reachable (eg. the return value).
	private Nat callDepth;

	// Number of anonymous functions called at the root level. This is to make sure that we don't
	// remove the thread too early if the root function is not tracked. If the root function calls
	// more than one tracked functions, we would otherwise assign it to multiple thread IDs
	// otherwise.
	private Nat rootAnonDepth;

	// Current thread ID (the simple thread ID generated by this system).
	Nat threadId;

	// Future to watch whenever this thread terminated.
	FutureBase? watch;

	// Entries of called functions. We expect this array to contain at least one element when we
	// receive calls to 'onNewLocation'.
	StackFrame[] frames;

	// Owning Program object, so we can access the callback.
	Program owner;

	// Memory reads and writes by this thread since the last statement.
	// Not stored inside a particular frame in order to properly track reading function
	// parameters, etc.
	MemTracker memory;

	// Waiting for some external event?
	Bool sleeping;

	// Is the thread currently paused? A thread is paused if it is not currently running any code in
	// the program (i.e. do we have control of the thread currently). This means that 'paused' is
	// true even if the thread is waiting for its turn to make a new step.
	Bool paused;

	// Was this thread a part of a known busy wait loop before the last step? In the C frontend, the
	// function 'atomics_busy_wait' sets this to true.
	Bool knownBusyWait;

	// Is the thread currently waiting for user interaction.
	Bool waiting() { !running; }

	// Is the thread alive?
	Bool alive() { (rootAnonDepth + callDepth) > 0; }

	// Did the thread crash? (Only relevant when "alive" returns false)
	Bool crashed() { terminating; }

	// Do we have barriers in the current function?
	Bool barriersAvailable() {
		if (frames.any & callDepth > 0)
			frames.last.hints.barriersAvailable;
		else
			false;
	}

	// Is the thread currently running? If 'false', the thread is waiting in our semaphore. Thus,
	// 'running' is true even if the thread is currently waiting inside a sleep block or similar.
	private Bool running;

	// Terminate the thread at the next opportunity to do so.
	private Bool doTerminate;

	// Did we throw the termination exception? If so, we will not intercept execution anymore, since
	// destructors might be intercepted.
	private Bool terminating;

	// Create.
	init(Program owner, Nat threadId) {
		init() {
			sema(0);
			callDepth = 0;
			threadId = threadId;
			owner = owner;
			running = true;
		}
	}

	// Get the current location.
	SrcPos? pos() {
		if (frames.empty())
			return null;
		frames.last.pos;
	}

	// To string.
	void toS(StrBuf to) : override {
		to << "Thread " << threadId;
	}

	// Called by a monitored thread to possibly pause execution.
	// Returns 'false' if this event is not interesting to propagate.
	// 'offset' is the offset in the original asm listing. It is used
	// to decide when to abort barrier skips that end up in an infinite
	// loop without proper barriers (e.g. busy-wait).
	Bool onNewLocation(SrcPos pos, StackVar[] vars, Nat offset) {
		if (terminating)
			return false;

		popFrames();

		var last = frames.last;
		last.variables = vars;

		// Stop barrier step if we detect a loop.
		if (last.lastOffset > offset)
			barrierStep = false;
		last.lastOffset = offset;

		if (pos.any) {
			last.pos = pos;

			if (!barrierStep) {
				// Remember we stopped here last so that the next barrier step does not repeat this
				// one.
				last.lastStop = pos;

				wait();
				// Only clear if we waited, to highlight properly.
				memory.clearNew();
			} else if (barrierSpeed != Duration()) {
				if (pos != last.lastStop) {
					// Pause for a while.
					paused = true;
					owner.notifyChange(true);
					if (!barrierStep) {
						// Someone asked us to pause!
						wait();
					} else {
						sleep(barrierSpeed);
					}
					paused = false;
				}
			}
		}

		true;
	}

	// Called by a monitored thread when a barrier instruction was hit.
	void onNewBarrier(SrcPos pos, Barrier type, Nat offset) {
		if (terminating)
			return;

		var last = frames.last;
		if (pos.any)
			last.pos = pos;
		// Update the last offset, to help the model checker with duplicates.
		if (last.lastOffset < offset)
			last.lastOffset = offset;

		if (barrierStep) {
			if (last.pos != last.lastStop) {
				last.lastStop = last.pos;

				wait();
			}

			// If this is a release barrier, make sure to stop at the next step. Otherwise, we
			// may miss some interesting interleavings (e.g. let the new thread run first when
			// starting a new thread).
			// Note: We have to do this even if we did not decide to stop here. Otherwise, we fail
			// to stop after a barrier if we were just woken from sleep. This is an issue since
			// that will cause us to stop at a "regular" location, which likely has the same
			// location as this barrier.
			if (type & Barrier:release)
				barrierStep = false;
		} else {
			// If we did not wish to wait, just trigger a check now. Otherwise we might miss parts
			// of this statement that happened before the barrier. We don't wait here, so don't
			// trigger a repaint.
			paused = true;
			// Set 'barrierStep' so we can detect explicit calls to 'pause'.
			barrierStep = true;
			owner.notifyChange(false);
			if (!barrierStep) {
				// Someone asked us to pause.
				barrierStep = false;
				wait();
			}
			barrierStep = false;
			paused = false;
		}

		// We always clear memory at a barrier, even if we did not wait.
		// TODO: It might be enough to clear reads at an acquire barrier.
		memory.clearAll();
	}

	// Called when we are about to enter a barrier function (the function itself is generally not
	// traced).
	void onNewFnBarrier(SrcPos pos, Str name, Barrier type, StackVar[] vars, Nat offset) {
		if (terminating)
			return;

		popFrames();
		var last = frames.last;
		if (last.lastOffset < offset)
			last.lastOffset = offset;

		callDepth++;
		if (pos.empty)
			pos = last.pos;
		frames.push(StackFrame(name, last.hints, vars, pos));

		try {
			// Also stop if stepping normally:
			barrierStep = true;
			onNewBarrier(SrcPos(), type, 0);
		} catch (Exception e) {
			callDepth--;
			throw e;
		}

		callDepth--;
		popFrames();
	}

	// Called before a function call to let us know the current position.
	void beforeCall(Nat offset) {
		if (terminating)
			return;

		// We don't detect cycles here, so only allow the offset to increase.
		var last = frames.last;
		if (last.lastOffset < offset)
			last.lastOffset = offset;
	}

	// Called when a monitored thread is about to return.
	// Returns 'false' if this event is not interesting to propagate.
	void onFunctionReturn(StackVar[] vars) {
		if (terminating)
			return;

		popFrames();

		var last = frames.last;
		last.variables = vars;
		last.returned = true;
		wait();

		memory.clearNew();
	}

	// Called when a new function was entered.
	MemTracker onFunctionEntered(Str name, SrcPos pos, progvis:data:ViewHints hints, StackVar[] vars) {
		popFrames();

		callDepth++;
		frames.push(StackFrame(name, hints, vars, pos));

		if (terminating)
			return memory;

		if (hints.pauseOnEntry())
			wait();

		memory;
	}

	// Called when a function is about to return.
	// Returns 'false' if this event is not interesting to propagate.
	Bool onFunctionExited() {
		// print("Function ${frames.last.function} exited.");

		// If this is the last frame, and it did not contain a return statement, we should pause one
		// time before the thread terminates, otherwise barrier steps will skip a bit too much in
		// some cases.
		if (!terminating & barrierStep) {
			if (callDepth == 1 & frames.any) {
				var last = frames.last;
				if (!last.returned & last.lastStop != last.pos) {
					wait();
				}
			}
		}

		if (callDepth > 0)
			callDepth--;

		popFrames();

		// Tell the system that we have exited if this is the last function in the stack.
		if (callDepth == 0) {
			if (rootAnonDepth == 0) {
				return true;
			}
		}
		return !terminating;
	}

	// Called when an anonymous function was entered.
	MemTracker onAnonFunctionEntered() {
		if (callDepth == 0)
			rootAnonDepth++;

		memory;
	}

	// Called when an anonymous function exited.
	Bool onAnonFunctionExited() {
		if (callDepth == 0)
			if (rootAnonDepth > 0)
				rootAnonDepth--;

		return (rootAnonDepth + callDepth) == 0;
	}

	// Called when function is about to throw an exception. Disables further tracing of the function.
	void onFatalException() {
		terminating = true;
	}

	// Make the thread sleep until something else wakes it. Used to implement synchronization primitives.
	// Note: 'value' is a RawPtr to avoid accidental deep copies due to thread switches.
	void lockSleep(unsafe:RawPtr value) {
		sleeping = true;
		if (frames.any) {
			var last = frames.last;
			StackVar var("For", value.asVariant());
			frames.push(StackFrame("Waiting...", last.hints, [var], last.pos));
		}

		wait();

		// Stop at the next thing, even if we are waiting for a barrier.
		barrierStep = false;

		// Remove any "waiting for" frame if needed.
		popFrames();
	}

	// Wake the thread again. Assumes that 'lockSleep' was called earlier.
	void lockWake() {
		sleeping = false;
		wake();
	}

	// Set the animation delay. Resumes the thread if it was stopped.
	void resume(Duration duration) {
		autoStep = duration;
		barrierStep = false;

		if (!sleeping)
			wake();
	}

	// Resume execution, stopping at the next location.
	void resume() {
		if (running | sleeping)
			return;

		autoStep = Duration();
		barrierStep = false;
		wake();
	}

	// Resume execution, but step at the next barrier.
	void resumeBarrier() {
		if (running | sleeping)
			return;

		barrierSpeed = autoStep = Duration();
		barrierStep = true;
		wake();
	}

	// Resume execution, but step at 'speed' intervals until the next barrier is reached.
	void resumeBarrier(Duration speed) {
		if (running | sleeping)
			return;

		autoStep = Duration();
		barrierSpeed = speed;
		barrierStep = true;
		wake();
	}

	// Pause the thread at the nearest convenient location.
	void pause() {
		autoStep = Duration();
		barrierStep = false;
	}

	// Terminate the thread.
	void terminate() {
		doTerminate = true;
		autoStep = Duration();
		wake();
		// Once more, just to be safe...
		sema.up();
	}

	// Decrease the stack frames until the proper depth is reached.
	private void popFrames() {
		while (frames.count > max(1n, callDepth))
			frames.pop();
	}

	// Determine whether or not we shall wait.
	private void wait() {
		// Remember if this 'wait' was due to us needing to sleep for a semaphore etc. If so,
		// we should not notify the owner when we wake, as that wake was not due to a user action.
		Bool wasSleeping = sleeping;
		paused = true;
		owner.notifyChange(true);
		if (wasSleeping | autoStep == Duration()) {
			running = false;
			sema.down();
		} else {
			sleep(autoStep);

			// If paused during sleep, keep waiting.
			if (autoStep == Duration()) {
				running = false;
				sema.down();
			}
		}
		// Just to be safe, this is set in "wake" as well.
		running = true;

		// Reset the busy wait flag.
		knownBusyWait = false;

		if (doTerminate) {
			paused = false;
			terminating = true;
			throw ExitError();
		} else if (!wasSleeping) {
			owner.notifyAdvance(threadId, barrierStep);
		}
		paused = false;
	}

	// Wake the thread. Calls sema.up if appropriate, and makes sure to clear the relevant flags as
	// soon as possible (since it is sometimes too late to re-set the running flag at a later time).
	private void wake() {
		if (running)
			return;

		knownBusyWait = false;
		running = true;
		sema.up();
	}
}

/**
 * A variable in a stack-frame.
 *
 * Note: We fill in this type directly from machine code, don't alter the layout!
 */
class StackVar {
	Str name;
	unsafe:RawPtr value;

	// If we need to properly destroy 'value' when we're done with it, this Variant will contain the
	// same value as 'value'. Otherwise, this variant is empty.
	Variant destroy;

	init(Str name) {
		init { name = name; }
	}

	init(Str name, Variant val) {
		init {
			name = name;
			destroy = val;
		}

		// Make sure to use the correct value.
		value = unsafe:RawPtr(destroy);
	}
}


/**
 * A stack frame of a thread.
 */
class StackFrame on Render {
	// Name of the function. (TODO: Add a SrcPos?)
	Str function;

	// View hints for this function. Used to scrape variables of the stack.
	progvis:data:ViewHints hints;

	// The current state of all variables. Ordered roughly as they appear in the source.
	StackVar[] variables;

	// Location in this frame.
	SrcPos pos;

	// Last regular step location in this frame. Barrier stops are not updated this way.
	SrcPos lastStop;

	// Last offset. So that we can detect loops.
	Nat lastOffset;

	// Did we return from this frame?
	Bool returned;

	// Create.
	init(Str name, progvis:data:ViewHints hints, StackVar[] vars, SrcPos pos) {
		init {
			function = name;
			hints = hints;
			variables = vars;
			pos = pos;
			returned = false;
		}
	}
}