A beginning is a very delicate time

.gitignore

@@ -0,0 +1,5 @@
+klee-*
+drawSquare
+drawSquare.bc
+*.swo
+*.swp

Makefile

@@ -0,0 +1,18 @@
+all: klee
+
+clean:
+	rm -f drawSquare.bc drawSquare
+
+klee: drawSquare.bc drawSquare
+	klee drawSquare.bc
+	for ktest in klee-last/*.ktest; do \
+		KTEST_FILE="$$ktest" ./drawSquare || true; \
+	done
+
+drawSquare.bc: drawSquare.c
+	clang -emit-llvm -c -g -o $@ $(CFLAGS) $^
+
+drawSquare: drawSquare.c
+	clang -Os -lkleeRuntest -o $@ $(CFLAGS) $^
+
+.PHONY: all clean klee

README.md

@@ -0,0 +1,4 @@
+# Getting started
+
+1. Run `nix-shell`
+2. Run `make clean klee CFLAGS=-DdrawSquare=drawSquareWeird` to run `drawSquareWeird`

drawSquare.c

@@ -0,0 +1,217 @@
+// 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, y0, x1, 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, y0, x1, y1};
+    } else {
+        exit(1);
+    }
+}
+
+/* drawSquare implementations follow. */
+
+void drawSquareWeird(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);
+    }
+}
+
+static void drawSquareAlmostCorrect(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);
+}
+
+/* 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;
+}

klee.nix

@@ -0,0 +1,39 @@
+{ stdenv
+, lib
+, fetchFromGitHub
+, cmake
+, llvmPackages_9
+, clang_9
+, z3
+, stp
+, cryptominisat
+, gperftools
+, sqlite
+, gtest
+, lit
+, debug ? false
+}:
+
+stdenv.mkDerivation rec {
+  pname = "klee";
+  version = "2.2";
+  src = fetchFromGitHub {
+    owner = "klee";
+    repo = "klee";
+    rev = "v${version}";
+    sha256 = "Ar3BKfADjJvvP0dI9+x/l3RDs8ncx4jmO7ol4MgOr4M=";
+  };
+  buildInputs = [ llvmPackages_9.llvm clang_9 z3 stp cryptominisat gperftools sqlite ];
+  nativeBuildInputs = [ cmake gtest lit ];
+  cmakeFlags = [
+    "-DCMAKE_BUILD_TYPE=${if debug then "Debug" else "Release"}"
+    "-DKLEE_RUNTIME_BUILD_TYPE=${if debug then "Debug" else "Release"}"
+    "-DENABLE_UNIT_TESTS=ON"
+    "-DGTEST_SRC_DIR=${gtest.src}"
+    "-DGTEST_INCLUDE_DIR=${gtest.src}/googletest/include"
+    "-DENABLE_POSIX_RUNTIME=ON"
+  ];
+  /*testPhase = ''
+    make systemtests unittests
+  '';*/
+}

shell.nix

@@ -0,0 +1,14 @@
+{ pkgs ? import (builtins.fetchTarball {
+  name = "nixpkgs-unstable";
+  url = https://github.com/NixOS/nixpkgs/archive/8f80568885d1b37cccbede85143c00711b19390c.tar.gz;
+  sha256 = "080cbcj4b08aa02qybf10pbf54cdvaxvgddx1w5gzrga1nacyilh";
+}) {}
+}:
+
+let
+  klee = pkgs.callPackage ./klee.nix {};
+in
+pkgs.stdenv.mkDerivation {
+  name = "ap-cs-klee";
+  buildInputs = with pkgs; [ klee clang_9 gnumake ];
+}