use progvis:program;

/**
 * Memory access.
 *
 * Used to report whether data was read from and/or written to. Also reports which threads read and
 * wrote to the data for the model checker.
 *
 * The class makes a distinction between "new" reads/writes and "old" reads/writes. This is mainly
 * for the benefit of the visualization.
 *
 * 'error' is used to indicate if an error was present.
 */
value MemAccess {
	// Reads - 0=none, 1=old, 2>=new
	Byte read;
	// Writes - 0=none, 1=old, 2>=new
	Byte write;
	// Read error?
	Bool readError;
	// Write error?
	Bool writeError;

	// Exact reads+writes. This is mainly for the model checker. Contains the operations that are
	// important for the current memory checker, this may not overlap entirely with the values in
	// 'read' and 'write'. Stores thread ID:s of writing threads, followed by a zero, followed by
	// thread ID:s of reading threads.
	Nat[] threads;

	// Create.
	init() {
		init {}
	}

	// Clear everything.
	void clear() {
		read = 0;
		write = 0;
		readError = false;
		writeError = false;
		threads.clear();
	}

	// Any error?
	Bool error() {
		readError | writeError;
	}
}


/**
 * Memory model to use.
 */
enum MemoryChecks {
	// Don't use memory accesses at all in the visualization, not even for highlighting.
	none,

	// No checks at all, but visualizes accesses. Essentially sequential consistency.
	sequential,

	// Only check individual statements.
	statements,

	// Check between barriers. This is what the C/C++ standard requires (except for relaxed atomics)
	barriers,
}


// Create a memory check.
MemCheck create(MemoryChecks checks) {
	if (checks == MemoryChecks:none)
		ZeroMemCheck();
	else if (checks == MemoryChecks:sequential)
		NoMemCheck();
	else if (checks == MemoryChecks:statements)
		StmtMemCheck();
	else
		FullMemCheck();
}

/**
 * Object that keeps track of all reads and writes by threads during a traversal.
 *
 * It is possible to ask this object which threads read and write certain data, and to detect race
 * conditions from those observations. Collects information on any instances where reads and writes
 * cause race conditions.
 *
 * Abstract base class, there are implementations for the different models.
 */
class MemCheck {
	// Memory trackers for each of the threads currently alive. Mapped thread-id->tracker.
	protected Nat->MemTracker threads;

	// Error messages we produced.
	protected Str[] errors;

	// Add a thread.
	void add(Nat id, MemTracker tracker) {
		threads.put(id, tracker);
	}

	// Get errors, if any.
	ProgramError? error() {
		if (errors.any)
			return DataRaceError(errors);
		else
			return null;
	}

	// Query the memory access for some data. 'old' is used to inhibit old errors, for example.
	MemAccess query(MemAccess old, unsafe:RawPtr object, Nat offset, Nat size) : abstract;
}


/**
 * Mem check implementation that does not highlight anything. Mostly for programmatical use of
 * Progvis, where the highlights would be confusing.
 */
class ZeroMemCheck extends MemCheck {
	// Query the memory access for some data.
	MemAccess query(MemAccess old, unsafe:RawPtr object, Nat offset, Nat size) : override {
		return MemAccess();
	}
}


/**
 * Mem check implementation without checks, for sequential. Highlights reads and writes for clarity.
 */
class NoMemCheck extends MemCheck {
	// Query the memory access for some data.
	MemAccess query(MemAccess old, unsafe:RawPtr object, Nat offset, Nat size) : override {
		MemAccess result;

		// Check reads and writes for the visualization. We don't check correctness.
		for (k, v in threads) {
			if (v.newWrites.has(object, offset, size)) {
				result.write = 2;
			}
			if (v.newReads.has(object, offset, size)) {
				result.read = 2;
			}
		}

		// Note: We don't touch "threads" as we don't check for errors.

		result;
	}
}


/**
 * Mem check implementation that only considers new reads/writes.
 */
class StmtMemCheck extends MemCheck {
	// Query the memory access for some data.
	MemAccess query(MemAccess old, unsafe:RawPtr object, Nat offset, Nat size) : override {
		MemAccess result;

		// Check writes.
		for (k, v in threads) {
			if (v.newWrites.has(object, offset, size)) {
				result.write = 2;
				result.threads << k;
			}
		}

		if (result.threads.count > 1) {
			if (!old.writeError)
				dualWriteError(result.threads);
			result.writeError = true;
		}

		result.threads << 0;
		Nat writtenBy = result.threads[0];

		// Check reads.
		for (k, v in threads) {
			if (v.newReads.has(object, offset, size)) {
				if ((writtenBy != 0) & (writtenBy != k))
					result.readError = true;
				result.read = 2;
				result.threads << k;
			}
		}

		if (result.readError) {
			if (!old.readError) {
				readWriteError(result.threads);
			}
		}

		result;
	}

	// Add an error message concerning multiple writes.
	private void dualWriteError(Nat[] writes) {
		writes.sort();

		StrBuf result;
		result << "Threads " << join(writes, ", ") << " all wrote to the same value concurrently.";
		errors << result.toS;
	}

	// Add an error message concerning read-write errors.
	private void readWriteError(Nat[] threads) {
		Nat[] writes;
		Nat[] reads;

		Bool zero = false;
		for (v in threads) {
			if (v == 0) {
				zero = true;
			} else if (zero) {
				reads << v;
			} else {
				writes << v;
			}
		}

		writes.sort();
		reads.sort();

		StrBuf result;
		if (writes.count > 1)
			result << "Threads ";
		else
			result << "Thread ";
		result << join(writes, ", ") << " wrote to a value that ";
		if (reads.count > 1)
			result << "threads ";
		else
			result << "thread ";
		result << join(reads, ", ") << " read from concurrently.";
		errors << result.toS;
	}
}


/**
 * Object that keeps track of all reads and writes by threads during a traversal. Takes barrier
 * information into account.
 */
class FullMemCheck extends MemCheck {
	// Query the memory access for some data.
	// This is the fast-path: it does not allocate memory in the case no errors happen
	// (which is the normal case). It calls one of the error functions in case of an error.
	// These will have to re-do parts of the work in order to provide better error messages,
	// but as they are on the slow path, this is fine.
	MemAccess query(MemAccess old, unsafe:RawPtr object, Nat offset, Nat size) : override {
		MemAccess result;

		// Check writes.
		for (k, v in threads) {
			if (v.writes.has(object, offset, size)) {
				result.write |= 1;
				result.threads << k;

				if (v.newWrites.has(object, offset, size)) {
					result.write = 2;
				}
			}
		}

		if (result.threads.count > 1) {
			if (!old.writeError)
				dualWriteError(result.threads);
			result.writeError = true;
		}

		result.threads << 0;
		Nat writtenBy = result.threads[0];

		// Check reads.
		for (k, v in threads) {
			if (v.reads.has(object, offset, size)) {
				if ((writtenBy != 0) & (writtenBy != k))
					result.readError = true;
				result.read |= 1;
				result.threads << k;

				if (v.newReads.has(object, offset, size)) {
					result.read = 2;
				}
			}
		}

		if (result.readError) {
			if (!old.readError) {
				readWriteError(result.threads);
			}
		}

		result;
	}


	// Add an error message concerning multiple writes.
	private void dualWriteError(Nat[] writes) {
		writes.sort();

		StrBuf result;
		result << "Threads " << join(writes, ", ") << " all wrote to the same value concurrently.";
		errors << result.toS;
	}

	// Add an error message concerning read-write errors.
	private void readWriteError(Nat[] threads) {
		Nat[] writes;
		Nat[] reads;

		Bool zero = false;
		for (v in threads) {
			if (v == 0) {
				zero = true;
			} else if (zero) {
				reads << v;
			} else {
				writes << v;
			}
		}

		writes.sort();
		reads.sort();

		StrBuf result;
		if (writes.count > 1)
			result << "Threads ";
		else
			result << "Thread ";
		result << join(writes, ", ") << " wrote to a value that ";
		if (reads.count > 1)
			result << "threads ";
		else
			result << "thread ";
		result << join(reads, ", ") << " read from concurrently.";
		errors << result.toS;
	}

}