// Edit drawSquare.

#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <stdbool.h>

#include <klee/klee.h>

#ifndef drawSquare
#define drawSquare drawSquareReordered
#endif

typedef struct line {
	int x0, y0, x1, y1;
} line_t;

static line_t referenceLines[4];
static int referenceIdx = 0;

static line_t actualLines[4];
static int actualIdx = 0;

/* drawReferenceLine implementation. */
void drawReferenceLine(int x0, int y0, int x1, int y1) {
	if (referenceIdx < sizeof(referenceLines) / sizeof(line_t)) {
		referenceLines[referenceIdx++] = (line_t) {.x0 = x0, .y0 = y0, .x1 = x1, .y1 = y1};
	} else {
		exit(1);
	}
}

/* drawLine implementation. */
void drawLine(int x0, int y0, int x1, int y1) {
	if (actualIdx < sizeof(actualLines) / sizeof(line_t)) {
		actualLines[actualIdx++] = (line_t) {.x0 = x0, .y0 = y0, .x1 = x1, .y1 = y1};
	} else {
		exit(1);
	}
}

/* drawSquare implementations follow. */

static void drawSquareStudent1(int x, int y, int len) {
	if (x+len > 10){
		len = 10-x;
	}

	if (y+len > 10){
		len = 10-y;
	}

	drawLine(x, y, x+len, y);

	drawLine(x, y, x, y+len);

	drawLine(x+len, y, x+len, y+len);

	drawLine(x, y+len, x+len, y+len);
}

void drawSquareStudent2(int x, int y, int len)
{

	if(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) && len>0) 

	{

		drawLine(x, y, x+len, y);

		drawLine(x+len, y, x+len, y-len);

		drawLine(x+len, y-len, x, y-len);

		drawLine(x, y-len, x, y);

	}

	else

	{

		while(len<=0)

		{

			len++;

		}

		while(((x+len<10) && (x-len>= 0)) && ((y-len>0) && (y+len<=10)) == false)
		{

			len--;

		}

		drawLine(x, y, x+len, y);

		drawLine(x+len, y, x+len, y-len);

		drawLine(x+len, y-len, x, y-len);

		drawLine(x, y-len, x, y);
	}
}

void drawSquareStudent3(int x, int y, int len)
{
	if (0 <= x && x > 10 && 0 < y && y <= 10 && len > 0){

		drawLine(x, y, x + len, y);

		drawLine(x + len, y, x + len, y - len);
		drawLine(x + len, y - len, x, y - len);
		drawLine(x, y - len, x, y);
	}

	else if (x + len < 0|| y - len >= 10){

		len++;
		drawLine(x, y, x + len, y);

		drawLine(x + len, y, x + len, y - len);
		drawLine(x + len, y - len, x, y - len);
		drawLine(x, y - len, x, y);
	}

	else {

		len--;

		drawLine(x, y, x + len, y);

		drawLine(x + len, y, x + len, y - len);
		drawLine(x + len, y - len, x, y - len);
		drawLine(x, y - len, x, y);
	}
}

/* Example drawSquare that's just drawReferenceSquare reordered. */
static void drawSquareReordered(int x, int y, int len) {
	if (x+len > 10){
		len = 10-x;
	}

	if (y-len < 0){
		len = y;
	}

	drawLine(x, y-len, x, y);
	drawLine(x+len, y-len, x, y-len);
	drawLine(x, y, x+len, y);
	drawLine(x+len, y-len, x+len, y);
}

/** Draws the "reference" square. */
static void drawReferenceSquare(int x, int y, int len) {
	if (x+len > 10){
		len = 10-x;
	}

	if (y-len < 0){
		len = y;
	}

	drawReferenceLine(x, y, x+len, y);
	drawReferenceLine(x+len, y, x+len, y-len);
	drawReferenceLine(x+len, y-len, x, y-len);
	drawReferenceLine(x, y-len, x, y);
}

/** Compares that the drawn square is equal to the reference square. */
static int compareSquares(void) {
	int ret = 0;

	const int numLines = sizeof(actualLines) / sizeof(line_t);
	int confirmed[numLines] = {0};
	int numConfirmed = 0;
	for (int actualIdx = 0; actualIdx < numLines; actualIdx++) {
		line_t *actualLine = &actualLines[actualIdx];
		bool found = false;
		for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) {
			line_t *referenceLine = &referenceLines[referenceIdx];
			bool skipThis = false;
			for (int idx = 0; idx < numConfirmed; idx++) {
				if (confirmed[idx] == referenceIdx) {
					skipThis = true;
					break;
				}
			}

			if (!skipThis && (
						(actualLine->x0 == referenceLine->x0
						 && actualLine->y0 == referenceLine->y0
						 && actualLine->x1 == referenceLine->x1
						 && actualLine->y1 == referenceLine->y1) ||
						(actualLine->x1 == referenceLine->x0
						 && actualLine->y1 == referenceLine->y0
						 && actualLine->x0 == referenceLine->x1
						 && actualLine->y0 == referenceLine->y1))) {
				found = true;
				confirmed[numConfirmed++] = referenceIdx;
				break;
			}
		}
		if (!found) {
			ret = 1;
			break;
		}
	}

	return ret;
}

int main() {
	int x, y, len;
	klee_make_symbolic(&x, sizeof(x), "x");
	klee_make_symbolic(&y, sizeof(y), "y");
	klee_make_symbolic(&len, sizeof(len), "len");
	klee_assume(x >= 0 && x < 10 && y >= 0 && y < 10 && len > 0 && len <= 10);

	drawReferenceSquare(x, y, len);
	drawSquare(x, y, len);

	int ret = compareSquares();

	if (klee_is_replay()) {
		printf("Inputs: x=%d, y=%d, len=%d\n", x, y, len);

		const int numLines = sizeof(referenceLines) / sizeof(line_t);
		for (int referenceIdx = 0; referenceIdx < numLines; referenceIdx++) {
			line_t *referenceLine = &referenceLines[referenceIdx];
			printf("Reference: (%d, %d) -> (%d, %d)\n", referenceLine->x0, referenceLine->y0, referenceLine->x1, referenceLine->y1);
		}
		for (int actualIdx = 0; actualIdx < numLines; actualIdx++) {
			line_t *actualLine = &actualLines[actualIdx];
			printf("Actual: (%d, %d) -> (%d, %d)\n", actualLine->x0, actualLine->y0, actualLine->x1, actualLine->y1);
		}

		if (ret == 0) {
			printf("All outputs matched\n");
		} else {
			printf("Outputs mismatched\n");
		}
	}

	return 0;
}